author krauss Sat, 02 Jan 2010 23:18:58 +0100 changeset 34229 f66bb6536f6a parent 34228 bc0cea4cae52 child 34230 b0d21ae2528e
simplified
```--- a/src/HOL/Tools/Function/termination.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -194,32 +194,36 @@
| dest_call D t = error "dest_call"

-fun derive_desc_aux thy tac c (vs, _, l', _, r', Gam) m1 m2 D =
+fun mk_desc thy tac vs Gam l r m1 m2 =
+  let
+    fun try rel =
+      try_proof (cterm_of thy
+        (Term.list_all (vs,
+           Logic.mk_implies (HOLogic.mk_Trueprop Gam,
+             HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
+               \$ (m2 \$ r) \$ (m1 \$ l)))))) tac
+  in
+    case try @{const_name HOL.less} of
+       Solved thm => Less thm
+     | Stuck thm =>
+       (case try @{const_name HOL.less_eq} of
+          Solved thm2 => LessEq (thm2, thm)
+        | Stuck thm2 =>
+          if prems_of thm2 = [HOLogic.Trueprop \$ HOLogic.false_const]
+          then False thm2 else None (thm2, thm)
+        | _ => raise Match) (* FIXME *)
+     | _ => raise Match
+end
+
+fun derive_descent thy tac c m1 m2 D =
case get_descent D c m1 m2 of
SOME _ => D
-  | NONE => let
-    fun cgoal rel =
-      Term.list_all (vs,
-        Logic.mk_implies (HOLogic.mk_Trueprop Gam,
-          HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
-            \$ (m2 \$ r') \$ (m1 \$ l'))))
-      |> cterm_of thy
-    in
-      note_descent c m1 m2
-        (case try_proof (cgoal @{const_name HOL.less}) tac of
-           Solved thm => Less thm
-         | Stuck thm =>
-           (case try_proof (cgoal @{const_name HOL.less_eq}) tac of
-              Solved thm2 => LessEq (thm2, thm)
-            | Stuck thm2 =>
-              if prems_of thm2 = [HOLogic.Trueprop \$ HOLogic.false_const]
-              then False thm2 else None (thm2, thm)
-            | _ => raise Match) (* FIXME *)
-         | _ => raise Match) D
-      end
-
-fun derive_descent thy tac c m1 m2 D =
-  derive_desc_aux thy tac c (dest_call D c) m1 m2 D
+  | NONE =>
+    let
+      val (vs, _, l, _, r, Gam) = dest_call D c
+    in
+      note_descent c m1 m2 (mk_desc thy tac vs Gam l r m1 m2) D
+    end

fun CALLS tac i st =
if Thm.no_prems st then all_tac st```