Theory SAS_Plus_Representation

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAS_Plus_Representation
imports State_Variable_Representation
begin

section "SAS+ Representation"

text ‹ We now continue by defining a concrete implementation of SAS+.›

text ‹ SAS+ operators and SAS+ problems again use records. In contrast to STRIPS, the operator 
effect is contracted into a single list however since we now potentially deal with more than two 
possible values for each problem variable. ›

record  ('variable, 'domain) sas_plus_operator = 
  precondition_of :: "('variable, 'domain) assignment list" 
  effect_of :: "('variable, 'domain) assignment list" 

record  ('variable, 'domain) sas_plus_problem =
  variables_of :: "'variable list" (‹(_𝒱+)› [1000] 999)
  operators_of :: "('variable, 'domain) sas_plus_operator list" (‹(_𝒪+)› [1000] 999)
  initial_of :: "('variable, 'domain) state" (‹(_I+)› [1000] 999)
  goal_of :: "('variable, 'domain) state" (‹(_G+)› [1000] 999)
  range_of :: "'variable ⇀ 'domain list"

definition range_of':: "('variable, 'domain) sas_plus_problem ⇒ 'variable ⇒ 'domain set"  (‹ℛ+ _ _› 52)
  where
  "range_of' Ψ v ≡
     (case sas_plus_problem.range_of Ψ v of None ⇒ {} 
           | Some as ⇒ set as)"

definition to_precondition 
  :: "('variable, 'domain) sas_plus_operator ⇒ ('variable, 'domain) assignment list" 
  where "to_precondition ≡ precondition_of"

definition to_effect 
  :: "('variable, 'domain) sas_plus_operator ⇒ ('variable, 'domain) Effect" 
  where "to_effect op ≡ [(v, a) . (v, a) ← effect_of op]"

type_synonym  ('variable, 'domain) sas_plus_plan 
  = "('variable, 'domain) sas_plus_operator list"

type_synonym  ('variable, 'domain) sas_plus_parallel_plan 
  = "('variable, 'domain) sas_plus_operator list list"

abbreviation  empty_operator 
  :: "('variable, 'domain) sas_plus_operator" (‹ρ›)
  where "empty_operator ≡ ⦇ precondition_of = [], effect_of = [] ⦈" 

definition is_valid_operator_sas_plus
  :: "('variable, 'domain) sas_plus_problem  ⇒ ('variable, 'domain) sas_plus_operator ⇒ bool" 
  where "is_valid_operator_sas_plus Ψ op ≡ let 
      pre = precondition_of op
      ; eff = effect_of op
      ; vs = variables_of Ψ
      ; D = range_of Ψ
    in list_all (λ(v, a). ListMem v vs) pre
      ∧ list_all (λ(v, a). (D v ≠ None) ∧ ListMem a (the (D v))) pre 
      ∧ list_all (λ(v, a). ListMem v vs) eff
      ∧ list_all (λ(v, a). (D v ≠ None) ∧ ListMem a (the (D v))) eff
      ∧ list_all (λ(v, a). list_all (λ(v', a'). v ≠ v' ∨ a = a') pre) pre
      ∧ list_all (λ(v, a). list_all (λ(v', a'). v ≠ v' ∨ a = a') eff) eff"

definition "is_valid_problem_sas_plus Ψ 
  ≡ let ops = operators_of Ψ
      ; vs = variables_of Ψ
      ; I = initial_of Ψ
      ; G = goal_of Ψ
      ; D = range_of Ψ
    in list_all (λv. D v ≠ None) vs
    ∧ list_all (is_valid_operator_sas_plus Ψ) ops 
    ∧ (∀v. I v ≠ None ⟷ ListMem v vs) 
    ∧ (∀v. I v ≠ None ⟶ ListMem (the (I v)) (the (D v)))
    ∧ (∀v. G v ≠ None ⟶ ListMem v (variables_of Ψ))
    ∧ (∀v. G v ≠ None ⟶ ListMem (the (G v)) (the (D v)))" 

definition is_operator_applicable_in
  :: "('variable, 'domain) state 
    ⇒ ('variable, 'domain) sas_plus_operator 
    ⇒ bool"
  where "is_operator_applicable_in s op 
    ≡ map_of (precondition_of op) ⊆m s" 

(* TODO rename execute_operator_in *)
definition execute_operator_sas_plus
  :: "('variable, 'domain) state 
    ⇒ ('variable, 'domain) sas_plus_operator
    ⇒ ('variable, 'domain) state" (infixl ‹⪢+› 52)
  where "execute_operator_sas_plus s op ≡ s ++ map_of (effect_of op)"

― ‹ Set up simp rules to keep use of local parameters transparent within proofs (i.e. 
automatically substitute definitions). ›
lemma[simp]: 
  "is_operator_applicable_in s op = (map_of (precondition_of op) ⊆m s)" 
  "s ⪢+ op = s ++ map_of (effect_of op)"
  unfolding initial_of_def goal_of_def variables_of_def range_of_def operators_of_def      
    SAS_Plus_Representation.is_operator_applicable_in_def
    SAS_Plus_Representation.execute_operator_sas_plus_def
  by simp+

lemma range_of_not_empty:
  "(sas_plus_problem.range_of Ψ v ≠ None ∧ sas_plus_problem.range_of Ψ v ≠ Some [])
    ⟷ (ℛ+ Ψ v) ≠ {}"
  apply (cases "sas_plus_problem.range_of Ψ v")
  by (auto simp add: SAS_Plus_Representation.range_of'_def)

lemma is_valid_operator_sas_plus_then:
  fixes Ψ::"('v,'d) sas_plus_problem"
  assumes "is_valid_operator_sas_plus Ψ op"
  shows "∀(v, a) ∈ set (precondition_of op). v ∈ set ((Ψ)𝒱+)"
    and "∀(v, a) ∈ set (precondition_of op). (ℛ+ Ψ v) ≠ {} ∧ a ∈ ℛ+ Ψ v" 
    and "∀(v, a) ∈ set (effect_of op). v ∈ set ((Ψ)𝒱+)"
    and "∀(v, a) ∈ set (effect_of op). (ℛ+ Ψ v) ≠ {} ∧ a ∈ ℛ+ Ψ v" 
    and "∀(v, a) ∈ set (precondition_of op). ∀(v', a') ∈ set (precondition_of op). v ≠ v' ∨ a = a'"
    and "∀(v, a) ∈ set (effect_of op). 
      ∀(v', a') ∈ set (effect_of op). v ≠ v' ∨ a = a'"
proof -
  let ?vs = "sas_plus_problem.variables_of Ψ" 
    and ?pre = "precondition_of op"
    and ?eff = "effect_of op"
    and ?D = "sas_plus_problem.range_of Ψ"
  have "∀(v, a)∈set ?pre. v ∈ set ?vs"
    and "∀(v, a)∈set ?pre.
          (?D v ≠ None) ∧
          a ∈ set (the (?D v))"
    and "∀(v, a)∈set ?eff. v ∈ set ?vs"
    and "∀(v, a)∈set ?eff.
          (?D v ≠ None) ∧
          a ∈ set (the (?D v))"
    and "∀(v, a)∈set ?pre.
          ∀(v', a')∈set ?pre. v ≠ v' ∨ a = a'"
    and "∀(v, a)∈set ?eff. 
      ∀(v', a')∈set ?eff. v ≠ v' ∨ a = a'"
    using assms
    unfolding is_valid_operator_sas_plus_def Let_def list_all_iff ListMem_iff 
    by meson+
  moreover have "∀(v, a) ∈ set ?pre. v ∈ set ((Ψ)𝒱+)"
    and "∀(v, a) ∈ set ?eff. v ∈ set ((Ψ)𝒱+)"
    and "∀(v, a) ∈ set ?pre. ∀(v', a') ∈ set ?pre. v ≠ v' ∨ a = a'"
    and "∀(v, a) ∈ set ?eff. ∀(v', a') ∈ set ?eff. v ≠ v' ∨ a = a'" 
    using calculation 
    unfolding variables_of_def
    by blast+
  moreover {
    have "∀(v, a) ∈ set ?pre. (?D v ≠ None) ∧ a ∈ set (the (?D v))"
      using assms 
      unfolding is_valid_operator_sas_plus_def Let_def list_all_iff ListMem_iff
      by argo
    hence "∀(v, a) ∈ set ?pre. ((ℛ+ Ψ v) ≠ {}) ∧ a ∈ ℛ+ Ψ v" 
      using range_of'_def 
      by fastforce
  }
  moreover {
    have "∀(v, a) ∈ set ?eff. (?D v ≠ None) ∧ a ∈ set (the (?D v))"
      using assms 
      unfolding is_valid_operator_sas_plus_def Let_def list_all_iff ListMem_iff
      by argo
    hence "∀(v, a) ∈ set ?eff. ((ℛ+ Ψ v) ≠ {}) ∧ a ∈ ℛ+ Ψ v" 
      using range_of'_def
      by fastforce
  }
  ultimately show "∀(v, a) ∈ set (precondition_of op). v ∈ set ((Ψ)𝒱+)"
    and "∀(v, a) ∈ set (precondition_of op). (ℛ+ Ψ v) ≠ {} ∧ a ∈ ℛ+ Ψ v" 
    and "∀(v, a) ∈ set (effect_of op). v ∈ set ((Ψ)𝒱+)"
    and "∀(v, a) ∈ set (effect_of op). (ℛ+ Ψ v) ≠ {} ∧ a ∈ ℛ+ Ψ v" 
    and "∀(v, a) ∈ set (precondition_of op). ∀(v', a') ∈ set (precondition_of op). v ≠ v' ∨ a = a'"
    and "∀(v, a) ∈ set (effect_of op). 
      ∀(v', a') ∈ set (effect_of op). v ≠ v' ∨ a = a'" 
    by blast+
qed

(* TODO can be replaced by proof for sublocale? *)
lemma is_valid_problem_sas_plus_then:
  fixes Ψ::"('v,'d) sas_plus_problem"
  assumes "is_valid_problem_sas_plus Ψ"
  shows "∀v ∈ set ((Ψ)𝒱+). (ℛ+ Ψ v) ≠ {}"
    and "∀op ∈ set ((Ψ)𝒪+). is_valid_operator_sas_plus Ψ op"
    and "dom ((Ψ)I+) = set ((Ψ)𝒱+)"
    and "∀v ∈ dom ((Ψ)I+). the (((Ψ)I+) v) ∈ ℛ+ Ψ v"
    and "dom ((Ψ)G+) ⊆ set ((Ψ)𝒱+)"
    and "∀v ∈ dom ((Ψ)G+). the (((Ψ)G+) v) ∈ ℛ+ Ψ v" 
proof -
  let ?vs = "sas_plus_problem.variables_of Ψ"
    and ?ops = "sas_plus_problem.operators_of Ψ"
    and ?I = "sas_plus_problem.initial_of Ψ"
    and ?G = "sas_plus_problem.goal_of Ψ"
    and ?D = "sas_plus_problem.range_of Ψ"
  {
    fix v 
    have "(?D v ≠ None ∧ ?D v ≠ Some []) ⟷ ((ℛ+ Ψ v) ≠ {})"
      by (cases "?D v"; (auto simp: range_of'_def))
  } note nb = this
  have nb1: "∀v ∈ set ?vs. ?D v ≠ None"
    and "∀op ∈ set ?ops. is_valid_operator_sas_plus Ψ op"
    and "∀v. (?I v ≠ None) = (v ∈ set ?vs)"
    and nb2: "∀v. ?I v ≠ None ⟶ the (?I v) ∈ set (the (?D v))"
    and "∀v. ?G v ≠ None ⟶ v ∈ set ?vs"
    and nb3: "∀v. ?G v ≠ None ⟶ the (?G v) ∈ set (the (?D v))"
    using assms 
    unfolding SAS_Plus_Representation.is_valid_problem_sas_plus_def Let_def 
      list_all_iff ListMem_iff 
    by argo+
  then have G3: "∀op ∈ set ((Ψ)𝒪+). is_valid_operator_sas_plus Ψ op"
    and G4: "dom ((Ψ)I+) = set ((Ψ)𝒱+)"
    and G5: "dom ((Ψ)G+) ⊆ set ((Ψ)𝒱+)"
    unfolding variables_of_def operators_of_def
    by auto+
  moreover {
    fix v
    assume "v ∈ set ((Ψ)𝒱+)"
    then have "?D v ≠ None"
      using nb1 
      by force+
  } note G6 = this
  moreover {
    fix v
    assume "v ∈ dom ((Ψ)I+)"
    moreover have "((Ψ)I+) v ≠ None"
      using calculation
      by blast+
    moreover {
      have "v ∈ set ((Ψ)𝒱+)"
        using G4 calculation(1)
        by argo
      then have "sas_plus_problem.range_of Ψ v ≠ None" 
        using range_of_not_empty
        unfolding range_of'_def
        using G6 
        by fast+
      hence "set (the (?D v)) = ℛ+ Ψ v" 
        by (simp add: ‹sas_plus_problem.range_of Ψ v ≠ None› option.case_eq_if range_of'_def)
    }
    ultimately have "the (((Ψ)I+) v) ∈ ℛ+ Ψ v"
      using nb2
      by force
  }
  moreover {
    fix v
    assume "v ∈ dom ((Ψ)G+)"
    then have "((Ψ)G+) v ≠ None"
      by blast
    moreover {
      have "v ∈ set ((Ψ)𝒱+)"
        using G5 calculation(1)
        by fast
      then have "sas_plus_problem.range_of Ψ v ≠ None" 
        using range_of_not_empty
        using G6
        by fast+
      hence "set (the (?D v)) = ℛ+ Ψ v" 
        by (simp add: ‹sas_plus_problem.range_of Ψ v ≠ None› option.case_eq_if range_of'_def)
    }
    ultimately have "the (((Ψ)G+) v) ∈ ℛ+ Ψ v"
      using nb3
      by auto
  }
  ultimately show "∀v ∈ set ((Ψ)𝒱+). (ℛ+ Ψ v) ≠ {}"
    and "∀op ∈ set((Ψ)𝒪+). is_valid_operator_sas_plus Ψ op"
    and "dom ((Ψ)I+) = set ((Ψ)𝒱+)"
    and "∀v ∈ dom ((Ψ)I+). the (((Ψ)I+) v) ∈ ℛ+ Ψ v"
    and "dom ((Ψ)G+) ⊆ set ((Ψ)𝒱+)"
    and "∀v ∈ dom ((Ψ)G+). the (((Ψ)G+) v) ∈ ℛ+ Ψ v"
    by blast+
qed

end