Theory 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
end