diff -r fafcc54e531d -r 7ef153ded7e2 QuotMain.thy
--- a/QuotMain.thy	Thu Nov 26 19:51:31 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 20:32:33 2009 +0100
@@ -474,41 +474,6 @@
 
 *)
 
-lemma my_equiv_res_forallR:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes b: "(All Q) \<longrightarrow> (All P)"
-  shows "(All Q) \<longrightarrow> Ball (Respects E) P"
-using b by auto
-
-lemma my_equiv_res_forallL:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  assumes b: "(All Q) \<longrightarrow> (All P)"
-  shows "Ball (Respects E) P \<longrightarrow> (All P)"
-using a b
-unfolding EQUIV_def
-by (metis IN_RESPECTS)
-
-lemma my_equiv_res_existsR:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  and     b: "(Ex Q) \<longrightarrow> (Ex P)"
-  shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
-using a b
-unfolding EQUIV_def
-by (metis IN_RESPECTS)
-
-lemma my_equiv_res_existsL:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes b: "(Ex Q) \<longrightarrow> (Ex P)"
-  shows "Bex (Respects E) Q \<longrightarrow> (Ex P)"
-using b
-by (auto)
-
 lemma universal_twice:
   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
   shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
@@ -531,49 +496,15 @@
 in
   Seq.single thm
 end
- 
+
 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
 *}
 
 ML {*
-fun REGULARIZE_tac' lthy rel_refl rel_eqv =
-   (REPEAT1 o FIRST1) 
-     [(K (print_tac "start")) THEN' (K no_tac), 
-      DT lthy "1" (rtac rel_refl),
-      DT lthy "2" atac,
-      DT lthy "3" (rtac @{thm universal_twice}),
-      DT lthy "4" (rtac @{thm impI} THEN' atac),
-      DT lthy "5" (rtac @{thm implication_twice}),
-      DT lthy "6" (rtac @{thm my_equiv_res_forallR}),
-      DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})),
-      (* For a = b \<longrightarrow> a \<approx> b *)
-      DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
-      DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
-*}
-
-ML {*
 fun regularize_tac ctxt rel_eqv rel_refl =
   (ObjectLogic.full_atomize_tac) THEN'
-  REPEAT_ALL_NEW (FIRST' [
-    rtac rel_refl,
-    atac,
-    rtac @{thm universal_twice},
-    rtac @{thm impI} THEN' atac,
-    rtac @{thm implication_twice},
-    EqSubst.eqsubst_tac ctxt [0]
-      [(@{thm equiv_res_forall} OF [rel_eqv]),
-       (@{thm equiv_res_exists} OF [rel_eqv])],
-    (* For a = b \<longrightarrow> a \<approx> b *)
-    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
-    (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-  ]);
-*}
-
-ML {*
-fun regularize_tac ctxt rel_eqv rel_refl =
-  (ObjectLogic.full_atomize_tac) THEN'
-  REPEAT_ALL_NEW (FIRST' 
-   [(K (print_tac "start")) THEN' (K no_tac), 
+  REPEAT_ALL_NEW (FIRST'
+   [(K (print_tac "start")) THEN' (K no_tac),
     DT ctxt "1" (rtac rel_refl),
     DT ctxt "2" atac,
     DT ctxt "3" (rtac @{thm universal_twice}),
@@ -588,7 +519,89 @@
   ]);
 *}
 
-thm RIGHT_RES_FORALL_REGULAR
+lemma move_forall: "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
+by auto
+
+lemma move_exists: "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+by auto
+
+lemma [mono]: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
+by blast
+
+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 =
+  REPEAT_ALL_NEW(FIRST' [
+    FIRST' (map rtac rel_eqvs),
+    rtac @{thm IDENTITY_EQUIV},
+    rtac @{thm LIST_EQUIV}
+  ])
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
+fun regularize_tac ctxt rel_eqvs rel_refl =
+  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)
+  in
+  (ObjectLogic.full_atomize_tac) THEN'
+  (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs))
+  THEN'
+  REPEAT_ALL_NEW (FIRST' [
+    (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
+    (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
+    (resolve_tac (Inductive.get_monos ctxt)),
+    (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    rtac @{thm move_forall},
+    rtac @{thm move_exists},
+    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl)
+  ])
+  end
+*}
 
 section {* Injections of REP and ABSes *}
 
@@ -808,10 +821,6 @@
 *}
 
 ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
-
-ML {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
     rtac trans_thm,
@@ -1285,7 +1294,7 @@
     in
       rtac rule THEN' RANGE [
         rtac rthm',
-        regularize_tac lthy rel_eqv rel_refl,
+        regularize_tac lthy [rel_eqv] rel_refl,
         REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
         clean_tac lthy quot defs reps_same absrep aps
       ]