--- a/QuotMain.thy	Mon Nov 23 16:13:19 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 20:10:39 2009 +0100
@@ -1441,6 +1441,78 @@
   Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
 *}
 
+(* Final wrappers *)
+
+
+ML {*
+fun regularize_goal lthy thm rel_eqv rel_refl qtrm =
+  let
+    val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;
+    fun tac ctxt =
+      (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})
+      ]);
+    val cthm = Goal.prove lthy [] [] reg_trm
+      (fn {context, ...} => tac context 1);
+  in
+    cthm OF [thm]
+  end
+*}
+
+ML {*
+fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =
+  let
+    val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));
+    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
+      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
+    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
+  in
+    @{thm Pure.equal_elim_rule1} OF [cthm, thm]
+  end
+*}
+
+ML {*
+fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
+let
+  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
+  val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
+  val t_a = atomize_thm rthm;
+  val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;
+  val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;
+  val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;
+  val (alls, exs) = findallex lthy rty qty (prop_of t_a);
+  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
+  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
+  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
+  val abs = findabs rty (prop_of t_a);
+  val aps = findaps rty (prop_of t_a);
+  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
+  val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
+  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
+  val defs_sym = flat (map (add_lower_defs lthy) defs);
+  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
+  val t_id = simp_ids lthy t_l;
+  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
+  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
+  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+  val t_rv = ObjectLogic.rulify t_r
+in
+  Thm.varifyT t_rv
+end
+*}
+
 
 end
 
+