src/HOL/Tools/function_package/auto_term.ML

use proper RecdefPackage.get_hints;
tuned;

(*  Title:      HOL/Tools/function_package/auto_term.ML
    ID:         $Id$
    Author:     Alexander Krauss, TU Muenchen

A package for general recursive function definitions. 
The auto_term method.
*)


signature FUNDEF_AUTO_TERM =
sig
    val setup : theory -> theory
end

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 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 setup = Method.add_methods
  [("auto_term", Method.simple_args Args.name mk_termination_meth,
    "termination prover for recdef compatibility")]

end