--- a/Quot/Examples/IntEx.thy	Mon Dec 07 15:21:51 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 17:57:33 2009 +0100
@@ -255,12 +255,59 @@
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by simp
 
+(* test about lifting identity equations *)
 
-lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
-defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac  @{context} 1 *})
+ML {*
+(* helper code from QuotMain *)
+val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
+val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
+val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+val simpset = (mk_minimal_ss @{context}) 
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
+                       addsimprocs [simproc] addSolver equiv_solver
+*}
+
+(* What regularising does *)
+(*========================*)
+
+(* 0. preliminary simplification step *)
+thm ball_reg_eqv bex_reg_eqv babs_reg_eqv
+    ball_reg_eqv_range bex_reg_eqv_range
+(* 1. first two rtacs *)
+thm ball_reg_right bex_reg_left
+(* 2. monos *)
+(* 3. commutation rules *)
+thm ball_all_comm bex_ex_comm
+(* 4. then rel-equality *)
+thm eq_imp_rel
+(* 5. then simplification like 0 *)
+(* finally jump to 1 *)
+
+
+(* What cleaning does *)
+(*====================*)
+
+(* 1. conversion *)
+thm lambda_prs
+(* 2. simplification with *)
+thm all_prs ex_prs
+(* 3. Simplification with *)
+thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep
+(* 4. Test for refl *)
+
+lemma
+  shows "equivp (op \<approx>)"
+  and   "equivp ((op \<approx>) ===> (op \<approx>))"
+apply -
+apply(tactic {* equiv_tac @{context} 1 *})
+apply(tactic {* equiv_tac @{context} 1 *})?
+oops
+
+
+lemma
+  "(\<lambda>y. y) = (\<lambda>x. x) \<longrightarrow>
+    (op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))"
+apply(tactic {* simp_tac simpset  1 *})
 sorry
 
 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
@@ -268,6 +315,7 @@
 
 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})
+apply(tactic {* regularize_tac @{context} 1*})?
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})