Theory Finite_Map_Ext

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
section ‹Finite Maps›
theory Finite_Map_Ext
  imports "HOL-Library.Finite_Map"
begin

type_notation fmap ("(_ ⇀⇩f /_)" [22, 21] 21)

nonterminal fmaplets and fmaplet

syntax
  "_fmaplet"  :: "['a, 'a] ⇒ fmaplet"              ("_ /↦⇩f/ _")
  "_fmaplets" :: "['a, 'a] ⇒ fmaplet"              ("_ /[↦⇩f]/ _")
  ""          :: "fmaplet ⇒ fmaplets"              ("_")
  "_FMaplets" :: "[fmaplet, fmaplets] ⇒ fmaplets"  ("_,/ _")
  "_FMapUpd"  :: "['a ⇀ 'b, fmaplets] ⇒ 'a ⇀ 'b" ("_/'(_')" [900, 0] 900)
  "_FMap"     :: "fmaplets ⇒ 'a ⇀ 'b"             ("(1[_])")

syntax (ASCII)
  "_fmaplet"  :: "['a, 'a] ⇒ fmaplet"              ("_ /|->f/ _")
  "_fmaplets" :: "['a, 'a] ⇒ fmaplet"              ("_ /[|->f]/ _")

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"

(*** Helper Lemmas **********************************************************)

subsection ‹Helper Lemmas›

lemma fmrel_on_fset_fmdom:
  "fmrel_on_fset (fmdom ym) f xm ym ⟹
   k |∈| fmdom ym ⟹
   k |∈| fmdom xm"
  by (metis fmdom_notD fmdom_notI fmrel_on_fsetD option.rel_sel)

(*** Finite Map Merge *******************************************************)

subsection ‹Merge Operation›

definition "fmmerge f xm ym ≡
  fmap_of_list (map
    (λk. (k, f (the (fmlookup xm k)) (the (fmlookup ym k))))
    (sorted_list_of_fset (fmdom xm |∩| fmdom ym)))"

lemma fmdom_fmmerge [simp]:
  "fmdom (fmmerge g xm ym) = fmdom xm |∩| fmdom ym"
  by (auto simp add: fmmerge_def fmdom_of_list)

lemma fmmerge_commut:
  assumes "⋀x y. x ∈ fmran' xm ⟹ f x y = f y x"
  shows "fmmerge f xm ym = fmmerge f ym xm"
proof -
  obtain zm where zm: "zm = sorted_list_of_fset (fmdom xm |∩| fmdom ym)"
    by auto
  with assms have
    "map (λk. (k, f (the (fmlookup xm k)) (the (fmlookup ym k)))) zm =
     map (λk. (k, f (the (fmlookup ym k)) (the (fmlookup xm k)))) zm"
    by (auto) (metis fmdom_notI fmran'I option.collapse)
  thus ?thesis
    unfolding fmmerge_def zm
    by (metis (no_types, lifting) inf_commute)
qed

lemma fmrel_on_fset_fmmerge1 [intro]:
  assumes "⋀x y z. z ∈ fmran' zm ⟹ f x z ⟹ f y z ⟹ f (g x y) z"
  assumes "fmrel_on_fset (fmdom zm) f xm zm"
  assumes "fmrel_on_fset (fmdom zm) f ym zm"
  shows "fmrel_on_fset (fmdom zm) f (fmmerge g xm ym) zm"
proof -
  {
    fix x a b c
    assume "x |∈| fmdom zm"
    moreover hence "x |∈| fmdom xm |∩| fmdom ym"
      by (meson assms(2) assms(3) finterI fmrel_on_fset_fmdom)
    moreover assume "fmlookup xm x = Some a"
                and "fmlookup ym x = Some b"
                and "fmlookup zm x = Some c"
    moreover from assms calculation have "f (g a b) c"
      by (metis fmran'I fmrel_on_fsetD option.rel_inject(2))
    ultimately have
      "rel_option f (fmlookup (fmmerge g xm ym) x) (fmlookup zm x)"
      unfolding fmmerge_def fmlookup_of_list apply auto
      unfolding option_rel_Some2 apply (rule_tac ?x="g a b" in exI)
      unfolding map_of_map_restrict restrict_map_def
      by auto
  }
  with assms(2) assms(3) show ?thesis
    by (meson fmdomE fmrel_on_fsetI fmrel_on_fset_fmdom)
qed

lemma fmrel_on_fset_fmmerge2 [intro]:
  assumes "⋀x y. x ∈ fmran' xm ⟹ f x (g x y)"
  shows "fmrel_on_fset (fmdom ym) f xm (fmmerge g xm ym)"
proof -
  {
    fix x a b
    assume "x |∈| fmdom xm |∩| fmdom ym"
       and "fmlookup xm x = Some a"
       and "fmlookup ym x = Some b"
    hence "rel_option f (fmlookup xm x) (fmlookup (fmmerge g xm ym) x)"
      unfolding fmmerge_def fmlookup_of_list apply auto
      unfolding option_rel_Some1 apply (rule_tac ?x="g a b" in exI)
      by (auto simp add: map_of_map_restrict assms fmran'I)
  }
  with assms show ?thesis
    apply auto
    apply (rule fmrel_on_fsetI)
    by (metis (full_types) finterD1 fmdomE fmdom_fmmerge fmdom_notD rel_option_None2)
qed

(*** Acyclicity *************************************************************)

subsection ‹Acyclicity›

abbreviation "acyclic_on xs r ≡ (∀x. x ∈ xs ⟶ (x, x) ∉ r⇧+)"

abbreviation "acyclicP_on xs r ≡ acyclic_on xs {(x, y). r x y}"

lemma fmrel_acyclic:
  "acyclicP_on (fmran' xm) R ⟹
   fmrel R⇧+⇧+ xm ym ⟹
   fmrel R ym xm ⟹
   xm = ym"
  by (metis (full_types) fmap_ext fmran'I fmrel_cases option.sel
        tranclp.trancl_into_trancl tranclp_unfold)

lemma fmrel_acyclic':
  assumes "acyclicP_on (fmran' ym) R"
  assumes "fmrel R⇧+⇧+ xm ym"
  assumes "fmrel R ym xm"
  shows "xm = ym"
proof -
  {
    fix x
    from assms(1) have
      "rel_option R⇧+⇧+ (fmlookup xm x) (fmlookup ym x) ⟹
       rel_option R (fmlookup ym x) (fmlookup xm x) ⟹
       rel_option R (fmlookup xm x) (fmlookup ym x)"
      by (metis (full_types) fmdom'_notD fmlookup_dom'_iff
            fmran'I option.rel_sel option.sel
            tranclp_into_tranclp2 tranclp_unfold)
  }
  with assms show ?thesis
    unfolding fmrel_iff
    by (metis fmap.rel_mono_strong fmrelI fmrel_acyclic tranclp.simps)
qed

lemma fmrel_on_fset_acyclic:
  "acyclicP_on (fmran' xm) R ⟹
   fmrel_on_fset (fmdom ym) R⇧+⇧+ xm ym ⟹
   fmrel_on_fset (fmdom xm) R ym xm ⟹
   xm = ym"
  unfolding fmrel_on_fset_fmrel_restrict
  by (metis (no_types, lifting) fmdom_filter fmfilter_alt_defs(5)
        fmfilter_cong fmlookup_filter fmrel_acyclic fmrel_fmdom_eq
        fmrestrict_fset_dom option.simps(3))

lemma fmrel_on_fset_acyclic':
  "acyclicP_on (fmran' ym) R ⟹
   fmrel_on_fset (fmdom ym) R⇧+⇧+ xm ym ⟹
   fmrel_on_fset (fmdom xm) R ym xm ⟹
   xm = ym"
  unfolding fmrel_on_fset_fmrel_restrict
  by (metis (no_types, lifting) ffmember_filter fmdom_filter
        fmfilter_alt_defs(5) fmfilter_cong fmrel_acyclic'
        fmrel_fmdom_eq fmrestrict_fset_dom)

(*** Transitive Closures ****************************************************)

subsection ‹Transitive Closures›

lemma fmrel_trans:
  "(⋀x y z. x ∈ fmran' xm ⟹ P x y ⟹ Q y z ⟹ R x z) ⟹
   fmrel P xm ym ⟹ fmrel Q ym zm ⟹ fmrel R xm zm"
  unfolding fmrel_iff
  by (metis fmdomE fmdom_notD fmran'I option.rel_inject(2) option.rel_sel)

lemma fmrel_on_fset_trans:
  "(⋀x y z. x ∈ fmran' xm ⟹ P x y ⟹ Q y z ⟹ R x z) ⟹
   fmrel_on_fset (fmdom ym) P xm ym ⟹
   fmrel_on_fset (fmdom zm) Q ym zm ⟹
   fmrel_on_fset (fmdom zm) R xm zm"
  apply (rule fmrel_on_fsetI)
  unfolding option.rel_sel apply auto
  apply (meson fmdom_notI fmrel_on_fset_fmdom)
  by (metis fmdom_notI fmran'I fmrel_on_fsetD fmrel_on_fset_fmdom
            option.rel_sel option.sel)

lemma trancl_to_fmrel:
  "(fmrel f)⇧+⇧+ xm ym ⟹ fmrel f⇧+⇧+ xm ym"
  apply (induct rule: tranclp_induct)
  apply (simp add: fmap.rel_mono_strong)
  by (rule fmrel_trans; auto)

lemma fmrel_trancl_fmdom_eq:
  "(fmrel f)⇧+⇧+ xm ym ⟹ fmdom xm = fmdom ym"
  by (induct rule: tranclp_induct; simp add: fmrel_fmdom_eq)

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmupd_fmdrop:
  "fmlookup xm k = Some x ⟹
   xm = fmupd k x (fmdrop k xm)"
  apply (rule fmap_ext)
  unfolding fmlookup_drop fmupd_lookup
  by auto

lemma fmap_eqdom_Cons1:
  assumes "fmlookup xm i = None"
      and "fmdom (fmupd i x xm) = fmdom ym"
      and "fmrel R (fmupd i x xm) ym"
    shows "(∃z zm. fmlookup zm i = None ∧ ym = (fmupd i z zm) ∧
                   R x z ∧ fmrel R xm zm)"
proof -
  from assms(2) obtain y where "fmlookup ym i = Some y" by force
  then obtain z zm where z_zm: "ym = fmupd i z zm ∧ fmlookup zm i = None"
    using fmupd_fmdrop by force
  {
    assume "¬ R x z"
    with z_zm have "¬ fmrel R (fmupd i x xm) ym"
      by (metis fmrel_iff fmupd_lookup option.simps(11))
  }
  with assms(3) moreover have "R x z" by auto
  {
    assume "¬ fmrel R xm zm"
    with assms(1) have "¬ fmrel R (fmupd i x xm) ym"
      by (metis fmrel_iff fmupd_lookup option.rel_sel z_zm)
  }
  with assms(3) moreover have "fmrel R xm zm" by auto
  ultimately show ?thesis using z_zm by blast
qed

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmap_eqdom_induct [consumes 2, case_names nil step]:
  assumes R: "fmrel R xm ym"
    and dom_eq: "fmdom xm = fmdom ym"
    and nil: "P (fmap_of_list []) (fmap_of_list [])"
    and step:
    "⋀x xm y ym i.
    ⟦R x y; fmrel R xm ym; fmdom xm = fmdom ym; P xm ym⟧ ⟹
    P (fmupd i x xm) (fmupd i y ym)"
  shows "P xm ym"
  using R dom_eq
proof (induct xm arbitrary: ym)
  case fmempty thus ?case
    by (metis fempty_iff fmdom_empty fmempty_of_list fmfilter_alt_defs(5)
              fmfilter_false fmrestrict_fset_dom local.nil)
next
  case (fmupd i x xm) show ?case
  proof -
    obtain y where "fmlookup ym i = Some y"
      by (metis fmupd.prems(1) fmrel_cases fmupd_lookup option.discI)
    from fmupd.hyps(2) fmupd.prems(1) fmupd.prems(2) obtain z zm where
      "fmlookup zm i = None" and
      ym_eq_z_zm: "ym = (fmupd i z zm)" and
      R_x_z: "R x z" and
      R_xm_zm: "fmrel R xm zm"
      using fmap_eqdom_Cons1 by metis
    hence dom_xm_eq_dom_zm: "fmdom xm = fmdom zm"
      using fmrel_fmdom_eq by blast
    with R_xm_zm fmupd.hyps(1) have "P xm zm" by blast
    with R_x_z R_xm_zm dom_xm_eq_dom_zm have
      "P (fmupd i x xm) (fmupd i z zm)"
      by (rule step)
    thus ?thesis by (simp add: ym_eq_z_zm)
  qed
qed

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmrel_to_rtrancl:
  assumes as_r: "reflp r"
      and rel_rpp_xm_ym: "fmrel r⇧*⇧* xm ym"
    shows "(fmrel r)⇧*⇧* xm ym"
proof -
  from rel_rpp_xm_ym have "fmdom xm = fmdom ym"
    using fmrel_fmdom_eq by blast
  with rel_rpp_xm_ym show "(fmrel r)⇧*⇧* xm ym"
  proof (induct rule: fmap_eqdom_induct)
    case nil show ?case by auto
  next
    case (step x xm y ym i) show ?case
    proof -
      from step.hyps(1) have "(fmrel r)⇧*⇧* (fmupd i x xm) (fmupd i y xm)"
      proof (induct rule: rtranclp_induct)
        case base show ?case by simp
      next
        case (step y z) show ?case
        proof -
          from as_r have "fmrel r xm xm"
            by (simp add: fmap.rel_reflp reflpD)
          with step.hyps(2) have "(fmrel r)⇧*⇧* (fmupd i y xm) (fmupd i z xm)"
            by (simp add: fmrel_upd r_into_rtranclp)
          with step.hyps(3) show ?thesis by simp
        qed
      qed
      also from step.hyps(4) have "(fmrel r)⇧*⇧* (fmupd i y xm) (fmupd i y ym)"
      proof (induct rule: rtranclp_induct)
        case base show ?case by simp
      next
        case (step ya za) show ?case
        proof -
          from step.hyps(2) as_r have "(fmrel r)⇧*⇧* (fmupd i y ya) (fmupd i y za)"
            by (simp add: fmrel_upd r_into_rtranclp reflp_def)
          with step.hyps(3) show ?thesis by simp
        qed
      qed
      finally show ?thesis by simp
    qed
  qed
qed

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53585232/632199"}
  and provided with the permission of the author of the answer.›

lemma fmrel_to_trancl:
  assumes "reflp r"
      and "fmrel r⇧+⇧+ xm ym"
    shows "(fmrel r)⇧+⇧+ xm ym"
proof -
  from assms(2) have "fmrel r⇧*⇧* xm ym"
    by (drule_tac ?Ra="r⇧*⇧*" in fmap.rel_mono_strong; auto)
  with assms(1) have "(fmrel r)⇧*⇧* xm ym"
    by (simp add: fmrel_to_rtrancl)
  with assms(1) show ?thesis
    by (metis fmap.rel_reflp reflpD rtranclpD tranclp.r_into_trancl)
qed

lemma fmrel_tranclp_induct:
  "fmrel r⇧+⇧+ a b ⟹
   reflp r ⟹
   (⋀y. fmrel r a y ⟹ P y) ⟹
   (⋀y z. (fmrel r)⇧+⇧+ a y ⟹ fmrel r y z ⟹ P y ⟹ P z) ⟹ P b"
  apply (drule fmrel_to_trancl, simp)
  by (erule tranclp_induct; simp)

lemma fmrel_converse_tranclp_induct:
  "fmrel r⇧+⇧+ a b ⟹
   reflp r ⟹
   (⋀y. fmrel r y b ⟹ P y) ⟹
   (⋀y z. fmrel r y z ⟹ fmrel r⇧+⇧+ z b ⟹ P z ⟹ P y) ⟹ P a"
  apply (drule fmrel_to_trancl, simp)
  by (erule converse_tranclp_induct; simp add: trancl_to_fmrel)

lemma fmrel_tranclp_trans_induct:
  "fmrel r⇧+⇧+ a b ⟹
   reflp r ⟹
   (⋀x y. fmrel r x y ⟹ P x y) ⟹
   (⋀x y z. fmrel r⇧+⇧+ x y ⟹ P x y ⟹ fmrel r⇧+⇧+ y z ⟹ P y z ⟹ P x z) ⟹
   P a b"
  apply (drule fmrel_to_trancl, simp)
  apply (erule tranclp_trans_induct, simp)
  using trancl_to_fmrel by blast

(*** Finite Map Size Calculation ********************************************)

subsection ‹Size Calculation›

text ‹
  The contents of the subsection was derived from the accepted answer
  on the website Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/53244203/632199"}
  and provided with the permission of the author of the answer.›

abbreviation "tcf ≡ (λ v::('a × nat). (λ r::nat. snd v + r))"

interpretation tcf: comp_fun_commute tcf
proof
  fix x y :: "'a × nat"
  show "tcf y ∘ tcf x = tcf x ∘ tcf y"
  proof -
    fix z
    have "(tcf y ∘ tcf x) z = snd y + snd x + z" by auto
    also have "(tcf x ∘ tcf y) z = snd y + snd x + z" by auto
    finally have "(tcf y ∘ tcf x) z = (tcf x ∘ tcf y) z" by auto
    thus "(tcf y ∘ tcf x) = (tcf x ∘ tcf y)" by auto
  qed
qed

lemma ffold_rec_exp:
  assumes "k |∈| fmdom x"
    and "ky = (k, the (fmlookup (fmmap f x) k))"
  shows "ffold tcf 0 (fset_of_fmap (fmmap f x)) =
        tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap f x)) |-| {|ky|}))"
proof -
  have "ky |∈| (fset_of_fmap (fmmap f x))"
    using assms by auto
  thus ?thesis
    by (simp add: tcf.ffold_rec)
qed

lemma elem_le_ffold [intro]:
  "k |∈| fmdom x ⟹
   f (the (fmlookup x k)) < Suc (ffold tcf 0 (fset_of_fmap (fmmap f x)))"
  by (subst ffold_rec_exp, auto)

lemma elem_le_ffold' [intro]:
  "z ∈ fmran' x ⟹
   f z < Suc (ffold tcf 0 (fset_of_fmap (fmmap f x)))"
  apply (erule fmran'E)
  apply (frule fmdomI)
  by (subst ffold_rec_exp, auto)

(*** Code Setup *************************************************************)

subsection ‹Code Setup›

abbreviation "fmmerge_fun f xm ym ≡
  fmap_of_list (map
    (λk. if k |∈| fmdom xm ∧ k |∈| fmdom ym
         then (k, f (the (fmlookup xm k)) (the (fmlookup ym k)))
         else (k, undefined))
    (sorted_list_of_fset (fmdom xm |∩| fmdom ym)))"

lemma fmmerge_fun_simp [code_abbrev, simp]:
  "fmmerge_fun f xm ym = fmmerge f xm ym"
  unfolding fmmerge_def
  apply (rule_tac ?f="fmap_of_list" in HOL.arg_cong)
  by simp

end