author  paulson 
Fri, 24 Aug 2007 14:16:44 +0200  
changeset 24425  ca97c6f3d9cd 
parent 24320  ea5be4be3bae 
child 24546  c90cee3163b7 
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 

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

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

9 
sig 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

10 
val prover: ResReconstruct.atp ref 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

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

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

14 
val time_limit: int ref 
21224  15 
val set_prover: string > unit 
21588  16 

19194  17 
datatype mode = Auto  Fol  Hol 
19450
651d949776f8
exported linkup_logic_mode and changed the default setting
paulson
parents:
19445
diff
changeset

18 
val linkup_logic_mode : mode ref 
19722  19 
val write_subgoal_file: bool > mode > Proof.context > thm list > thm list > int > string 
19194  20 
val cond_rm_tmp: string > unit 
20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

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

23 
val run_blacklist_filter: bool ref 
24287  24 
val theory_const : bool ref 
25 
val pass_mark : real ref 

26 
val convergence : real ref 

27 
val max_new : int ref 

28 
val follow_defs : bool ref 

19894  29 
val add_all : unit > unit 
19227
d15f2baa7ecc
Added more functions to the signature and tidied up some functions.
mengj
parents:
19205
diff
changeset

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

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

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

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

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

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

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

38 
val rm_clasimp : unit > unit 
21311  39 
val is_fol_thms : thm list > bool 
22989  40 
val tvar_classes_of_terms : term list > string list 
41 
val tfree_classes_of_terms : term list > string list 

42 
val type_consts_of_terms : theory > term list > string list 

15347  43 
end; 
44 

22865  45 
structure ResAtp: RES_ATP = 
15347  46 
struct 
47 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

48 
structure Recon = ResReconstruct; 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

49 

22130  50 
fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s)); 
21070  51 

19194  52 
(********************************************************************) 
53 
(* some settings for both background automatic ATP calling procedure*) 

54 
(* and also explicit ATP invocation methods *) 

55 
(********************************************************************) 

56 

57 
(*** background linkup ***) 

24287  58 
val run_blacklist_filter = ref true; 
21224  59 
val time_limit = ref 60; 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

60 
val prover = ref Recon.E; 
21224  61 

24287  62 
(*** relevance filter parameters ***) 
63 
val run_relevance_filter = ref true; 

64 
val theory_const = ref true; 

65 
val pass_mark = ref 0.5; 

66 
val convergence = ref 3.2; (*Higher numbers allow longer inference chains*) 

67 
val max_new = ref 60; (*Limits how many clauses can be picked up per stage*) 

68 
val follow_defs = ref false; (*Follow definitions. Makes problems bigger.*) 

69 

21588  70 
fun set_prover atp = 
21224  71 
case String.map Char.toLower atp of 
21588  72 
"e" => 
24287  73 
(max_new := 100; 
74 
theory_const := false; 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

75 
prover := Recon.E) 
21588  76 
 "spass" => 
24287  77 
(max_new := 40; 
78 
theory_const := true; 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

79 
prover := Recon.SPASS) 
21588  80 
 "vampire" => 
24287  81 
(max_new := 60; 
82 
theory_const := false; 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

83 
prover := Recon.Vampire) 
21224  84 
 _ => error ("No such prover: " ^ atp); 
85 

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

87 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

88 
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

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

90 

17819  91 
(*Return the path to a "helper" like SPASS or tptp2X, first checking that 
21588  92 
it exists. FIXME: modify to use Path primitives and move to some central place.*) 
17819  93 
fun helper_path evar base = 
94 
case getenv evar of 

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

21588  96 
 home => 
17819  97 
let val path = home ^ "/" ^ base 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

98 
in if File.exists (File.explode_platform_path path) then path 
21588  99 
else error ("Could not find the file " ^ path) 
100 
end; 

17819  101 

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

103 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name))) 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

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

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

106 
else error ("No such directory: " ^ !destdir); 
15644  107 

17717  108 
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; 
109 

19194  110 
fun atp_input_file () = 
21588  111 
let val file = !problem_name 
19194  112 
in 
21588  113 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file)) 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

114 
else if File.exists (File.explode_platform_path (!destdir)) 
21588  115 
then !destdir ^ "/" ^ file 
116 
else error ("No such directory: " ^ !destdir) 

19194  117 
end; 
118 

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

119 
val include_all = ref true; 
19194  120 
val include_simpset = ref false; 
21588  121 
val include_claset = ref false; 
19194  122 
val include_atpset = ref true; 
20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

123 

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

124 
(*Tests show that follow_defs gives VERY poor results with "include_all"*) 
24287  125 
fun add_all() = (include_all:=true; follow_defs := false); 
20246
fdfe7399e057
"all theorems" mode forces definitionexpansion off.
paulson
parents:
20224
diff
changeset

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

127 

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

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

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

130 

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

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

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

133 

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

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

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

136 

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

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

138 
fun rm_atpset() = include_atpset:=false; 
19194  139 

140 

141 
(******************************************************************) 

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

143 
(******************************************************************) 

144 

145 
datatype logic = FOL  HOL  HOLC  HOLCS; 

146 

147 
fun string_of_logic FOL = "FOL" 

148 
 string_of_logic HOL = "HOL" 

149 
 string_of_logic HOLC = "HOLC" 

150 
 string_of_logic HOLCS = "HOLCS"; 

151 

152 
fun is_fol_logic FOL = true 

153 
 is_fol_logic _ = false 

154 

155 
(*HOLCS will not occur here*) 

156 
fun upgrade_lg HOLC _ = HOLC 

157 
 upgrade_lg HOL HOLC = HOLC 

158 
 upgrade_lg HOL _ = HOL 

21588  159 
 upgrade_lg FOL lg = lg; 
19194  160 

161 
(* check types *) 

19451  162 
fun has_bool_hfn (Type("bool",_)) = true 
163 
 has_bool_hfn (Type("fun",_)) = true 

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

165 
 has_bool_hfn _ = false; 

19194  166 

19451  167 
fun is_hol_fn tp = 
19194  168 
let val (targs,tr) = strip_type tp 
169 
in 

21588  170 
exists (has_bool_hfn) (tr::targs) 
19194  171 
end; 
172 

19451  173 
fun is_hol_pred tp = 
174 
let val (targs,tr) = strip_type tp 

175 
in 

21588  176 
exists (has_bool_hfn) targs 
19451  177 
end; 
19194  178 

179 
exception FN_LG of term; 

180 

21588  181 
fun fn_lg (t as Const(f,tp)) (lg,seen) = 
182 
if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 

183 
 fn_lg (t as Free(f,tp)) (lg,seen) = 

184 
if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 

19194  185 
 fn_lg (t as Var(f,tp)) (lg,seen) = 
20854  186 
if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen) 
187 
 fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen) 

21588  188 
 fn_lg f _ = raise FN_LG(f); 
19194  189 

190 

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

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

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

193 
let val (f,args) = strip_comb tm 
21588  194 
val (lg',seen') = if f mem seen then (FOL,seen) 
195 
else fn_lg f (FOL,seen) 

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

196 
in 
21588  197 
if is_fol_logic lg' then () 
22130  198 
else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f)); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

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

200 
end 
19194  201 
 term_lg _ (lg,seen) = (lg,seen) 
202 

203 
exception PRED_LG of term; 

204 

21588  205 
fun pred_lg (t as Const(P,tp)) (lg,seen)= 
206 
if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 

207 
else (lg,insert (op =) t seen) 

19194  208 
 pred_lg (t as Free(P,tp)) (lg,seen) = 
21588  209 
if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

210 
else (lg,insert (op =) t seen) 
20854  211 
 pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen) 
19194  212 
 pred_lg P _ = raise PRED_LG(P); 
213 

214 

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

216 
 lit_lg P (lg,seen) = 

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

217 
let val (pred,args) = strip_comb P 
21588  218 
val (lg',seen') = if pred mem seen then (lg,seen) 
219 
else pred_lg pred (lg,seen) 

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

220 
in 
21588  221 
if is_fol_logic lg' then () 
22130  222 
else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)); 
21588  223 
term_lg args (lg',seen') 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

224 
end; 
19194  225 

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

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

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

228 
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

229 
in 
21588  230 
if is_fol_logic lg then () 
22130  231 
else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit)); 
21588  232 
lits_lg lits (lg,seen') 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

233 
end 
19194  234 
 lits_lg lits (lg,seen) = (lg,seen); 
235 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

236 
fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

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

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

239 

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

240 
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

241 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

242 
fun logic_of_clause tm = lits_lg (dest_disj tm); 
19194  243 

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

245 
 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

246 
let val (lg,seen') = logic_of_clause cls (FOL,seen) 
21588  247 
val _ = 
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

248 
if is_fol_logic lg then () 
22130  249 
else Output.debug (fn () => ("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

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

252 
end 
19194  253 
 logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); 
254 

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

21588  256 
 problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
19194  257 
problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen)); 
21588  258 

19194  259 
fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]); 
260 

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

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

263 
(***************************************************************) 
24287  264 
(* Relevance Filtering *) 
265 
(***************************************************************) 

266 

267 
(*A surprising number of theorems contain only a few significant constants. 

268 
These include all induction rules, and other general theorems. Filtering 

269 
theorems in clause form reveals these complexities in the form of Skolem 

270 
functions. If we were instead to filter theorems in their natural form, 

271 
some other method of measuring theorem complexity would become necessary.*) 

272 

273 
fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0); 

274 

275 
(*The default seems best in practice. A constant function of one ignores 

276 
the constant frequencies.*) 

277 
val weight_fn = ref log_weight2; 

278 

279 

280 
(*Including equality in this list might be expected to stop rules like subset_antisym from 

281 
being chosen, but for some reason filtering works better with them listed. The 

282 
logical signs All, Ex, &, and > are omitted because any remaining occurrrences 

283 
must be within comprehensions.*) 

284 
val standard_consts = ["Trueprop","==>","all","==","op ","Not","op ="]; 

285 

286 

287 
(*** constants with types ***) 

288 

289 
(*An abstraction of Isabelle types*) 

290 
datatype const_typ = CTVar  CType of string * const_typ list 

291 

292 
(*Is the second type an instance of the first one?*) 

293 
fun match_type (CType(con1,args1)) (CType(con2,args2)) = 

294 
con1=con2 andalso match_types args1 args2 

295 
 match_type CTVar _ = true 

296 
 match_type _ CTVar = false 

297 
and match_types [] [] = true 

298 
 match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2; 

299 

300 
(*Is there a unifiable constant?*) 

301 
fun uni_mem gctab (c,c_typ) = 

302 
case Symtab.lookup gctab c of 

303 
NONE => false 

304 
 SOME ctyps_list => exists (match_types c_typ) ctyps_list; 

305 

306 
(*Maps a "real" type to a const_typ*) 

307 
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 

308 
 const_typ_of (TFree _) = CTVar 

309 
 const_typ_of (TVar _) = CTVar 

310 

311 
(*Pairs a constant with the list of its type instantiations (using const_typ)*) 

312 
fun const_with_typ thy (c,typ) = 

313 
let val tvars = Sign.const_typargs thy (c,typ) 

314 
in (c, map const_typ_of tvars) end 

315 
handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) 

316 

317 
(*Add a const/type pair to the table, but a [] entry means a standard connective, 

318 
which we ignore.*) 

319 
fun add_const_typ_table ((c,ctyps), tab) = 

320 
Symtab.map_default (c, [ctyps]) (fn [] => []  ctyps_list => insert (op =) ctyps ctyps_list) 

321 
tab; 

322 

323 
(*Free variables are included, as well as constants, to handle locales*) 

324 
fun add_term_consts_typs_rm thy (Const(c, typ), tab) = 

325 
add_const_typ_table (const_with_typ thy (c,typ), tab) 

326 
 add_term_consts_typs_rm thy (Free(c, typ), tab) = 

327 
add_const_typ_table (const_with_typ thy (c,typ), tab) 

328 
 add_term_consts_typs_rm thy (t $ u, tab) = 

329 
add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab)) 

330 
 add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab) 

331 
 add_term_consts_typs_rm thy (_, tab) = tab; 

332 

333 
(*The empty list here indicates that the constant is being ignored*) 

334 
fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; 

335 

336 
val null_const_tab : const_typ list list Symtab.table = 

337 
foldl add_standard_const Symtab.empty standard_consts; 

338 

339 
fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab; 

340 

341 
(*Inserts a dummy "constant" referring to the theory name, so that relevance 

342 
takes the given theory into account.*) 

343 
fun const_prop_of th = 

344 
if !theory_const then 

345 
let val name = Context.theory_name (theory_of_thm th) 

346 
val t = Const (name ^ ". 1", HOLogic.boolT) 

347 
in t $ prop_of th end 

348 
else prop_of th; 

349 

350 
(**** Constant / Type Frequencies ****) 

351 

352 
(*A twodimensional symbol table counts frequencies of constants. It's keyed first by 

353 
constant name and second by its list of type instantiations. For the latter, we need 

354 
a linear ordering on type const_typ list.*) 

355 

356 
local 

357 

358 
fun cons_nr CTVar = 0 

359 
 cons_nr (CType _) = 1; 

360 

361 
in 

362 

363 
fun const_typ_ord TU = 

364 
case TU of 

365 
(CType (a, Ts), CType (b, Us)) => 

366 
(case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us)  ord => ord) 

367 
 (T, U) => int_ord (cons_nr T, cons_nr U); 

368 

369 
end; 

370 

371 
structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord); 

372 

373 
fun count_axiom_consts thy ((thm,_), tab) = 

374 
let fun count_const (a, T, tab) = 

375 
let val (c, cts) = const_with_typ thy (a,T) 

376 
in (*Twodimensional table update. Constant maps to types maps to count.*) 

377 
Symtab.map_default (c, CTtab.empty) 

378 
(CTtab.map_default (cts,0) (fn n => n+1)) tab 

379 
end 

380 
fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab) 

381 
 count_term_consts (Free(a,T), tab) = count_const(a,T,tab) 

382 
 count_term_consts (t $ u, tab) = 

383 
count_term_consts (t, count_term_consts (u, tab)) 

384 
 count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) 

385 
 count_term_consts (_, tab) = tab 

386 
in count_term_consts (const_prop_of thm, tab) end; 

387 

388 

389 
(**** Actual Filtering Code ****) 

390 

391 
(*The frequency of a constant is the sum of those of all instances of its type.*) 

392 
fun const_frequency ctab (c, cts) = 

393 
let val pairs = CTtab.dest (the (Symtab.lookup ctab c)) 

394 
fun add ((cts',m), n) = if match_types cts cts' then m+n else n 

395 
in List.foldl add 0 pairs end; 

396 

397 
(*Add in a constant's weight, as determined by its frequency.*) 

398 
fun add_ct_weight ctab ((c,T), w) = 

399 
w + !weight_fn (real (const_frequency ctab (c,T))); 

400 

401 
(*Relevant constants are weighted according to frequency, 

402 
but irrelevant constants are simply counted. Otherwise, Skolem functions, 

403 
which are rare, would harm a clause's chances of being picked.*) 

404 
fun clause_weight ctab gctyps consts_typs = 

405 
let val rel = filter (uni_mem gctyps) consts_typs 

406 
val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel 

407 
in 

408 
rel_weight / (rel_weight + real (length consts_typs  length rel)) 

409 
end; 

410 

411 
(*Multiplies out to a list of pairs: 'a * 'b list > ('a * 'b) list > ('a * 'b) list*) 

412 
fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys; 

413 

414 
fun consts_typs_of_term thy t = 

415 
let val tab = add_term_consts_typs_rm thy (t, null_const_tab) 

416 
in Symtab.fold add_expand_pairs tab [] end; 

417 

418 
fun pair_consts_typs_axiom thy (thm,name) = 

419 
((thm,name), (consts_typs_of_term thy (const_prop_of thm))); 

420 

421 
exception ConstFree; 

422 
fun dest_ConstFree (Const aT) = aT 

423 
 dest_ConstFree (Free aT) = aT 

424 
 dest_ConstFree _ = raise ConstFree; 

425 

426 
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) 

427 
fun defines thy (thm,(name,n)) gctypes = 

428 
let val tm = prop_of thm 

429 
fun defs lhs rhs = 

430 
let val (rator,args) = strip_comb lhs 

431 
val ct = const_with_typ thy (dest_ConstFree rator) 

432 
in forall is_Var args andalso uni_mem gctypes ct andalso 

433 
Term.add_vars rhs [] subset Term.add_vars lhs [] 

434 
end 

435 
handle ConstFree => false 

436 
in 

437 
case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 

438 
defs lhs rhs andalso 

439 
(Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true) 

440 
 _ => false 

441 
end; 

442 

443 
type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); 

444 

445 
(*For a reverse sort, putting the largest values first.*) 

446 
fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1); 

447 

448 
(*Limit the number of new clauses, to prevent runaway acceptance.*) 

449 
fun take_best (newpairs : (annotd_cls*real) list) = 

450 
let val nnew = length newpairs 

451 
in 

452 
if nnew <= !max_new then (map #1 newpairs, []) 

453 
else 

454 
let val cls = sort compare_pairs newpairs 

455 
val accepted = List.take (cls, !max_new) 

456 
in 

457 
Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 

458 
", exceeds the limit of " ^ Int.toString (!max_new))); 

459 
Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); 

460 
Output.debug (fn () => "Actually passed: " ^ 

461 
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); 

462 

463 
(map #1 accepted, map #1 (List.drop (cls, !max_new))) 

464 
end 

465 
end; 

466 

467 
fun relevant_clauses thy ctab p rel_consts = 

468 
let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) 

469 
 relevant (newpairs,rejects) [] = 

470 
let val (newrels,more_rejects) = take_best newpairs 

471 
val new_consts = List.concat (map #2 newrels) 

472 
val rel_consts' = foldl add_const_typ_table rel_consts new_consts 

473 
val newp = p + (1.0p) / !convergence 

474 
in 

475 
Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels))); 

476 
(map #1 newrels) @ 

477 
(relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects)) 

478 
end 

479 
 relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = 

480 
let val weight = clause_weight ctab rel_consts consts_typs 

481 
in 

482 
if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts) 

483 
then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 

484 
" passes: " ^ Real.toString weight)); 

485 
relevant ((ax,weight)::newrels, rejects) axs) 

486 
else relevant (newrels, ax::rejects) axs 

487 
end 

488 
in Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); 

489 
relevant ([],[]) 

490 
end; 

491 

492 
fun relevance_filter thy axioms goals = 

493 
if !run_relevance_filter andalso !pass_mark >= 0.1 

494 
then 

495 
let val _ = Output.debug (fn () => "Start of relevance filtering"); 

496 
val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms 

497 
val goal_const_tab = get_goal_consts_typs thy goals 

498 
val _ = Output.debug (fn () => ("Initial constants: " ^ 

499 
space_implode ", " (Symtab.keys goal_const_tab))); 

500 
val rels = relevant_clauses thy const_tab (!pass_mark) 

501 
goal_const_tab (map (pair_consts_typs_axiom thy) axioms) 

502 
in 

503 
Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels))); 

504 
rels 

505 
end 

506 
else axioms; 

507 

508 
(***************************************************************) 

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

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

510 
(***************************************************************) 
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 
(*** white list and black list of lemmas ***) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

513 

24215  514 
(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data 
515 
or identified with ATPset (which however is too big currently)*) 

516 
val whitelist = [subsetI]; 

21588  517 

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

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

519 

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

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

521 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

522 
fun setinsert (x,s) = Symtab.update (x,()) s; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

523 

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

524 
(*Reject theorems with names like "List.filter.filter_list_def" or 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

525 
"Accessible_Part.acc.defs", as these are definitions arising from packages.*) 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

526 
fun is_package_def a = 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21790
diff
changeset

527 
let val names = NameSpace.explode a 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

528 
in 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

529 
length names > 2 andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

530 
not (hd names = "local") andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

531 
String.isSuffix "_def" a orelse String.isSuffix "_defs" a 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

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

533 

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

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

535 
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

536 

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

537 
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

538 
 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

539 
 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

540 
 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

541 
 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

542 
 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

543 

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

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

546 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

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

548 

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 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

551 
exception HASH_CLAUSE; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

552 

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

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

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

555 
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

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

557 

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

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

559 
(thm * (string * int)) tuples. The theorems are hashed into the table. *) 
21588  560 
fun make_unique xs = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

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

562 
in 
22130  563 
Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses")); 
21588  564 
app (ignore o Polyhash.peekInsert ht) xs; 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

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

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

567 

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

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

569 
boost an ATP's performance (for some reason)*) 
21588  570 
fun subtract_cls c_clauses ax_clauses = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

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

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

573 
in 
21588  574 
app (ignore o Polyhash.peekInsert ht) ax_clauses; 
575 
filter (not o known) c_clauses 

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

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

577 

21224  578 
fun all_valid_thms ctxt = 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

579 
let 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

580 
fun blacklisted s = !run_blacklist_filter andalso is_package_def s 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

581 

dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

582 
fun extern_valid space (name, ths) = 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

583 
let 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

584 
val is_valid = ProofContext.valid_thms ctxt; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

585 
val xname = NameSpace.extern space name; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

586 
in 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

587 
if blacklisted name then I 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

588 
else if is_valid (xname, ths) then cons (xname, ths) 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

589 
else if is_valid (name, ths) then cons (name, ths) 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

590 
else I 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

591 
end; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

592 
val thy = ProofContext.theory_of ctxt; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

593 
val all_thys = thy :: Theory.ancestors_of thy; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

594 

dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

595 
fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab []; 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

596 
in 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

597 
maps (dest_valid o PureThy.theorems_of) all_thys @ 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

598 
fold (extern_valid (#1 (ProofContext.theorems_of ctxt))) 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

599 
(FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])) [] 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

600 
end; 
21224  601 

21588  602 
fun multi_name a (th, (n,pairs)) = 
21224  603 
(n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) 
604 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

605 
fun add_single_names ((a, []), pairs) = pairs 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

606 
 add_single_names ((a, [th]), pairs) = (a,th)::pairs 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

607 
 add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths); 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

608 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

609 
val multi_base_blacklist = 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

610 
["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"]; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

611 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

612 
(*Ignore blacklisted basenames*) 
21588  613 
fun add_multi_names ((a, ths), pairs) = 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

614 
if (Sign.base_name a) mem_string multi_base_blacklist then pairs 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

615 
else add_single_names ((a, ths), pairs); 
21224  616 

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

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

618 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

619 
(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*) 
21588  620 
fun name_thm_pairs ctxt = 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

621 
let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt) 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

622 
val ht = mk_clause_table 900 (*ht for blacklisted theorems*) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

623 
fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

624 
in 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

625 
app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt); 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

626 
filter (not o blacklisted o #2) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

627 
(foldl add_single_names (foldl add_multi_names [] mults) singles) 
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24215
diff
changeset

628 
end; 
21224  629 

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

631 
 check_named (_,th) = true; 

19894  632 

22193  633 
fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th); 
634 

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

635 
(* get lemmas from claset, simpset, atpset and extra supplied rules *) 
21588  636 
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894  637 
let val included_thms = 
21588  638 
if !include_all 
639 
then (tap (fn ths => Output.debug 

22130  640 
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) 
21588  641 
(name_thm_pairs ctxt)) 
642 
else 

643 
let val claset_thms = 

644 
if !include_claset then ResAxioms.claset_rules_of ctxt 

645 
else [] 

646 
val simpset_thms = 

647 
if !include_simpset then ResAxioms.simpset_rules_of ctxt 

648 
else [] 

649 
val atpset_thms = 

650 
if !include_atpset then ResAxioms.atpset_rules_of ctxt 

651 
else [] 

22193  652 
val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) 
21588  653 
in claset_thms @ simpset_thms @ atpset_thms end 
654 
val user_rules = filter check_named 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

655 
(map ResAxioms.pairname 
24215  656 
(if null user_thms then whitelist else user_thms)) 
19894  657 
in 
21224  658 
(filter check_named included_thms, user_rules) 
19894  659 
end; 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

660 

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

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

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

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

664 

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

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

666 

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

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

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

669 

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

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

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

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

673 

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

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

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

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

677 

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

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

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

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

681 

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

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

683 

21397
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

684 
(*Type constructors used to instantiate overloaded constants are the only ones needed.*) 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

685 
fun add_type_consts_in_term thy = 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

686 
let val const_typargs = Sign.const_typargs thy 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

687 
fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

688 
 add_tcs (Abs (_, T, u)) x = add_tcs u x 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

689 
 add_tcs (t $ u) x = add_tcs t (add_tcs u x) 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

690 
 add_tcs _ x = x 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

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

692 

21397
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

693 
fun type_consts_of_terms thy ts = 
2134b81a0b37
Now includes only types used to instantiate overloaded constants in arity clauses
paulson
parents:
21373
diff
changeset

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

695 

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

696 

19194  697 
(***************************************************************) 
698 
(* ATP invocation methods setup *) 

699 
(***************************************************************) 

700 

21588  701 
fun cnf_hyps_thms ctxt = 
20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20131
diff
changeset

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

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

705 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
19194  706 
datatype mode = Auto  Fol  Hol; 
707 

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

708 
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

709 

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

710 
(*Ensures that no higherorder theorems "leak out"*) 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

711 
fun restrict_to_logic thy logic cls = 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

712 
if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls 
21588  713 
else cls; 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

714 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

715 
(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

716 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

717 
(** Too general means, positive equality literal with a variable X as one operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

718 
when X does not occur properly in the other operand. This rules out clearly 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

719 
inconsistent clauses such as V=aV=b, though it by no means guarantees soundness. **) 
21588  720 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

721 
fun occurs ix = 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

722 
let fun occ(Var (jx,_)) = (ix=jx) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

723 
 occ(t1$t2) = occ t1 orelse occ t2 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

724 
 occ(Abs(_,_,t)) = occ t 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

725 
 occ _ = false 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

726 
in occ end; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

727 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

728 
fun is_recordtype T = not (null (RecordPackage.dest_recTs T)); 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

729 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

730 
(*Unwanted equalities include 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

731 
(1) those between a variable that does not properly occur in the second operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

732 
(2) those between a variable and a record, since these seem to be prolific "cases" thms 
21588  733 
*) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

734 
fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

735 
 too_general_eqterms _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

736 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

737 
fun too_general_equality (Const ("op =", _) $ x $ y) = 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

738 
too_general_eqterms (x,y) orelse too_general_eqterms(y,x) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

739 
 too_general_equality _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

740 

7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

741 
(* tautologous? *) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

742 
fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

743 
 is_taut _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

744 

21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

745 
(*True if the term contains a variable whose (atomic) type is in the given list.*) 
21588  746 
fun has_typed_var tycons = 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

747 
let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

748 
 var_tycon _ = false 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

749 
in exists var_tycon o term_vars end; 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

750 

22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

751 
(*Clauses are forbidden to contain variables of these types. The typical reason is that 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

752 
they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=(). 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

753 
The resulting clause will have no type constraint, yielding false proofs. Even "bool" 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

754 
leads to many unsound proofs, though (obviously) only for higherorder problems.*) 
24215  755 
val unwanted_types = ["Product_Type.unit","bool"]; 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

756 

21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

757 
fun unwanted t = 
24215  758 
is_taut t orelse has_typed_var unwanted_types t orelse 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

759 
forall too_general_equality (dest_disj t); 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

760 

21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

761 
(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

762 
likely to lead to unsound proofs.*) 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

763 
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls; 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

764 

24320  765 
fun tptp_writer thy logic = ResHolClause.tptp_write_file thy (logic=FOL); 
19445
da75577642a9
tidying; ATP options including CASC mode for Vampire
paulson
parents:
19442
diff
changeset

766 

24320  767 
fun dfg_writer thy logic = ResHolClause.dfg_write_file thy (logic=FOL); 
19194  768 

20022  769 
(*Called by the oraclebased methods declared in res_atp_methods.ML*) 
19722  770 
fun write_subgoal_file dfg mode ctxt conjectures user_thms n = 
24300  771 
let val conj_cls = Meson.make_clauses conjectures 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

772 
> ResAxioms.assume_abstract_list "subgoal" > Meson.finish_cnf 
21588  773 
val hyp_cls = cnf_hyps_thms ctxt 
774 
val goal_cls = conj_cls@hyp_cls 

775 
val goal_tms = map prop_of goal_cls 

22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

776 
val thy = ProofContext.theory_of ctxt 
21588  777 
val logic = case mode of 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

778 
Auto => problem_logic_goals [goal_tms] 
21588  779 
 Fol => FOL 
780 
 Hol => HOL 

781 
val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms 

22865  782 
val cla_simp_atp_clauses = included_thms 
21588  783 
> ResAxioms.cnf_rules_pairs > make_unique 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

784 
> restrict_to_logic thy logic 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

785 
> remove_unwanted_clauses 
21588  786 
val user_cls = ResAxioms.cnf_rules_pairs user_rules 
24287  787 
val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms) 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

788 
val subs = tfree_classes_of_terms goal_tms 
21373
18f519614978
Arity clauses are now produced only for types and type classes actually used.
paulson
parents:
21311
diff
changeset

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

790 
val supers = tvar_classes_of_terms axtms 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

791 
and tycons = type_consts_of_terms thy (goal_tms@axtms) 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

792 
(*TFrees in conjecture clauses; TVars in axiom clauses*) 
22645  793 
val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers 
794 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 

21588  795 
val writer = if dfg then dfg_writer else tptp_writer 
796 
and file = atp_input_file() 

797 
and user_lemmas_names = map #1 user_rules 

19194  798 
in 
24320  799 
writer thy logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names; 
22130  800 
Output.debug (fn () => "Writing to " ^ file); 
21588  801 
file 
19194  802 
end; 
803 

804 

805 
(**** remove tmp files ****) 

21588  806 
fun cond_rm_tmp file = 
22130  807 
if !Output.debugging orelse !destdir <> "" 
808 
then Output.debug (fn () => "ATP input kept...") 

20870  809 
else OS.FileSys.remove file; 
19194  810 

811 

812 
(***************************************************************) 

813 
(* automatic ATP invocation *) 

814 
(***************************************************************) 

815 

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

818 
let 
17422  819 
fun make_atp_list [] n = [] 
17717  820 
 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

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

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

824 
in 
22130  825 
Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile); 
17764  826 
(*options are separated by Watcher.setting_sep, currently #"%"*) 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

827 
case !prover of 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

828 
Recon.SPASS => 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

829 
let val spass = helper_path "SPASS_HOME" "SPASS" 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

830 
val sopts = 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

831 
"Auto%SOS=1%PGiven=0%PProblem=0%Splits=0%FullRed=0%DocProof%TimeLimit=" ^ time 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

832 
in 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

833 
("spass", spass, sopts, probfile) :: make_atp_list xs (n+1) 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

834 
end 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

835 
 Recon.Vampire => 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

836 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

837 
val vopts = "mode casc%t " ^ time (*what about m 100000?*) 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

838 
in 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

839 
("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1) 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

840 
end 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

841 
 Recon.E => 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

842 
let val eproof = helper_path "E_HOME" "eproof" 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

843 
val eopts = "tstpin%tstpout%l5%xAutoDev%tAutoDev%silent%cpulimit=" ^ time 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

844 
in 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

845 
("E", eproof, eopts, probfile) :: make_atp_list xs (n+1) 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

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

847 
end 
15452  848 

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

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

851 
Watcher.callResProvers(childout,atp_list); 
22130  852 
Output.debug (fn () => "Sent commands to watcher!") 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

853 
end 
21588  854 

22193  855 
(*For debugging the generated set of theorem names*) 
21888  856 
fun trace_vector fname = 
22193  857 
let val path = File.explode_platform_path (fname ^ "_thm_names") 
21888  858 
in Vector.app (File.append path o (fn s => s ^ "\n")) end; 
16357  859 

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

863 
subgoals, each involving &&.*) 

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

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

868 
fun get_neg_subgoals [] _ = [] 
22865  869 
 get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21980
diff
changeset

870 
get_neg_subgoals gls (n+1) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

871 
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

872 
val logic = case !linkup_logic_mode of 
23387  873 
Auto => problem_logic_goals (map (map prop_of) goal_cls) 
21588  874 
 Fol => FOL 
875 
 Hol => HOL 

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

876 
val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

877 
val included_cls = included_thms > ResAxioms.cnf_rules_pairs > make_unique 
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

878 
> restrict_to_logic thy logic 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

879 
> remove_unwanted_clauses 
22130  880 
val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls)) 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

881 
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

882 
(*clauses relevant to goal gl*) 
24287  883 
val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls 
22130  884 
val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls))) 
21070  885 
axcls_list 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24320
diff
changeset

886 
val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

887 
fun write_all [] [] _ = [] 
21588  888 
 write_all (ccls::ccls_list) (axcls::axcls_list) k = 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

889 
let val fname = probfile k 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

890 
val _ = Output.debug (fn () => "About to write file " ^ fname) 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

891 
val axcls = make_unique axcls 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

892 
val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)") 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

893 
val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

894 
val ccls = subtract_cls ccls axcls 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

895 
val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)") 
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

896 
val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

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

898 
and axtms = map (prop_of o #1) axcls 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

899 
val subs = tfree_classes_of_terms ccltms 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

900 
and supers = tvar_classes_of_terms axtms 
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

901 
and tycons = type_consts_of_terms thy (ccltms@axtms) 
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

902 
(*TFrees in conjecture clauses; TVars in axiom clauses*) 
22645  903 
val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers 
904 
val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses)) 

905 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 

22130  906 
val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses)) 
24320  907 
val clnames = writer thy logic ccls fname (axcls,classrel_clauses,arity_clauses) [] 
21888  908 
val thm_names = Vector.fromList clnames 
22193  909 
val _ = if !Output.debugging then trace_vector fname thm_names else () 
20870  910 
in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end 
911 
val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1) 

19194  912 
in 
20870  913 
(filenames, thm_names_list) 
19194  914 
end; 
15644  915 

21588  916 
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
17775  917 
Posix.Process.pid * string list) option); 
918 

919 
fun kill_last_watcher () = 

21588  920 
(case !last_watcher_pid of 
17775  921 
NONE => () 
21588  922 
 SOME (_, _, pid, files) => 
22130  923 
(Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid); 
21588  924 
Watcher.killWatcher pid; 
925 
ignore (map (try cond_rm_tmp) files))) 

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

927 

21980
d22f7e3c5ad9
xsymbol is no longer switched off in the ATP linkup
paulson
parents:
21900
diff
changeset

928 
(*writes out the current problems and calls ATPs*) 
d22f7e3c5ad9
xsymbol is no longer switched off in the ATP linkup
paulson
parents:
21900
diff
changeset

929 
fun isar_atp (ctxt, th) = 
17717  930 
if Thm.no_prems th then () 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

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

932 
let 
17775  933 
val _ = kill_last_watcher() 
20870  934 
val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th) 
22012
adf68479ae1b
Proof.context now sent to watcher and used in type inference step of proof reconstruction
paulson
parents:
21999
diff
changeset

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

937 
last_watcher_pid := SOME (childin, childout, pid, files); 
22130  938 
Output.debug (fn () => "problem files: " ^ space_implode ", " files); 
939 
Output.debug (fn () => "pid: " ^ string_of_pid pid); 

22578  940 
watcher_call_provers (Thm.theory_of_thm th) (Thm.prems_of th) (childin, childout, pid) 
20954  941 
end; 
942 

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

21588  944 
fun callatp () = 
20954  945 
let val th = topthm() 
946 
val ctxt = ProofContext.init (theory_of_thm th) 

21980
d22f7e3c5ad9
xsymbol is no longer switched off in the ATP linkup
paulson
parents:
21900
diff
changeset

947 
in isar_atp (ctxt, th) end; 
15608  948 

21588  949 
val isar_atp_writeonly = setmp print_mode [] 
17717  950 
(fn (ctxt,th) => 
951 
if Thm.no_prems th then () 

21588  952 
else 
953 
let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 

954 
else prob_pathname 

20022  955 
in ignore (write_problem_files probfile (ctxt,th)) end); 
15452  956 

16357  957 

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

959 

22865  960 
fun sledgehammer state = 
961 
let 

962 
val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state); 

963 
val thy = ProofContext.theory_of ctxt; 

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

964 
in 
22130  965 
Output.debug (fn () => "subgoals in isar_atp:\n" ^ 
21588  966 
Pretty.string_of (ProofContext.pretty_term ctxt 
967 
(Logic.mk_conjunction_list (Thm.prems_of goal)))); 

22130  968 
Output.debug (fn () => "current theory: " ^ Context.theory_name thy); 
21132  969 
if !time_limit > 0 then isar_atp (ctxt, goal) 
22865  970 
else (warning ("Writing problem file only: " ^ !problem_name); 
22193  971 
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

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

973 

22865  974 
val _ = OuterSyntax.add_parsers 
975 
[OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag 

976 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))]; 

17091  977 

15347  978 
end; 