--- a/LamEx.thy	Wed Nov 25 10:39:53 2009 +0100
+++ b/LamEx.thy	Wed Nov 25 10:52:21 2009 +0100
@@ -218,21 +218,24 @@
 apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})
 done
 
-ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
-lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. \<lbrakk>x = Var a; xa = Var b; a = b\<rbrakk> \<Longrightarrow> P\<Colon>bool;
-     \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = App x xb; xa = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
-     \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. \<lbrakk>x = Lam a x; xa = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
+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>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
     \<Longrightarrow> P"
-apply (tactic {* procedure_tac @{thm alpha.cases} @{context} 1 *})
-sorry
-ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
-lemma "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
+apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *})
+done
+
+ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
+ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
         \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
-(* apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) *)
-sorry
+apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
+apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+done
 
 lemma var_inject: "(Var a = Var b) = (a = b)"
 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})