Theory FMap_Lemmas

(* Author: Matthias Brun,   ETH Zürich, 2019 *)
(* Author: Dmitriy Traytel, ETH Zürich, 2019 *)

(*<*)
theory FMap_Lemmas
  imports "HOL-Library.Finite_Map"
          Nominal2_Lemmas
begin
(*>*)

text ‹Nominal setup for finite maps.›

abbreviation fmap_update (‹_'(_ $$:= _')› [1000,0,0] 1000)  where "fmap_update Γ x τ ≡ fmupd x τ Γ"
notation fmlookup (infixl ‹$$› 999)
notation fmempty (‹{$$}›)

instantiation fmap :: (pt, pt) pt
begin

unbundle fmap.lifting

lift_definition
  permute_fmap :: "perm ⇒ ('a, 'b) fmap ⇒ ('a, 'b) fmap"
  is
  "permute :: perm ⇒ ('a ⇀ 'b) ⇒ ('a ⇀ 'b)"
proof -
  fix p and f :: "'a ⇀ 'b"
  assume "finite (dom f)"
  then show "finite (dom (p ∙ f))"
  proof (rule finite_surj[of _ _ "permute p"]; unfold dom_def, safe)
    fix x y
    assume some: "(p ∙ f) x = Some y"
    show "x ∈ permute p ` {a. f a ≠ None}"
    proof (rule image_eqI[of _ _ "- p ∙ x"])
      from some show "- p ∙ x ∈ {a. f a ≠ None}"
        by (auto simp: permute_self pemute_minus_self
          dest: arg_cong[of _ _ "permute (- p)"] intro!: exI[of _ "- p ∙ y"])
    qed (simp only: permute_minus_cancel)
  qed
qed

instance
proof
  fix x :: "('a, 'b) fmap"
  show "0 ∙ x = x"
    by transfer simp
next
  fix p q and x :: "('a, 'b) fmap"
  show "(p + q) ∙ x = p ∙ q ∙ x"
    by transfer simp
qed

end

lemma fmempty_eqvt[eqvt]:
  shows "(p ∙ {$$}) = {$$}"
  by transfer simp

lemma fmap_update_eqvt[eqvt]:
  shows "(p ∙ f(a $$:= b)) = (p ∙ f)((p ∙ a) $$:= (p ∙ b))"
  by transfer (simp add: map_upd_def)

lemma fmap_apply_eqvt[eqvt]:
  shows "(p ∙ (f $$ b)) = (p ∙ f) $$ (p ∙ b)"
  by transfer simp

lemma fresh_fmempty[simp]:
  shows "a ♯ {$$}"
  unfolding fresh_def supp_def
  by transfer simp

lemma fresh_fmap_update:
  shows "⟦a ♯ f; a ♯ x; a ♯ y⟧ ⟹ a ♯ f(x $$:= y)"
  unfolding fresh_conv_MOST
  by (elim MOST_rev_mp) simp

lemma supp_fmempty[simp]:
  shows "supp {$$} = {}"
  by (simp add: supp_def)

lemma supp_fmap_update:
  shows "supp (f(x $$:= y)) ⊆ supp(f, x, y)"
  using fresh_fmap_update
  by (auto simp: fresh_def supp_Pair)

instance fmap :: (fs, fs) fs
proof
  fix x :: "('a, 'b) fmap"
  show "finite (supp x)"
    by (induct x rule: fmap_induct)
      (simp_all add: supp_Pair finite_supp finite_subset[OF supp_fmap_update])
qed

lemma fresh_transfer[transfer_rule]:
  "((=) ===> pcr_fmap (=) (=) ===> (=)) fresh fresh"
  unfolding fresh_def supp_def rel_fun_def pcr_fmap_def cr_fmap_def simp_thms
    option.rel_eq fun_eq_iff[symmetric]
  by (auto elim!: finite_subset[rotated] simp: fmap_ext)

lemma fmmap_eqvt[eqvt]: "p ∙ (fmmap f F) = fmmap (p ∙ f) (p ∙ F)"
  by (induct F arbitrary: f rule: fmap_induct) (auto simp add: fmap_update_eqvt fmmap_fmupd)

lemma fmap_freshness_lemma:
  fixes h :: "('a::at,'b::pt) fmap"
  assumes a: "∃a. atom a ♯ (h, h $$ a)"
  shows  "∃x. ∀a. atom a ♯ h ⟶ h $$ a = x"
  using assms unfolding fresh_Pair
  by transfer (simp add: fresh_Pair freshness_lemma)

lemma fmap_freshness_lemma_unique:
  fixes h :: "('a::at,'b::pt) fmap"
  assumes "∃a. atom a ♯ (h, h $$ a)"
  shows "∃!x. ∀a. atom a ♯ h ⟶ h $$ a = x"
  using assms unfolding fresh_Pair
  by transfer (rule freshness_lemma_unique, auto simp: fresh_Pair)

lemma fmdrop_fset_fmupd[simp]:
  "(fmdrop_fset A f)(x $$:= y) = fmdrop_fset (A |-| {|x|}) f(x $$:= y)"
  including fmap.lifting and fset.lifting
  by transfer (auto simp: map_drop_set_def map_upd_def map_filter_def)

lemma fresh_fset_fminus:
  assumes "atom x ♯ A"
  shows   "A |-| {|x|} = A"
  using assms by (induct A) (simp_all add: finsert_fminus_if fresh_finsert)

lemma fresh_fun_app:
  shows "atom x ♯ F ⟹ x ≠ y ⟹ F y = Some a ⟹ atom x ♯ a"
  using supp_fun_app[of F y]
  by (auto simp: fresh_def supp_Some atom_not_fresh_eq)

lemma fresh_fmap_fresh_Some:
  "atom x ♯ F ⟹ x ≠ y ⟹ F $$ y = Some a ⟹ atom x ♯ a"
  including fmap.lifting
  by (transfer) (auto elim: fresh_fun_app)

lemma fmdrop_eqvt: "p ∙ fmdrop x F = fmdrop (p ∙ x) (p ∙ F)"
  by transfer (auto simp: map_drop_def map_filter_def)

lemma fmfilter_eqvt: "p ∙ fmfilter Q F = fmfilter (p ∙ Q) (p ∙ F)"
  by transfer (auto simp: map_filter_def)

lemma fmdrop_eq_iff:
  "fmdrop x B = fmdrop y B ⟷ x = y ∨ (x ∉ fmdom' B ∧ y ∉ fmdom' B)"
  by transfer (auto simp: map_drop_def map_filter_def fun_eq_iff, metis)

lemma fresh_fun_upd:
  shows "⟦a ♯ f; a ♯ x; a ♯ y⟧ ⟹ a ♯ f(x := y)"
  unfolding fresh_conv_MOST by (elim MOST_rev_mp) simp

lemma supp_fun_upd:
  shows "supp (f(x := y)) ⊆ supp(f, x, y)"
  using fresh_fun_upd by (auto simp: fresh_def supp_Pair)

lemma map_drop_fun_upd: "map_drop x F = F(x := None)"
  unfolding map_drop_def map_filter_def by auto

lemma fresh_fmdrop_in_fmdom: "⟦ x ∈ fmdom' B; y ♯ B; y ♯ x ⟧ ⟹ y ♯ fmdrop x B"
  by transfer (auto simp: map_drop_fun_upd fresh_None intro!: fresh_fun_upd)

lemma fresh_fmdrop:
  assumes "x ♯ B" "x ♯ y"
  shows   "x ♯ fmdrop y B"
  using assms by (cases "y ∈ fmdom' B") (auto dest!: fresh_fmdrop_in_fmdom simp: fmdrop_idle')

lemma fresh_fmdrop_fset:
  fixes x :: atom and A :: "(_ :: at_base) fset"
  assumes "x ♯ A" "x ♯ B"
  shows   "x ♯ fmdrop_fset A B"
  using assms(1) by (induct A) (auto simp: fresh_fmdrop assms(2) fresh_finsert)

(*<*)
end
(*>*)