changeset 113:4ca6534d5d2a

Added a theory that searches for a given theorem To be used non-interactively Used something like this: $ isabelle-process -I < TestProofExists.thy
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 24 Aug 2009 11:10:42 +0200
parents d4c60fc2ac0a
children 3ad2d97896d1
files isabelle/TestProofExists.thy
diffstat 1 files changed, 18 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/isabelle/TestProofExists.thy	Mon Aug 24 11:10:42 2009 +0200
@@ -0,0 +1,18 @@
+theory TestProofExists
+imports "../proof_binary" Main
+begin
+
+ML {*
+  case FindTheorems.find_theorems
+      (ProofContext.init @{theory})
+      (SOME (Goal.init @{cterm "mono (f::nat \<Rightarrow> ('a::linorder)) \<Longrightarrow> e < f u \<longrightarrow> (\<forall>x<l. f x \<le> e) \<longrightarrow> e < f (binsearch f e l u) \<and>
+(\<forall>x<binsearch f e l u. f x \<le> e)"}))
+      (NONE)
+      (true)
+      [(true, FindTheorems.Solves)]
+  of (NONE, _) => exit 127 (* Should never happen, as we remove duplicates *)
+   | (SOME 0, _) => exit 1 (* Nothing was found *)
+   | (SOME _, _) => exit 0 (* One ore more theorems can prove the statement! *)
+  *}
+
+end
\ No newline at end of file