Theory Env-Nominal

theory "Env-Nominal"
  imports Env "Nominal-Utils" "Nominal-HOLCF"
begin

subsubsection ‹Equivariance lemmas›

lemma edom_perm:
  fixes f :: "'a::pt ⇒ 'b::{pcpo_pt}"
  shows "edom (π ∙ f) = π ∙ (edom f)"
  by (simp add: edom_def)

lemmas edom_perm_rev[simp,eqvt] = edom_perm[symmetric]

lemma mem_edom_perm[simp]:
  fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt}"
  shows "xa ∈ edom (p ∙ ρ) ⟷ - p ∙ xa ∈ edom ρ" 
  by (metis (mono_tags) edom_perm_rev mem_Collect_eq permute_set_eq)

lemma env_restr_eqvt[eqvt]:
  fixes m :: "'a::pt ⇒ 'b::{cont_pt,pcpo}"
  shows "π ∙ m f|` d = (π ∙ m) f|` (π ∙ d)"
  by (auto simp add: env_restr_def)

lemma env_delete_eqvt[eqvt]:
  fixes m :: "'a::pt ⇒ 'b::{cont_pt,pcpo}"
  shows "π ∙ env_delete x m = env_delete (π ∙ x) (π ∙ m)"
  by (auto simp add: env_delete_def)

lemma esing_eqvt[eqvt]: "π ∙ (esing x) = esing (π ∙ x)"
  unfolding esing_def
  apply perm_simp
  apply (simp add: Abs_cfun_eqvt)
  done

subsubsection ‹Permutation and restriction›

lemma env_restr_perm:
  fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
  assumes "supp p ♯* S" and [simp]: "finite S"
  shows "(p ∙ ρ) f|` S = ρ f|` S"
using assms
apply -
apply (rule ext)
apply (case_tac "x ∈ S")
apply (simp)
apply (subst permute_fun_def)
apply (simp add: permute_pure)
apply (subst perm_supp_eq)
apply (auto simp add:perm_supp_eq supp_minus_perm fresh_star_def fresh_def supp_set_elem_finite)
done

lemma env_restr_perm':
  fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
  assumes "supp p ♯* S" and [simp]: "finite S"
  shows "p ∙ (ρ f|` S) = ρ f|` S"
  by (simp add: perm_supp_eq[OF assms(1)]  env_restr_perm[OF assms])

lemma env_restr_flip:
  fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
  assumes "x ∉ S" and "x' ∉ S"
  shows "((x' ↔ x) ∙ ρ) f|` S = ρ f|` S"
  using assms
  apply -
  apply rule
  apply (auto  simp add: permute_flip_at env_restr_def split:if_splits)
  by (metis eqvt_lambda flip_at_base_simps(3) minus_flip permute_pure unpermute_def)

lemma env_restr_flip':
  fixes ρ :: "'a::at_base ⇒ 'b::{pcpo_pt,pure}"
  assumes "x ∉ S" and "x' ∉ S"
  shows "(x' ↔ x) ∙ (ρ f|` S) = ρ f|` S"
  by (simp add: flip_set_both_not_in[OF assms]  env_restr_flip[OF assms])



subsubsection ‹Pure codomains›
(*
lemma edom_fv_pure:
  fixes f :: "('a::at_base ⇒ 'b::{pcpo,pure})"
  assumes "finite (edom f)"
  shows  "fv f = edom f"
using assms
proof (induction "edom f" arbitrary: f)
  case empty
  hence "f = ⊥" unfolding edom_def by auto
  thus ?case by (auto simp add: fv_def fresh_def supp_def)
next
  case (insert x S)
  have "f = (env_delete x f)(x := f x)" by auto

  from `insert x S = edom f`  and `x ∉ S`
  have "S = edom (env_delete x f)" by auto
  hence "fv (env_delete x f) = edom (env_delete x f)" by (rule insert)
*)

lemma edom_fv_pure:
  fixes f :: "('a::at_base ⇒ 'b::{pcpo,pure})"
  assumes "finite (edom f)"
  shows  "fv f ⊆ edom f"
using assms
proof (induction "edom f" arbitrary: f)
  case empty
  hence "f = ⊥" unfolding edom_def by auto
  thus ?case by (auto simp add: fv_def fresh_def supp_def)
next
  case (insert x S)
  have "f = (env_delete x f)(x := f x)" by auto
  hence "fv f ⊆ fv (env_delete x f) ∪ fv x ∪ fv (f x)"
    using eqvt_fresh_cong3[where f = fun_upd and x = "env_delete x f" and y = x and z = "f x", OF fun_upd_eqvt]
    apply (auto simp add: fv_def fresh_def)
    by (metis fresh_def pure_fresh)
  also

  from ‹insert x S = edom f›  and ‹x ∉ S›
  have "S = edom (env_delete x f)" by auto
  hence "fv (env_delete x f) ⊆ edom (env_delete x f)" by (rule insert)
  also
  have "fv (f x) = {}" by (rule fv_pure)
  also
  from ‹insert x S = edom f› have "x ∈ edom f" by auto
  hence "edom (env_delete x f) ∪ fv x ∪ {} ⊆ edom f" by auto
  finally
  show ?case by this (intro Un_mono subset_refl)
qed

(*
lemma domA_fresh_pure:
  fixes Γ :: "('a::at_base × 'b::pure) list"
  shows  "x ∈ domA Γ ⟷ ¬(atom x ♯ Γ)"
  unfolding domA_fv_pure[symmetric]
  by (auto simp add: fv_def fresh_def)
*)

end