--- a/QuotMain.thy	Tue Nov 24 14:16:57 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 14:19:54 2009 +0100
@@ -1528,6 +1528,67 @@
   end
 *}
 
+lemma procedure:
+  assumes a: "A"
+  and     b: "A \<Longrightarrow> B"
+  and     c: "B = C"
+  and     d: "C = D"
+  shows   "D"
+  using a b c d
+  by simp
+
+ML {* 
+fun procedure_inst ctxt rtrm qtrm =
+let
+  val thy = ProofContext.theory_of ctxt
+  val rtrm' = HOLogic.dest_Trueprop rtrm
+  val qtrm' = HOLogic.dest_Trueprop qtrm
+  val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+  val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
+in
+  Drule.instantiate' []
+    [SOME (cterm_of thy rtrm'),
+     SOME (cterm_of thy reg_goal),
+     SOME (cterm_of thy inj_goal)]
+  @{thm procedure}
+end
+
+fun procedure_tac rthm =
+  Subgoal.FOCUS (fn {context, concl, ...} =>
+    let
+      val rthm' = atomize_thm rthm
+      val rule = procedure_inst context (prop_of rthm') (term_of concl)
+    in
+      EVERY1 [rtac rule, rtac rthm']
+    end)
+*}
+
+(* FIXME: allex_prs and lambda_prs can be one function *)
+
+ML {*
+fun allex_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
+  THEN' (quotient_tac quot);
+*}
+
+ML {*
+fun lambda_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}
+  THEN' (RANGE [quotient_tac quot, quotient_tac quot]));
+*}
+
+ML {*
+fun clean_tac lthy quot defs reps_same =
+  let
+    val lower = flat (map (add_lower_defs lthy) defs)
+  in
+    (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
+    (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
+    (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
+    (simp_tac (HOL_ss addsimps [reps_same]))
+  end
+*}
+
 
 end