Theory Finite_Map_Multiset
theory Finite_Map_Multiset
imports
"HOL-Library.Finite_Map"
Nested_Multisets_Ordinals.Duplicate_Free_Multiset
begin
notation image_mset (infixr ‹`#› 90)
section ‹Finite maps and multisets›
subsection ‹Finite sets and multisets›
abbreviation mset_fset :: ‹'a fset ⇒ 'a multiset› where
‹mset_fset N ≡ mset_set (fset N)›
definition fset_mset :: ‹'a multiset ⇒ 'a fset› where
‹fset_mset N ≡ Abs_fset (set_mset N)›
lemma fset_mset_mset_fset: ‹fset_mset (mset_fset N) = N›
by (auto simp: fset.fset_inverse fset_mset_def)
lemma mset_fset_fset_mset[simp]:
‹mset_fset (fset_mset N) = remdups_mset N›
by (auto simp: fset.fset_inverse fset_mset_def Abs_fset_inverse remdups_mset_def)
lemma in_mset_fset_fmember[simp]: ‹x ∈# mset_fset N ⟷ x |∈| N›
by simp
lemma in_fset_mset_mset[simp]: ‹x |∈| fset_mset N ⟷ x ∈# N›
by (simp add: fset_mset_def Abs_fset_inverse)
subsection ‹Finite map and multisets›
text ‹Roughly the same as \<^term>‹ran› and \<^term>‹dom›, but with duplication in the content (unlike their
finite sets counterpart) while still working on finite domains (unlike a function mapping).
Remark that \<^term>‹dom_m› (the keys) does not contain duplicates, but we keep for symmetry (and for
easier use of multiset operators as in the definition of \<^term>‹ran_m›).
›
definition dom_m where
‹dom_m N = mset_fset (fmdom N)›
definition ran_m where
‹ran_m N = the `# fmlookup N `# dom_m N›
lemma dom_m_fmdrop[simp]: ‹dom_m (fmdrop C N) = remove1_mset C (dom_m N)›
unfolding dom_m_def
by (cases ‹C |∈| fmdom N›)
(auto simp: mset_set.remove)
lemma dom_m_fmdrop_All: ‹dom_m (fmdrop C N) = removeAll_mset C (dom_m N)›
unfolding dom_m_def
by (cases ‹C |∈| fmdom N›)
(auto simp: mset_set.remove)
lemma dom_m_fmupd[simp]: ‹dom_m (fmupd k C N) = add_mset k (remove1_mset k (dom_m N))›
unfolding dom_m_def
by (cases ‹k |∈| fmdom N›)
(auto simp: mset_set.remove mset_set.insert_remove)
lemma distinct_mset_dom: ‹distinct_mset (dom_m N)›
by (simp add: distinct_mset_mset_set dom_m_def)
lemma in_dom_m_lookup_iff: ‹C ∈# dom_m N' ⟷ fmlookup N' C ≠ None›
by (auto simp: dom_m_def fmdom.rep_eq fmlookup_dom'_iff)
lemma in_dom_in_ran_m[simp]: ‹i ∈# dom_m N ⟹ the (fmlookup N i) ∈# ran_m N›
by (auto simp: ran_m_def)
lemma fmupd_same[simp]:
‹x1 ∈# dom_m x1aa ⟹ fmupd x1 (the (fmlookup x1aa x1)) x1aa = x1aa›
by (metis fmap_ext fmupd_lookup in_dom_m_lookup_iff option.collapse)
lemma ran_m_fmempty[simp]: ‹ran_m fmempty = {#}› and
dom_m_fmempty[simp]: ‹dom_m fmempty = {#}›
by (auto simp: ran_m_def dom_m_def)
lemma fmrestrict_set_fmupd:
‹a ∈ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmupd a C (fmrestrict_set xs N)›
‹a ∉ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmrestrict_set xs N›
by (auto simp: fmfilter_alt_defs)
lemma fset_fmdom_fmrestrict_set:
‹fset (fmdom (fmrestrict_set xs N)) = fset (fmdom N) ∩ xs›
by (auto simp: fmfilter_alt_defs)
lemma dom_m_fmrestrict_set: ‹dom_m (fmrestrict_set (set xs) N) = mset xs ∩# dom_m N›
using fset_fmdom_fmrestrict_set[of ‹set xs› N] distinct_mset_dom[of N]
distinct_mset_inter_remdups_mset[of ‹mset_fset (fmdom N)› ‹mset xs›]
by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
remdups_mset_def)
lemma dom_m_fmrestrict_set': ‹dom_m (fmrestrict_set xs N) = mset_set (xs ∩ set_mset (dom_m N))›
using fset_fmdom_fmrestrict_set[of ‹xs› N] distinct_mset_dom[of N]
by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
remdups_mset_def)
lemma indom_mI: ‹fmlookup m x = Some y ⟹ x ∈# dom_m m›
by (drule fmdomI) (auto simp: dom_m_def)
lemma fmupd_fmdrop_id:
assumes ‹k |∈| fmdom N'›
shows ‹fmupd k (the (fmlookup N' k)) (fmdrop k N') = N'›
proof -
have [simp]: ‹map_upd k (the (fmlookup N' k))
(λx. if x ≠ k then fmlookup N' x else None) =
map_upd k (the (fmlookup N' k))
(fmlookup N')›
by (auto intro!: ext simp: map_upd_def)
have [simp]: ‹map_upd k (the (fmlookup N' k)) (fmlookup N') = fmlookup N'›
using assms
by (auto intro!: ext simp: map_upd_def)
have [simp]: ‹finite (dom (λx. if x = k then None else fmlookup N' x))›
by (subst dom_if) auto
show ?thesis
apply (auto simp: fmupd_def fmupd.abs_eq[symmetric])
unfolding fmlookup_drop
apply (simp add: fmlookup_inverse)
done
qed
lemma fm_member_split: ‹k |∈| fmdom N' ⟹ ∃N'' v. N' = fmupd k v N'' ∧ the (fmlookup N' k) = v ∧
k |∉| fmdom N''›
by (rule exI[of _ ‹fmdrop k N'›])
(auto simp: fmupd_fmdrop_id)
lemma ‹fmdrop k (fmupd k va N'') = fmdrop k N''›
by (simp add: fmap_ext)
lemma fmap_ext_fmdom:
‹(fmdom N = fmdom N') ⟹ (⋀ x. x |∈| fmdom N ⟹ fmlookup N x = fmlookup N' x) ⟹
N = N'›
by (rule fmap_ext)
(case_tac ‹x |∈| fmdom N›, auto simp: fmdom_notD)
lemma fmrestrict_set_insert_in:
‹xa ∈ fset (fmdom N) ⟹
fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
apply (rule fmap_ext_fmdom)
apply (auto simp: fset_fmdom_fmrestrict_set; fail)[]
apply (auto simp: fmlookup_dom_iff; fail)
done
lemma fmrestrict_set_insert_notin:
‹xa ∉ fset (fmdom N) ⟹
fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
by (rule fmap_ext_fmdom)
(auto simp: fset_fmdom_fmrestrict_set)
lemma fmrestrict_set_insert_in_dom_m[simp]:
‹xa ∈# dom_m N ⟹
fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
by (simp add: fmrestrict_set_insert_in dom_m_def)
lemma fmrestrict_set_insert_notin_dom_m[simp]:
‹xa ∉# dom_m N ⟹
fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
by (simp add: fmrestrict_set_insert_notin dom_m_def)
lemma fmlookup_restrict_set_id: ‹fset (fmdom N) ⊆ A ⟹ fmrestrict_set A N = N›
by (metis fmap_ext fmdom'_alt_def fmdom'_notD fmlookup_restrict_set subset_iff)
lemma fmlookup_restrict_set_id': ‹set_mset (dom_m N) ⊆ A ⟹ fmrestrict_set A N = N›
by (rule fmlookup_restrict_set_id)
(auto simp: dom_m_def)
lemma ran_m_mapsto_upd:
assumes
NC: ‹C ∈# dom_m N›
shows ‹ran_m (fmupd C C' N) = add_mset C' (remove1_mset (the (fmlookup N C)) (ran_m N))›
proof -
define N' where
‹N' = fmdrop C N›
have N_N': ‹dom_m N = add_mset C (dom_m N')›
using NC unfolding N'_def by auto
have ‹C ∉# dom_m N'›
using NC distinct_mset_dom[of N] unfolding N_N' by auto
then show ?thesis
by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong)
qed
lemma ran_m_mapsto_upd_notin:
assumes NC: ‹C ∉# dom_m N›
shows ‹ran_m (fmupd C C' N) = add_mset C' (ran_m N)›
using NC
by (auto simp: ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong split: if_splits)
lemma image_mset_If_eq_notin:
‹C ∉# A ⟹ {#f (if x = C then a x else b x). x ∈# A#} = {# f(b x). x ∈# A #}›
by (induction A) auto
lemma filter_mset_cong2:
"(⋀x. x ∈# M ⟹ f x = g x) ⟹ M = N ⟹ filter_mset f M = filter_mset g N"
by (hypsubst, rule filter_mset_cong, simp)
lemma ran_m_fmdrop:
‹C ∈# dom_m N ⟹ ran_m (fmdrop C N) = remove1_mset (the (fmlookup N C)) (ran_m N)›
using distinct_mset_dom[of N]
by (cases ‹fmlookup N C›)
(auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
lemma ran_m_fmdrop_notin:
‹C ∉# dom_m N ⟹ ran_m (fmdrop C N) = ran_m N›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
lemma ran_m_fmdrop_If:
‹ran_m (fmdrop C N) = (if C ∈# dom_m N then remove1_mset (the (fmlookup N C)) (ran_m N) else ran_m N)›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)
lemma dom_m_empty_iff[iff]:
‹dom_m NU = {#} ⟷ NU = fmempty›
by (cases NU) (auto simp: dom_m_def mset_set.insert_remove)
end