1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/TPTP.thy	Wed Mar 23 10:06:27 2011 +0100
     1.3 @@ -0,0 +1,57 @@
     1.4 +(*  Title:      HOL/ex/TPTP.thy
     1.5 +    Author:     Jasmin Blanchette
     1.6 +    Copyright   2011
     1.7 +
     1.8 +TPTP "IsabelleP" tactic.
     1.9 +*)
    1.10 +
    1.11 +theory TPTP
    1.12 +imports Main
    1.13 +uses "sledgehammer_tactics.ML"
    1.14 +begin
    1.15 +
    1.16 +declare mem_def [simp add]
    1.17 +
    1.18 +declare [[smt_oracle]]
    1.19 +
    1.20 +ML {* proofs := 0 *}
    1.21 +
    1.22 +ML {*
    1.23 +fun SOLVE_TIMEOUT seconds name tac st =
    1.24 +  let
    1.25 +    val result =
    1.26 +      TimeLimit.timeLimit (Time.fromSeconds seconds)
    1.27 +        (fn () => SINGLE (SOLVE tac) st) ()
    1.28 +      handle TimeLimit.TimeOut => NONE
    1.29 +        | ERROR _ => NONE
    1.30 +  in
    1.31 +    (case result of
    1.32 +      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
    1.33 +    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
    1.34 +  end
    1.35 +*}
    1.36 +
    1.37 +ML {*
    1.38 +fun isabellep_tac max_secs =
    1.39 +   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
    1.40 +       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    1.41 +   ORELSE
    1.42 +   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
    1.43 +   ORELSE
    1.44 +   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
    1.45 +   ORELSE
    1.46 +   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
    1.47 +       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    1.48 +   ORELSE
    1.49 +   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
    1.50 +   ORELSE
    1.51 +   SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
    1.52 +   ORELSE
    1.53 +   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
    1.54 +   ORELSE
    1.55 +   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
    1.56 +   ORELSE
    1.57 +   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
    1.58 +*}
    1.59 +
    1.60 +end