author krauss Fri, 08 Aug 2008 09:44:16 +0200 changeset 27790 37b4e65d1dbf parent 27789 1bf827e3258d child 27791 23d2567c578e
FundefLib.try_proof : attempt a proof and see if it works
```--- a/src/HOL/Tools/function_package/fundef_lib.ML	Fri Aug 08 09:26:15 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Fri Aug 08 09:44:16 2008 +0200
@@ -134,4 +134,12 @@
|> rev

+datatype proof_attempt = Solved of thm | Stuck of thm | Fail
+
+fun try_proof cgoal tac =
+    case SINGLE tac (Goal.init cgoal) of
+      NONE => Fail
+    | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
+
+
end```
```--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Aug 08 09:26:15 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Aug 08 09:44:16 2008 +0200
@@ -16,6 +16,8 @@
structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
struct

+open FundefLib
+
(** General stuff **)

fun mk_measures domT mfuns =
@@ -79,21 +81,18 @@

fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
let
-      val goals = mk_goal (vars, prems, mfun \$ lhs, mfun \$ rhs)
-      val less_thm = goals @{const_name HOL.less} |> prove thy solve_tac
+      val goals = cterm_of thy o mk_goal (vars, prems, mfun \$ lhs, mfun \$ rhs)
in
-      if Thm.no_prems less_thm then
-        Less (Goal.finish less_thm)
-      else
-        let
-          val lesseq_thm = goals @{const_name HOL.less_eq} |> prove thy solve_tac
-        in
-          if Thm.no_prems lesseq_thm then
-            LessEq (Goal.finish lesseq_thm, less_thm)
-          else
-            if prems_of lesseq_thm = [HOLogic.Trueprop \$ HOLogic.false_const] then False lesseq_thm
-            else None (lesseq_thm, less_thm)
-        end
+      case try_proof (goals @{const_name HOL.less}) solve_tac of
+        Solved thm => Less thm
+      | Stuck thm =>
+        (case try_proof (goals @{const_name HOL.less_eq}) solve_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
end

```