--- a/LFex.thy	Sat Nov 28 03:17:22 2009 +0100
+++ b/LFex.thy	Sat Nov 28 04:02:54 2009 +0100
@@ -182,56 +182,48 @@
 
 thm akind_aty_atrm.induct
 
-lemma left_ball_regular:
-  assumes a: "EQUIV R"
-  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
-apply (rule LEFT_RES_FORALL_REGULAR)
-using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
-apply (simp)
-done
-
-lemma right_bex_regular:
-  assumes a: "EQUIV R"
-  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
-apply (rule RIGHT_RES_EXISTS_REGULAR)
-using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
-apply (simp)
-done
-
-lemma ball_respects_refl:
-  fixes P::"'a \<Rightarrow> bool"
-  and x::"'a"
-  assumes a: "EQUIV R2"
-  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
-apply(rule iffI)
-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)
-apply(simp)
-apply(simp)
-done
-
 ML {*
-fun ball_simproc rel_eqvs ss redex =
+fun ball_reg_eqv_simproc rel_eqvs ss redex =
   let
     val ctxt = Simplifier.the_context ss
     val thy = ProofContext.theory_of ctxt
   in
   case redex of
       (ogl as ((Const (@{const_name "Ball"}, _)) $
-        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) =>
+        ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
+      (let
+        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
+        val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
+        val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
+(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+      in
+        SOME thm
+      end
+      handle _ => NONE
+      )
+  | _ => NONE
+  end
+*}
+
+ML {*
+fun ball_reg_eqv_range_simproc rel_eqvs ss redex =
+  let
+    val ctxt = Simplifier.the_context ss
+    val thy = ProofContext.theory_of ctxt
+  in
+  case redex of
+      (ogl as ((Const (@{const_name "Ball"}, _)) $
+        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
       (let
         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
         val _ = tracing (Syntax.string_of_term ctxt glc);
         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
-        val thm = (@{thm eq_reflection} OF [@{thm ball_respects_refl} OF [eqv]]);
-        val R1c = cterm_of @{theory} R1;
+        val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
+        val R1c = cterm_of thy R1;
         val thmi = Drule.instantiate' [] [SOME R1c] thm;
-        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));
+(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
         val _ = tracing "AAA";
         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
@@ -249,26 +241,22 @@
 ML {*
 fun regularize_tac ctxt rel_eqvs =
   let
-    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs;
-    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs;
-    val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2);
-    val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+    val pat1 = [@{term "Ball (Respects R) P"}];
+    val pat2 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
     val thy = ProofContext.theory_of ctxt
-    val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs))
-  in
-  (ObjectLogic.full_atomize_tac) THEN'
-  (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN'
+    val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))
+    val simproc2 = Simplifier.simproc_i thy "" pat2 (K (ball_reg_eqv_range_simproc rel_eqvs))
+    val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2]
+  in 
+  ObjectLogic.full_atomize_tac THEN'
+  simp_tac simp_ctxt THEN'
   REPEAT_ALL_NEW (FIRST' [
-    (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
-    (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
-    (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-    (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-    (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-    (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
-    (resolve_tac (Inductive.get_monos ctxt)),
+    rtac @{thm ball_reg_right},
+    rtac @{thm bex_reg_left},
+    resolve_tac (Inductive.get_monos ctxt),
     rtac @{thm move_forall},
     rtac @{thm move_exists},
-    (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc]))
+    simp_tac simp_ctxt
   ])
   end
 *}
@@ -337,9 +325,6 @@
     val te = @{thm eq_reflection} OF [t]
     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
     val tl = Thm.lhs_of ts;
-(*    val _ = rrrt := ts;
-    val _ = rrr1 := ctrm;
-    val _ = rrr2 := tl;*)
     val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
     val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
 (*    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
@@ -378,12 +363,6 @@
 ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
 ML_prf {* val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *}
 apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
-thm FORALL_PRS[symmetric]
-ML_prf {*
-fun allex_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [1] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
-  THEN' (quotient_tac quot);
-*}
 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
 ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
 ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}

--- a/QuotMain.thy	Sat Nov 28 03:17:22 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 04:02:54 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 *}
 
@@ -1206,7 +1173,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

--- a/QuotScript.thy	Sat Nov 28 03:17:22 2009 +0100
+++ b/QuotScript.thy	Sat Nov 28 04:02:54 2009 +0100
@@ -429,67 +429,96 @@
 by (auto)
 
 
-(* TODO: Put the following lemmas in proper places *)
 
-lemma equiv_res_forall:
+(* Set of lemmas for regularisation of ball and bex *)
+lemma ball_reg_eqv:
+  fixes P :: "'a \<Rightarrow> bool"
+  assumes a: "EQUIV R"
+  shows "Ball (Respects R) P = (All P)"
+  by (metis EQUIV_def IN_RESPECTS a)
+
+lemma bex_reg_eqv:
   fixes P :: "'a \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  shows "Ball (Respects E) P = (All P)"
-  using a by (metis EQUIV_def IN_RESPECTS a)
+  assumes a: "EQUIV R"
+  shows "Bex (Respects R) P = (Ex P)"
+  by (metis EQUIV_def IN_RESPECTS a)
+
+lemma ball_reg_right:
+  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+  shows "All P \<longrightarrow> Ball R Q"
+  by (metis COMBC_def Collect_def Collect_mem_eq a)
+
+lemma bex_reg_left:
+  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+  shows "Bex R Q \<longrightarrow> Ex P"
+  by (metis COMBC_def Collect_def Collect_mem_eq a)
+
+lemma ball_reg_left:
+  assumes a: "EQUIV R"
+  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+  by (metis EQUIV_REFL IN_RESPECTS a)
 
-lemma equiv_res_exists:
-  fixes P :: "'a \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  shows "Bex (Respects E) P = (Ex P)"
-  using a by (metis EQUIV_def IN_RESPECTS a)
+lemma bex_reg_right:
+  assumes a: "EQUIV R"
+  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+  by (metis EQUIV_REFL IN_RESPECTS a)
 
-lemma FORALL_REGULAR:
+lemma ball_reg_eqv_range:
+  fixes P::"'a \<Rightarrow> bool"
+  and x::"'a"
+  assumes a: "EQUIV R2"
+  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+  apply(rule iffI)
+  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)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma bex_reg_eqv_range:
+  fixes P::"'a \<Rightarrow> bool"
+  and x::"'a"
+  assumes a: "EQUIV R2"
+  shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
+  apply(auto)
+  apply(rule_tac x="\<lambda>y. f x" in bexI)
+  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
+
+lemma all_reg:
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "All P"
   shows "All Q"
   using a b by (metis)
 
-lemma EXISTS_REGULAR:
+lemma ex_reg:
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "Ex P"
   shows "Ex Q"
   using a b by (metis)
 
-lemma RES_FORALL_REGULAR:
+lemma ball_reg:
   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   and     b: "Ball R P"
   shows "Ball R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
-lemma RES_EXISTS_REGULAR:
+lemma bex_reg:
   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   and     b: "Bex R P"
   shows "Bex R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
-lemma LEFT_RES_FORALL_REGULAR:
-  assumes a: "\<And>x. (R x \<and> (Q x \<longrightarrow> P x))"
-  shows "Ball R Q \<longrightarrow> All P"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
 
-lemma RIGHT_RES_FORALL_REGULAR:
-  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
-  shows "All P \<longrightarrow> Ball R Q"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
 
-lemma LEFT_RES_EXISTS_REGULAR:
-  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
-  shows "Bex R Q \<longrightarrow> Ex P"
-  using a by (metis COMBC_def Collect_def Collect_mem_eq)
-
-lemma RIGHT_RES_EXISTS_REGULAR:
-  assumes a: "\<And>x. (R x \<and> (P x \<longrightarrow> Q x))"
-  shows "Ex P \<longrightarrow> Bex R Q"
-  using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 (* TODO: Add similar *)
 lemma RES_FORALL_RSP: