--- a/Nominal/TySch.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -9,7 +9,6 @@
 ML {* val _ = cheat_equivp := false *}
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = cheat_alpha_eqvt := false *}
-ML {* val _ = recursive := false  *}
 
 nominal_datatype t =
   Var "name"
@@ -24,68 +23,6 @@
 thm t_tyS_induct
 thm t_tyS_distinct
 
-lemma supports:
-  "(supp (atom i)) supports (Var i)"
-  "(supp A \<union> supp M) supports (Fun A M)"
-apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh t_tyS_perm)
-apply clarify
-apply(simp_all add: fresh_atom)
-done
-
-lemma fs:
-  "finite (supp (x\<Colon>t)) \<and> finite (supp (z\<Colon>tyS))"
-apply(induct rule: t_tyS_induct)
-apply(rule supports_finite)
-apply(rule supports)
-apply(simp add: supp_atom)
-apply(rule supports_finite)
-apply(rule supports)
-apply(simp add: supp_atom)
-sorry
-
-instance t and tyS :: fs
-apply default
-apply (simp_all add: fs)
-sorry
-
-(* Should be moved to a proper place *)
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
-lemma supp_fv_t_tyS:
-  shows "supp T = fv_t T" 
-  and   "supp S = fv_tyS S"
-apply(induct T and S rule: t_tyS_inducts)
-apply(simp_all add: t_tyS_fv)
-(* VarTS case *)
-apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_eq_iff)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-(* FunTS case *)
-apply(simp only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: t_tyS_eq_iff)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-(* All case *)
-apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: t_tyS_perm)
-apply(simp only: permute_ABS)
-apply(simp only: t_tyS_eq_iff)
-apply(simp only: Abs_eq_iff)
-apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)
-apply(simp only: alpha_gen)
-apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
-apply(simp only: supp_Abs)
-done
-
 lemma
   shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS_eq_iff)
@@ -120,5 +57,4 @@
   apply auto
   done
 
-
 end