author  paulson 
Wed, 15 Nov 2006 11:33:59 +0100  
changeset 21373  18f519614978 
parent 21311  3556301c18cd 
child 21397  2134b81a0b37 
permissions  rwrr 
19194  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA 
15608  2 
ID: $Id$ 
3 
Copyright 2004 University of Cambridge 

15347  4 

5 
ATPs with TPTP format input. 

6 
*) 

15452  7 

20954  8 
(*Currently unused, during debugging*) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

9 
signature RES_ATP = 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

10 
sig 
17306  11 
val prover: string ref 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

12 
val custom_spass: string list ref 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

13 
val destdir: string ref 
17849  14 
val helper_path: string > string > string 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

15 
val problem_name: string ref 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

16 
val time_limit: int ref 
21224  17 
val set_prover: string > unit 
19194  18 

19 
datatype mode = Auto  Fol  Hol 

19450
651d949776f8
exported linkup_logic_mode and changed the default setting
paulson
parents:
19445
diff
changeset

20 
val linkup_logic_mode : mode ref 
19722  21 
val write_subgoal_file: bool > mode > Proof.context > thm list > thm list > int > string 
19194  22 
val vampire_time: int ref 
23 
val eprover_time: int ref 

19722  24 
val spass_time: int ref 
19194  25 
val run_vampire: int > unit 
26 
val run_eprover: int > unit 

19722  27 
val run_spass: int > unit 
19194  28 
val vampireLimit: unit > int 
29 
val eproverLimit: unit > int 

19722  30 
val spassLimit: unit > int 
20289  31 
val atp_method: (Proof.context > thm list > int > tactic) > 
32 
Method.src > Proof.context > Proof.method 

19194  33 
val cond_rm_tmp: string > unit 
34 
val fol_keep_types: bool ref 

35 
val hol_full_types: unit > unit 

36 
val hol_partial_types: unit > unit 

37 
val hol_const_types_only: unit > unit 

38 
val hol_no_types: unit > unit 

39 
val hol_typ_level: unit > ResHolClause.type_level 

20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

40 
val include_all: bool ref 
19194  41 
val run_relevance_filter: bool ref 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

42 
val run_blacklist_filter: bool ref 
20372
e42674e0486e
blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents:
20289
diff
changeset

43 
val blacklist: string list ref 
19894  44 
val add_all : unit > unit 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

45 
val add_claset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

46 
val add_simpset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

47 
val add_clasimp : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

48 
val add_atpset : unit > unit 
19894  49 
val rm_all : unit > unit 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

50 
val rm_claset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

51 
val rm_simpset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

52 
val rm_atpset : unit > unit 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

53 
val rm_clasimp : unit > unit 
21311  54 
val is_fol_thms : thm list > bool 
15347  55 
end; 
56 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

57 
structure ResAtp = 
15347  58 
struct 
59 

21070  60 
fun timestamp s = Output.debug ("At " ^ Time.toString (Time.now()) ^ ": " ^ s); 
61 

19194  62 
(********************************************************************) 
63 
(* some settings for both background automatic ATP calling procedure*) 

64 
(* and also explicit ATP invocation methods *) 

65 
(********************************************************************) 

66 

67 
(*** background linkup ***) 

68 
val call_atp = ref false; 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
17091
diff
changeset

69 
val hook_count = ref 0; 
21224  70 
val time_limit = ref 60; 
71 
val prover = ref ""; 

72 

73 
fun set_prover atp = 

74 
case String.map Char.toLower atp of 

75 
"e" => 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

76 
(ReduceAxiomsN.max_new := 100; 
21224  77 
ReduceAxiomsN.theory_const := false; 
78 
prover := "E") 

79 
 "spass" => 

80 
(ReduceAxiomsN.max_new := 40; 

81 
ReduceAxiomsN.theory_const := true; 

82 
prover := "spass") 

83 
 "vampire" => 

84 
(ReduceAxiomsN.max_new := 60; 

85 
ReduceAxiomsN.theory_const := false; 

86 
prover := "vampire") 

87 
 _ => error ("No such prover: " ^ atp); 

88 

89 
val _ = set_prover "E"; (* use E as the default prover *) 

90 

17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset

91 
val custom_spass = (*specialized options for SPASS*) 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

92 
ref ["Auto=0","FullRed=0","IORe","IOFc","RTaut","RFSub","RBSub"]; 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

93 
val destdir = ref ""; (*Empty means write files to /tmp*) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

94 
val problem_name = ref "prob"; 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

95 

17819  96 
(*Return the path to a "helper" like SPASS or tptp2X, first checking that 
97 
it exists. FIXME: modify to use Path primitives and move to some central place.*) 

98 
fun helper_path evar base = 

99 
case getenv evar of 

100 
"" => error ("Isabelle environment variable " ^ evar ^ " not defined") 

101 
 home => 

102 
let val path = home ^ "/" ^ base 

103 
in if File.exists (File.unpack_platform_path path) then path 

104 
else error ("Could not find the file " ^ path) 

105 
end; 

106 

17717  107 
fun probfile_nosuffix _ = 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

108 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name))) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

109 
else if File.exists (File.unpack_platform_path (!destdir)) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

110 
then !destdir ^ "/" ^ !problem_name 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

111 
else error ("No such directory: " ^ !destdir); 
15644  112 

17717  113 
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; 
114 

19194  115 

116 
(*** ATP methods ***) 

117 
val vampire_time = ref 60; 

118 
val eprover_time = ref 60; 

19722  119 
val spass_time = ref 60; 
120 

19194  121 
fun run_vampire time = 
122 
if (time >0) then vampire_time:= time 

123 
else vampire_time:=60; 

124 

125 
fun run_eprover time = 

126 
if (time > 0) then eprover_time:= time 

127 
else eprover_time:=60; 

128 

19722  129 
fun run_spass time = 
130 
if (time > 0) then spass_time:=time 

131 
else spass_time:=60; 

132 

133 

19194  134 
fun vampireLimit () = !vampire_time; 
135 
fun eproverLimit () = !eprover_time; 

19722  136 
fun spassLimit () = !spass_time; 
19194  137 

138 
val fol_keep_types = ResClause.keep_types; 

139 
val hol_full_types = ResHolClause.full_types; 

140 
val hol_partial_types = ResHolClause.partial_types; 

141 
val hol_const_types_only = ResHolClause.const_types_only; 

142 
val hol_no_types = ResHolClause.no_types; 

143 
fun hol_typ_level () = ResHolClause.find_typ_level (); 

144 
fun is_typed_hol () = 

145 
let val tp_level = hol_typ_level() 

146 
in 

147 
not (tp_level = ResHolClause.T_NONE) 

148 
end; 

149 

150 
fun atp_input_file () = 

151 
let val file = !problem_name 

152 
in 

153 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file)) 

154 
else if File.exists (File.unpack_platform_path (!destdir)) 

155 
then !destdir ^ "/" ^ file 

156 
else error ("No such directory: " ^ !destdir) 

157 
end; 

158 

20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

159 
val include_all = ref true; 
19194  160 
val include_simpset = ref false; 
161 
val include_claset = ref false; 

162 
val include_atpset = ref true; 

20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

163 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

164 
(*Tests show that follow_defs gives VERY poor results with "include_all"*) 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

165 
fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false); 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

166 
fun rm_all() = include_all:=false; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

167 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

168 
fun add_simpset() = include_simpset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

169 
fun rm_simpset() = include_simpset:=false; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

170 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

171 
fun add_claset() = include_claset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

172 
fun rm_claset() = include_claset:=false; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

173 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

174 
fun add_clasimp() = (include_simpset:=true;include_claset:=true); 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

175 
fun rm_clasimp() = (include_simpset:=false;include_claset:=false); 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

176 

fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

177 
fun add_atpset() = include_atpset:=true; 
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

178 
fun rm_atpset() = include_atpset:=false; 
19194  179 

180 

181 
(**** relevance filter ****) 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

182 
val run_relevance_filter = ReduceAxiomsN.run_relevance_filter; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

183 
val run_blacklist_filter = ref true; 
19194  184 

185 
(******************************************************************) 

186 
(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *) 

187 
(******************************************************************) 

188 

189 
datatype logic = FOL  HOL  HOLC  HOLCS; 

190 

191 
fun string_of_logic FOL = "FOL" 

192 
 string_of_logic HOL = "HOL" 

193 
 string_of_logic HOLC = "HOLC" 

194 
 string_of_logic HOLCS = "HOLCS"; 

195 

196 
fun is_fol_logic FOL = true 

197 
 is_fol_logic _ = false 

198 

199 
(*HOLCS will not occur here*) 

200 
fun upgrade_lg HOLC _ = HOLC 

201 
 upgrade_lg HOL HOLC = HOLC 

202 
 upgrade_lg HOL _ = HOL 

203 
 upgrade_lg FOL lg = lg; 

204 

205 
(* check types *) 

19451  206 
fun has_bool_hfn (Type("bool",_)) = true 
207 
 has_bool_hfn (Type("fun",_)) = true 

208 
 has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts 

209 
 has_bool_hfn _ = false; 

19194  210 

19451  211 
fun is_hol_fn tp = 
19194  212 
let val (targs,tr) = strip_type tp 
213 
in 

19451  214 
exists (has_bool_hfn) (tr::targs) 
19194  215 
end; 
216 

19451  217 
fun is_hol_pred tp = 
218 
let val (targs,tr) = strip_type tp 

219 
in 

220 
exists (has_bool_hfn) targs 

221 
end; 

19194  222 

223 
exception FN_LG of term; 

224 

225 
fun fn_lg (t as Const(f,tp)) (lg,seen) = 

20854  226 
if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
19194  227 
 fn_lg (t as Free(f,tp)) (lg,seen) = 
20854  228 
if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
19194  229 
 fn_lg (t as Var(f,tp)) (lg,seen) = 
20854  230 
if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen) 
231 
 fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen) 

19194  232 
 fn_lg f _ = raise FN_LG(f); 
233 

234 

235 
fun term_lg [] (lg,seen) = (lg,seen) 

236 
 term_lg (tm::tms) (FOL,seen) = 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

237 
let val (f,args) = strip_comb tm 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

238 
val (lg',seen') = if f mem seen then (FOL,seen) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

239 
else fn_lg f (FOL,seen) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

240 
in 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

241 
if is_fol_logic lg' then () 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

242 
else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f); 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

243 
term_lg (args@tms) (lg',seen') 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

244 
end 
19194  245 
 term_lg _ (lg,seen) = (lg,seen) 
246 

247 
exception PRED_LG of term; 

248 

249 
fun pred_lg (t as Const(P,tp)) (lg,seen)= 

20854  250 
if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
19194  251 
 pred_lg (t as Free(P,tp)) (lg,seen) = 
20854  252 
if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
253 
 pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen) 

19194  254 
 pred_lg P _ = raise PRED_LG(P); 
255 

256 

257 
fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen) 

258 
 lit_lg P (lg,seen) = 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

259 
let val (pred,args) = strip_comb P 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

260 
val (lg',seen') = if pred mem seen then (lg,seen) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

261 
else pred_lg pred (lg,seen) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

262 
in 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

263 
if is_fol_logic lg' then () 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

264 
else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred); 
19194  265 
term_lg args (lg',seen') 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

266 
end; 
19194  267 

268 
fun lits_lg [] (lg,seen) = (lg,seen) 

269 
 lits_lg (lit::lits) (FOL,seen) = 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

270 
let val (lg,seen') = lit_lg lit (FOL,seen) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

271 
in 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

272 
if is_fol_logic lg then () 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

273 
else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit); 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

274 
lits_lg lits (lg,seen') 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

275 
end 
19194  276 
 lits_lg lits (lg,seen) = (lg,seen); 
277 

19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

278 
fun dest_disj_aux (Const ("op ", _) $ t $ t') disjs = 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

279 
dest_disj_aux t (dest_disj_aux t' disjs) 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

280 
 dest_disj_aux t disjs = t::disjs; 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

281 

d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

282 
fun dest_disj t = dest_disj_aux t []; 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

283 

19194  284 
fun logic_of_clause tm (lg,seen) = 
285 
let val tm' = HOLogic.dest_Trueprop tm 

19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

286 
val disjs = dest_disj tm' 
19194  287 
in 
288 
lits_lg disjs (lg,seen) 

289 
end; 

290 

291 
fun logic_of_clauses [] (lg,seen) = (lg,seen) 

292 
 logic_of_clauses (cls::clss) (FOL,seen) = 

19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

293 
let val (lg,seen') = logic_of_clause cls (FOL,seen) 
19641
f1de44e61ec1
replaced lowlevel Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
wenzelm
parents:
19617
diff
changeset

294 
val _ = 
f1de44e61ec1
replaced lowlevel Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
wenzelm
parents:
19617
diff
changeset

295 
if is_fol_logic lg then () 
19746  296 
else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls) 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

297 
in 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

298 
logic_of_clauses clss (lg,seen') 
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

299 
end 
19194  300 
 logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); 
301 

302 
fun problem_logic_goals_aux [] (lg,seen) = lg 

303 
 problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 

304 
problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen)); 

305 

306 
fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]); 

307 

21311  308 
fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL); 
309 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

310 
(***************************************************************) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

311 
(* Retrieving and filtering lemmas *) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

312 
(***************************************************************) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

313 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

314 
(*** white list and black list of lemmas ***) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

315 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

316 
(*The rule subsetI is frequently omitted by the relevance filter.*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

317 
val whitelist = ref [subsetI]; 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

318 

20444  319 
(*Names of theorems and theorem lists to be banned. The final numeric suffix of 
320 
theorem lists is first removed. 

321 

322 
These theorems typically produce clauses that are prolific (match too many equality or 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

323 
membership literals) and relate to seldomused facts. Some duplicate other rules. 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

324 
FIXME: this blacklist needs to be maintained using theory data and added to using 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

325 
an attribute.*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

326 
val blacklist = ref 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

327 
["Datatype.prod.size", 
21132  328 
"Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*) 
21224  329 
"Datatype.unit.induct", 
20372
e42674e0486e
blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents:
20289
diff
changeset

330 
"Datatype.unit.inducts", 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

331 
"Datatype.unit.split_asm", 
20372
e42674e0486e
blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents:
20289
diff
changeset

332 
"Datatype.unit.split", 
20444  333 
"Datatype.unit.splits", 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

334 
"Divides.dvd_0_left_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

335 
"Finite_Set.card_0_eq", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

336 
"Finite_Set.card_infinite", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

337 
"Finite_Set.Max_ge", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

338 
"Finite_Set.Max_in", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

339 
"Finite_Set.Max_le_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

340 
"Finite_Set.Max_less_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

341 
"Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

342 
"Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

343 
"Finite_Set.Min_ge_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

344 
"Finite_Set.Min_gr_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

345 
"Finite_Set.Min_in", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

346 
"Finite_Set.Min_le", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

347 
"Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

348 
"Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

349 
"Finite_Set.min.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

350 
"Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

351 
"Fun.vimage_image_eq", (*involves an existential quantifier*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

352 
"HOL.split_if_asm", (*splitting theorem*) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

353 
"HOL.split_if", (*splitting theorem*) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

354 
"IntDef.abs_split", 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

355 
"IntDef.Integ.Abs_Integ_inject", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

356 
"IntDef.Integ.Abs_Integ_inverse", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

357 
"IntDiv.zdvd_0_left", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

358 
"List.append_eq_append_conv", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

359 
"List.hd_Cons_tl", (*Says everything is [] or Cons. Probably prolific.*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

360 
"List.in_listsD", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

361 
"List.in_listsI", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

362 
"List.lists.Cons", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

363 
"List.listsE", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

364 
"Nat.less_one", (*not directional? obscure*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

365 
"Nat.not_gr0", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

366 
"Nat.one_eq_mult_iff", (*duplicate by symmetry*) 
21243  367 
"Nat.of_nat_0_eq_iff", 
368 
"Nat.of_nat_eq_0_iff", 

369 
"Nat.of_nat_le_0_iff", 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

370 
"NatSimprocs.divide_le_0_iff_number_of", (*too many clauses*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

371 
"NatSimprocs.divide_less_0_iff_number_of", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

372 
"NatSimprocs.equation_minus_iff_1", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

373 
"NatSimprocs.equation_minus_iff_number_of", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

374 
"NatSimprocs.le_minus_iff_1", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

375 
"NatSimprocs.le_minus_iff_number_of", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

376 
"NatSimprocs.less_minus_iff_1", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

377 
"NatSimprocs.less_minus_iff_number_of", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

378 
"NatSimprocs.minus_equation_iff_number_of", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

379 
"NatSimprocs.minus_le_iff_1", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

380 
"NatSimprocs.minus_le_iff_number_of", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

381 
"NatSimprocs.minus_less_iff_1", (*not directional*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

382 
"NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

383 
"NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

384 
"NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

385 
"NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

386 
"NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

387 
"NatSimprocs.zero_less_divide_iff_number_of", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

388 
"OrderedGroup.abs_0_eq", (*duplicate by symmetry*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

389 
"OrderedGroup.diff_eq_0_iff_eq", (*prolific?*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

390 
"OrderedGroup.join_0_eq_0", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

391 
"OrderedGroup.meet_0_eq_0", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

392 
"OrderedGroup.pprt_eq_0", (*obscure*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

393 
"OrderedGroup.pprt_eq_id", (*obscure*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

394 
"OrderedGroup.pprt_mono", (*obscure*) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

395 
"Orderings.split_max", (*splitting theorem*) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

396 
"Orderings.split_min", (*splitting theorem*) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

397 
"Parity.even_nat_power", (*obscure, somewhat prolilfic*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

398 
"Parity.power_eq_0_iff_number_of", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

399 
"Parity.power_le_zero_eq_number_of", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

400 
"Parity.power_less_zero_eq_number_of", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

401 
"Parity.zero_le_power_eq_number_of", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

402 
"Parity.zero_less_power_eq_number_of", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

403 
"Power.zero_less_power_abs_iff", 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

404 
"Product_Type.split_eta_SetCompr", (*involves an existential quantifier*) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

405 
"Product_Type.split_paired_Ball_Sigma", (*splitting theorem*) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

406 
"Product_Type.split_paired_Bex_Sigma", (*splitting theorem*) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

407 
"Product_Type.split_split_asm", (*splitting theorem*) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

408 
"Product_Type.split_split", (*splitting theorem*) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

409 
"Product_Type.unit_abs_eta_conv", 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

410 
"Product_Type.unit_induct", 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

411 
"Relation.diagI", 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

412 
"Relation.Domain_def", (*involves an existential quantifier*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

413 
"Relation.Image_def", (*involves an existential quantifier*) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

414 
"Relation.ImageI", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

415 
"Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

416 
"Ring_and_Field.divide_cancel_right", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

417 
"Ring_and_Field.divide_divide_eq_left", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

418 
"Ring_and_Field.divide_divide_eq_right", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

419 
"Ring_and_Field.divide_eq_0_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

420 
"Ring_and_Field.divide_eq_1_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

421 
"Ring_and_Field.divide_eq_eq_1", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

422 
"Ring_and_Field.divide_le_0_1_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

423 
"Ring_and_Field.divide_le_eq_1_neg", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

424 
"Ring_and_Field.divide_le_eq_1_pos", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

425 
"Ring_and_Field.divide_less_0_1_iff", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

426 
"Ring_and_Field.divide_less_eq_1_neg", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

427 
"Ring_and_Field.divide_less_eq_1_pos", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

428 
"Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

429 
"Ring_and_Field.field_mult_cancel_left", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

430 
"Ring_and_Field.field_mult_cancel_right", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

431 
"Ring_and_Field.inverse_le_iff_le_neg", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

432 
"Ring_and_Field.inverse_le_iff_le", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

433 
"Ring_and_Field.inverse_less_iff_less_neg", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

434 
"Ring_and_Field.inverse_less_iff_less", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

435 
"Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

436 
"Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

437 
"Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

438 
"Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

439 
"Ring_and_Field.one_eq_divide_iff", (*duplicate by symmetry*) 
20444  440 
"Set.ball_simps", "Set.bex_simps", (*quantifier rewriting: useless*) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

441 
"Set.Collect_bex_eq", (*involves an existential quantifier*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

442 
"Set.Collect_ex_eq", (*involves an existential quantifier*) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

443 
"Set.Diff_eq_empty_iff", (*redundant with paramodulation*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

444 
"Set.Diff_insert0", 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

445 
"Set.disjoint_insert", 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

446 
"Set.empty_Union_conv", (*redundant with paramodulation*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

447 
"Set.full_SetCompr_eq", (*involves an existential quantifier*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

448 
"Set.image_Collect", (*involves an existential quantifier*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

449 
"Set.image_def", (*involves an existential quantifier*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

450 
"Set.insert_disjoint", 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

451 
"Set.Int_UNIV", (*redundant with paramodulation*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

452 
"Set.Inter_iff", (*We already have InterI, InterE*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

453 
"Set.Inter_UNIV_conv", 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

454 
"Set.psubsetE", (*too prolific and obscure*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

455 
"Set.psubsetI", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

456 
"Set.singleton_insert_inj_eq'", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

457 
"Set.singleton_insert_inj_eq", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

458 
"Set.singletonD", (*these two duplicate some "insert" lemmas*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

459 
"Set.singletonI", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

460 
"Set.Un_empty", (*redundant with paramodulation*) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

461 
"Set.UNION_def", (*involves an existential quantifier*) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

462 
"Set.Union_empty_conv", (*redundant with paramodulation*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

463 
"Set.Union_iff", (*We already have UnionI, UnionE*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

464 
"SetInterval.atLeastAtMost_iff", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

465 
"SetInterval.atLeastLessThan_iff", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

466 
"SetInterval.greaterThanAtMost_iff", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

467 
"SetInterval.greaterThanLessThan_iff", (*obscure and prolific*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

468 
"SetInterval.ivl_subset"]; (*excessive case analysis*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

469 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

470 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

471 
(*These might be prolific but are probably OK, and min and max are basic. 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

472 
"Orderings.max_less_iff_conj", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

473 
"Orderings.min_less_iff_conj", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

474 
"Orderings.min_max.below_inf.below_inf_conv", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

475 
"Orderings.min_max.below_sup.above_sup_conv", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

476 
Very prolific and somewhat obscure: 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

477 
"Set.InterD", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

478 
"Set.UnionI", 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

479 
*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

480 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

481 
(*** retrieve lemmas from clasimpset and atpset, may filter them ***) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

482 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

483 
(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

484 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

485 
exception HASH_CLAUSE and HASH_STRING; 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

486 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

487 
(*Catches (for deletion) theorems automatically generated from other theorems*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

488 
fun insert_suffixed_names ht x = 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

489 
(Polyhash.insert ht (x^"_iff1", ()); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

490 
Polyhash.insert ht (x^"_iff2", ()); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

491 
Polyhash.insert ht (x^"_dest", ())); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

492 

20444  493 
(*Are all characters in this string digits?*) 
494 
fun all_numeric s = null (String.tokens Char.isDigit s); 

495 

496 
(*Delete a suffix of the form _\d+*) 

497 
fun delete_numeric_suffix s = 

498 
case rev (String.fields (fn c => c = #"_") s) of 

499 
last::rest => 

500 
if all_numeric last 

20446
7e616709bca2
String.concatWith (not available in PolyML) replaced by space_implode
webertj
parents:
20444
diff
changeset

501 
then [s, space_implode "_" (rev rest)] 
20444  502 
else [s] 
503 
 [] => [s]; 

504 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

505 
fun banned_thmlist s = 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

506 
(Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"]; 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

507 

20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

508 
(*Reject theorems with names like "List.filter.filter_list_def" or 
20823
5480ec4b542d
restored the "length of name > 2" check for package definitions
paulson
parents:
20781
diff
changeset

509 
"Accessible_Part.acc.defs", as these are definitions arising from packages. 
5480ec4b542d
restored the "length of name > 2" check for package definitions
paulson
parents:
20781
diff
changeset

510 
FIXME: this will also block definitions within locales*) 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

511 
fun is_package_def a = 
20823
5480ec4b542d
restored the "length of name > 2" check for package definitions
paulson
parents:
20781
diff
changeset

512 
length (NameSpace.unpack a) > 2 andalso 
5480ec4b542d
restored the "length of name > 2" check for package definitions
paulson
parents:
20781
diff
changeset

513 
String.isSuffix "_def" a orelse String.isSuffix "_defs" a; 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

514 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

515 
fun make_banned_test xs = 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

516 
let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

517 
(6000, HASH_STRING) 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

518 
fun banned_aux s = 
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

519 
isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

520 
fun banned s = exists banned_aux (delete_numeric_suffix s) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

521 
in app (fn x => Polyhash.insert ht (x,())) (!blacklist); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

522 
app (insert_suffixed_names ht) (!blacklist @ xs); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

523 
banned 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

524 
end; 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

525 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

526 
(** a hash function from Term.term to int, and also a hash table **) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

527 
val xor_words = List.foldl Word.xorb 0w0; 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

528 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

529 
fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w) 
20661
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

530 
 hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

531 
 hashw_term ((Var(_,_)), w) = w 
20661
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

532 
 hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

533 
 hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

534 
 hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w))); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

535 

21070  536 
fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) 
537 
 hash_literal P = hashw_term(P,0w0); 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

538 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

539 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

540 
fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

541 
 get_literals (Const("op ",_)$P$Q) lits = get_literals Q (get_literals P lits) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

542 
 get_literals lit lits = (lit::lits); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

543 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

544 
fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t []))); 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

545 

9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

546 
fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

547 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

548 
(*Create a hash table for clauses, of the given size*) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

549 
fun mk_clause_table n = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

550 
Polyhash.mkTable (hash_term o prop_of, equal_thm) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

551 
(n, HASH_CLAUSE); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

552 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

553 
(*Use a hash table to eliminate duplicates from xs. Argument is a list of 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

554 
(thm * (string * int)) tuples. The theorems are hashed into the table. *) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

555 
fun make_unique xs = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

556 
let val ht = mk_clause_table 7000 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

557 
in 
21070  558 
Output.debug("make_unique gets " ^ Int.toString (length xs) ^ " clauses"); 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

559 
app (ignore o Polyhash.peekInsert ht) xs; 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

560 
Polyhash.listItems ht 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

561 
end; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

562 

20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

563 
(*Remove existing axiom clauses from the conjecture clauses, as this can dramatically 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

564 
boost an ATP's performance (for some reason)*) 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

565 
fun subtract_cls c_clauses ax_clauses = 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

566 
let val ht = mk_clause_table 2200 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

567 
fun known x = isSome (Polyhash.peek ht x) 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

568 
in 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

569 
app (ignore o Polyhash.peekInsert ht) ax_clauses; 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

570 
filter (not o known) c_clauses 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

571 
end; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

572 

20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

573 
(*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

574 
Duplicates are removed later.*) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

575 
fun get_relevant_clauses thy cls_thms white_cls goals = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

576 
white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

577 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

578 
fun display_thms [] = () 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

579 
 display_thms ((name,thm)::nthms) = 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

580 
let val nthm = name ^ ": " ^ (string_of_thm thm) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

581 
in Output.debug nthm; display_thms nthms end; 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

582 

21224  583 
fun all_valid_thms ctxt = 
584 
PureThy.thms_containing (ProofContext.theory_of ctxt) ([], []) @ 

585 
filter (ProofContext.valid_thms ctxt) 

586 
(FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])); 

587 

588 
fun multi_name a (th, (n,pairs)) = 

589 
(n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) 

590 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

591 
fun add_multi_names ((a, []), pairs) = pairs 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

592 
 add_multi_names ((a, [th]), pairs) = (a,th)::pairs 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

593 
 add_multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths); 
21224  594 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

595 
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

596 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

597 
(*The single theorems go BEFORE the multiple ones*) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

598 
fun name_thm_pairs ctxt = 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

599 
let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

600 
in foldl add_multi_names (foldl add_multi_names [] mults) singles end; 
21224  601 

602 
fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false) 

603 
 check_named (_,th) = true; 

19894  604 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

605 
(* get lemmas from claset, simpset, atpset and extra supplied rules *) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

606 
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894  607 
let val included_thms = 
608 
if !include_all 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

609 
then (tap (fn ths => Output.debug 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

610 
("Including all " ^ Int.toString (length ths) ^ " theorems")) 
21224  611 
(name_thm_pairs ctxt)) 
19894  612 
else 
613 
let val claset_thms = 

614 
if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt 

615 
else [] 

616 
val simpset_thms = 

617 
if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt 

618 
else [] 

619 
val atpset_thms = 

620 
if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt 

621 
else [] 

622 
val _ = if !Output.show_debug_msgs 

623 
then (Output.debug "ATP theorems: "; display_thms atpset_thms) 

624 
else () 

625 
in claset_thms @ simpset_thms @ atpset_thms end 

21224  626 
val user_rules = filter check_named 
627 
(map (ResAxioms.pairname) 

628 
(if null user_thms then !whitelist else user_thms)) 

19894  629 
in 
21224  630 
(filter check_named included_thms, user_rules) 
19894  631 
end; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

632 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

633 
(*Remove lemmas that are banned from the backlist. Also remove duplicates. *) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

634 
fun blacklist_filter thms = 
19894  635 
if !run_blacklist_filter then 
21070  636 
let val _ = Output.debug("blacklist filter gets " ^ Int.toString (length thms) ^ " theorems") 
637 
val banned = make_banned_test (map #1 thms) 

19894  638 
fun ok (a,_) = not (banned a) 
21070  639 
val okthms = filter ok thms 
640 
val _ = Output.debug("...and returns " ^ Int.toString (length okthms)) 

641 
in okthms end 

19894  642 
else thms; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

643 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

644 
(***************************************************************) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

645 
(* Type Classes Present in the Axiom or Conjecture Clauses *) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

646 
(***************************************************************) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

647 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

648 
fun setinsert (x,s) = Symtab.update (x,()) s; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

649 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

650 
fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts); 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

651 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

652 
(*Remove this trivial type class*) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

653 
fun delete_type cset = Symtab.delete_safe "HOL.type" cset; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

654 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

655 
fun tvar_classes_of_terms ts = 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

656 
let val sorts_list = map (map #2 o term_tvars) ts 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

657 
in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

658 

33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

659 
fun tfree_classes_of_terms ts = 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

660 
let val sorts_list = map (map #2 o term_tfrees) ts 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

661 
in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

662 

21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

663 
(*fold type constructors*) 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

664 
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

665 
 fold_type_consts f T x = x; 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

666 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

667 
val add_type_consts_in_type = fold_type_consts setinsert; 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

668 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

669 
val add_type_consts_in_term = fold_types add_type_consts_in_type; 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

670 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

671 
fun type_consts_of_terms ts = 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

672 
Symtab.keys (fold add_type_consts_in_term ts Symtab.empty); 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

673 

18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

674 

19194  675 
(***************************************************************) 
676 
(* ATP invocation methods setup *) 

677 
(***************************************************************) 

678 

679 
fun cnf_hyps_thms ctxt = 

20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20131
diff
changeset

680 
let val ths = Assumption.prems_of ctxt 
19617  681 
in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end; 
19194  682 

20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

683 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  684 
datatype mode = Auto  Fol  Hol; 
685 

19450
651d949776f8
exported linkup_logic_mode and changed the default setting
paulson
parents:
19445
diff
changeset

686 
val linkup_logic_mode = ref Auto; 
19205
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

687 

20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

688 
(*Ensures that no higherorder theorems "leak out"*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

689 
fun restrict_to_logic logic cls = 
20532  690 
if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

691 
else cls; 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

692 

20131
c89ee2f4efd5
Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents:
20022
diff
changeset

693 
fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas = 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

694 
if is_fol_logic logic 
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

695 
then ResClause.tptp_write_file goals filename (axioms, classrels, arities) 
20131
c89ee2f4efd5
Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents:
20022
diff
changeset

696 
else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas; 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

697 

20131
c89ee2f4efd5
Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents:
20022
diff
changeset

698 
fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas = 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

699 
if is_fol_logic logic 
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

700 
then ResClause.dfg_write_file goals filename (axioms, classrels, arities) 
20131
c89ee2f4efd5
Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents:
20022
diff
changeset

701 
else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas; 
19194  702 

20022  703 
(*Called by the oraclebased methods declared in res_atp_methods.ML*) 
19722  704 
fun write_subgoal_file dfg mode ctxt conjectures user_thms n = 
19442  705 
let val conj_cls = make_clauses conjectures 
20444  706 
> ResAxioms.assume_abstract_list > Meson.finish_cnf 
19442  707 
val hyp_cls = cnf_hyps_thms ctxt 
19194  708 
val goal_cls = conj_cls@hyp_cls 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

709 
val logic = case mode of 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

710 
Auto => problem_logic_goals [map prop_of goal_cls] 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

711 
 Fol => FOL 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

712 
 Hol => HOL 
19894  713 
val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

714 
val cla_simp_atp_clauses = included_thms > blacklist_filter 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

715 
> ResAxioms.cnf_rules_pairs > make_unique 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

716 
> restrict_to_logic logic 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

717 
val user_cls = ResAxioms.cnf_rules_pairs user_rules 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

718 
val thy = ProofContext.theory_of ctxt 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

719 
val axclauses = get_relevant_clauses thy cla_simp_atp_clauses 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

720 
user_cls (map prop_of goal_cls) > make_unique 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

721 
val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol () 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

722 
val subs = tfree_classes_of_terms (map prop_of goal_cls) 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

723 
and axtms = map (prop_of o #1) axclauses 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

724 
val supers = tvar_classes_of_terms axtms 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

725 
and tycons = type_consts_of_terms axtms 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

726 
(*TFrees in conjecture clauses; TVars in axiom clauses*) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

727 
val classrel_clauses = 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

728 
if keep_types then ResClause.make_classrel_clauses thy subs supers 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

729 
else [] 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

730 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else [] 
19722  731 
val writer = if dfg then dfg_writer else tptp_writer 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

732 
and file = atp_input_file() 
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

733 
and user_lemmas_names = map #1 user_rules 
19194  734 
in 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

735 
writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; 
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

736 
Output.debug ("Writing to " ^ file); 
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

737 
file 
19194  738 
end; 
739 

740 

741 
(**** remove tmp files ****) 

742 
fun cond_rm_tmp file = 

20870  743 
if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
744 
else OS.FileSys.remove file; 

19194  745 

746 

747 
(****** setup ATPs as Isabelle methods ******) 

748 
fun atp_meth' tac ths ctxt = 

749 
Method.SIMPLE_METHOD' HEADGOAL 

750 
(tac ctxt ths); 

751 

752 
fun atp_meth tac ths ctxt = 

753 
let val thy = ProofContext.theory_of ctxt 

754 
val _ = ResClause.init thy 

755 
val _ = ResHolClause.init thy 

756 
in 

757 
atp_meth' tac ths ctxt 

758 
end; 

759 

760 
fun atp_method tac = Method.thms_ctxt_args (atp_meth tac); 

761 

762 
(***************************************************************) 

763 
(* automatic ATP invocation *) 

764 
(***************************************************************) 

765 

17306  766 
(* call prover with settings and problem file for the current subgoal *) 
17764  767 
fun watcher_call_provers sign sg_terms (childin, childout, pid) = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

768 
let 
17422  769 
fun make_atp_list [] n = [] 
17717  770 
 make_atp_list (sg_term::xs) n = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

771 
let 
17717  772 
val probfile = prob_pathname n 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

773 
val time = Int.toString (!time_limit) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

774 
in 
18680  775 
Output.debug ("problem file in watcher_call_provers is " ^ probfile); 
17764  776 
(*options are separated by Watcher.setting_sep, currently #"%"*) 
17306  777 
if !prover = "spass" 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

778 
then 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

779 
let val spass = helper_path "SPASS_HOME" "SPASS" 
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

780 
val sopts = 
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

781 
"Auto%SOS=1%PGiven=0%PProblem=0%Splits=0%FullRed=0%DocProof%TimeLimit=" ^ time 
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

782 
in 
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

783 
("spass", spass, sopts, probfile) :: make_atp_list xs (n+1) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

784 
end 
17306  785 
else if !prover = "vampire" 
17235
8e55ad29b690
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents:
17234
diff
changeset

786 
then 
17819  787 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
21132  788 
val vopts = "mode casc%t " ^ time (*what about m 100000?*) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

789 
in 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

790 
("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

791 
end 
17306  792 
else if !prover = "E" 
793 
then 

17819  794 
let val Eprover = helper_path "E_HOME" "eproof" 
17306  795 
in 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

796 
("E", Eprover, 
21224  797 
"tptpin%l5%xAutoDev%tAutoDev%silent%cpulimit=" ^ time, probfile) :: 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

798 
make_atp_list xs (n+1) 
17306  799 
end 
800 
else error ("Invalid prover name: " ^ !prover) 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

801 
end 
15452  802 

17422  803 
val atp_list = make_atp_list sg_terms 1 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

804 
in 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

805 
Watcher.callResProvers(childout,atp_list); 
18680  806 
Output.debug "Sent commands to watcher!" 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

807 
end 
20022  808 

809 
fun trace_array fname = 

20995
51c41f167adc
Logging of theorem names to the /tmp directory now works
paulson
parents:
20954
diff
changeset

810 
let val path = File.unpack_platform_path fname 
20022  811 
in Array.app (File.append path o (fn s => s ^ "\n")) end; 
16357  812 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

813 
(*Converting a subgoal into negated conjecture clauses*) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

814 
fun neg_clauses th n = 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

815 
let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

816 
val st = Seq.hd (EVERY' tacs n th) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

817 
val negs = Option.valOf (metahyps_thms n st) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

818 
in make_clauses negs > ResAxioms.assume_abstract_list > Meson.finish_cnf end; 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

819 

20022  820 
(*We write out problem files for each subgoal. Argument probfile generates filenames, 
18986  821 
and allows the suppression of the suffix "_1" in problemgeneration mode. 
822 
FIXME: does not cope with &&, and it isn't easy because one could have multiple 

823 
subgoals, each involving &&.*) 

20022  824 
fun write_problem_files probfile (ctxt,th) = 
18753
aa82bd41555d
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
paulson
parents:
18700
diff
changeset

825 
let val goals = Thm.prems_of th 
19194  826 
val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) 
17717  827 
val thy = ProofContext.theory_of ctxt 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

828 
fun get_neg_subgoals [] _ = [] 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

829 
 get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

830 
val goal_cls = get_neg_subgoals goals 1 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

831 
val logic = case !linkup_logic_mode of 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

832 
Auto => problem_logic_goals (map ((map prop_of)) goal_cls) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

833 
 Fol => FOL 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

834 
 Hol => HOL 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

835 
val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

836 
val included_cls = included_thms > blacklist_filter 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

837 
> ResAxioms.cnf_rules_pairs > make_unique 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

838 
> restrict_to_logic logic 
21070  839 
val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls)) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

840 
val white_cls = ResAxioms.cnf_rules_pairs white_thms 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

841 
(*clauses relevant to goal gl*) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

842 
val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl]) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

843 
goals 
21070  844 
val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls))) 
845 
axcls_list 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

846 
val keep_types = if is_fol_logic logic then !ResClause.keep_types 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

847 
else is_typed_hol () 
19718  848 
val writer = if !prover = "spass" then dfg_writer else tptp_writer 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

849 
fun write_all [] [] _ = [] 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

850 
 write_all (ccls::ccls_list) (axcls::axcls_list) k = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

851 
let val fname = probfile k 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

852 
val axcls = make_unique axcls 
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

853 
val ccls = subtract_cls ccls axcls 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

854 
val subs = tfree_classes_of_terms (map prop_of ccls) 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

855 
and axtms = map (prop_of o #1) axcls 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

856 
val supers = tvar_classes_of_terms axtms 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

857 
and tycons = type_consts_of_terms axtms 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

858 
(*TFrees in conjecture clauses; TVars in axiom clauses*) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

859 
val classrel_clauses = 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

860 
if keep_types then ResClause.make_classrel_clauses thy subs supers 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

861 
else [] 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

862 
val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

863 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

864 
else [] 
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

865 
val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

866 
val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) [] 
20870  867 
val thm_names = Array.fromList clnames 
868 
val _ = if !Output.show_debug_msgs 

869 
then trace_array (fname ^ "_thm_names") thm_names else () 

870 
in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end 

871 
val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1) 

19194  872 
in 
20870  873 
(filenames, thm_names_list) 
19194  874 
end; 
15644  875 

17775  876 
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
877 
Posix.Process.pid * string list) option); 

878 

879 
fun kill_last_watcher () = 

880 
(case !last_watcher_pid of 

881 
NONE => () 

19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

882 
 SOME (_, _, pid, files) => 
18680  883 
(Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid); 
17775  884 
Watcher.killWatcher pid; 
20870  885 
ignore (map (try cond_rm_tmp) files))) 
18680  886 
handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed"; 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

887 

ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

888 
(*writes out the current clasimpset to a tptp file; 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

889 
turns off xsymbol at start of function, restoring it at end *) 
20954  890 
fun isar_atp_body (ctxt, th) = 
17717  891 
if Thm.no_prems th then () 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

892 
else 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

893 
let 
17775  894 
val _ = kill_last_watcher() 
20870  895 
val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th) 
896 
val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list) 

15608  897 
in 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17764
diff
changeset

898 
last_watcher_pid := SOME (childin, childout, pid, files); 
18680  899 
Output.debug ("problem files: " ^ space_implode ", " files); 
900 
Output.debug ("pid: " ^ string_of_pid pid); 

17717  901 
watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) 
20954  902 
end; 
903 

904 
val isar_atp = setmp print_mode [] isar_atp_body; 

905 

906 
(*For ML scripts, and primarily, for debugging*) 

907 
fun callatp () = 

908 
let val th = topthm() 

909 
val ctxt = ProofContext.init (theory_of_thm th) 

910 
in isar_atp_body (ctxt, th) end; 

15608  911 

17422  912 
val isar_atp_writeonly = setmp print_mode [] 
17717  913 
(fn (ctxt,th) => 
914 
if Thm.no_prems th then () 

915 
else 

20022  916 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
917 
else prob_pathname 

918 
in ignore (write_problem_files probfile (ctxt,th)) end); 

15452  919 

16357  920 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

921 
(** the Isar toplevel hook **) 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

922 

19205
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

923 
fun invoke_atp_ml (ctxt, goal) = 
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

924 
let val thy = ProofContext.theory_of ctxt; 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

925 
in 
18680  926 
Output.debug ("subgoals in isar_atp:\n" ^ 
19205
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

927 
Pretty.string_of (ProofContext.pretty_term ctxt 
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

928 
(Logic.mk_conjunction_list (Thm.prems_of goal)))); 
18680  929 
Output.debug ("current theory: " ^ Context.theory_name thy); 
20419  930 
inc hook_count; 
18680  931 
Output.debug ("in hook for time: " ^ Int.toString (!hook_count)); 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16904
diff
changeset

932 
ResClause.init thy; 
19194  933 
ResHolClause.init thy; 
21132  934 
if !time_limit > 0 then isar_atp (ctxt, goal) 
935 
else (warning "Writing problem file only"; isar_atp_writeonly (ctxt, goal)) 

19205
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

936 
end; 
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

937 

4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

938 
val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep 
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

939 
(fn state => 
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

940 
let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state) 
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

941 
in invoke_atp_ml (ctxt, goal) end); 
16357  942 

17091  943 
val call_atpP = 
17746  944 
OuterSyntax.command 
17091  945 
"ProofGeneral.call_atp" 
946 
"call automatic theorem provers" 

947 
OuterKeyword.diag 

19205
4ec788c69f82
Tidying. New invoke_atp_ml for toplevel debugging. Flag to force FOL mode.
paulson
parents:
19194
diff
changeset

948 
(Scan.succeed invoke_atp); 
17091  949 

950 
val _ = OuterSyntax.add_parsers [call_atpP]; 

951 

15347  952 
end; 