--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Finite_Alpha.thy	Wed Sep 21 12:01:34 2011 +0200
@@ -0,0 +1,115 @@
+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