Theory Finite-Map-Extras.Finite_Map_Extras
section ‹ Extra Features for Finite Maps ›
theory Finite_Map_Extras
imports "HOL-Library.Finite_Map"
begin
text ‹ Extra lemmas and syntactic sugar for ‹fmap› ›
notation fmlookup (infixl ‹$$› 900)
notation fmempty (‹{$$}›)
nonterminal fmaplets and fmaplet
syntax
"_fmaplet" :: "['a, 'a] ⇒ fmaplet" ("_ /$$:=/ _")
"_fmaplets" :: "['a, 'a] ⇒ fmaplet" ("_ /[$$:=]/ _")
"" :: "fmaplet ⇒ fmaplets" ("_")
"_Fmaplets" :: "[fmaplet, fmaplets] ⇒ fmaplets" ("_,/ _")
"_FmapUpd" :: "[('a, 'b) fmap, fmaplets] ⇒ ('a, 'b) fmap" ("_/'(_')" [900, 0] 900)
"_Fmap" :: "fmaplets ⇒ ('a, 'b) fmap" ("(1{_})")
syntax_consts
"_fmaplet" "_fmaplets" "_Fmaplets" "_FmapUpd" "_Fmap" ⇌ fmupd
translations
"_FmapUpd m (_Fmaplets xy ms)" ⇌ "_FmapUpd (_FmapUpd m xy) ms"
"_FmapUpd m (_fmaplet x y)" ⇌ "CONST fmupd x y m"
"_Fmap ms" ⇌ "_FmapUpd (CONST fmempty) ms"
"_Fmap (_Fmaplets ms1 ms2)" ↽ "_FmapUpd (_Fmap ms1) ms2"
"_Fmaplets ms1 (_Fmaplets ms2 ms3)" ↽ "_Fmaplets (_Fmaplets ms1 ms2) ms3"
abbreviation (infixl ‹$$!› 900) where
"m $$! k ≡ the (m $$ k)"
lemma :
assumes "k⇩1 ≠ k⇩2"
shows "{k⇩1 $$:= v⇩1} ++⇩f {k⇩2 $$:= v⇩2} = {k⇩2 $$:= v⇩2} ++⇩f {k⇩1 $$:= v⇩1}"
proof (intro fmap_ext)
fix k
consider
(a) "k = k⇩1" |
(b) "k = k⇩2" |
(c) "k ≠ k⇩1 ∧ k ≠ k⇩2"
by auto
with assms show "({k⇩1 $$:= v⇩1} ++⇩f {k⇩2 $$:= v⇩2}) $$ k = ({k⇩2 $$:= v⇩2} ++⇩f {k⇩1 $$:= v⇩1}) $$ k"
by auto
qed
lemma :
assumes "m $$ k = None"
shows "m ++⇩f {k $$:= v} = {k $$:= v} ++⇩f m"
using assms
proof (induction m arbitrary: k v)
case fmempty
then show ?case
by simp
next
case (fmupd x y m)
have "m(x $$:= y) ++⇩f {k $$:= v} = m ++⇩f {x $$:= y} ++⇩f {k $$:= v}"
by simp
also from fmupd.hyps and fmupd.IH have "… = {x $$:= y} ++⇩f m ++⇩f {k $$:= v}"
by simp
also from fmupd.prems and fmupd.hyps and fmupd.IH have "… = {x $$:= y} ++⇩f {k $$:= v} ++⇩f m"
by (metis fmadd_assoc fmupd_lookup)
also have "… = {k $$:= v} ++⇩f m(x $$:= y)"
proof (cases "x ≠ k")
case True
then have "{x $$:= y} ++⇩f {k $$:= v} ++⇩f m = {k $$:= v} ++⇩f {x $$:= y} ++⇩f m"
using fmadd_singletons_comm by metis
also from fmupd.prems and fmupd.hyps and fmupd.IH have "… = {k $$:= v} ++⇩f m ++⇩f {x $$:= y}"
by (metis fmadd_assoc)
finally show ?thesis
by simp
next
case False
with fmupd.prems show ?thesis
by auto
qed
finally show ?case .
qed
lemma :
assumes "fmdom' m⇩1 ∩ fmdom' m⇩2 = {}"
shows "m⇩1 ++⇩f m⇩2 = m⇩2 ++⇩f m⇩1"
using assms
proof (induction m⇩2 arbitrary: m⇩1)
case fmempty
then show ?case
by simp
next
case (fmupd k v m⇩2)
then show ?case
proof (cases "m⇩1 $$ k = None")
case True
from fmupd.hyps have "m⇩1 ++⇩f m⇩2(k $$:= v) = m⇩1 ++⇩f m⇩2 ++⇩f {k $$:= v}"
by simp
also from fmupd.prems and fmupd.hyps and fmupd.IH have "… = m⇩2 ++⇩f m⇩1 ++⇩f {k $$:= v}"
by simp
also from True have "… = m⇩2 ++⇩f {k $$:= v} ++⇩f m⇩1"
using fmap_singleton_comm by (metis fmadd_assoc)
finally show ?thesis
by simp
next
case False
with fmupd.prems show ?thesis
by auto
qed
qed
lemma : "fmran {k $$:= v} = {|v|}"
proof -
have "v' |∈| fmran {k $$:= v} ⟹ v' = v" for v'
proof -
assume "v' |∈| fmran {k $$:= v}"
fix k'
have "fmdom' {k $$:= v} = {k}"
by simp
then show "v' = v"
proof (cases "k' = k")
case True
with ‹v' |∈| fmran {k $$:= v}› show ?thesis
using fmdom'I by fastforce
next
case False
with ‹fmdom' {k $$:= v} = {k}› and ‹v' |∈| fmran {k $$:= v}› show ?thesis
using fmdom'I by fastforce
qed
qed
moreover have "v |∈| fmran {k $$:= v}"
by (simp add: fmranI)
ultimately show ?thesis
by (simp add: fsubsetI fsubset_antisym)
qed
lemma :
assumes "fmdom' m⇩1 ∩ fmdom' m⇩2 = {}"
shows "fmmap_keys f (m⇩1 ++⇩f m⇩2) = fmmap_keys f m⇩1 ++⇩f fmmap_keys f m⇩2"
using assms
by (simp add: fmap_ext)
lemma :
assumes "m $$ k = None"
shows "map (λk'. (k', m(k $$:= v) $$! k')) (insort k xs) =
insort_key fst (k, v) (map (λk'. (k', m(k $$:= v) $$! k')) xs)"
using assms by (induction xs) auto
lemma :
assumes "m $$ k = None"
shows "sorted_list_of_fmap (m(k $$:= v)) = insort_key fst (k, v) (sorted_list_of_fmap m)"
proof -
have "sorted_list_of_fmap (m(k $$:= v)) =
map (λk'. (k', m(k $$:= v) $$! k')) (sorted_list_of_fset (fmdom (m(k $$:= v))))"
unfolding sorted_list_of_fmap_def ..
also have "… = map (λk'. (k', m(k $$:= v) $$! k')) (sorted_list_of_fset (finsert k (fmdom m)))"
by simp
also from ‹m $$ k = None› have "… =
map (λk'. (k', m(k $$:= v) $$! k')) (insort k (sorted_list_of_fset (fmdom m - {|k|})))"
by (simp add: sorted_list_of_fset.rep_eq)
also from ‹m $$ k = None› have "… =
map (λk'. (k', m(k $$:= v) $$! k')) (insort k (sorted_list_of_fset (fmdom m)))"
by (simp add: fmdom_notI)
also from ‹m $$ k = None› have "… =
insort_key fst (k, v) (map (λk'. (k', m(k $$:= v) $$! k')) (sorted_list_of_fset (fmdom m)))"
using map_insort_is_insort_key by fastforce
also have "… = insort_key fst (k, v) (map (λk'. (k', m $$! k')) (sorted_list_of_fset (fmdom m)))"
proof -
from ‹m $$ k = None› have "⋀k'. k' ∈ fmdom' m ⟹ m(k $$:= v) $$! k' = m $$! k'"
using fmdom'_notI by force
moreover from ‹m $$ k = None› have "k ∉ set (sorted_list_of_fset (fmdom m))"
using fmdom'_alt_def and fmdom'_notI and in_set_member by force
ultimately show ?thesis
by (metis (mono_tags, lifting) fmdom'_alt_def map_eq_conv sorted_list_of_fset_simps(1))
qed
finally show ?thesis
unfolding sorted_list_of_fmap_def by simp
qed
lemma :
assumes "distinct (map fst ps)"
and "inj f"
shows "distinct (map fst (map (λ(k, v). (f k, v)) ps))"
proof -
have "map fst (map (λ(k, v). (f k, v)) ps) = map f (map fst ps)"
by (induction ps) auto
moreover from assms have "distinct (map f (map fst ps))"
by (simp add: distinct_map inj_on_def)
ultimately show ?thesis
by presburger
qed
lemma :
shows "distinct (map fst (sorted_list_of_fmap m))"
unfolding sorted_list_of_fmap_def and sorted_list_of_fset_def
by (simp add: distinct_map inj_on_def)
lemma :
assumes "k ∉ set (map fst ps)"
and "inj f"
shows "f k ∉ set (map fst (map (λ(k, v). (f k, v)) ps))"
using assms by (induction ps) (simp add: member_rec(2), fastforce simp add: injD)
lemma :
assumes "distinct (map fst ps)"
and "k ∉ set (map fst ps)"
and "inj f"
and "mono f"
shows "map (λ(k, v). (f k, v)) (insort_key fst (k, v) ps) =
insort_key fst (f k, v) (map (λ(k, v). (f k, v)) ps)"
using assms
proof (induction ps)
case Nil
then show ?case
by simp
next
let ?g = "(λ(k, v). (f k, v))"
case (Cons p ps)
then show ?case
proof (cases "k ≤ fst p")
case True
let ?f_p = "(f (fst p), snd p)"
have "insort_key fst (f k, v) (map ?g (p # ps)) = insort_key fst (f k, v) (?f_p # map ?g ps)"
by (simp add: prod.case_eq_if)
moreover from Cons.prems(4) and True have "f k ≤ f (fst p)"
by (auto dest: monoE)
then have "insort_key fst (f k, v) (?f_p # map ?g ps) = (f k, v) # ?f_p # map ?g ps"
by simp
ultimately have "insort_key fst (f k, v) (map ?g (p # ps)) = (f k, v) # ?f_p # map ?g ps"
by simp
moreover from True have "map ?g (insort_key fst (k, v) (p # ps)) = (f k, v) # ?f_p # map ?g ps"
by (simp add: case_prod_beta')
ultimately show ?thesis
by simp
next
case False
let ?f_p = "(f (fst p), snd p)"
have "insort_key fst (f k, v) (map ?g (p # ps)) = insort_key fst (f k, v) (?f_p # map ?g ps)"
by (simp add: prod.case_eq_if)
moreover from ‹mono f› and False have "f (fst p) ≤ f k"
using not_le by (blast dest: mono_invE)
ultimately have "insort_key fst (f k, v) (map ?g (p # ps)) =
?f_p # insort_key fst (f k, v) (map ?g ps)"
using False and ‹inj f› by (fastforce dest: injD)
also from Cons.IH and Cons.prems(1,2) and assms(3,4) have "… =
?f_p # (map ?g (insort_key fst (k, v) ps))"
by (fastforce simp add: member_rec(1))
also have "… = map ?g (p # insort_key fst (k, v) ps)"
by (simp add: case_prod_beta)
finally show ?thesis
using False by simp
qed
qed
lemma :
assumes "inj f"
and "mono f"
and "m $$ k = None"
shows "map (λ(k, v). (f k, v)) (sorted_list_of_fmap (m(k $$:= v))) =
insort_key fst (f k, v) (map (λ(k, v). (f k, v)) (sorted_list_of_fmap m))"
proof -
let ?g = "(λ(k, v). (f k, v))"
from ‹m $$ k = None› have "map ?g (sorted_list_of_fmap (m(k $$:= v))) =
map ?g (insort_key fst (k, v) (sorted_list_of_fmap m))"
using sorted_list_of_fmap_is_insort_key_fst by fastforce
also have "… = insort_key fst (f k, v) (map ?g (sorted_list_of_fmap m))"
proof -
have "distinct (map fst (sorted_list_of_fmap m))"
by (simp add: distinct_sorted_list_of_fmap)
moreover from ‹m $$ k = None› have "k ∉ set (map fst (sorted_list_of_fmap m))"
by (metis image_set map_of_eq_None_iff map_of_sorted_list)
ultimately show ?thesis
by (simp add: map_insort_key_fst assms(1,2))
qed
finally show ?thesis .
qed
lemma :
assumes "distinct (map fst ps)"
and "k ∉ set (map fst ps)"
shows "fmap_of_list (insort_key fst (k, v) ps) = (fmap_of_list ps)(k $$:= v)"
using assms
proof (induction ps)
case Nil
then show ?case
by simp
next
case (Cons p ps)
then show ?case
proof (cases "k ≤ fst p")
case True
then show ?thesis
by simp
next
case False
then have "fmap_of_list (insort_key fst (k, v) (p # ps)) =
fmap_of_list (p # insort_key fst (k, v) ps)"
by simp
also have "… = (fmap_of_list (insort_key fst (k, v) ps))(fst p $$:= snd p)"
by (metis fmap_of_list_simps(2) prod.collapse)
also from Cons.prems(1,2) and Cons.IH have "… = (fmap_of_list ps)(k $$:= v)(fst p $$:= snd p)"
by (fastforce simp add: member_rec(1))
finally show ?thesis
proof -
assume *: "fmap_of_list (insort_key fst (k, v) (p # ps)) =
(fmap_of_list ps)(k $$:= v)(fst p $$:= snd p)"
from Cons.prems(2) have "k ∉ set (fst p # map fst ps)"
by simp
then have **: "{k $$:= v} $$ (fst p) = None"
by (fastforce simp add: member_rec(1))
have "fmap_of_list (p # ps) = (fmap_of_list ps)(fst p $$:= snd p)"
by (metis fmap_of_list_simps(2) prod.collapse)
with * and ** show ?thesis
using fmap_singleton_comm by (metis fmadd_fmupd fmap_of_list_simps(1,2) fmupd_alt_def)
qed
qed
qed
lemma :
assumes "inj f"
and "m $$ k = None"
shows "fmap_of_list (insort_key fst (f k, v) (map (λ(k, v). (f k, v)) (sorted_list_of_fmap m))) =
(fmap_of_list (map (λ(k, v). (f k, v)) (sorted_list_of_fmap m)))(f k $$:= v)"
proof -
let ?g = "λ(k, v). (f k, v)"
let ?ps = "map ?g (sorted_list_of_fmap m)"
from ‹inj f› have "distinct (map fst ?ps)"
using distinct_fst_inj and distinct_sorted_list_of_fmap by fastforce
moreover have "f k ∉ set (map fst ?ps)"
proof -
from ‹m $$ k = None› have "k ∉ set (map fst (sorted_list_of_fmap m))"
by (metis map_of_eq_None_iff map_of_sorted_list set_map)
with ‹inj f› show ?thesis
using map_inj_pair_non_membership by force
qed
ultimately show ?thesis
using fmap_of_list_insort_key_fst by fast
qed
lemma :
fixes m :: "('a::linorder, 'b) fmap"
and f :: "'a ⇒ 'c::linorder"
assumes "inj f"
and "mono f"
and "m $$ k = None"
shows "fmap_of_list (map (λ(k, v). (f k, v)) (sorted_list_of_fmap (m(k $$:= v)))) =
(fmap_of_list (map (λ(k, v). (f k, v)) (sorted_list_of_fmap m)))(f k $$:= v)"
proof -
let ?g = "λ(k, v). (f k, v)"
from assms(3) have "fmap_of_list (map ?g (sorted_list_of_fmap (m(k $$:= v)))) =
fmap_of_list (map ?g (insort_key fst (k, v) (sorted_list_of_fmap m)))"
by (simp add: sorted_list_of_fmap_is_insort_key_fst)
also from assms have "… = fmap_of_list (insort_key fst (f k, v) (map ?g (sorted_list_of_fmap m)))"
using calculation and map_sorted_list_of_fmap by fastforce
also from assms(1,3) have "… = (fmap_of_list (map ?g (sorted_list_of_fmap m)))(f k $$:= v)"
by (simp add: fmap_of_list_insort_key_fst_map)
finally show ?thesis .
qed
text ‹ Map difference ›
lemma :
assumes "m ⊆⇩f n"
and "n ⊆⇩f m"
shows "m = n"
proof -
from ‹m ⊆⇩f n› have "∀k ∈ dom (($$) m). (($$) m) k = (($$) n) k"
by (simp add: fmsubset.rep_eq map_le_def)
moreover from ‹n ⊆⇩f m› have "∀k ∈ dom (($$) n). (($$) n) k = (($$) m) k"
by (simp add: fmsubset.rep_eq map_le_def)
ultimately show ?thesis
proof (intro fmap_ext)
fix k
consider
(a) "k ∈ dom (($$) m)" |
(b) "k ∈ dom (($$) n)" |
(c) "k ∉ dom (($$) m) ∧ k ∉ dom (($$) n)"
by auto
then show "m $$ k = n $$ k"
proof cases
case a
with ‹∀k ∈ dom (($$) m). m $$ k = n $$ k› show ?thesis
by simp
next
case b
with ‹∀k ∈ dom (($$) n). n $$ k = m $$ k› show ?thesis
by simp
next
case c
then show ?thesis
by (simp add: fmdom'_notD)
qed
qed
qed
abbreviation
:: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap" (infixl ‹--⇩f› 100) where
"m⇩1 --⇩f m⇩2 ≡ fmfilter (λx. x ∉ fmdom' m⇩2) m⇩1"
lemma :
assumes "m⇩2 ⊆⇩f m⇩1"
shows "m⇩2 ++⇩f (m⇩1 --⇩f m⇩2) = m⇩1"
proof -
have *: "m⇩2 ++⇩f (m⇩1 --⇩f m⇩2) ⊆⇩f m⇩1"
proof -
have "∀k v. (m⇩2 ++⇩f (m⇩1 --⇩f m⇩2)) $$ k = Some v ⟶ m⇩1 $$ k = Some v"
proof (intro allI impI)
fix k v
assume "(m⇩2 ++⇩f (m⇩1 --⇩f m⇩2)) $$ k = Some v"
then have **: "(if k |∈| fmdom (m⇩1 --⇩f m⇩2) then (m⇩1 --⇩f m⇩2) $$ k else m⇩2 $$ k) = Some v"
by simp
then show "m⇩1 $$ k = Some v"
proof (cases "k |∈| fmdom (m⇩1 --⇩f m⇩2)")
case True
with ** show ?thesis
by simp
next
case False
with ** and ‹m⇩2 ⊆⇩f m⇩1› show ?thesis
by (metis (mono_tags, lifting) fmpredD fmsubset_alt_def)
qed
qed
then have "fmpred (λk v. m⇩1 $$ k = Some v) (m⇩2 ++⇩f (m⇩1 --⇩f m⇩2))"
by (blast intro: fmpred_iff)
then show ?thesis
by (auto simp add: fmsubset_alt_def)
qed
then have "m⇩1 ⊆⇩f m⇩2 ++⇩f (m⇩1 --⇩f m⇩2)"
by (simp add: fmsubset.rep_eq map_le_def)
with * show ?thesis
by (simp add: fsubset_antisym)
qed
lemma :
assumes "m $$ k = None"
shows "m(k $$:= v) --⇩f {k $$:= v} = m"
proof -
let ?P = "(λk'. k' ∉ {k})"
have "m(k $$:= v) --⇩f {k $$:= v} = fmfilter (λx. x ∉ fmdom' {k $$:= v}) (m(k $$:= v))" ..
also have "… = fmfilter ?P (m(k $$:= v))"
by simp
also have "… = (if ?P k then (fmfilter ?P m)(k $$:= v) else fmfilter ?P m)"
by simp
also have "… = fmfilter ?P m"
by simp
finally show ?thesis
proof -
from ‹m $$ k = None› have "⋀k' v'. m $$ k' = Some v' ⟹ ?P k'"
by fastforce
then show ?thesis
by simp
qed
qed
text ‹ Map symmetric difference ›
abbreviation :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap" (infixl ‹Δ⇩f› 100) where
"m⇩1 Δ⇩f m⇩2 ≡ (m⇩1 --⇩f m⇩2) ++⇩f (m⇩2 --⇩f m⇩1)"
text ‹ Domain restriction ›
abbreviation :: "'a set ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap" (infixl ‹⊲› 150) where
"s ⊲ m ≡ fmfilter (λx. x ∈ s) m"
text ‹ Domain exclusion ›
abbreviation :: "'a set ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap" (infixl ‹⊲'/› 150) where
"s ⊲/ m ≡ fmfilter (λx. x ∉ s) m"
text ‹ Intersection plus ›
abbreviation :: "('a, 'b::monoid_add) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap"
(infixl ‹∩⇩+› 100)
where
"m⇩1 ∩⇩+ m⇩2 ≡ fmmap_keys (λk v. v + m⇩1 $$! k) (fmdom' m⇩1 ⊲ m⇩2)"
text ‹ Union override right ›
abbreviation :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap"
(infixl ‹∪⇩→› 100)
where
"m⇩1 ∪⇩→ m⇩2 ≡ (fmdom' m⇩2 ⊲/ m⇩1) ++⇩f m⇩2"
text ‹ Union override left ›
abbreviation :: "('a, 'b) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap"
(infixl ‹∪⇩←› 100)
where
"m⇩1 ∪⇩← m⇩2 ≡ m⇩1 ++⇩f (fmdom' m⇩1 ⊲/ m⇩2)"
text ‹ Union override plus ›
abbreviation :: "('a, 'b::monoid_add) fmap ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap"
(infixl ‹∪⇩+› 100)
where
"m⇩1 ∪⇩+ m⇩2 ≡ (m⇩1 Δ⇩f m⇩2) ++⇩f (m⇩1 ∩⇩+ m⇩2)"
text ‹ Extra lemmas for the non-standard map operators ›
lemma :
assumes "m $$ k = Some v"
shows "{k} ⊲ m = {k $$:= v}"
using assms
proof (induction m)
case fmempty
then show ?case
by simp
next
case (fmupd k' v' m)
then show ?case
proof (cases "k = k'")
case True
with ‹m(k' $$:= v') $$ k = Some v› have "v = v'"
by simp
with True have "{k} ⊲ m(k' $$:= v') = ({k} ⊲ m)(k $$:= v)"
by simp
also from True and ‹m $$ k' = None› have "… = {$$}(k $$:= v)"
by (simp add: fmap_ext)
finally show ?thesis
by simp
next
case False
with ‹m(k' $$:= v') $$ k = Some v› have *: "m $$ k = Some v"
by simp
with False have "{k} ⊲ m(k' $$:= v') = {k} ⊲ m"
by simp
with * and fmupd.IH show ?thesis
by simp
qed
qed
lemma :
shows "(A ∪ B) ⊲ m = A ⊲ m ++⇩f B ⊲ m"
proof -
have "($$) ((A ∪ B) ⊲ m) ⊆⇩m ($$) (A ⊲ m ++⇩f B ⊲ m)"
proof (unfold map_le_def, intro ballI)
fix k
assume "k ∈ dom (($$) ((A ∪ B) ⊲ m))"
then show "((A ∪ B) ⊲ m) $$ k = (A ⊲ m ++⇩f B ⊲ m) $$ k"
by auto
qed
moreover have "($$) (A ⊲ m ++⇩f B ⊲ m) ⊆⇩m ($$) ((A ∪ B) ⊲ m)"
proof (unfold map_le_def, intro ballI)
fix k
assume "k ∈ dom (($$) (A ⊲ m ++⇩f B ⊲ m))"
then show "(A ⊲ m ++⇩f B ⊲ m) $$ k = ((A ∪ B) ⊲ m) $$ k"
by auto
qed
ultimately show ?thesis
using fmlookup_inject and map_le_antisym by blast
qed
lemma :
shows "s ⊲/ (m⇩1 ++⇩f m⇩2) = (s ⊲/ m⇩1) ++⇩f (s ⊲/ m⇩2)"
by (blast intro: fmfilter_add_distrib)
lemma :
shows "m = s ⊲/ m ++⇩f s ⊲ m"
proof (induction m)
case fmempty
then show ?case
by simp
next
case (fmupd k v m)
from fmupd.hyps have "s ⊲/ m(k $$:= v) ++⇩f s ⊲ m(k $$:= v) =
s ⊲/ (m ++⇩f {k $$:= v}) ++⇩f s ⊲ (m ++⇩f {k $$:= v})"
by simp
also have "… = s ⊲/ m ++⇩f s ⊲/ {k $$:= v} ++⇩f s ⊲ m ++⇩f s ⊲ {k $$:= v}"
using dom_exc_add_distr by simp
finally show ?case
proof (cases "k ∈ s")
case True
then have "s ⊲/ m ++⇩f s ⊲/ {k $$:= v} ++⇩f s ⊲ m ++⇩f s ⊲ {k $$:= v} =
s ⊲/ m ++⇩f {$$} ++⇩f s ⊲ m ++⇩f {k $$:= v}"
by simp
also have "… = s ⊲/ m ++⇩f s ⊲ m ++⇩f {k $$:= v}"
by simp
also from fmupd.IH have "… = m ++⇩f {k $$:= v}"
by simp
finally show ?thesis using fmupd.hyps
by auto
next
case False
then have "s ⊲/ m ++⇩f s ⊲/ {k $$:= v} ++⇩f s ⊲ m ++⇩f s ⊲ {k $$:= v} =
s ⊲/ m ++⇩f {k $$:= v} ++⇩f s ⊲ m ++⇩f {$$}"
by simp
also have "… = s ⊲/ m ++⇩f {k $$:= v} ++⇩f s ⊲ m"
by simp
also from fmupd.hyps have "… = s ⊲/ m ++⇩f s ⊲ m ++⇩f {k $$:= v}"
using fmap_singleton_comm by (metis (full_types) fmadd_assoc fmlookup_filter)
also from fmupd.IH have "… = m ++⇩f {k $$:= v}"
by simp
finally show ?thesis
by auto
qed
qed
lemma :
assumes "m⇩1 $$ k = None"
and "m⇩2 $$ k = Some v'"
shows "fmdom' (m⇩1(k $$:= v)) ⊲ m⇩2 = fmdom' m⇩1 ⊲ m⇩2 ++⇩f {k $$:= v'}"
proof -
from ‹m⇩1 $$ k = None› have "fmdom' (m⇩1(k $$:= v)) ⊲ m⇩2 = (fmdom' m⇩1 ∪ {k}) ⊲ m⇩2"
by simp
also have "… = fmdom' m⇩1 ⊲ m⇩2 ++⇩f {k} ⊲ m⇩2"
using dom_res_union_distr .
finally show ?thesis
using ‹m⇩2 $$ k = Some v'› and dom_res_singleton by fastforce
qed
lemma :
assumes "m⇩2 $$ k = None"
shows "fmdom' (m⇩1(k $$:= v)) ⊲ m⇩2 = fmdom' m⇩1 ⊲ m⇩2"
proof -
have "fmdom' (m⇩1(k $$:= v)) ⊲ m⇩2 = fmfilter (λk'. k' = k ∨ k' ∈ fmdom' m⇩1) m⇩2"
by simp
also have "… = fmdom' m⇩1 ⊲ m⇩2"
proof (intro fmfilter_cong')
show "m⇩2 = m⇩2" ..
next
from assms show "k' ∈ fmdom' m⇩2 ⟹ (k' = k ∨ k' ∈ fmdom' m⇩1) = (k' ∈ fmdom' m⇩1)" for k'
by (cases "k' = k") (simp_all add: fmdom'_notI)
qed
finally show ?thesis .
qed
lemma :
assumes "m⇩1 $$ k = None"
and "m⇩2 $$ k = Some v'"
shows "m⇩1(k $$:= v) ∩⇩+ m⇩2 = (m⇩1 ∩⇩+ m⇩2) ++⇩f {k $$:= v' + v}"
proof -
let ?f = "λk' v'. v' + m⇩1(k $$:= v) $$! k'"
from assms have "m⇩1(k $$:= v) ∩⇩+ m⇩2 = fmmap_keys ?f ((fmdom' m⇩1 ⊲ m⇩2) ++⇩f {k $$:= v'})"
using dom_res_addition_in by fastforce
also have "… = fmmap_keys ?f (fmdom' m⇩1 ⊲ m⇩2) ++⇩f fmmap_keys ?f {k $$:= v'}"
proof -
from ‹m⇩1 $$ k = None› have "fmdom' (fmdom' m⇩1 ⊲ m⇩2) ∩ fmdom' {k $$:= v'} = {}"
by (simp add: fmdom'_notI)
then show ?thesis
using fmmap_keys_hom by blast
qed
also from assms
have "… = fmmap_keys ?f (fmdom' m⇩1 ⊲ m⇩2) ++⇩f {k $$:= v' + v}"
proof -
have "fmmap_keys ?f {k $$:= v'} = {k $$:= v' + v}"
proof (intro fmap_ext)
fix k'
have "fmmap_keys ?f {k $$:= v'} $$ k' = map_option (?f k') ({k $$:= v'} $$ k')"
using fmlookup_fmmap_keys .
also have "… = map_option (?f k') (if k = k' then Some v' else {$$} $$ k')"
by simp
also have "… = {k $$:= v' + v} $$ k'"
by (cases "k' = k") simp_all
finally show "fmmap_keys ?f {k $$:= v'} $$ k' = {k $$:= v' + v} $$ k'" .
qed
then show ?thesis
by simp
qed
also have "… = fmmap_keys (λk' v'. v' + m⇩1 $$! k') (fmdom' m⇩1 ⊲ m⇩2) ++⇩f {k $$:= v' + v}"
by (simp add: fmap_ext)
finally show ?thesis .
qed
lemma :
assumes "m⇩1 $$ k = None"
and "m⇩2 $$ k = None"
shows "m⇩1(k $$:= v) ∩⇩+ m⇩2 = (m⇩1 ∩⇩+ m⇩2)"
proof -
let ?f = "λk' v'. v' + m⇩1(k $$:= v) $$! k'"
from ‹m⇩2 $$ k = None›
have "m⇩1(k $$:= v) ∩⇩+ m⇩2 = fmmap_keys ?f (fmdom' m⇩1 ⊲ m⇩2)"
using dom_res_addition_not_in by metis
also have "… = fmmap_keys (λk' v'. v' + m⇩1 $$! k') (fmdom' m⇩1 ⊲ m⇩2)"
proof (intro fmap_ext)
fix k'
have "fmmap_keys ?f (fmdom' m⇩1 ⊲ m⇩2) $$ k' = map_option (?f k') ((fmdom' m⇩1 ⊲ m⇩2) $$ k')"
using fmlookup_fmmap_keys .
also from ‹m⇩1 $$ k = None› have "… = fmmap_keys (λk' v'. v' + m⇩1 $$! k') (fmdom' m⇩1 ⊲ m⇩2) $$ k'"
by (cases "k' = k") (simp_all add: fmdom'_notI)
finally show "fmmap_keys ?f (fmdom' m⇩1 ⊲ m⇩2) $$ k' =
fmmap_keys (λk' v'. v' + m⇩1 $$! k') (fmdom' m⇩1 ⊲ m⇩2) $$ k'" .
qed
finally show ?thesis .
qed
lemma :
assumes "m⇩1 $$ k = None"
and "m⇩2 $$ k = None"
shows "m⇩1(k $$:= v) ∪⇩+ m⇩2 = (m⇩1 ∪⇩+ m⇩2) ++⇩f {k $$:= v}"
proof -
from ‹m⇩2 $$ k = None› have "(m⇩1(k $$:= v)) ∪⇩+ m⇩2 =
fmdom' m⇩2 ⊲/ m⇩1 ++⇩f {k $$:= v} ++⇩f fmdom' (m⇩1(k $$:= v)) ⊲/ m⇩2 ++⇩f (m⇩1(k $$:= v) ∩⇩+ m⇩2)"
by (simp add: fmdom'_notI)
also from assms have "… =
fmdom' m⇩2 ⊲/ m⇩1 ++⇩f {k $$:= v} ++⇩f fmdom' m⇩1 ⊲/ m⇩2 ++⇩f (m⇩1(k $$:= v) ∩⇩+ m⇩2)"
by (smt (verit, best) Int_iff Int_insert_left_if0 fmdom'_fmupd fmdom'_notI fmfilter_cong')
also from assms have "… = fmdom' m⇩2 ⊲/ m⇩1 ++⇩f {k $$:= v} ++⇩f fmdom' m⇩1 ⊲/ m⇩2 ++⇩f (m⇩1 ∩⇩+ m⇩2)"
using inter_plus_addition_notin by metis
also from assms have "… = fmdom' m⇩2 ⊲/ m⇩1 ++⇩f fmdom' m⇩1 ⊲/ m⇩2 ++⇩f (m⇩1 ∩⇩+ m⇩2) ++⇩f {k $$:= v}"
using fmap_singleton_comm
by (metis (mono_tags, lifting) fmadd_assoc fmdom'_notI fmfilter_fmmap_keys fmlookup_filter)
finally show ?thesis .
qed
end