--- a/Nominal/Ex/SingleLet.thy	Mon Jul 26 09:19:28 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 27 09:09:02 2010 +0200
@@ -21,6 +21,14 @@
 where
   "bn (As x y t) = {atom x}"
 
+thm alpha_bn_imps
+thm distinct
+thm eq_iff
+thm fv_defs
+thm perm_simps
+thm perm_laws
+
+
 typ trm
 typ assg
 term Var 
@@ -28,25 +36,35 @@
 term Baz
 term bn
 term fv_trm
+term alpha_bn
 
-lemma a1:
-  shows "alpha_trm_raw x1 y1 \<Longrightarrow> True"
-  and   "alpha_assg_raw x2 y2 \<Longrightarrow> alpha_bn_raw x2 y2"
-  and   "alpha_bn_raw x3 y3 \<Longrightarrow> True"
-apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(rule TrueI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-sorry
+
 
 lemma a2:
   shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1"
   and   "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
   and   "alpha_bn_raw x3 y3 \<Longrightarrow>  fv_bn_raw x3 = fv_bn_raw y3"
 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
-apply(simp_all only: alphas prod_alpha_def)
-apply(auto)[1]
-apply(auto simp add: prod_alpha_def)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
+-- ""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc)
+-- ""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
+apply(simp only: Un_insert_left Un_empty_right Un_empty_left)
+-- ""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
+--""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
+apply(simp (no_asm) only: simp_thms)
+--""
+apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
+apply(simp only: Un_assoc set.simps append.simps)
 done
 
 lemma [quot_respect]: