# Theory SystemAbstraction

```theory SystemAbstraction
imports
Main
"HOL-Library.Sublist"
"HOL-Library.Finite_Map"
FactoredSystem
FactoredSystemLib
ActionSeqProcess
Dependency
TopologicalProps
FmapUtils
ListUtils

begin

section "System Abstraction"

text ‹ Projection of an object (state, action, sequence of action or factored representation)
to a variable set `vs` restricts the domain of the object or its components---in case of composite
objects---to `vs`. [Abdulaziz et al., p.12]

This section presents the relevant definitions (`action\_proj`, `as\_proj`, `prob\_proj` and `ss\_proj`)
as well as their characterization. ›

subsection "Projection of Actions, Sequences of Actions and Factored Representations."

definition action_proj where
"action_proj a vs ≡ (fmrestrict_set vs (fst a), fmrestrict_set vs (snd a))"

lemma action_proj_pair: "action_proj (p, e) vs = (fmrestrict_set vs p, fmrestrict_set vs e)"
unfolding action_proj_def
by simp

definition prob_proj where
"prob_proj PROB vs ≡ (λa. action_proj a vs) ` PROB"

― ‹NOTE  using 'fun' due to multiple defining equations.›
― ‹NOTE  name shortened.›
fun as_proj where
"as_proj [] _ = []"
| "as_proj (a # as) vs = (if fmdom' (fmrestrict_set vs (snd a)) ≠ {}
then action_proj a vs # as_proj as vs
else as_proj as vs
)"

― ‹TODO the lemma might be superfluous (follows directly from 'as\_proj.simps').›
lemma as_proj_pair:
"as_proj ((p, e) # as) vs = (if (fmdom' (fmrestrict_set vs e) ≠ {})
then action_proj (p, e) vs # as_proj as vs
else as_proj as vs
)"
"as_proj [] vs = []"
by (simp)+

lemma proj_state_succ:
fixes s a vs
assumes "(fst a ⊆⇩f s)"
shows  "(state_succ (fmrestrict_set vs s) (action_proj a vs) = fmrestrict_set vs (state_succ s a))"
proof -
have "
fmrestrict_set vs (if fst a ⊆⇩f s then snd a ++ s else s)
= fmrestrict_set vs (snd a ++ s)
"
using assms
by simp
moreover
{
assume "fst (action_proj a vs) ⊆⇩f fmrestrict_set vs s"
then have "
(state_succ (fmrestrict_set vs s) (action_proj a vs)
= fmrestrict_set vs (snd a ++ s))
"
by force
}
moreover {
assume "¬(fst (action_proj a vs) ⊆⇩f fmrestrict_set vs s)"
then have "
(state_succ (fmrestrict_set vs s) (action_proj a vs)
= fmrestrict_set vs (snd a ++ s))
"
unfolding state_succ_def  action_proj_def
using assms fmsubset_restrict_set_mono
by auto
}
ultimately show ?thesis
unfolding state_succ_def
by argo
qed

lemma graph_plan_lemma_1:
fixes s vs as
assumes "sat_precond_as s as"
shows "(exec_plan (fmrestrict_set vs s) (as_proj as vs) = (fmrestrict_set vs (exec_plan s as)))"
using assms
proof (induction as arbitrary: s vs)
case (Cons a as)
then show ?case
proof (cases "fmdom' (fmrestrict_set vs (snd a)) ≠ {}")
case True
then have
"state_succ (fmrestrict_set vs s) (action_proj a vs) = fmrestrict_set vs (state_succ s a)"
using Cons.prems proj_state_succ
by fastforce
then show ?thesis
unfolding exec_plan.simps sat_precond_as.simps as_proj.simps
using Cons.IH Cons.prems True
by simp
next
case False
then have "(fmdom' (snd a) ∩ vs = {})"
using False fmdom'_restrict_set_precise[of vs "snd a"]
by argo
then have "fmrestrict_set vs s = fmrestrict_set vs (state_succ s a)"
using disj_imp_eq_proj_exec
by blast
then show ?thesis
unfolding exec_plan.simps sat_precond_as.simps as_proj.simps
using Cons.IH Cons.prems False
by simp
qed
qed simp

― ‹TODO the proofs are inefficient (detailed proofs?).›
lemma  proj_action_dom_eq_inter:
shows "
action_dom (fst (action_proj a vs)) (snd (action_proj a vs))
= (action_dom (fst a) (snd a) ∩ vs)
"
unfolding action_dom_def action_proj_def
by (auto simp: fmdom'_restrict_set_precise)

lemma graph_plan_neq_mems_state_set_neq_len:
shows "prob_dom (prob_proj PROB vs) = (prob_dom PROB ∩ vs)"
proof -
have "
prob_dom (prob_proj PROB vs)
= (
⋃(s1, s2)∈(λa. (fmrestrict_set vs (fst a), fmrestrict_set vs (snd a)))
`  PROB. action_dom s1 s2
)
"
unfolding prob_dom_def prob_proj_def action_proj_def
by blast
moreover
{
have "
(prob_dom PROB ∩ vs)
= (⋃a∈PROB. action_dom (fst a) (snd a)  ∩ vs)
"
unfolding prob_dom_def prob_proj_def
using SUP_cong
by auto
also have "… = (⋃a∈PROB. action_dom (fst (action_proj a vs)) (snd (action_proj a vs)))"
using proj_action_dom_eq_inter[symmetric]
by fast
finally have "
(prob_dom PROB ∩ vs)
= (⋃a∈PROB. fmdom' (fmrestrict_set vs (fst a)) ∪ fmdom' (fmrestrict_set vs (snd a)))
"
unfolding action_dom_def action_proj_def
by simp
}
ultimately show ?thesis
by (metis (mono_tags, lifting) SUP_cong UN_simps(10) action_dom_def case_prod_beta' prod.sel(1)
snd_conv)
qed

― ‹TODO more detailed proof.›
lemma graph_plan_not_eq_last_diff_paths:
fixes PROB vs
assumes "(s ∈ valid_states PROB)"
shows "((fmrestrict_set vs s) ∈ valid_states (prob_proj PROB vs))"

unfolding valid_states_def
using graph_plan_neq_mems_state_set_neq_len
by (metis (mono_tags, lifting)
assms fmdom'.rep_eq fmlookup_fmrestrict_set_dom inf_commute mem_Collect_eq valid_states_def)

lemma dom_eff_subset_imp_dom_succ_eq_proj:
fixes h s vs
assumes "(fmdom' (snd h) ⊆ fmdom' s)"
shows "(fmdom' (state_succ s (action_proj h vs)) = fmdom' (state_succ s h))"
proof (cases "fst (fmrestrict_set vs (fst h), fmrestrict_set vs (snd h)) ⊆⇩f s")
case true: True
then show ?thesis
proof (cases "fst h ⊆⇩f s")
case True
then show ?thesis
unfolding state_succ_def action_proj_def
using true True
inf.absorb_iff2 inf.left_commute sup.absorb_iff1)
next
case False
then show ?thesis
unfolding state_succ_def action_proj_def
using true False
fmlookup_fmrestrict_set_dom inf_le2 sup.absorb_iff1)
qed
next
case False
then have "fmdom' s = fmdom' (if fst h ⊆⇩f s then snd h ++ s else s)"
using sat_precond_as_proj_4
by auto
then show ?thesis
unfolding state_succ_def action_proj_def
using False
by presburger
qed

lemma drest_proj_succ_eq_drest_succ:
fixes h s vs
assumes "fst h ⊆⇩f s" "(fmdom' (snd h) ⊆ fmdom' s)"
shows "(fmrestrict_set vs (state_succ s (action_proj h vs)) = fmrestrict_set vs (state_succ s h))"
proof -
{
have 1: "fmrestrict_set vs (fst h) ⊆⇩f s"
using assms(1) submap_imp_state_succ_submap_a
then have "
fmrestrict_set vs (state_succ s (action_proj h vs))
= fmrestrict_set vs (fmrestrict_set vs (snd h) ++ s)
"
unfolding state_succ_def action_proj_def
by simp
also have "… = fmrestrict_set vs s ++⇩f fmrestrict_set vs (fmrestrict_set vs (snd h))"
by simp
― ‹TODO
refactor the step 'fmrestrict\_set ?X (fmrestrict\_set ?X ?f) = fmrestrict\_set ?X ?f' into
own lemma in 'FmapUtils.thy'.›
also have "… = fmrestrict_set vs s ++⇩f fmrestrict_set vs (snd h)"
using fmfilter_alt_defs(4) fmfilter_cong fmlookup_filter fmrestrict_set_dom option.simps(3)
by metis
finally have "
fmrestrict_set vs (state_succ s (action_proj h vs))
= fmrestrict_set vs (snd h ++ s)
"
by simp
}
moreover have "fmrestrict_set vs (state_succ s h) = fmrestrict_set vs ((snd h) ++ s)"
unfolding state_succ_def
using assms(1)
by simp
ultimately show ?thesis
by simp
qed

― ‹TODO remove? This is equivalent to 'proj\_state\_succ'.›
lemma drest_succ_proj_eq_drest_succ:
fixes s vs as
assumes "(fst a ⊆⇩f s)"
shows "(state_succ (fmrestrict_set vs s) (action_proj a vs) = fmrestrict_set vs (state_succ s a))"
using assms proj_state_succ
by blast

lemma exec_drest_cons_proj_eq_succ:
fixes as PROB vs a
assumes "fst a ⊆⇩f s"
shows "(
exec_plan (fmrestrict_set vs s) (action_proj a vs # as)
= exec_plan (fmrestrict_set vs (state_succ s a)) as
)"
proof -
have "exec_plan (state_succ (fmrestrict_set vs s) (action_proj a vs)) as =
exec_plan (fmrestrict_set vs (state_succ s a)) as"
using assms drest_succ_proj_eq_drest_succ
by metis
then show ?thesis
unfolding prob_proj_def
by simp
qed

lemma exec_drest:
fixes as a vs
assumes "(fst a ⊆⇩f s)"
shows "(
exec_plan (fmrestrict_set vs (state_succ s a)) as
= exec_plan (fmrestrict_set vs s) (action_proj a vs # as)
)"
using assms proj_state_succ
by fastforce

lemma not_empty_eff_in_as_proj:
fixes as a vs
assumes "fmdom' (fmrestrict_set vs (snd a)) ≠ {}"
shows "(as_proj (a # as) vs = (action_proj a vs # as_proj as vs))"
unfolding action_proj_def as_proj.simps
using assms
by argo

lemma empty_eff_not_in_as_proj:
fixes as a vs
assumes "(fmdom' (fmrestrict_set vs (snd a)) = {})"
shows "(as_proj (a # as) vs = as_proj as vs)"
unfolding action_proj_def
using assms
by simp

lemma empty_eff_drest_no_eff:
fixes s and a and vs
assumes "(fmdom' (fmrestrict_set vs (snd a)) = {})"
shows "(fmrestrict_set vs (state_succ s (action_proj a vs)) = fmrestrict_set vs s)"
proof -
have "fmdom' (snd (action_proj a vs)) = {}"
unfolding action_proj_def
using assms
by simp
then have "state_succ s (action_proj a vs) = s"
using empty_eff_exec_eq
by fast
then show ?thesis
by simp
qed

lemma sat_precond_exec_as_proj_eq_proj_exec:
fixes as vs s
assumes "(sat_precond_as s as)"
shows "(exec_plan (fmrestrict_set vs s) (as_proj as vs) = fmrestrict_set vs (exec_plan s as))"
using assms
proof (induction as)
case (Cons a as)
then show ?case
using Cons.prems graph_plan_lemma_1
by blast
qed auto

lemma action_proj_in_prob_proj:
assumes "(a ∈ PROB)"
shows "(action_proj a vs ∈ prob_proj PROB vs)"
unfolding action_proj_def prob_proj_def
using assms
by simp

lemma valid_as_valid_as_proj:
fixes PROB vs
assumes "(as ∈ valid_plans PROB)"
shows "(as_proj as vs ∈ valid_plans (prob_proj PROB vs))"
using assms
proof (induction "as" arbitrary: PROB vs)
case (Cons a as)
then show ?case
using assms Cons
proof(cases "fmdom' (fmrestrict_set vs (snd a)) ≠ {}")
case True
then have 1: "as_proj (a # as) vs = action_proj a vs # as_proj as vs"
using True
by simp
then have "as ∈ valid_plans PROB"
using Cons.prems valid_plan_valid_tail
by fast
then  have "as_proj as vs ∈ valid_plans (prob_proj PROB vs)"
using Cons.IH 1
by simp
then have "action_proj a vs # as_proj as vs ∈ valid_plans (prob_proj PROB vs)"
by metis
then show ?thesis
using 1
by argo
next
case False
then have "as_proj (a # as) vs = as_proj as vs"
using False
by auto
then have "as_proj (a # as) vs ∈ valid_plans (prob_proj PROB vs)"
using assms Cons valid_plan_valid_tail
by metis
then show ?thesis
using assms Cons.IH(1)
by blast
qed

lemma finite_imp_finite_prob_proj:
fixes PROB
assumes "finite PROB"
shows "(finite (prob_proj PROB vs))"
unfolding prob_proj_def
using assms
by simp

― ‹NOTE Base 2 in 5th assumption had to be explicitely fixed to 'nat' type to be able to use the
linearity lemma for powers of natural numbers.›
lemma
fixes PROB vs as and s :: "'a state"
assumes "finite PROB" "s ∈ valid_states PROB" "as ∈ (valid_plans PROB)" "finite vs"
"length (as_proj as vs) > ((2 :: nat) ^ card vs) - 1" "sat_precond_as s as"
shows "(∃as1 as2 as3.
(as1 @ as2 @ as3 = as_proj as vs)
∧ (exec_plan (fmrestrict_set vs s) (as1 @ as2) = exec_plan (fmrestrict_set vs s) as1)
∧ (as2 ≠ [])
)"
proof -
{
have "card (fmdom' (fmrestrict_set vs s)) ≤ card vs"
using assms(4) graph_plan_card_state_set
by fast
then have "(2 :: nat) ^ (card (fmdom' (fmrestrict_set vs s))) - 1 ≤ 2 ^ (card vs) - 1"
using power_increasing diff_le_mono
by force
also have "... < length (as_proj as vs)"
using assms(5)
by blast
finally have "2 ^ card (fmdom' (fmrestrict_set vs s)) - 1 < length (as_proj as vs)"
by blast
}
note 1 = this
moreover have "fmrestrict_set vs s ∈ valid_states (prob_proj PROB vs)"
using assms(2) graph_plan_not_eq_last_diff_paths
by blast
moreover have "as_proj as vs ∈ valid_plans (prob_proj PROB vs)"
using assms(3) valid_as_valid_as_proj
by blast
moreover have "finite (prob_proj PROB vs)"
using assms(1) finite_imp_finite_prob_proj
by blast
ultimately show ?thesis
using lemma_2[where PROB="prob_proj PROB vs" and as="as_proj as vs" and s="fmrestrict_set vs s"]
by blast
qed

lemma as_proj_eq_filter_action_proj:
fixes as vs
shows "as_proj as vs = filter (λa. fmdom' (snd a) ≠ {}) (map (λa. action_proj a vs) as)"
by (induction as) (auto simp add: action_proj_def)

lemma append_eq_as_proj:
fixes as1 as2 as3 p vs
assumes "(as1 @ as2 @ as3 = as_proj p vs)"
shows "(∃p_1 p_2 p_3.
(p_1 @ p_2 @ p_3 = p)
∧ (as2 = as_proj p_2 vs)
∧ (as1 = as_proj p_1 vs)
)"
using assms append_eq_as_proj_1 as_proj_eq_filter_action_proj
by (metis (no_types, lifting))

lemma succ_drest_eq_drest_succ:
fixes a s vs
shows "
state_succ (fmrestrict_set vs s) (action_proj a vs)
= fmrestrict_set vs (state_succ s (action_proj a vs))
"
proof -
let ?lhs = "state_succ (fmrestrict_set vs s) (action_proj a vs)"
let ?rhs = "fmrestrict_set vs (state_succ s (action_proj a vs))"
― ‹NOTE Show lhs and rhs equality by splitting on the cases introduced by the if-then branching
of 'state\_succ'.›
{
assume P1: "fst (fmrestrict_set vs (fst a), fmrestrict_set vs (snd a)) ⊆⇩f fmrestrict_set vs s"
then have a: "fst (fmrestrict_set vs (fst a), fmrestrict_set vs (snd a)) ⊆⇩f s"
using drest_smap_drest_smap_drest
by auto
then have "?lhs = fmrestrict_set vs (snd a) ++ fmrestrict_set vs s"
unfolding state_succ_def action_proj_def
using P1
by simp
moreover {
have rhs: "?rhs = fmrestrict_set vs (fmrestrict_set vs (snd a) ++ s)"
unfolding state_succ_def action_proj_def
using a
by auto
also have "… = (fmrestrict_set vs (fmrestrict_set vs (snd a)) ++ fmrestrict_set vs s)"
by simp
finally have "?rhs = (fmrestrict_set vs (snd a) ++ fmrestrict_set vs s)"
unfolding fmfilter_alt_defs(4)
by fastforce
}
ultimately have "?lhs = ?rhs"
by argo
}
moreover {
assume P2: "¬(fst (fmrestrict_set vs (fst a), fmrestrict_set vs (snd a)) ⊆⇩f fmrestrict_set vs s)"
then have a: "¬(fst (fmrestrict_set vs (fst a), fmrestrict_set vs (snd a)) ⊆⇩f s)"
using drest_smap_drest_smap_drest
by auto
then have "?lhs = fmrestrict_set vs s"
unfolding state_succ_def action_proj_def
using P2
by argo
moreover have "?rhs = fmrestrict_set vs s"
unfolding state_succ_def action_proj_def
using a
by presburger
ultimately have "?lhs = ?rhs"
by simp
}
ultimately show "?lhs = ?rhs"
by blast
qed

lemma proj_exec_proj_eq_exec_proj:
fixes s as vs
shows "
fmrestrict_set vs (exec_plan (fmrestrict_set vs s) (as_proj as vs))
= exec_plan (fmrestrict_set vs s) (as_proj as vs)
"
proof (induction as arbitrary: s vs)
case (Cons a as)
then show ?case

lemma proj_exec_proj_eq_exec_proj':
fixes s as vs
shows "
fmrestrict_set vs (exec_plan (fmrestrict_set vs s) (as_proj as vs))
= fmrestrict_set vs (exec_plan s (as_proj as vs))
"
proof (induction as arbitrary: s vs)
case (Cons a as)
then show ?case

lemma graph_plan_lemma_9:
fixes s as vs
shows "
fmrestrict_set vs (exec_plan s (as_proj as vs))
= exec_plan (fmrestrict_set vs s) (as_proj as vs)
"
by (metis proj_exec_proj_eq_exec_proj' proj_exec_proj_eq_exec_proj)

lemma act_dom_proj_eff_subset_act_dom_eff:
fixes a vs
shows "fmdom' (snd (action_proj a vs)) ⊆ fmdom' (snd a)"
proof -
have "snd (action_proj a vs) = fmrestrict_set vs (snd a)"
unfolding action_proj_def
by simp
then have "fmlookup (fmrestrict_set vs (snd a)) ⊆⇩m fmlookup (snd a)"
then have "dom (fmlookup (fmrestrict_set vs (snd a))) ⊆ dom (fmlookup (snd a))"
using map_le_implies_dom_le
by blast
then have "fmdom' (fmrestrict_set vs (snd a)) ⊆ fmdom' (snd a)"
using fmdom'.rep_eq
by metis
then show ?thesis
unfolding action_proj_def
by simp
qed

lemma exec_as_proj_valid:
fixes as s PROB vs
assumes "s ∈ valid_states PROB" "(as ∈ valid_plans PROB)"
shows  "(exec_plan s (as_proj as vs) ∈ valid_states PROB)"
using assms
proof (induction as arbitrary: s PROB vs)
case (Cons a as)
then have 1: "as ∈ valid_plans PROB"
using Cons.prems(2) valid_plan_valid_tail
by fast
then have 2: "exec_plan s (as_proj as vs) ∈ valid_states PROB"
using Cons.prems(1) Cons.IH(1)
by blast
― ‹NOTE split on the if-then branch introduced by 'as\_proj'.›
moreover {
assume P: "fmdom' (fmrestrict_set vs (snd a)) ≠ {}"
then have "
exec_plan s (as_proj (a # as) vs)
= exec_plan (state_succ s (action_proj a vs)) (as_proj as vs)
"
by simp
― ‹NOTE split on the if-then branch introduced by 'state\_succ'›
moreover
{
assume "fst (action_proj a vs) ⊆⇩f s"
then have 3: "
exec_plan (state_succ s (action_proj a vs)) (as_proj as vs)
= exec_plan (snd (action_proj a vs) ++ s) (as_proj as vs)
"
unfolding state_succ_def
using calculation
by simp
{
― ‹TODO Unsure why this proof step is necessary at all, but it should be refactored into a
dedicated lemma @{term "s ∈ valid_states PROB ⟹ fmdom' s = prob_dom PROB"}.›
{
have "s ∈ valid_states PROB"
using Cons.prems
by simp
then have "s ∈ {s'. fmdom' s' = prob_dom PROB}"
unfolding valid_states_def
by simp
then obtain s' where "s' = s" "fmdom' s' = prob_dom PROB"
by auto
then have "fmdom' s = prob_dom PROB"
by simp
}
― ‹TODO Refactor this step ('also ...' for subset chain; replace fact
`fmdom' s = prob\_dom PROB` in last step with MP step from lemma refactored above.›
moreover {
have "(snd (action_proj a vs) ++ s) = (s ++⇩f fmrestrict_set vs (snd a))"
by simp
then have a: "a ∈ PROB"
by fast
then have "action_dom (fst a) (snd a) ⊆ prob_dom PROB"
using exec_as_proj_valid_2
by blast
then have "fmdom' (snd a) ⊆ action_dom (fst a) (snd a)"
unfolding action_dom_def
by simp
then have "fmdom' (fmrestrict_set vs (snd a)) ⊆ fmdom' (snd a)"
using action_proj_def act_dom_proj_eff_subset_act_dom_eff snd_conv
by metis
then have "fmdom' (fmrestrict_set vs (snd a)) ⊆ prob_dom PROB"
using FDOM_eff_subset_prob_dom_pair a
by blast
then have "fmdom' (s ++⇩f fmrestrict_set vs (snd a)) = fmdom' s"
}
ultimately have "(snd (action_proj a vs) ++ s) ∈ valid_states PROB"
by simp
}
then have "exec_plan s (as_proj (a # as) vs) ∈ valid_states PROB"
using 1 3 calculation(1) Cons.IH[where s = "snd (action_proj a vs) ++ s"]
by presburger
}
moreover {
assume "¬(fst (action_proj a vs) ⊆⇩f s)"
then have "
exec_plan (state_succ s (action_proj a vs)) (as_proj as vs)
= exec_plan s (as_proj as vs)
"
unfolding state_succ_def
by simp
then have "exec_plan s (as_proj (a # as) vs) ∈ valid_states PROB"
using 2
by force
}
ultimately have "exec_plan s (as_proj (a # as) vs) ∈ valid_states PROB"
by blast
}
moreover
{
assume "fmdom' (fmrestrict_set vs (snd a)) = {}"
then have "
exec_plan s (as_proj (a # as) vs) =
exec_plan s (as_proj as vs)
"
by simp
then have "exec_plan s (as_proj (a # as) vs) ∈ valid_states PROB"
using 2
by argo
}
ultimately show ?case
by blast
qed simp

lemma drest_exec_as_proj_eq_drest_exec:
fixes s as vs
assumes "sat_precond_as s as"
shows "(fmrestrict_set vs (exec_plan s (as_proj as vs)) = fmrestrict_set vs (exec_plan s as))"
proof -
have 1: "
(fmrestrict_set vs (exec_plan s (as_proj as vs))
= exec_plan (fmrestrict_set vs s) (as_proj as vs))
"
using graph_plan_lemma_9 by auto
then obtain s' where 2: "exec_plan (fmrestrict_set vs s) (as_proj as vs) = fmrestrict_set vs s'"
using 1
by metis
then have "fmrestrict_set vs s' = fmrestrict_set vs (exec_plan s as)"
using assms sat_precond_exec_as_proj_eq_proj_exec
by metis
then show
"fmrestrict_set vs (exec_plan s (as_proj as vs)) = fmrestrict_set vs (exec_plan s as)"
using 1 2
by argo
qed

lemma action_proj_idempot:
fixes a vs
shows "action_proj (action_proj a vs) vs = (action_proj a vs)"
unfolding action_proj_def

lemma  action_proj_idempot':
fixes a vs
assumes "(action_dom (fst a) (snd a) ⊆ vs)"
shows "(action_proj a vs = a)"
using assms
proof -
have 1: "action_proj a vs = (fmrestrict_set vs (fst a), fmrestrict_set vs (snd a))"
then have 2: "(fmdom' (fst a) ∪ fmdom' (snd a)) ⊆ vs"
unfolding action_dom_def
using assms
― ‹NOTE Show that both components of 'a' remain unchanged.›
{
then have "fmdom' (fst a) ⊆ vs"
by blast
then have "fmrestrict_set vs (fst a) = (fst a)"
using exec_drest_5
by auto
}
moreover {
have "fmdom' (snd a) ⊆ vs"
using 2
by auto
then have "fmrestrict_set vs (snd a) = (snd a)"
using exec_drest_5
by blast
}
ultimately show ?thesis
using 1
by simp
qed

lemma action_proj_idempot'':
fixes P vs
assumes "prob_dom P ⊆ vs"
shows "prob_proj P vs = P"
using assms
proof -
― ‹TODO refactor.›
{
fix a
assume "a ∈ P"
then have "action_dom (fst a) (snd a) ⊆ vs"
using assms exec_as_proj_valid_2
by fast
then have "action_proj a vs = a"
using action_proj_idempot'
by fast
}
then have "prob_proj P vs = P"
unfolding prob_proj_def
by force
then show ?thesis
unfolding prob_proj_def
by simp
qed

lemma sat_precond_as_proj:
fixes as s s' vs
assumes "(sat_precond_as s as)" "(fmrestrict_set vs s = fmrestrict_set vs s')"
shows "(sat_precond_as s' (as_proj as vs))"
using assms
proof (induction as arbitrary: s s' vs)
case (Cons a as)
then have 1:
"fst a ⊆⇩f s" "sat_precond_as (state_succ s a) as"
using Cons.prems(1)
by simp+
then have 2: "fmrestrict_set vs (fst a) ⊆⇩f s"
using assms(1) sat_precond_as_proj_4
by blast
moreover
{
assume "fmdom' (fmrestrict_set vs (snd a)) ≠ {}"
then have "
sat_precond_as s' (as_proj (a # as) vs)
= (
fst (action_proj a vs) ⊆⇩f s'
∧ sat_precond_as (state_succ s' (action_proj a vs)) (as_proj as vs)
)
"
using calculation
by simp
moreover
{
have "fst (action_proj a vs) ⊆⇩f s' = (fmrestrict_set vs (fst a) ⊆⇩f s')"
unfolding action_proj_def
by simp
moreover have "(fmrestrict_set vs (fst a) ⊆⇩f s) = (fmrestrict_set vs (fst a) ⊆⇩f s')"
using Cons.prems(2) sat_precond_as_proj_1
by blast
ultimately have "fst (action_proj a vs) ⊆⇩f s'"
using 2
by blast
}
― ‹TODO detailled proof for this sledgehammered step.›
moreover have "sat_precond_as (state_succ s' (action_proj a vs)) (as_proj as vs)"
using 1 Cons.IH Cons.prems(2) drest_succ_proj_eq_drest_succ succ_drest_eq_drest_succ
by metis
ultimately have "(sat_precond_as s' (as_proj (a # as) vs))"
by blast
}
moreover
{
assume P1: "¬(fmdom' (fmrestrict_set vs (snd a)) ≠ {})"
then have "sat_precond_as s' (as_proj (a # as) vs)"
proof (cases "as_proj (a # as) vs")
case Cons2: (Cons a' list)
― ‹TODO unfold the sledgehammered metis steps.›
then have a: "
sat_precond_as s' (as_proj (a # as) vs)
= (fst a' ⊆⇩f s') ∧ sat_precond_as (state_succ s' a') list
"
using P1 Cons.IH Cons.prems(1, 2) Cons2
by (metis sat_precond_as_proj_3 empty_eff_not_in_as_proj sat_precond_as.simps(2))
then have b: "fst a' ⊆⇩f s'"
unfolding sat_precond_as.simps(2)
using P1 Cons.IH Cons.prems(1, 2) sat_precond_as_proj_3 empty_eff_not_in_as_proj
by (metis sat_precond_as.simps(2))
then have "sat_precond_as (state_succ s' a') list"
using a
by blast
then show ?thesis
using a b
by blast
qed fastforce
}
ultimately show ?case
by blast
qed simp

lemma sat_precond_drest_as_proj:
fixes as s s' vs
assumes "(sat_precond_as s as)" "(fmrestrict_set vs s = fmrestrict_set vs s')"
shows "(sat_precond_as (fmrestrict_set vs s') (as_proj as vs))"
using assms
proof (induction as arbitrary: s s' vs)
case (Cons a as)
then have 1: "fst a ⊆⇩f s" "sat_precond_as (state_succ s a) as"
using Cons.prems
by auto+
then have "fmrestrict_set vs (fst a) ⊆⇩f fmrestrict_set vs s"
using fmsubset_restrict_set_mono
by blast
then have "fst (action_proj a vs) ⊆⇩f fmrestrict_set vs s'"
unfolding action_proj_def
using Cons.prems(2) sat_precond_as_proj_1
by simp
then have "fmrestrict_set vs (snd a) = fmrestrict_set vs (snd (action_proj a vs))"
unfolding action_proj_def
then have "fst (action_proj a vs) ⊆⇩f s"
unfolding action_proj_def
using 1(1) fst_conv sat_precond_as_proj_4
by auto
― ‹TODO unfold these sledgehammered steps.›
then have "
fmrestrict_set vs (state_succ s a)
= fmrestrict_set vs (state_succ (fmrestrict_set vs s') (action_proj a vs))
"
using 1(1) Cons.prems(2)
by (metis fmfilter_alt_defs(4) fmfilter_true fmlookup_restrict_set
drest_succ_proj_eq_drest_succ option.simps(3))
then show ?case
using Cons.prems(1, 2)
by (metis fmfilter_alt_defs(4) fmfilter_true fmlookup_restrict_set sat_precond_as_proj
option.simps(3))
qed simp

lemma as_proj_eq_as:
assumes "(no_effectless_act as)" "(as ∈ valid_plans PROB)" "(prob_dom PROB ⊆ vs)"
shows "(as_proj as vs = as)"
using assms
proof (induction as arbitrary: PROB vs)
case (Cons a as)
― ‹NOTE We only need to look at the first branch of 'as\_proj'.›
― ‹TODO step should be refactored and proven explicitely because it's so pivotal.›
then have "fmdom' (fmrestrict_set vs (snd a)) ≠ {}"
unfolding fmdom'_restrict_set_precise
by (metis
FDOM_eff_subset_prob_dom_pair dual_order.trans inf.orderE
― ‹NOTE Proof 'action\_proj a vs = a' for the first branch of 'as\_proj'.›
moreover {
assume "fmdom' (fmrestrict_set vs (snd a)) ≠ {}"
― ‹NOTE show 'action\_proj a vs = a'.›
moreover {
have "as_proj (a # as) vs = action_proj a vs # as_proj as vs"
using calculation
by force
then have "a ∈ PROB"
by fast
then have "action_dom (fst a) (snd a) ⊆ prob_dom PROB"
using exec_as_proj_valid_2
by fast
then have "action_dom (fst a) (snd a) ⊆ vs"
using Cons.prems(3)
by fast
then have "action_proj a vs = a"
using action_proj_idempot'
by fast
}
― ‹NOTE show that 'as\_proj as vs = as'.›
moreover {
have 1: "no_effectless_act as"
using Cons.prems(1)
by simp
then have "as ∈ valid_plans PROB"
using Cons.prems(2) valid_plan_valid_tail
by fast
then have "as_proj as vs = as"
using Cons.prems(3) Cons.IH 1
by blast
}
ultimately have "as_proj (a # as) vs = a # as"
by simp
}
ultimately show ?case
by fast
qed simp

lemma exec_rem_effless_as_proj_eq_exec_as_proj:
fixes s
shows "exec_plan s (as_proj (rem_effectless_act as) vs) = exec_plan s (as_proj as vs)"
proof (induction as arbitrary: s vs)
case (Cons a as)
― ‹Split cases on the branching introduced by `remove\_effectless\_act` and `as\_proj`.›
then show ?case
proof (cases "fmdom' (snd a) ≠ {}")
case true1: True
then show ?thesis
proof (cases "fmdom' (fmrestrict_set vs (snd a)) ≠ {}")
case False
then show ?thesis by (simp add: Cons true1)
next
case False
then show ?thesis
proof (cases "fmdom' (fmrestrict_set vs (snd a)) ≠ {}")
case true2: True
then have 1: "fmdom' (snd a) ∩ vs = {}"
using False Int_empty_left
by force
― ‹NOTE This step shows that the case for @{term "fmdom' (fmrestrict_set vs (snd a)) ≠ {}"} is
impossible.›
― ‹TODO could be refactored into a (simp) lemma (`as\_proj\_eq\_as` also uses this?).›
then have "fmdom' (fmrestrict_set vs (snd a)) = {}"
then show ?thesis
using true2
by blast
qed
qed simp

lemma exec_as_proj_eq_exec_as:
fixes PROB as vs s
assumes "(as ∈ valid_plans PROB)" "(prob_dom PROB ⊆ vs)"
shows "(exec_plan s (as_proj as vs) = exec_plan s as)"
using assms as_proj_eq_as exec_rem_effless_as_proj_eq_exec_as_proj rem_effectless_works_1 rem_effectless_works_6
rem_effectless_works_9 sublist_valid_plan
by metis

lemma dom_prob_proj: "prob_dom (prob_proj PROB vs) ⊆ vs"
using graph_plan_neq_mems_state_set_neq_len
by fast

― ‹TODO refactor into `FmapUtils.thy`.›
lemma subset_proj_absorb_1_a:
fixes f vs1 vs2
assumes "(vs1 ⊆ vs2)"
shows "fmrestrict_set vs1 (fmrestrict_set vs2 f) = fmrestrict_set vs1 f"
using assms
proof -
{
fix v
have "fmlookup (fmrestrict_set vs1 (fmrestrict_set vs2 f)) v = fmlookup (fmrestrict_set vs1 f) v"
using assms
proof (cases "v ∈ vs1")
case False
then show ?thesis
proof (cases "v ∈ vs2")
case False
then have "v ∉ vs1"
using False assms
by blast
then have
"fmlookup (fmrestrict_set vs1 (fmrestrict_set vs2 f)) v = None"
"fmlookup (fmrestrict_set vs1 f) v = None"
by simp+
then show ?thesis
by argo
qed simp
qed auto
}
then show ?thesis
using fmap_ext
by blast
qed

lemma subset_proj_absorb_1:
assumes "(vs1 ⊆ vs2)"
shows "(action_proj (action_proj a vs2) vs1 = action_proj a vs1)"
using assms
proof -
have
"fmrestrict_set vs1 (fmrestrict_set vs2 (fst a)) = fmrestrict_set vs1 (fst a)"
"fmrestrict_set vs1 (fmrestrict_set vs2 (snd a)) = fmrestrict_set vs1 (snd a)"
using assms subset_proj_absorb_1_a
by blast+
then show ?thesis
unfolding action_proj_def
by simp
qed

lemma subset_proj_absorb:
fixes PROB vs1 vs2
assumes "vs1 ⊆ vs2"
shows "prob_proj (prob_proj PROB vs2) vs1 = prob_proj PROB vs1"
proof -
{
have "
prob_proj (prob_proj PROB vs2) vs1
= ((λa. action_proj a vs1) ∘ (λa. action_proj a vs2)) ` PROB
"
unfolding prob_proj_def
by fastforce
also have "… = (λa. action_proj (action_proj a vs2) vs1) ` PROB"
by fastforce
also have "… = (λa. action_proj a vs1) ` PROB"
using assms subset_proj_absorb_1
by metis
also have "… = prob_proj PROB vs1"
unfolding prob_proj_def
by simp
finally have "prob_proj (prob_proj PROB vs2) vs1 = prob_proj PROB vs1"
by simp
}
then show ?thesis
by simp
qed

lemma union_proj_absorb:
fixes PROB vs vs'
shows "prob_proj (prob_proj PROB (vs ∪ vs')) vs = prob_proj PROB vs"

lemma NOT_VS_IN_DOM_PROJ_PRE_EFF:
fixes ROB vs v a
assumes "¬(v ∈ vs)" "(a ∈ PROB)"
shows "(
((v ∈ fmdom' (fst a)) ⟶ (v ∈ fmdom' (fst (action_proj a (prob_dom PROB - vs)))))
∧ ((v ∈ fmdom' (snd a)) ⟶ (v ∈ fmdom' (snd (action_proj a (prob_dom PROB - vs)))))
)"
unfolding action_proj_def
using assms
FDOM_eff_subset_prob_dom_pair)

lemma IN_DISJ_DEP_IMP_DEP_DIFF:
fixes PROB vs vs' v v'
assumes "(v ∈ vs')" "(v' ∈ vs')" "(disjnt vs vs')"
shows "(dep PROB v v' ⟶ dep (prob_proj PROB (prob_dom PROB - vs)) v v')"
using assms
proof (cases "v = v'")
case False
{
assume P: "dep PROB v v'"
then obtain a where a:
"(v ∈ fmdom' (fst a) ∧ v' ∈ fmdom' (snd a) ∨ v ∈ fmdom' (snd a) ∧ v' ∈ fmdom' (snd a))"
"a ∈ PROB"
unfolding dep_def
using False
by blast
{
have "v ∉ vs"
using assms(1, 3)
unfolding disjnt_def
by blast
then have "(v ∈ fmdom' (fst a) ⟶ v ∈ fmdom' (fst (action_proj a (prob_dom PROB - vs))))"
"(v ∈ fmdom' (snd a) ⟶ v ∈ fmdom' (snd (action_proj a (prob_dom PROB - vs))))"
using a NOT_VS_IN_DOM_PROJ_PRE_EFF
by metis+
}
note b = this
then consider (i) "v ∈ fmdom' (fst a) ∧ v' ∈ fmdom' (snd a)"
| (ii) "v ∈ fmdom' (snd a) ∧ v' ∈ fmdom' (snd a)"
using a
by blast
then have "dep (prob_proj PROB (prob_dom PROB - vs)) v v'"
proof (cases)
case i
then show ?thesis
using assms(2, 3) a(2) b(1)
by (meson dep_def disjnt_iff action_proj_in_prob_proj NOT_VS_IN_DOM_PROJ_PRE_EFF)
next
case ii
then show ?thesis
using assms(2, 3) a(2) b(2)
by (meson dep_def disjnt_iff action_proj_in_prob_proj NOT_VS_IN_DOM_PROJ_PRE_EFF)
qed
}
then show ?thesis
by blast
qed (auto simp: dep_def prob_proj_def disjnt_def)

lemma  PROB_DOM_PROJ_DIFF:
fixes P vs
shows "prob_dom (prob_proj PROB (prob_dom PROB - vs)) = (prob_dom PROB) - vs"
using graph_plan_neq_mems_state_set_neq_len
by fastforce

lemma  two_children_parent_mems_le_finite:
fixes PROB vs
assumes "(vs ⊆ prob_dom PROB)"
shows "(prob_dom (prob_proj PROB vs) = vs)"
using assms graph_plan_neq_mems_state_set_neq_len
by fast

― ‹TODO showcase (non-trivial proof).›
― ‹TODO find explicit proof.›
lemma PROJ_DOM_PRE_EFF_SUBSET_DOM:
fixes a vs
shows "
(fmdom' (fst (action_proj a vs)) ⊆ fmdom' (fst a))
∧ (fmdom' (snd (action_proj a vs)) ⊆ fmdom' (snd a))
"
unfolding action_proj_def
by (auto simp: fmdom'_restrict_set_precise)

lemma NOT_IN_PRE_EFF_NOT_IN_PRE_EFF_PROJ:
fixes a v vs
shows "
(¬(v ∈ fmdom' (fst a)) ⟶ ¬(v ∈ fmdom' (fst (action_proj a vs))))
∧ (¬(v ∈ fmdom' (snd a)) ⟶ ¬(v ∈ fmdom' (snd (action_proj a vs))))
"
using PROJ_DOM_PRE_EFF_SUBSET_DOM rev_subsetD
by metis

lemma dep_proj_dep:
assumes "dep (prob_proj PROB vs) v v'"
shows "dep PROB v v'"
using assms
unfolding dep_def prob_proj_def action_proj_def image_def
apply (auto simp: fmdom'_restrict_set_precise)
by auto

lemma NDEP_PROJ_NDEP:
fixes PROB vs vs' vs''
assumes "(¬dep_var_set PROB vs vs')"
shows "(¬dep_var_set (prob_proj PROB vs'') vs vs')"
using assms dep_proj_dep
unfolding dep_var_set_def
by metis

lemma SUBSET_PROJ_DOM_DISJ:
fixes PROB vs vs'
assumes "(vs ⊆ (prob_dom (prob_proj PROB (prob_dom PROB - vs'))))"
shows "disjnt vs vs'"
using assms
by (auto simp add: PROB_DOM_PROJ_DIFF subset_iff disjnt_iff)

― ‹TODO showcase (lemma which is solved effortlessly by automation).›
lemma NOT_VS_DEP_IMP_DEP_PROJ:
fixes PROB vs v v'
assumes "¬(v ∈ vs)" "¬(v' ∈ vs)" "(dep PROB v v')"
shows "(dep (prob_proj PROB (prob_dom PROB - vs)) v v')"
using assms
by (metis Diff_disjoint Diff_iff disjnt_def insertCI IN_DISJ_DEP_IMP_DEP_DIFF)

lemma DISJ_PROJ_NDEP_IMP_NDEP:
fixes PROB vs vs' vs''
assumes
"(disjnt vs vs'')" "disjnt vs vs'"
"¬(dep_var_set (prob_proj PROB (prob_dom PROB - vs)) vs' vs'')"
shows "¬(dep_var_set PROB vs' vs'')"
proof -
{
assume C: "dep_var_set PROB vs' vs''"
then obtain v1 v2 where "v1 ∈ vs'" "v2 ∈ vs''" "disjnt vs' vs''" "dep PROB v1 v2"
unfolding dep_var_set_def
by blast
then have "∃v1 v2.
v1 ∈ vs' ∧ v2 ∈ vs'' ∧ disjnt vs' vs'' ∧ dep (prob_proj PROB (prob_dom PROB - vs)) v1 v2
"
using assms(1, 2) IntI disjnt_def empty_iff NOT_VS_DEP_IMP_DEP_PROJ
by metis
then have False
using assms
unfolding dep_var_set_def
by blast
}
then show ?thesis
using assms
unfolding dep_var_set_def
by argo
qed

lemma PROJ_DOM_IDEMPOT:
fixes PROB
shows "prob_proj PROB (prob_dom PROB) = PROB"
using action_proj_idempot''
by blast

lemma prob_proj_idempot:
fixes vs vs'
assumes "(vs ⊆ vs')"
shows "(prob_proj PROB vs = prob_proj (prob_proj PROB vs') vs)"
using assms subset_proj_absorb
by blast

lemma prob_proj_dom_diff_eq_prob_proj_prob_proj_dom_diff:
fixes vs vs'
shows "
prob_proj PROB (prob_dom PROB - (vs ∪ vs'))
= prob_proj
(prob_proj PROB (prob_dom PROB - vs))
(prob_dom (prob_proj PROB (prob_dom PROB - vs)) - vs')
"
using PROB_DOM_PROJ_DIFF subset_proj_absorb
by (metis Compl_Diff_eq Diff_subset compl_eq_compl_iff sup_assoc)

lemma PROJ_DEP_IMP_DEP:
fixes PROB vs v v'
assumes "dep (prob_proj PROB (prob_dom PROB - vs)) v v'"
shows "dep PROB v v'"
using assms
unfolding dep_def prob_proj_def
proof (cases "v = v'")
case False
then show "(∃a.
a ∈ PROB
∧ (v ∈ fmdom' (fst a) ∧ v' ∈ fmdom' (snd a) ∨ v ∈ fmdom' (snd a) ∧ v' ∈ fmdom' (snd a)))
∨ v = v'"
using assms
unfolding dep_def prob_proj_def
by (smt image_iff NOT_IN_PRE_EFF_NOT_IN_PRE_EFF_PROJ)
qed blast

lemma PROJ_NDEP_TC_IMP_NDEP_TC_OR:
fixes PROB vs v v'
assumes "¬((λv1' v2'. dep (prob_proj PROB (prob_dom PROB - vs)) v1' v2')⇧+⇧+ v v')"
shows "(
(¬((λv1' v2'. dep PROB v1' v2')⇧+⇧+ v v'))
∨ (∃v''.
v'' ∈ vs
∧ ((λv1' v2'. dep PROB v1' v2')⇧+⇧+ v v'')
∧ ((λv1' v2'. dep PROB v1' v2')⇧+⇧+ v'' v')
)
)"
using assms NOT_VS_DEP_IMP_DEP_PROJ DEP_REFL REFL_TC_CONJ[of
"λv v'. dep PROB v  v'" "λv. ¬(v ∈ vs)" "λv v'. dep (prob_proj PROB (prob_dom PROB- vs)) v v'"
v v']
by fastforce

lemma every_action_proj_eq_as_proj:
fixes as vs
shows "list_all (λ a. action_proj a vs = a) (as_proj as vs)"
by (induction as) (auto simp add: action_proj_idempot)

lemma empty_eff_not_in_as_proj_2:
fixes a as vs
assumes "fmdom' (snd (action_proj a vs)) = {}"
shows "(as_proj as vs = as_proj (a # as) vs)"
using assms

declare[[smt_timeout=100]]

lemma sublist_as_proj_eq_as:
fixes as' as vs
assumes "subseq as' (as_proj as vs)"
shows "(as_proj as' vs = as')"
using assms
proof (induction as arbitrary: as' vs)
case Nil
moreover have "as' = []"
using Nil.prems sublist_NIL
by force
then show ?case
by simp
next
case cons: (Cons a as)
then show ?case
proof (cases "as'")
case (Cons aa list)
then show ?thesis
proof (cases "fmdom' (fmrestrict_set vs (snd aa)) ≠ {}")
case True
then have "as_proj as' vs = action_proj aa vs # as_proj list vs"
using Cons True
by auto
then show ?thesis
by (metis as_proj.simps(2) cons.IH cons.prems action_proj_idempot local.Cons
subseq_Cons2_iff)
next
case False
then have "as_proj as' vs = as_proj list vs"
using Cons False
by simp
then show ?thesis using cons False
unfolding Cons
by (smt action_proj_def action_proj_idempot as_proj.simps(2) prod.inject subseq_Cons2_neq)
qed
qed simp
qed

lemma DISJ_EFF_DISJ_PROJ_EFF:
fixes a s vs
assumes "fmdom' (snd a) ∩ s = {}"
shows "(fmdom' (snd (action_proj a vs)) ∩ s = {})
"
proof -
have 1: "snd (action_proj a vs) = fmrestrict_set vs (snd a)"
unfolding action_proj_def
by simp
then have "fmdom' (fmrestrict_set vs (snd a)) ⊆ fmdom' (snd a)"
using act_dom_proj_eff_subset_act_dom_eff
by metis
then show ?thesis
using assms 1
by auto
qed

― ‹NOTE showcase (the step using `graph\_plan\_lemma\_5`--- labelled by '[1]'--- is non-trivial proof
due to missing premises and the last six proof steps are redundant).›
lemma state_succ_proj_eq_state_succ:
fixes a s vs
assumes "(varset_action a vs)" "(fst a ⊆⇩f s)" "(fmdom' (snd a) ⊆ fmdom' s)"
shows "(state_succ s (action_proj a vs) = state_succ s a)"
proof -
have 1: "fmdom' (snd a) ∩ (fmdom' s - vs) = {}"
using assms(1) vset_disj_eff_diff
by blast
then have  2:
"fmrestrict_set (fmdom' s - vs) s = fmrestrict_set (fmdom' s - vs) (state_succ s a)"
using disj_imp_eq_proj_exec[where vs = "fmdom' s - vs"]
by blast
then have "fmdom' (snd (action_proj a vs)) ∩ (fmdom' s - vs) = {}"
using 1 DISJ_EFF_DISJ_PROJ_EFF[where s = "(fmdom' s - vs)"]
by blast
then have "
fmrestrict_set (fmdom' s - vs) s
= fmrestrict_set (fmdom' s - vs) (state_succ s (action_proj a vs))
"
using disj_imp_eq_proj_exec[where a = "(action_proj a vs)" and vs = "fmdom' s - vs"]
by blast
then have "fmdom' (snd (action_proj a vs)) ∩ (fmdom' s - vs) = {}"
using 1 DISJ_EFF_DISJ_PROJ_EFF[where s = "(fmdom' s - vs)"]
by blast
then have "
fmrestrict_set (fmdom' s - vs) s =
fmrestrict_set (fmdom' s - vs) (state_succ s (action_proj a vs))
"
using disj_imp_eq_proj_exec[of "action_proj a vs" "fmdom' s - vs"]
by fast
― ‹[1]›
― ‹TODO unwrap this step.›
then show ?thesis
using 2 FDOM_state_succ graph_plan_lemma_5[where s = "state_succ s (action_proj a vs)"
and s' = "state_succ s a" and vs = vs] assms(2, 3) dom_eff_subset_imp_dom_succ_eq_proj
drest_proj_succ_eq_drest_succ
by metis
qed

― ‹NOTE duplicate declaration of lemma `state\_succ\_proj\_eq\_state\_succ` removed.›

lemma no_effectless_proj:
fixes vs as
shows "no_effectless_act (as_proj as vs)"
by (induction as arbitrary: vs) (auto simp add: action_proj_def)

― ‹NOTE duplicate (this is identical to `valid\_as\_valid\_as\_proj`).›
lemma as_proj_valid_in_prob_proj:
fixes PROB vs as
assumes "(as ∈ valid_plans PROB)"
shows "(as_proj as vs ∈ valid_plans (prob_proj PROB vs))"
using assms valid_as_valid_as_proj
by blast

― ‹TODO Unwrap the smt proof.›
lemma prob_proj_comm:
fixes PROB vs vs'
shows "prob_proj (prob_proj PROB vs) vs' = prob_proj (prob_proj PROB vs') vs"
by (smt graph_plan_neq_mems_state_set_neq_len inf_commute inf_le2 PROJ_DOM_IDEMPOT prob_proj_idempot)

― ‹TODO Unwrap the metis proof.›
lemma vset_proj_imp_vset:
fixes vs vs' a
assumes "(varset_action a vs')" "(varset_action (action_proj a vs') vs)"
shows "(varset_action a vs)"
unfolding varset_action_def action_proj_def
using assms
by (metis action_proj_def exec_drest_5 snd_conv varset_action_def)

lemma  vset_imp_vset_act_proj_diff:
fixes PROB vs vs' a
assumes "(varset_action a vs)"
shows "(varset_action (action_proj a (prob_dom PROB - vs')) vs)"
proof -
have 1: "(fmdom' (snd a) ⊆ vs)"
using assms varset_action_def
by metis
moreover
{
― ‹TODO refactor and put into `Fmap\_Utils`.›
have "
fmdom' (snd (
fmrestrict_set (prob_dom PROB - vs') (fst a)
, fmrestrict_set (prob_dom PROB - vs') (snd a)
))
= (fmdom' (snd a) ∩ (prob_dom PROB - vs'))
"
by (simp add: Int_def Set.filter_def fmfilter_alt_defs(4))
also have "… ⊆ fmdom' (snd a)"
by simp
finally have "fmdom' (snd (
fmrestrict_set (prob_dom PROB - vs') (fst a)
, fmrestrict_set (prob_dom PROB - vs') (snd a)
))
⊆ vs
"
using 1 by simp
}
ultimately show ?thesis
unfolding varset_action_def dep_var_set_def dep_def action_proj_def
by blast
qed

lemma action_proj_disj_diff:
assumes "(action_dom (fst a) (snd a) ⊆ vs1)" "(vs2 ∩ vs3 = {})"
shows "(action_proj (action_proj a (vs1 - vs2)) vs3 = action_proj a vs3)"
proof -
have "∀f fa fb p.
action_proj (action_proj (action_proj p f) fb) fa = action_proj (action_proj p f) fb
∨ ¬ action_dom (fst p::('a, 'b) fmap) (snd p::(_, 'c) fmap) ∩ (f ∩ fb) ⊆ fa
"
by (metis (no_types) action_proj_idempot' proj_action_dom_eq_inter inf_assoc)
then have "∀f fa p.
action_proj (action_proj (p::('a, 'b) fmap × (_, 'c) fmap) f) fa
= action_proj p (f ∩ fa)
"
by (metis (no_types) inf.cobounded2 inf_commute subset_proj_absorb_1)
then show ?thesis
using assms
by (metis Diff_Int_distrib2 Diff_empty action_proj_idempot')
qed

lemma disj_proj_proj_eq_proj:
fixes PROB vs vs'
assumes "(vs ∩ vs' = {})"
shows "prob_proj (prob_proj PROB (prob_dom PROB - vs')) vs = prob_proj PROB vs"
proof -
{
fix a
assume P: "a ∈ PROB"
moreover have "action_dom (fst a) (snd a) ⊆ prob_dom PROB"
using P exec_as_proj_valid_2
by blast
ultimately have "action_proj (action_proj a (prob_dom PROB - vs')) vs = action_proj a vs"
using assms action_proj_disj_diff[of a "prob_dom PROB" vs' vs]
by blast
}
then show ?thesis
unfolding prob_proj_def
by (smt image_cong image_image)
qed

lemma n_replace_proj_le_n_as_2:
fixes a vs vs'
assumes "(vs ⊆ vs')" "(varset_action a vs')"
shows "(varset_action (action_proj a vs') vs ⟷ varset_action a vs)"
unfolding varset_action_def action_proj_def
using assms

― ‹NOTE type of `PROB` had to be fixed for use of `empty\_problem\_bound`.›
lemma empty_problem_proj_bound:
fixes PROB :: "'a problem"
shows "problem_plan_bound (prob_proj PROB {}) = 0"
proof -
― ‹TODO refactor?›
{
have "prob_proj {} {} = {}"
unfolding prob_proj_def action_proj_def
using image_empty
by simp
moreover {
assume P: "PROB ≠ {}"
have "∀a. (fmrestrict_set {} (fst a), fmrestrict_set {} (snd a)) = (fmempty, fmempty)"
using fmrestrict_set_null
by simp
then have "prob_proj PROB {} = {(fmempty, fmempty)}"
unfolding prob_proj_def action_proj_def
using P
by auto
}
ultimately consider
(i) "prob_proj PROB {} = {}"
| (ii) "prob_proj PROB {} = {(fmempty, fmempty)}"
by (cases "PROB = {}") force+
then have "prob_dom (prob_proj PROB {}) = {}"
unfolding prob_dom_def action_dom_def using fmdom'_empty
by (cases) force+
}
then show ?thesis
using empty_problem_bound[where PROB="prob_proj PROB {}"]
by blast
qed

lemma problem_plan_bound_works_proj:
fixes PROB :: "'a problem" and s as vs
assumes "finite PROB" "(s ∈ valid_states PROB)" "(as ∈ valid_plans PROB)" "(sat_precond_as s as)"
shows "(∃as'.
(exec_plan (fmrestrict_set vs s) as' = exec_plan (fmrestrict_set vs s) (as_proj as vs))
∧ (length as' ≤ problem_plan_bound (prob_proj PROB vs))
∧ (subseq as' (as_proj as vs))
∧ (sat_precond_as s as')
∧ (no_effectless_act as')
)"
proof -
{
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 "fmrestrict_set vs s ∈ valid_states (prob_proj PROB vs)"
using assms(2) graph_plan_not_eq_last_diff_paths
by auto
moreover have "as_proj as vs ∈ valid_plans (prob_proj PROB vs)"
using assms(3) valid_as_valid_as_proj
by blast
moreover have "finite (prob_proj PROB vs)"
unfolding prob_proj_def
using assms(1)
by simp
ultimately have "∃as'.
exec_plan (fmrestrict_set vs s) (as_proj as vs) = exec_plan (fmrestrict_set vs s) as'
∧ subseq as' (as_proj as vs) ∧ length as' ≤ problem_plan_bound (prob_proj PROB vs)
"
using problem_plan_bound_works[of "prob_proj PROB vs"
"fmrestrict_set vs s" "as_proj as vs"]
by blast
}
then obtain as' where
"exec_plan (fmrestrict_set vs s) (as_proj as vs) = exec_plan (fmrestrict_set vs s) as'"
"subseq as' (as_proj as vs) ∧ length as' ≤ problem_plan_bound (prob_proj PROB vs)"
by fast
moreover {
have "
exec_plan (fmrestrict_set vs s) as
= exec_plan (fmrestrict_set vs s) (rem_condless_act (fmrestrict_set vs s) [] as)
"
using rem_condless_valid_1[of "fmrestrict_set vs s" as]
by blast
then have "subseq (rem_condless_act (fmrestrict_set vs s) [] as') as'"
using rem_condless_valid_8 [of "fmrestrict_set vs s" as']
by blast
}
moreover have "length (rem_condless_act (fmrestrict_set vs s) [] as') ≤ length as'"
using rem_condless_valid_3[of "fmrestrict_set vs s"]
by fast
moreover have 4:
"sat_precond_as (fmrestrict_set vs s) (rem_condless_act (fmrestrict_set vs s) [] as')"
using rem_condless_valid_2[of "fmrestrict_set vs s" as']
by blast
moreover have "
exec_plan (fmrestrict_set vs s) (rem_condless_act (fmrestrict_set vs s) [] as')
= exec_plan (fmrestrict_set vs s)
(rem_effectless_act (rem_condless_act (fmrestrict_set vs s) [] as'))
"
using rem_effectless_works_1[of "fmrestrict_set vs s"
"rem_condless_act (fmrestrict_set vs s) [] as'"]
by blast
moreover {
have "
subseq (rem_effectless_act (rem_condless_act (fmrestrict_set vs s) [] as))
(rem_condless_act (fmrestrict_set vs s) [] as)
"
using rem_effectless_works_9[of
"(rem_condless_act (fmrestrict_set vs s) [] (as :: 'a action list))"]
by blast
then have "
length (rem_effectless_act (rem_condless_act (fmrestrict_set vs s) [] as'))
≤ length (rem_condless_act (fmrestrict_set vs s) [] as')
"
using rem_effectless_works_3[of
"(rem_condless_act (fmrestrict_set vs s) [] (as' :: 'a action list))"]
by simp
then have "
sat_precond_as (fmrestrict_set vs s)
(rem_effectless_act (rem_condless_act (fmrestrict_set vs s) [] as'))
"
using 4 rem_effectless_works_2[of "fmrestrict_set vs s"
"(rem_condless_act (fmrestrict_set vs s) [] as')"]
by blast
then have
"no_effectless_act (rem_effectless_act (rem_condless_act (fmrestrict_set vs s) [] as'))"
using rem_effectless_works_6[of "(rem_condless_act (fmrestrict_set vs s) [] (as' ::'a action list))"]
by simp
}
ultimately show ?thesis
using rem_effectless_works_13 rem_condless_valid_1 order_trans
no_effectless_proj sat_precond_drest_sat_precond subseq_order.order_trans
by (metis (no_types, lifting))
qed

― ‹TODO refactor into `Fmap\_Utils`.›
lemma action_proj_inter_i: "fmrestrict_set V (fmrestrict_set W f) = fmrestrict_set (V ∩ W) f"
unfolding fmfilter_alt_defs(4)
by simp

lemma action_proj_inter: "action_proj (action_proj a vs1) vs2 = action_proj a (vs1 ∩ vs2)"
proof -
have
"fmrestrict_set vs2 (fmrestrict_set vs1 (fst a)) = fmrestrict_set (vs1 ∩ vs2) (fst a)"
"fmrestrict_set vs2 (fmrestrict_set vs1 (snd a)) = fmrestrict_set (vs1 ∩ vs2) (snd a)"
using inf_commute action_proj_inter_i
by metis+
then show ?thesis
unfolding action_proj_def
by simp
qed

lemma prob_proj_inter: "prob_proj (prob_proj PROB vs1) vs2 = prob_proj PROB (vs1 ∩ vs2)"
unfolding prob_proj_def
using set_eq_iff image_iff action_proj_inter
supply[[smt_timeout=100]]
by (smt image_cong image_image)

subsection "Snapshotting"

text ‹ A snapshot is an abstraction concept of the system in which the assignment of a set of
variables is fixed and actions whose preconditions or effects violate the fixed assignments are
eliminated. [Abdulaziz et al., p.28]

Formally this notion is build on the definition of agreement of states (`agree`), which
states that variables `v`, `v'`in the shared domain of two states must be assigned to the same
value. A snapshot w.r.t to a state `s` is then defined as the set of actions of a problem where the
precondition and the effect agree. [Abdulaziz et al., Definition 16, HOL4 Definition 16, p.28] ›

― ‹NOTE  name shortened.›
definition agree where
"agree s1 s2 ≡ (∀v. (v ∈ fmdom' s1) ∧ (v ∈ fmdom' s2) ⟶ (fmlookup s1 v = fmlookup s2 v))"

lemma state_succ_fixpoint_if:
fixes a s PROB
assumes "a ∈ PROB" "(s ∈ valid_states PROB)" "fst a ⊆⇩f s" "agree (snd a) s"
shows "state_succ s a = s"
proof -
{
have "fmdom' (snd a) ⊆ fmdom' s"
using assms(1, 2) FDOM_eff_subset_FDOM_valid_states_pair
by blast
moreover have "∀x. x ∈ fmdom' (snd a) ⟶ fmlookup (snd a) x = fmlookup s x"
using assms(4) calculation(1) agree_def subsetCE
by metis
moreover have "s ++⇩f snd a = s"
using calculation(2)
by (metis fmap_ext fmdom'_notD fmdom_notI fmlookup_add)
}
then show ?thesis
by metis
qed

lemma agree_state_succ_idempot:
assumes "(a ∈ PROB)" "(s ∈ valid_states PROB)" "(agree (snd a) s)"
shows "(state_succ s a = s)"
proof (cases "fst a ⊆⇩f s")
case True
then show ?thesis
using assms state_succ_fixpoint_if
by blast
next
case False
then show ?thesis
by simp
qed

― ‹TODO refactor into `Fmap\_Utils`.›
lemma fmdom'_fmrestrict_set:
fixes X f
shows "fmdom' (fmrestrict_set X f) = X ∩ (fmdom' f)"
unfolding fmdom'_alt_def fmfilter_alt_defs(4)
by auto

― ‹TODO refactor into 'Fmap\_Utils'.›
fixes X f g
shows "fmdom' (fmrestrict_set X (f ++⇩f g)) = X ∩ (fmdom' f ∪ fmdom' g)"
proof -
have "fmrestrict_set X (f ++⇩f g) = fmrestrict_set X f ++⇩f fmrestrict_set X g"
by fast
then show ?thesis
by metis
qed

― ‹TODO refactor into 'Fmap\_Utils'.›
lemma fmrestrict_agree:
fixes X x f g
assumes "agree (fmrestrict_set X f) (fmrestrict_set X g)" "x ∈ X ∩ fmdom' f ∩ fmdom' g"
shows "fmlookup (fmrestrict_set X f) x = fmlookup (fmrestrict_set X g) x"
proof -
{
fix v
assume "v ∈ X ∩ fmdom' f ∩ fmdom' g"
then have "v ∈ fmdom' (fmrestrict_set X f) ∧ v ∈ fmdom' (fmrestrict_set X g)"
using fmdom'_fmrestrict_set
by force
then have "fmlookup (fmrestrict_set X f) v = fmlookup (fmrestrict_set X g) v"
using assms(1)
unfolding agree_def
by blast
}
then show ?thesis
using assms
by blast
qed

lemma agree_restrict_state_succ_idempot:
assumes "(a ∈ PROB)" "(s ∈ valid_states PROB)"
"(agree (fmrestrict_set vs (snd a)) (fmrestrict_set vs s))"
shows "(fmrestrict_set vs (state_succ s a) = fmrestrict_set vs s)"
proof (cases "fst a ⊆⇩f s")
case True
then have "state_succ s a = s ++⇩f snd a"
by simp
{
fix v
have "fmlookup (fmrestrict_set vs (s ++⇩f snd a)) v = fmlookup (fmrestrict_set vs s) v"
proof (cases "v ∈ fmdom' (snd a)")
case True
then have 1: "fmdom' (fmrestrict_set vs (s ++⇩f snd a)) = vs ∩ (fmdom' s ∪ fmdom' (snd a))"
by metis
then have 2: "fmdom' (fmrestrict_set vs (snd a)) = vs ∩ fmdom' (snd a)"
using fmdom'_fmrestrict_set
by metis
then show ?thesis
using 1 2
proof (cases "v ∈ vs")
case true: True
then show ?thesis
proof (cases "v ∈ (fmdom' s ∩ fmdom' (snd a))")
case True
then have "v ∈ vs ∩ fmdom' s ∩ fmdom' (snd a)"
using true
by blast
then have "fmlookup (fmrestrict_set vs (snd a)) v = fmlookup (fmrestrict_set vs s) v"
using assms(3) fmrestrict_agree
by fast
then show ?thesis
by fastforce
next
case False
then have "fmdom' (snd a) ⊆ fmdom' s"
using assms(1, 2) FDOM_eff_subset_FDOM_valid_states_pair
by metis
then have "v ∉ fmdom' (snd a)"
using true False
by blast
then show ?thesis
by fastforce
qed
qed auto
qed fastforce
}
then show ?thesis
using fmap_ext
by metis
next
case False
then show ?thesis
unfolding state_succ_def
by simp
qed

lemma agree_exec_idempot:
assumes "(as ∈ valid_plans PROB)" "(s ∈ valid_states PROB)"
"(∀a. ListMem a as ⟶ agree (snd a) s)"
shows "(exec_plan s as = s)"
using assms
proof (induction as arbitrary: PROB s)
case (Cons a as)
then have 1: "a ∈ PROB"
by fast
then have 2: "as ∈ valid_plans PROB"
using Cons.prems(1) valid_plan_valid_tail
by fast
then have 3: "∀a. ListMem a as ⟶ agree (snd a) s"
using Cons.prems(3) ListMem.simps
by metis
then have "ListMem a (a # as)"
using elem
by fast
then have "agree (snd a) s"
using Cons.prems(3)
by blast
then have 4: "state_succ s a = s"
using Cons.prems(1, 2) 1 agree_state_succ_idempot
by blast
then have "exec_plan s as = s"
using Cons.IH Cons.prems(2) 2 3
by blast
then show ?case
using 4
by simp
qed simp

lemma agree_restrict_exec_idempot:
fixes s s'
assumes "(as ∈ valid_plans PROB)" "(s' ∈ valid_states PROB)" "(s ∈ valid_states PROB)"
"(∀a. ListMem a as ⟶ agree (fmrestrict_set vs (snd a)) (fmrestrict_set vs s))"
"(fmrestrict_set vs s' = fmrestrict_set vs s)"
shows  "(fmrestrict_set vs (exec_plan s' as) = fmrestrict_set vs s)"
using assms
proof (induction as arbitrary: PROB s s' vs)
case (Cons a as)
have 1: "as ∈ valid_plans PROB"
using Cons.prems(1) valid_plan_valid_tail
by fast
then have 2: "∀a. ListMem a as ⟶ agree (fmrestrict_set vs (snd a)) (fmrestrict_set vs s)"
using Cons.prems(4) ListMem.simps
by metis
then have 3: "a ∈ PROB"
by metis
moreover
{
have "ListMem a (a # as)"
using elem
by fast
then have "agree (fmrestrict_set vs (snd a)) (fmrestrict_set vs s)"
using Cons.prems(4) calculation(1)
by blast
then  have "agree (fmrestrict_set vs (snd a)) (fmrestrict_set vs s')"
using Cons.prems(5)
by simp
}
ultimately show ?case
using assms
proof (cases "fst a ⊆⇩f s'")
case True
{
have a: "s' ∈ valid_states PROB"
using Cons.prems(2)
by simp
moreover have "state_succ s' a ∈ valid_states PROB"
using 3 a lemma_1_i
by blast
moreover have
" ∀a. ListMem a as ⟶ agree (fmrestrict_set vs (snd a)) (fmrestrict_set vs s)"
using 2
by blast
moreover {
have "ListMem a (a # as)"
using elem
by fast
then have "agree (fmrestrict_set vs (snd a)) (fmrestrict_set vs s)"
using Cons.prems(4) calculation(1)
by blast
then have "fmrestrict_set vs (state_succ s' a) = fmrestrict_set vs s"
using Cons.prems(5) 3 a agree_restrict_state_succ_idempot
by metis
}
ultimately have "fmrestrict_set vs (exec_plan (state_succ s' a) as) = fmrestrict_set vs s"
using assms(3) 1 Cons.IH[where s'="state_succ s' a"]
by auto
}
then show ?thesis
by simp
next case False
moreover have "exec_plan s' (a # as) = exec_plan s' as"
using False
ultimately show ?thesis
using Cons.IH Cons.prems(2, 3, 5) 1 2
by presburger
qed
qed simp

lemma agree_restrict_exec_idempot_pair:
fixes s s'
assumes "(as ∈ valid_plans PROB)" "(s' ∈ valid_states PROB)" "(s ∈ valid_states PROB)"
"(∀p e. ListMem (p, e) as ⟶ agree (fmrestrict_set vs e) (fmrestrict_set vs s))"
"(fmrestrict_set vs s' = fmrestrict_set vs s)"
shows "(fmrestrict_set vs (exec_plan s' as) = fmrestrict_set vs s)"
using assms agree_restrict_exec_idempot
by fastforce

lemma agree_comm: "agree x x' = agree x' x"
unfolding agree_def
by fastforce

lemma restricted_agree_imp_agree:
assumes "(fmdom' s2 ⊆ vs)" "(agree (fmrestrict_set vs s1) s2)"
shows "(agree s1 s2)"
using assms contra_subsetD fmlookup_restrict_set Int_iff fmdom'_fmrestrict_set
unfolding agree_def
by metis

lemma agree_imp_submap:
assumes "f1 ⊆⇩f f2"
shows "agree f1 f2"
using assms
unfolding agree_def

lemma agree_FUNION:
assumes "(agree fm fm1)" "(agree fm fm2)"
shows "(agree fm (fm1 ++ fm2))"
using assms

lemma agree_fm_list_union:
fixes fm
assumes "(∀fm'. ListMem fm' fmList ⟶ agree fm fm')"
shows "(agree fm (foldr fmap_add_ltr fmList fmempty))"
using assms proof (induction "fmList" arbitrary: fm)
case Nil
then have "foldr fmap_add_ltr [] fmempty = fmempty"
using Nil
by simp
then show ?case
unfolding agree_def
by auto
next
case (Cons a fmList)
then have "∀fm'. ListMem fm' fmList ⟶ agree fm fm'"
using Cons.prems insert
by fast
then have 1: "agree fm (foldr fmap_add_ltr fmList fmempty)"
using Cons.IH
by blast
then have "agree fm a"
using Cons.prems elem
by fast
then have "agree fm (a ++ foldr fmap_add_ltr fmList fmempty)"
using 1 agree_FUNION
by blast
then show ?case
by simp
qed

lemma DRESTRICT_EQ_AGREE:
assumes "(fmdom' s2 ⊆ vs2)" "(fmdom' s1 ⊆ vs1)"
shows "((fmrestrict_set vs2 s1 = fmrestrict_set vs1 s2) ⟶ agree s1 s2)"
using assms fmdom'_restrict_set restricted_agree_imp_agree
by (metis agree_def)

lemma  SUBMAPS_AGREE: "(s1 ⊆⇩f s) ∧ (s2 ⊆⇩f s) ⟹ (agree s1 s2)"
unfolding agree_def
by (metis as_needed_asses_submap_exec_ii)

― ‹NOTE name shortened.›
definition snapshot where
"snapshot PROB s = {a | a. a ∈ PROB ∧ agree (fst a) s ∧ agree (snd a) s}"

lemma snapshot_pair: "snapshot PROB s = {(p, e). (p, e) ∈ PROB ∧ agree p s ∧ agree e s}"
unfolding snapshot_def
by fastforce

lemma action_agree_valid_in_snapshot:
assumes "(a ∈ PROB)" "(agree (fst a) s)" "(agree (snd a) s)"
shows "(a ∈ snapshot PROB s)"
unfolding snapshot_def
using assms
by blast

lemma as_mem_agree_valid_in_snapshot:
assumes "(∀a. ListMem a as ⟶ agree (fst a) s ∧ agree (snd a) s)" "(as ∈ valid_plans PROB)"
shows "(as ∈ valid_plans (snapshot PROB s))"
using assms
proof (induction as)
case Nil
then show ?case
using empty_plan_is_valid
by blast
next
case (Cons a as)
{
have "∀a. ListMem a as ⟶ agree (fst a) s ∧ agree (snd a) s"
using Cons.prems(1) insert
by fast
moreover have "(as ∈ valid_plans PROB)"
using Cons.prems(2) valid_plan_valid_tail
by fast
ultimately have "set as ⊆ snapshot PROB s"
using Cons.IH valid_plans_def
by fast
}
note 1 = this
{
have a: "a ∈ PROB"
by metis
then have "ListMem a (a # as)"
using elem
by fast
then have "agree (fst a) s ∧ agree (snd a) s"
using Cons.prems(1)
by blast
then have "a ∈ snapshot PROB s"
using a snapshot_def
by auto
}
then have "set (a # as) ⊆ snapshot PROB s"
using 1 set_simps(2)
by simp
then show ?case using valid_plans_def
by blast
qed

lemma fmrestrict_agree_monotonous:
fixes f g X
assumes "agree f g"
shows "agree (fmrestrict_set X f) (fmrestrict_set X g)"
proof -
let ?F="fmdom' (fmrestrict_set X f)"
let ?G="fmdom' (fmrestrict_set X g)"
have 1: "?F = X ∩ fmdom' f" "?G = X ∩ fmdom' g"
using fmdom'_fmrestrict_set
by metis+
{
fix v
assume "v ∈ ?F" "v ∈ ?G"
then have "v ∈ fmdom' f" "v ∈ fmdom' g"
using 1
by blast+
then have "fmlookup f v = fmlookup g v"
using assms
unfolding agree_def
by blast
then have "fmlookup (fmrestrict_set X f) v = fmlookup (fmrestrict_set X g) v"
unfolding fmlookup_restrict_set
by argo
}
then show ?thesis
using assms
unfolding agree_def
by blast
qed

― ‹TODO remove if not used.›
lemma SUBMAP_FUNION_DRESTRICT_i:
fixes v vsa vsb f g
assumes "v ∈ vsa"
shows "
fmlookup (fmrestrict_set ((vsa ∪ vsb) ∩ vs) f) v
= fmlookup (fmrestrict_set (vsa ∩ vs) f) v
"
unfolding fmlookup_restrict_set
using assms
by auto

lemma SUBMAP_FUNION_DRESTRICT':
assumes "(agree fma fmb)" "(vsa ⊆ fmdom' fma)" "(vsb ⊆ fmdom' fmb)"
"(fmrestrict_set vsa fm  = fmrestrict_set (vsa ∩ vs) fma)"
"(fmrestrict_set vsb fm = fmrestrict_set (vsb ∩ vs) fmb)"
shows "(fmrestrict_set (vsa ∪ vsb) fm = fmrestrict_set ((vsa ∪ vsb) ∩ vs) (fma ++ fmb))"
proof -
let ?f="fmrestrict_set (vsa ∪ vsb) fm"
let ?g="fmrestrict_set ((vsa ∪ vsb) ∩ vs) (fma ++ fmb)"
have 1: "?g = fmrestrict_set ((vsa ∪ vsb) ∩ vs) fmb ++⇩f fmrestrict_set ((vsa ∪ vsb) ∩ vs) fma"
by simp
have 2: "agree (fmrestrict_set ((vsa ∪ vsb) ∩ vs) fma) (fmrestrict_set ((vsa ∪ vsb) ∩ vs) fmb)"
using assms(1) fmrestrict_agree_monotonous
by blast
have 3:
"fmdom' (fmrestrict_set ((vsa ∪ vsb) ∩ vs) fma) = ((vsa ∪ vsb) ∩ vs) ∩ fmdom' fma"
"fmdom' (fmrestrict_set ((vsa ∪ vsb) ∩ vs) fmb) = ((vsa ∪ vsb) ∩ vs) ∩ fmdom' fmb"
using fmdom'_fmrestrict_set
by metis+
{
fix v
have "fmlookup ?f v = fmlookup ?g v"
proof (cases "v ∈ ((vsa ∪ vsb) ∩ vs)")
case True
― ‹TODO unwrap smt proof.›
then show ?thesis
using assms(1, 2, 3, 4, 5) 1
by (smt (verit) IntD1 SUBMAP_FUNION_DRESTRICT_i UnE agree_def domIff fmdom'.rep_eq fmdom'_alt_def
subset_iff sup_commute)
next
case False
then show ?thesis
proof -
have "v ∉ vsa ∪ vsb ∨ v ∉ vs"
using False
by blast
then have "fmlookup (fmrestrict_set (vsa ∪ vsb) fm) v = None"
using assms(4, 5)
by (metis Int_iff Un_iff fmlookup_restrict_set)
then show ?thesis
using False
by auto
qed
qed
}
then show ?thesis
using 1 fmap_ext
by blast
qed

lemma UNION_FUNION_DRESTRICT_SUBMAP:
assumes "(vs1 ⊆ fmdom' fma)" "(vs2 ⊆ fmdom' fmb)" "(agree fma fmb)"
"(fmrestrict_set vs1 fma ⊆⇩f s)" "(fmrestrict_set vs2 fmb ⊆⇩f s)"
shows "(fmrestrict_set (vs1 ∪ vs2) (fma ++ fmb) ⊆⇩f s)"
proof -
{
let ?f="fmrestrict_set (vs1 ∪ vs2) (fma ++ fmb)"
fix v
assume P: "v ∈ fmdom' ?f"
{
have "v ∈ (vs1 ∪ vs2) ∩ (fmdom' fma ∪ fmdom' fmb)"
using P
by force
then have "v ∈ vs1 ∪ vs2" "v ∈ fmdom' fma ∪ fmdom' fmb"
by fast+
}
note 1 = this
then have 2: "fmlookup ?f v = fmlookup (fmb ++⇩f fma) v"
by argo
then consider
(i) "v ∈ vs1"
| (ii) "v ∈ vs2"
| (iii) "¬v∈ vs1 ∧ ¬v∈vs2"
by blast
then have "fmlookup ?f v = fmlookup s v"
proof (cases)
case i
then have "v ∈ fmdom' fma"
using assms(1)
by blast
then have "fmlookup ?f v = fmlookup fma v"
also have "… = fmlookup (fmrestrict_set vs1 fma) v"
unfolding fmlookup_restrict_set
using i
by simp
finally show ?thesis
using assms(4)
by (metis (mono_tags, lifting) P domIff fmdom'_notI fmsubset.rep_eq map_le_def)
next
― ‹TODO unwrap smt proof.›
case ii
then show ?thesis
using assms(2, 3, 5) 2 P
by (smt SUBMAP_FUNION_DRESTRICT_i agree_def
```