src/HOL/Tools/function_package/descent.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/descent.ML	Tue Dec 16 08:46:07 2008 +0100
@@ -0,0 +1,44 @@
+(*  Title:       HOL/Tools/function_package/descent.ML
+    Author:      Alexander Krauss, TU Muenchen
+
+Descent proofs for termination
+*)
+
+
+signature DESCENT =
+sig
+
+  val derive_diag : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+                    -> Termination.data -> int -> tactic
+
+  val derive_all  : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+                    -> Termination.data -> int -> tactic
+
+end
+
+
+structure Descent : DESCENT =
+struct
+
+fun gen_descent diag ctxt tac cont D = Termination.CALLS (fn (cs, i) =>
+  let
+    val thy = ProofContext.theory_of ctxt
+    val measures_of = Termination.get_measures D
+
+    fun derive c D =
+      let
+        val (_, p, _, q, _, _) = Termination.dest_call D c
+      in
+        if diag andalso p = q
+        then fold (fn m => Termination.derive_descent thy tac c m m) (measures_of p) D
+        else fold_product (Termination.derive_descent thy tac c)
+               (measures_of p) (measures_of q) D
+      end
+  in
+    cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
+  end)
+
+val derive_diag = gen_descent true
+val derive_all = gen_descent false
+
+end