Theory List_Supplement
theory List_Supplement
imports Main
begin
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
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
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
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)
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 = {}")
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)
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
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
thus ?thesis
using ih nb
by (cases "fst x = v") fastforce+
qed simp
qed fastforce
endTheory CNF_Supplement
theory CNF_Supplement
imports "Propositional_Proof_Systems.CNF_Formulas_Sema"
begin
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
endTheory CNF_Semantics_Supplement
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
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
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
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
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"
endTheory STRIPS_Representation
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"
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"
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"
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)"
endTheory STRIPS_Semantics
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:
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)
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
{
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:
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
{
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
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
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
lemma map_of_constant_assignments_dom:
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
{
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
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
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} ›
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)"
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) π"
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
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
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
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)"
{
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
{
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
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
}
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
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
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
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
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
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
also have "… = id ` set (add_effects_of op) ∪ id ` set (delete_effects_of op)"
by force
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
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
}
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
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
}
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
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.} ›
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)
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
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
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
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
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 -
{
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
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)
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)
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. ›
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)
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
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
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 -
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 -
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
{
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 π"
{
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.›
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
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"
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)"
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
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
endTheory SAS_Plus_Semantics
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"
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} ›
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)
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
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"
{
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)
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:
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
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
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
endTheory SAS_Plus_STRIPS
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 ← ψ]"
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 Ψ))"
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 ⦈"
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
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
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:
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 "v ∈ set ((Ψ)⇩𝒱⇩+) ∧ s v ≠ None ∧ a ∈ ℛ⇩+ Ψ v"