author  paulson 
Mon, 02 Oct 2006 17:30:56 +0200  
changeset 20823  5480ec4b542d 
parent 20781  e26fe5c63c2f 
child 20854  f9cf9e62d11c 
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 

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

8 
(*FIXME: Do we need this signature?*) 
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 
19194  17 

18 
datatype mode = Auto  Fol  Hol 

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

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

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

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

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

19194  32 
val cond_rm_tmp: string > unit 
33 
val keep_atp_input: bool ref 

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 

19194  59 
(********************************************************************) 
60 
(* some settings for both background automatic ATP calling procedure*) 

61 
(* and also explicit ATP invocation methods *) 

62 
(********************************************************************) 

63 

64 
(*** background linkup ***) 

65 
val call_atp = ref false; 

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

66 
val hook_count = ref 0; 
20419  67 
val time_limit = ref 80; 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17317
diff
changeset

68 
val prover = ref "E"; (* use E as the default prover *) 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset

69 
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

70 
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

71 
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

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

73 

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

76 
fun helper_path evar base = 

77 
case getenv evar of 

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

79 
 home => 

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

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

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

83 
end; 

84 

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

86 
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

87 
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

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

89 
else error ("No such directory: " ^ !destdir); 
15644  90 

17717  91 
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; 
92 

19194  93 

94 
(*** ATP methods ***) 

95 
val vampire_time = ref 60; 

96 
val eprover_time = ref 60; 

19722  97 
val spass_time = ref 60; 
98 

19194  99 
fun run_vampire time = 
100 
if (time >0) then vampire_time:= time 

101 
else vampire_time:=60; 

102 

103 
fun run_eprover time = 

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

105 
else eprover_time:=60; 

106 

19722  107 
fun run_spass time = 
108 
if (time > 0) then spass_time:=time 

109 
else spass_time:=60; 

110 

111 

19194  112 
fun vampireLimit () = !vampire_time; 
113 
fun eproverLimit () = !eprover_time; 

19722  114 
fun spassLimit () = !spass_time; 
19194  115 

116 
val keep_atp_input = ref false; 

117 
val fol_keep_types = ResClause.keep_types; 

118 
val hol_full_types = ResHolClause.full_types; 

119 
val hol_partial_types = ResHolClause.partial_types; 

120 
val hol_const_types_only = ResHolClause.const_types_only; 

121 
val hol_no_types = ResHolClause.no_types; 

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

123 
fun is_typed_hol () = 

124 
let val tp_level = hol_typ_level() 

125 
in 

126 
not (tp_level = ResHolClause.T_NONE) 

127 
end; 

128 

129 
fun atp_input_file () = 

130 
let val file = !problem_name 

131 
in 

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

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

134 
then !destdir ^ "/" ^ file 

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

136 
end; 

137 

19894  138 
val include_all = ref false; 
19194  139 
val include_simpset = ref false; 
140 
val include_claset = ref false; 

141 
val include_atpset = ref true; 

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

142 

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

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

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

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

146 

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

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

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

149 

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

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

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

152 

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

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

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

155 

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

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

157 
fun rm_atpset() = include_atpset:=false; 
19194  158 

159 

160 
(**** relevance filter ****) 

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

161 
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

162 
val run_blacklist_filter = ref true; 
19194  163 

164 
(******************************************************************) 

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

166 
(******************************************************************) 

167 

168 
datatype logic = FOL  HOL  HOLC  HOLCS; 

169 

170 
fun string_of_logic FOL = "FOL" 

171 
 string_of_logic HOL = "HOL" 

172 
 string_of_logic HOLC = "HOLC" 

173 
 string_of_logic HOLCS = "HOLCS"; 

174 

175 
fun is_fol_logic FOL = true 

176 
 is_fol_logic _ = false 

177 

178 
(*HOLCS will not occur here*) 

179 
fun upgrade_lg HOLC _ = HOLC 

180 
 upgrade_lg HOL HOLC = HOLC 

181 
 upgrade_lg HOL _ = HOL 

182 
 upgrade_lg FOL lg = lg; 

183 

184 
(* check types *) 

19451  185 
fun has_bool_hfn (Type("bool",_)) = true 
186 
 has_bool_hfn (Type("fun",_)) = true 

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

188 
 has_bool_hfn _ = false; 

19194  189 

19451  190 
fun is_hol_fn tp = 
19194  191 
let val (targs,tr) = strip_type tp 
192 
in 

19451  193 
exists (has_bool_hfn) (tr::targs) 
19194  194 
end; 
195 

19451  196 
fun is_hol_pred tp = 
197 
let val (targs,tr) = strip_type tp 

198 
in 

199 
exists (has_bool_hfn) targs 

200 
end; 

19194  201 

202 
exception FN_LG of term; 

203 

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

19451  205 
if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
19194  206 
 fn_lg (t as Free(f,tp)) (lg,seen) = 
19451  207 
if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
19194  208 
 fn_lg (t as Var(f,tp)) (lg,seen) = 
19451  209 
if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen) 
19194  210 
 fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen) 
211 
 fn_lg f _ = raise FN_LG(f); 

212 

213 

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

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

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

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

217 
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

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

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

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

221 
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

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

223 
end 
19194  224 
 term_lg _ (lg,seen) = (lg,seen) 
225 

226 
exception PRED_LG of term; 

227 

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

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

229 
if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
19194  230 
 pred_lg (t as Free(P,tp)) (lg,seen) = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

231 
if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
19194  232 
 pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen) 
233 
 pred_lg P _ = raise PRED_LG(P); 

234 

235 

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

237 
 lit_lg P (lg,seen) = 

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

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

239 
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

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

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

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

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

245 
end; 
19194  246 

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

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

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

249 
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

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

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

252 
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

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

254 
end 
19194  255 
 lits_lg lits (lg,seen) = (lg,seen); 
256 

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

257 
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

258 
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

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

260 

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

261 
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

262 

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

265 
val disjs = dest_disj tm' 
19194  266 
in 
267 
lits_lg disjs (lg,seen) 

268 
end; 

269 

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

271 
 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

272 
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

273 
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

274 
if is_fol_logic lg then () 
19746  275 
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

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

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

278 
end 
19194  279 
 logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); 
280 

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

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

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

284 

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

286 

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

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

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

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

290 

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

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

292 

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

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

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

295 

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

298 

299 
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

300 
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

301 
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

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

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

304 
["Datatype.prod.size", 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

305 
"Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*) 
20372
e42674e0486e
blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents:
20289
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

445 

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

446 

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

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

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

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

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

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

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

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

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

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

456 

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

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

458 

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

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

460 

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

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

462 

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

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

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

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

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

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

468 

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

471 

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

473 
fun delete_numeric_suffix s = 

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

475 
last::rest => 

476 
if all_numeric last 

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

477 
then [s, space_implode "_" (rev rest)] 
20444  478 
else [s] 
479 
 [] => [s]; 

480 

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

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

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

483 

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

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

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

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

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

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

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

490 

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

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

492 
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

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

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

495 
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

496 
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

497 
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

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

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

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

501 

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

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

503 
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

504 

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

505 
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

506 
 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

507 
 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

508 
 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

509 
 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

510 
 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

511 

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

512 
fun hashw_pred (P,w) = 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

513 
let val (p,args) = strip_comb P 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

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

515 
List.foldl hashw_term w (p::args) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

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

517 

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

518 
fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0)) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

519 
 hash_literal P = hashw_pred(P,0w0); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

520 

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

521 

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

522 
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

523 
 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

524 
 get_literals lit lits = (lit::lits); 
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 

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

527 
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

528 

20661
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

529 
(*Versions ONLY for "faking" a theorem name. Here we take variable names into account 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

530 
so that similar theorems don't collide. FIXME: this entire business of "faking" 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

531 
theorem names must end!*) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

532 
fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w)) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

533 
 hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

534 
 hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts); 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

535 

46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

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

537 
 full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

538 
 full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w)) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

539 
 full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

540 
 full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w)) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

541 
 full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w))); 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

542 

46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

543 
fun full_hashw_thm (th,w) = 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

544 
let val {prop,hyps,...} = rep_thm th 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

545 
in List.foldl full_hashw_term w (prop::hyps) end 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

546 

46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

547 
fun full_hash_thm th = full_hashw_thm (th,0w0); 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

548 

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

549 
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

550 

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

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

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

553 
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

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

555 

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

556 
(*Use a hash table to eliminate duplicates from xs. Argument is a list of 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

557 
(name, theorem) pairs, but the theorems are hashed into the table. *) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

558 
fun make_unique xs = 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

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

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

561 
(app (ignore o Polyhash.peekInsert ht) (map swap xs); 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

562 
map swap (Polyhash.listItems ht)) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

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

564 

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

565 
(*FIXME: SLOW!!!*) 
20022  566 
fun mem_thm th [] = false 
567 
 mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names; 

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

568 

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

569 
(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses. 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

570 
It would be faster to compare names, rather than theorems, and to use 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

571 
a symbol table or hash table.*) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

572 
fun insert_thms [] thms_names = thms_names 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

573 
 insert_thms ((thm,name)::thms_names) thms_names' = 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

574 
if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

575 
else insert_thms thms_names ((thm,name)::thms_names'); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

576 

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

577 
(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

578 
fun get_relevant_clauses thy cls_thms white_cls goals = 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

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

580 

20661
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

581 
(*This name is cryptic but short. Unlike gensym, we get the same name each time.*) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

582 
fun fake_thm_name th = 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

583 
Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th); 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

584 

46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

585 
fun put_name_pair ("",th) = (fake_thm_name th, th) 
46832fee1215
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents:
20643
diff
changeset

586 
 put_name_pair (a,th) = (a,th); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

587 

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

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

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

590 
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

591 
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

592 

19894  593 
fun all_facts_of ctxt = 
594 
FactIndex.find (ProofContext.fact_index_of ctxt) ([], []) 

595 
> maps #2 > map (`Thm.name_of_thm); 

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")) 
19894  603 
(all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt))) 
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 

618 
val user_rules = map (put_name_pair o ResAxioms.pairname) 

619 
(if null user_thms then !whitelist else user_thms) 

620 
in 

621 
(map put_name_pair included_thms, user_rules) 

622 
end; 

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

623 

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

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

625 
fun blacklist_filter thms = 
19894  626 
if !run_blacklist_filter then 
627 
let val banned = make_banned_test (map #1 thms) 

628 
fun ok (a,_) = not (banned a) 

629 
in filter ok thms end 

630 
else thms; 

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

631 

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

632 

19194  633 
(***************************************************************) 
634 
(* ATP invocation methods setup *) 

635 
(***************************************************************) 

636 

637 
fun cnf_hyps_thms ctxt = 

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

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

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

641 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  642 
datatype mode = Auto  Fol  Hol; 
643 

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

644 
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

645 

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

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

647 
fun restrict_to_logic logic cls = 
20532  648 
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

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

650 

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

651 
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

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

653 
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

654 
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

655 

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

656 
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

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

658 
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

659 
else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas; 
19194  660 

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

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

668 
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

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

670 
 Hol => HOL 
19894  671 
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

672 
val cla_simp_atp_clauses = included_thms > blacklist_filter 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

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

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

675 
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

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

677 
val axclauses = get_relevant_clauses thy cla_simp_atp_clauses 
20022  678 
user_cls (map prop_of goal_cls) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

679 
val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol () 
19194  680 
val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] 
681 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] 

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

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

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

686 
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

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

688 
file 
19194  689 
end; 
690 

691 

692 
(**** remove tmp files ****) 

693 
fun cond_rm_tmp file = 

19746  694 
if !keep_atp_input then Output.debug "ATP input kept..." 
695 
else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir)) 

696 
else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file); 

19194  697 

698 

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

700 
fun atp_meth' tac ths ctxt = 

701 
Method.SIMPLE_METHOD' HEADGOAL 

702 
(tac ctxt ths); 

703 

704 
fun atp_meth tac ths ctxt = 

705 
let val thy = ProofContext.theory_of ctxt 

706 
val _ = ResClause.init thy 

707 
val _ = ResHolClause.init thy 

708 
in 

709 
atp_meth' tac ths ctxt 

710 
end; 

711 

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

713 

714 
(***************************************************************) 

715 
(* automatic ATP invocation *) 

716 
(***************************************************************) 

717 

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

720 
let 
17422  721 
fun make_atp_list [] n = [] 
17717  722 
 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

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

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

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

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

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

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

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

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

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

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

738 
then 
17819  739 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

740 
val casc = if !time_limit > 70 then "mode casc%" else "" 
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

741 
val vopts = casc ^ "m 100000%t " ^ time 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

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

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

744 
end 
17306  745 
else if !prover = "E" 
746 
then 

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

749 
("E", Eprover, 
19744
73aab222fecb
Giving the "silent" switch to E, to produce less output
paulson
parents:
19722
diff
changeset

750 
"tptpin%l5%xAuto%tAuto%silent%cpulimit=" ^ time, probfile) :: 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

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

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

754 
end 
15452  755 

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

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

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

760 
end 
20022  761 

762 
fun trace_array fname = 

763 
let val path = File.tmp_path (Path.basic fname) 

764 
in Array.app (File.append path o (fn s => s ^ "\n")) end; 

16357  765 

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

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

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

768 
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

769 
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

770 
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

771 
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

772 

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

776 
subgoals, each involving &&.*) 

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

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

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

782 
 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

783 
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

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

785 
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

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

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

788 
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

789 
val included_cls = included_thms > blacklist_filter 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

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

791 
> restrict_to_logic logic 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

792 
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

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

794 
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

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

796 
val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls)) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

797 
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

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

799 
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

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

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

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

803 
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

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

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

808 
 write_all (ccls::ccls_list) (axcls::axcls_list) k = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

809 
(writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [], 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

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

811 
:: write_all ccls_list axcls_list (k+1) 
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

812 
val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1) 
20022  813 
val thm_names = Array.fromList clnames 
814 
val _ = if !Output.show_debug_msgs 

815 
then trace_array "thm_names" thm_names else () 

19194  816 
in 
20022  817 
(filenames, thm_names) 
19194  818 
end; 
15644  819 

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

822 

823 
fun kill_last_watcher () = 

824 
(case !last_watcher_pid of 

825 
NONE => () 

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

826 
 SOME (_, _, pid, files) => 
18680  827 
(Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid); 
17775  828 
Watcher.killWatcher pid; 
829 
ignore (map (try OS.FileSys.remove) files))) 

18680  830 
handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed"; 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

831 

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

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

833 
turns off xsymbol at start of function, restoring it at end *) 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

834 
val isar_atp = setmp print_mode [] 
17717  835 
(fn (ctxt, th) => 
836 
if Thm.no_prems th then () 

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

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

838 
let 
17775  839 
val _ = kill_last_watcher() 
19675
a4894fb2a5f2
removing the string array from the result of get_clasimp_atp_lemmas
paulson
parents:
19641
diff
changeset

840 
val (files,thm_names) = write_problem_files prob_pathname (ctxt,th) 
a4894fb2a5f2
removing the string array from the result of get_clasimp_atp_lemmas
paulson
parents:
19641
diff
changeset

841 
val (childin, childout, pid) = Watcher.createWatcher (th, thm_names) 
15608  842 
in 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17764
diff
changeset

843 
last_watcher_pid := SOME (childin, childout, pid, files); 
18680  844 
Output.debug ("problem files: " ^ space_implode ", " files); 
845 
Output.debug ("pid: " ^ string_of_pid pid); 

17717  846 
watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

847 
end); 
15608  848 

17422  849 
val isar_atp_writeonly = setmp print_mode [] 
17717  850 
(fn (ctxt,th) => 
851 
if Thm.no_prems th then () 

852 
else 

20022  853 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
854 
else prob_pathname 

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

15452  856 

16357  857 

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

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

859 

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

860 
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

861 
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

862 
in 
18680  863 
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

864 
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

865 
(Logic.mk_conjunction_list (Thm.prems_of goal)))); 
18680  866 
Output.debug ("current theory: " ^ Context.theory_name thy); 
20419  867 
inc hook_count; 
18680  868 
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

869 
ResClause.init thy; 
19194  870 
ResHolClause.init thy; 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

871 
if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal) 
17502  872 
else 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

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

874 

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

875 
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

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

877 
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

878 
in invoke_atp_ml (ctxt, goal) end); 
16357  879 

17091  880 
val call_atpP = 
17746  881 
OuterSyntax.command 
17091  882 
"ProofGeneral.call_atp" 
883 
"call automatic theorem provers" 

884 
OuterKeyword.diag 

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

885 
(Scan.succeed invoke_atp); 
17091  886 

887 
val _ = OuterSyntax.add_parsers [call_atpP]; 

888 

15347  889 
end; 