# HG changeset patch
# User blanchet
# Date 1300815509 -3600
# Node ID a2a69b32d8999cc49cfe23ca6aa965a68ff53763
# Parent  9fe5daa2e7059985fbe3420e4fc3b7f2c289ed08
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers

diff -r 9fe5daa2e705 -r a2a69b32d899 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Mar 22 18:27:47 2011 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 22 18:38:29 2011 +0100
@@ -466,8 +466,8 @@
   Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
   Library/Sum_of_Squares/sos_wrapper.ML					\
   Library/Sum_of_Squares/sum_of_squares.ML				\
-  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
-  Library/While_Combinator.thy Library/Zorn.thy				\
+  Library/TPTP.thy Library/Transitive_Closure_Table.thy			\
+  Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy	\
   $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
   Library/reflection.ML Library/reify_data.ML				\
   Library/Quickcheck_Narrowing.thy \
diff -r 9fe5daa2e705 -r a2a69b32d899 src/HOL/Library/TPTP.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/TPTP.thy	Tue Mar 22 18:38:29 2011 +0100
@@ -0,0 +1,50 @@
+theory TPTP
+imports Main
+uses "~~/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML"
+begin
+
+declare mem_def [simp add]
+
+declare [[smt_oracle]]
+
+ML {* proofs := 0 *}
+
+ML {*
+fun SOLVE_TIMEOUT seconds name tac st =
+  let
+    val result =
+      TimeLimit.timeLimit (Time.fromSeconds seconds)
+        (fn () => SINGLE (SOLVE tac) st) ()
+      handle TimeLimit.TimeOut => NONE
+        | ERROR _ => NONE
+  in
+    (case result of
+      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
+  end
+*}
+
+ML {*
+fun isabellep_tac max_secs =
+   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
+       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
+       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
+   ORELSE
+   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
+*}
+
+end