# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1258985289 -3600
# Node ID eb15be678ac46184e753b2edbe14b4e4f8befa79
# Parent  2f17bbd47c479b2fb065ca0e2d06d3f595dc7205
lift_thm with a goal.

diff -r 2f17bbd47c47 -r eb15be678ac4 IntEx.thy
--- a/IntEx.thy	Mon Nov 23 14:40:53 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 15:08:09 2009 +0100
@@ -142,6 +142,81 @@
   lift_thm lthy qty ty_name rsp_thms defs t
 *}
 
+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 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
+*}
+
 print_quotients
 ML {* quotdata_lookup @{context} "IntEx.my_int" *}
 ML {* quotdata_lookup @{context} "my_int" *}
@@ -156,6 +231,11 @@
   val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm
 *}
 
+ML {*
+  lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "Trueprop (\<forall>a b. 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} *})