| author | wenzelm |
| Tue, 05 Apr 2011 14:25:18 +0200 | |
| changeset 42224 | 578a51fae383 |
| parent 42213 | bac7733a13c9 |
| permissions | -rw-r--r-- |
|
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
1 |
(* Title: HOL/ex/TPTP.thy |
|
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 |
|
|
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
5 |
TPTP "IsabelleP" tactic. |
|
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
6 |
*) |
|
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
7 |
|
|
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
|
8 |
theory TPTP |
|
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
|
9 |
imports Main |
|
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42063
diff
changeset
|
10 |
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
|
11 |
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
|
12 |
|
|
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 |
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
|
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 [[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
|
16 |
|
|
42106
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset
|
17 |
refute_params [maxtime = 10000, no_assms, expect = genuine] |
|
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset
|
18 |
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
|
19 |
batch_size = 1, expect = genuine] |
|
42106
ed1d40888b1b
specify proper defaults for Nitpick and Refute on TPTP + tuning
blanchet
parents:
42078
diff
changeset
|
20 |
|
|
42078
d5bf0ce40bd7
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
wenzelm
parents:
42071
diff
changeset
|
21 |
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
|
22 |
|
|
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
|
23 |
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
|
24 |
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
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
(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
|
29 |
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
|
30 |
| 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
|
31 |
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
|
32 |
(case result of |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
33 |
NONE => (warning ("FAILURE: " ^ name); Seq.empty)
|
|
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
34 |
| 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
|
35 |
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
|
36 |
*} |
|
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 |
|
|
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 |
ML {*
|
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
39 |
fun isabellep_tac ctxt cs ss css max_secs = |
|
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
40 |
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
|
41 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
42 |
SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
|
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
43 |
(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
|
44 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
45 |
SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss)) |
|
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
46 |
ORELSE |
|
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
47 |
SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac cs)) |
|
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
|
48 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
49 |
SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css |
|
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
50 |
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
|
51 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
52 |
SOLVE_TIMEOUT (max_secs div 10) "metis" (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
|
53 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
54 |
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs)) |
|
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
|
55 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
56 |
SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs)) |
|
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
|
57 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
58 |
SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css)) |
|
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
|
59 |
ORELSE |
|
42213
bac7733a13c9
use the proper contexts/simpsets/etc. in the TPTP proof method
blanchet
parents:
42211
diff
changeset
|
60 |
SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css)) |
|
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
|
61 |
*} |
|
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 |
|
|
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
|
63 |
end |