# 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 ∨ (∃m∈set 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 = [(v⇩_{a}, True). v⇩_{a}← add_effects_of op] @ [(v⇩_{d}, False). v⇩_{d}← 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 \<^term>‹s› 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 as⇩_{1}as⇩_{2}where "as = as⇩_{1}@ as⇩_{2}" and "as⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and "as⇩_{2}= 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 as⇩_{1}as⇩_{2}where a1: "as = as⇩_{1}@ as⇩_{2}" and a2: "as⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and a3: "as⇩_{2}= 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 as⇩_{1}as⇩_{2}where a1: "as = as⇩_{1}@ as⇩_{2}" and a2: "as⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and a3: "as⇩_{2}= 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 es⇩_{1}es⇩_{2}where "e = (es⇩_{1}@ es⇩_{2})" and "es⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and "es⇩_{2}= map (λv. (v, False)) (delete_effects_of op)" proof - obtain es⇩_{1}es⇩_{2}where a: "e = (es⇩_{1}@ es⇩_{2})" and b: "es⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and c: "es⇩_{2}= 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 (es⇩_{1}@ es⇩_{2})" and "es⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and "es⇩_{2}= map (λv. (v, False)) (delete_effects_of op)" shows "∀v ∈ set (add_effects_of op). (∃e' ∈ set es⇩_{1}. e' = (v, True))" and "∀v ∈ set (delete_effects_of op). (∃e' ∈ set es⇩_{2}. 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 es⇩_{1}= (λv. (v, True)) ` set (add_effects_of op)" using assms(2) List.set_map by auto then obtain e' where "e' ∈ set es⇩_{1}" and "e' = (λv. (v, True)) v" using a by blast then have "∃e' ∈ set es⇩_{1}. e' = (v, True)" by blast } thus "v ∈ set (add_effects_of op) ⟹ ∃e' ∈ set es⇩_{1}. 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 es⇩_{2}= (λv. (v, False)) ` set (delete_effects_of op)" using assms(3) List.set_map by force then obtain e'' where "e'' ∈ set es⇩_{2}" and "e'' = (λv. (v, False)) v" using a by blast then have "∃e'' ∈ set es⇩_{2}. e'' = (v, False)" by blast } thus "∀v∈set (delete_effects_of op). ∃e'∈set es⇩_{2}. 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 as⇩_{1}as⇩_{2}where b: "?as = as⇩_{1}@ as⇩_{2}" and c: "as⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and "as⇩_{2}= map (λv. (v, False)) (delete_effects_of op)" using effect_to_assignments_ii by blast have d: "map_of ?as = map_of as⇩_{2}++ map_of as⇩_{1}" 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 as⇩_{1}) = set (add_effects_of op)" using c map_of_constant_assignments_dom by metis then have "v ∈ dom (map_of as⇩_{1})" using a by blast then have "map_of ?as v = map_of as⇩_{1}v" using d by force } moreover { let ?f = "λ_. True" from c have "map_of as⇩_{1}= (Some ∘ ?f) |` (set (add_effects_of op))" using map_of_map_restrict by fast then have "map_of as⇩_{1}v = Some True" using a by auto } moreover have "s' = s ++ map_of as⇩_{2}++ map_of as⇩_{1}" 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 as⇩_{1}as⇩_{2}where b: "?as = as⇩_{1}@ as⇩_{2}" and c: "as⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and d: "as⇩_{2}= map (λv. (v, False)) (delete_effects_of op)" using effect_to_assignments_ii by blast have e: "map_of ?as = map_of as⇩_{2}++ map_of as⇩_{1}" using b Map.map_of_append by auto { have "dom (map_of as⇩_{1}) = set (add_effects_of op)" using c map_of_constant_assignments_dom by metis then have "v ∉ dom (map_of as⇩_{1})" using a1 by blast } note f = this { let ?vs = "delete_effects_of op" have "?vs ≠ []" using a2 by force then have "dom (map_of as⇩_{2}) = set ?vs" using d map_of_constant_assignments_dom by metis } note g = this { have "s' = s ++ map_of as⇩_{2}++ map_of as⇩_{1}" 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 as⇩_{2}"] moreover have "s' v = (s ++ map_of as⇩_{2}) v" using calculation map_add_dom_app_simps(3)[OF f, of "s ++ map_of as⇩_{2}"] by blast moreover have "v ∈ dom (map_of as⇩_{2})" using a2 g by argo ultimately have "s' v = map_of as⇩_{2}v" by fastforce } moreover { let ?f = "λ_. False" from d have "map_of as⇩_{2}= (Some ∘ ?f) |` (set (delete_effects_of op))" using map_of_map_restrict by fast then have "map_of as⇩_{2}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 as⇩_{1}as⇩_{2}where b: "?as = as⇩_{1}@ as⇩_{2}" and c: "as⇩_{1}= map (λv. (v, True)) (add_effects_of op)" and d: "as⇩_{2}= map (λv. (v, False)) (delete_effects_of op)" using effect_to_assignments_ii by blast have e: "map_of ?as = map_of as⇩_{2}++ map_of as⇩_{1}" using b Map.map_of_append by auto { have "dom (map_of as⇩_{1}) = set (add_effects_of op)" using c map_of_constant_assignments_dom by metis then have "v ∉ dom (map_of as⇩_{1})" using a1 by blast } moreover { have "dom (map_of as⇩_{2}) = set (delete_effects_of op)" using d map_of_constant_assignments_dom by metis then have "v ∉ dom (map_of as⇩_{2})" 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 op⇩_{1}op⇩_{2}≡ let add⇩_{1}= add_effects_of op⇩_{1}; add⇩_{2}= add_effects_of op⇩_{2}; del⇩_{1}= delete_effects_of op⇩_{1}; del⇩_{2}= delete_effects_of op⇩_{2}in ¬list_ex (λv. list_ex ((=) v) del⇩_{2}) add⇩_{1}∧ ¬list_ex (λv. list_ex ((=) v) add⇩_{2}) del⇩_{1}" 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 op⇩_{1}op⇩_{2}≡ list_ex (λv. list_ex ((=) v) (delete_effects_of op⇩_{1})) (precondition_of op⇩_{2}) ∨ list_ex (λv. list_ex ((=) v) (precondition_of op⇩_{1})) (delete_effects_of op⇩_{2})" (* 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 "op⇩_{1}∈ set ops" and "op⇩_{2}∈ set ops" shows "are_operator_effects_consistent op⇩_{1}op⇩_{2}= (set (add_effects_of op⇩_{1}) ∩ set (delete_effects_of op⇩_{2}) = {} ∧ set (delete_effects_of op⇩_{1}) ∩ set (add_effects_of op⇩_{2}) = {})" proof - have "(¬list_ex (λv. list_ex ((=) v) (delete_effects_of op⇩_{2})) (add_effects_of op⇩_{1})) = (set (add_effects_of op⇩_{1}) ∩ set (delete_effects_of op⇩_{2}) = {})" using list_ex_intersection[of "delete_effects_of op⇩_{2}" "add_effects_of op⇩_{1}"] by meson moreover have "(¬list_ex (λv. list_ex ((=) v) (add_effects_of op⇩_{2})) (delete_effects_of op⇩_{1})) = (set (delete_effects_of op⇩_{1}) ∩ set (add_effects_of op⇩_{2}) = {})" using list_ex_intersection[of "add_effects_of op⇩_{2}" "delete_effects_of op⇩_{1}"] by meson ultimately show "are_operator_effects_consistent op⇩_{1}op⇩_{2}= (set (add_effects_of op⇩_{1}) ∩ set (delete_effects_of op⇩_{2}) = {} ∧ set (delete_effects_of op⇩_{1}) ∩ set (add_effects_of op⇩_{2}) = {})" unfolding are_operator_effects_consistent_def by presburger qed lemma are_all_operator_effects_consistent_set: "are_all_operator_effects_consistent ops ⟷ (∀op⇩_{1}∈ set ops. ∀op⇩_{2}∈ set ops. (set (add_effects_of op⇩_{1}) ∩ set (delete_effects_of op⇩_{2}) = {}) ∧ (set (delete_effects_of op⇩_{1}) ∩ set (add_effects_of op⇩_{2}) = {}))" proof - { fix op⇩_{1}op⇩_{2}assume "op⇩_{1}∈ set ops" and "op⇩_{2}∈ set ops" hence "are_operator_effects_consistent op⇩_{1}op⇩_{2}= (set (add_effects_of op⇩_{1}) ∩ set (delete_effects_of op⇩_{2}) = {} ∧ set (delete_effects_of op⇩_{1}) ∩ set (add_effects_of op⇩_{2}) = {})" using are_operator_effects_consistent_set[of op⇩_{1}ops op⇩_{2}] 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 op⇩_{1}op⇩_{2}" shows "are_operators_interfering op⇩_{2}op⇩_{1}" 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 op⇩_{1}op⇩_{2}" and "op⇩_{1}≠ op⇩_{2}" shows "op⇩_{1}∉ set ops ∨ op⇩_{2}∉ set ops" using assms proof (induction ops) case (Cons op ops) thm Cons.IH[OF _ Cons.prems(2, 3)] have nb⇩_{1}: "∀op' ∈ set ops. ¬are_operators_interfering op op'" and nb⇩_{2}: "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 = op⇩_{1}" | (B) "op = op⇩_{2}" | (C) "op ≠ op⇩_{1}∧ op ≠ op⇩_{2}" by blast thus ?case proof (cases) case A { assume "op⇩_{2}∈ set (op # ops)" then have "op⇩_{2}∈ set ops" using Cons.prems(3) A by force then have "¬are_operators_interfering op⇩_{1}op⇩_{2}" using nb⇩_{1}A by fastforce hence False using Cons.prems(2).. } thus ?thesis by blast next case B { assume "op⇩_{1}∈ set (op # ops)" then have "op⇩_{1}∈ set ops" using Cons.prems(3) B by force then have "¬are_operators_interfering op⇩_{1}op⇩_{2}" using nb⇩_{1}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 nb⇩_{2}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 nb⇩_{1}: "∀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 nb⇩_{2}: "∀op ∈ set ops. ¬are_operators_interfering a op" using assms(3) unfolding are_all_operators_non_interfering_def list_all_iff by simp have nb⇩_{3}: "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] nb⇩_{1}nb⇩_{2}nb⇩_{3}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 "∀op∈set 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 \<^term>‹ops› all operators in the corresponding set are applicable in a given state \<^term>‹s› and all operator effects are consistent, if an operator \<^term>‹op› exists with \<^term>‹op ∈ set ops› and with \<^term>‹v› being an add effect of \<^term>‹op›, then the successor state @{text[display, indent=4] "s' ≡ execute_parallel_operator s ops"} will evaluate \<^term>‹v› to true, that is @{text[display, indent=4] "execute_parallel_operator s ops v = Some True"} Symmetrically, if \<^term>‹v› 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 \<^term>‹v› 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 \<^term>‹I›. First, all parallel operators \<^term>‹ops = π ! k› for any index \<^term>‹k› with \<^term>‹k < length τ - 1› (meaning that \<^term>‹k› is not the index of the last element). must be applicable and their effects must be consistent. Otherwise, the trace would have terminated and \<^term>‹ops› would have been the last element. This would violate the assumption that \<^term>‹k < 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 \<^term>‹k› with\newline \<^term>‹k < length (trace_parallel_plan_strips I π)›, the \<^term>‹k›-th element of the trace is state reached by executing the plan prefix \<^term>‹take k π› consisting of the first \<^term>‹k› 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 \<^term>‹I› and \<^term>‹G›, we can show that it's equivalent to say that \<^term>‹π› is a solution for \<^term>‹I› and \<^term>‹G›---i.e. \<^term>‹G ⊆⇩_{m}execute_parallel_plan I π›---and that the goal state is subsumed by the last element of the trace of \<^term>‹π› with initial state \<^term>‹I›. › 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 nb⇩_{1}: "∀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 nb⇩_{1}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 nb⇩_{2}= 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 nb⇩_{2}by blast } moreover have "∀ops ∈ set (embed π). ∀op ∈ set ops. op ∈ set ((Π)⇩_{𝒪})" using embedding_lemma_iii[OF nb⇩_{1}]. 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 nb⇩_{1}= 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 nb⇩_{2}: "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 nb⇩_{3}: "are_operator_effects_consistent op op" using nb⇩_{1}[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 nb⇩_{2}unfolding is_operator_applicable_in_def by (simp add: execute_operator_def nb⇩_{2}) 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 \<^term>‹k < 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 nb⇩_{1}: "∀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 nb⇩_{2}: "∀v. ?I v ≠ None ⟶ the (?I v) ∈ set (the (?D v))" and "∀v. ?G v ≠ None ⟶ v ∈ set ?vs" and nb⇩_{3}: "∀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 nb⇩_{1}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 nb⇩_{2}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 nb⇩_{3}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 \<^term>‹op› that is applicable in a state \<^term>‹s› and has a consistent set of effects (second assumption) we can now show that the successor state \<^term>‹s' ≡ s ⪢⇩_{+}op› has the following properties: \begin{itemize} \item \<^term>‹s' v = Some a› if \<^term>‹(v, a)› exist in \<^term>‹set (effect_of op)›; and, \item \<^term>‹s' 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 \<^term>‹v›. › 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 \<^term>‹ops› 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 \<^term>‹I›, 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 \<^term>‹k < 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 \<^term>‹k < length τ›, the parallel execution of the plan prefix \<^term>‹take k ψ› with initial state \<^term>‹I› equals the \<^term>‹k›-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 nb⇩_{1}: "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 nb⇩_{2}: "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 nb⇩_{2}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 nb⇩_{1}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 nb⇩_{1}nb⇩_{2}] 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 "