theory Finite_Alpha
imports "../Nominal2"
begin

lemma
  assumes "(supp x - as) \<sharp>* p"
      and "p \<bullet> x = y"
      and "p \<bullet> as = bs"
    shows "(as, x) \<approx>set (op =) supp p (bs, y)"
  using assms unfolding alphas
  by (metis Diff_eqvt atom_set_perm_eq supp_eqvt)

lemma
  assumes "(supp x - set as) \<sharp>* p"
      and "p \<bullet> x = y"
      and "p \<bullet> as = bs"
    shows "(as, x) \<approx>lst (op =) supp p (bs, y)"
  using assms unfolding alphas
  by (metis Diff_eqvt atom_set_perm_eq supp_eqvt supp_of_atom_list)

lemma
  assumes "(supp x - as) \<sharp>* p"
      and "p \<bullet> x = y"
      and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y"
      and "finite (supp x)"
  shows "(as, x) \<approx>res (op =) supp p (bs, y)"
  using assms
  unfolding alpha_res_alpha_set
  unfolding alphas
  apply simp
  apply rule
  apply (rule trans)
  apply (rule supp_perm_eq[symmetric, of _ p])
  apply (simp add: supp_finite_atom_set fresh_star_def)
  apply blast
  apply (simp add: eqvts)
  apply (simp add: fresh_star_def)
  apply blast
  done

lemma
  assumes "(as, x) \<approx>res (op =) supp p (bs, y)"
  shows "(supp x - as) \<sharp>* p"
    and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y"
    and "p \<bullet> x = y"
  using assms
  apply -
  prefer 3
  apply (auto simp add: alphas)[2]
  unfolding alpha_res_alpha_set
  unfolding alphas
  by blast

(* On the raw level *)

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)

thm alpha_lam_raw.intros(3)[unfolded alphas, simplified]

lemma alpha_fv: "alpha_lam_raw l r \<Longrightarrow> fv_lam_raw l = fv_lam_raw r"
  by (induct rule: alpha_lam_raw.induct) (simp_all add: alphas)

lemma finite_fv_raw: "finite (fv_lam_raw l)"
  by (induct rule: lam_raw.induct) (simp_all add: supp_at_base)

lemma "(fv_lam_raw l - {atom n}) \<sharp>* p \<Longrightarrow> alpha_lam_raw (p \<bullet> l) r \<Longrightarrow>
  fv_lam_raw l - {atom n} = fv_lam_raw r - {atom (p \<bullet> n)}"
  apply (rule trans)
  apply (rule supp_perm_eq[symmetric])
  apply (subst supp_finite_atom_set)
  apply (rule finite_Diff)
  apply (rule finite_fv_raw)
  apply assumption
  apply (simp add: eqvts)
  apply (subst alpha_fv)
  apply assumption
  apply (rule)
  done

(* For the res binding *)

nominal_datatype ty2 =
  Var2 "name"
| Fun2 "ty2" "ty2"

nominal_datatype tys2 =
  All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty

lemma alpha_fv': "alpha_tys2_raw l r \<Longrightarrow> fv_tys2_raw l = fv_tys2_raw r"
  by (induct rule: alpha_tys2_raw.induct) (simp_all add: alphas)

lemma finite_fv_raw': "finite (fv_tys2_raw l)"
  by (induct rule: tys2_raw.induct) (simp_all add: supp_at_base finite_supp)

thm alpha_tys2_raw.intros[unfolded alphas, simplified]

lemma "(supp x - atom ` (fset as)) \<sharp>* p \<Longrightarrow> p \<bullet> (x :: tys2) = y \<Longrightarrow>
  p \<bullet> (atom ` (fset as) \<inter> supp x) = atom ` (fset bs) \<inter> supp y \<Longrightarrow>
  supp x - atom ` (fset as) = supp y - atom ` (fset bs)"
  apply (rule trans)
  apply (rule supp_perm_eq[symmetric])
  apply (subst supp_finite_atom_set)
  apply (rule finite_Diff)
  apply (rule finite_supp)
  apply assumption
  apply (simp add: eqvts)
  apply blast
  done

end