# HG changeset patch # User wenzelm # Date 1434735901 -7200 # Node ID 1409b4015671c672435dc9278a56eeb14d6f85ae # Parent 52e956416fbf54941e6a19665c2331385aac3947 tuned; diff -r 52e956416fbf -r 1409b4015671 src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Fri Jun 19 19:29:57 2015 +0200 +++ b/src/HOL/Library/old_recdef.ML Fri Jun 19 19:45:01 2015 +0200 @@ -930,25 +930,6 @@ -(*** notable theorems ***) - -structure Thms = -struct - val WFREC_COROLLARY = @{thm tfl_wfrec}; - val WF_INDUCTION_THM = @{thm tfl_wf_induct}; - val CUT_DEF = @{thm tfl_cut_def}; - val eqT = @{thm tfl_eq_True}; - val rev_eq_mp = @{thm tfl_rev_eq_mp}; - val simp_thm = @{thm tfl_simp_thm}; - val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True}; - val imp_trans = @{thm tfl_imp_trans}; - val disj_assoc = @{thm tfl_disj_assoc}; - val tfl_disjE = @{thm tfl_disjE}; - val choose_thm = @{thm tfl_exE}; -end; - - - (*** emulation of HOL inference rules for TFL ***) structure Rules: RULES = @@ -1030,7 +1011,7 @@ fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; -fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans) +fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans}) handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg; @@ -1109,7 +1090,7 @@ val th2' = DISCH disj1 th2; val th3' = DISCH disj2 th3; in - th3' RS (th2' RS (th1 RS Thms.tfl_disjE)) + th3' RS (th2' RS (th1 RS @{thm tfl_disjE})) handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg end; @@ -1237,7 +1218,7 @@ val t$u = Thm.term_of redex val residue = Thm.cterm_of ctxt (Term.betapply (t, u)) in - GEN ctxt fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) + GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE}) handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg end; @@ -1312,7 +1293,7 @@ rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq; -fun RIGHT_ASSOC ctxt = rewrite_rule ctxt [Thms.disj_assoc]; +fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc}; @@ -2087,7 +2068,7 @@ local val f_eq_wfrec_R_M = - #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY)))) + #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl @{thm tfl_wfrec})))) val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M val _ = dest_Free f val (wfrec,_) = USyntax.strip_comb rhs @@ -2142,7 +2123,7 @@ let val thy = Proof_Context.theory_of ctxt val tych = Thry.typecheck thy val f = #lhs(USyntax.dest_eq(concl def)) - val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def + val corollary = Rules.MATCH_MP @{thm tfl_wfrec} def val pats' = filter given pats val given_pats = map pat_of pats' val rows = map row_of_pat pats' @@ -2163,7 +2144,7 @@ val extract = Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs) val (rules, TCs) = ListPair.unzip (map extract corollaries') - val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules + val rules0 = map (rewrite_rule ctxt @{thms tfl_cut_def}) rules val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR) val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0) in @@ -2203,7 +2184,7 @@ else () val (case_rewrites,context_congs) = extraction_thms thy val tych = Thry.typecheck thy - val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY + val WFREC_THM0 = Rules.ISPEC (tych functional) @{thm tfl_wfrec} val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0 val R = Free (singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] eqns)) Rname, Rtype) @@ -2518,14 +2499,14 @@ (*---------------------------------------------------------------------------- * Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)] * - * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove + * Instantiates tfl_wf_induct, getting Sinduct and then tries to prove * recursion induction (Rinduct) by proving the antecedent of Sinduct from * the antecedent of Rinduct. *---------------------------------------------------------------------------*) fun mk_induction thy {fconst, R, SV, pat_TCs_list} = let val ctxt = Proof_Context.init_global thy val tych = Thry.typecheck thy - val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM) + val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) @{thm tfl_wf_induct}) val (pats,TCsl) = ListPair.unzip pat_TCs_list val case_thm = complete_cases thy pats val domain = (type_of o hd) pats @@ -2580,7 +2561,7 @@ if (can (Thry.match_term thy asm) tc) then Rules.UNDISCH (Rules.MATCH_MP - (Rules.MATCH_MP Thms.simp_thm (Rules.DISCH (tych asm) ind)) + (Rules.MATCH_MP @{thm tfl_simp_thm} (Rules.DISCH (tych asm) ind)) hth) else loop rst in loop asl @@ -2623,7 +2604,7 @@ * The termination condition (tc) is simplified to |- tc = tc' (there * might not be a change!) and then 3 attempts are made: * - * 1. if |- tc = T, then eliminate it with eqT; otherwise, + * 1. if |- tc = T, then eliminate it with tfl_eq_True; otherwise, * 2. apply the terminator to tc'. If |- tc' = T then eliminate; else * 3. replace tc by tc' in both the rules and the induction theorem. *---------------------------------------------------------------------*) @@ -2634,14 +2615,14 @@ val tc_eq = simplifier tc1 val _ = trace_thms ctxt "result: " [tc_eq] in - elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind) + elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind) handle Utils.ERR _ => - (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq) + (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq) (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)), terminator))) (r,ind) handle Utils.ERR _ => - (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq), + (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq), simplify_induction thy tc_eq ind)) end @@ -2662,9 +2643,9 @@ let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc))) in Rules.GEN_ALL ctxt - (Rules.MATCH_MP Thms.eqT tc_eq + (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq handle Utils.ERR _ => - (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq) + (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq) (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)), terminator)) handle Utils.ERR _ => tc_eq))