diff -r 66d388a84e3c -r 50838e25f73c Nominal/Test.thy
--- a/Nominal/Test.thy	Fri Mar 19 15:43:43 2010 +0100
+++ b/Nominal/Test.thy	Fri Mar 19 15:43:59 2010 +0100
@@ -6,13 +6,6 @@
 
 atom_decl name
 
-(* maybe should be added to Infinite.thy *)
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
-ML {* val _ = cheat_alpha_eqvt := false *}
-ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = recursive := false *}
 
 nominal_datatype lm =
@@ -247,6 +240,11 @@
 thm lam'_bp'.distinct
 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
 
+lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+apply (simp add: supp_Abs supp_Pair)
+apply blast
+done
+
 lemma supp_fv':
   shows "supp t = fv_lam' t" 
   and "supp bp = fv_bp' bp"
@@ -439,7 +437,7 @@
   VarTS "name"
 | FunTS "t" "t"
 and  tyS =
-  All xs::"name set" ty::"t" bind xs in ty
+  All xs::"name fset" ty::"t" bind xs in ty
 
 thm t_tyS.fv
 thm t_tyS.eq_iff
@@ -480,16 +478,16 @@
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 (* All case *)
-apply(rule_tac t="supp (All fun t)" and s="supp (Abs (atom ` fun) t)" in subst)
+apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" 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: eqvts)
 apply(simp only: alpha_gen)
 apply(simp only: supp_eqvt[symmetric])
-apply(simp only: eqvts)
+apply(simp only: eqvts eqvts_raw)
 apply(rule trans)
 apply(rule finite_supp_Abs)
 apply(simp add: finite_fv_t_tyS)
@@ -570,6 +568,27 @@
 thm trm5_lts.induct
 thm trm5_lts.distinct
 
+lemma
+  shows "fv_trm5 t = supp t"
+  and "fv_lts l = supp l \<and> fv_bv5 l = {a. infinite {b. \<not>alpha_bv5 ((a \<rightleftharpoons> b) \<bullet> l) l}}"
+apply(induct t and l rule: trm5_lts.inducts)
+apply(simp_all only: trm5_lts.fv)
+apply(simp_all only: supp_Abs[symmetric])
+(*apply(simp_all only: supp_abs_sum)*)
+apply(simp_all (no_asm) only: supp_def)
+apply(simp_all only: trm5_lts.perm)
+apply(simp_all only: permute_ABS)
+apply(simp_all only: trm5_lts.eq_iff Abs_eq_iff)
+(*apply(simp_all only: alpha_gen2)*)
+apply(simp_all only: alpha_gen)
+apply(simp_all only: eqvts[symmetric] supp_Pair)
+apply(simp_all only: eqvts Pair_eq)
+apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
+apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
+apply(simp_all only: de_Morgan_conj[symmetric])
+apply simp_all
+done
+
 (* example from my PHD *)
 
 atom_decl coname