Theory FMap_Lemmas

theory FMap_Lemmas
  imports Nominal2.Nominal2
          "HOL-Library.Finite_Map"
          Nominal2_Lemmas
begin


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)"
  subgoal for p f
    apply (erule finite_surj[of _ _ "permute p"]; unfold dom_def, safe)
    subgoal for x y
      apply (rule image_eqI[of _ _ "- p ∙ x"])
      subgoal by (simp only: permute_minus_cancel)
      subgoal
        by (drule arg_cong[of _ _ "permute (- p)"])
          (auto simp: permute_self pemute_minus_self intro!: exI[of _ "- p ∙ y"])
      done
    done
  done

instance
  apply standard
   apply transfer
   apply simp
  apply transfer
  apply simp
  done

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
  apply standard
  subgoal for x
    apply (induct x rule: fmap_induct)
     apply simp
    apply (rule finite_subset[OF supp_fmap_update])
    apply (simp add: supp_Pair finite_supp)
    done
  done

lemma fmap_reorder_neq_updates:
  assumes "a ≠ b"
  shows   "Γ(a $$:= x)(b $$:= y) = Γ(b $$:= y)(a $$:= x)"
  using assms by transfer (auto simp: map_upd_def)

lemma fmap_upd_upd[simp]: "Γ(x $$:= y)(x $$:= z) = Γ(x $$:= z)"
  by transfer (simp add: map_upd_def)



lemma fresh_transfer[transfer_rule]:
  "((=) ===> pcr_fmap (=) (=) ===> (=)) fresh fresh"
  unfolding fresh_def supp_def rel_fun_def pcr_fmap_def cr_fmap_def
    permute_fmap_def fun_eq_iff
  apply (simp add: fmlookup_inverse)
  apply safe
  subgoal
    apply (erule finite_subset[rotated])
    apply safe
    apply (metis (full_types) eqvt_lambda fmap_ext option.rel_eq permute_fmap.rep_eq)
    done
  subgoal
    apply (erule finite_subset[rotated])
    apply safe
    apply (metis (mono_tags) eqvt_lambda option.rel_eq permute_fmap.rep_eq)
    done
  done

lemma fmmap_fmupd: "fmmap f F(x $$:= y) = (fmmap f F)(x $$:= f y)"
  by transfer (auto simp: fun_eq_iff map_upd_def)

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 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)

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_fmupd: "fmdrop x F(y $$:= z) = (if x = y then fmdrop x F else (fmdrop x F)(y $$:= z))"
  by transfer (auto simp: map_drop_def map_filter_def map_upd_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 fmdrop_idle: "x ∉ fmdom' B ⟹ fmdrop x B = B"
  by transfer (auto simp: map_drop_def map_filter_def)

lemma fmdrop_fmupd_same: "fmdrop x B(x $$:= y) = fmdrop x B"
  by transfer (auto simp: map_drop_def map_filter_def map_upd_def)

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)

lemma fmdrop_fset_fmdom[simp]: "fmdrop_fset (fmdom A) A = {$$}"
  by (induct A) (simp_all add: fmap_ext fmdom_notD)

end