--- a/QuotMain.thy	Mon Oct 26 02:06:01 2009 +0100
+++ b/QuotMain.thy	Mon Oct 26 10:02:50 2009 +0100
@@ -547,6 +547,22 @@
        (regularise (prop_of thm) rty rel lthy))
 *}
 
+ML {*
+fun regularize thm rty rel rel_eqv lthy =
+  let
+    val g = build_regularize_goal thm rty rel lthy;
+    fun tac ctxt =
+       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+        [(@{thm equiv_res_forall} OF [rel_eqv]),
+         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
+         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
+         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
+    val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
+  in
+    cthm OF [thm]
+  end
+*}
+
 section {* RepAbs injection *}
 
 (* Needed to have a meta-equality *)
@@ -616,4 +632,110 @@
   Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
 *}
 
+ML {*
+fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+let
+  val pat = Drule.strip_imp_concl (cprop_of thm)
+  val insts = Thm.match (pat, concl)
+in
+  rtac (Drule.instantiate insts thm) 1
 end
+handle _ => no_tac
+)
+*}
+
+ML {*
+fun res_forall_rsp_tac ctxt =
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+  THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+*}
+
+ML {*
+fun res_exists_rsp_tac ctxt =
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+  THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+*}
+
+
+ML {*
+fun quotient_tac quot_thm =
+  REPEAT_ALL_NEW (FIRST' [
+    rtac @{thm FUN_QUOTIENT},
+    rtac quot_thm,
+    rtac @{thm IDENTITY_QUOTIENT}
+  ])
+*}
+
+ML {*
+fun LAMBDA_RES_TAC ctxt i st =
+  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+    (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | _ => fn _ => no_tac) i st
+*}
+
+ML {*
+fun WEAK_LAMBDA_RES_TAC ctxt i st =
+  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+    (_ $ (_ $ _$(Abs(_,_,_)))) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | (_ $ (_ $ (Abs(_,_,_))$_)) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | _ => fn _ => no_tac) i st
+*}
+
+
+ML {*
+fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
+  (FIRST' [
+    rtac @{thm FUN_QUOTIENT},
+    rtac quot_thm,
+    rtac @{thm IDENTITY_QUOTIENT},
+    rtac @{thm ext},
+    rtac trans_thm,
+    LAMBDA_RES_TAC ctxt,
+    res_forall_rsp_tac ctxt,
+    res_exists_rsp_tac ctxt,
+    (
+     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
+     THEN_ALL_NEW (fn _ => no_tac)
+    ),
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+    rtac refl,
+    (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+    rtac reflex_thm,
+    atac,
+    (
+     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+     THEN_ALL_NEW (fn _ => no_tac)
+    ),
+    WEAK_LAMBDA_RES_TAC ctxt
+    ])
+*}
+
+section {* Cleaning the goal *}
+
+text {* Does the same as 'subst' in a given theorem *}
+ML {*
+fun eqsubst_thm ctxt thms thm =
+  let
+    val goalstate = Goal.init (Thm.cprop_of thm)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_thm"
+    | SOME th => cprem_of th 1
+    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
+    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
+  in
+    Simplifier.rewrite_rule [rt] thm
+  end
+*}
+
+end