# Theory FmapUtils

```theory FmapUtils
imports "HOL-Library.Finite_Map" FactoredSystemLib
begin

― ‹TODO
A lemma 'fmrestrict\_set\_twice\_eq'
'fmrestrict\_set ?vs (fmrestrict\_set ?vs ?f) = fmrestrict\_set ?vs ?f'
to replace the recurring proofs steps using 'by (simp add: fmfilter\_alt\_defs(4))' would make sense.›

― ‹NOTE hide the '++' operator from 'Map' to prevent warnings.›

― ‹TODO more explicit proof.›
lemma IN_FDOM_DRESTRICT_DIFF:
fixes vs v f
assumes "¬(v ∈ vs)" "fmdom' f ⊆ fdom" "v ∈ fmdom' f"
shows "v ∈ fmdom' (fmrestrict_set (fdom - vs) f)"
using assms
by (metis DiffI Int_def Int_iff Set.filter_def fmdom'_filter fmfilter_alt_defs(4) inf.order_iff)

lemma disj_dom_drest_fupdate_eq: "
disjnt (fmdom' x) vs ⟹ (fmrestrict_set vs s = fmrestrict_set vs (x ++ s))
"
proof -
fix vs s x
assume P: "disjnt (fmdom' x) vs"
moreover have 1: "∀x''. (x'' ∈ vs) ⟶ (fmlookup (x ++ s) x'' = fmlookup s  x'')"
moreover
{
fix x''
have "fmlookup (fmrestrict_set vs s) x'' = fmlookup (fmrestrict_set vs (x ++ s)) x''"
apply(cases "x'' ∉ fmdom' x")
apply(cases "x'' ∉ vs")
done
}
ultimately show "(fmrestrict_set vs s = fmrestrict_set vs (x ++ s))"
using fmap_ext by blast
qed

― ‹TODO refactor into 'FmapUtils.thy'.›
lemma graph_plan_card_state_set:
fixes PROB vs
assumes "finite vs"
shows "card (fmdom' (fmrestrict_set vs s)) ≤ card vs"
proof -
let ?vs' = "fmdom' (fmrestrict_set vs s)"
have "?vs' ⊆ vs"
using fmdom'_restrict_set
by metis
moreover have "card ?vs' ≤ card vs"
using assms calculation card_mono
by blast
ultimately show ?thesis by blast
qed

lemma exec_drest_5:
fixes x vs
assumes "fmdom' x ⊆ vs"
shows "(fmrestrict_set vs x = x)"
proof -
― ‹TODO refactor and make into ISAR proof.›
{
fix v
have "fmlookup (fmrestrict_set vs x) v = fmlookup x v"
apply(cases "v ∈ fmdom' x")
subgoal using assms by auto
done
then have "fmlookup (fmrestrict_set vs x) v = fmlookup x v"
by fast
}
moreover have "fmlookup (fmrestrict_set vs x) = fmlookup x"
using calculation fmap_ext
by auto
ultimately show ?thesis
using fmlookup_inject
by blast
qed

lemma graph_plan_lemma_5:
fixes s s' vs
assumes "(fmrestrict_set (fmdom' s - vs) s = fmrestrict_set (fmdom' s' - vs) s')"
"(fmrestrict_set vs s = fmrestrict_set vs s')"
shows "(s = s')"
proof -
have "∀x. fmlookup s x = fmlookup s' x"
using assms(1, 2) fmdom'_notD fminusI fmlookup_restrict_set Diff_iff
by metis
then show ?thesis using fmap_ext
by blast
qed

lemma drest_smap_drest_smap_drest:
fixes x s vs
shows "fmrestrict_set vs x ⊆⇩f s ⟷ fmrestrict_set vs x ⊆⇩f fmrestrict_set vs s"
proof -
― ‹TODO this could be refactored into standalone lemma since it's very common in proofs.›
have 1: "fmlookup (fmrestrict_set vs s) ⊆⇩m fmlookup s"
by (metis fmdom'.rep_eq fmdom'_notI fmlookup_restrict_set map_le_def)
moreover
{
assume P1: "fmrestrict_set vs x ⊆⇩f s"
moreover have 2: "fmlookup (fmrestrict_set vs x) ⊆⇩m fmlookup s"
using P1 fmsubset.rep_eq by blast
{
fix v
assume "v ∈ fmdom' (fmrestrict_set vs x)"
then have "fmlookup (fmrestrict_set vs x) v = fmlookup (fmrestrict_set vs s) v"
by (metis (full_types) "2" domIff fmdom'_notI fmlookup_restrict_set map_le_def)
}
ultimately have "fmrestrict_set vs x ⊆⇩f fmrestrict_set vs s"
unfolding fmsubset.rep_eq
}
moreover
{
assume P2: "fmrestrict_set vs x ⊆⇩f fmrestrict_set vs s"
moreover have "fmrestrict_set vs s ⊆⇩f s"
using 1 fmsubset.rep_eq
by blast
ultimately have "fmrestrict_set vs x ⊆⇩f s"
using fmsubset.rep_eq map_le_trans
by blast
}
ultimately show ?thesis by blast
qed

lemma sat_precond_as_proj_1:
fixes s s' vs x
assumes "fmrestrict_set vs s = fmrestrict_set vs s'"
shows "fmrestrict_set vs x ⊆⇩f s ⟷ fmrestrict_set vs x ⊆⇩f s'"
using assms drest_smap_drest_smap_drest
by metis

lemma sat_precond_as_proj_4:
fixes fm1 fm2 vs
assumes "fm2 ⊆⇩f fm1"
shows "(fmrestrict_set vs fm2 ⊆⇩f fm1)"
using assms fmpred_restrict_set fmsubset_alt_def
by metis

lemma sublist_as_proj_eq_as_1:
fixes x s vs
assumes "(x ⊆⇩f fmrestrict_set vs s)"
shows "(x ⊆⇩f s)"
using assms
by (meson fmsubset.rep_eq fmsubset_alt_def fmsubset_pred drest_smap_drest_smap_drest map_le_refl)

lemma limited_dom_neq_restricted_neq:
assumes "fmdom' f1 ⊆ vs" "f1 ++ f2 ≠ f2"
shows "fmrestrict_set vs (f1 ++ f2) ≠ fmrestrict_set vs f2"
proof -
{
assume C: "fmrestrict_set vs (f1 ++ f2) = fmrestrict_set vs f2"
then have "∀x ∈ fmdom' (fmrestrict_set vs (f1 ++ f2)).
fmlookup (fmrestrict_set vs (f1 ++ f2)) x
= fmlookup (fmrestrict_set vs f2) x"
by simp
obtain v where a: "v ∈ fmdom' f1" "fmlookup (f1 ++ f2) v ≠ fmlookup f2 v"
using assms(2)
then have b: "v ∈ vs"
using assms(1)
by blast
moreover {
have "fmdom' (fmrestrict_set vs (f1 ++ f2)) = vs ∩ fmdom' (f1 ++ f2)"
then have "v ∈ fmdom' (fmrestrict_set vs (f1 ++ f2))"
using C a b
by fastforce
}
then have False
by (metis C a(2) calculation fmlookup_restrict_set)
}
then show ?thesis
by auto
qed

lemma fmlookup_fmrestrict_set_dom: "⋀vs s. dom (fmlookup (fmrestrict_set vs s)) = vs ∩ (fmdom' s)"