# Theory Finite_Map_Multiset

```(*
File:         Finite_Map_Multiset.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
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›

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)›

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
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''›

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)›

lemma fmrestrict_set_insert_notin_dom_m[simp]:
‹xa  ∉# dom_m N ⟹
fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›

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```