--- a/LamEx.thy	Thu Nov 05 09:38:34 2009 +0100
+++ b/LamEx.thy	Thu Nov 05 09:55:21 2009 +0100
@@ -33,16 +33,26 @@
 print_theorems
 
 lemma alpha_refl:
-  shows "x \<approx> x"
-  apply (rule rlam.induct)
-  apply (simp_all add:a1 a2)
-  apply (rule a3)
-  apply (simp_all)
-  (* apply (simp add: pt_swap_bij'') *)
+  fixes t::"rlam"
+  shows "t \<approx> t"
+  apply(induct t rule: rlam.induct)
+  apply(simp add: a1)
+  apply(simp add: a2)
+  apply(rule a3)
+  apply(subst pt_swap_bij'')
+  apply(rule pt_name_inst)
+  apply(rule at_name_inst)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma alpha_EQUIV:
+  shows "EQUIV alpha"
 sorry
 
 quotient lam = rlam / alpha
-sorry
+  apply(rule alpha_EQUIV)
+  done
 
 print_quotients
 
@@ -126,12 +136,14 @@
   shows "Lam a t = Lam b s"
 sorry
 
-lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
+lemma perm_rsp: 
+  "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
   sorry
 
-lemma fresh_rsp: "(op = ===> alpha ===> op =) fresh fresh" 
+lemma fresh_rsp: 
+  "(op = ===> alpha ===> op =) fresh fresh" 
   apply(auto)
   (* this is probably only true if some type conditions are imposed *)
   sorry
@@ -190,6 +202,10 @@
 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *}
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
+thm a2
+ML {* val t_a = atomize_thm @{thm a2} *}
+ML {* val t_r = regularize t_a @{typ rlam} @{term alpha} @{thm alpha_EQUIV} @{thm alpha_refl} @{context} *}
+
 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}