blanchet@44670
|
1 |
(* Title: HOL/TPTP/CASC_Setup.thy
|
blanchet@42942
|
2 |
Author: Jasmin Blanchette
|
blanchet@42942
|
3 |
Copyright 2011
|
blanchet@42942
|
4 |
|
blanchet@43472
|
5 |
Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and
|
blanchet@43472
|
6 |
TNT divisions. This theory file should be loaded by the Isabelle theory files
|
blanchet@43472
|
7 |
generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files.
|
blanchet@42942
|
8 |
*)
|
blanchet@42942
|
9 |
|
blanchet@43472
|
10 |
theory CASC_Setup
|
blanchet@44669
|
11 |
imports Complex_Main
|
blanchet@44670
|
12 |
uses "../ex/sledgehammer_tactics.ML"
|
blanchet@42918
|
13 |
begin
|
blanchet@42918
|
14 |
|
blanchet@44670
|
15 |
consts
|
blanchet@44670
|
16 |
is_int :: "'a \<Rightarrow> bool"
|
blanchet@44670
|
17 |
is_rat :: "'a \<Rightarrow> bool"
|
blanchet@44670
|
18 |
|
blanchet@44670
|
19 |
overloading rat_is_int \<equiv> "is_int :: rat \<Rightarrow> bool"
|
blanchet@44670
|
20 |
begin
|
blanchet@44670
|
21 |
definition "rat_is_int (q\<Colon>rat) \<longleftrightarrow> (\<exists>n\<Colon>int. q = of_int n)"
|
blanchet@44670
|
22 |
end
|
blanchet@44670
|
23 |
|
blanchet@44670
|
24 |
overloading real_is_int \<equiv> "is_int :: real \<Rightarrow> bool"
|
blanchet@44670
|
25 |
begin
|
blanchet@44670
|
26 |
definition "real_is_int (x\<Colon>real) \<longleftrightarrow> x \<in> \<int>"
|
blanchet@44670
|
27 |
end
|
blanchet@44670
|
28 |
|
blanchet@44670
|
29 |
overloading real_is_rat \<equiv> "is_rat :: real \<Rightarrow> bool"
|
blanchet@44670
|
30 |
begin
|
blanchet@44670
|
31 |
definition "real_is_rat (x\<Colon>real) \<longleftrightarrow> x \<in> \<rat>"
|
blanchet@44670
|
32 |
end
|
blanchet@44670
|
33 |
|
blanchet@44670
|
34 |
consts
|
blanchet@44670
|
35 |
to_int :: "'a \<Rightarrow> int"
|
blanchet@44670
|
36 |
to_rat :: "'a \<Rightarrow> rat"
|
blanchet@44670
|
37 |
to_real :: "'a \<Rightarrow> real"
|
blanchet@44670
|
38 |
|
blanchet@44670
|
39 |
overloading rat_to_int \<equiv> "to_int :: rat \<Rightarrow> int"
|
blanchet@44670
|
40 |
begin
|
blanchet@44670
|
41 |
definition "rat_to_int (q\<Colon>rat) = floor q"
|
blanchet@44670
|
42 |
end
|
blanchet@44670
|
43 |
|
blanchet@44670
|
44 |
overloading real_to_int \<equiv> "to_int :: real \<Rightarrow> int"
|
blanchet@44670
|
45 |
begin
|
blanchet@44670
|
46 |
definition "real_to_int (x\<Colon>real) = floor x"
|
blanchet@44670
|
47 |
end
|
blanchet@44670
|
48 |
|
blanchet@44670
|
49 |
overloading int_to_rat \<equiv> "to_rat :: int \<Rightarrow> rat"
|
blanchet@44670
|
50 |
begin
|
blanchet@44670
|
51 |
definition "int_to_rat (n\<Colon>int) = (of_int n\<Colon>rat)"
|
blanchet@44670
|
52 |
end
|
blanchet@44670
|
53 |
|
blanchet@44670
|
54 |
overloading real_to_rat \<equiv> "to_rat :: real \<Rightarrow> rat"
|
blanchet@44670
|
55 |
begin
|
blanchet@44670
|
56 |
definition "real_to_rat (x\<Colon>real) = (inv real x\<Colon>rat)"
|
blanchet@44670
|
57 |
end
|
blanchet@44670
|
58 |
|
blanchet@44670
|
59 |
overloading int_to_real \<equiv> "to_real :: int \<Rightarrow> real"
|
blanchet@44670
|
60 |
begin
|
blanchet@44670
|
61 |
definition "int_to_real (n\<Colon>int) = real n"
|
blanchet@44670
|
62 |
end
|
blanchet@44670
|
63 |
|
blanchet@44670
|
64 |
overloading rat_to_real \<equiv> "to_real :: rat \<Rightarrow> real"
|
blanchet@44670
|
65 |
begin
|
blanchet@44670
|
66 |
definition "rat_to_real (x\<Colon>rat) = (of_rat x\<Colon>real)"
|
blanchet@44670
|
67 |
end
|
blanchet@44670
|
68 |
|
blanchet@44670
|
69 |
declare
|
blanchet@44670
|
70 |
rat_is_int_def [simp]
|
blanchet@44670
|
71 |
real_is_int_def [simp]
|
blanchet@44670
|
72 |
real_is_rat_def [simp]
|
blanchet@44670
|
73 |
rat_to_int_def [simp]
|
blanchet@44670
|
74 |
real_to_int_def [simp]
|
blanchet@44670
|
75 |
int_to_rat_def [simp]
|
blanchet@44670
|
76 |
real_to_rat_def [simp]
|
blanchet@44670
|
77 |
int_to_real_def [simp]
|
blanchet@44670
|
78 |
rat_to_real_def [simp]
|
blanchet@44670
|
79 |
|
blanchet@44670
|
80 |
lemma to_rat_is_int [intro, simp]: "is_int (to_rat (n\<Colon>int))"
|
blanchet@44670
|
81 |
by (metis int_to_rat_def rat_is_int_def)
|
blanchet@44670
|
82 |
|
blanchet@44670
|
83 |
lemma to_real_is_int [intro, simp]: "is_int (to_real (n\<Colon>int))"
|
blanchet@44670
|
84 |
by (metis Ints_real_of_int int_to_real_def real_is_int_def)
|
blanchet@44670
|
85 |
|
blanchet@44670
|
86 |
lemma to_real_is_rat [intro, simp]: "is_rat (to_real (q\<Colon>rat))"
|
blanchet@44670
|
87 |
by (metis Rats_of_rat rat_to_real_def real_is_rat_def)
|
blanchet@44670
|
88 |
|
blanchet@44670
|
89 |
lemma inj_of_rat [intro, simp]: "inj (of_rat\<Colon>rat\<Rightarrow>real)"
|
blanchet@44670
|
90 |
by (metis injI of_rat_eq_iff rat_to_real_def)
|
blanchet@44670
|
91 |
|
blanchet@42918
|
92 |
declare mem_def [simp add]
|
blanchet@42918
|
93 |
|
blanchet@42918
|
94 |
declare [[smt_oracle]]
|
blanchet@42918
|
95 |
|
blanchet@42970
|
96 |
refute_params [maxtime = 10000, no_assms, expect = genuine]
|
blanchet@42970
|
97 |
nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
|
blanchet@43078
|
98 |
batch_size = 1, expect = genuine]
|
blanchet@42970
|
99 |
|
wenzelm@42949
|
100 |
ML {* Proofterm.proofs := 0 *}
|
blanchet@42918
|
101 |
|
blanchet@42918
|
102 |
ML {*
|
blanchet@42918
|
103 |
fun SOLVE_TIMEOUT seconds name tac st =
|
blanchet@42918
|
104 |
let
|
blanchet@42918
|
105 |
val result =
|
blanchet@42918
|
106 |
TimeLimit.timeLimit (Time.fromSeconds seconds)
|
blanchet@42918
|
107 |
(fn () => SINGLE (SOLVE tac) st) ()
|
blanchet@42918
|
108 |
handle TimeLimit.TimeOut => NONE
|
blanchet@42918
|
109 |
| ERROR _ => NONE
|
blanchet@42918
|
110 |
in
|
blanchet@42918
|
111 |
(case result of
|
blanchet@43080
|
112 |
NONE => (warning ("FAILURE: " ^ name); Seq.empty)
|
blanchet@43080
|
113 |
| SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
|
blanchet@42918
|
114 |
end
|
blanchet@42918
|
115 |
*}
|
blanchet@42918
|
116 |
|
blanchet@42918
|
117 |
ML {*
|
wenzelm@43672
|
118 |
fun isabellep_tac ctxt max_secs =
|
blanchet@43080
|
119 |
SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
|
blanchet@43080
|
120 |
ORELSE
|
blanchet@42918
|
121 |
SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
|
blanchet@45319
|
122 |
(ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
|
blanchet@45319
|
123 |
Sledgehammer_Filter.no_relevance_override))
|
blanchet@42918
|
124 |
ORELSE
|
wenzelm@43672
|
125 |
SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
|
blanchet@42918
|
126 |
ORELSE
|
wenzelm@43672
|
127 |
SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
|
blanchet@42918
|
128 |
ORELSE
|
wenzelm@43672
|
129 |
SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
|
blanchet@45319
|
130 |
THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []
|
blanchet@45319
|
131 |
Sledgehammer_Filter.no_relevance_override))
|
blanchet@42918
|
132 |
ORELSE
|
blanchet@44046
|
133 |
SOLVE_TIMEOUT (max_secs div 10) "metis"
|
blanchet@44053
|
134 |
(ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
|
blanchet@42918
|
135 |
ORELSE
|
wenzelm@43672
|
136 |
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
|
blanchet@42918
|
137 |
ORELSE
|
blanchet@44671
|
138 |
SOLVE_TIMEOUT (max_secs div 20) "best" (ALLGOALS (best_tac ctxt))
|
blanchet@44671
|
139 |
ORELSE
|
blanchet@44671
|
140 |
SOLVE_TIMEOUT (max_secs div 20) "arith" (ALLGOALS (Arith_Data.arith_tac ctxt))
|
blanchet@42918
|
141 |
ORELSE
|
wenzelm@43672
|
142 |
SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
|
blanchet@42918
|
143 |
ORELSE
|
wenzelm@43672
|
144 |
SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
|
blanchet@42918
|
145 |
*}
|
blanchet@42918
|
146 |
|
blanchet@43698
|
147 |
method_setup isabellep = {*
|
blanchet@44671
|
148 |
Scan.lift (Scan.optional Parse.nat 6000) >>
|
blanchet@43698
|
149 |
(fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
|
blanchet@44002
|
150 |
*} "combination of Isabelle provers and oracles for CASC"
|
blanchet@43698
|
151 |
|
blanchet@42918
|
152 |
end
|