# Theory AcycSspace

```theory AcycSspace
imports
FactoredSystem
ActionSeqProcess
SystemAbstraction
Acyclicity
FmapUtils
begin

section "Acyclic State Spaces"

― ‹NOTE name shortened.›
― ‹NOTE type for `max` had to be fixed to natural number maximum (due to problem with loose
typing).›
value "(state_successors (prob_proj PROB vs))"
definition S
where "S vs lss PROB s ≡ wlp
(λx y. y ∈ (state_successors (prob_proj PROB vs) x))
(λs. problem_plan_bound (snapshot PROB s))
(max :: nat ⇒ nat ⇒ nat) (λx y. x + y + 1) s lss
"

― ‹NOTE name shortened.›
― ‹NOTE using `fun` because of multiple defining equations.›
fun vars_change where
"vars_change [] vs s = []"
| "vars_change (a # as) vs s = (if fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s
then state_succ s a # vars_change as vs (state_succ s a)
else vars_change as vs (state_succ s a)
)"

lemma vars_change_cat:
fixes s
shows "
vars_change (as1 @ as2) vs s
= (vars_change as1 vs s @ vars_change as2 vs (exec_plan s as1))
"
by (induction as1 arbitrary: s as2 vs) auto

lemma empty_change_no_change:
fixes s
assumes "(vars_change as vs s = [])"
shows "(fmrestrict_set vs (exec_plan s as) = fmrestrict_set vs s)"
using assms
proof (induction as arbitrary: s vs)
case (Cons a as)
then show ?case
proof (cases "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s")
case True
― ‹NOTE This case violates the induction premise @{term "vars_change (a # as) vs s = []"} since the
empty list is impossible.›
then have "state_succ s a # vars_change as vs (state_succ s a) = []"
using Cons.prems True
by simp
then show "fmrestrict_set vs (exec_plan s (a # as)) = fmrestrict_set vs s"
by blast
next
case False
then have "vars_change as vs (state_succ s a) = []"
using Cons.prems False
by force
then have
"fmrestrict_set vs (exec_plan (state_succ s a) as) = fmrestrict_set vs (state_succ s a)"
using Cons.IH[of vs "(state_succ s a)"]
by blast
then show "fmrestrict_set vs (exec_plan s (a # as)) = fmrestrict_set vs s"
using False
by simp
qed
qed auto

― ‹NOTE renamed variable `a` to `b` to not conflict with naming for list head in induction step.›
lemma zero_change_imp_all_effects_submap:
fixes s s'
assumes "(vars_change as vs s = [])" "(sat_precond_as s as)" "(ListMem b as)"
"(fmrestrict_set vs s = fmrestrict_set vs s')"
shows "(fmrestrict_set vs (snd b) ⊆⇩f fmrestrict_set vs s')"
using assms
proof (induction as arbitrary: s s' vs b)
case (Cons a as)
― ‹NOTE Having either @{term "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"} or
@{term "¬ListMem b as"} leads to simpler propositions so we split here.›
then show "(fmrestrict_set vs (snd b) ⊆⇩f fmrestrict_set vs s')"
using Cons.prems(1)
proof (cases "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s ∧ ListMem b as")
case True
let ?s="state_succ s a"
have "vars_change as vs ?s = []"
using True Cons.prems(1)
by auto
moreover have "sat_precond_as ?s as"
using Cons.prems(2) sat_precond_as.simps(2)
by blast
ultimately show ?thesis
using True Cons.prems(4) Cons.IH
by auto
next
case False
then consider
(i) "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"
| (ii) "¬ListMem b as"
by blast
then show ?thesis
using Cons.prems(1)
proof (cases)
case ii
then have "a = b"
using Cons.prems(3) ListMem_iff set_ConsD
by metis
― ‹NOTE Mysteriously sledgehammer finds a proof here while the premises of
`no\_change\_vs\_eff\_submap` cannot be proven individually.›
then show ?thesis
using Cons.prems(1, 2, 4) no_change_vs_eff_submap
by (metis list.distinct(1) sat_precond_as.simps(2) vars_change.simps(2))
qed simp
qed
qed (simp add: ListMem_iff)

lemma zero_change_imp_all_preconds_submap:
fixes s s'
assumes "(vars_change as vs s = [])" "(sat_precond_as s as)" "(ListMem b as)"
"(fmrestrict_set vs s = fmrestrict_set vs s')"
shows "(fmrestrict_set vs (fst b) ⊆⇩f fmrestrict_set vs s')"
using assms
proof (induction as arbitrary: vs s s')
case (Cons a as)
― ‹NOTE Having either @{term "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"} or
@{term "¬ListMem b as"} leads to simpler propositions so we split here.›
then show "(fmrestrict_set vs (fst b) ⊆⇩f fmrestrict_set vs s')"
using Cons.prems(1)
proof (cases "fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s ∧ ListMem b as")
case True
let ?s="state_succ s a"
have "vars_change as vs ?s = []"
using True Cons.prems(1)
by auto
moreover have "sat_precond_as ?s as"
using Cons.prems(2) sat_precond_as.simps(2)
by blast
ultimately show ?thesis
using True Cons.prems(4) Cons.IH
by auto
next
case False
then consider
(i) "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s"
| (ii) "¬ListMem b as"
by blast
then show ?thesis
using Cons.prems(1)
proof (cases)
case ii
then have "a = b"
using Cons.prems(3) ListMem_iff set_ConsD
by metis
then show ?thesis
using Cons.prems(2, 4) fmsubset_restrict_set_mono
by (metis sat_precond_as.simps(2))
qed simp
qed
qed (simp add: ListMem_iff)

lemma no_vs_change_valid_in_snapshot:
assumes "(as ∈ valid_plans PROB)" "(sat_precond_as s as)" "(vars_change as vs s = [])"
shows "(as ∈ valid_plans (snapshot PROB (fmrestrict_set vs s)))"
proof -
{
fix a
assume P: "ListMem a as"
then have "agree (fst a) (fmrestrict_set vs s)"
by (metis agree_imp_submap assms(2) assms(3) fmdom'_restrict_set
restricted_agree_imp_agree zero_change_imp_all_preconds_submap)
moreover have "agree (snd a) (fmrestrict_set vs s)"
by (metis (no_types) P agree_imp_submap assms(2) assms(3) fmdom'_restrict_set
restricted_agree_imp_agree zero_change_imp_all_effects_submap)
ultimately have "agree (fst a) (fmrestrict_set vs s)" "agree (snd a) (fmrestrict_set vs s)"
by simp+
}
then show ?thesis
using assms(1) as_mem_agree_valid_in_snapshot
by blast
qed

― ‹NOTE type of `PROB` had to be fixed for `problem\_plan\_bound\_works`.›
lemma no_vs_change_obtain_snapshot_bound_1st_step:
fixes PROB :: "'a problem"
assumes "finite PROB" "(vars_change as vs s = [])" "(sat_precond_as s as)"
"(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃as'.
(
exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
= exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
)
∧ (subseq as' as)
∧ (length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
)"
proof -
let ?s="(fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s)"
let ?PROB="(snapshot PROB (fmrestrict_set vs s))"
{
have "finite (snapshot PROB (fmrestrict_set vs s))"
using assms(1) FINITE_snapshot
by blast
}
moreover {
have "
fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s
∈ valid_states (snapshot PROB (fmrestrict_set vs s))"
using assms(4) graph_plan_not_eq_last_diff_paths valid_states_snapshot
by blast
}
moreover {
have "as ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
using assms(2, 3, 5) no_vs_change_valid_in_snapshot
by blast
}
ultimately show ?thesis
using problem_plan_bound_works[of ?PROB ?s as]
by blast
qed

― ‹NOTE type of `PROB` had to be fixed for `no\_vs\_change\_obtain\_snapshot\_bound\_1st\_step`.›
lemma no_vs_change_obtain_snapshot_bound_2nd_step:
fixes PROB :: "'a problem"
assumes "finite PROB" "(vars_change as vs s = [])" "(sat_precond_as s as)"
"(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃as'.
(
exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s)))  s) as
= exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
)
∧ (subseq as' as)
∧ (sat_precond_as s as')
∧ (length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
)"
proof -
obtain as'' where 1:
"
exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
= exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as''"
"subseq as'' as" "length as'' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
using assms no_vs_change_obtain_snapshot_bound_1st_step
by blast
let ?s'="(fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s)"
let ?as'="rem_condless_act ?s' [] as''"
have "exec_plan ?s' as = exec_plan ?s' as''"
using 1(1) rem_condless_valid_1
by blast
moreover have "subseq ?as' as"
using 1(2) rem_condless_valid_8 sublist_trans
by blast
moreover have "sat_precond_as s ?as'"
using sat_precond_drest_sat_precond rem_condless_valid_2
by fast
moreover have "(length ?as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))"
using 1 rem_condless_valid_3 le_trans
by blast
ultimately show ?thesis
using 1 rem_condless_valid_1
by auto
qed

lemma no_vs_change_obtain_snapshot_bound_3rd_step:
assumes "finite (PROB :: 'a problem)" "(vars_change as vs s = [])" "(no_effectless_act as)"
"(sat_precond_as s as)" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃as'.
(
fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as)
= fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')
)
∧ (subseq as' as)
∧ (length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
)"
proof -
obtain as' :: "(('a, bool) fmap × ('a, bool) fmap) list" where
"(
exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as
= exec_plan (fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) s) as'
)" "subseq as' as" "sat_precond_as s as'"
"length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
using assms(1, 2, 4, 5, 6) no_vs_change_obtain_snapshot_bound_2nd_step
by blast
moreover have
"exec_plan (fmrestrict_set vs s) (as_proj as vs) = fmrestrict_set vs (exec_plan s as)"
using assms(4) sat_precond_exec_as_proj_eq_proj_exec
by blast
moreover have "as_proj as (prob_dom (snapshot PROB (fmrestrict_set vs s))) = as"
using assms(2, 3, 4, 6) as_proj_eq_as no_vs_change_valid_in_snapshot
by blast
ultimately show ?thesis
using sublist_as_proj_eq_as proj_exec_proj_eq_exec_proj'
by metis
qed

― ‹NOTE added lemma.›
― ‹TODO remove unused assumptions.›
lemma no_vs_change_snapshot_s_vs_is_valid_bound_i:
fixes PROB :: "'a problem"
assumes  "finite PROB" "(vars_change as vs s = [])" "(no_effectless_act as)"
"(sat_precond_as s as)" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
"fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as) =
fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')"
"subseq as' as" "length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
shows
"fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
(exec_plan s as)
= fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
s
∧ fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
(exec_plan s as')
= fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
s"
proof -
let ?vs="(prob_dom (snapshot PROB (fmrestrict_set vs s)))"
let ?vs'="(fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))"
let ?vs''="(fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))"
let ?s="(exec_plan s as)"
let ?s'="(exec_plan s as')"
have 1: "as ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
using assms(2, 4, 6) no_vs_change_valid_in_snapshot
by blast
{
{
fix a
assume "ListMem a as"
then have "fmdom' (snd a) ⊆ prob_dom (snapshot PROB (fmrestrict_set vs s))"
using 1 FDOM_eff_subset_prob_dom_pair valid_plan_mems
by metis
then have "fmdom' (fmrestrict_set (fmdom' (exec_plan s as)
- prob_dom (snapshot PROB (fmrestrict_set vs s))) (snd a))
= {}"
using subset_inter_diff_empty[of "fmdom' (snd a)"
"prob_dom (snapshot PROB (fmrestrict_set vs s))"] fmdom'_restrict_set_precise
by metis
}
then have
"fmrestrict_set ?vs' (exec_plan s as) = fmrestrict_set ?vs' s"
using disjoint_effects_no_effects[of as ?vs' s]
by blast
}
moreover {
{
fix a
assume P: "ListMem a as'"
moreover have α: "as' ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
using assms(8) 1 sublist_valid_plan
by blast
moreover have "a ∈ PROB"
using P α snapshot_subset subsetCE valid_plan_mems
by fast
ultimately have "fmdom' (snd a) ⊆ prob_dom (snapshot PROB (fmrestrict_set vs s))"
using FDOM_eff_subset_prob_dom_pair valid_plan_mems
by metis
then have "fmdom' (fmrestrict_set (fmdom' (exec_plan s as')
- prob_dom (snapshot PROB (fmrestrict_set vs s))) (snd a))
= {}"
using subset_inter_diff_empty[of "fmdom' (snd a)"
"prob_dom (snapshot PROB (fmrestrict_set vs s))"] fmdom'_restrict_set_precise
by metis
}
then have
"fmrestrict_set ?vs'' (exec_plan s as') = fmrestrict_set ?vs'' s"
using disjoint_effects_no_effects[of as' ?vs'' s]
by blast
}
ultimately show ?thesis
by blast
qed

― ‹NOTE type for `PROB` had to be fixed.›
lemma no_vs_change_snapshot_s_vs_is_valid_bound:
fixes PROB :: "'a problem"
assumes "finite PROB" "(vars_change as vs s = [])" "(no_effectless_act as)"
"(sat_precond_as s as)" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃as'.
(exec_plan s as = exec_plan s as')
∧ (subseq as' as)
∧ (length as' <= problem_plan_bound (snapshot PROB (fmrestrict_set vs s)))
)"
proof -
obtain as' where 1:
"fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as) =
fmrestrict_set (prob_dom (snapshot PROB (fmrestrict_set vs s))) (exec_plan s as')"
"subseq as' as" "length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
using assms no_vs_change_obtain_snapshot_bound_3rd_step
by blast
{

have a: "fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
(exec_plan s as)
= fmrestrict_set (fmdom' (exec_plan s as) - prob_dom (snapshot PROB (fmrestrict_set vs s)))
s "
"fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
(exec_plan s as')
= fmrestrict_set (fmdom' (exec_plan s as') - prob_dom (snapshot PROB (fmrestrict_set vs s)))
s"
using assms 1 no_vs_change_snapshot_s_vs_is_valid_bound_i
by blast+
moreover have "as' ∈ valid_plans (snapshot PROB (fmrestrict_set vs s))"
using "1"(2) assms(2) assms(4) assms(6) no_vs_change_valid_in_snapshot sublist_valid_plan
by blast
moreover have "(exec_plan s as) ∈ valid_states PROB"
using assms(5, 6) valid_as_valid_exec
by blast
moreover have "(exec_plan s as') ∈ valid_states PROB"
using assms(5, 6) 1 valid_as_valid_exec sublist_valid_plan
by blast
ultimately have "exec_plan s as = exec_plan s as'"
using assms
unfolding valid_states_def
using graph_plan_lemma_5[where vs="prob_dom (snapshot PROB (fmrestrict_set vs s))", OF _ 1(1)]
by force
}
then show ?thesis
using 1
by blast
qed

― ‹TODO showcase (problems with stronger typing: Isabelle requires strict typing for `max`; whereas
in HOL4 this is not required, possible because 'MAX' is natural number specific.›
lemma snapshot_bound_leq_S:
shows "
problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
≤ S vs lss PROB (fmrestrict_set vs s)
"
proof -
have "geq_arg (max :: nat ⇒ nat ⇒ nat)"
unfolding geq_arg_def
using max.cobounded1
by simp
then show ?thesis
unfolding S_def
using individual_weight_less_eq_lp[where
g="max :: nat ⇒ nat ⇒ nat"
and x="(fmrestrict_set vs s)" and R="(λx y. y ∈ state_successors (prob_proj PROB vs) x)"
and w="(λs. problem_plan_bound (snapshot PROB s))" and f="(λx y. x + y + 1)" and l=lss]
by blast
qed

― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
― ‹NOTE the type of `1` had to be restricted to `nat` to ensure the proofs for `geq\_arg` work.›
lemma S_geq_S_succ_plus_ell:
assumes "(s ∈ valid_states PROB)"
"(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
"(s' ∈ state_successors (prob_proj PROB vs) s)" "(set lss = valid_states (prob_proj PROB vs))"
shows "(
problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
+ S vs lss PROB (fmrestrict_set vs s')
+ (1 :: nat)
≤ S vs lss PROB (fmrestrict_set vs s)
)"
proof -
let ?f="λx y. x + y + (1 :: nat)"
let ?R="(λx y. y ∈ state_successors (prob_proj PROB vs) x)"
let ?w="(λs. problem_plan_bound (snapshot PROB s))"
let ?g="max :: nat ⇒ nat ⇒ nat"
let ?vtx1="(fmrestrict_set vs s')"
let ?G="lss"
let ?vtx2="(fmrestrict_set vs s)"
have "geq_arg ?f"
unfolding geq_arg_def
by simp
moreover have "geq_arg ?g"
unfolding geq_arg_def
by simp
moreover have "∀x. ListMem x lss ⟶ ¬?R x x"
unfolding state_successors_def
by blast
moreover have "?R ?vtx2 ?vtx1"
unfolding state_successors_def
using assms(3) state_in_successor_proj_in_state_in_successor state_successors_def
by blast
moreover have
"ListMem ?vtx1 ?G"
using assms(1, 3, 4)
by (metis ListMem_iff contra_subsetD graph_plan_not_eq_last_diff_paths proj_successors_of_valid_are_valid)
moreover have "top_sorted_abs ?R ?G"
using assms(2)
by simp
ultimately show ?thesis
unfolding S_def
using lp_geq_lp_from_successor[of ?f ?g ?G ?R ?vtx2 ?vtx1 ?w]
by blast
qed

lemma vars_change_cons:
fixes s s'
assumes "(vars_change as vs s = (s' # ss))"
shows "(∃as1 act as2.
(as = as1 @ (act # as2))
∧ (vars_change as1 vs s = [])
∧ (state_succ (exec_plan s as1) act = s')
∧ (vars_change as2 vs (state_succ (exec_plan s as1) act) = ss)
)"
using assms
proof (induction as arbitrary: s s' vs ss)
case (Cons a as)
then show ?case
proof (cases "fmrestrict_set vs (state_succ s a) ≠ fmrestrict_set vs s")
case True
then have "state_succ s a = s'" "vars_change as vs (state_succ s a) = ss"
using Cons.prems
by simp+
then show ?thesis
by fastforce
next
case False
then have "vars_change as vs (state_succ s a) = s' # ss"
using Cons.prems
by simp
then obtain as1 act as2 where
"as = as1 @ act # as2" "vars_change as1 vs (state_succ s a) = []"
"state_succ (exec_plan (state_succ s a) as1) act = s'"
"vars_change as2 vs (state_succ (exec_plan (state_succ s a) as1) act) = ss"
using Cons.IH
by blast
then show ?thesis
by (metis False append_Cons exec_plan.simps(2) vars_change.simps(2))
qed
qed simp

lemma vars_change_cons_2:
fixes s s'
assumes "(vars_change as vs s = (s' # ss))"
shows "(fmrestrict_set vs s' ≠ fmrestrict_set vs s)"
using assms
apply(induction as arbitrary: s s' vs ss)
apply(auto)
by (metis list.inject)

― ‹NOTE first argument of `top\_sorted\_abs had to be wrapped into lambda.›
lemma problem_plan_bound_S_bound_1st_step:
fixes PROB :: "'a problem"
assumes "finite PROB" "(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
"(set lss = valid_states (prob_proj PROB vs))" "(s ∈ valid_states PROB)"
"(as ∈ valid_plans PROB)" "(no_effectless_act as)" "(sat_precond_as s as)"
shows "(∃as'.
(exec_plan s as' = exec_plan s as)
∧ (subseq as' as)
∧ (length as' <= S vs lss PROB (fmrestrict_set vs s))
)"
using assms
proof (induction "vars_change as vs s" arbitrary: PROB as vs s lss)
case Nil
then obtain as' where
"exec_plan s as = exec_plan s as'" "subseq as' as"
"length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
using Nil(1) Nil.prems(1,4,5,6,7) no_vs_change_snapshot_s_vs_is_valid_bound
by metis
moreover have "
problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
≤ S vs lss PROB (fmrestrict_set vs s)
"
using snapshot_bound_leq_S le_trans
by fast
ultimately show ?case
using le_trans
by fastforce
next
case (Cons s' ss)
then obtain as1 act as2 where 1:
"as = as1 @ act # as2" "vars_change as1 vs s = []" "state_succ (exec_plan s as1) act = s'"
"vars_change as2 vs (state_succ (exec_plan s as1) act) = ss"
using vars_change_cons
by smt
text‹ Obtain conclusion of induction hypothesis for 'as2' and
'(state\_succ (exec\_plan s as1) act)'. ›
{
{
have "as1 ∈ valid_plans PROB"
using Cons.prems(5) 1(1) valid_append_valid_pref
by blast
moreover have "act ∈ PROB"
using Cons.prems(5) 1 valid_append_valid_suff valid_plan_valid_head
by fast
ultimately have "state_succ (exec_plan s as1) act ∈ valid_states PROB"
using Cons.prems(4) valid_as_valid_exec lemma_1_i
by blast
}
moreover have "as2 ∈ valid_plans PROB"
using Cons.prems(5) 1(1) valid_append_valid_suff valid_plan_valid_tail
by fast
moreover have "no_effectless_act as2"
using Cons.prems(6) 1(1) rem_effectless_works_13 sublist_append_back
by blast
moreover have "sat_precond_as (state_succ (exec_plan s as1) act) as2"
using Cons.prems(7) 1(1) graph_plan_lemma_17 sat_precond_as.simps(2)
by blast
ultimately have "∃as'.
exec_plan (state_succ (exec_plan s as1) act) as'
= exec_plan (state_succ (exec_plan s as1) act) as2
∧ subseq as' as2
∧ length as' ≤ S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
using Cons.prems(1, 2, 3) 1(4)
Cons(1)[where as="as2" and s="(state_succ (exec_plan s as1) act)"]
by blast
}
note a=this
{
have "no_effectless_act as1"
using Cons.prems(6) 1(1) rem_effectless_works_12
by blast
moreover have "sat_precond_as s as1"
using Cons.prems(7) 1(1) sat_precond_as_pfx
by blast
moreover have "as1 ∈ valid_plans PROB"
using Cons.prems(5) 1(1) valid_append_valid_pref
by blast
ultimately have "∃as'. exec_plan s as1 = exec_plan s as' ∧
subseq as' as1 ∧ length as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
using no_vs_change_snapshot_s_vs_is_valid_bound[of _ as1]
using Cons.prems(1, 4) 1(2)
by blast
}
then obtain as'' where b:
"exec_plan s as1 = exec_plan s as''" "subseq as'' as1"
"length as'' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))"
by blast
{
obtain as' where i:
"exec_plan (state_succ (exec_plan s as1) act) as'
= exec_plan (state_succ (exec_plan s as1) act) as2"
"subseq as' as2"
"length as' ≤ S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
using a
by blast
let ?as'="as'' @ act # as'"
have "exec_plan s ?as' = exec_plan s as"
using 1(1) b(1) i(1) exec_plan_Append exec_plan.simps(2)
by metis
moreover have "subseq ?as' as"
using 1(1) b(2) i(2) subseq_append_iff
by blast
moreover
{
{
― ‹NOTE this is proved earlier in the original proof script. Moved here to improve
transparency.›
have "sat_precond_as (exec_plan s as1) (act # as2)"
using empty_replace_proj_dual7
using 1(1) Cons.prems(7)
by blast
then have "fst act ⊆⇩f (exec_plan s as1)"
by simp
}
note A = this
{
have
"fmrestrict_set vs (state_succ (exec_plan s as1) act)
= (state_succ (fmrestrict_set vs (exec_plan s as'')) (action_proj act vs))"
using b(1) A drest_succ_proj_eq_drest_succ[where s="exec_plan s as1", symmetric]
by simp
also have "… = (state_succ (fmrestrict_set vs s) (action_proj act vs))"
using 1(2) b(1) empty_change_no_change
by fastforce
finally have "… = fmrestrict_set  vs (state_succ s (action_proj act vs))"
using  succ_drest_eq_drest_succ
by blast
}
note B = this
have C: "fmrestrict_set vs (exec_plan s as'') = fmrestrict_set vs s"
using 1(2) b(1) empty_change_no_change
by fastforce
{
have "act ∈ PROB"
using Cons.prems(5) 1 valid_append_valid_suff valid_plan_valid_head
by fast
then have ℵ: "action_proj act vs ∈ prob_proj PROB vs"
using action_proj_in_prob_proj
by blast
then have "(state_succ s (action_proj act vs)) ∈ (state_successors (prob_proj PROB vs) s)"
proof (cases "fst (action_proj act vs) ⊆⇩f s")
case True
then show ?thesis
unfolding state_successors_def
using Cons.hyps(2) 1(3) b(1) A B C ℵ DiffI imageI singletonD vars_change_cons_2
drest_succ_proj_eq_drest_succ
by metis
next
case False
then show ?thesis
unfolding state_successors_def
using Cons.hyps(2) 1(3) b(1) A B C ℵ DiffI imageI singletonD
drest_succ_proj_eq_drest_succ vars_change_cons_2
by metis
qed
}
then have D:
"problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
+ S vs lss PROB (fmrestrict_set vs (state_succ s (action_proj act vs)))
+ 1
≤ S vs lss PROB (fmrestrict_set vs s)"
using Cons.prems(2, 3, 4) S_geq_S_succ_plus_ell[where s'="state_succ s (action_proj act vs)"]
by blast
{
have
"length ?as' ≤ problem_plan_bound (snapshot PROB (fmrestrict_set vs s))
+ 1 + S vs lss PROB (fmrestrict_set vs (state_succ (exec_plan s as1) act))"
using b i
by fastforce
then have "length ?as' ≤ S vs lss PROB (fmrestrict_set vs s)"
using b(1) A B C D drest_succ_proj_eq_drest_succ
by (smt Suc_eq_plus1 add_Suc dual_order.trans)
}
}
ultimately have ?case
by blast
}
then show ?case
by blast
qed

― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
lemma problem_plan_bound_S_bound_2nd_step:
assumes "finite (PROB :: 'a problem)"
"(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
"(set lss = valid_states (prob_proj PROB vs))" "(s ∈ valid_states PROB)"
"(as ∈ valid_plans PROB)"
shows "(∃as'.
(exec_plan s as' = exec_plan s as)
∧ (subseq as' as)
∧ (length as' ≤ S vs lss PROB (fmrestrict_set vs s))
)"
proof -
― ‹NOTE Proof premises and obtain conclusion of `problem\_plan\_bound\_S\_bound\_1st\_step`.›
{
have a: "rem_condless_act s [] (rem_effectless_act as) ∈ valid_plans PROB"
using assms(5) rem_effectless_works_4' rem_condless_valid_10
by blast
then have b: "no_effectless_act (rem_condless_act s [] (rem_effectless_act as))"
using assms rem_effectless_works_6 rem_condless_valid_9
by fast
then have "sat_precond_as s (rem_condless_act s [] (rem_effectless_act as))"
using assms rem_condless_valid_2
by blast
then have "∃as'.
exec_plan s as' = exec_plan s (rem_condless_act s [] (rem_effectless_act as))
∧ subseq as' (rem_condless_act s [] (rem_effectless_act as))
∧ length as' ≤ S vs lss PROB (fmrestrict_set vs s)
"
using assms a b problem_plan_bound_S_bound_1st_step
by blast
}
then obtain as' where 1:
"exec_plan s as' = exec_plan s (rem_condless_act s [] (rem_effectless_act as))"
"subseq as' (rem_condless_act s [] (rem_effectless_act as))"
"length as' ≤ S vs lss PROB (fmrestrict_set vs s)"
by blast
then have 2: "exec_plan s as' = exec_plan s as"
using rem_condless_valid_1 rem_effectless_works_14
by metis
then have "subseq as' as"
using 1(2) rem_condless_valid_8 rem_effectless_works_9 sublist_trans
by metis
then show ?thesis
using 1(3) 2
by blast
qed

― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
lemma S_in_MPLS_leq_2_pow_n:
assumes "finite (PROB :: 'a problem)"
"(top_sorted_abs (λ x y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
"(set lss = valid_states (prob_proj PROB vs))" "(s ∈ valid_states PROB)"
"(as ∈ valid_plans PROB)"
shows "(∃as'.
(exec_plan s as' = exec_plan s as)
∧ (subseq as' as)
∧ (length as' ≤ Sup {S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB  vs)})
)"
proof -
obtain as' where
"exec_plan s as' = exec_plan s as" "subseq as' as"
"length as' ≤ S vs lss PROB (fmrestrict_set vs s)"
using assms problem_plan_bound_S_bound_2nd_step
by blast
moreover {
― ‹NOTE Derive sufficient conditions for inferring that `S vs lss PROB` is smaller or equal to
the supremum of the set @{term "{S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB vs)}"}: i.e.
being contained and that the supremum is contained as well.›
let ?S="{S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB vs)}"
{
have "fmrestrict_set vs s ∈ valid_states (prob_proj PROB vs)"
using assms(4) graph_plan_not_eq_last_diff_paths
by blast
then have "S vs lss PROB (fmrestrict_set vs s) ∈ ?S"
using calculation(1)
by blast
}
moreover
{
have "finite (prob_proj PROB vs)"
by (simp add: assms(1) prob_proj_def)
then have "finite ?S"
using Setcompr_eq_image assms(3)
by (metis List.finite_set finite_imageI)
}
ultimately have "S vs lss PROB (fmrestrict_set vs s) ≤ Sup ?S"
using le_cSup_finite by blast
}
ultimately show ?thesis
using le_trans
by blast
qed

― ‹NOTE first argument of `top\_sorted\_abs` had to be wrapped into lambda.›
lemma problem_plan_bound_S_bound:
fixes PROB :: "'a problem"
assumes "finite PROB" "(top_sorted_abs (λx y. y ∈ state_successors (prob_proj PROB vs) x) lss)"
"(set lss = valid_states (prob_proj PROB vs))"
shows "
problem_plan_bound PROB
≤ Sup {S vs lss PROB (s' :: 'a state) | s'. s' ∈ valid_states (prob_proj PROB vs)}
"
proof -
let ?f="λPROB.
Sup {S vs lss PROB (s' :: 'a state) | s'. s' ∈ valid_states (prob_proj PROB vs)} + 1"
{
fix as and s :: "'a state"
assume "s ∈ valid_states PROB" "as ∈ valid_plans PROB"
then obtain as' where a:
"exec_plan s as' = exec_plan s as" "subseq as' as"
"length as' ≤ Sup {S vs lss PROB s' |s'. s' ∈ valid_states (prob_proj PROB vs)}"
using assms S_in_MPLS_leq_2_pow_n
by blast
then have "length as' < ?f PROB"
by linarith
moreover have "exec_plan s as = exec_plan s as'"
using a(1)
by simp
ultimately have
"∃as'. exec_plan s as = exec_plan s as' ∧ subseq as' as ∧ length as' < ?f PROB"
using a(2)
by blast
}
then show ?thesis
using assms(1) problem_plan_bound_UBound[where f="?f"]
by fastforce
qed

subsection "State Space Acyclicity"

text ‹ State space acyclicity is again formalized using graphs to model the state space. However
the relation inducing the graph is the successor relation on states. [Abdulaziz et al.,
Definition 15, HOL4 Definition 15, p.27]

With this, the acyclic system compositional bound `S` can be shown to be an upper bound on the
sublist diameter (lemma `problem\_plan\_bound\_S\_bound\_thesis`). [Abdulaziz et al., p.29] ›

― ‹NOTE name shortened.›
― ‹NOTE first argument of 'top\_sorted\_abs' had to be wrapped into lambda.›
definition sspace_DAG where
"sspace_DAG PROB lss ≡ (
(set lss = valid_states PROB)
∧ (top_sorted_abs (λx y. y ∈ state_successors PROB x) lss)
)"

lemma problem_plan_bound_S_bound_2nd_step_thesis:
assumes "finite (PROB :: 'a problem)" "(sspace_DAG (prob_proj PROB vs) lss)"
"(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)"
shows "(∃as'.   (exec_plan s as' = exec_plan s as)
∧ (subseq as' as)
∧ (length as' ≤ S vs lss PROB (fmrestrict_set vs s))
)"
using assms problem_plan_bound_S_bound_2nd_step sspace_DAG_def
by fast

text ‹And finally, this is the main lemma about the upper bounding algorithm.›

theorem problem_plan_bound_S_bound_thesis:
assumes "finite (PROB :: 'a problem)" "(sspace_DAG (prob_proj PROB vs) lss)"
shows "(
problem_plan_bound PROB
≤ Sup {S vs lss PROB s' | s'. s' ∈ valid_states (prob_proj PROB vs)}
)"
using assms problem_plan_bound_S_bound sspace_DAG_def
by fast

end```