--- a/FSet.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/FSet.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -322,7 +322,7 @@
 
 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
 apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})
-oops
+done
 
 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
@@ -347,7 +347,7 @@
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(rule cheat)
 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
@@ -449,7 +449,7 @@
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply (tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
+apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)

--- a/IntEx.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -149,7 +149,7 @@
 
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
-apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
@@ -189,8 +189,8 @@
 
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
-apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
@@ -226,7 +226,7 @@
 
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}

--- a/LFex.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/LFex.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -182,84 +182,6 @@
 
 thm akind_aty_atrm.induct
 
-ML {*
-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"}, _)) $ 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_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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
-        val _ = tracing "AAA";
-        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
-        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
-      in
-        SOME thm2
-      end
-      handle _ => NONE
-
-      )
-  | _ => NONE
-  end
-*}
-
-ML {*
-fun regularize_tac ctxt rel_eqvs =
-  let
-    val pat1 = [@{term "Ball (Respects R) P"}];
-    val pat2 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
-    val thy = ProofContext.theory_of ctxt
-    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 ball_reg_right},
-    rtac @{thm bex_reg_left},
-    resolve_tac (Inductive.get_monos ctxt),
-    rtac @{thm move_forall},
-    rtac @{thm move_exists},
-    simp_tac simp_ctxt
-  ])
-  end
-*}
 
 ML {* val defs =
   @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
@@ -375,8 +297,24 @@
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *})
-apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<longrightarrow>"]}) 1 *})
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+
+
+
+
 
 
 

--- a/QuotMain.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -488,45 +488,6 @@
 
 *)
 
-lemma universal_twice:
-  assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
-  shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
-using * by auto
-
-lemma implication_twice:
-  assumes a: "c \<longrightarrow> a"
-  assumes b: "b \<longrightarrow> d"
-  shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-using a b by auto
-
-(* version of regularize_tac including debugging information *)
-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),
-    DT ctxt "1" (resolve_tac rel_refl),
-    DT ctxt "2" atac,
-    DT ctxt "3" (rtac @{thm universal_twice}),
-    DT ctxt "4" (rtac @{thm impI} THEN' atac),
-    DT ctxt "5" (rtac @{thm implication_twice}),
-    DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
-      [(@{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 ball_reg_right})
-  ]);
-*}
-
-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
@@ -544,32 +505,169 @@
 *}
 
 ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+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"}, _)) $ 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 bex_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 "Bex"}, _)) $
+        ((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 bex_reg_eqv} OF [eqv]]);
+(*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+      in
+        SOME thm
+      end
+      handle _ => NONE
+      )
+  | _ => NONE
+  end
+*}
+
+ML {*
+fun prep_trm thy (x, (T, t)) =
+  (cterm_of thy (Var (x, T)), cterm_of thy t)
+
+fun prep_ty thy (x, (S, ty)) =
+  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+*}
+
+ML {*
+fun matching_prs thy pat trm =
+let
+  val univ = Unify.matchers thy [(pat, trm)]
+  val SOME (env, _) = Seq.pull univ
+  val tenv = Vartab.dest (Envir.term_env env)
+  val tyenv = Vartab.dest (Envir.type_env env)
+in
+  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+end
 *}
 
-(*
 ML {*
-fun regularize_tac ctxt rel_eqvs rel_refl =
+fun ball_reg_eqv_range_simproc rel_eqvs ss redex =
   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 ctxt = Simplifier.the_context ss
+    val thy = ProofContext.theory_of ctxt
   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' (resolve_tac rel_refl))])
+  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_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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
+        val _ = tracing "AAA";
+        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
+        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
+      in
+        SOME thm2
+      end
+      handle _ => NONE
+
+      )
+  | _ => NONE
   end
 *}
-*)
+
+ML {*
+fun bex_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 "Bex"}, _)) $
+        ((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 bex_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 inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
+        val _ = tracing "AAA";
+        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
+        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
+      in
+        SOME thm2
+      end
+      handle _ => NONE
+
+      )
+  | _ => NONE
+  end
+*}
+
+lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
+by (simp add: EQUIV_REFL)
+
+ML {*
+fun regularize_tac ctxt rel_eqvs =
+  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 rel_eqvs))
+    val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))
+    val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
+    val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
+    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]) rel_eqvs
+  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 *}
 
@@ -779,6 +877,10 @@
 *}
 
 ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
            LAMBDA_RES_TAC ctxt,
@@ -881,6 +983,31 @@
   REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
+ML {*
+fun get_inj_repabs_tac ctxt rel lhs rhs =
+let
+  val _ = tracing "input"
+  val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
+  val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
+  val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
+in  
+  case (rel, lhs, rhs) of
+    (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
+      => rtac @{thm REP_ABS_RSP(1)}
+  | (_, Const (@{const_name "Ball"}, _) $ _, 
+        Const (@{const_name "Ball"}, _) $ _)
+      => rtac @{thm RES_FORALL_RSP}
+  | _ => K no_tac
+end
+*}
+
+ML {* 
+fun inj_repabs_tac ctxt =
+  SUBGOAL (fn (goal, i) =>
+     (case (HOLogic.dest_Trueprop goal) of
+        (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
+      | _ => K no_tac) i)
+*}
 
 section {* Cleaning of the theorem *}
 
@@ -932,26 +1059,6 @@
   THEN' (quotient_tac quot)
 *}
 
-ML {* 
-fun prep_trm thy (x, (T, t)) = 
-  (cterm_of thy (Var (x, T)), cterm_of thy t) 
-
-fun prep_ty thy (x, (S, ty)) = 
-  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) 
-*}
-
-ML {*
-fun matching_prs thy pat trm = 
-let
-  val univ = Unify.matchers thy [(pat, trm)] 
-  val SOME (env, _) = Seq.pull univ
-  val tenv = Vartab.dest (Envir.term_env env)
-  val tyenv = Vartab.dest (Envir.type_env env)
-in
-  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-end 
-*}
-
 (* Rewrites the term with LAMBDA_PRS thm.
 
 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
@@ -1137,12 +1244,12 @@
       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
       val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
     in
-      EVERY1 
-       [rtac rule, 
+      EVERY1
+       [rtac rule,
         RANGE [rtac rthm',
-               regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *)
+               regularize_tac lthy rel_eqv,
                REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
-               clean_tac lthy quot defs aps]] 
+               clean_tac lthy quot defs aps]]
     end) lthy
 *}
 

--- a/QuotScript.thy	Sat Nov 28 05:09:22 2009 +0100
+++ b/QuotScript.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -517,6 +517,13 @@
   shows "Bex R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
+lemma ball_all_comm:
+  "(\<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 bex_ex_comm:
+  "((\<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