author  mengj 
Wed, 20 Sep 2006 13:53:03 +0200  
changeset 20643  267f30cbe2cb 
parent 20532  64181717e37c 
child 20661  46832fee1215 
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 
fun fake_thm_name th = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

460 
Context.theory_name (theory_of_thm th) ^ "." ^ gensym""; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

461 

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

462 
fun put_name_pair ("",th) = (fake_thm_name th, th) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

463 
 put_name_pair (a,th) = (a,th); 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

464 

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

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

466 

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

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

468 

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

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

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

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

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

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

474 

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

477 

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

479 
fun delete_numeric_suffix s = 

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

481 
last::rest => 

482 
if all_numeric last 

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

483 
then [s, space_implode "_" (rev rest)] 
20444  484 
else [s] 
485 
 [] => [s]; 

486 

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

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

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

489 

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

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

491 
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

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

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

494 
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

495 
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

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

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

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

499 

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

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

501 
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

502 

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

503 
fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

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

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

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

507 
 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

508 
 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

509 

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

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

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

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

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

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

515 

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

516 
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

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

518 

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

519 

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

520 
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

521 
 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

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

523 

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

524 

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

525 
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

526 

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

527 
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

528 

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

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

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

531 
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

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

533 

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

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

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

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

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

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

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

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

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

542 

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

543 
(*FIXME: SLOW!!!*) 
20022  544 
fun mem_thm th [] = false 
545 
 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

546 

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

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

548 
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

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

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

551 
 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

552 
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

553 
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

554 

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

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

556 
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

557 
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

558 

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

559 

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

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

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

562 
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

563 
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

564 

19894  565 
fun all_facts_of ctxt = 
566 
FactIndex.find (ProofContext.fact_index_of ctxt) ([], []) 

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

568 

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

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

570 
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894  571 
let val included_thms = 
572 
if !include_all 

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

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

574 
("Including all " ^ Int.toString (length ths) ^ " theorems")) 
19894  575 
(all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt))) 
576 
else 

577 
let val claset_thms = 

578 
if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt 

579 
else [] 

580 
val simpset_thms = 

581 
if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt 

582 
else [] 

583 
val atpset_thms = 

584 
if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt 

585 
else [] 

586 
val _ = if !Output.show_debug_msgs 

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

588 
else () 

589 
in claset_thms @ simpset_thms @ atpset_thms end 

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

591 
(if null user_thms then !whitelist else user_thms) 

592 
in 

593 
(map put_name_pair included_thms, user_rules) 

594 
end; 

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

595 

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

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

597 
fun blacklist_filter thms = 
19894  598 
if !run_blacklist_filter then 
599 
let val banned = make_banned_test (map #1 thms) 

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

601 
in filter ok thms end 

602 
else thms; 

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

603 

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

604 

19194  605 
(***************************************************************) 
606 
(* ATP invocation methods setup *) 

607 
(***************************************************************) 

608 

609 
fun cnf_hyps_thms ctxt = 

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

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

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

613 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  614 
datatype mode = Auto  Fol  Hol; 
615 

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

616 
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

617 

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

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

619 
fun restrict_to_logic logic cls = 
20532  620 
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

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

622 

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

623 
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

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

625 
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

626 
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

627 

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

628 
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

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

630 
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

631 
else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas; 
19194  632 

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

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

640 
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

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

642 
 Hol => HOL 
19894  643 
val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms 
20131
c89ee2f4efd5
Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents:
20022
diff
changeset

644 
val user_lemmas_names = map #1 user_rules 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

645 
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

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

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

648 
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

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

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

652 
val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol () 
19194  653 
val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] 
654 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] 

19722  655 
val writer = if dfg then dfg_writer else tptp_writer 
19194  656 
val file = atp_input_file() 
657 
in 

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

658 
(writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; 
19746  659 
Output.debug ("Writing to " ^ file); 
19194  660 
file) 
661 
end; 

662 

663 

664 
(**** remove tmp files ****) 

665 
fun cond_rm_tmp file = 

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

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

19194  669 

670 

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

672 
fun atp_meth' tac ths ctxt = 

673 
Method.SIMPLE_METHOD' HEADGOAL 

674 
(tac ctxt ths); 

675 

676 
fun atp_meth tac ths ctxt = 

677 
let val thy = ProofContext.theory_of ctxt 

678 
val _ = ResClause.init thy 

679 
val _ = ResHolClause.init thy 

680 
in 

681 
atp_meth' tac ths ctxt 

682 
end; 

683 

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

685 

686 
(***************************************************************) 

687 
(* automatic ATP invocation *) 

688 
(***************************************************************) 

689 

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

692 
let 
17422  693 
fun make_atp_list [] n = [] 
17717  694 
 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

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

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

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

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

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

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

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

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

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

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

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

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

713 
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

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

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

716 
end 
17306  717 
else if !prover = "E" 
718 
then 

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

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

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

723 
make_atp_list xs (n+1) 
17306  724 
end 
725 
else error ("Invalid prover name: " ^ !prover) 

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

726 
end 
15452  727 

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

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

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

732 
end 
20022  733 

734 
fun trace_array fname = 

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

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

16357  737 

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

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

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

740 
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

741 
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

742 
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

743 
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

744 

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

748 
subgoals, each involving &&.*) 

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

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

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

754 
 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

755 
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

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

757 
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

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

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

760 
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

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

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

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

764 
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

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

766 
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

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

768 
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

769 
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

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

771 
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

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

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

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

775 
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

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

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

780 
 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

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

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

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

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

787 
then trace_array "thm_names" thm_names else () 

19194  788 
in 
20022  789 
(filenames, thm_names) 
19194  790 
end; 
15644  791 

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

794 

795 
fun kill_last_watcher () = 

796 
(case !last_watcher_pid of 

797 
NONE => () 

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

798 
 SOME (_, _, pid, files) => 
18680  799 
(Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid); 
17775  800 
Watcher.killWatcher pid; 
801 
ignore (map (try OS.FileSys.remove) files))) 

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

803 

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

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

805 
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

806 
val isar_atp = setmp print_mode [] 
17717  807 
(fn (ctxt, th) => 
808 
if Thm.no_prems th then () 

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

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

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

812 
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

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

815 
last_watcher_pid := SOME (childin, childout, pid, files); 
18680  816 
Output.debug ("problem files: " ^ space_implode ", " files); 
817 
Output.debug ("pid: " ^ string_of_pid pid); 

17717  818 
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

819 
end); 
15608  820 

17422  821 
val isar_atp_writeonly = setmp print_mode [] 
17717  822 
(fn (ctxt,th) => 
823 
if Thm.no_prems th then () 

824 
else 

20022  825 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
826 
else prob_pathname 

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

15452  828 

16357  829 

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

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

831 

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

832 
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

833 
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

834 
in 
18680  835 
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

836 
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

837 
(Logic.mk_conjunction_list (Thm.prems_of goal)))); 
18680  838 
Output.debug ("current theory: " ^ Context.theory_name thy); 
20419  839 
inc hook_count; 
18680  840 
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

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

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

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

846 

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

847 
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

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

849 
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

850 
in invoke_atp_ml (ctxt, goal) end); 
16357  851 

17091  852 
val call_atpP = 
17746  853 
OuterSyntax.command 
17091  854 
"ProofGeneral.call_atp" 
855 
"call automatic theorem provers" 

856 
OuterKeyword.diag 

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

857 
(Scan.succeed invoke_atp); 
17091  858 

859 
val _ = OuterSyntax.add_parsers [call_atpP]; 

860 

15347  861 
end; 