author | blanchet |
Wed, 13 Jul 2011 22:16:19 +0200 | |
changeset 43804 | eb9be23db2b7 |
parent 43212 | src/HOL/ex/CASC_Setup.thy@050a03afe024 |
child 43805 | 0349175384f8 |
permissions | -rw-r--r-- |
42601 | 1 |
(* Title: HOL/ex/CASC_Setup.thy |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
2 |
Author: Jasmin Blanchette |
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
3 |
Copyright 2011 |
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
4 |
|
42601 | 5 |
Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and |
6 |
TNT divisions. This theory file should be loaded by the Isabelle theory files |
|
7 |
generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files. |
|
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
8 |
*) |
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
9 |
|
42601 | 10 |
theory CASC_Setup |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
11 |
imports Main |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
12 |
uses "sledgehammer_tactics.ML" |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
13 |
begin |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
14 |
|
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
15 |
declare mem_def [simp add] |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
16 |
|
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
17 |
declare [[smt_oracle]] |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
18 |
|
42106
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset
|
19 |
refute_params [maxtime = 10000, no_assms, expect = genuine] |
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset
|
20 |
nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms, |
42211
9e2673711c77
make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
blanchet
parents:
42106
diff
changeset
|
21 |
batch_size = 1, expect = genuine] |
42106
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset
|
22 |
|
42078
d5bf0ce40bd7
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
wenzelm
parents:
42071
diff
changeset
|
23 |
ML {* Proofterm.proofs := 0 *} |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
24 |
|
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
25 |
ML {* |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
26 |
fun SOLVE_TIMEOUT seconds name tac st = |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
27 |
let |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
28 |
val result = |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
29 |
TimeLimit.timeLimit (Time.fromSeconds seconds) |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
30 |
(fn () => SINGLE (SOLVE tac) st) () |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
31 |
handle TimeLimit.TimeOut => NONE |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
32 |
| ERROR _ => NONE |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
33 |
in |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
34 |
(case result of |
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
35 |
NONE => (warning ("FAILURE: " ^ name); Seq.empty) |
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
36 |
| SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st')) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
37 |
end |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
38 |
*} |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
39 |
|
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
40 |
ML {* |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
41 |
fun isabellep_tac ctxt max_secs = |
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
42 |
SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
43 |
ORELSE |
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
44 |
SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
45 |
(ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
46 |
ORELSE |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
47 |
SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) |
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
48 |
ORELSE |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
49 |
SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
50 |
ORELSE |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
51 |
SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt |
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
52 |
THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
53 |
ORELSE |
43205 | 54 |
SOLVE_TIMEOUT (max_secs div 10) "metis" |
43212 | 55 |
(ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
56 |
ORELSE |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
57 |
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
58 |
ORELSE |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
59 |
SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt)) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
60 |
ORELSE |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
61 |
SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt)) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
62 |
ORELSE |
42800
df2dc9406287
just one universal Proof.context -- discontinued claset/clasimpset;
wenzelm
parents:
42601
diff
changeset
|
63 |
SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt)) |
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
64 |
*} |
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
65 |
|
42827 | 66 |
method_setup isabellep = {* |
43161 | 67 |
Scan.lift (Scan.optional Parse.nat 1) >> |
42827 | 68 |
(fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m)) |
43161 | 69 |
*} "combination of Isabelle provers and oracles for CASC" |
42827 | 70 |
|
42063
a2a69b32d899
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
blanchet
parents:
diff
changeset
|
71 |
end |