--- a/Nominal/Test.thy	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 18:02:08 2010 +0100
@@ -10,7 +10,6 @@
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = recursive := false *}
 
-(*
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -22,19 +21,6 @@
   bi::"bp \<Rightarrow> atom set"
 where
   "bi (BP x t) = {atom x}"
-*)
-
-nominal_datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LAM x::"name" t::"lam" bind x in t
-| LET bp::"bp" t::"lam"   bind "bi bp" in t
-and bp =
-  BP "name"
-binder
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x) = {atom x}"
 
 thm lam_bp_fv
 thm lam_bp_inject
@@ -56,28 +42,10 @@
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
   by (rule eqvts)
 
-term alpha_bi
-
-lemma alpha_bi:
-  shows "alpha_bi b b' = True"
-apply(induct b rule: lam_bp_inducts(2))
-apply(simp_all)
-apply(induct b' rule: lam_bp_inducts(2))
-apply (simp_all add: lam_bp_inject)
-done
-
-lemma fv_bi:
-  shows "fv_bi b = {}"
-apply(induct b rule: lam_bp_inducts(2))
-apply(auto)[1]
-apply(simp_all)
-apply(simp add: lam_bp_fv)
-done
-
 lemma supp_fv:
   "supp t = fv_lam t" and 
-  "supp b = fv_bp b"
-apply(induct t and b rule: lam_bp_inducts)
+  "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
+apply(induct t and bp rule: lam_bp_inducts)
 apply(simp_all add: lam_bp_fv)
 (* VAR case *)
 apply(simp only: supp_def)
@@ -111,31 +79,32 @@
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
 apply(simp only: lam_bp_inject)
-(*
 apply(simp only: de_Morgan_conj)
 apply(simp only: Collect_disj_eq)
 apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
-*)
 apply(simp only: supp_def[symmetric])
 apply(simp only: supp_at_base)
-(*apply(simp)*)
+apply(simp)
 (* LET case *)
-apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs_tst bi bp_raw lam_raw)" in subst)
+apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
-apply(simp only: permute_ABS_tst)
+apply(simp only: permute_ABS)
 apply(simp only: lam_bp_inject)
-apply(simp only: eqvts_raw)
-apply(simp only: Abs_tst_eq_iff)
-apply(simp only: alpha_bi)
+apply(simp only: eqvts)
+apply(simp only: Abs_eq_iff)
+apply(simp only: ex_simps)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
 apply(simp only: alpha_gen)
-apply(simp only: alpha_tst) 
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
-apply simp
-apply(simp add: supp_Abs_tst)
-apply(simp add: fv_bi)
+apply(blast)
+apply(simp add: supp_Abs)
+apply(blast)
 done
 
 text {* example 2 *}