# HG changeset patch # User wenzelm # Date 1160177461 -7200 # Node ID 4066ee15b278ef106cf425c55db41226c5e262e8 # Parent 528054ca23e321e288838450788dd58b966c6957 tuned method syntax: polymorhic term argument; tuned rule instantiation; diff -r 528054ca23e3 -r 4066ee15b278 src/HOL/Tools/function_package/auto_term.ML --- a/src/HOL/Tools/function_package/auto_term.ML Sat Oct 07 01:30:58 2006 +0200 +++ b/src/HOL/Tools/function_package/auto_term.ML Sat Oct 07 01:31:01 2006 +0200 @@ -2,50 +2,49 @@ ID: $Id$ Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. +A package for general recursive function definitions. The auto_term method. *) signature FUNDEF_AUTO_TERM = sig - val setup : theory -> theory + val setup: theory -> theory end -structure FundefAutoTerm : FUNDEF_AUTO_TERM = +structure FundefAutoTerm : FUNDEF_AUTO_TERM = struct open FundefCommon open FundefAbbrev - -fun auto_term_tac tc_intro_rule relstr wf_rules ss = - (resolve_tac [tc_intro_rule] 1) (* produce the usual goals *) - THEN (instantiate_tac [("R", relstr)]) (* instantiate with the given relation *) - THEN (ALLGOALS - (fn 1 => REPEAT (ares_tac wf_rules 1) (* Solve wellfoundedness *) - | i => asm_simp_tac ss i)) (* Simplify termination conditions *) +fun auto_term_tac ctxt rule rel wf_rules ss = + let + val cert = Thm.cterm_of (ProofContext.theory_of ctxt) -fun mk_termination_meth relstr ctxt = - let - val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt) - val ss = local_simpset_of ctxt addsimps simps - - val intro_rule = ProofContext.get_thm ctxt (Name "termination") - (* FIXME avoid internal name lookup -- dynamic scoping! *) - in - Method.RAW_METHOD (K (auto_term_tac - intro_rule - relstr - wfs - ss)) - end + val rel' = cert (singleton (Variable.polymorphic ctxt) rel) + val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) + val prem = #1 (Logic.dest_implies (Thm.prop_of rule')) + val R' = cert (Var (the_single (Term.add_vars prem []))) + in + resolve_tac [Drule.cterm_instantiate [(R', rel')] rule'] 1 (* produce the usual goals *) + THEN (ALLGOALS + (fn 1 => REPEAT (ares_tac wf_rules 1) (* Solve wellfoundedness *) + | i => asm_simp_tac ss i)) (* Simplify termination conditions *) + end +fun termination_meth src = Method.syntax Args.term src #> (fn (ctxt, rel) => + let + val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt) + val ss = local_simpset_of ctxt addsimps simps + + val intro_rule = ProofContext.get_thm ctxt (Name "termination") + (* FIXME avoid internal name lookup -- dynamic scoping! *) + in Method.RAW_METHOD (K (auto_term_tac ctxt intro_rule rel wfs ss)) end) val setup = Method.add_methods - [("auto_term", Method.simple_args Args.name mk_termination_meth, - "termination prover for recdef compatibility")] + [("auto_term", termination_meth, "termination prover for recdef compatibility")] end