diff -r 4b4742aa43f2 -r 11f6a561eb4b Nominal/Ex/Finite_Alpha.thy
--- a/Nominal/Ex/Finite_Alpha.thy	Sat Dec 17 17:03:01 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-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