--- a/LamEx.thy	Fri Oct 30 16:37:09 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 18:31:06 2009 +0100
@@ -179,7 +179,6 @@
 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *}
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
 
-
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
   Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
@@ -219,6 +218,112 @@
 
 
 
+lemma get_rid: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
+apply (auto)
+done
+
+lemma get_rid2: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+apply (auto)
+done
+
+ML {* val t_a = atomize_thm @{thm alpha.cases} *}
+prove {* build_regularize_goal t_a rty rel @{context}  *}
+  ML_prf {*  fun tac ctxt =
+     (FIRST' [
+      rtac rel_refl,
+      atac,
+      rtac @{thm get_rid},
+      rtac @{thm get_rid2},
+      (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+        [(@{thm equiv_res_forall} OF [rel_eqv]),
+         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
+      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl)
+    ]);
+ *}
+  apply (atomize(full))
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule get_rid)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (simp)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (rule impI)
+  apply (simp)
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule get_rid2)
+  apply (rule impI)
+  apply (simp)
+  apply (tactic {* tac @{context} 1 *})
+  apply (simp)
+  apply (rule get_rid2)
+  apply (rule get_rid)
+  apply (rule get_rid)
+  apply (rule get_rid)
+  apply (rule get_rid2)
+  apply (rule impI)
+  apply (simp)
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule get_rid)
+  apply (rule get_rid2)
+
+
+  apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *})
+ML_prf {*
+fun focus_compose t = Subgoal.FOCUS (fn {concl, ...} =>
+  rtac t 1)
+*}
+thm spec[of _ "x"]
+  apply (rule allI)
+  apply (drule_tac x="a2" in spec)
+  apply (rule impI)
+  apply (erule impE)
+  apply (assumption)
+  apply (rule allI)
+  apply (drule_tac x="P" in spec)
+  apply (atomize(full))
+  apply (rule allI)
+  apply (rule allI)
+  apply (rule allI)
+  apply (rule impI)
+  apply (rule get_rid2)
+
+  thm get_rid2
+  apply (tactic {* compose_tac (false, @{thm get_rid2}, 0) 1 *})
+
+  thm spec
+
+  ML_prf {* val t = snd (Subgoal.focus @{context} 1 (Isar.goal ())) *}
+ML_prf {* Seq.pull (compose_tac (false, @{thm get_rid}, 2) 1 t) *}
+
+
+  thm get_rid
+  apply (rule allI)
+  apply (drule spec)
+
+  thm spec
+  apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *})
+
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule impI)
+  apply (erule impE)
+  apply (assumption)
+  apply (tactic {* tac @{context} 1 *})
+  apply (rule impI)
+  apply (erule impE)
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+  apply (tactic {* tac @{context} 1 *})
+
+ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
+ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
+ML {* val t_a = simp_allex_prs @{context} quot t_l *}
+ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym