--- a/IntEx.thy	Mon Nov 23 16:13:19 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 20:10:39 2009 +0100
@@ -143,93 +143,6 @@
 *}
 
 ML {*
-fun regularize_goal thm rel_eqv rel_refl lthy qtrm =
-  let
-    val reg_trm = mk_REGULARIZE_goal @{context} (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 atomize_goal thy gl =
-  let
-    val vars = map Free (Term.add_frees gl []);
-    fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm;
-    val gla = fold lambda_all vars (@{term "Trueprop"} $ gl)
-    val glf = Type.legacy_freeze gla
-    val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf))
-  in
-    term_of glac
-  end
-*}
-
-ML {* atomize_goal @{theory} @{term "PLUS a b = PLUS b a"} *}
-
-
-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 consts = lookup_quot_consts defs;
-  val t_a = atomize_thm rthm;
-  val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;
-  val t_r = regularize_goal t_a rel_eqv rel_refl lthy 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
-*}
-
-ML {*
 fun lift_thm_g_my_int lthy t g =
   lift_thm_goal lthy qty ty_name rsp_thms defs t g
 *}
@@ -238,27 +151,14 @@
 ML {* quotdata_lookup @{context} "IntEx.my_int" *}
 ML {* quotdata_lookup @{context} "my_int" *}
 
-ML {* 
-  val test = lift_thm_my_int @{context} @{thm plus_sym_pre} 
-*}
-
 ML {*
-  val aqtrm = (prop_of (atomize_thm test))
-  val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) 
-  val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm
+  val test = lift_thm_my_int @{context} @{thm plus_sym_pre}
 *}
 
 ML {*
   lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "PLUS a b = PLUS b a"}
 *}
 
-
-prove {* reg_artm  *}
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
-apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
-done
-
-
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
   apply (cases i)
@@ -269,21 +169,10 @@
 
 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
-ML {*
-  val arthm = atomize_thm @{thm plus_assoc_pre}
-  val aqthm = atomize_thm test2
-  val aqtrm = prop_of aqthm
-  val artrm = prop_of arthm
-*}
+ML {* lift_thm_g_my_int @{context} @{thm plus_assoc_pre} @{term "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"} *}
 
-prove testtest: {* mk_REGULARIZE_goal @{context} artrm aqtrm  *}
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
-apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
-done
 
-ML {* @{thm testtest} OF [arthm] *}
 
-ML {* val reg_atrm = prop_of (@{thm testtest} OF [arthm]) *}
 
 (*
 does not work.

--- 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
 
+