--- a/QuotMain.thy	Sat Nov 28 04:37:04 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 04:37:30 2009 +0100
@@ -511,11 +511,11 @@
     DT ctxt "4" (rtac @{thm impI} THEN' atac),
     DT ctxt "5" (rtac @{thm implication_twice}),
     DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
-      [(@{thm equiv_res_forall} OF [rel_eqv]),
-       (@{thm equiv_res_exists} OF [rel_eqv])]),
+      [(@{thm ball_reg_eqv} OF [rel_eqv]),
+       (@{thm ball_reg_eqv} OF [rel_eqv])]),
     (* For a = b \<longrightarrow> a \<approx> b *)
     DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)),
-    DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+    DT ctxt "8" (rtac @{thm ball_reg_right})
   ]);
 *}
 
@@ -534,41 +534,6 @@
 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
 by auto
 
-lemma ball_respects_refl:
-  fixes P Q::"'a \<Rightarrow> bool"
-  and x::"'a"
-  assumes a: "EQUIV R2"
-  and     b: "\<And>f. Q (f x) \<longrightarrow> P (f x)"
-  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))"
-apply(rule impI)
-apply(rule allI)
-apply(drule_tac x="\<lambda>y. f x" in bspec)
-apply(simp add: Respects_def IN_RESPECTS)
-apply(rule impI)
-using a EQUIV_REFL_SYM_TRANS[of "R2"]
-apply(simp add: REFL_def)
-using b
-apply(simp)
-done
-
-lemma bex_respects_refl:
-  fixes P Q::"'a \<Rightarrow> bool"
-  and x::"'a"
-  assumes a: "EQUIV R2"
-  and     b: "\<And>f. P (f x) \<longrightarrow> Q (f x)"
-  shows   "(Ex (\<lambda>f. P (f x))) \<longrightarrow> (Bex (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)))"
-apply(rule impI)
-apply(erule exE)
-thm bexI
-apply(rule_tac x="\<lambda>y. f x" in bexI)
-using b
-apply(simp)
-apply(simp add: Respects_def IN_RESPECTS)
-apply(rule impI)
-using a EQUIV_REFL_SYM_TRANS[of "R2"]
-apply(simp add: REFL_def)
-done
-
 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
 ML {*
 fun equiv_tac rel_eqvs =
@@ -582,6 +547,7 @@
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 *}
 
+(*
 ML {*
 fun regularize_tac ctxt rel_eqvs rel_refl =
   let
@@ -603,6 +569,7 @@
      (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))])
   end
 *}
+*)
 
 section {* Injections of REP and ABSes *}
 
@@ -1015,6 +982,13 @@
 end 
 *}
 
+(* Rewrites the term with LAMBDA_PRS thm.
+
+Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
+    with: f
+
+It proves the QUOTIENT assumptions by calling quotient_tac
+ *)
 ML {*
 fun lambda_prs_conv1 ctxt quot_thms ctrm =
   case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
@@ -1196,7 +1170,7 @@
       EVERY1 
        [rtac rule, 
         RANGE [rtac rthm',
-               regularize_tac lthy rel_eqv rel_refl,
+               regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *)
                REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
                clean_tac lthy quot defs aps]] 
     end) lthy