Session Verified_SAT_Based_AI_Planning

Theory List_Supplement

(*
  Author: Fred Kurz
*)
theory List_Supplement
imports Main
begin

lemma list_foot: 
  assumes "l  []" 
  obtains y ys where "l = ys @ [y]"
proof -
  {
    assume a: "l  []"
    have "y ys. l = ys @ [y]" 
      using a 
      proof (induction l)
        case (Cons a l)
        then show ?case 
          proof (cases "l = []")
            case True
            have "[] @ [a] = a # l" 
              using True
              by simp
            thus ?thesis 
              using Cons.prems(1)
              by simp
          next
            case False
            thm Cons
            then obtain y ys where "l = ys @ [y]" 
              using Cons.IH
              by blast
            then have "a # l = a # ys @ [y]" 
              by blast
            thus ?thesis
              by fastforce
          qed
      qed simp
  }
  thus ?thesis 
    using assms that 
    by blast
qed

lemma list_ex_intersection: "list_ex (λv. list_ex ((=) v) ys) xs  set xs  set ys  {}"
proof -
  {
    assume "list_ex (λv. list_ex ((=) v) ys) xs"
    then have "v  set xs. list_ex ((=) v) ys" 
      using list_ex_iff
      by fast
    moreover have "v. list_ex ((=) v) ys = (v'  set ys. v = v')" 
      using list_ex_iff
      by blast
    ultimately have "v  set xs. (v'  set ys. v = v')"
      by blast
    then obtain v v' where "v  set xs" and "v'  set ys" and "v = v'"
      by blast
    then have "set xs  set ys  {}"
      by blast
  } moreover {
    assume  "set xs  set ys  {}"
    then obtain v v' where "v  set xs" and "v'  set ys" and "v = v'"
      by blast
    then have "list_ex (λv. v'  set ys. v = v') xs" 
      using list_ex_iff 
      by fast
    moreover have "v. (v'  set ys. v = v') = list_ex ((=) v) ys" 
      using list_ex_iff
      by blast
    ultimately have "list_ex (λv. list_ex ((=) v) ys) xs" 
      by force
  } ultimately show ?thesis
    by blast
qed

lemma length_map_upt: "length (map f [a..<b]) = b - a" 
proof -
  have "length [a..<b] = b - a" 
    using length_upt
    by blast
  moreover have "length (map f [a..<b]) = length [a..<b]"
    by simp
  ultimately show ?thesis
    by argo
qed

lemma not_list_ex_equals_list_all_not: "(¬list_ex P xs) = list_all (λx. ¬P x) xs" 
proof -
  have "(¬list_ex P xs) = (¬Bex (set xs) P)"
    using list_ex_iff 
    by blast
  also have " = Ball (set xs) (λx. ¬P x)"
    by blast 
  finally show ?thesis
    by (simp add: Ball_set_list_all)
qed

lemma element_of_subseqs_then_subset:
  assumes "l  set (subseqs l')" 
  shows"set l  set l'" 
  using assms
proof (induction l' arbitrary: l)
  case (Cons x l')
  have "set (subseqs (x # l')) = (Cons x) ` set (subseqs l')  set (subseqs l')"
    unfolding subseqs.simps(2) Let_def set_map set_append..
  then consider (A) "l  (Cons x) ` set (subseqs l')"
    | (B) "l  set (subseqs l')" 
    using Cons.prems
    by blast
  thus ?case 
    proof (cases)
      case A
      then obtain l'' where "l''  set (subseqs l')" and "l = x # l''" 
        by blast
      moreover have "set l''  set l'" 
        using Cons.IH[of l'', OF calculation(1)].
      ultimately show ?thesis 
        by auto
    next
      case B
      then show ?thesis 
        using Cons.IH
        by auto
    qed
qed simp

(* TODO rewrite using list comprehension ‹embed xs = [[x]. x ← xs]› *)
text ‹ Embed a list into a list of singleton lists. ›
primrec embed :: "'a list  'a list list" 
  where "embed [] = []" 
  | "embed (x # xs) = [x] # embed xs"

lemma set_of_embed_is: "set (embed xs) = { [x] | x. x  set xs }" 
  by (induction xs; force+)

lemma concat_is_inverse_of_embed:
  "concat (embed xs) = xs"
  by (induction xs; simp)

lemma embed_append[simp]: "embed (xs @ ys) = embed xs @ embed ys"
proof (induction xs)
  case (Cons x xs)
  have "embed (x # xs @ ys) = [x] # embed (xs @ ys)" 
    try0
    by simp
  also have " = [x] # (embed xs @ embed ys)" 
    using Cons.IH 
    by simp
  finally show ?case 
    by fastforce
qed simp

end

Theory Map_Supplement

(*
  Author: Fred Kurz
*)
theory Map_Supplement
imports Main
begin

lemma map_of_defined_if_constructed_from_list_of_constant_assignments:
  "l = map (λx. (x, a)) xs  x  set xs. (map_of l) x = Some a" 
proof (induction xs arbitrary: l)
  case (Cons x xs)
  let ?l' = "map (λv. (v, a)) xs"
  from Cons.prems(1) have "l = (x, a) # map (λv. (v, a)) xs" 
    by force
  moreover have "v  set xs. (map_of ?l') v = Some a" 
    using Cons.IH[where l="?l'"]
    by blast
  ultimately show ?case
    by auto
qed auto

― ‹ NOTE Function graph is the set of pairs (x, f x) for a (total) function f. ›
― ‹ TODO Remove the first premise (follows from the second). ›
lemma map_of_from_function_graph_is_some_if:
  fixes f :: "'a  'b"
  assumes "set xs  {}"
   and "x  set xs"
  shows "(map_of (map (λx. (x, f x)) xs)) x = Some (f x)" 
  using assms 
proof (induction xs arbitrary: f x)
  ― ‹ NOTE Base case follows trivially from violation of assumption set xs ≠ {}›. ›
  case (Cons a xs)
    thm Cons
    let ?m = "map_of (map (λx. (x, f x)) xs)" 
    have a: "map_of (map (λx. (x, f x)) (Cons a xs)) = ?m(a  f a)" 
      unfolding map_of_def
      by simp
    thus ?case 
      proof(cases "x = a")
        case False
        thus ?thesis 
        proof (cases "set xs = {}")
            ― ‹ NOTE Follows from contradiction (x ∈ set (Cons a xs) ∧ set xs = {} ∧ x ≠ a ≡ ⊥›)›
            case True
            thus ?thesis 
              using Cons.prems(2)
              by fastforce
          next
            case False
            then have "x  set xs" 
              using x  a Cons.prems(2)
              by fastforce
            moreover have "map_of (map (λx. (x, f x)) (Cons a xs)) x = ?m x"
              using x  a
              by fastforce
            ultimately show ?thesis 
              using Cons.IH[OF False]
              by presburger
          qed 
      qed force
    qed blast

lemma foldl_map_append_is_some_if:
  assumes "b x = Some y  (m  set ms. m x = Some y)" 
    and "m'  set ms. m' x = Some y  m' x = None"
  shows "foldl (++) b ms x = Some y" 
using assms
proof (induction ms arbitrary: b)
  ― ‹ NOTE Induction base case violates first assumption (we have at least one element in ms 
    and hence ms ≠ []›). ›
  case (Cons a ms)
  consider (b_is_some_y) "b x = Some y" 
    | (m_is_some_y) "m  set (a # ms). m x = Some y" 
    using Cons.prems(1)
    by blast
  hence "(b ++ a) x = Some y  (mset ms. m x = Some y)"
    proof (cases)
      case b_is_some_y
      moreover have "a x = Some y  a x = None" 
        using Cons.prems(2)
        by simp
      ultimately show ?thesis 
        using map_add_Some_iff[of b a x y]
        by blast
    next
      case m_is_some_y
      then show ?thesis 
        proof (cases "a x = Some y")
          case False 
          then obtain m where "m  set ms" and "m x = Some y" 
            using m_is_some_y try0
            by auto
          thus ?thesis
            by blast
        qed simp
    qed
  moreover have "m'  set ms. m' x = Some y  m' x = None"  
    using Cons.prems(2)
    by fastforce
  ultimately show ?case using Cons.IH[where b="b ++ a"]
    by simp
qed auto

(* TODO "∀(v, a) ∈ set l. ∀(v', a') ∈ set l. v ≠ v' ∨ a = a'" ↝
  "∀(v', a') ∈ set l. v ≠ v' ∨ a = a'" (this is too strong; we only consider (v, a), i.e. fixed v)
*)
(* TODO isn't this the same as map_of_is_SomeI? *)
lemma map_of_constant_assignments_defined_if:
  assumes "(v, a)  set l. (v', a')  set l. v  v'  a = a'"
    and "(v, a)  set l" 
  shows "map_of l v = Some a" 
  using assms
proof (induction l)
  case (Cons x l)
  thm Cons
  then show ?case 
    proof (cases "x = (v, a)")
      case False
      have v_a_in_l: "(v, a)  set l" 
        using Cons.prems(2) False
        by fastforce
      {
        have "(v, a)  set l. (v', a')  set l. v  v'  a = a'"
          using Cons.prems(1)
          by auto 
        hence "map_of l v = Some a"
          using Cons.IH v_a_in_l
          by linarith
      } note ih = this
      {
        have "x  set (x # l)" 
          by auto
        hence "fst x  v  snd x = a" 
          using Cons.prems(1) v_a_in_l
          by fastforce
      } note nb = this
      ― ‹ NOTE If @{text "fst x = v"} then @{text "snd x = a"} by fact @{text "nb"}; moreover if 
        on the other hand @{text "fst x ≠ v"}, then the proposition follows from the induction 
        hypothesis since @{text "map_of (x # l) v = map_of l v"} in that case. ›
      thus ?thesis
        using ih nb
        by (cases "fst x = v") fastforce+
    qed simp
qed fastforce

end

Theory CNF_Supplement

(*
  Author: Fred Kurz
*)
theory CNF_Supplement
  imports "Propositional_Proof_Systems.CNF_Formulas_Sema"
begin

(* TODO fix warnings *)

fun is_literal_formula 
  where "is_literal_formula (Atom _) = True"
  | "is_literal_formula (¬(Atom _)) = True" 
  | "is_literal_formula _ = False" 

fun literal_formula_to_literal :: "'a formula  'a literal"
  where "literal_formula_to_literal (Atom a) = a+"
  | "literal_formula_to_literal (¬(Atom a)) = a¯" 

lemma is_literal_formula_then_cnf_is_singleton_clause:
  assumes "is_literal_formula f"
  obtains C where "cnf f = { C }" 
proof -
  consider (f_is_positive_literal) "a. f = Atom a" 
    | (f_is_negative_literal) "a. f = ¬(Atom a)"
    using assms is_literal_formula.elims(2)[of f]
    by meson 
  then have "C. cnf f = { C }"
    proof (cases)
      case f_is_positive_literal
      then obtain a where "f = Atom a" 
        by force
      then have "cnf f = {{ a+ }}"
        by force
      thus ?thesis
        by simp
    next
      case f_is_negative_literal
      then obtain a where "f = ¬(Atom a)" 
        by force
      then have "cnf f = {{ a¯ }}"
        by force
      thus ?thesis
        by simp
    qed
  thus ?thesis 
    using that
    by presburger 
qed

lemma literal_formula_to_literal_is_inverse_of_form_of_lit: 
  "literal_formula_to_literal (form_of_lit L) = L"
  by (cases L, simp+)

lemma is_nnf_cnf: 
  assumes "is_cnf F" 
    shows "is_nnf F" 
  using assms 
proof (induction F)
  case (Or F1 F2)
  have "is_disj (F1  F2)"
    using Or.prems is_cnf.simps(5)
    by simp
  thus ?case 
    using disj_is_nnf 
    by blast
qed simp+

lemma cnf_of_literal_formula:
  assumes "is_literal_formula f" 
  shows "cnf f = {{ literal_formula_to_literal f }}"
proof -
  consider (f_is_positive_literal) "a. f = Atom a"
    | (f_is_negative_literal) "a. f = (¬(Atom a))"
    using assms is_literal_formula.elims(2)[of f "a. f = Atom a"]
       is_literal_formula.elims(2)[of f "a. f = (¬(Atom a))"]
    by blast
  thus ?thesis 
    by(cases, force+)
qed

lemma is_cnf_foldr_and_if: 
  assumes "f  set fs. is_cnf f"
  shows "is_cnf (foldr () fs (¬))" 
  using assms
proof (induction fs)
  case (Cons f fs)
  have "foldr () (f # fs) (¬) = f  (foldr () fs (¬))" 
    by simp
  moreover {
    have "f  set fs. is_cnf f" 
      using Cons.prems
      by force
    hence "is_cnf (foldr () fs (¬))" 
      using Cons.IH
      by blast
  }
  moreover have "is_cnf f" 
    using Cons.prems
    by simp
  ultimately show ?case
    by simp
qed simp

end

Theory CNF_Semantics_Supplement

(*
  Author: Fred Kurz
*)
theory CNF_Semantics_Supplement
  imports "Propositional_Proof_Systems.CNF_Formulas_Sema" "CNF_Supplement"
begin

lemma not_model_if_exists_unmodeled_singleton_clause:
  assumes "is_cnf F"
    and "{L}  cnf F"
    and "¬lit_semantics ν L" 
  shows "¬ν  F" 
proof (rule ccontr)
  assume "¬¬ν  F"  
  then have a: "ν  F"
    by blast
  moreover have "is_nnf F" 
    using is_nnf_cnf[OF assms(1)]
    by simp 
  moreover {
    let ?C = "{L}" 
    have "¬(L'. L'  ?C  lit_semantics ν L')" 
      using assms(3)
      by fast
    then have "¬(C  cnf F. L. L  C  lit_semantics ν L)"
      using assms(2)
      by blast
    hence "¬cnf_semantics ν (cnf F)" 
      unfolding cnf_semantics_def clause_semantics_def
      by fast
  }
  ultimately have "¬ ν  F" 
    using cnf_semantics
    by blast
  thus False 
    using a 
    by blast
qed

― ‹ NOTE This follows by contraposition from the previous lemma 
not_model_if_exists_unmodeled_singleton_clause›. ›
corollary model_then_all_singleton_clauses_modelled:
  assumes "is_cnf F"
    and "{L}  cnf F"
    and "ν  F" 
  shows "lit_semantics ν L" 
  using not_model_if_exists_unmodeled_singleton_clause[OF assms(1, 2)] assms(3)
  by blast

― ‹ NOTE This is essentially the ⇒› direction of the compactness theorem when treating CNFs as sets
of formulas (sets of disjunctions in this case). ›
lemma model_for_cnf_is_model_of_all_subsets:
  assumes "cnf_semantics ν "
    and "ℱ'  " 
  shows "cnf_semantics ν ℱ'" 
proof -
  {
    fix C
    assume "C  ℱ'"
    then have "C  " 
      using assms(2)
      by blast
    then have "clause_semantics ν C" 
      using assms(1)
      unfolding cnf_semantics_def
      by blast
  }
  thus ?thesis 
    unfolding cnf_semantics_def
    by blast
qed

lemma cnf_semantics_monotonous_in_cnf_subsets_if:
  assumes "𝒜  Φ" 
    and "is_cnf Φ" 
    and "cnf Φ'  cnf Φ" 
  shows "cnf_semantics 𝒜 (cnf Φ')"
proof -
  {
    have "is_nnf Φ"
      using is_nnf_cnf[OF assms(2)].
    hence "cnf_semantics 𝒜 (cnf Φ)" 
      using cnf_semantics assms(1)
      by blast
  }
  thus ?thesis 
    using model_for_cnf_is_model_of_all_subsets[OF _ assms(3)]
    by simp
qed

corollary modelling_relation_monotonous_in_cnf_subsets_if:
  assumes "𝒜  Φ" 
    and "is_cnf Φ" 
    and "is_cnf Φ'"
    and "cnf Φ'  cnf Φ" 
  shows "𝒜  Φ'"
proof -
  have "cnf_semantics 𝒜 (cnf Φ')" 
    using cnf_semantics_monotonous_in_cnf_subsets_if[OF assms(1, 2, 4)].
  thus ?thesis
    using cnf_semantics is_nnf_cnf[OF assms(3)]
    by blast  
qed

― ‹ NOTE Show that any clause C› containing a subset C› for which all literals
  L› evaluate to False› for the given valuation 𝒜›, then the clause
  semantics evaluation can be reduced to the set C - C'› where all literals of 
  C'› have been removed. ›
lemma lit_semantics_reducible_to_subset_if:
  assumes "C'  C"
    and "L  C'. ¬lit_semantics 𝒜 L"
  shows "clause_semantics 𝒜 C = clause_semantics 𝒜 (C - C')"
  unfolding clause_semantics_def
  using assms
  by fast

end

Theory State_Variable_Representation

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory State_Variable_Representation
  imports Main "Propositional_Proof_Systems.Formulas" "Propositional_Proof_Systems.Sema" 
    "Propositional_Proof_Systems.CNF"
begin
section "State-Variable Representation"

text ‹ Moving on to the Isabelle implementation of state-variable representation, we
first add a more concrete representation of states using Isabelle maps. To this end, we add a 
type synonym \isaname{state} for maps of variables to values. 
Since maps can be conveniently constructed from lists of 
assignments---i.e. pairs (v, a) :: 'variable × 'domain›---we also add a corresponding type 
synonym \isaname{assignment}. ›

type_synonym ('variable, 'domain) state = "'variable  'domain"

type_synonym ('variable, 'domain) assignment = "'variable × 'domain"

text ‹ Effects and effect condition (see \autoref{sub:state-variable-representation}) are 
implemented in a straight forward manner using a datatype with constructors for each effect type.›

type_synonym ('variable, 'domain) Effect = "('variable × 'domain) list"

end

Theory STRIPS_Representation

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

section "STRIPS Representation"

(*<*)
type_synonym  ('variable) strips_state = "('variable, bool) state"
(*>*)
text ‹ We start by declaring a \isakeyword{record} for STRIPS operators.
This which allows us to define a data type and automatically generated selector operations. 
\footnote{For the full reference on records see \cite[11.6, pp.260-265]{wenzel--2018}} 

The record specification given below closely resembles the canonical representation of
STRIPS operators with fields corresponding to precondition, add effects as well as delete effects.›

record  ('variable) strips_operator = 
  precondition_of :: "'variable list" 
  add_effects_of :: "'variable list" 
  delete_effects_of :: "'variable list" 

― ‹ This constructor function is sometimes a more descriptive and replacement for the record 
syntax and can moreover be helpful if the record syntax leads to type ambiguity.›
abbreviation  operator_for
  :: "'variable list  'variable list  'variable list  'variable strips_operator"
  where "operator_for pre add delete   
    precondition_of = pre
    , add_effects_of = add
    , delete_effects_of = delete " 

definition  to_precondition
  :: "'variable strips_operator  ('variable, bool) assignment list"
  where "to_precondition op  map (λv. (v, True)) (precondition_of op)" 

definition  to_effect
  :: "'variable strips_operator  ('variable, bool) Effect" 
  where "to_effect op =  [(va, True). va  add_effects_of op] @ [(vd, False). vd  delete_effects_of op]"

text ‹ Similar to the operator definition, we use a record to represent STRIPS problems and specify
fields for the variables, operators, as well as the initial and goal state. ›

record  ('variable) strips_problem =
  variables_of :: "'variable list" ("(_𝒱)" [1000] 999)
  operators_of :: "'variable strips_operator list" ("(_𝒪)" [1000] 999)
  initial_of :: "'variable strips_state" ("(_I)" [1000] 999)
  goal_of :: "'variable strips_state" ("(_G)" [1000] 999)

value  "stop" (* Tell document preparation to stop collecting for the last tag *)
(*<*)
― ‹ This constructor function is sometimes a more descriptive and replacement for the record 
syntax and can moreover be helpful if the record syntax leads to type ambiguity.›
(* TODO change identifier gs ~> G *)
abbreviation problem_for 
  :: "'variable list 
   'variable strips_operator list 
   'variable strips_state 
   'variable strips_state
   ('variable) strips_problem"
  where "problem_for vs ops I gs   
    variables_of = vs
    , operators_of = ops
    , initial_of = I
    , goal_of = gs " 

type_synonym ('variable) strips_plan = "'variable strips_operator list"

type_synonym ('variable) strips_parallel_plan = "'variable strips_operator list list"

definition is_valid_operator_strips
  :: "'variable strips_problem  'variable strips_operator  bool"
  where "is_valid_operator_strips Π op  let 
      vs = variables_of Π 
      ; pre = precondition_of op
      ; add = add_effects_of op
      ; del = delete_effects_of op
    in list_all (λv. ListMem v vs) pre 
     list_all (λv. ListMem v vs) add
     list_all (λv. ListMem v vs) del
     list_all (λv. ¬ListMem v del) add
     list_all (λv. ¬ListMem v add) del"

definition "is_valid_problem_strips Π
   let ops = operators_of Π
      ; vs = variables_of Π
      ; I = initial_of Π
      ; G = goal_of Π
    in  list_all (is_valid_operator_strips Π) ops 
     (v. I v  None  ListMem v vs) 
     (v. G v  None  ListMem v vs)"

definition is_operator_applicable_in
  :: "'variable strips_state  'variable strips_operator  bool"
  where "is_operator_applicable_in s op  let p = precondition_of op in
    list_all (λv. s v = Some True) p"

(* TODO effect_to_strips and effect_to_assignments could just be removed if we prove a lemma 
  showing the equivalence to effcond semantics.*)
definition effect__strips 
  :: "'variable strips_operator  ('variable, bool) Effect"
  where "effect__strips op 
    = 
      map (λv. (v, True)) (add_effects_of op)
      @ map (λv. (v, False)) (delete_effects_of op)"

definition effect_to_assignments 
  where "effect_to_assignments op  effect__strips op"
(*>*)

text ‹ As discussed in \autoref{sub:serial-sas-plus-and-parallel-strips}, the effect of
a STRIPS operator can be normalized to a conjunction of atomic effects. We can therefore construct 
the successor state by simply converting the list of add effects to assignments to term‹True› resp. 
converting the list of delete effect to a list of assignments to term‹False› and then adding the 
map corresponding to the assignments to the given state terms as shown below in definition 
\ref{isadef:operator-execution-strips}. 
\footnote{Function \path{effect_to_assignments} converts the operator effect to a list of 
assignments. }›

definition  execute_operator
  :: "'variable strips_state 
     'variable strips_operator 
     'variable strips_state" (infixl "" 52)
  where "execute_operator s op
     s ++ map_of (effect_to_assignments op)"

end

Theory STRIPS_Semantics

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory STRIPS_Semantics
  imports "STRIPS_Representation"
    "List_Supplement"
    "Map_Supplement"
begin
section "STRIPS Semantics"
text ‹ Having provided a concrete implementation of STRIPS and a corresponding locale strips›, we
can now continue to define the semantics of serial and parallel STRIPS plan execution (see
\autoref{sub:serial-sas-plus-and-parallel-strips} and
\autoref{sub:parallel-sas-plus-and-parallel-strips}). ›
subsection "Serial Plan Execution Semantics"

text ‹ Serial plan execution is defined by primitive recursion on the plan.
Definition \autoref{isadef:execute_serial_plan} returns the given state if the state argument does
note satisfy the precondition of the next operator in the plan.
Otherwise it executes the rest of the plan on the successor state term‹execute_operator s op of
the given state and operator. ›

primrec  execute_serial_plan
  where "execute_serial_plan s [] = s"
  | "execute_serial_plan s (op # ops)
    = (if is_operator_applicable_in s op
      then execute_serial_plan (execute_operator s op) ops
      else s
  )"

text ‹ Analogously, a STRIPS trace either returns the singleton list containing only the given
state in case the precondition of the next operator in the plan is not satisfied. Otherwise, the
given state is prepended to trace of the rest of the plan for the successor state of executing the
next operator on the given state. ›

fun  trace_serial_plan_strips
  :: "'variable strips_state  'variable strips_plan  'variable strips_state list"
  where "trace_serial_plan_strips s [] = [s]"
  | "trace_serial_plan_strips s (op # ops)
      = s # (if is_operator_applicable_in s op
        then trace_serial_plan_strips (execute_operator s op) ops
        else [])"

text ‹ Finally, a serial solution is a plan which transforms a given problems initial state into
its goal state and for which all operators are elements of the problem's operator list. ›

definition  is_serial_solution_for_problem
  where "is_serial_solution_for_problem Π π
     (goal_of Π) m execute_serial_plan (initial_of Π) π
       list_all (λop. ListMem op (operators_of Π)) π"

lemma is_valid_problem_strips_initial_of_dom:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
  shows "dom ((Π)I) = set ((Π)𝒱)"
  proof -
    {
      let ?I = "strips_problem.initial_of Π"
      let ?vs = "strips_problem.variables_of Π"
      fix v
      have "?I v  None  ListMem v ?vs"
        using assms(1)
        unfolding is_valid_problem_strips_def
        by meson
      hence "v  dom ?I  v  set ?vs"
        using ListMem_iff
        by fast
    }
    thus ?thesis
      by auto
  qed

lemma is_valid_problem_dom_of_goal_state_is:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
  shows "dom ((Π)G)  set ((Π)𝒱)"
  proof -
    let ?vs = "strips_problem.variables_of Π"
    let ?G = "strips_problem.goal_of Π"
    have nb: "v. ?G v  None  ListMem v ?vs"
      using assms(1)
      unfolding is_valid_problem_strips_def
      by meson
    {
      fix v
      assume "v  dom ?G"
      then have "?G v  None"
        by blast
      hence "v  set ?vs"
        using nb
        unfolding ListMem_iff
        by blast
    }
    thus ?thesis
      by auto
  qed

lemma is_valid_problem_strips_operator_variable_sets:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "op  set ((Π)𝒪)"
  shows "set (precondition_of op)  set ((Π)𝒱)"
    and "set (add_effects_of op)  set ((Π)𝒱)"
    and "set (delete_effects_of op)  set ((Π)𝒱)"
    and "disjnt (set (add_effects_of op)) (set (delete_effects_of op))"
  proof -
    let ?ops = "strips_problem.operators_of Π"
      and ?vs = "strips_problem.variables_of Π"
    have "list_all (is_valid_operator_strips Π) ?ops"
      using assms(1)
      unfolding is_valid_problem_strips_def
      by meson
    moreover have "v  set (precondition_of op). v  set ((Π)𝒱)"
      and "v  set (add_effects_of op). v  set ((Π)𝒱)"
      and "v  set (delete_effects_of op). v  set ((Π)𝒱)"
      and "v  set (add_effects_of op). v  set (delete_effects_of op)"
      and "v  set (delete_effects_of op). v  set (add_effects_of op)"
      using assms(2) calculation
      unfolding is_valid_operator_strips_def list_all_iff Let_def ListMem_iff
      using variables_of_def
      by auto+
    ultimately show "set (precondition_of op)  set ((Π)𝒱)"
      and "set (add_effects_of op)  set ((Π)𝒱)"
      and "set (delete_effects_of op)  set ((Π)𝒱)"
      and "disjnt (set (add_effects_of op)) (set (delete_effects_of op))"
      unfolding disjnt_def
      by fast+
  qed

lemma effect_to_assignments_i:
  assumes "as = effect_to_assignments op"
  shows "as =  (map (λv. (v, True)) (add_effects_of op)
      @ map (λv. (v, False)) (delete_effects_of op))"
  using assms
  unfolding effect_to_assignments_def effect__strips_def
  by auto

lemma effect_to_assignments_ii:
  ― ‹ NOTE effect_to_assignments› can be simplified drastically given that only atomic effects
  and the add-effects as well as delete-effects lists only consist of variables.›
  assumes "as = effect_to_assignments op"
  obtains as1 as2
  where "as = as1 @ as2"
    and "as1 = map (λv. (v, True)) (add_effects_of op)"
    and "as2 = map (λv. (v, False)) (delete_effects_of op)"
  by (simp add: assms effect__strips_def effect_to_assignments_def)

― ‹ NOTE Show that for every variable v› in either the add effect list or the delete effect
list, there exists an assignment in  \isaname{effect_to_assignments op} representing setting v› to
true respectively setting v› to false. Note that the first assumption amounts to saying that
the add effect list is not empty. This also requires us to split lemma
\isaname{effect_to_assignments_iii} into two separate lemmas since add and delete effect lists are
not required to both contain at least one variable simultaneously. ›
lemma effect_to_assignments_iii_a:
  fixes v
  assumes "v  set (add_effects_of op)"
    and "as = effect_to_assignments op"
  obtains a where "a  set as" "a = (v, True)"
  proof -
    let ?add_assignments = "(λv. (v, True)) ` set (add_effects_of op)"
    let ?delete_assignments = "(λv. (v, False)) ` set (delete_effects_of op)"
    obtain as1 as2
      where a1: "as = as1 @ as2"
        and a2: "as1 = map (λv. (v, True)) (add_effects_of op)"
        and a3: "as2 = map (λv. (v, False)) (delete_effects_of op)"
      using assms(2) effect_to_assignments_ii
      by blast
    then have b: "set as
      = ?add_assignments  ?delete_assignments"
      by auto
    ― ‹ NOTE The existence of an assignment as proposed can be shown by the following sequence of
      set inclusions. ›
    {
      from b have "?add_assignments  set as"
        by blast
      moreover have "{(v, True)}  ?add_assignments"
        using assms(1) a2
        by blast
      ultimately have "a. a  set as  a = (v, True)"
        by blast
    }
    then show ?thesis
      using that
      by blast
  qed

lemma effect_to_assignments_iii_b:
  ― ‹ NOTE This proof is symmetrical to the one above. ›
  fixes v
  assumes "v  set (delete_effects_of op)"
    and "as = effect_to_assignments op"
  obtains a where "a  set as" "a = (v, False)"
  proof -
    let ?add_assignments = "(λv. (v, True)) ` set (add_effects_of op)"
    let ?delete_assignments = "(λv. (v, False)) ` set (delete_effects_of op)"
    obtain as1 as2
      where a1: "as = as1 @ as2"
        and a2: "as1 = map (λv. (v, True)) (add_effects_of op)"
        and a3: "as2 = map (λv. (v, False)) (delete_effects_of op)"
      using assms(2) effect_to_assignments_ii
      by blast
    then have b: "set as
      = ?add_assignments  ?delete_assignments"
      by auto
    ― ‹ NOTE The existence of an assignment as proposed can be shown by the following sequence of
      set inclusions. ›
    {
      from b have "?delete_assignments  set as"
        by blast
      moreover have "{(v, False)}  ?delete_assignments"
        using assms(1) a2
        by blast
      ultimately have "a. a  set as  a = (v, False)"
        by blast
    }
    then show ?thesis
      using that
      by blast
  qed

lemma effect__strips_i:
  fixes op
  assumes "e = effect__strips op"
  obtains es1 es2
    where "e = (es1 @ es2)"
      and "es1 = map (λv. (v, True)) (add_effects_of op)"
      and "es2 = map (λv. (v, False)) (delete_effects_of op)"
  proof -
    obtain es1 es2 where a: "e = (es1 @ es2)"
      and b: "es1 = map (λv. (v, True)) (add_effects_of op)"
      and c: "es2 = map (λv. (v, False)) (delete_effects_of op)"
      using assms(1)
      unfolding effect__strips_def
      by blast
    then show ?thesis
      using that
      by force
  qed

lemma effect__strips_ii:
  fixes op
  assumes "e = ConjunctiveEffect (es1 @ es2)"
    and "es1 = map (λv. (v, True)) (add_effects_of op)"
    and "es2 = map (λv. (v, False)) (delete_effects_of op)"
  shows "v  set (add_effects_of op). (e'  set es1. e' = (v, True))"
    and "v  set (delete_effects_of op). (e'  set es2. e' = (v, False))"
  proof
  ― ‹ NOTE Show that for each variable v› in the add effect list, we can obtain an atomic effect
  with true value. ›
    fix v
    {
      assume a: "v  set (add_effects_of op)"
      have "set es1 = (λv. (v, True)) ` set (add_effects_of op)"
        using assms(2) List.set_map
        by auto
      then obtain e'
        where "e'  set es1"
        and "e' =  (λv. (v, True)) v"
        using a
        by blast
      then have "e'  set es1. e' = (v, True)"
        by blast
    }
    thus "v  set (add_effects_of op)  e'  set es1. e' = (v, True)"
      by fast
  ― ‹ NOTE the proof is symmetrical to the one above: for each variable v in the delete effect list,
  we can obtain an atomic effect with v being false. ›
  next
    {
      fix v
      assume a: "v  set (delete_effects_of op)"
      have "set es2 = (λv. (v, False)) ` set (delete_effects_of op)"
        using assms(3) List.set_map
        by force
      then obtain e''
        where "e''  set es2"
        and "e'' =  (λv. (v, False)) v"
        using a
        by blast
      then have "e''  set es2. e'' = (v, False)"
        by blast
    }
    thus "vset (delete_effects_of op). e'set es2. e' = (v, False)"
      by fast
  qed

(* TODO refactor theory Appendix AND make visible? *)
lemma map_of_constant_assignments_dom:
  ― ‹ NOTE ancillary lemma used in the proof below. ›
  assumes "m = map_of (map (λv. (v, d)) vs)"
  shows "dom m = set vs"
  proof -
    let ?vs' = "map (λv. (v, d)) vs"
    have "dom m = fst ` set ?vs'"
      using assms(1) dom_map_of_conv_image_fst
      by metis
    moreover have "fst ` set ?vs' = set vs"
      by force
    ultimately show ?thesis
      by argo
  qed

lemma effect__strips_iii_a:
  assumes "s' = (s  op)"
  shows "v. v  set (add_effects_of op)  s' v = Some True"
  proof -
    fix v
    assume a: "v  set (add_effects_of op)"
    let ?as = "effect_to_assignments op"
    obtain as1 as2 where b: "?as = as1 @ as2"
      and c: "as1 = map (λv. (v, True)) (add_effects_of op)"
      and "as2 = map (λv. (v, False)) (delete_effects_of op)"
      using effect_to_assignments_ii
      by blast
    have d: "map_of ?as = map_of as2 ++ map_of as1"
      using b Map.map_of_append
      by auto
    {
      ― ‹ TODO refactor? ›
      let ?vs = "add_effects_of op"
      have "?vs  []"
        using a
        by force
      then have "dom (map_of as1) = set (add_effects_of op)"
        using c map_of_constant_assignments_dom
        by metis
      then have "v  dom (map_of as1)"
        using a
        by blast
      then have "map_of ?as v = map_of as1 v"
        using d
        by force
    } moreover {
      let ?f = "λ_. True"
      from c have "map_of as1 = (Some  ?f) |` (set (add_effects_of op))"
        using map_of_map_restrict
        by fast
      then have "map_of as1 v = Some True"
        using a
        by auto
    }
    moreover have "s' = s ++ map_of as2 ++ map_of as1"
      using assms(1)
      unfolding execute_operator_def
      using b
      by simp
    ultimately show "s' v = Some True"
      by simp
  qed

(* TODO In contrast to the proof above we need proof preparation with auto. Why? *)
lemma effect__strips_iii_b:
  assumes "s' = (s  op)"
  shows "v. v  set (delete_effects_of op)  v  set (add_effects_of op)  s' v = Some False"
  proof (auto)
    fix v
    assume a1: "v  set (add_effects_of op)" and a2: "v  set (delete_effects_of op)"
    let ?as = "effect_to_assignments op"
    obtain as1 as2 where b: "?as = as1 @ as2"
      and c: "as1 = map (λv. (v, True)) (add_effects_of op)"
      and d: "as2 = map (λv. (v, False)) (delete_effects_of op)"
      using effect_to_assignments_ii
      by blast
    have e: "map_of ?as = map_of as2 ++ map_of as1"
      using b Map.map_of_append
      by auto
    {
      have "dom (map_of as1) = set (add_effects_of op)"
        using c map_of_constant_assignments_dom
        by metis
      then have "v  dom (map_of as1)"
        using a1
        by blast
    } note f = this
    {
      let ?vs = "delete_effects_of op"
      have "?vs  []"
        using a2
        by force
      then have "dom (map_of as2) = set ?vs"
        using d  map_of_constant_assignments_dom
        by metis
    } note g = this
    {
      have "s' = s ++ map_of as2 ++ map_of as1"
        using assms(1)
        unfolding execute_operator_def
        using b
        by simp
      thm  f map_add_dom_app_simps(3)[OF f, of "s ++ map_of as2"]
      moreover have "s' v = (s ++ map_of as2) v"
        using calculation  map_add_dom_app_simps(3)[OF f, of "s ++ map_of as2"]
        by blast
      moreover have "v  dom (map_of as2)"
        using a2 g
        by argo
      ultimately have "s' v = map_of as2 v"
        by fastforce
    }
    moreover
    {
      let ?f = "λ_. False"
      from d have "map_of as2 = (Some  ?f) |` (set (delete_effects_of op))"
        using map_of_map_restrict
        by fast
      then have "map_of as2 v = Some False"
        using a2
        by force
    }
    ultimately show  " s' v = Some False"
      by argo
  qed

(* TODO We need proof preparation with auto. Why? *)
lemma effect__strips_iii_c:
  assumes "s' = (s  op)"
  shows "v. v  set (add_effects_of op)  v  set (delete_effects_of op)  s' v = s v"
  proof (auto)
    fix v
    assume a1: "v  set (add_effects_of op)" and a2: "v  set (delete_effects_of op)"
    let ?as = "effect_to_assignments op"
    obtain as1 as2 where b: "?as = as1 @ as2"
      and c: "as1 = map (λv. (v, True)) (add_effects_of op)"
      and d: "as2 = map (λv. (v, False)) (delete_effects_of op)"
      using effect_to_assignments_ii
      by blast
    have e: "map_of ?as = map_of as2 ++ map_of as1"
      using b Map.map_of_append
      by auto
    {
      have "dom (map_of as1) = set (add_effects_of op)"
        using c map_of_constant_assignments_dom
        by metis
      then have "v  dom (map_of as1)"
        using a1
        by blast
    } moreover  {
      have "dom (map_of as2) = set (delete_effects_of op)"
        using d map_of_constant_assignments_dom
        by metis
      then have "v  dom (map_of as2)"
        using a2
        by blast
    }
    ultimately show "s' v = s v"
      using assms(1)
      unfolding execute_operator_def
      by (simp add: b map_add_dom_app_simps(3))
  qed

text ‹The following theorem combines three preceding sublemmas which show
that the following properties hold for the successor state s' ≡ execute_operator op s›
obtained by executing an operator op› in a state s›:
\footnote{Lemmas \path{effect__strips_iii_a}, \path{effect__strips_iii_b}, and
\path{effect__strips_iii_c} (not shown).}

\begin{itemize}
  \item every add effect is satisfied in s'› (sublemma  \isaname{effect__strips_iii_a}); and,
  \item every delete effect that is not also an add effect is not satisfied in s'› (sublemma
\isaname{effect__strips_iii_b}); and finally
  \item the state remains unchanged---i.e. s' v = s v›---for all variables which are neither an
add effect nor a delete effect.
\end{itemize} ›

(* TODO? Rewrite theorem ‹operator_effect__strips› to match ‹s ++ map_of (
effect_to_assignments op)› rather than ‹execute_operator Π op s› since we need this
form later on for the parallel execution theorem? *)
theorem  operator_effect__strips:
  assumes "s' = (s  op)"
  shows
    "v.
      v  set (add_effects_of op)
       s' v = Some True"
    and "v.
      v  set (add_effects_of op)  v  set (delete_effects_of op)
       s' v = Some False"
    and "v.
      v  set (add_effects_of op)  v  set (delete_effects_of op)
       s' v = s v"
proof (auto)
  show "v.
    v  set (add_effects_of op)
     s' v = Some True"
    using assms effect__strips_iii_a
    by fast
next
  show "v.
    v  set (add_effects_of op)
     v  set (delete_effects_of op)
      s' v = Some False"
    using assms effect__strips_iii_b
    by fast
next
  show "v.
    v  set (add_effects_of op)
     v  set (delete_effects_of op)
     s' v = s v"
    using assms effect__strips_iii_c
    by metis
qed

subsection "Parallel Plan Semantics"

definition "are_all_operators_applicable s ops
   list_all (λop. is_operator_applicable_in s op) ops"

definition "are_operator_effects_consistent op1 op2  let
    add1 = add_effects_of op1
    ; add2 = add_effects_of op2
    ; del1 = delete_effects_of op1
    ; del2 = delete_effects_of op2
  in ¬list_ex (λv. list_ex ((=) v) del2) add1  ¬list_ex (λv. list_ex ((=) v) add2) del1"

definition "are_all_operator_effects_consistent ops 
  list_all (λop. list_all (are_operator_effects_consistent op) ops) ops"

definition execute_parallel_operator
  :: "'variable strips_state
     'variable strips_operator list
     'variable strips_state"
  where "execute_parallel_operator s ops
     foldl (++) s (map (map_of  effect_to_assignments) ops)"
text ‹ The parallel STRIPS execution semantics is defined in similar way as the serial STRIPS
execution semantics. However, the applicability test is lifted to parallel operators and we
additionally test for operator consistency (which was unecessary in the serial case). ›

fun  execute_parallel_plan
  :: "'variable strips_state
     'variable strips_parallel_plan
     'variable strips_state"
  where "execute_parallel_plan s [] = s"
  | "execute_parallel_plan s (ops # opss) = (if
      are_all_operators_applicable s ops
       are_all_operator_effects_consistent ops
    then execute_parallel_plan (execute_parallel_operator s ops) opss
    else s)"

definition "are_operators_interfering op1 op2
   list_ex (λv. list_ex ((=) v) (delete_effects_of op1)) (precondition_of op2)
      list_ex (λv. list_ex ((=) v) (precondition_of op1)) (delete_effects_of op2)"

(* TODO rewrite as inductive predicate *)
primrec are_all_operators_non_interfering
  :: "'variable strips_operator list  bool"
  where "are_all_operators_non_interfering [] = True"
  | "are_all_operators_non_interfering (op # ops)
    = (list_all (λop'. ¬are_operators_interfering op op') ops
       are_all_operators_non_interfering ops)"

text ‹ Since traces mirror the execution semantics, the same is true for the definition of
parallel STRIPS plan traces. ›

fun  trace_parallel_plan_strips
  :: "'variable strips_state  'variable strips_parallel_plan  'variable strips_state list"
  where "trace_parallel_plan_strips s [] = [s]"
  | "trace_parallel_plan_strips s (ops # opss) = s # (if
      are_all_operators_applicable s ops
       are_all_operator_effects_consistent ops
    then trace_parallel_plan_strips (execute_parallel_operator s ops) opss
    else [])"

text ‹ Similarly, the definition of parallel solutions requires that the parallel execution
semantics transforms the initial problem into the goal state of the problem and that every
operator of every parallel operator in the parallel plan is an operator that is defined in the
problem description. ›

definition  is_parallel_solution_for_problem
  where "is_parallel_solution_for_problem Π π
     (strips_problem.goal_of Π) m execute_parallel_plan
        (strips_problem.initial_of Π) π
       list_all (λops. list_all (λop.
        ListMem op (strips_problem.operators_of Π)) ops) π"


(* TODO rename are_all_operators_applicable_in_set *)
lemma are_all_operators_applicable_set:
  "are_all_operators_applicable s ops
     (op  set ops. v  set (precondition_of op). s v = Some True)"
  unfolding are_all_operators_applicable_def
    STRIPS_Representation.is_operator_applicable_in_def list_all_iff
  by presburger

(* TODO rename are_all_operators_applicable_in_cons *)
lemma are_all_operators_applicable_cons:
  assumes "are_all_operators_applicable s (op # ops)"
  shows "is_operator_applicable_in s op"
    and "are_all_operators_applicable s ops"
  proof -
    from assms have a: "list_all (λop. is_operator_applicable_in s op) (op # ops)"
      unfolding are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
      by blast
    then have "is_operator_applicable_in s op"
      by fastforce
    moreover {
      from a have "list_all (λop. is_operator_applicable_in s op) ops"
        by simp
      then have "are_all_operators_applicable s ops"
      using are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
        by blast
      }
    ultimately show "is_operator_applicable_in s op"
      and "are_all_operators_applicable s ops"
       by fast+
  qed

lemma are_operator_effects_consistent_set:
  assumes "op1  set ops"
    and "op2  set ops"
  shows "are_operator_effects_consistent op1 op2
     = (set (add_effects_of op1)  set (delete_effects_of op2) = {}
       set (delete_effects_of op1)  set (add_effects_of op2) = {})"
  proof -
    have "(¬list_ex (λv. list_ex ((=) v) (delete_effects_of op2)) (add_effects_of op1))
      = (set (add_effects_of op1)  set (delete_effects_of op2) = {})"
      using list_ex_intersection[of "delete_effects_of op2" "add_effects_of op1"]
      by meson
    moreover have "(¬list_ex (λv. list_ex ((=) v) (add_effects_of op2)) (delete_effects_of op1))
      = (set (delete_effects_of op1)  set (add_effects_of op2) = {})"
      using list_ex_intersection[of "add_effects_of op2"  "delete_effects_of op1"]
      by meson
    ultimately show "are_operator_effects_consistent op1 op2
       = (set (add_effects_of op1)  set (delete_effects_of op2) = {}
         set (delete_effects_of op1)  set (add_effects_of op2) = {})"
      unfolding are_operator_effects_consistent_def
      by presburger
  qed

lemma are_all_operator_effects_consistent_set:
  "are_all_operator_effects_consistent ops
     (op1  set ops. op2  set ops.
      (set (add_effects_of op1)  set (delete_effects_of op2) = {})
         (set (delete_effects_of op1)  set (add_effects_of op2) = {}))"
  proof -
    {
      fix op1 op2
      assume "op1  set ops" and "op2  set ops"
      hence "are_operator_effects_consistent op1 op2
        = (set (add_effects_of op1)  set (delete_effects_of op2) = {}
           set (delete_effects_of op1)  set (add_effects_of op2) = {})"
        using are_operator_effects_consistent_set[of op1 ops op2]
        by fast
    }
    thus ?thesis
      unfolding are_all_operator_effects_consistent_def list_all_iff
      by force
  qed

lemma are_all_effects_consistent_tail:
  assumes "are_all_operator_effects_consistent (op # ops)"
  shows "are_all_operator_effects_consistent ops"
  proof -
    from assms
    have a: "list_all (λop'. list_all (are_operator_effects_consistent op')
      (Cons op ops)) (Cons op ops)"
      unfolding are_all_operator_effects_consistent_def
      by blast
    then have b_1: "list_all (are_operator_effects_consistent op) (op # ops)"
      and b_2: "list_all (λop'. list_all (are_operator_effects_consistent op') (op # ops)) ops"
      by force+
    then have "list_all (are_operator_effects_consistent op) ops"
      by simp
    moreover
    {
      {
        fix z
        assume "z  set (Cons op ops)"
         and "list_all (are_operator_effects_consistent z) (op # ops)"
        then have "list_all (are_operator_effects_consistent z) ops"
          by auto
      }
      then have "list_all (λop'. list_all (are_operator_effects_consistent op') ops) ops"
        using list.pred_mono_strong[of
            "(λop'. list_all (are_operator_effects_consistent op') (op # ops))"
            "Cons op ops" "(λop'. list_all (are_operator_effects_consistent op')  ops)"
          ] a
        by fastforce
    }
    ultimately have "list_all (are_operator_effects_consistent op) ops
       list_all (λop'. list_all (are_operator_effects_consistent op') ops) ops"
      by blast
    then show ?thesis
      using are_all_operator_effects_consistent_def
      by fast
  qed

lemma are_all_operators_non_interfering_tail:
  assumes "are_all_operators_non_interfering (op # ops)"
  shows "are_all_operators_non_interfering ops"
  using assms
  unfolding are_all_operators_non_interfering_def
  by simp

lemma are_operators_interfering_symmetric:
  assumes "are_operators_interfering op1 op2"
  shows "are_operators_interfering op2 op1"
  using assms
  unfolding are_operators_interfering_def list_ex_iff
  by fast

― ‹ A small technical characterizing operator lists with property
\isaname{are_all_operators_non_interfering ops}. We show that pairs of distinct operators which interfere
with one another cannot both be contained in the corresponding operator set. ›
lemma are_all_operators_non_interfering_set_contains_no_distinct_interfering_operator_pairs:
  assumes "are_all_operators_non_interfering ops"
    and "are_operators_interfering op1 op2"
    and "op1  op2"
  shows "op1  set ops  op2  set ops"
  using assms
  proof (induction ops)
    case (Cons op ops)
    thm Cons.IH[OF _ Cons.prems(2, 3)]
    have nb1: "op'  set ops. ¬are_operators_interfering op op'"
      and nb2: "are_all_operators_non_interfering ops"
      using Cons.prems(1)
      unfolding are_all_operators_non_interfering.simps(2) list_all_iff
      by blast+
    then consider (A) "op = op1"
      | (B) "op = op2"
      | (C) "op  op1  op  op2"
      by blast
    thus ?case
      proof (cases)
        case A
        {
          assume "op2  set (op # ops)"
          then have "op2  set ops"
            using Cons.prems(3) A
            by force
          then have "¬are_operators_interfering op1 op2"
            using nb1 A
            by fastforce
          hence False
            using Cons.prems(2)..
        }
        thus ?thesis
          by blast
      next
        case B
        {
          assume "op1  set (op # ops)"
          then have "op1  set ops"
            using Cons.prems(3) B
            by force
          then have "¬are_operators_interfering op1 op2"
            using nb1 B are_operators_interfering_symmetric
            by blast
          hence False
            using Cons.prems(2)..
        }
        thus ?thesis
          by blast
      next
        case C
        thus ?thesis
          using Cons.IH[OF nb2 Cons.prems(2, 3)]
          by force
      qed
  qed simp

(* TODO The recurring ‹list_all ↝ ∀› transformations could be refactored into a general
lemma.
   TODO refactor (also used in lemma ‹execute_serial_plan_split_i›). *)
lemma execute_parallel_plan_precondition_cons_i:
  fixes s :: "('variable, bool) state"
  assumes "¬are_operators_interfering op op'"
    and "is_operator_applicable_in s op"
    and "is_operator_applicable_in s op'"
  shows "is_operator_applicable_in (s ++ map_of (effect_to_assignments op)) op'"
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments op)"
    ― ‹ TODO slightly hackish to exploit the definition of execute_operator›, but we
  otherwise have to rewrite theorem operator_effect__strips› (which is a todo as of now). ›
    {
      have a: "?s' = s  op"
        by (simp add: execute_operator_def)
      then have "v. v  set (add_effects_of op)  ?s' v = Some True"
        and "v. v  set (add_effects_of op)  v  set (delete_effects_of op)  ?s' v = Some False"
        and "v. v  set (add_effects_of op)  v  set (delete_effects_of op)  ?s' v = s v"
        using operator_effect__strips
        by metis+
    }
    note a = this
    ― ‹ TODO refactor lemma not_have_interference_set›. ›
    {
      fix v
      assume α: "v  set (precondition_of op')"
      {
        fix v
        have "¬list_ex ((=) v) (delete_effects_of op)
          = list_all (λv'. ¬v = v') (delete_effects_of op)"
          using not_list_ex_equals_list_all_not[
              where P="(=) v" and xs="delete_effects_of op"]
          by blast
      } moreover {
        from assms(1)
        have "¬list_ex (λv. list_ex ((=) v) (delete_effects_of op)) (precondition_of op')"
          unfolding are_operators_interfering_def
          by blast
        then have "list_all (λv. ¬list_ex ((=) v) (delete_effects_of op)) (precondition_of op')"
          using not_list_ex_equals_list_all_not[
              where P="λv. list_ex ((=) v) (delete_effects_of op)" and xs="precondition_of op'"]
          by blast
      }
      ultimately have β:
        "list_all (λv. list_all (λv'. ¬v = v') (delete_effects_of op)) (precondition_of op')"
        by presburger
      moreover {
        fix v
        have "list_all (λv'. ¬v = v') (delete_effects_of op)
          = (v'  set (delete_effects_of op). ¬v = v')"
          using list_all_iff [where P="λv'. ¬v = v'" and x="delete_effects_of op"]
          .
      }
      ultimately have "v  set (precondition_of op'). v'  set (delete_effects_of op). ¬v = v'"
        using β list_all_iff[
          where P="λv. list_all (λv'. ¬v = v') (delete_effects_of op)"
            and x="precondition_of op'"]
        by presburger
      then have "v  set (delete_effects_of op)"
        using α
        by fast
    }
    note b = this
    {
      fix v
      assume a: "v  set (precondition_of op')"
      have "list_all (λv. s v = Some True) (precondition_of op')"
        using assms(3)
        unfolding is_operator_applicable_in_def
          STRIPS_Representation.is_operator_applicable_in_def
        by presburger
      then have "v  set (precondition_of op'). s v = Some True"
        using list_all_iff[where P="λv. s v = Some True" and x="precondition_of op'"]
        by blast
      then have "s v = Some True"
        using a
        by blast
    }
    note c = this
    {
      fix v
      assume d: "v  set (precondition_of op')"
      then have "?s' v = Some True"
      proof (cases "v  set (add_effects_of op)")
        case True
        then show ?thesis
          using a
          by blast
      next
        case e: False
        then show ?thesis
        proof (cases "v  set (delete_effects_of op)")
          case True
          then show ?thesis
            using assms(1) b d
              by fast
          next
            case False
            then have "?s' v = s v"
              using a e
              by blast
            then show ?thesis
              using c d
              by presburger
          qed
      qed
    }
    then have "list_all (λv. ?s' v = Some True) (precondition_of op')"
      using list_all_iff[where P="λv. ?s' v = Some True" and x="precondition_of op'"]
      by blast
    then show ?thesis
      unfolding is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
      by auto
  qed

― ‹ The third assumption are_all_operators_non_interfering (a # ops)›" is not part of the
precondition of \isaname{execute_parallel_operator} but is required for the proof of the
subgoal hat applicable is maintained. ›
lemma execute_parallel_plan_precondition_cons:
  fixes a :: "'variable strips_operator"
  assumes "are_all_operators_applicable s (a # ops)"
    and "are_all_operator_effects_consistent (a # ops)"
    and "are_all_operators_non_interfering (a # ops)"
  shows "are_all_operators_applicable (s ++ map_of (effect_to_assignments a)) ops"
    and "are_all_operator_effects_consistent ops"
    and "are_all_operators_non_interfering ops"
  using are_all_effects_consistent_tail[OF assms(2)]
    are_all_operators_non_interfering_tail[OF assms(3)]
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    have nb1: "op  set (a # ops). is_operator_applicable_in s op"
      using assms(1) are_all_operators_applicable_set
      unfolding are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def list_all_iff
      by blast
    have nb2: "op  set ops. ¬are_operators_interfering a op"
      using assms(3)
      unfolding are_all_operators_non_interfering_def list_all_iff
      by simp
    have nb3: "is_operator_applicable_in s a"
      using assms(1) are_all_operators_applicable_set
      unfolding are_all_operators_applicable_def is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def list_all_iff
      by force
    {
      fix op
      assume op_in_ops: "op  set ops"
      hence "is_operator_applicable_in ?s' op"
        using execute_parallel_plan_precondition_cons_i[of a op] nb1 nb2 nb3
        by force
    }
    then show "are_all_operators_applicable ?s' ops"
      unfolding are_all_operators_applicable_def list_all_iff
        is_operator_applicable_in_def
      by blast
  qed

lemma execute_parallel_operator_cons[simp]:
  "execute_parallel_operator s (op # ops)
    = execute_parallel_operator (s ++ map_of (effect_to_assignments op)) ops"
  unfolding execute_parallel_operator_def
  by simp

lemma execute_parallel_operator_cons_equals:
  assumes "are_all_operators_applicable s (a # ops)"
    and "are_all_operator_effects_consistent (a # ops)"
    and "are_all_operators_non_interfering (a # ops)"
  shows "execute_parallel_operator s (a # ops)
    = execute_parallel_operator (s ++ map_of (effect_to_assignments a)) ops"
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    {
      from assms(1, 2)
      have "execute_parallel_operator s (Cons a ops)
        = foldl (++) s (map (map_of  effect_to_assignments) (Cons a ops))"
         unfolding execute_parallel_operator_def
         by presburger
       also have " = foldl (++) (?s')
         (map (map_of  effect_to_assignments) ops)"
         by auto
       finally have "execute_parallel_operator s (Cons a ops)
         = foldl (++) (?s')
          (map (map_of  effect_to_assignments) ops)"
         using execute_parallel_operator_def
         by blast
     }
    ― ‹ NOTE the precondition of \isaname{execute_parallel} for a # ops› is also true for the tail
    list and state ?s'› as shown in lemma
    \isaname{execute_parallel_operator_precondition_cons}. Hence the precondition for the r.h.s.
    of the goal also holds. ›
     moreover have "execute_parallel_operator ?s' ops
        = foldl (++) (s ++ (map_of  effect_to_assignments) a)
          (map (map_of  effect_to_assignments) ops)"
         by (simp add: execute_parallel_operator_def)
    ultimately show ?thesis
      by force
  qed

― ‹ We show here that following the lemma above, executing one operator of a parallel
operator can be replaced by a (single) STRIPS operator execution. ›
corollary execute_parallel_operator_cons_equals_corollary:
  assumes "are_all_operators_applicable s (a # ops)"
  shows "execute_parallel_operator s (a # ops)
    = execute_parallel_operator (s  a) ops"
  proof -
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    from assms
    have "execute_parallel_operator s (a # ops)
      = execute_parallel_operator (s ++ map_of (effect_to_assignments a)) ops"
      using execute_parallel_operator_cons_equals
      by simp
    moreover have "?s' = s  a"
      unfolding execute_operator_def
      by simp
    ultimately show ?thesis
      by argo
  qed

(* TODO duplicate? *)
lemma effect_to_assignments_simp[simp]: "effect_to_assignments op
  = map (λv. (v, True)) (add_effects_of op) @ map (λv. (v, False)) (delete_effects_of op)"
  by (simp add: effect_to_assignments_i)

lemma effect_to_assignments_set_is[simp]:
  "set (effect_to_assignments op) = { ((v, a), True) | v a. (v, a)  set (add_effects_of op) }
     { ((v, a), False) | v a. (v, a)  set (delete_effects_of op) }"
proof -
    obtain as where "effect__strips op = as"
      and "as = map (λv. (v, True)) (add_effects_of op)
        @ map (λv. (v, False)) (delete_effects_of op)"
      unfolding effect__strips_def
      by blast
    moreover have "as
      = map (λv. (v, True)) (add_effects_of op) @ map (λv. (v, False)) (delete_effects_of op)"
      using calculation(2)
      unfolding map_append map_map comp_apply
      by auto
    moreover have "effect_to_assignments op = as"
      unfolding effect_to_assignments_def calculation(1, 2)
      by auto
    ultimately show ?thesis
      unfolding set_map
      by auto
  qed

corollary effect_to_assignments_construction_from_function_graph:
  assumes "set (add_effects_of op)  set (delete_effects_of op) = {}"
  shows "effect_to_assignments op = map
    (λv. (v, if ListMem v (add_effects_of op) then True else False))
    (add_effects_of op @ delete_effects_of op)"
    and "effect_to_assignments op = map
    (λv. (v, if ListMem v (delete_effects_of op) then False else True))
    (add_effects_of op @ delete_effects_of op)"
  proof -
    let ?f = "λv. (v, if ListMem v (add_effects_of op) then True else False)"
      and ?g = "λv. (v, if ListMem v (delete_effects_of op) then False else True)"
    {
      have "map ?f (add_effects_of op @ delete_effects_of op)
        = map ?f (add_effects_of op) @ map ?f (delete_effects_of op)"
        using map_append
        by fast
      ― ‹ TODO slow. ›
      hence "effect_to_assignments op = map ?f (add_effects_of op @ delete_effects_of op)"
        using ListMem_iff assms
        by fastforce
    } moreover {
      have "map ?g (add_effects_of op @ delete_effects_of op)
        = map ?g (add_effects_of op) @ map ?g (delete_effects_of op)"
        using map_append
        by fast
      ― ‹ TODO slow. ›
      hence "effect_to_assignments op = map ?g (add_effects_of op @ delete_effects_of op)"
        using ListMem_iff assms
        by fastforce
    }
    ultimately show "effect_to_assignments op = map
      (λv. (v, if ListMem v (add_effects_of op) then True else False))
      (add_effects_of op @ delete_effects_of op)"
      and "effect_to_assignments op = map
      (λv. (v, if ListMem v (delete_effects_of op) then False else True))
      (add_effects_of op @ delete_effects_of op)"
      by blast+
  qed

corollary map_of_effect_to_assignments_is_none_if:
  assumes "¬v  set (add_effects_of op)"
    and "¬v  set (delete_effects_of op)"
  shows "map_of (effect_to_assignments op) v = None"
  proof -
    let ?l = "effect_to_assignments op"
    {
      have "set ?l = { (v, True) | v. v  set (add_effects_of op) }
         { (v, False) | v. v  set (delete_effects_of op)}"
        by auto
      then have "fst ` set ?l
        = (fst ` {(v, True) | v. v  set (add_effects_of op)})
           (fst ` {(v, False) | v. v  set (delete_effects_of op)})"
        using image_Un[of fst "{(v, True) | v. v  set (add_effects_of op)}"
           "{(v, False) | v. v  set (delete_effects_of op)}"]
        by presburger
      ― ‹ TODO slow.›
      also have " = (fst ` (λv. (v, True)) ` set (add_effects_of op))
         (fst ` (λv. (v, False)) ` set (delete_effects_of op))"
        using setcompr_eq_image[of "λv. (v, True)" "λv. v  set (add_effects_of op)"]
          setcompr_eq_image[of "λv. (v, False)" "λv. v  set (delete_effects_of op)"]
        by simp
      ― ‹ TODO slow.›
      also have " = id ` set (add_effects_of op)  id ` set (delete_effects_of op)"
        by force
      ― ‹ TODO slow.›
      finally have "fst ` set ?l = set (add_effects_of op)  set (delete_effects_of op)"
        by auto
      hence "v  fst ` set ?l"
        using assms(1, 2)
        by blast
    }
    thus ?thesis
      using map_of_eq_None_iff[of ?l v]
      by blast
  qed

lemma execute_parallel_operator_positive_effect_if_i:
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op  set ops"
    and "v  set (add_effects_of op)"
  shows "map_of (effect_to_assignments op) v = Some True"
  proof -
    let ?f = "λx. if ListMem x (add_effects_of op) then True else False"
      and ?l'= " map (λv. (v, if ListMem v (add_effects_of op) then True else False))
        (add_effects_of op @ delete_effects_of op)"
    have "set (add_effects_of op)  {}"
      using assms(4)
      by fastforce
    moreover {
      have "set (add_effects_of op)  set (delete_effects_of op) = {}"
        using are_all_operator_effects_consistent_set assms(2, 3)
        by fast
      moreover have "effect_to_assignments op = ?l'"
        using effect_to_assignments_construction_from_function_graph(1) calculation
        by fast
      ultimately have "map_of (effect_to_assignments op) = map_of ?l'"
        by argo
    }
    ultimately have "map_of (effect_to_assignments op) v = Some (?f v)"
      using Map_Supplement.map_of_from_function_graph_is_some_if[
          of _ _ "?f", OF _ assms(4)]
      by simp
    thus ?thesis
      using ListMem_iff assms(4)
      by metis
  qed

lemma execute_parallel_operator_positive_effect_if:
  fixes ops
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op  set ops"
    and "v  set (add_effects_of op)"
  shows "execute_parallel_operator s ops v = Some True"
  proof -
    let ?l = "map (map_of  effect_to_assignments) ops"
    have set_l_is: "set ?l = (map_of  effect_to_assignments) ` set ops"
      using set_map
      by fastforce
    {
      let ?m = "(map_of  effect_to_assignments) op"
      have "?m  set ?l"
        using assms(3) set_l_is
        by blast
      moreover have "?m v = Some True"
        using execute_parallel_operator_positive_effect_if_i[OF assms]
        by fastforce
      ultimately have "m  set ?l. m v = Some True"
        by blast
    }
    moreover {
      fix m'
      assume "m'  set ?l"
      then obtain op'
        where op'_in_set_ops: "op'  set ops"
          and m'_is: "m' = (map_of  effect_to_assignments) op'"
        by auto
      then have "set (add_effects_of op)  set (delete_effects_of op') = {}"
        using assms(2, 3) are_all_operator_effects_consistent_set[of ops]
        by blast
      then have "v  set (delete_effects_of op')"
        using assms(4)
        by blast
      then consider (v_in_set_add_effects) "v  set (add_effects_of op')"
        | (otherwise) "¬v  set (add_effects_of op')  ¬v  set (delete_effects_of op')"
        by blast
      hence "m' v = Some True  m' v = None"
        proof (cases)
          case v_in_set_add_effects
          ― ‹ TODO slow. ›
          thus ?thesis
            using execute_parallel_operator_positive_effect_if_i[
                OF assms(1, 2) op'_in_set_ops, of v] m'_is
            by simp
        next
          case otherwise
          then have "¬v  set (add_effects_of op')"
            and "¬v  set (delete_effects_of op')"
            by blast+
          thus ?thesis
            using map_of_effect_to_assignments_is_none_if[of v op'] m'_is
            by fastforce
        qed
    }
    ― ‹ TODO slow. ›
    ultimately show ?thesis
      unfolding execute_parallel_operator_def
      using foldl_map_append_is_some_if[of s v True ?l]
      by meson
  qed

lemma execute_parallel_operator_negative_effect_if_i:
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op  set ops"
    and "v  set (delete_effects_of op)"
  shows "map_of (effect_to_assignments op) v = Some False"
  proof -
    let ?f = "λx. if ListMem x (delete_effects_of op) then False else True"
      and ?l'= " map (λv. (v, if ListMem v (delete_effects_of op) then False else True))
        (add_effects_of op @ delete_effects_of op)"
    have "set (delete_effects_of op @ add_effects_of op)  {}"
      using assms(4)
      by fastforce
    moreover have "v  set (delete_effects_of op @ add_effects_of op)"
      using assms(4)
      by simp
    moreover {
      have "set (add_effects_of op)  set (delete_effects_of op) = {}"
        using are_all_operator_effects_consistent_set assms(2, 3)
        by fast
      moreover have "effect_to_assignments op = ?l'"
        using effect_to_assignments_construction_from_function_graph(2) calculation
        by blast
      ultimately have "map_of (effect_to_assignments op) = map_of ?l'"
        by argo
    }
    ultimately have "map_of (effect_to_assignments op) v = Some (?f v)"
      using Map_Supplement.map_of_from_function_graph_is_some_if[
          of "add_effects_of op @ delete_effects_of op" v "?f"]
      by force
    thus ?thesis
      using assms(4)
      unfolding ListMem_iff
      by presburger
  qed

lemma execute_parallel_operator_negative_effect_if:
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "op  set ops"
    and "v  set (delete_effects_of op)"
  shows "execute_parallel_operator s ops v = Some False"
  proof -
    let ?l = "map (map_of  effect_to_assignments) ops"
    have set_l_is: "set ?l = (map_of  effect_to_assignments) ` set ops"
      using set_map
      by fastforce
    {
      let ?m = "(map_of  effect_to_assignments) op"
      have "?m  set ?l"
        using assms(3) set_l_is
        by blast
      moreover have "?m v = Some False"
        using execute_parallel_operator_negative_effect_if_i[OF assms]
        by fastforce
      ultimately have "m  set ?l. m v = Some False"
        by blast
    }
    moreover {
      fix m'
      assume "m'  set ?l"
      then obtain op'
        where op'_in_set_ops: "op'  set ops"
          and m'_is: "m' = (map_of  effect_to_assignments) op'"
        by auto
      then have "set (delete_effects_of op)  set (add_effects_of op') = {}"
        using assms(2, 3) are_all_operator_effects_consistent_set[of ops]
        by blast
      then have "v  set (add_effects_of op')"
        using assms(4)
        by blast
      then consider (v_in_set_delete_effects) "v  set (delete_effects_of op')"
        | (otherwise) "¬v  set (add_effects_of op')  ¬v  set (delete_effects_of op')"
        by blast
      hence "m' v = Some False  m' v = None"
        proof (cases)
          case v_in_set_delete_effects
          ― ‹ TODO slow. ›
          thus ?thesis
            using execute_parallel_operator_negative_effect_if_i[
                OF assms(1, 2) op'_in_set_ops, of v] m'_is
            by simp
        next
          case otherwise
          then have "¬v  set (add_effects_of op')"
            and "¬v  set (delete_effects_of op')"
            by blast+
          thus ?thesis
            using map_of_effect_to_assignments_is_none_if[of v op'] m'_is
            by fastforce
        qed
    }
    ― ‹ TODO slow. ›
    ultimately show ?thesis
      unfolding execute_parallel_operator_def
      using foldl_map_append_is_some_if[of s v False ?l]
      by meson
  qed

lemma execute_parallel_operator_no_effect_if:
  assumes "op  set ops. ¬v  set (add_effects_of op)  ¬v  set (delete_effects_of op)"
  shows "execute_parallel_operator s ops v = s v"
  using assms
  unfolding execute_parallel_operator_def
  proof (induction ops arbitrary: s)
    case (Cons a ops)
    let ?f = "map_of  effect_to_assignments"
    {
      have "v  set (add_effects_of a)  v  set (delete_effects_of a)"
        using Cons.prems(1)
        by force
      then have "?f a v = None"
        using map_of_effect_to_assignments_is_none_if[of v a]
        by fastforce
      then have "v  dom (?f a)"
        by blast
      hence "(s ++ ?f a) v = s v"
        using map_add_dom_app_simps(3)[of v "?f a" s]
        by blast
    }
    moreover {
      have "opset ops. v  set (add_effects_of op)  v  set (delete_effects_of op)"
        using Cons.prems(1)
        by simp
      hence "foldl (++) (s ++ ?f a) (map ?f ops) v = (s ++ ?f a) v"
        using Cons.IH[of "s ++ ?f a"]
        by blast
    }
    moreover {
      have "map ?f (a # ops) = ?f a # map ?f ops"
        by force
      then have "foldl (++) s (map ?f (a # ops))
        = foldl (++) (s ++ ?f a) (map ?f ops)"
        using foldl_Cons
        by force
    }
    ultimately show ?case
      by argo
  qed fastforce

corollary execute_parallel_operators_strips_none_if:
  assumes "op  set ops. ¬v  set (add_effects_of op)  ¬v  set (delete_effects_of op)"
    and "s v = None"
  shows "execute_parallel_operator s ops v = None"
  using execute_parallel_operator_no_effect_if[OF assms(1)] assms(2)
  by simp

corollary execute_parallel_operators_strips_none_if_contraposition:
  assumes "¬execute_parallel_operator s ops v = None"
  shows "(op  set ops. v  set (add_effects_of op)  v  set (delete_effects_of op))
     s v  None"
  proof -
    let ?P = "(op  set ops. ¬v  set (add_effects_of op)  ¬v  set (delete_effects_of op))
       s v = None"
      and ?Q = "execute_parallel_operator s ops v = None"
    have "?P  ?Q"
      using execute_parallel_operators_strips_none_if[of ops v s]
      by blast
    then have "¬?P"
      using contrapos_nn[of ?Q ?P]
      using assms
      by argo
    thus ?thesis
      by meson
  qed

text ‹ We will now move on to showing the equivalent to theorem \isaname{operator_effect__strips}
in \isaname{execute_parallel_operator_effect}.
Under the condition that for a list of operators termops all
operators in the corresponding set are applicable in a given state terms and all operator effects
are consistent, if an operator termop exists with termop  set ops and with termv being
an add effect of termop, then the successor state

  @{text[display, indent=4] "s' ≡ execute_parallel_operator s ops"}

will evaluate termv to true, that is

  @{text[display, indent=4] "execute_parallel_operator s ops v = Some True"}

Symmetrically, if termv is a delete effect, we have

  @{text[display, indent=4] "execute_parallel_operator s ops v = Some False"}

under the same condition as for the positive effect.
Lastly, if termv is neither an add effect nor a delete effect for any operator in the
operator set corresponding to $ops$, then the state after parallel operator execution remains
unchanged, i.e.

  @{text[display, indent=4] "execute_parallel_operator s ops v = s v"}

theorem  execute_parallel_operator_effect:
  assumes "are_all_operators_applicable s ops"
  and "are_all_operator_effects_consistent ops"
shows "op  set ops  v  set (add_effects_of op)
   execute_parallel_operator s ops v = Some True"
  and "op  set ops  v  set (delete_effects_of op)
     execute_parallel_operator s ops v = Some False"
  and "(op  set ops.
    v  set (add_effects_of op)  v  set (delete_effects_of op))
     execute_parallel_operator s ops v = s v"
  using execute_parallel_operator_positive_effect_if[OF assms]
    execute_parallel_operator_negative_effect_if[OF assms]
    execute_parallel_operator_no_effect_if[of ops v s]
  by blast+


lemma is_parallel_solution_for_problem_operator_set:
  fixes Π:: "'a strips_problem"
  assumes "is_parallel_solution_for_problem Π π"
    and "ops  set π"
    and "op  set ops"
  shows "op  set ((Π)𝒪)"
  proof -
    have "ops  set π. op  set ops. op  set (strips_problem.operators_of Π)"
      using assms(1)
      unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff..
    thus ?thesis
      using assms(2, 3)
      by fastforce
  qed

lemma trace_parallel_plan_strips_not_nil: "trace_parallel_plan_strips I π  []"
  proof (cases π)
    case (Cons a list)
    then show ?thesis
      by (cases "are_all_operators_applicable I (hd π)  are_all_operator_effects_consistent (hd π)"
        , simp+)
  qed simp

corollary length_trace_parallel_plan_gt_0[simp]: "0 < length (trace_parallel_plan_strips I π)"
  using trace_parallel_plan_strips_not_nil..

corollary length_trace_minus_one_lt_length_trace[simp]:
  "length (trace_parallel_plan_strips I π) - 1 < length (trace_parallel_plan_strips I π)"
  using diff_less[OF _ length_trace_parallel_plan_gt_0]
  by auto

lemma trace_parallel_plan_strips_head_is_initial_state:
  "trace_parallel_plan_strips I π ! 0 = I"
  proof  (cases π)
    case (Cons a list)
    then show ?thesis
      by (cases "are_all_operators_applicable I a  are_all_operator_effects_consistent a", simp+)
  qed simp

lemma trace_parallel_plan_strips_length_gt_one_if:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  shows "1 < length (trace_parallel_plan_strips I π)"
  using assms
  by linarith

― ‹ This lemma simply shows that the last element of a trace_parallel_plan_strips execution›
step s # trace_parallel_plan_strips s' π› always is the last element of
trace_parallel_plan_strips s' π› since trace_parallel_plan_strips› always returns at least a
singleton list (even if π = []›). ›
lemma trace_parallel_plan_strips_last_cons_then:
  "last (s # trace_parallel_plan_strips s' π) = last (trace_parallel_plan_strips s' π)"
  by (cases π, simp, force)

text ‹ Parallel plan traces have some important properties that we want to confirm before
proceeding. Let termτ  trace_parallel_plan_strips I π be a trace for a parallel plan termπ
with initial state termI.

First, all parallel operators termops = π ! k for any index termk with termk < length τ - 1
(meaning that termk is not the index of the last element).
must be applicable and their effects must be consistent. Otherwise, the trace would have terminated
and termops would have been the last element. This would violate the assumption that termk < length τ - 1
is not the last index since the index of the last element is term‹length τ - 1.
\footnote{More precisely, the index of the last element is term‹length τ - 1 if termτ is not
empty which is however always true since the trace contains at least the initial state.} ›

(* TODO? hide? *)
lemma  trace_parallel_plan_strips_operator_preconditions:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  shows "are_all_operators_applicable (trace_parallel_plan_strips I π ! k) (π ! k)
       are_all_operator_effects_consistent (π ! k)"
  using assms
  proof  (induction "π" arbitrary: I k)
    ― ‹ NOTE Base case yields contradiction with assumption and can be left to automation. ›
    case (Cons a π)
    then show ?case
      proof (cases "are_all_operators_applicable I a  are_all_operator_effects_consistent a")
        case True
        have trace_parallel_plan_strips_cons: "trace_parallel_plan_strips I (a # π)
          = I # trace_parallel_plan_strips (execute_parallel_operator I a) π"
          using True
          by simp
        then show ?thesis
        proof (cases "k")
          case 0
          have "trace_parallel_plan_strips I (a # π) ! 0 = I"
            using trace_parallel_plan_strips_cons
            by simp
          moreover have "(a # π) ! 0 = a"
            by simp
          ultimately show ?thesis
            using True 0
            by presburger
        next
          case (Suc k')
          let ?I' = "execute_parallel_operator I a"
          have "trace_parallel_plan_strips I (a # π) ! Suc k' = trace_parallel_plan_strips ?I' π ! k'"
            using trace_parallel_plan_strips_cons
            by simp
          moreover have "(a # π) ! Suc k' = π ! k'"
            by simp
          moreover {
            have "length (trace_parallel_plan_strips I (a # π))
              = 1 + length (trace_parallel_plan_strips ?I' π)"
              unfolding trace_parallel_plan_strips_cons
              by simp
            then have "k' < length (trace_parallel_plan_strips ?I' π) - 1"
              using Suc Cons.prems
              by fastforce
            hence "are_all_operators_applicable (trace_parallel_plan_strips ?I' π ! k') (π ! k')
             are_all_operator_effects_consistent (π ! k')"
              using Cons.IH[of k']
              by blast
          }
          ultimately show ?thesis
            using Suc
            by argo
        qed
      next
        case False
        then have "trace_parallel_plan_strips I (a # π) = [I]"
          by force
        then have "length (trace_parallel_plan_strips I (a # π)) - 1 = 0"
          by simp
        ― ‹ NOTE Thesis follows from contradiction with assumption. ›
        then show ?thesis
          using Cons.prems
          by force
      qed
  qed auto

text ‹ Another interesting property that we verify below is that elements of the trace
store the result of plan prefix execution. This means that for an index termk with\newline
termk < length (trace_parallel_plan_strips I π), the termk-th element of the trace is state
reached by executing the plan prefix term‹take k π consisting of the first termk parallel
operators of termπ. ›

lemma  trace_parallel_plan_plan_prefix:
  assumes "k < length (trace_parallel_plan_strips I π)"
  shows "trace_parallel_plan_strips I π ! k = execute_parallel_plan I (take k π)"
  using assms
  proof  (induction π arbitrary: I k)
    case (Cons a π)
    then show ?case
      proof (cases "are_all_operators_applicable I a  are_all_operator_effects_consistent a")
        case True
        let  = "trace_parallel_plan_strips I (a # π)"
          and ?I' = "execute_parallel_operator I a"
        have σ_equals: " = I # trace_parallel_plan_strips ?I' π"
          using True
          by auto
        then show ?thesis
          proof (cases "k = 0")
            case False
            obtain k' where k_is_suc_of_k': "k = Suc k'"
              using not0_implies_Suc[OF False]
              by blast
            then have "execute_parallel_plan I (take k (a # π))
              = execute_parallel_plan ?I' (take k' π)"
              using True
              by simp
            moreover have "trace_parallel_plan_strips I (a # π) ! k
              = trace_parallel_plan_strips ?I' π ! k'"
              using σ_equals k_is_suc_of_k'
              by simp
            moreover {
              have "k' < length (trace_parallel_plan_strips (execute_parallel_operator I a) π)"
                using Cons.prems σ_equals k_is_suc_of_k'
                by force
              hence "trace_parallel_plan_strips ?I' π ! k'
                = execute_parallel_plan ?I' (take k' π)"
                using Cons.IH[of k' ?I']
                by blast
            }
            ultimately show ?thesis
              by presburger
          qed simp
      next
        case operator_precondition_violated: False
        then show ?thesis
        proof (cases "k = 0")
          case False
          then have "trace_parallel_plan_strips I (a # π) = [I]"
            using operator_precondition_violated
            by force
          moreover have "execute_parallel_plan I (take k (a # π)) = I"
            using Cons.prems operator_precondition_violated
            by force
          ultimately show ?thesis
            using Cons.prems nth_Cons_0
            by auto
        qed simp
      qed
  qed simp


lemma length_trace_parallel_plan_strips_lte_length_plan_plus_one:
  shows "length (trace_parallel_plan_strips I π)  length π + 1"
  proof (induction π arbitrary: I)
    case (Cons a π)
    then show ?case
      proof (cases "are_all_operators_applicable I a  are_all_operator_effects_consistent a")
        case True
        let ?I' = "execute_parallel_operator I a"
        {
          have "trace_parallel_plan_strips I (a # π) = I # trace_parallel_plan_strips ?I' π"
            using True
            by auto
          then have "length (trace_parallel_plan_strips I (a # π))
            = length (trace_parallel_plan_strips ?I' π) + 1"
            by simp
          moreover have "length (trace_parallel_plan_strips ?I' π)  length π + 1"
            using Cons.IH[of ?I']
            by blast
          ultimately have "length (trace_parallel_plan_strips I (a # π))  length (a # π) + 1"
            by simp
        }
        thus ?thesis
          by blast
      qed auto
  qed simp

― ‹ Show that π› is at least a singleton list. ›
lemma plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  obtains ops π' where "π = ops # π'"
  proof -
    let  = "trace_parallel_plan_strips I π"
    have "length   length π + 1"
      using length_trace_parallel_plan_strips_lte_length_plan_plus_one
      by fast
    then have "0 < length π"
      using trace_parallel_plan_strips_length_gt_one_if assms
      by force
    then obtain k' where "length π = Suc k'"
      using gr0_implies_Suc
      by meson
    thus ?thesis using that
      using length_Suc_conv[of π k']
      by blast
  qed

― ‹ Show that if a parallel plan trace does not have maximum length, in the last state
reached through operator execution the parallel operator execution condition was violated. ›
corollary length_trace_parallel_plan_strips_lt_length_plan_plus_one_then:
  assumes "length (trace_parallel_plan_strips I π) < length π + 1"
  shows "¬are_all_operators_applicable
      (execute_parallel_plan I (take (length (trace_parallel_plan_strips I π) - 1) π))
      (π ! (length (trace_parallel_plan_strips I π) - 1))
     ¬are_all_operator_effects_consistent (π ! (length (trace_parallel_plan_strips I π) - 1))"
  using assms
  proof (induction π arbitrary: I)
    case (Cons ops π)
    let  = "trace_parallel_plan_strips I (ops # π)"
      and ?I' = "execute_parallel_operator I ops"
    show ?case
      proof (cases "are_all_operators_applicable I ops  are_all_operator_effects_consistent ops")
        case True
        then have τ_is: " = I # trace_parallel_plan_strips ?I' π"
          by fastforce
        show ?thesis
          proof (cases "length (trace_parallel_plan_strips ?I' π) < length π + 1")
            case True
            then have "¬ are_all_operators_applicable
              (execute_parallel_plan ?I'
                (take (length (trace_parallel_plan_strips ?I' π) - 1) π))
              (π ! (length (trace_parallel_plan_strips ?I' π) - 1))
             ¬ are_all_operator_effects_consistent
              (π ! (length (trace_parallel_plan_strips ?I' π) - 1))"
              using Cons.IH[of ?I']
              by blast
            moreover have "trace_parallel_plan_strips ?I' π  []"
              using trace_parallel_plan_strips_not_nil
              by blast
            ultimately show ?thesis
              unfolding take_Cons'
              by simp
          next
            case False
            then have "length (trace_parallel_plan_strips ?I' π)  length π + 1"
              by fastforce
            thm Cons.prems
            moreover have "length (trace_parallel_plan_strips I (ops # π))
              = 1 + length (trace_parallel_plan_strips ?I' π)"
              using True
              by force
            moreover have "length (trace_parallel_plan_strips ?I' π)
              < length (ops # π)"
              using Cons.prems calculation(2)
              by force
            ultimately have False
              by fastforce
            thus ?thesis..
          qed
      next
        case False
        then have τ_is_singleton: " = [I]"
          using False
          by auto
        then have "ops = (ops # π) ! (length  - 1)"
          by fastforce
        moreover have "execute_parallel_plan I (take (length  - 1) π) = I"
          using τ_is_singleton
          by auto
        ― ‹ TODO slow. ›
        ultimately show ?thesis
          using False
          by auto
      qed
  qed simp

lemma trace_parallel_plan_step_effect_is:
  assumes "k < length (trace_parallel_plan_strips I π) - 1"
  shows "trace_parallel_plan_strips I π ! Suc k
    = execute_parallel_operator (trace_parallel_plan_strips I π ! k) (π ! k)"
  proof -
    ― ‹ NOTE Rewrite the proposition using lemma trace_parallel_plan_strips_subplan›. ›
    {
      let  = "trace_parallel_plan_strips I π"
      have "Suc k < length "
        using assms
        by linarith
      hence "trace_parallel_plan_strips I π ! Suc k
        = execute_parallel_plan I (take (Suc k) π)"
        using trace_parallel_plan_plan_prefix[of "Suc k" I π]
        by blast
    }
    moreover have "execute_parallel_plan I (take (Suc k) π)
      = execute_parallel_operator (trace_parallel_plan_strips I π ! k) (π ! k)"
      using assms
      proof (induction k arbitrary: I π)
        case 0
        then have "execute_parallel_operator (trace_parallel_plan_strips I π ! 0) (π ! 0)
            = execute_parallel_operator I (π ! 0)"
          using trace_parallel_plan_strips_head_is_initial_state[of I π]
          by argo
        moreover {
          obtain ops π' where "π = ops # π'"
            using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF "0.prems"]
            by blast
          then have "take (Suc 0) π = [π ! 0]"
            by simp
          hence "execute_parallel_plan I (take (Suc 0) π)
            = execute_parallel_plan I [π ! 0]"
            by argo
        }
        moreover {
          have "0 < length (trace_parallel_plan_strips I π) - 1"
            using trace_parallel_plan_strips_length_gt_one_if "0.prems"
            by fastforce
          hence "are_all_operators_applicable I (π ! 0)
             are_all_operator_effects_consistent (π ! 0)"
            using trace_parallel_plan_strips_operator_preconditions[of 0 I π]
              trace_parallel_plan_strips_head_is_initial_state[of I π]
            by argo
        }
        ultimately show ?case
          by auto
      next
        case (Suc k)
        obtain ops π' where π_split: "π = ops # π'"
          using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF Suc.prems]
          by blast
        let ?I' = "execute_parallel_operator I ops"
        {
          have "length (trace_parallel_plan_strips I π) =
            1 + length (trace_parallel_plan_strips ?I' π')"
            using Suc.prems π_split
            by fastforce
          then have "k < length (trace_parallel_plan_strips ?I' π')"
            using Suc.prems
            by fastforce
          moreover have "trace_parallel_plan_strips I π ! Suc k
            = trace_parallel_plan_strips ?I' π' ! k"
            using Suc.prems π_split
            by force
          ultimately have "trace_parallel_plan_strips I π ! Suc k
            = execute_parallel_plan ?I' (take k π')"
            using trace_parallel_plan_plan_prefix[of k ?I' π']
            by argo
        }
        moreover have "execute_parallel_plan I (take (Suc (Suc k)) π)
          = execute_parallel_plan ?I' (take (Suc k) π')"
          using Suc.prems π_split
          by fastforce
        moreover {
          have "0 < length (trace_parallel_plan_strips I π) - 1"
            using Suc.prems
            by linarith
          hence "are_all_operators_applicable I (π ! 0)
             are_all_operator_effects_consistent (π ! 0)"
            using trace_parallel_plan_strips_operator_preconditions[of 0 I π]
              trace_parallel_plan_strips_head_is_initial_state[of I π]
            by argo
        }
        ultimately show ?case
          using Suc.IH Suc.prems π_split
          by auto
      qed
    ultimately show ?thesis
      using assms
      by argo
  qed

― ‹ Show that every state in a plan execution trace of a valid problem description is defined
for all problem variables. This is true because the initial state is defined for all problem
variables—by definition of @{text "is_valid_problem_strips Π"}—and no operator can remove a
previously defined variable (only positive and negative effects are possible). ›
(* TODO refactor ‹STRIPS_Semantics› + abstract/concretize first two assumptions (e.g. second one
only needs all operators are problem operators)? *)
lemma trace_parallel_plan_strips_none_if:
  fixes Π:: "'a strips_problem"
  assumes "is_valid_problem_strips Π"
    and "is_parallel_solution_for_problem Π π"
    and "k < length (trace_parallel_plan_strips ((Π)I) π)"
  shows "(trace_parallel_plan_strips ((Π)I) π ! k) v = None  v  set ((Π)𝒱)"
  proof -
    let ?vs = "strips_problem.variables_of Π"
      and ?ops = "strips_problem.operators_of Π"
      and  = "trace_parallel_plan_strips ((Π)I) π"
      and ?I = "strips_problem.initial_of Π"
    show ?thesis
      using assms
      proof (induction k)
        case 0
        have " ! 0 = ?I"
          using trace_parallel_plan_strips_head_is_initial_state
          by auto
        then show ?case
          using is_valid_problem_strips_initial_of_dom[OF assms(1)]
          by auto
      next
        case (Suc k)
        have k_lt_length_τ_minus_one: "k < length  - 1"
          using Suc.prems(3)
          by linarith
        then have IH: "(trace_parallel_plan_strips ?I π ! k) v = None  v set ((Π)𝒱)"
          using Suc.IH[OF Suc.prems(1, 2)]
          by force
        have τ_Suc_k_is: "( ! Suc k) = execute_parallel_operator ( ! k) (π ! k)"
          using trace_parallel_plan_step_effect_is[OF k_lt_length_τ_minus_one].
        have all_operators_applicable: "are_all_operators_applicable ( ! k) (π ! k)"
          and all_effects_consistent: "are_all_operator_effects_consistent (π ! k)"
          using trace_parallel_plan_strips_operator_preconditions[OF k_lt_length_τ_minus_one]
          by simp+
        show ?case
          proof (rule iffI)
            assume τ_Suc_k_of_v_is_None: "( ! Suc k) v = None"
            show "v  set ((Π)𝒱)"
              proof (rule ccontr)
                assume "¬v  set ((Π)𝒱)"
                then have v_in_set_vs: "v  set((Π)𝒱)"
                  by blast
                show False
                  proof (cases "op  set (π ! k).
                    v  set (add_effects_of op)  v  set (delete_effects_of op)")
                    case True
                    then obtain op
                      where op_in_πk: "op  set (π ! k)"
                        and "v  set (add_effects_of op)  v  set (delete_effects_of op)"..
                    then consider (A) "v  set (add_effects_of op)"
                      | (B) "v  set (delete_effects_of op)"
                      by blast
                    thus False
                      using execute_parallel_operator_positive_effect_if[OF
                              all_operators_applicable all_effects_consistent op_in_πk]
                            execute_parallel_operator_negative_effect_if[OF
                              all_operators_applicable all_effects_consistent op_in_πk]
                            τ_Suc_k_of_v_is_None τ_Suc_k_is
                      by (cases, fastforce+)
                  next
                    case False
                    then have "op  set (π ! k).
                      v  set (add_effects_of op)  v  set (delete_effects_of op)"
                      by blast
                    then have "( ! Suc k) v = ( ! k) v"
                      using execute_parallel_operator_no_effect_if τ_Suc_k_is
                      by fastforce
                    then have "v  set ((Π)𝒱)"
                      using IH  τ_Suc_k_of_v_is_None
                      by simp
                    thus False
                      using v_in_set_vs
                      by blast
                  qed
              qed
          next
            assume v_notin_vs: "v  set ((Π)𝒱)"
            {
              fix op
              assume op_in_πk: "op  set (π ! k)"
              {
                have "1 < length "
                  using trace_parallel_plan_strips_length_gt_one_if[OF k_lt_length_τ_minus_one].
                then have "0 < length  - 1"
                  using k_lt_length_τ_minus_one
                  by linarith
                moreover have "length  - 1  length π"
                  using length_trace_parallel_plan_strips_lte_length_plan_plus_one le_diff_conv
                  by blast
                then have "k < length π"
                  using k_lt_length_τ_minus_one
                  by force
                hence "π ! k  set π"
                  by simp
              }
              then have op_in_ops: "op  set ?ops"
                using is_parallel_solution_for_problem_operator_set[OF assms(2) _ op_in_πk]
                by force
              hence "v  set (add_effects_of op)" and "v  set (delete_effects_of op)"
                subgoal
                  using is_valid_problem_strips_operator_variable_sets(2) assms(1) op_in_ops
                    v_notin_vs
                  by auto
                subgoal
                  using is_valid_problem_strips_operator_variable_sets(3) assms(1) op_in_ops
                    v_notin_vs
                  by auto
                done
            }
            then have "( ! Suc k) v = ( ! k) v"
              using execute_parallel_operator_no_effect_if τ_Suc_k_is
              by metis
            thus "( ! Suc k) v = None"
              using IH v_notin_vs
              by fastforce
          qed
      qed
  qed

text ‹ Finally, given initial and goal states termI and termG, we can show that it's
equivalent to say that termπ is a solution for termI and termG---i.e.
termG m execute_parallel_plan I π---and
that the goal state is subsumed by the last element of the trace of termπ with initial state
termI. ›

lemma  execute_parallel_plan_reaches_goal_iff_goal_is_last_element_of_trace:
  "G m execute_parallel_plan I π
     G m last (trace_parallel_plan_strips I π)"
  proof  -
    let ?LHS = "G m execute_parallel_plan I π"
      and ?RHS = "G m last (trace_parallel_plan_strips I π)"
    show ?thesis
      proof (rule iffI)
        assume ?LHS
        thus ?RHS
          proof (induction π arbitrary: I)
            ― ‹ NOTE Nil case follows from simplification. ›
            case (Cons a π)
            thus ?case
              using Cons.prems
              proof (cases "are_all_operators_applicable I a  are_all_operator_effects_consistent a")
                case True
                let ?I' = "execute_parallel_operator I a"
                {
                  have "execute_parallel_plan I (a # π) = execute_parallel_plan ?I' π"
                    using True
                    by auto
                  then have "G m execute_parallel_plan ?I' π"
                    using Cons.prems
                    by presburger
                  hence "G m last (trace_parallel_plan_strips ?I' π)"
                    using Cons.IH[of ?I']
                    by blast
                }
                moreover {
                  have "trace_parallel_plan_strips I (a # π)
                    = I # trace_parallel_plan_strips ?I' π"
                    using True
                    by simp
                  then have "last (trace_parallel_plan_strips I (a # π))
                    = last (I # trace_parallel_plan_strips ?I' π)"
                    by argo
                  hence "last (trace_parallel_plan_strips I (a # π))
                    = last (trace_parallel_plan_strips ?I' π)"
                    using trace_parallel_plan_strips_last_cons_then[of I ?I' π]
                    by argo
                }
                ultimately show ?thesis
                  by argo
              qed force
            qed simp
      next
        assume ?RHS
        thus ?LHS
          proof (induction π arbitrary: I)
            ― ‹ NOTE Nil case follows from simplification. ›
            case (Cons a π)
            thus ?case
              proof (cases "are_all_operators_applicable I a  are_all_operator_effects_consistent a")
                case True
                let ?I' = "execute_parallel_operator I a"
                {
                  have "trace_parallel_plan_strips I (a # π) = I # (trace_parallel_plan_strips ?I' π)"
                    using True
                    by simp
                  then have "last (trace_parallel_plan_strips I (a # π))
                    = last (trace_parallel_plan_strips ?I' π)"
                    using trace_parallel_plan_strips_last_cons_then[of I ?I' π]
                    by argo
                  hence "G m last (trace_parallel_plan_strips ?I' π)"
                    using Cons.prems
                    by argo
                }
                thus ?thesis
                  using True Cons
                  by simp
              next
                case False
                then have "last (trace_parallel_plan_strips I (a # π)) = I"
                  and "execute_parallel_plan I (a # π) = I"
                  by (fastforce, force)
                thus ?thesis
                  using Cons.prems
                  by argo
              qed
          qed fastforce
      qed
  qed

subsection "Serializable Parallel Plans"

text ‹ With the groundwork on parallel and serial execution of STRIPS in place we can now address
the question under which conditions a parallel solution to a problem corresponds to a serial
solution and vice versa.
As we will see (in theorem \ref{isathm:embedding-serial-strips-plan}), while a serial plan can
be trivially rewritten as a parallel plan consisting of singleton operator list for each operator
in the plan, the condition for parallel plan solutions also involves non interference. ›


― ‹ Given that non interference implies that operator execution order can be switched
arbitrarily, it stands to reason that parallel operator execution can be serialized if non
interference is mandated in addition to the regular parallel execution condition (applicability and
effect consistency). This is in fact true as we show in the lemma below
\footnote{In the source literatur it is required that $\mathrm{app}_S(s)$ is defined which requires that
$\mathrm{app}_o(s)$ is defined for every $o \in S$. This again means that the preconditions
hold in $s$ and the set of effects is consistent which translates to the execution condition
in execute_parallel_operator›.
\cite[Lemma 2.11., p.1037]{DBLP:journals/ai/RintanenHN06}

Also, the proposition \cite[Lemma 2.11., p.1037]{DBLP:journals/ai/RintanenHN06} is in fact
proposed to be true for any total ordering of the operator set but we only proof it for the
implicit total ordering induced by the specific order in the operator list of the problem
statement.} ›
(* TODO rename execute_parallel_operator_equals_execute_serial_if *)
lemma execute_parallel_operator_equals_execute_sequential_strips_if:
  fixes s :: "('variable, bool) state"
  assumes "are_all_operators_applicable s ops"
    and "are_all_operator_effects_consistent ops"
    and "are_all_operators_non_interfering ops"
  shows "execute_parallel_operator s ops = execute_serial_plan s ops"
  using assms
  proof (induction ops arbitrary: s)
    case Nil
    have "execute_parallel_operator s Nil
      = foldl (++) s (map (map_of  effect_to_assignments) Nil)"
      using Nil.prems(1,2)
      unfolding execute_parallel_operator_def
      by presburger
    also have " = s"
      by simp
    finally have "execute_parallel_operator s Nil = s"
      by blast
    moreover have "execute_serial_plan s Nil = s"
      by auto
    ultimately show ?case
      by simp
  next
    case (Cons a ops)
    ― ‹ NOTE Use the preceding lemmas to show that the premises hold for the sublist and use the IH
  to obtain the theorem for the sublist ops. ›
    have a: "is_operator_applicable_in s a"
      using are_all_operators_applicable_cons Cons.prems(1)
      by blast+
    let ?s' = "s ++ map_of (effect_to_assignments a)"
    {
      from Cons.prems
      have "are_all_operators_applicable ?s' ops"
        and "are_all_operator_effects_consistent ops"
        and "are_all_operators_non_interfering ops"
        using execute_parallel_plan_precondition_cons
        by blast+
      then have "execute_serial_plan ?s' ops
        = execute_parallel_operator ?s' ops"
        using Cons.IH
        by presburger
    }
    moreover from Cons.prems
    have "execute_parallel_operator s (Cons a ops)
      = execute_parallel_operator ?s' ops"
      using execute_parallel_operator_cons_equals_corollary
      unfolding execute_operator_def
      by simp
    moreover
    from a have "execute_serial_plan s (Cons a ops)
      = execute_serial_plan ?s' ops"
      unfolding execute_serial_plan_def execute_operator_def
        is_operator_applicable_in_def
      by fastforce
    ultimately show ?case
      by argo
  qed

lemma execute_serial_plan_split_i:
  assumes "are_all_operators_applicable s (op # π)"
    and "are_all_operators_non_interfering (op # π)"
  shows "are_all_operators_applicable (s  op) π"
  using assms
  proof (induction π arbitrary: s)
    case Nil
    then show ?case
      unfolding are_all_operators_applicable_def
      by simp
  next
    case (Cons op' π)
    let ?t = "s  op"
    {
      fix x
      assume "x  set (op' # π)"
      moreover have "op  set (op # op' # π)"
        by simp
      moreover have "¬are_operators_interfering op x"
        using Cons.prems(2) calculation(1)
        unfolding are_all_operators_non_interfering_def list_all_iff
        by fastforce
      moreover have "is_operator_applicable_in s op"
        using Cons.prems(1)
        unfolding are_all_operators_applicable_def list_all_iff
          is_operator_applicable_in_def
        by force
      moreover have "is_operator_applicable_in s x"
        using are_all_operators_applicable_cons(2)[OF Cons.prems(1)] calculation(1)
        unfolding are_all_operators_applicable_def list_all_iff
          is_operator_applicable_in_def
        by fast
      ultimately have "is_operator_applicable_in ?t x"
        using execute_parallel_plan_precondition_cons_i[of op x s]
        by (auto simp: execute_operator_def)
    }
    thus ?case
      using are_all_operators_applicable_cons(2)
      unfolding is_operator_applicable_in_def
        STRIPS_Representation.is_operator_applicable_in_def
        are_all_operators_applicable_def list_all_iff
      by simp
  qed

― ‹ Show that plans $\pi$ can be split into separate executions of partial plans $\pi_1$ and
$\pi_2$ with $\pi = \pi_1 @ \pi_2$, if all operators in $\pi_1$ are applicable in the given state
$s$ and there is no interference between subsequent operators in $\pi_1$. This is the case because
non interference ensures that no precondition for any operator in $\pi_1$ is negated by the
execution of a preceding operator. Note that the non interference constraint excludes partial
plans where a precondition is first violated during execution but later restored which would also
allow splitting but does not meet the non interference constraint (which must hold for all
possible executing orders). ›
lemma execute_serial_plan_split:
  fixes s :: "('variable, bool) state"
  assumes "are_all_operators_applicable s π1"
    and "are_all_operators_non_interfering π1"
  shows "execute_serial_plan s (π1 @ π2)
    = execute_serial_plan (execute_serial_plan s π1) π2"
  using assms
  proof (induction π1 arbitrary: s)
    case (Cons op π1)
    let ?t = "s  op"
    {
      have "are_all_operators_applicable (s  op) π1"
        using execute_serial_plan_split_i[OF Cons.prems(1, 2)].
      moreover have "are_all_operators_non_interfering π1"
        using are_all_operators_non_interfering_tail[OF Cons.prems(2)].
      ultimately have "execute_serial_plan ?t (π1 @ π2) =
        execute_serial_plan (execute_serial_plan ?t π1) π2"
        using Cons.IH[of ?t]
        by blast
    }
    moreover have "STRIPS_Representation.is_operator_applicable_in s op"
      using Cons.prems(1)
      unfolding are_all_operators_applicable_def list_all_iff
      by fastforce
    ultimately show ?case
      unfolding execute_serial_plan_def
      by simp
  qed simp

(* TODO refactor *)
lemma embedding_lemma_i:
  fixes I :: "('variable, bool) state"
  assumes "is_operator_applicable_in I op"
    and "are_operator_effects_consistent op op"
  shows "I  op = execute_parallel_operator I [op]"
  proof -
    have "are_all_operators_applicable I [op]"
      using assms(1)
      unfolding are_all_operators_applicable_def list_all_iff is_operator_applicable_in_def
      by fastforce
    moreover have "are_all_operator_effects_consistent [op]"
      unfolding are_all_operator_effects_consistent_def list_all_iff
      using assms(2)
      by fastforce
    moreover have "are_all_operators_non_interfering [op]"
      by simp
    moreover have "I  op = execute_serial_plan I [op]"
      using assms(1)
      unfolding  is_operator_applicable_in_def
      by (simp add: assms(1) execute_operator_def)
    ultimately show ?thesis
      using execute_parallel_operator_equals_execute_sequential_strips_if
      by force
  qed

lemma execute_serial_plan_is_execute_parallel_plan_ii:
  fixes I :: "'variable strips_state"
  assumes "op  set π. are_operator_effects_consistent op op"
    and "G m execute_serial_plan I π"
  shows "G m execute_parallel_plan I (embed π)"
  proof -
    show ?thesis
      using assms
      proof (induction π arbitrary: I)
        case (Cons op π)
        then show ?case
          proof (cases "is_operator_applicable_in I op")
            case True
            let ?J = "I  op"
              and ?J' = "execute_parallel_operator I [op]"
            {
              have "G m execute_serial_plan ?J π"
                using Cons.prems(2) True
                unfolding is_operator_applicable_in_def
                by (simp add: True)
              hence "G m execute_parallel_plan ?J (embed π)"
                using Cons.IH[of ?J] Cons.prems(1)
                by fastforce
            }
            moreover {
              have "are_all_operators_applicable I [op]"
                using True
                unfolding are_all_operators_applicable_def list_all_iff
                  is_operator_applicable_in_def
                by fastforce
              moreover have "are_all_operator_effects_consistent [op]"
                unfolding are_all_operator_effects_consistent_def list_all_iff
                using Cons.prems(1)
                by fastforce
              moreover have "?J = ?J'"
                using execute_parallel_operator_equals_execute_sequential_strips_if[OF
                    calculation(1, 2)] Cons.prems(1) True
                unfolding  is_operator_applicable_in_def
                by (simp add: True)
              ultimately have "execute_parallel_plan I (embed (op # π))
                = execute_parallel_plan ?J (embed π)"
                by fastforce
            }
            ultimately show ?thesis
              by presburger
          next
            case False
            then have "G m I"
              using Cons.prems is_operator_applicable_in_def
              by simp
            moreover {
              have "¬are_all_operators_applicable I [op]"
                using False
                unfolding are_all_operators_applicable_def list_all_iff
                  is_operator_applicable_in_def
                by force
              hence "execute_parallel_plan I (embed (op # π)) = I"
                by simp
            }
            ultimately show ?thesis
              by presburger
          qed
      qed simp
  qed

lemma embedding_lemma_iii:
  fixes Π:: "'a strips_problem"
  assumes "op  set π. op  set ((Π)𝒪)"
  shows "ops  set (embed π). op  set ops. op  set ((Π)𝒪)"
  proof -
    (* TODO refactor *)
    have nb: "set (embed π) = { [op] | op. op  set π }"
      by (induction π; force)
    {
      fix ops
      assume "ops  set (embed π)"
      moreover obtain op where "op  set π" and "ops = [op]"
        using nb calculation
        by blast
      ultimately have "op  set ops. op  set ((Π)𝒪)"
        using assms(1)
        by simp
    }
    thus ?thesis..
  qed

text ‹ We show in the following theorem that---as mentioned---a serial solution termπ to a
STRIPS problem termΠ corresponds directly to a parallel solution obtained by embedding each operator
in termπ in a list (by use of function term‹embed›). The proof shows this by first
confirming that

    @{text[display, indent=4] "G ⊆m execute_serial_plan ((Π)I) π
    ⟹ G ⊆m execute_serial_plan ((Π)I) (embed π)"}

using lemma \isaname{execute_serial_plan_is_execute_parallel_plan_strip_ii}; and
moreover by showing that

    @{text[display, indent=4] "∀ops ∈ set (embed π). ∀op ∈ set ops. op ∈ (Π)𝒪"}

meaning that under the given assumptions, all parallel operators of the embedded serial plan are
again operators in the operator set of the problem. ›
theorem  embedding_lemma:
  assumes "is_valid_problem_strips Π"
    and "is_serial_solution_for_problem Π π"
  shows "is_parallel_solution_for_problem Π (embed π)"
  proof  -
    (* TODO refactor ‹STRIPS_Representation› (characterization of valid operator).
  *)have nb1: "op  set π. op  set ((Π)𝒪)"
      using assms(2)
      unfolding is_serial_solution_for_problem_def list_all_iff ListMem_iff operators_of_def
      by blast
    (* TODO refactor lemma is_valid_operator_strips_then
  *)      {
      fix op
      assume "op  set π"
      moreover have "op  set ((Π)𝒪)"
        using nb1 calculation
        by fast
      moreover have "is_valid_operator_strips Π op"
        using assms(1) calculation(2)
        unfolding is_valid_problem_strips_def is_valid_problem_strips_def list_all_iff operators_of_def
        by meson
      moreover have "list_all (λv. ¬ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "list_all (λv. ¬ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(3)
        unfolding is_valid_operator_strips_def
        by meson+
      moreover have "¬list_ex (λv. ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(4, 5) not_list_ex_equals_list_all_not
        by blast+
      moreover have "¬list_ex (λv. list_ex ((=) v) (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. list_ex ((=) v) (add_effects_of op)) (delete_effects_of op)"
        using calculation(6, 7)
        unfolding list_ex_iff ListMem_iff
        by blast+
      ultimately have "are_operator_effects_consistent op op"
        unfolding are_operator_effects_consistent_def Let_def
        by blast
    } note nb2 = this
    moreover {
      have "(Π)G m execute_serial_plan ((Π)I) π"
        using assms(2)
        unfolding is_serial_solution_for_problem_def
        by simp
      hence "(Π)G m execute_parallel_plan ((Π)I) (embed π)"
        using execute_serial_plan_is_execute_parallel_plan_ii nb2
        by blast
    }
    moreover have "ops  set (embed π). op  set ops. op  set ((Π)𝒪)"
      using embedding_lemma_iii[OF nb1].
    ultimately show ?thesis
      unfolding is_parallel_solution_for_problem_def goal_of_def
        initial_of_def operators_of_def list_all_iff ListMem_iff
      by blast
  qed

lemma flattening_lemma_i:
  fixes Π:: "'a strips_problem"
  assumes "ops  set π. op  set ops. op  set ((Π)𝒪)"
  shows "op  set (concat π). op  set ((Π)𝒪)"
  proof -
    {
      fix op
      assume "op  set (concat π)"
      moreover have "op  (ops  set π. set ops)"
        using calculation
        unfolding set_concat.
      then obtain ops where "ops  set π" and "op  set ops"
        using UN_iff
        by blast
      ultimately have "op  set ((Π)𝒪)"
        using assms
        by blast
    }
    thus ?thesis..
  qed

lemma flattening_lemma_ii:
  fixes I :: "'variable strips_state"
  assumes "ops  set π. op. ops = [op]  is_valid_operator_strips Π op "
    and "G m execute_parallel_plan I π"
  shows "G m execute_serial_plan I (concat π)"
  proof -
    let ?π' = "concat π"
    (* TODO refactor lemma is_valid_operator_strips_then *)
    {
      fix op
      assume "is_valid_operator_strips Π op"
      moreover have "list_all (λv. ¬ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "list_all (λv. ¬ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(1)
        unfolding is_valid_operator_strips_def
        by meson+
      moreover have "¬list_ex (λv. ListMem v (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. ListMem v (add_effects_of op)) (delete_effects_of op)"
        using calculation(2, 3) not_list_ex_equals_list_all_not
        by blast+
      moreover have "¬list_ex (λv. list_ex ((=) v) (delete_effects_of op)) (add_effects_of op)"
        and "¬list_ex (λv. list_ex ((=) v) (add_effects_of op)) (delete_effects_of op)"
        using calculation(4, 5)
        unfolding list_ex_iff ListMem_iff
        by blast+
      ultimately have "are_operator_effects_consistent op op"
        unfolding are_operator_effects_consistent_def Let_def
        by blast
    } note nb1 = this
    show ?thesis
      using assms
      proof (induction π arbitrary: I)
        case (Cons ops π)
        obtain op where ops_is: "ops = [op]" and is_valid_op: "is_valid_operator_strips Π op"
          using Cons.prems(1)
          by fastforce
        show ?case
          proof (cases "are_all_operators_applicable I ops")
            case True
            let ?J = "execute_parallel_operator I [op]"
              and ?J' = "I  op"
            have nb2: "is_operator_applicable_in I op"
              using True ops_is
              unfolding are_all_operators_applicable_def list_all_iff
                is_operator_applicable_in_def
              by simp
            have nb3: "are_operator_effects_consistent op op"
              using nb1[OF is_valid_op].
            {
              then have "are_all_operator_effects_consistent ops"
                unfolding are_all_operator_effects_consistent_def list_all_iff
                using ops_is
                by fastforce
              hence "G m execute_parallel_plan ?J π"
                using Cons.prems(2) ops_is True
                by fastforce
            }
            moreover have "execute_serial_plan I (concat (ops # π))
              = execute_serial_plan ?J' (concat π)"
              using ops_is nb2
              unfolding is_operator_applicable_in_def
              by (simp add: execute_operator_def nb2)
            moreover have "?J = ?J'"
              unfolding execute_parallel_operator_def execute_operator_def comp_apply
              by fastforce
            ultimately show ?thesis
              using Cons.IH Cons.prems
              by force
          next
            case False
            moreover have "G m I"
              using Cons.prems(2) calculation
              by force
            moreover {
              have "¬is_operator_applicable_in I op"
                using ops_is False
                unfolding are_all_operators_applicable_def list_all_iff
                  is_operator_applicable_in_def
                by fastforce
              hence "execute_serial_plan I (concat (ops # π)) = I"
                using ops_is is_operator_applicable_in_def
                by simp
            }
            ultimately show ?thesis
              by argo
          qed
      qed force
  qed

text ‹ The opposite direction is also easy to show if we can normalize the parallel plan to the
form of an embedded serial plan as shown below. ›

lemma flattening_lemma:
  assumes "is_valid_problem_strips Π"
    and "ops  set π. op. ops = [op]"
    and "is_parallel_solution_for_problem Π π"
  shows "is_serial_solution_for_problem Π (concat π)"
  proof  -
    let ?π' = "concat π"
    {
      have "ops  set π. op  set ops. op  set ((Π)𝒪)"
        using assms(3)
        unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff
        by force
      hence "op  set ?π'. op  set ((Π)𝒪)"
        using flattening_lemma_i
        by blast
    }
    moreover {
      {
        fix ops
        assume "ops  set π"
        moreover obtain op where "ops = [op]"
          using assms(2) calculation
          by blast
        moreover have "op  set ((Π)𝒪)"
          using assms(3) calculation
          unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff
          by force
        moreover have "is_valid_operator_strips Π op"
          using assms(1) calculation(3)
          unfolding is_valid_problem_strips_def Let_def list_all_iff ListMem_iff
          by simp
        ultimately have "op. ops = [op]  is_valid_operator_strips Π op"
          by blast
      }
      moreover have "(Π)G m execute_parallel_plan ((Π)I) π"
        using assms(3)
        unfolding is_parallel_solution_for_problem_def
        by simp
      ultimately have "(Π)G m execute_serial_plan ((Π)I) ?π'"
        using flattening_lemma_ii
        by blast
    }
    ultimately show "is_serial_solution_for_problem Π ?π'"
      unfolding is_serial_solution_for_problem_def list_all_iff ListMem_iff
      by simp
  qed


text ‹ Finally, we can obtain the important result that a parallel plan with a trace that
reaches the goal state of a given problem termΠ, and for which both the parallel operator execution
condition as well as non interference is assured at every point termk < length π, the flattening of
the parallel plan term‹concat π is a serial solution for the initial and goal state of the problem.
To wit, by lemma \ref{isathm:parallel-solution-trace-strips} we have

    @{text[display, indent=4] "(G ⊆m execute_parallel_plan I π)
      = (G ⊆m last (trace_parallel_plan_strips I π))"}

so the second assumption entails that termπ is a solution for the initial state and the goal state
of the problem. (which implicitely means that  termπ is a solution
for the inital state and goal state of the problem). The trace formulation is used in this case
because it allows us to write the---state dependent---applicability condition more succinctly. The
proof (shown below) is by structural induction on termπ with arbitrary initial state.›

(* TODO Demote to lemma; add theorem about problem solutions. Move text to theorem. *)
theorem  execute_parallel_plan_is_execute_sequential_plan_if:
  fixes I :: "('variable, bool) state"
  assumes "is_valid_problem Π"
    and "G m last (trace_parallel_plan_strips I π)"
    and "k < length π.
      are_all_operators_applicable (trace_parallel_plan_strips I π ! k) (π ! k)
       are_all_operator_effects_consistent (π ! k)
       are_all_operators_non_interfering (π ! k)"
  shows "G m execute_serial_plan I (concat π)"
  using assms
  proof (induction π arbitrary: I)
    case (Cons ops π)
    let ?ops' = "take (length ops) (concat (ops # π))"
    let ?J = "execute_parallel_operator I ops"
      and ?J' = "execute_serial_plan I ?ops'"
    {
      have "trace_parallel_plan_strips I π ! 0 = I" and "(ops # π) ! 0 = ops"
        unfolding trace_parallel_plan_strips_head_is_initial_state
        by simp+
      then have "are_all_operators_applicable I ops"
        and "are_all_operator_effects_consistent ops"
        and "are_all_operators_non_interfering ops"
        using Cons.prems(3)
        by auto+
      then have "trace_parallel_plan_strips I (ops # π)
        = I # trace_parallel_plan_strips ?J π"
        by fastforce
    } note nb = this
    {
      have "last (trace_parallel_plan_strips I (ops # π))
        = last (trace_parallel_plan_strips ?J π)"
        using trace_parallel_plan_strips_last_cons_then nb
        by metis
      hence "G m last (trace_parallel_plan_strips ?J π)"
        using Cons.prems(2)
        by force
    }
    moreover {
      fix k
      assume "k < length π"
      moreover have "k + 1 < length (ops # π)"
        using calculation
        by force
      moreover have "π ! k = (ops # π) ! (k + 1)"
        by simp
      ultimately have "are_all_operators_applicable
        (trace_parallel_plan_strips ?J π ! k) (π ! k)"
        and "are_all_operator_effects_consistent (π ! k)"
        and "are_all_operators_non_interfering (π ! k)"
        using Cons.prems(3) nb
        by force+
    }
    ultimately have "G m execute_serial_plan ?J (concat π)"
      using Cons.IH[OF Cons.prems(1), of ?J]
      by blast
    moreover {
      have "execute_serial_plan I (concat (ops # π))
        = execute_serial_plan ?J' (concat π)"
        using execute_serial_plan_split[of I ops] Cons.prems(3)
        by auto
      thm execute_parallel_operator_equals_execute_sequential_strips_if[of I]
      moreover have "?J = ?J'"
        using execute_parallel_operator_equals_execute_sequential_strips_if Cons.prems(3)
        by fastforce
      ultimately have "execute_serial_plan I (concat (ops # π))
        = execute_serial_plan ?J (concat π)"
        using execute_serial_plan_split[of I ops] Cons.prems(3)
        by argo
    }
    ultimately show ?case
      by argo
  qed force

subsection "Auxiliary lemmas about STRIPS"

lemma set_to_precondition_of_op_is[simp]: "set (to_precondition op)
  = { (v, True) | v. v  set (precondition_of op) }"
  unfolding to_precondition_def STRIPS_Representation.to_precondition_def set_map
  by blast


end

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

Theory SAS_Plus_Semantics

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAS_Plus_Semantics  
  imports "SAS_Plus_Representation" "List_Supplement"
    "Map_Supplement"
begin
section "SAS+ Semantics"


subsection "Serial Execution Semantics"

text ‹ Serial plan execution is implemented recursively just like in the STRIPS case. By and large, 
compared to definition \ref{isadef:plan-execution-strips}, we only substitute the operator 
applicability function with its SAS+ counterpart. ›

primrec execute_serial_plan_sas_plus
  where "execute_serial_plan_sas_plus s [] = s"
  | "execute_serial_plan_sas_plus s (op # ops) 
    = (if is_operator_applicable_in s op 
    then execute_serial_plan_sas_plus (execute_operator_sas_plus s op) ops
    else s)" 

text ‹ Similarly, serial SAS+ solutions are defined just like in STRIPS but based on the 
corresponding SAS+ definitions. ›

definition is_serial_solution_for_problem
  :: "('variable, 'domain) sas_plus_problem  ('variable, 'domain) sas_plus_plan  bool" 
  where "is_serial_solution_for_problem Ψ ψ
     let 
        I = sas_plus_problem.initial_of Ψ
        ; G = sas_plus_problem.goal_of Ψ
        ; ops = sas_plus_problem.operators_of Ψ
      in G m execute_serial_plan_sas_plus I ψ
         list_all (λop. ListMem op ops) ψ" 


context
begin

private lemma execute_operator_sas_plus_effect_i:
  assumes "is_operator_applicable_in s op"
    and "(v, a)  set (effect_of op). (v', a')  set (effect_of op).
      v  v'  a = a'"
    and"(v, a)  set (effect_of op)"
  shows "(s + op) v = Some a"
proof -
  let ?effect = "effect_of op"
  have "map_of ?effect v = Some a" 
    using map_of_constant_assignments_defined_if[OF assms(2, 3)] try0
    by blast
  thus ?thesis 
    unfolding execute_operator_sas_plus_def map_add_def
    by fastforce
qed
    
private lemma  execute_operator_sas_plus_effect_ii:
  assumes "is_operator_applicable_in s op"
    and "(v', a')  set (effect_of op). v'  v"
  shows "(s + op) v = s v"
proof -
  let ?effect = "effect_of op" 
  {
    have "v  fst ` set ?effect" 
      using assms(2)
      by fastforce
    then have "v  dom (map_of ?effect)"
      using dom_map_of_conv_image_fst[of ?effect]
      by argo
    hence "(s ++ map_of ?effect) v = s v" 
      using map_add_dom_app_simps(3)[of v "map_of ?effect" s]
      by blast
  }
  thus ?thesis 
    by fastforce
qed

text ‹ Given an operator termop that is applicable in a state terms and has a consistent set 
of effects (second assumption) we can now show that the successor state terms'  s + op 
has the following properties:
\begin{itemize}
  \item terms' v = Some a if term(v, a) exist in term‹set (effect_of op); and,
  \item terms' v = s v if no term(v, a') exist in term‹set (effect_of op).
\end{itemize} 
The second property is the case if the operator doesn't have an effect for a variable termv. ›

theorem execute_operator_sas_plus_effect:
  assumes "is_operator_applicable_in s op"
    and "(v, a)  set (effect_of op). 
      (v', a')  set (effect_of op). v  v'  a = a'"
  shows "(v, a)  set (effect_of op) 
       (s + op) v = Some a"
    and "(a. (v, a)  set (effect_of op)) 
       (s + op) v = s v"
proof -
  show "(v, a)  set (effect_of op) 
     (s + op) v = Some a" 
    using execute_operator_sas_plus_effect_i[OF assms(1, 2)]
    by blast
next 
  show "(a. (v, a)  set (effect_of op)) 
     (s + op) v = s v" 
    using execute_operator_sas_plus_effect_ii[OF assms(1)]
    by blast
qed

end


subsection "Parallel Execution Semantics"

― ‹ Define a type synonym for \emph{SAS+ parallel plans} and add a definition lifting SAS+
operator applicability to parallel plans. ›

type_synonym ('variable, 'domain) sas_plus_parallel_plan 
  = "('variable, 'domain) sas_plus_operator list list" 
    
definition are_all_operators_applicable_in
  :: "('variable, 'domain) state 
     ('variable, 'domain) sas_plus_operator list
     bool"
  where "are_all_operators_applicable_in s ops 
     list_all (is_operator_applicable_in s) ops"

definition are_operator_effects_consistent
  :: "('variable, 'domain) sas_plus_operator
     ('variable, 'domain) sas_plus_operator
     bool"
  where "are_operator_effects_consistent op op' 
     let 
        effect = effect_of op
        ; effect' = effect_of op'
      in list_all (λ(v, a). list_all (λ(v', a'). v  v'  a = a') effect') effect"

definition are_all_operator_effects_consistent
  :: "('variable, 'domain) sas_plus_operator list
     bool"
  where "are_all_operator_effects_consistent ops 
     list_all (λop. list_all (are_operator_effects_consistent op) ops) ops"   

definition execute_parallel_operator_sas_plus
  :: "('variable, 'domain) state 
     ('variable, 'domain) sas_plus_operator list 
     ('variable, 'domain) state"
  where "execute_parallel_operator_sas_plus s ops 
     foldl (++) s (map (map_of  effect_of) ops)" 

text ‹ We now define parallel execution and parallel traces for SAS+ by lifting the tests for 
applicability and effect consistency to parallel SAS+ operators. The definitions are again very
similar to their STRIPS analogs (definitions \ref{isadef:parallel-plan-execution-strips} and 
\ref{isadef:parallel-plan-trace-strips}). ›

fun execute_parallel_plan_sas_plus
  :: "('variable, 'domain) state 
     ('variable, 'domain) sas_plus_parallel_plan
     ('variable, 'domain) state" 
  where "execute_parallel_plan_sas_plus s [] = s"
  | "execute_parallel_plan_sas_plus s (ops # opss) = (if 
      are_all_operators_applicable_in s ops 
       are_all_operator_effects_consistent ops
    then execute_parallel_plan_sas_plus 
      (execute_parallel_operator_sas_plus s ops) opss
    else s)"

fun trace_parallel_plan_sas_plus
  :: "('variable, 'domain) state  
     ('variable, 'domain) sas_plus_parallel_plan 
     ('variable, 'domain) state list"
  where "trace_parallel_plan_sas_plus s [] = [s]"
  | "trace_parallel_plan_sas_plus s (ops # opss) = s # (if 
      are_all_operators_applicable_in s ops 
       are_all_operator_effects_consistent ops
    then trace_parallel_plan_sas_plus 
      (execute_parallel_operator_sas_plus s ops) opss
    else [])"

text ‹ A plan termψ is a solution for a SAS+ problem termΨ if 
\begin{enumerate}
  \item starting from the initial state termΨ, SAS+ parallel plan execution 
    reaches a state which satisfies the described goal state term‹sas_plus_problem.goal_of Ψ; and,
  \item all parallel operators termops in the plan termψ only consist of operators that
    are specified in the problem description.
\end{enumerate} ›
definition is_parallel_solution_for_problem 
  :: "('variable, 'domain) sas_plus_problem 
     ('variable, 'domain) sas_plus_parallel_plan 
     bool"
  where "is_parallel_solution_for_problem Ψ ψ 
     let 
        G = sas_plus_problem.goal_of Ψ
        ; I = sas_plus_problem.initial_of Ψ
        ; Ops = sas_plus_problem.operators_of Ψ
      in G m execute_parallel_plan_sas_plus I ψ
       list_all (λops. list_all (λop. ListMem op Ops) ops) ψ" 

context 
begin

lemma execute_parallel_operator_sas_plus_cons[simp]:
  "execute_parallel_operator_sas_plus s (op # ops)
    = execute_parallel_operator_sas_plus (s ++  map_of (effect_of op)) ops" 
  unfolding execute_parallel_operator_sas_plus_def
  by simp

text ‹The following lemmas show the properties of SAS+ parallel plan execution traces. 
The results are analogous to those for STRIPS. So, let termτ  trace_parallel_plan_sas_plus I ψ 
be a trace of a parallel SAS+ plan termψ with initial state termI, then
\begin{itemize}
  \item the head of the trace termτ ! 0 is the initial state of the 
problem (lemma \ref{isathm:head-parallel-plan-trace-sas-plus}); moreover,
  \item for all but the last element of the trace---i.e. elements with index 
termk < length τ - 1---the parallel operator termπ ! k is executable (lemma 
\ref{isathm:parallel-plan-trace-operator-execution-conditions-sas-plus}); and 
finally, 
  \item for all termk < length τ, the parallel execution of the plan prefix term‹take k ψ with 
initial state termI equals the termk-th element of the trace termτ ! k (lemma 
\ref{isathm:parallel-trace-plan-prefixes-sas-plus}).
\end{itemize} ›

(* TODO? Make invisible? *)
lemma trace_parallel_plan_sas_plus_head_is_initial_state: 
  "trace_parallel_plan_sas_plus I ψ ! 0 = I"
proof (cases ψ)
  case (Cons a list)
  then show ?thesis 
    by (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a"; 
        simp+)
qed simp

lemma trace_parallel_plan_sas_plus_length_gt_one_if:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ) - 1"  
  shows "1 < length (trace_parallel_plan_sas_plus I ψ)" 
  using assms
  by linarith
    
lemma length_trace_parallel_plan_sas_plus_lte_length_plan_plus_one:
  shows "length (trace_parallel_plan_sas_plus I ψ)  length ψ + 1" 
proof (induction ψ arbitrary: I)
  case (Cons a ψ)
  then show ?case 
    proof (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a")
      case True
      let ?I' = "execute_parallel_operator_sas_plus I a" 
      {
        have "trace_parallel_plan_sas_plus I (a # ψ) = I # trace_parallel_plan_sas_plus ?I' ψ" 
          using True
          by auto
        then have "length (trace_parallel_plan_sas_plus I (a # ψ)) 
          = length (trace_parallel_plan_sas_plus ?I' ψ) + 1"
          by simp
        moreover have "length (trace_parallel_plan_sas_plus ?I' ψ)  length ψ + 1"
          using Cons.IH[of ?I']
          by blast
        ultimately have "length (trace_parallel_plan_sas_plus I (a # ψ))  length (a # ψ) + 1"
          by simp
      }
      thus ?thesis
        by blast
    qed auto
qed simp
    
lemma plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ) - 1" 
  obtains ops ψ' where "ψ = ops # ψ'" 
proof -
  let  = "trace_parallel_plan_sas_plus I ψ"
  have "length   length ψ + 1" 
    using length_trace_parallel_plan_sas_plus_lte_length_plan_plus_one
    by fast
  then have "0 < length ψ"
    using trace_parallel_plan_sas_plus_length_gt_one_if[OF assms]
    by fastforce
  then obtain k' where "length ψ = Suc k'"
    using gr0_implies_Suc
    by meson
  thus ?thesis using that  
    using length_Suc_conv[of ψ k']
    by blast
qed

lemma trace_parallel_plan_sas_plus_step_implies_operator_execution_condition_holds:
  assumes "k < length (trace_parallel_plan_sas_plus I π) - 1"
  shows "are_all_operators_applicable_in (trace_parallel_plan_sas_plus I π ! k) (π ! k)
       are_all_operator_effects_consistent (π ! k)"
using assms 
proof  (induction "π" arbitrary: I k)
  ― ‹ NOTE Base case yields contradiction with assumption and can be left to automation. ›
  case (Cons a π)
  then show ?case 
    proof (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a")
      case True
      have trace_parallel_plan_sas_plus_cons: "trace_parallel_plan_sas_plus I (a # π) 
        = I # trace_parallel_plan_sas_plus (execute_parallel_operator_sas_plus I a) π"
        using True
        by simp  
      then show ?thesis 
      proof (cases "k")
        case 0
        have "trace_parallel_plan_sas_plus I (a # π) ! 0 = I" 
          using trace_parallel_plan_sas_plus_cons
          by simp
        moreover have "(a # π) ! 0 = a"
          by simp
        ultimately show ?thesis 
          using True 0
          by presburger
      next
        case (Suc k')
        have "trace_parallel_plan_sas_plus I (a # π) ! Suc k' 
          = trace_parallel_plan_sas_plus (execute_parallel_operator_sas_plus I a) π ! k'" 
          using trace_parallel_plan_sas_plus_cons
          by simp
        moreover have "(a # π) ! Suc k' = π ! k'"
          by simp
        moreover {
          let ?I' = "execute_parallel_operator_sas_plus I a"
          have "length (trace_parallel_plan_sas_plus I (a # π)) 
            = 1 + length (trace_parallel_plan_sas_plus ?I' π)" 
            using trace_parallel_plan_sas_plus_cons 
            by auto
          then have "k' < length (trace_parallel_plan_sas_plus ?I' π) - 1" 
            using Cons.prems Suc
            unfolding Suc_eq_plus1
            by fastforce
          hence "are_all_operators_applicable_in
            (trace_parallel_plan_sas_plus (execute_parallel_operator_sas_plus I a) π ! k')
            (π ! k') 
           are_all_operator_effects_consistent (π ! k')"
            using Cons.IH[of k' "execute_parallel_operator_sas_plus I a"] Cons.prems Suc trace_parallel_plan_sas_plus_cons
            by simp
        }
        ultimately show ?thesis 
          using Suc
          by argo
      qed 
    next
      case False
      then have "trace_parallel_plan_sas_plus I (a # π) = [I]"
        by force
      then have "length (trace_parallel_plan_sas_plus I (a # π)) - 1 = 0" 
        by simp
      ― ‹ NOTE Thesis follows from contradiction with assumption. ›
      then show ?thesis 
        using Cons.prems
        by force 
    qed
qed auto

lemma trace_parallel_plan_sas_plus_prefix:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ)"
  shows "trace_parallel_plan_sas_plus I ψ ! k = execute_parallel_plan_sas_plus I (take k ψ)" 
  using assms
proof  (induction ψ arbitrary: I k)
  case (Cons a ψ)
  then show ?case 
    proof (cases "are_all_operators_applicable_in I a  are_all_operator_effects_consistent a")
      case True
      let  = "trace_parallel_plan_sas_plus I (a # ψ)"
        and ?I' = "execute_parallel_operator_sas_plus I a" 
      have σ_equals: " = I # trace_parallel_plan_sas_plus ?I' ψ" 
        using True
        by auto
      then show ?thesis 
        proof (cases "k = 0")
          case False
          obtain k' where k_is_suc_of_k': "k = Suc k'" 
            using not0_implies_Suc[OF False]
            by blast
          then have "execute_parallel_plan_sas_plus I (take k (a # ψ))
            = execute_parallel_plan_sas_plus ?I' (take k' ψ)" 
            using True
            by simp
          moreover have "trace_parallel_plan_sas_plus I (a # ψ) ! k 
            = trace_parallel_plan_sas_plus ?I' ψ ! k'" 
            using σ_equals k_is_suc_of_k'
            by simp
          moreover {
            have "k' < length (trace_parallel_plan_sas_plus ?I' ψ)"
              using Cons.prems σ_equals k_is_suc_of_k'
              by force
            hence "trace_parallel_plan_sas_plus ?I' ψ ! k' 
              = execute_parallel_plan_sas_plus ?I' (take k' ψ)" 
              using Cons.IH[of k' ?I']
              by blast
          }
          ultimately show ?thesis
            by presburger
        qed simp
    next
      case operator_precondition_violated: False
      then show ?thesis 
      proof (cases "k = 0")
        case False
        then have "trace_parallel_plan_sas_plus I (a # ψ) = [I]"
          using operator_precondition_violated
          by force
        moreover have "execute_parallel_plan_sas_plus I (take k (a # ψ)) = I" 
          using Cons.prems operator_precondition_violated 
          by force
        ultimately show ?thesis 
          using Cons.prems nth_Cons_0
          by auto
      qed simp
    qed
qed simp

lemma trace_parallel_plan_sas_plus_step_effect_is:
  assumes "k < length (trace_parallel_plan_sas_plus I ψ) - 1"
  shows "trace_parallel_plan_sas_plus I ψ ! Suc k 
    = execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! k) (ψ ! k)" 
proof -
  let  = "trace_parallel_plan_sas_plus I ψ"
  let k = " ! k"
    and k' = " ! Suc k"
  ― ‹ NOTE rewrite the goal using the subplan formulation to be able. This allows us to make the 
    initial state arbitrary. ›
  {
    have suc_k_lt_length_τ: "Suc k < length " 
      using assms 
      by linarith
    hence "k' = execute_parallel_plan_sas_plus I (take (Suc k) ψ)"
      using trace_parallel_plan_sas_plus_prefix[of "Suc k"]
      by blast
  } note rewrite_goal = this
  have "execute_parallel_plan_sas_plus I (take (Suc k) ψ) 
    = execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! k) (ψ ! k)" 
    using assms
    proof (induction k arbitrary: I ψ)
      case 0
      obtain ops ψ' where ψ_is: "ψ = ops # ψ'" 
        using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF "0.prems"] 
        by force
      {
        have "take (Suc 0) ψ  = [ψ ! 0]" 
          using ψ_is
          by simp
        hence "execute_parallel_plan_sas_plus I (take (Suc 0) ψ) 
          = execute_parallel_plan_sas_plus I [ψ ! 0]"
          by argo
      }
      moreover {
        have "trace_parallel_plan_sas_plus I ψ ! 0 = I" 
          using trace_parallel_plan_sas_plus_head_is_initial_state.
        moreover {
          have "are_all_operators_applicable_in I (ψ ! 0)" 
            and "are_all_operator_effects_consistent (ψ ! 0)" 
            using trace_parallel_plan_sas_plus_step_implies_operator_execution_condition_holds[OF
                "0.prems"] calculation 
            by argo+
          then have "execute_parallel_plan_sas_plus I [ψ ! 0] 
            = execute_parallel_operator_sas_plus I (ψ ! 0)"
            by simp
        }
        ultimately have "execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! 0) 
            (ψ ! 0)
          = execute_parallel_plan_sas_plus I [ψ ! 0]"
          by argo
      }
      ultimately show ?case 
        by argo
    next
      case (Suc k)
      obtain ops ψ' where ψ_is: "ψ = ops # ψ'" 
        using plan_is_at_least_singleton_plan_if_trace_has_at_least_two_elements[OF Suc.prems]
        by blast
      let ?I' = "execute_parallel_operator_sas_plus I ops"
      have "execute_parallel_plan_sas_plus I (take (Suc (Suc k)) ψ)
        = execute_parallel_plan_sas_plus ?I' (take (Suc k) ψ')" 
        using Suc.prems ψ_is
        by fastforce
      moreover {
        thm Suc.IH[of ]
        have "length (trace_parallel_plan_sas_plus I ψ)
          = 1 + length (trace_parallel_plan_sas_plus ?I' ψ')" 
          using ψ_is Suc.prems
          by fastforce
        moreover have "k < length (trace_parallel_plan_sas_plus ?I' ψ') - 1"
          using Suc.prems calculation
          by fastforce
        ultimately have "execute_parallel_plan_sas_plus ?I' (take (Suc k) ψ') =
          execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus ?I' ψ' ! k) 
          (ψ' ! k)"
          using Suc.IH[of ?I' ψ']
          by blast          
      }
      moreover have "execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus ?I' ψ' ! k) 
          (ψ' ! k)
        = execute_parallel_operator_sas_plus (trace_parallel_plan_sas_plus I ψ ! Suc k)
          (ψ ! Suc k)" 
        using Suc.prems ψ_is
        by auto
      ultimately show ?case
        by argo 
    qed 
  thus ?thesis 
    using rewrite_goal
    by argo
qed

text ‹ Finally, we obtain the result corresponding to lemma 
\ref{isathm:parallel-solution-trace-strips} in the SAS+ case: it is equivalent to say that parallel 
SAS+ execution reaches the problem's goal state and that the last element of the corresponding 
trace satisfies the goal state. ›
lemma  execute_parallel_plan_sas_plus_reaches_goal_iff_goal_is_last_element_of_trace:
  "G m execute_parallel_plan_sas_plus I ψ 
     G m last (trace_parallel_plan_sas_plus I ψ)" 
proof   -
  let  = "trace_parallel_plan_sas_plus I ψ" 
  show ?thesis 
  proof (rule iffI)
    assume "G m execute_parallel_plan_sas_plus I ψ"
    thus "G m last " 
      proof (induction ψ arbitrary: I)
        ― ‹ NOTE Base case follows from simplification. ›
        case (Cons ops ψ)
        show ?case
          proof (cases "are_all_operators_applicable_in I ops 
             are_all_operator_effects_consistent ops")
            case True
            let ?s = "execute_parallel_operator_sas_plus I ops"
            {
              have "G m execute_parallel_plan_sas_plus ?s ψ"
                using True Cons.prems
                by simp
              hence "G m last (trace_parallel_plan_sas_plus ?s ψ)" 
                using Cons.IH
                by auto
            }
            moreover {
              have "trace_parallel_plan_sas_plus I (ops # ψ) 
                = I # trace_parallel_plan_sas_plus ?s ψ" 
                using True 
                by simp
              moreover have "trace_parallel_plan_sas_plus ?s ψ  []" 
                using trace_parallel_plan_sas_plus.elims
                by blast 
              ultimately have "last (trace_parallel_plan_sas_plus I (ops # ψ)) 
                = last (trace_parallel_plan_sas_plus ?s ψ)" 
                using last_ConsR
                  by simp
            }
            ultimately show ?thesis 
              by argo
          next
            case False
            then have "G m I"
              using Cons.prems 
              by force
            thus ?thesis
              using False
              by force
          qed
      qed force
  next 
    assume "G m last "
    thus "G m execute_parallel_plan_sas_plus I ψ" 
      proof (induction ψ arbitrary: I)
        case (Cons ops ψ)
        thus ?case
          proof (cases "are_all_operators_applicable_in I ops
             are_all_operator_effects_consistent ops")
            case True
            let ?s = "execute_parallel_operator_sas_plus I ops"
            {
              have "trace_parallel_plan_sas_plus I (ops # ψ) 
                = I # trace_parallel_plan_sas_plus ?s ψ" 
                using True 
                by simp
              moreover have "trace_parallel_plan_sas_plus ?s ψ  []" 
                using trace_parallel_plan_sas_plus.elims
                by blast 
              ultimately have "last (trace_parallel_plan_sas_plus I (ops # ψ)) 
                = last (trace_parallel_plan_sas_plus ?s ψ)" 
                using last_ConsR
                by simp
              hence "G m execute_parallel_plan_sas_plus ?s ψ"
                using Cons.IH[of ?s] Cons.prems 
                by argo
            }
            moreover have "execute_parallel_plan_sas_plus I (ops # ψ) 
                = execute_parallel_plan_sas_plus ?s ψ" 
              using True
              by force
            ultimately show ?thesis 
              by argo
          next
            case False
            have "G m I"
              using Cons.prems False 
              by simp
            thus ?thesis
              using False
              by force
          qed
      qed simp
  qed
qed

lemma is_parallel_solution_for_problem_plan_operator_set:
  (* TODO refactor move + make visible? *)
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "is_parallel_solution_for_problem Ψ ψ" 
  shows "ops  set ψ. op  set ops. op  set ((Ψ)𝒪+)"
  using assms
  unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff operators_of_def 
  by presburger

end


subsection "Serializable Parallel Plans"

text ‹ Again we want to establish conditions for the serializability of plans. Let
termΨ be a SAS+ problem instance and let termψ be a serial solution. We obtain the following 
two important results, namely that
\begin{enumerate}
  \item the embedding term‹embed ψ of termψ is a parallel solution for termΨ 
(lemma \ref{isathm:serial-sas-plus-embedding}); and conversely that,
  \item a parallel solution to termΨ that has the form of an embedded serial plan can be 
concatenated to obtain a serial solution (lemma 
\ref{isathm:embedded-serial-solution-flattening-sas-plus}).
\end{enumerate} ›


context
begin

(* TODO refactor *)
lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_i:
  assumes "is_operator_applicable_in s op"
    "are_operator_effects_consistent op op" 
  shows "s + op = execute_parallel_operator_sas_plus s [op]"
proof -
  have "are_all_operators_applicable_in s [op]"
    unfolding are_all_operators_applicable_in_def 
       SAS_Plus_Representation.execute_operator_sas_plus_def
      is_operator_applicable_in_def SAS_Plus_Representation.is_operator_applicable_in_def
      list_all_iff  
    using assms(1) 
    by fastforce
  moreover have "are_all_operator_effects_consistent [op]"
    unfolding are_all_operator_effects_consistent_def list_all_iff
    using assms(2)
    by fastforce
  ultimately show ?thesis
    unfolding execute_parallel_operator_sas_plus_def execute_operator_sas_plus_def
    by simp
qed

lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_ii:
  fixes I :: "('variable, 'domain) state"
  assumes "op  set ψ. are_operator_effects_consistent op op"
    and "G m execute_serial_plan_sas_plus I ψ" 
  shows "G m execute_parallel_plan_sas_plus I (embed ψ)" 
  using assms
proof (induction ψ arbitrary: I)
  case (Cons op ψ)
  show ?case 
    proof (cases "are_all_operators_applicable_in I [op]")
      case True
      let ?J = "execute_operator_sas_plus I op" 
        let ?J' = "execute_parallel_operator_sas_plus I [op]" 
      have "SAS_Plus_Representation.is_operator_applicable_in I op"
        using True 
        unfolding are_all_operators_applicable_in_def list_all_iff
        by force
      moreover have "G m execute_serial_plan_sas_plus ?J ψ" 
        using Cons.prems(2) calculation(1) 
        by simp
      moreover have "are_all_operator_effects_consistent [op]" 
        unfolding are_all_operator_effects_consistent_def list_all_iff Let_def
        using Cons.prems(1)
        by simp
      moreover have "execute_parallel_plan_sas_plus I ([op] # embed ψ) 
        = execute_parallel_plan_sas_plus ?J' (embed ψ)"
        using True calculation(3) 
        by simp
      moreover {
        have "is_operator_applicable_in I op" 
          "are_operator_effects_consistent op op" 
          using True Cons.prems(1)
          unfolding are_all_operators_applicable_in_def 
            SAS_Plus_Representation.is_operator_applicable_in_def list_all_iff 
          by fastforce+
        hence "?J = ?J'" 
          using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_i
            calculation(1) 
          by blast
      }
      ultimately show ?thesis 
        using Cons.IH[of ?J] Cons.prems(1)
        by simp
    next
      case False
      moreover have "¬is_operator_applicable_in I op" 
        using calculation 
        unfolding are_all_operators_applicable_in_def 
          SAS_Plus_Representation.is_operator_applicable_in_def list_all_iff 
        by fastforce
      moreover have "G m I" 
        using Cons.prems(2) calculation(2)
        unfolding is_operator_applicable_in_def
        by simp
      moreover have "execute_parallel_plan_sas_plus I ([op] # embed ψ) = I" 
        using calculation(1)
        by fastforce
      ultimately show ?thesis
        by force
    qed
  qed simp

lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iii:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "is_serial_solution_for_problem Ψ ψ"
    and "op  set ψ"
  shows "are_operator_effects_consistent op op"
proof -
  have "op  set ((Ψ)𝒪+)"
    using assms(2) assms(3)
    unfolding is_serial_solution_for_problem_def Let_def list_all_iff ListMem_iff 
    by fastforce
  then have "is_valid_operator_sas_plus Ψ op" 
    using is_valid_problem_sas_plus_then(2) assms(1, 3) 
    by auto
  thus ?thesis
    unfolding are_operator_effects_consistent_def Let_def list_all_iff ListMem_iff
    using is_valid_operator_sas_plus_then(6)
    by fast
qed

lemma execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iv:
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "op  set ψ. op  set ((Ψ)𝒪+)"
  shows "ops  set (embed ψ). op  set ops. op  set ((Ψ)𝒪+)"
proof -
  let ?ψ' = "embed ψ"
  have nb: "set ?ψ' = { [op] | op. op  set ψ }" 
    by (induction ψ; force)
  {
    fix ops
    assume "ops  set ?ψ'"
    moreover obtain op where "ops = [op]" and "op  set ((Ψ)𝒪+)"
      using assms(1) nb calculation 
      by blast
    ultimately have "op  set ops. op  set ((Ψ)𝒪+)"
      by fastforce
  }
  thus ?thesis..
qed

theorem execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus:
  assumes "is_valid_problem_sas_plus Ψ" 
    and "is_serial_solution_for_problem Ψ ψ" 
  shows "is_parallel_solution_for_problem Ψ (embed ψ)" 
proof  -
  let ?ops = "sas_plus_problem.operators_of Ψ" 
    and ?ψ' = "embed ψ" 
  {
    thm execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_ii[OF]
    have "(Ψ)G+ m execute_serial_plan_sas_plus ((Ψ)I+) ψ"
      using assms(2) 
      unfolding is_serial_solution_for_problem_def Let_def
      by simp
    moreover have "op  set ψ. are_operator_effects_consistent op op" 
      using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iii[OF assms]..
    ultimately have "(Ψ)G+ m execute_parallel_plan_sas_plus ((Ψ)I+) ?ψ'" 
      using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_ii
      by blast
  }
  moreover {
    have "op  set ψ. op  set ((Ψ)𝒪+)"
      using assms(2) 
      unfolding is_serial_solution_for_problem_def Let_def list_all_iff ListMem_iff
      by fastforce
    hence "ops  set ?ψ'. op  set ops. op  set ((Ψ)𝒪+)" 
      using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_iv
      by blast
  }
  ultimately show ?thesis
    unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff Let_def goal_of_def 
      initial_of_def
    by fastforce
qed

lemma flattening_lemma_i:
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "ops  set π. op  set ops. op  set ((Ψ)𝒪+)"
  shows "op  set (concat π). op  set ((Ψ)𝒪+)"
proof -
  {
    fix op
    assume "op  set (concat π)" 
    moreover have "op  (ops  set π. set ops)" 
      using calculation
      unfolding set_concat.
    then obtain ops where "ops  set π" and "op  set ops" 
      using UN_iff
      by blast
    ultimately have "op  set ((Ψ)𝒪+)" 
      using assms
      by blast
  }
  thus ?thesis..
qed

lemma flattening_lemma_ii:
  fixes I :: "('variable, 'domain) state"
  assumes "ops  set ψ. op. ops = [op]  is_valid_operator_sas_plus Ψ op " 
    and "G m execute_parallel_plan_sas_plus I ψ" 
  shows "G m execute_serial_plan_sas_plus I (concat ψ)"
proof -
  show ?thesis 
    using assms
    proof (induction ψ arbitrary: I)
      case (Cons ops ψ)
      obtain op where ops_is: "ops = [op]" and is_valid_op: "is_valid_operator_sas_plus Ψ op" 
        using Cons.prems(1)
        by auto
      then show ?case 
        proof (cases "are_all_operators_applicable_in I ops")
          case True
          let ?J = "execute_parallel_operator_sas_plus I [op]" 
            and ?J' = "execute_operator_sas_plus I op" 
          have nb1: "is_operator_applicable_in I op" 
            using True ops_is
            unfolding are_all_operators_applicable_in_def is_operator_applicable_in_def 
              list_all_iff 
            by force
          have nb2: "are_operator_effects_consistent op op" 
            unfolding are_operator_effects_consistent_def list_all_iff Let_def 
            using is_valid_operator_sas_plus_then(6)[OF is_valid_op]
            by blast
          have "are_all_operator_effects_consistent ops" 
            using ops_is 
            unfolding are_all_operator_effects_consistent_def list_all_iff
            using nb2
            by force
          moreover have "G m execute_parallel_plan_sas_plus ?J ψ"
            using Cons.prems(2) True calculation ops_is
            by fastforce
          moreover have "execute_serial_plan_sas_plus I (concat (ops # ψ)) 
              = execute_serial_plan_sas_plus ?J' (concat ψ)"
              using ops_is nb1 is_operator_applicable_in_def
              by simp
          moreover have "?J = ?J'" 
            using execute_serial_plan_sas_plus_is_execute_parallel_plan_sas_plus_i[OF nb1 nb2]
            by simp
          ultimately show ?thesis
            using Cons.IH[of ?J] Cons.prems(1)
            by force
        next
          case False
          moreover have "G m I" 
            using Cons.prems(2) calculation
            by fastforce
          moreover {
            have "¬is_operator_applicable_in I op" 
              using False ops_is
              unfolding are_all_operators_applicable_in_def 
                is_operator_applicable_in_def list_all_iff
              by force
            moreover have "execute_serial_plan_sas_plus I (concat (ops # ψ)) 
              = execute_serial_plan_sas_plus I (op # concat ψ)" 
              using ops_is 
              by force
            ultimately have "execute_serial_plan_sas_plus I (concat (ops # ψ)) = I"
              using False 
              unfolding is_operator_applicable_in_def
              by fastforce
          }
          ultimately show ?thesis
            by argo
        qed  
    qed force
qed

lemma flattening_lemma:
  assumes "is_valid_problem_sas_plus Ψ"
    and "ops  set ψ. op. ops = [op]" 
    and "is_parallel_solution_for_problem Ψ ψ"
  shows "is_serial_solution_for_problem Ψ (concat ψ)"
proof  -
  let ?ψ' = "concat ψ" 
  {
    have "ops  set ψ. op  set ops. op  set ((Ψ)𝒪+)" 
      using assms(3)
      unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff
      by force
    hence "op  set ?ψ'. op  set ((Ψ)𝒪+)"
      using flattening_lemma_i
      by blast
  }
  moreover {
    {
      fix ops
      assume "ops  set ψ" 
      moreover obtain op where "ops = [op]" 
        using assms(2) calculation
        by blast
      moreover have "op  set ((Ψ)𝒪+)" 
        using assms(3) calculation
        unfolding is_parallel_solution_for_problem_def list_all_iff ListMem_iff 
        by force
      moreover have "is_valid_operator_sas_plus Ψ op" 
        using assms(1) calculation(3)
        unfolding is_valid_problem_sas_plus_def Let_def list_all_iff 
          ListMem_iff
        by simp
      ultimately have "op. ops = [op]  is_valid_operator_sas_plus Ψ op"
        by blast
    }
    moreover have "(Ψ)G+ m execute_parallel_plan_sas_plus ((Ψ)I+) ψ" 
      using assms(3) 
      unfolding is_parallel_solution_for_problem_def
      by fastforce
    ultimately have "(Ψ)G+ m execute_serial_plan_sas_plus ((Ψ)I+) ?ψ'" 
      using flattening_lemma_ii
      by blast
  }
  ultimately show "is_serial_solution_for_problem Ψ ?ψ'" 
    unfolding is_serial_solution_for_problem_def list_all_iff ListMem_iff
    by fastforce
qed
end

subsection "Auxiliary lemmata on SAS+"


context
begin

― ‹ Relate the locale definition range_of› with its corresponding implementation for valid 
operators and given an effect (v, a)›. ›
lemma is_valid_operator_sas_plus_then_range_of_sas_plus_op_is_set_range_of_op:
  assumes "is_valid_operator_sas_plus Ψ op"
    and "(v, a)  set (precondition_of op)  (v, a)  set (effect_of op)"
  shows "(+ Ψ v) = set (the (sas_plus_problem.range_of Ψ v))" 
proof -
  consider (A) "(v, a)  set (precondition_of op)"
    | (B)  "(v, a)  set (effect_of op)"
    using assms(2)..
  thus ?thesis 
    proof (cases)
      case A
      then have "(+ Ψ v)  {}" and "a  + Ψ v" 
        using assms 
        unfolding range_of_def
        using is_valid_operator_sas_plus_then(2)
        by fast+
      thus ?thesis
        unfolding range_of'_def option.case_eq_if
        by auto
    next
      case B
      then have "(+ Ψ v)  {}" and "a  + Ψ v" 
        using assms 
        unfolding range_of_def
        using is_valid_operator_sas_plus_then(4)
        by fast+
      thus ?thesis
        unfolding range_of'_def option.case_eq_if
        by auto
    qed  
qed 

lemma set_the_range_of_is_range_of_sas_plus_if:
  fixes Ψ :: "('v, 'd) sas_plus_problem"
  assumes "is_valid_problem_sas_plus Ψ"
    "v  set ((Ψ)𝒱+)"
  shows "set (the (sas_plus_problem.range_of Ψ v)) = + Ψ v"
proof-
  have "v  set((Ψ)𝒱+)" 
    using assms(2)
    unfolding variables_of_def.
  moreover have "(+ Ψ v)  {}"
    using assms(1) calculation is_valid_problem_sas_plus_then(1)
    by blast
  moreover have "sas_plus_problem.range_of Ψ v  None" 
    and "sas_plus_problem.range_of Ψ v  Some []"
    using calculation(2) range_of_not_empty
    unfolding range_of_def 
    by fast+
  ultimately show ?thesis
    unfolding option.case_eq_if range_of'_def
    by force
qed

lemma sublocale_sas_plus_finite_domain_representation_ii:
  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"
  using is_valid_problem_sas_plus_then[OF assms]
  by auto

end

end

Theory SAS_Plus_STRIPS

(*
  Author: Mohammad Abdulaziz, Fred Kurz
*)
theory SAS_Plus_STRIPS
  imports "STRIPS_Semantics" "SAS_Plus_Semantics" 
    "Map_Supplement"
begin

section "SAS+/STRIPS Equivalence"

text ‹ The following part is concerned with showing the equivalent expressiveness of SAS+ and
STRIPS as discussed in \autoref{sub:equivalence-sas-plus-strips}. ›

subsection "Translation of SAS+ Problems to STRIPS Problems"

definition possible_assignments_for 
  :: "('variable, 'domain) sas_plus_problem  'variable  ('variable × 'domain) list" 
  where "possible_assignments_for Ψ v  [(v, a). a  the (range_of Ψ v)]"

definition all_possible_assignments_for
  :: "('variable, 'domain) sas_plus_problem  ('variable × 'domain) list"
  where "all_possible_assignments_for Ψ 
     concat [possible_assignments_for Ψ v. v  variables_of Ψ]" 

definition state_to_strips_state
  :: "('variable, 'domain) sas_plus_problem 
     ('variable, 'domain) state 
     ('variable, 'domain) assignment strips_state" 
  ("φS _ _" 99)
  where "state_to_strips_state Ψ s 
     let defined = filter (λv. s v  None) (variables_of Ψ) in
      map_of (map (λ(v, a). ((v, a), the (s v) = a)) 
        (concat [possible_assignments_for Ψ v. v  defined]))"

definition sasp_op_to_strips
  :: "('variable, 'domain) sas_plus_problem
     ('variable, 'domain) sas_plus_operator
     ('variable, 'domain) assignment strips_operator" 
  ("φO _ _" 99)
  where "sasp_op_to_strips Ψ op  let
      pre = precondition_of op
      ; add = effect_of op
      ; delete = [(v, a'). (v, a)  effect_of op, a'  filter ((≠) a) (the (range_of Ψ v))]
    in STRIPS_Representation.operator_for pre add delete"

definition sas_plus_problem_to_strips_problem
  :: "('variable, 'domain) sas_plus_problem  ('variable, 'domain) assignment strips_problem" 
  ("φ _ " 99)
  where "sas_plus_problem_to_strips_problem Ψ  let 
      vs = [as. v  variables_of Ψ, as  (possible_assignments_for Ψ) v]
      ; ops = map (sasp_op_to_strips Ψ) (operators_of Ψ)
      ; I = state_to_strips_state Ψ (initial_of Ψ)
      ; G = state_to_strips_state Ψ (goal_of Ψ)
    in STRIPS_Representation.problem_for vs ops I G"

definition sas_plus_parallel_plan_to_strips_parallel_plan
  :: "('variable, 'domain) sas_plus_problem
     ('variable, 'domain) sas_plus_parallel_plan
     ('variable × 'domain) strips_parallel_plan" 
  ("φP _ _" 99)
  where "sas_plus_parallel_plan_to_strips_parallel_plan Ψ ψ
     [[sasp_op_to_strips Ψ op. op  ops]. ops  ψ]"

(* TODO first argument should be ('variable, 'domain) strips_problem *)
definition strips_state_to_state
  :: "('variable, 'domain) sas_plus_problem
     ('variable, 'domain) assignment strips_state
     ('variable, 'domain) state" 
  ("φS¯ _ _" 99)
  where "strips_state_to_state Ψ s 
     map_of (filter (λ(v, a). s (v, a) = Some True) (all_possible_assignments_for Ψ))"

(* TODO remove problem argument *)
definition strips_op_to_sasp 
  :: "('variable, 'domain) sas_plus_problem 
     ('variable × 'domain) strips_operator
     ('variable, 'domain) sas_plus_operator"
  ("φO¯ _ _" 99)
  where "strips_op_to_sasp Ψ op 
     let 
        precondition = strips_operator.precondition_of op
        ; effect = strips_operator.add_effects_of op 
      in  precondition_of = precondition, effect_of = effect " 

(* TODO ‹strips_parallel_plan_to_sas_plus_parallel_plan ↝ φ_P¯› and 
‹strips_op_to_sasp ↝ φ_O¯› *)
definition strips_parallel_plan_to_sas_plus_parallel_plan
  :: "('variable, 'domain) sas_plus_problem
     ('variable × 'domain) strips_parallel_plan
     ('variable, 'domain) sas_plus_parallel_plan" 
  ("φP¯ _ _" 99)
  where "strips_parallel_plan_to_sas_plus_parallel_plan Π π
     [[strips_op_to_sasp Π op. op  ops]. ops  π]"

text ‹ To set up the equivalence proof context, we declare a common locale 
\isaname{sas_plus_strips_equivalence} for both the STRIPS and SAS+ formalisms and make it a 
sublocale of both locale \isaname{strips} as well as \isaname{sas_plus}.
The declaration itself is omitted for brevity since it basically just joins locales 
\isaname{sas_plus} and \isaname{strips} while renaming the locale parameter to avoid name clashes.
The sublocale proofs are shown below.
\footnote{We append a suffix identifying the respective formalism to the the parameter names 
passed to the parameter names in the locale. This is necessary to avoid ambiguous names in the 
sublocale declarations. For example, without addition of suffixes the type for initial_of› is 
ambiguous and will therefore not be bound to either strips_problem.initial_of› or 
sas_plus_problem.initial_of›. 
Isabelle in fact considers it to be a a free variable in this case. We also qualify the parent 
locales in the sublocale declarations by adding \texttt{strips:} and \texttt{sas\_plus:} before 
the respective parent locale identifiers. } ›

definition "range_of_strips Π x  { True, False }"

context
begin

― ‹ Set-up simp rules. ›
lemma[simp]: 
  "(φ Ψ) = (let 
      vs = [as. v  variables_of Ψ, as  (possible_assignments_for Ψ) v]
      ; ops = map (sasp_op_to_strips Ψ) (operators_of Ψ)
      ; I = state_to_strips_state Ψ (initial_of Ψ)
      ; G = state_to_strips_state Ψ (goal_of Ψ)
    in STRIPS_Representation.problem_for vs ops I G)"
  and "(φS Ψ s)
    = (let defined = filter (λv. s v  None) (variables_of Ψ) in
      map_of (map (λ(v, a). ((v, a), the (s v) = a)) 
        (concat [possible_assignments_for Ψ v. v  defined])))"
  and "(φO Ψ op)
    = (let
      pre = precondition_of op
      ; add = effect_of op
      ; delete = [(v, a'). (v, a)  effect_of op, a'  filter ((≠) a) (the (range_of Ψ v))]
    in STRIPS_Representation.operator_for pre add delete)" 
  and "(φP Ψ ψ) = [[φO Ψ op. op  ops]. ops  ψ]"
  and "(φS¯ Ψ s')= map_of (filter (λ(v, a). s' (v, a) = Some True) 
    (all_possible_assignments_for Ψ))" 
  and "(φO¯ Ψ op') = (let 
        precondition = strips_operator.precondition_of op'
        ; effect = strips_operator.add_effects_of op' 
      in  precondition_of = precondition, effect_of = effect )" 
  and "(φP¯ Ψ π) = [[φO¯ Ψ op. op  ops]. ops  π]"
  unfolding
    SAS_Plus_STRIPS.sas_plus_problem_to_strips_problem_def
    sas_plus_problem_to_strips_problem_def
    SAS_Plus_STRIPS.state_to_strips_state_def
    state_to_strips_state_def
    SAS_Plus_STRIPS.sasp_op_to_strips_def
    sasp_op_to_strips_def
    SAS_Plus_STRIPS.sas_plus_parallel_plan_to_strips_parallel_plan_def
    sas_plus_parallel_plan_to_strips_parallel_plan_def
    SAS_Plus_STRIPS.strips_state_to_state_def
    strips_state_to_state_def 
    SAS_Plus_STRIPS.strips_op_to_sasp_def
    strips_op_to_sasp_def 
    SAS_Plus_STRIPS.strips_parallel_plan_to_sas_plus_parallel_plan_def
    strips_parallel_plan_to_sas_plus_parallel_plan_def 
  by blast+

lemmas [simp] = range_of'_def

lemma is_valid_problem_sas_plus_dom_sas_plus_problem_range_of:
  assumes "is_valid_problem_sas_plus Ψ" 
  shows "v  set ((Ψ)𝒱+). v  dom (sas_plus_problem.range_of Ψ)"
  using assms(1) is_valid_problem_sas_plus_then(1)
  unfolding is_valid_problem_sas_plus_def
  by (meson domIff list.pred_set)

lemma possible_assignments_for_set_is:
  assumes "v  dom (sas_plus_problem.range_of Ψ)"
  shows "set (possible_assignments_for Ψ v) 
    = { (v, a) | a. a  + Ψ v }" 
proof -
  have "sas_plus_problem.range_of Ψ v  None"
    using assms(1) 
    by auto
  thus  ?thesis 
    unfolding possible_assignments_for_def
    by fastforce
qed

lemma all_possible_assignments_for_set_is:
  assumes "v  set ((Ψ)𝒱+). range_of Ψ v  None" 
  shows "set (all_possible_assignments_for Ψ)
    = (v  set ((Ψ)𝒱+). { (v, a) | a. a  + Ψ v })" 
proof -
  let ?vs = "variables_of Ψ"
  have "set (all_possible_assignments_for Ψ) = 
    ((set ` (λv. map (λ(v, a). (v, a)) (possible_assignments_for Ψ v)) ` set ?vs))"
    unfolding all_possible_assignments_for_def set_concat
    using set_map 
    by auto
  also have " = (((λv. set (possible_assignments_for Ψ v)) ` set ?vs))"
    using image_comp set_map
    by simp
  (* TODO slow *)
  also have " = (((λv. { (v, a) | a. a  + Ψ v }) ` set ?vs))"
    using possible_assignments_for_set_is assms 
    by fastforce
  finally show ?thesis
    by force
qed

lemma state_to_strips_state_dom_is_i[simp]:
  assumes "v  set ((Ψ)𝒱+). v  dom (sas_plus_problem.range_of Ψ)"
  shows "set (concat 
      [possible_assignments_for Ψ v. v  filter (λv. s v  None) (variables_of Ψ)])
    = (v  { v | v. v  set ((Ψ)𝒱+)  s v  None }. 
      { (v, a) | a. a  + Ψ v })" 
proof -
  let ?vs = "variables_of Ψ"
  let ?defined = "filter (λv. s v  None) ?vs"
  let ?l = "concat [possible_assignments_for Ψ v. v  ?defined]"
  have nb: "set ?defined = { v | v. v  set ((Ψ)𝒱+)  s v  None }" 
    unfolding set_filter
    by force
  have "set ?l = (set ` set (map (possible_assignments_for Ψ) ?defined ))" 
    unfolding set_concat image_Union
    by blast
  also have " = (set ` (possible_assignments_for Ψ) ` set ?defined)" 
    unfolding set_map
    by blast
  also have " = (v  set ?defined. set (possible_assignments_for Ψ v))"
    by blast
  also have " = (v  { v | v. v  set ((Ψ)𝒱+)  s v  None }.
    set (possible_assignments_for Ψ v))"
    using nb 
    by argo
  finally show ?thesis
    using possible_assignments_for_set_is 
      is_valid_problem_sas_plus_dom_sas_plus_problem_range_of assms(1)
    by fastforce
qed

lemma state_to_strips_state_dom_is:
  ― ‹ NOTE A transformed state is defined on all possible assignments for all variables defined 
in the original state. ›
  assumes "is_valid_problem_sas_plus Ψ"
  shows "dom (φS Ψ s) 
    = (v  { v | v. v  set ((Ψ)𝒱+)  s v  None }. 
      { (v, a) | a. a  + Ψ v })"
proof -
  let ?vs = "variables_of Ψ"
  let ?l = "concat [possible_assignments_for Ψ v. v  filter (λv. s v  None) ?vs]"
  have nb: "v  set ((Ψ)𝒱+). v  dom (sas_plus_problem.range_of Ψ)"
    using is_valid_problem_sas_plus_dom_sas_plus_problem_range_of assms(1)
    by fastforce
  have "dom (φS Ψ s) = fst ` set (map (λ(v, a). ((v, a), the (s v) = a)) ?l)" 
    unfolding state_to_strips_state_def 
      SAS_Plus_STRIPS.state_to_strips_state_def 
    using dom_map_of_conv_image_fst[of "map (λ(v, a). ((v, a), the (s v) = a)) ?l"]
    by presburger
  also have " = fst ` (λ(v, a). ((v, a), the (s v) = a)) ` set ?l" 
    unfolding set_map
    by blast
  also have " = (λ(v, a). fst  ((v, a), the (s v) = a)) ` set ?l"
    unfolding image_comp[of fst "λ(v, a). ((v, a), the (s v) = a)"] comp_apply[of 
        fst "λ(v, a). ((v, a), the (s v) = a)"] prod.case_distrib
    by blast
  finally show ?thesis
    unfolding state_to_strips_state_dom_is_i[OF nb]
    by force
qed

corollary state_to_strips_state_dom_element_iff:
  assumes "is_valid_problem_sas_plus Ψ"
  shows "(v, a)  dom (φS Ψ s)  v  set ((Ψ)𝒱+)
     s v  None
     a  + Ψ v"
proof -
  let ?vs = "variables_of Ψ"
    and ?s' = "φS Ψ s"
  show ?thesis 
    proof (rule iffI)
      assume "(v, a)  dom (φS Ψ s)" 
      then have "v  { v | v. v  set ((Ψ)𝒱+)  s v  None }"
          and "a  + Ψ v"
        unfolding state_to_strips_state_dom_is[OF assms(1)]
        by force+
      moreover have "v  set ?vs" and "s v  None" 
        using calculation(1) 
        by fastforce+
      ultimately show 
        "v  set ((Ψ)𝒱+)  s v  None  a  + Ψ v"
        by force
    next 
      assume "