author  wenzelm 
Wed, 08 Nov 2006 13:48:29 +0100  
changeset 21243  afffe1f72143 
parent 21224  f86b8463af37 
child 21290  33b6bb5d6ab8 
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 
15347  54 
end; 
55 

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

56 
structure ResAtp = 
15347  57 
struct 
58 

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

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

63 
(* and also explicit ATP invocation methods *) 

64 
(********************************************************************) 

65 

66 
(*** background linkup ***) 

67 
val call_atp = ref false; 

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

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

71 

72 
fun set_prover atp = 

73 
case String.map Char.toLower atp of 

74 
"e" => 

75 
(ReduceAxiomsN.max_new := 80; 

76 
ReduceAxiomsN.theory_const := false; 

77 
prover := "E") 

78 
 "spass" => 

79 
(ReduceAxiomsN.max_new := 40; 

80 
ReduceAxiomsN.theory_const := true; 

81 
prover := "spass") 

82 
 "vampire" => 

83 
(ReduceAxiomsN.max_new := 60; 

84 
ReduceAxiomsN.theory_const := false; 

85 
prover := "vampire") 

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

87 

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

89 

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

90 
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

91 
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

92 
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

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

94 

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

97 
fun helper_path evar base = 

98 
case getenv evar of 

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

100 
 home => 

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

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

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

104 
end; 

105 

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

107 
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

108 
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

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

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

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

19194  114 

115 
(*** ATP methods ***) 

116 
val vampire_time = ref 60; 

117 
val eprover_time = ref 60; 

19722  118 
val spass_time = ref 60; 
119 

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

122 
else vampire_time:=60; 

123 

124 
fun run_eprover time = 

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

126 
else eprover_time:=60; 

127 

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

130 
else spass_time:=60; 

131 

132 

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

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

137 
val fol_keep_types = ResClause.keep_types; 

138 
val hol_full_types = ResHolClause.full_types; 

139 
val hol_partial_types = ResHolClause.partial_types; 

140 
val hol_const_types_only = ResHolClause.const_types_only; 

141 
val hol_no_types = ResHolClause.no_types; 

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

143 
fun is_typed_hol () = 

144 
let val tp_level = hol_typ_level() 

145 
in 

146 
not (tp_level = ResHolClause.T_NONE) 

147 
end; 

148 

149 
fun atp_input_file () = 

150 
let val file = !problem_name 

151 
in 

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

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

154 
then !destdir ^ "/" ^ file 

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

156 
end; 

157 

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

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

161 
val include_atpset = ref true; 

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

162 

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

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

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

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

166 

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

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

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

169 

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

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

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

172 

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

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

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

175 

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

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

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

179 

180 
(**** relevance filter ****) 

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

181 
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

182 
val run_blacklist_filter = ref true; 
19194  183 

184 
(******************************************************************) 

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

186 
(******************************************************************) 

187 

188 
datatype logic = FOL  HOL  HOLC  HOLCS; 

189 

190 
fun string_of_logic FOL = "FOL" 

191 
 string_of_logic HOL = "HOL" 

192 
 string_of_logic HOLC = "HOLC" 

193 
 string_of_logic HOLCS = "HOLCS"; 

194 

195 
fun is_fol_logic FOL = true 

196 
 is_fol_logic _ = false 

197 

198 
(*HOLCS will not occur here*) 

199 
fun upgrade_lg HOLC _ = HOLC 

200 
 upgrade_lg HOL HOLC = HOLC 

201 
 upgrade_lg HOL _ = HOL 

202 
 upgrade_lg FOL lg = lg; 

203 

204 
(* check types *) 

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

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

208 
 has_bool_hfn _ = false; 

19194  209 

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

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

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

218 
in 

219 
exists (has_bool_hfn) targs 

220 
end; 

19194  221 

222 
exception FN_LG of term; 

223 

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

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

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

233 

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

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

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

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

237 
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

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

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

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

241 
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

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

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

246 
exception PRED_LG of term; 

247 

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

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

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

255 

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

257 
 lit_lg P (lg,seen) = 

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

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

259 
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

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

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

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

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

265 
end; 
19194  266 

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

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

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

269 
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

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

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

272 
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

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

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

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

277 
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

278 
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

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

280 

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

281 
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

282 

19194  283 
fun logic_of_clause tm (lg,seen) = 
284 
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

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

288 
end; 

289 

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

291 
 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

292 
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

293 
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

294 
if is_fol_logic lg then () 
19746  295 
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

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

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

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

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

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

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

304 

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

306 

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

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

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

309 
(***************************************************************) 
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 
(*** white list and black list of 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 
(*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

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

315 

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

318 

319 
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

320 
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

321 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

338 
"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

339 
"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

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

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

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

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

344 
"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

345 
"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

346 
"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

347 
"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

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

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

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

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

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

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

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

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

356 
"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

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

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

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

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

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

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

363 
"Nat.one_eq_mult_iff", (*duplicate by symmetry*) 
21243  364 
"Nat.of_nat_0_eq_iff", 
365 
"Nat.of_nat_eq_0_iff", 

366 
"Nat.of_nat_le_0_iff", 

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

367 
"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

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

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

370 
"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

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

372 
"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

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

374 
"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

375 
"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

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

377 
"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

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

379 
"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

380 
"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

381 
"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

382 
"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

383 
"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

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

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

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

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

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

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

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

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

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

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

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

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

396 
"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

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

398 
"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

399 
"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

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

401 
"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

402 
"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

403 
"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

404 
"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

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

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

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

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

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

410 
"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

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

412 
"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

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

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

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

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

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

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

419 
"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

420 
"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

421 
"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

422 
"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

423 
"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

424 
"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

425 
"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

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

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

428 
"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

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

430 
"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

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

432 
"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

433 
"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

434 
"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

435 
"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

436 
"Ring_and_Field.one_eq_divide_iff", (*duplicate by symmetry*) 
20444  437 
"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

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

439 
"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

440 
"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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

455 
"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

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

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

458 
"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

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

460 
"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

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

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

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

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

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

466 

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

467 

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

468 
(*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

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

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

471 
"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

472 
"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

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

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

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

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

477 

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

478 
(*** 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

479 

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

480 
(*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

481 

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

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

483 

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

484 
(*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

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

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

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

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

489 

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

492 

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

494 
fun delete_numeric_suffix s = 

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

496 
last::rest => 

497 
if all_numeric last 

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

498 
then [s, space_implode "_" (rev rest)] 
20444  499 
else [s] 
500 
 [] => [s]; 

501 

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

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

503 
(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

504 

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

505 
(*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

506 
"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

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

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

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

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

511 

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

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

513 
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

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

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

516 
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

517 
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

518 
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

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

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

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

522 

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

523 
(** 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

524 
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

525 

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

526 
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

527 
 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

528 
 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

529 
 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

530 
 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

531 
 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

532 

21070  533 
fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0)) 
534 
 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

535 

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

536 

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

537 
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

538 
 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

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

540 

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

541 
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

542 

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

543 
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

544 

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

545 
(*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

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

547 
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

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

549 

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

550 
(*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

551 
(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

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

553 
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

554 
in 
21070  555 
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

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

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

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

559 

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

560 
(*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

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

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

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

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

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

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

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

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

569 

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

570 
(*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

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

572 
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

573 
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

574 

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

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

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

577 
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

578 
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

579 

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

582 
filter (ProofContext.valid_thms ctxt) 

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

584 

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

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

587 

588 
fun multi_names ((a, []), pairs) = pairs 

589 
 multi_names ((a, [th]), pairs) = (a,th)::pairs 

590 
 multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths); 

591 

592 
fun name_thm_pairs ctxt = foldl multi_names [] (all_valid_thms ctxt); 

593 

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

595 
 check_named (_,th) = true; 

19894  596 

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

597 
(* 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

598 
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894  599 
let val included_thms = 
600 
if !include_all 

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

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

602 
("Including all " ^ Int.toString (length ths) ^ " theorems")) 
21224  603 
(name_thm_pairs ctxt)) 
19894  604 
else 
605 
let val claset_thms = 

606 
if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt 

607 
else [] 

608 
val simpset_thms = 

609 
if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt 

610 
else [] 

611 
val atpset_thms = 

612 
if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt 

613 
else [] 

614 
val _ = if !Output.show_debug_msgs 

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

616 
else () 

617 
in claset_thms @ simpset_thms @ atpset_thms end 

21224  618 
val user_rules = filter check_named 
619 
(map (ResAxioms.pairname) 

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

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

624 

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

625 
(*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

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

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

633 
in okthms end 

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

635 

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

636 

19194  637 
(***************************************************************) 
638 
(* ATP invocation methods setup *) 

639 
(***************************************************************) 

640 

641 
fun cnf_hyps_thms ctxt = 

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

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

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

645 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  646 
datatype mode = Auto  Fol  Hol; 
647 

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

648 
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

649 

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

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

651 
fun restrict_to_logic logic cls = 
20532  652 
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

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

654 

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

655 
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

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

657 
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

658 
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

659 

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

660 
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

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

662 
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

663 
else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas; 
19194  664 

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

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

672 
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

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

674 
 Hol => HOL 
19894  675 
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

676 
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

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

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

679 
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

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

681 
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

682 
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

683 
val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol () 
19194  684 
val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] 
685 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] 

19722  686 
val writer = if dfg then dfg_writer else tptp_writer 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

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

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

690 
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

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

692 
file 
19194  693 
end; 
694 

695 

696 
(**** remove tmp files ****) 

697 
fun cond_rm_tmp file = 

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

19194  700 

701 

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

703 
fun atp_meth' tac ths ctxt = 

704 
Method.SIMPLE_METHOD' HEADGOAL 

705 
(tac ctxt ths); 

706 

707 
fun atp_meth tac ths ctxt = 

708 
let val thy = ProofContext.theory_of ctxt 

709 
val _ = ResClause.init thy 

710 
val _ = ResHolClause.init thy 

711 
in 

712 
atp_meth' tac ths ctxt 

713 
end; 

714 

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

716 

717 
(***************************************************************) 

718 
(* automatic ATP invocation *) 

719 
(***************************************************************) 

720 

17306  721 
(* call prover with settings and problem file for the current subgoal *) 
17764  722 
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

723 
let 
17422  724 
fun make_atp_list [] n = [] 
17717  725 
 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

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

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

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

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

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

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

736 
"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

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

738 
("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

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

741 
then 
17819  742 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
21132  743 
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

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

745 
("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

746 
end 
17306  747 
else if !prover = "E" 
748 
then 

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

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

753 
make_atp_list xs (n+1) 
17306  754 
end 
755 
else error ("Invalid prover name: " ^ !prover) 

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

756 
end 
15452  757 

17422  758 
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

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

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

762 
end 
20022  763 

764 
fun trace_array fname = 

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

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

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

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

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

770 
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

771 
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

772 
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

773 
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

774 

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

778 
subgoals, each involving &&.*) 

20022  779 
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

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

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

784 
 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

785 
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

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

787 
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

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

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

790 
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

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

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

793 
> restrict_to_logic logic 
21070  794 
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

795 
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

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

797 
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

798 
goals 
21070  799 
val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls))) 
800 
axcls_list 

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

801 
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

802 
else is_typed_hol () 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

803 
val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

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

805 
val _ = Output.debug ("classrel clauses = " ^ 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

806 
Int.toString (length classrel_clauses)) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

807 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

808 
else [] 
18680  809 
val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) 
19718  810 
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

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

812 
 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

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

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

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

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

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

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

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

19194  822 
in 
20870  823 
(filenames, thm_names_list) 
19194  824 
end; 
15644  825 

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

828 

829 
fun kill_last_watcher () = 

830 
(case !last_watcher_pid of 

831 
NONE => () 

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

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

837 

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

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

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

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

843 
let 
17775  844 
val _ = kill_last_watcher() 
20870  845 
val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th) 
846 
val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list) 

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

848 
last_watcher_pid := SOME (childin, childout, pid, files); 
18680  849 
Output.debug ("problem files: " ^ space_implode ", " files); 
850 
Output.debug ("pid: " ^ string_of_pid pid); 

17717  851 
watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) 
20954  852 
end; 
853 

854 
val isar_atp = setmp print_mode [] isar_atp_body; 

855 

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

857 
fun callatp () = 

858 
let val th = topthm() 

859 
val ctxt = ProofContext.init (theory_of_thm th) 

860 
in isar_atp_body (ctxt, th) end; 

15608  861 

17422  862 
val isar_atp_writeonly = setmp print_mode [] 
17717  863 
(fn (ctxt,th) => 
864 
if Thm.no_prems th then () 

865 
else 

20022  866 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
867 
else prob_pathname 

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

15452  869 

16357  870 

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

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

872 

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

873 
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

874 
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

875 
in 
18680  876 
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

877 
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

878 
(Logic.mk_conjunction_list (Thm.prems_of goal)))); 
18680  879 
Output.debug ("current theory: " ^ Context.theory_name thy); 
20419  880 
inc hook_count; 
18680  881 
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

882 
ResClause.init thy; 
19194  883 
ResHolClause.init thy; 
21132  884 
if !time_limit > 0 then isar_atp (ctxt, goal) 
885 
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

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

887 

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

888 
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

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

890 
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

891 
in invoke_atp_ml (ctxt, goal) end); 
16357  892 

17091  893 
val call_atpP = 
17746  894 
OuterSyntax.command 
17091  895 
"ProofGeneral.call_atp" 
896 
"call automatic theorem provers" 

897 
OuterKeyword.diag 

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

898 
(Scan.succeed invoke_atp); 
17091  899 

900 
val _ = OuterSyntax.add_parsers [call_atpP]; 

901 

15347  902 
end; 