Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/auto_term.ML
author krauss
Wed, 18 Apr 2007 11:37:43 +0200
changeset 22725 83099f0a9d8d
parent 22496 1f428200fd9c
child 22733 0b14bb35be90
permissions -rw-r--r--
added temporary hack to avoid schematic goals in "termination".

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

A package for general recursive function definitions.
Method "relation" to commence a termination proof using a user-specified relation.
*)

signature FUNDEF_RELATION =
sig
  val relation_tac: Proof.context -> term -> int -> tactic
  val setup: theory -> theory
end

structure FundefRelation : FUNDEF_RELATION =
struct

fun relation_tac ctxt rel =
    let
      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)

      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
      val rule = FundefCommon.get_termination_rule ctxt |> the
                  |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)

      val _ $ premise $ _ = Thm.prop_of rule
      val Rvar = cert (Var (the_single (Term.add_vars premise [])))
    in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end


val setup = Method.add_methods
  [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
    "proves termination using a user-specified wellfounded relation")]

end
isabelle