# HG changeset patch
# User krauss
# Date 1218181456 -7200
# Node ID 37b4e65d1dbf86d6c54a60f63c6380c7575a07d7
# Parent  1bf827e3258d3daed9891a6b8ad7706bba5af618
FundefLib.try_proof : attempt a proof and see if it works

diff -r 1bf827e3258d -r 37b4e65d1dbf src/HOL/Tools/function_package/fundef_lib.ML
--- 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
diff -r 1bf827e3258d -r 37b4e65d1dbf src/HOL/Tools/function_package/lexicographic_order.ML
--- 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