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.› hide_const (open) Map.map_add no_notation Map.map_add (infixl "++" 100) ― ‹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'')" by (metis calculation disjnt_iff fmap_add_ltr_def fmdom'_notD fmdom_notI fmlookup_add) 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") apply(auto simp add: "1") 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 subgoal by (simp add: fmdom'_notD) 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 by (simp add: map_le_def) } 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) by (metis fmap_add_ltr_def fmap_ext fmdom'_notD fmdom_notI fmlookup_add) then have b: "v ∈ vs" using assms(1) by blast moreover { have "fmdom' (fmrestrict_set vs (f1 ++ f2)) = vs ∩ fmdom' (f1 ++ f2)" by (simp add: fmdom'_alt_def fmfilter_alt_defs(4)) 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)" by (auto simp add: fmdom'_restrict_set_precise) end