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