# HG changeset patch # User wenzelm # Date 1436448054 -7200 # Node ID 7bf560b196a35bc55e4a209f26ffc904778bc34c # Parent 29e8bdc41f900a33dd835f6aa777ffc398b5938d clarified context; eliminated dead code; diff -r 29e8bdc41f90 -r 7bf560b196a3 src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Thu Jul 09 00:40:57 2015 +0200 +++ b/src/HOL/Library/old_recdef.ML Thu Jul 09 15:20:54 2015 +0200 @@ -219,13 +219,7 @@ rows: int list, TCs: term list list, full_pats_TCs: (term * term list) list} - val wfrec_eqns: theory -> xstring -> thm list -> term list -> - {WFR: term, - SV: term list, - proto_def: term, - extracta: (thm * term list) list, - pats: pattern list} - val mk_induction: theory -> + val mk_induction: Proof.context -> {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm val postprocess: Proof.context -> bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> @@ -2134,60 +2128,6 @@ end; -(*--------------------------------------------------------------------------- - * Perform the extraction without making the definition. Definition and - * extraction commute for the non-nested case. (Deferred recdefs) - * - * The purpose of wfrec_eqns is merely to instantiate the recursion theorem - * and extract termination conditions: no definition is made. - *---------------------------------------------------------------------------*) - -fun wfrec_eqns thy fid tflCongs eqns = - let val ctxt = Proof_Context.init_global thy - val {lhs,rhs} = USyntax.dest_eq (hd eqns) - val (f,args) = USyntax.strip_comb lhs - val (fname,_) = dest_atom f - val (SV,_) = front_last args (* SV = schematic variables *) - val g = list_comb(f,SV) - val h = Free(fname,type_of g) - val eqns1 = map (subst_free[(g,h)]) eqns - val {functional as Abs(x, Ty, _), pats} = mk_functional thy eqns1 - val given_pats = givens pats - (* val f = Free(x,Ty) *) - val Type("fun", [f_dty, f_rty]) = Ty - val _ = if x<>fid then - raise TFL_ERR "wfrec_eqns" - ("Expected a definition of " ^ - quote fid ^ " but found one of " ^ - quote x) - else () - val (case_rewrites,context_congs) = extraction_thms thy - val tych = Thry.typecheck thy - 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) - val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0 - val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM) - val _ = - if !trace then - writeln ("ORIGINAL PROTO_DEF: " ^ - Syntax.string_of_term_global thy proto_def) - else () - val R1 = USyntax.rand WFR - val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM) - val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats - val corollaries' = map (rewrite_rule ctxt case_rewrites) corollaries - val extract = - Rules.CONTEXT_REWRITE_RULE ctxt (f, R1::SV, @{thm cut_apply}, tflCongs @ context_congs) - in {proto_def = proto_def, - SV=SV, - WFR=WFR, - pats=pats, - extracta = map extract corollaries'} - end; - - (*---------------------------------------------------------------------------- * * INDUCTION THEOREM @@ -2238,9 +2178,9 @@ * *---------------------------------------------------------------------------*) -fun mk_case ty_info usednames thy = +fun mk_case ctxt ty_info usednames = let - val ctxt = Proof_Context.init_global thy + val thy = Proof_Context.theory_of ctxt val divide = ipartition (gvvariant usednames) val tych = Thry.typecheck thy fun tych_binding(x,y) = (tych x, tych y) @@ -2290,8 +2230,8 @@ end; -fun complete_cases thy = - let val ctxt = Proof_Context.init_global thy +fun complete_cases ctxt = + let val thy = Proof_Context.theory_of ctxt val tych = Thry.typecheck thy val ty_info = Thry.induct_info thy in fn pats => @@ -2310,8 +2250,8 @@ Rules.GEN ctxt (tych a) (Rules.RIGHT_ASSOC ctxt (Rules.CHOOSE ctxt (tych v, ex_th0) - (mk_case ty_info (vname::aname::names) - thy {path=[v], rows=rows}))) + (mk_case ctxt ty_info (vname::aname::names) + {path=[v], rows=rows}))) end end; @@ -2414,12 +2354,13 @@ * 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 +fun mk_induction ctxt {fconst, R, SV, pat_TCs_list} = +let + val thy = Proof_Context.theory_of ctxt val tych = Thry.typecheck thy 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 case_thm = complete_cases ctxt pats val domain = (type_of o hd) pats val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names) [] (pats::TCsl))) "P" @@ -2454,7 +2395,6 @@ - (*--------------------------------------------------------------------------- * * POST PROCESSING @@ -2661,7 +2601,7 @@ let val _ = writeln "Proving induction theorem ..." val ind = - Prim.mk_induction (Proof_Context.theory_of ctxt) + Prim.mk_induction ctxt {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} val _ = writeln "Postprocessing ..."; val {rules, induction, nested_tcs} =