146 fun regularize_goal thm rel_eqv rel_refl lthy qtrm =

   147   let

   148     val reg_trm = mk_REGULARIZE_goal @{context} (prop_of thm) qtrm;

   149     fun tac ctxt =

   150       (ObjectLogic.full_atomize_tac) THEN'

   151       REPEAT_ALL_NEW (FIRST' [

   152         rtac rel_refl,

   153         atac,

   154         rtac @{thm universal_twice},

   155         (rtac @{thm impI} THEN' atac),

   156         rtac @{thm implication_twice},

   157         EqSubst.eqsubst_tac ctxt [0]

   158           [(@{thm equiv_res_forall} OF [rel_eqv]),

   159            (@{thm equiv_res_exists} OF [rel_eqv])],

   160         (* For a = b \<longrightarrow> a \<approx> b *)

   161         (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),

   162         (rtac @{thm RIGHT_RES_FORALL_REGULAR})

   163       ]);

   164     val cthm = Goal.prove lthy [] [] reg_trm

   165       (fn {context, ...} => tac context 1);

   166   in

   167     cthm OF [thm]

   168   end

   169 *}

   170 

   171 ML {*

   172 fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =

   173   let

   174     val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));

   175     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'

   176       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));

   177     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);

   178   in

   179     @{thm Pure.equal_elim_rule1} OF [cthm, thm]

   180   end

   181 *}

   182 

   183 

   184 

   185 ML {*

   186 fun atomize_goal thy gl =

   187   let

   188     val vars = map Free (Term.add_frees gl []);

   189     fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm;

   190     val gla = fold lambda_all vars (@{term "Trueprop"} $ gl)

   191     val glf = Type.legacy_freeze gla

   192     val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf))

   193   in

   194     term_of glac

   195   end

   196 *}

   197 

   198 ML {* atomize_goal @{theory} @{term "PLUS a b = PLUS b a"} *}

   199 

   200 

   201 ML {*

   202 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =

   203 let

   204   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

   205   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

   206   val consts = lookup_quot_consts defs;

   207   val t_a = atomize_thm rthm;

   208   val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;

   209   val t_r = regularize_goal t_a rel_eqv rel_refl lthy goal_a;

   210   val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;

   211   val (alls, exs) = findallex lthy rty qty (prop_of t_a);

   212   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls

   213   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs

   214   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t

   215   val abs = findabs rty (prop_of t_a);

   216   val aps = findaps rty (prop_of t_a);

   217   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;

   218   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;

   219   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;

   220   val defs_sym = flat (map (add_lower_defs lthy) defs);

   221   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;

   222   val t_id = simp_ids lthy t_l;

   223   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;

   224   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;

   225   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;

   226   val t_rv = ObjectLogic.rulify t_r

   227 in

   228   Thm.varifyT t_rv

   229 end

   230 *}

   231 

   232 ML {*

   254 

   255 

   256 prove {* reg_artm  *}

   257 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})

   258 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})

   259 done

   260