src/HOL/ex/TPTP.thy
author blanchet
Wed Mar 23 10:06:27 2011 +0100 (2011-03-23)
changeset 42071 04577a7e0c51
parent 42063 src/HOL/Library/TPTP.thy@a2a69b32d899
child 42078 d5bf0ce40bd7
permissions -rw-r--r--
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
default to "e" rather than "vampire" since E is part of the Isabelle bundle
     1 (*  Title:      HOL/ex/TPTP.thy
     2     Author:     Jasmin Blanchette
     3     Copyright   2011
     4 
     5 TPTP "IsabelleP" tactic.
     6 *)
     7 
     8 theory TPTP
     9 imports Main
    10 uses "sledgehammer_tactics.ML"
    11 begin
    12 
    13 declare mem_def [simp add]
    14 
    15 declare [[smt_oracle]]
    16 
    17 ML {* proofs := 0 *}
    18 
    19 ML {*
    20 fun SOLVE_TIMEOUT seconds name tac st =
    21   let
    22     val result =
    23       TimeLimit.timeLimit (Time.fromSeconds seconds)
    24         (fn () => SINGLE (SOLVE tac) st) ()
    25       handle TimeLimit.TimeOut => NONE
    26         | ERROR _ => NONE
    27   in
    28     (case result of
    29       NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
    30     | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
    31   end
    32 *}
    33 
    34 ML {*
    35 fun isabellep_tac max_secs =
    36    SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
    37        (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    38    ORELSE
    39    SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
    40    ORELSE
    41    SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
    42    ORELSE
    43    SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
    44        THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    45    ORELSE
    46    SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
    47    ORELSE
    48    SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
    49    ORELSE
    50    SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
    51    ORELSE
    52    SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
    53    ORELSE
    54    SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
    55 *}
    56 
    57 end