| author | wenzelm |
| Wed, 23 Mar 2011 20:57:37 +0100 | |
| changeset 42078 | d5bf0ce40bd7 |
| parent 42071 | 04577a7e0c51 |
| child 42106 | ed1d40888b1b |
| 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 |
|
|
42078
d5bf0ce40bd7
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
wenzelm
parents:
42071
diff
changeset
|
17 |
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
|
18 |
|
|
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
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
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
|
24 |
(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
|
25 |
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
|
26 |
| 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
|
27 |
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
|
28 |
(case result of |
|
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 |
NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
|
|
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 |
| SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single 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 |
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
|
32 |
*} |
|
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 |
|
|
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 |
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
|
35 |
fun isabellep_tac max_secs = |
|
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 |
SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" |
|
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 |
(ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
|
|
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 |
ORELSE |
|
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 |
SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
|
|
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 |
ORELSE |
|
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 |
SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
|
|
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
|
42 |
ORELSE |
|
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 |
SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
|
|
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 |
THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
|
|
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
|
45 |
ORELSE |
|
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 |
SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
|
|
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
|
47 |
ORELSE |
|
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 |
SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
|
|
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
|
49 |
ORELSE |
|
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 |
SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
|
|
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 |
|
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
|
52 |
SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
|
|
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 |
|
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
|
54 |
SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
|
|
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 |
*} |
|
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 |
|
|
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 |
end |