--- a/QuotMain.thy	Sun Dec 06 13:41:42 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 23:32:27 2009 +0100
@@ -503,6 +503,11 @@
 *}
 
 ML {*
+fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
+val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+*}
+
+ML {*
 fun ball_reg_eqv_simproc ss redex =
   let
     val ctxt = Simplifier.the_context ss
@@ -601,8 +606,10 @@
   end
 *}
 
-thm ball_reg_eqv_range
+
 thm bex_reg_eqv_range
+thm ball_reg_eqv
+thm bex_reg_eqv
 
 ML {*
 fun bex_reg_eqv_range_simproc ss redex =
@@ -638,6 +645,7 @@
 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 by (simp add: equivp_reflp)
 
+(* does not work yet
 ML {*
 fun regularize_tac ctxt =
   let
@@ -650,12 +658,14 @@
     val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
-    val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
-    (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
+    val simp_set = HOL_basic_ss addsimps @{thms ball_reg_eqv bex_reg_eqv}
+                                 addsimprocs [simproc3, simproc4]
+                                 addSolver equiv_solver
+    * TODO: Make sure that there are no list_rel, pair_rel etc involved *
     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
   in
   ObjectLogic.full_atomize_tac THEN'
-  simp_tac simp_ctxt THEN'
+  simp_tac simp_set THEN'
   REPEAT_ALL_NEW (FIRST' [
     rtac @{thm ball_reg_right},
     rtac @{thm bex_reg_left},
@@ -663,9 +673,38 @@
     rtac @{thm ball_all_comm},
     rtac @{thm bex_ex_comm},
     resolve_tac eq_eqvs,
-    simp_tac simp_ctxt
+    simp_tac simp_set
   ])
   end
+*}*)
+
+ML {*
+fun regularize_tac ctxt =
+let
+  val pat1 = [@{term "Ball (Respects R) P"}];
+  val pat2 = [@{term "Bex (Respects R) P"}];
+  val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+  val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
+  val thy = ProofContext.theory_of ctxt
+  val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
+  val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
+  val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
+  val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
+  val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
+  (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
+  val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
+in
+  ObjectLogic.full_atomize_tac THEN'
+  simp_tac simp_ctxt THEN'
+  REPEAT_ALL_NEW (FIRST' [
+     rtac @{thm ball_reg_right},
+     rtac @{thm bex_reg_left},
+     resolve_tac (Inductive.get_monos ctxt),
+     rtac @{thm ball_all_comm},
+     rtac @{thm bex_ex_comm},
+     resolve_tac eq_eqvs,
+     simp_tac simp_ctxt])
+end
 *}
 
 section {* Injections of rep and abses *}