1.1 --- a/src/HOL/Tools/function_package/auto_term.ML	Sat Oct 07 01:30:58 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Sat Oct 07 01:31:01 2006 +0200
     1.3 @@ -2,50 +2,49 @@
     1.4      ID:         $Id$
     1.5      Author:     Alexander Krauss, TU Muenchen
     1.6  
     1.7 -A package for general recursive function definitions. 
     1.8 +A package for general recursive function definitions.
     1.9  The auto_term method.
    1.10  *)
    1.11  
    1.12  
    1.13  signature FUNDEF_AUTO_TERM =
    1.14  sig
    1.15 -    val setup : theory -> theory
    1.16 +  val setup: theory -> theory
    1.17  end
    1.18  
    1.19 -structure FundefAutoTerm : FUNDEF_AUTO_TERM = 
    1.20 +structure FundefAutoTerm : FUNDEF_AUTO_TERM =
    1.21  struct
    1.22  
    1.23  open FundefCommon
    1.24  open FundefAbbrev
    1.25  
    1.26  
    1.27 +fun auto_term_tac ctxt rule rel wf_rules ss =
    1.28 +  let
    1.29 +    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    1.30  
    1.31 -fun auto_term_tac tc_intro_rule relstr wf_rules ss =
    1.32 -    (resolve_tac [tc_intro_rule] 1)                    (* produce the usual goals *)
    1.33 -        THEN (instantiate_tac [("R", relstr)])    (* instantiate with the given relation *)
    1.34 -        THEN (ALLGOALS 
    1.35 -                  (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
    1.36 -                    | i => asm_simp_tac ss i))    (* Simplify termination conditions *)
    1.37 +    val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
    1.38 +    val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
    1.39 +    val prem = #1 (Logic.dest_implies (Thm.prop_of rule'))
    1.40 +    val R' = cert (Var (the_single (Term.add_vars prem [])))
    1.41 +  in
    1.42 +    resolve_tac [Drule.cterm_instantiate [(R', rel')] rule'] 1  (* produce the usual goals *)
    1.43 +    THEN (ALLGOALS
    1.44 +      (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
    1.45 +        | i => asm_simp_tac ss i))             (* Simplify termination conditions *)
    1.46 +  end
    1.47  
    1.48 -fun mk_termination_meth relstr ctxt =
    1.49 -    let
    1.50 -        val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt)
    1.51 -        val ss = local_simpset_of ctxt addsimps simps
    1.52 -            
    1.53 -        val intro_rule = ProofContext.get_thm ctxt (Name "termination")
    1.54 -          (* FIXME avoid internal name lookup -- dynamic scoping! *)
    1.55 -    in
    1.56 -        Method.RAW_METHOD (K (auto_term_tac
    1.57 -                                  intro_rule
    1.58 -                                  relstr
    1.59 -                                  wfs
    1.60 -                                  ss))
    1.61 -    end
    1.62  
    1.63 +fun termination_meth src = Method.syntax Args.term src #> (fn (ctxt, rel) =>
    1.64 +  let
    1.65 +    val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt)
    1.66 +    val ss = local_simpset_of ctxt addsimps simps
    1.67  
    1.68 +    val intro_rule = ProofContext.get_thm ctxt (Name "termination")
    1.69 +    (* FIXME avoid internal name lookup -- dynamic scoping! *)
    1.70 +  in Method.RAW_METHOD (K (auto_term_tac ctxt intro_rule rel wfs ss)) end)
    1.71  
    1.72  val setup = Method.add_methods
    1.73 -  [("auto_term", Method.simple_args Args.name mk_termination_meth,
    1.74 -    "termination prover for recdef compatibility")]
    1.75 +  [("auto_term", termination_meth, "termination prover for recdef compatibility")]
    1.76  
    1.77  end