--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 08:16:34 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 09:51:39 2010 +0100
@@ -235,16 +235,14 @@
 apply(erule alpha.cases)
 apply(simp_all)
 apply(simp add: a2)
-apply(rotate_tac 1)
 apply(erule alpha.cases)
 apply(simp_all)
+apply(rule a3)
 apply(simp add: alpha_gen.simps)
 apply(erule conjE)+
 apply(erule exE)+
 apply(erule conjE)+
-apply(rule a3)
 apply(rule_tac x="pia + pi" in exI)
-apply(simp add: alpha_gen.simps)
 apply(simp add: fresh_star_plus)
 apply(drule_tac x="- pia \<bullet> sa" in spec)
 apply(drule mp)
@@ -407,6 +405,7 @@
 apply auto
 done
 
+(*
 (* pi_abs would be also sufficient to prove the next lemma *)
 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
 apply (unfold rep_lam_def)
@@ -415,12 +414,12 @@
 lemma [quot_preserve]: "(prod_fun id rep_lam --->
            (abs_lam ---> abs_lam ---> id) ---> (abs_lam ---> id) ---> id ---> (prod_fun id rep_lam) ---> id)
            alpha_gen = alpha_gen"
-apply (simp add: expand_fun_eq)
-apply (simp add: alpha_gen.simps)
+apply (simp add: expand_fun_eq alpha_gen.simps Quotient_abs_rep[OF Quotient_lam])
 apply (simp add: replam_eqvt)
 apply (simp only: Quotient_abs_rep[OF Quotient_lam])
 apply auto
 done
+*)
 
 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)"
 apply (simp add: expand_fun_eq)
@@ -429,24 +428,26 @@
 
 lemma a3:
   "\<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s) \<Longrightarrow> Lam a t = Lam b s"
-  apply (lifting a3)
+  apply (unfold alpha_gen)
+  apply (lifting a3[unfolded alpha_gen])
   done
 
 
 lemma a3_inv:
   "Lam a t = Lam b s \<Longrightarrow> \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)"
-apply(lifting a3_inverse)
-done
+  apply (unfold alpha_gen)
+  apply (lifting a3_inverse[unfolded alpha_gen])
+  done
 
 lemma alpha_cases: 
   "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
-    \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
+    \<And>t1 t2 s1 s2. \<lbrakk>a1 = App t1 s1; a2 = App t2 s2; t1 = t2; s1 = s2\<rbrakk> \<Longrightarrow> P;
     \<And>a t b s. \<lbrakk>a1 = Lam a t; a2 = Lam b s; \<exists>pi. ({atom a}, t) \<approx>gen (op =) fv pi ({atom b}, s)\<rbrakk>
    \<Longrightarrow> P\<rbrakk>
     \<Longrightarrow> P"
-  by (lifting alpha.cases)
-
-thm alpha.induct
+unfolding alpha_gen
+apply (lifting alpha.cases[unfolded alpha_gen])
+done
 
 (* not sure whether needed *)
 lemma alpha_induct: 
@@ -454,7 +455,7 @@
     \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
  \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
-  by (lifting alpha.induct)
+unfolding alpha_gen by (lifting alpha.induct[unfolded alpha_gen])
 
 (* should they lift automatically *)
 lemma lam_inject [simp]: