Theory 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{_})")

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 fmap_lookup_the (infixl $$! 900) where
  "m $$! k  the (m $$ k)"

lemma fmadd_singletons_comm:
  assumes "k1  k2"
  shows "{k1 $$:= v1} ++f {k2 $$:= v2} = {k2 $$:= v2} ++f {k1 $$:= v1}"
proof (intro fmap_ext)
  fix k
  consider
    (a) "k = k1" |
    (b) "k = k2" |
    (c) "k  k1  k  k2"
    by auto
  with assms show "({k1 $$:= v1} ++f {k2 $$:= v2}) $$ k = ({k2 $$:= v2} ++f {k1 $$:= v1}) $$ k"
    by auto
qed

lemma fmap_singleton_comm:
  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 fmap_disj_comm:
  assumes "fmdom' m1  fmdom' m2 = {}"
  shows "m1 ++f m2 = m2 ++f m1"
  using assms
proof (induction m2 arbitrary: m1)
  case fmempty
  then show ?case
    by simp
next
  case (fmupd k v m2)
  then show ?case
  proof (cases "m1 $$ k = None")
    case True
    from fmupd.hyps have "m1 ++f m2(k $$:= v) = m1 ++f m2 ++f {k $$:= v}"
      by simp
    also from fmupd.prems and fmupd.hyps and fmupd.IH have " = m2 ++f m1 ++f {k $$:= v}"
      by simp
    also from True have " = m2 ++f {k $$:= v} ++f m1"
      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_singleton: "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 fmmap_keys_hom:
  assumes "fmdom' m1  fmdom' m2 = {}"
  shows "fmmap_keys f (m1 ++f m2) = fmmap_keys f m1 ++f fmmap_keys f m2"
  using assms
  by (simp add: fmap_ext)

lemma map_insort_is_insort_key:
  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 sorted_list_of_fmap_is_insort_key_fst:
  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 distinct_fst_inj:
  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 distinct_sorted_list_of_fmap:
  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 map_inj_pair_non_membership:
  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 map_insort_key_fst:
  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 map_sorted_list_of_fmap:
  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 fmap_of_list_insort_key_fst:
  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 fmap_of_list_insort_key_fst_map:
  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 fmap_of_list_sorted_list_of_fmap:
  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 fsubset_antisym:
  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
  fmdiff :: "('a, 'b) fmap  ('a, 'b) fmap  ('a, 'b) fmap" (infixl --f 100) where
  "m1 --f m2  fmfilter (λx. x  fmdom' m2) m1"

lemma fmdiff_partition:
  assumes "m2 f m1"
  shows "m2 ++f (m1 --f m2) = m1"
proof -
  have *: "m2 ++f (m1 --f m2) f m1"
  proof -
    have "k v. (m2 ++f (m1 --f m2)) $$ k = Some v  m1 $$ k = Some v"
    proof (intro allI impI)
      fix k v
      assume "(m2 ++f (m1 --f m2)) $$ k = Some v"
      then have **: "(if k |∈| fmdom (m1 --f m2) then (m1 --f m2) $$ k else m2 $$ k) = Some v"
        by simp
      then show "m1 $$ k = Some v"
      proof (cases "k |∈| fmdom (m1 --f m2)")
        case True
        with ** show ?thesis
          by simp
      next
        case False
        with ** and m2 f m1 show ?thesis
          by (metis (mono_tags, lifting) fmpredD fmsubset_alt_def)
      qed
    qed
    then have "fmpred (λk v. m1 $$ k = Some v) (m2 ++f (m1 --f m2))"
      by (blast intro: fmpred_iff)
    then show ?thesis
      by (auto simp add: fmsubset_alt_def)
  qed
  then have "m1 f m2 ++f (m1 --f m2)"
    by (simp add: fmsubset.rep_eq map_le_def)
  with * show ?thesis
    by (simp add: fsubset_antisym)
qed

lemma fmdiff_fmupd:
  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 fmsym_diff :: "('a, 'b) fmap  ('a, 'b) fmap  ('a, 'b) fmap" (infixl Δf 100) where
  "m1 Δf m2  (m1 --f m2) ++f (m2 --f m1)"

text ‹ Domain restriction ›

abbreviation dom_res :: "'a set  ('a, 'b) fmap  ('a, 'b) fmap" (infixl  150) where
  "s  m  fmfilter (λx. x  s) m"

text ‹ Domain exclusion ›

abbreviation dom_exc :: "'a set  ('a, 'b) fmap  ('a, 'b) fmap" (infixl ⊲'/ 150) where
  "s ⊲/ m  fmfilter (λx. x  s) m"

text ‹ Intersection plus ›

abbreviation intersection_plus :: "('a, 'b::monoid_add) fmap  ('a, 'b) fmap  ('a, 'b) fmap"
  (infixl + 100)
where
  "m1 + m2  fmmap_keys (λk v. v + m1 $$! k) (fmdom' m1  m2)"

text ‹ Union override right ›

abbreviation union_override_right :: "('a, 'b) fmap  ('a, 'b) fmap  ('a, 'b) fmap"
  (infixl  100)
where
  "m1  m2  (fmdom' m2 ⊲/ m1) ++f m2"

text ‹ Union override left ›

abbreviation union_override_left :: "('a, 'b) fmap  ('a, 'b) fmap  ('a, 'b) fmap"
  (infixl  100)
where
  "m1  m2  m1 ++f (fmdom' m1 ⊲/ m2)"

text ‹ Union override plus ›

abbreviation union_override_plus :: "('a, 'b::monoid_add) fmap  ('a, 'b) fmap  ('a, 'b) fmap"
  (infixl + 100)
where
  "m1 + m2  (m1 Δf m2) ++f (m1 + m2)"

text ‹ Extra lemmas for the non-standard map operators ›

lemma dom_res_singleton:
  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 dom_res_union_distr:
  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 dom_exc_add_distr:
  shows "s ⊲/ (m1 ++f m2) = (s ⊲/ m1) ++f (s ⊲/ m2)"
  by (blast intro: fmfilter_add_distrib)

lemma fmap_partition:
  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 dom_res_addition_in:
  assumes "m1 $$ k = None"
  and "m2 $$ k = Some v'"
  shows "fmdom' (m1(k $$:= v))  m2 = fmdom' m1  m2 ++f {k $$:= v'}"
proof -
  from m1 $$ k = None have "fmdom' (m1(k $$:= v))  m2 = (fmdom' m1  {k})  m2"
    by simp
  also have " = fmdom' m1  m2 ++f {k}  m2"
    using dom_res_union_distr .
  finally show ?thesis
    using m2 $$ k = Some v' and dom_res_singleton by fastforce
qed

lemma dom_res_addition_not_in:
  assumes "m2 $$ k = None"
  shows "fmdom' (m1(k $$:= v))  m2 = fmdom' m1  m2"
proof -
  have "fmdom' (m1(k $$:= v))  m2 = fmfilter (λk'. k' = k  k'  fmdom' m1) m2"
    by simp
  also have " = fmdom' m1  m2"
  proof (intro fmfilter_cong')
    show "m2 = m2" ..
  next
    from assms show "k'  fmdom' m2  (k' = k  k'  fmdom' m1) = (k'  fmdom' m1)" for k'
    by (cases "k' = k") (simp_all add: fmdom'_notI)
  qed
  finally show ?thesis .
qed

lemma inter_plus_addition_in:
  assumes "m1 $$ k = None"
  and "m2 $$ k = Some v'"
  shows "m1(k $$:= v) + m2 = (m1 + m2) ++f {k $$:= v' + v}"
proof -
  let ?f = "λk' v'. v' + m1(k $$:= v) $$! k'"
  from assms have "m1(k $$:= v) + m2 = fmmap_keys ?f ((fmdom' m1  m2) ++f {k $$:= v'})"
    using dom_res_addition_in by fastforce
  also have " = fmmap_keys ?f (fmdom' m1  m2) ++f fmmap_keys ?f {k $$:= v'}"
  proof -
    from m1 $$ k = None have "fmdom' (fmdom' m1  m2)  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' m1  m2) ++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' + m1 $$! k') (fmdom' m1  m2) ++f {k $$:= v' + v}"
    by (simp add: fmap_ext)
  finally show ?thesis .
qed

lemma inter_plus_addition_notin:
  assumes "m1 $$ k = None"
  and "m2 $$ k = None"
  shows "m1(k $$:= v) + m2 = (m1 + m2)"
proof -
  let ?f = "λk' v'. v' + m1(k $$:= v) $$! k'"
  from m2 $$ k = None
  have "m1(k $$:= v) + m2 = fmmap_keys ?f (fmdom' m1  m2)"
    using dom_res_addition_not_in by metis
  also have " = fmmap_keys (λk' v'. v' + m1 $$! k') (fmdom' m1  m2)"
  proof (intro fmap_ext)
    fix k'
    have "fmmap_keys ?f (fmdom' m1  m2) $$ k' = map_option (?f k') ((fmdom' m1  m2) $$ k')"
      using fmlookup_fmmap_keys .
    also from m1 $$ k = None have " = fmmap_keys (λk' v'. v' + m1 $$! k') (fmdom' m1  m2) $$ k'"
      by (cases "k' = k") (simp_all add: fmdom'_notI)
    finally show "fmmap_keys ?f (fmdom' m1  m2) $$ k' =
      fmmap_keys (λk' v'. v' + m1 $$! k') (fmdom' m1  m2) $$ k'" .
  qed
  finally show ?thesis .
qed

lemma union_plus_addition_notin: (* TODO: Find nicer proofs for SMT calls. *)
  assumes "m1 $$ k = None"
  and "m2 $$ k = None"
  shows "m1(k $$:= v) + m2 = (m1 + m2) ++f {k $$:= v}"
proof -
  from m2 $$ k = None have "(m1(k $$:= v)) + m2 =
    fmdom' m2 ⊲/ m1 ++f {k $$:= v} ++f fmdom' (m1(k $$:= v)) ⊲/ m2 ++f (m1(k $$:= v) + m2)"
    by (simp add: fmdom'_notI)
  also from assms have " =
    fmdom' m2 ⊲/ m1 ++f {k $$:= v} ++f fmdom' m1 ⊲/ m2 ++f (m1(k $$:= v) + m2)"
    by (smt (verit, best) Int_iff Int_insert_left_if0 fmdom'_fmupd fmdom'_notI fmfilter_cong')
  also from assms have " = fmdom' m2 ⊲/ m1 ++f {k $$:= v} ++f fmdom' m1 ⊲/ m2 ++f (m1 + m2)"
    using inter_plus_addition_notin by metis
  also from assms have " = fmdom' m2 ⊲/ m1 ++f fmdom' m1 ⊲/ m2 ++f (m1 + m2) ++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