# Theory Finite_Map_Multiset

(*
File:         Finite_Map_Multiset.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory Finite_Map_Multiset
imports

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]:

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 termran and termdom, but with duplication in the content (unlike their
finite sets counterpart) while still working on finite domains (unlike a function mapping).
Remark that termdom_m (the keys) does not contain duplicates, but we keep for symmetry (and for
easier use of multiset operators as in the definition of termran_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]:  and
dom_m_fmempty[simp]:
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