diff -r d24f59f78a86 -r 141a36535f1d Nominal/ExTySch.thy
--- a/Nominal/ExTySch.thy	Sat Mar 27 09:21:43 2010 +0100
+++ b/Nominal/ExTySch.thy	Sat Mar 27 09:41:00 2010 +0100
@@ -5,13 +5,31 @@
 (* Type Schemes *)
 atom_decl name
 
-(*ML {* val _ = alpha_type := AlphaRes *}*)
+ML {* val _ = alpha_type := AlphaRes *}
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"
 and tyS =
   All xs::"name fset" ty::"t" bind xs in ty
 
+lemma t_tyS_supp_fv: "fv_t t = supp t \<and> fv_tyS tyS = supp tyS"
+apply (induct rule: t_tyS.induct)
+apply (simp_all only: t_tyS.fv)
+apply (simp_all only: supp_abs(2)[symmetric])
+apply(simp_all (no_asm) only: supp_def)
+apply(simp_all only: t_tyS.perm permute_abs)
+apply(simp only: t_tyS.eq_iff supp_at_base[simplified supp_def])
+apply(simp only: t_tyS.eq_iff Collect_disj_eq[symmetric] infinite_Un[symmetric])
+apply simp
+apply(simp only: Abs_eq_iff t_tyS.eq_iff)
+apply (simp add: alphas)
+apply (simp add: eqvts[symmetric])
+apply (simp add: eqvts eqvts_raw)
+done
+
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS_supp_fv]
+
+
 lemma size_eqvt_raw:
   "size (pi \<bullet> t :: t_raw) = size t"
   "size (pi \<bullet> ts :: tyS_raw) = size ts"
@@ -69,8 +87,6 @@
 thm t_tyS.distinct
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
-
 lemma induct:
   assumes a1: "\<And>name b. P b (Var name)"
   and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
@@ -120,7 +136,6 @@
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alphas)
-  apply(auto)
   apply(simp add: fresh_star_def fresh_zero_perm)
   done
 
@@ -128,16 +143,15 @@
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts)
-  apply auto
+  apply(simp add: alphas fresh_star_def eqvts)
   done
 
 lemma
   shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
-oops
+  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
+done
 
 lemma
   assumes a: "a \<noteq> b"
@@ -145,7 +159,7 @@
   using a
   apply(simp add: t_tyS.eq_iff)
   apply(clarify)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
   apply auto
   done