src/HOL/Tools/Function/relation.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/relation.ML	Fri Oct 23 16:37:56 2009 +0200
@@ -0,0 +1,36 @@
+(*  Title:      HOL/Tools/Function/relation.ML
+    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 FUNCTION_RELATION =
+sig
+  val relation_tac: Proof.context -> term -> int -> tactic
+  val setup: theory -> theory
+end
+
+structure Function_Relation : FUNCTION_RELATION =
+struct
+
+fun inst_thm ctxt rel st =
+    let
+      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
+      val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
+      val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
+    in 
+      Drule.cterm_instantiate [(Rvar, rel')] st' 
+    end
+
+fun relation_tac ctxt rel i = 
+    TRY (Function_Common.apply_termination_rule ctxt i)
+    THEN PRIMITIVE (inst_thm ctxt rel)
+
+val setup =
+  Method.setup @{binding relation}
+    (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
+    "proves termination using a user-specified wellfounded relation"
+
+end