# HG changeset patch # User Cezary Kaliszyk # Date 1259003439 -3600 # Node ID 7e82493c6253c1a2e73892f76cc86112fb83aba1 # Parent 959ef7f6ecdb7d209051659bdb6922eb54a2a86f Finished temporary goal-directed lift_theorem wrapper. diff -r 959ef7f6ecdb -r 7e82493c6253 IntEx.thy --- 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 \ a \ 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 \ 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. diff -r 959ef7f6ecdb -r 7e82493c6253 QuotMain.thy --- 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 \ a \ 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 +