author  wenzelm 
Fri, 03 Oct 2008 16:37:09 +0200  
changeset 28477  9339d4dcec8b 
parent 28065  3899dff63cd7 
child 29267  8615b4f54047 
permissions  rwrr 
19194  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA 
15608  2 
ID: $Id$ 
3 
Copyright 2004 University of Cambridge 

15347  4 
*) 
15452  5 

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

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

7 
sig 
19194  8 
datatype mode = Auto  Fol  Hol 
22989  9 
val tvar_classes_of_terms : term list > string list 
10 
val tfree_classes_of_terms : term list > string list 

11 
val type_consts_of_terms : theory > term list > string list 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

12 
val write_problem_files : (theory > bool > Thm.thm list > string > 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

13 
(thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list * ResClause.classrelClause list * 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

14 
ResClause.arityClause list > string list > ResHolClause.axiom_name list) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

15 
> int > bool 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

16 
> (int > Path.T) > Proof.context * thm list * thm 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

17 
> string list * ResHolClause.axiom_name Vector.vector list 
15347  18 
end; 
19 

22865  20 
structure ResAtp: RES_ATP = 
15347  21 
struct 
22 

21070  23 

19194  24 
(********************************************************************) 
25 
(* some settings for both background automatic ATP calling procedure*) 

26 
(* and also explicit ATP invocation methods *) 

27 
(********************************************************************) 

28 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

29 
(*Translation mode can be autodetected, or forced to be firstorder or higherorder*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

30 
datatype mode = Auto  Fol  Hol; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

31 

9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

32 
val linkup_logic_mode = Auto; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

33 

19194  34 
(*** background linkup ***) 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

35 
val run_blacklist_filter = true; 
21224  36 

24287  37 
(*** relevance filter parameters ***) 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

38 
val run_relevance_filter = true; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

39 
val pass_mark = 0.5; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

40 
val convergence = 3.2; (*Higher numbers allow longer inference chains*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

41 
val follow_defs = false; (*Follow definitions. Makes problems bigger.*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

42 
val include_all = true; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

43 
val include_simpset = false; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

44 
val include_claset = false; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

45 
val include_atpset = true; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

46 

9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

47 
(***************************************************************) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

48 
(* Relevance Filtering *) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

49 
(***************************************************************) 
19194  50 

24958  51 
fun strip_Trueprop (Const("Trueprop",_) $ t) = t 
52 
 strip_Trueprop t = t; 

19194  53 

24287  54 
(*A surprising number of theorems contain only a few significant constants. 
55 
These include all induction rules, and other general theorems. Filtering 

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

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

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

59 

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

61 

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

63 
the constant frequencies.*) 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

64 
val weight_fn = log_weight2; 
24287  65 

66 

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

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

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

70 
must be within comprehensions.*) 

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

72 

73 

74 
(*** constants with types ***) 

75 

76 
(*An abstraction of Isabelle types*) 

77 
datatype const_typ = CTVar  CType of string * const_typ list 

78 

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

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

81 
con1=con2 andalso match_types args1 args2 

82 
 match_type CTVar _ = true 

83 
 match_type _ CTVar = false 

84 
and match_types [] [] = true 

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

86 

87 
(*Is there a unifiable constant?*) 

88 
fun uni_mem gctab (c,c_typ) = 

89 
case Symtab.lookup gctab c of 

90 
NONE => false 

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

92 

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

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

95 
 const_typ_of (TFree _) = CTVar 

96 
 const_typ_of (TVar _) = CTVar 

97 

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

99 
fun const_with_typ thy (c,typ) = 

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

101 
in (c, map const_typ_of tvars) end 

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

103 

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

105 
which we ignore.*) 

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

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

108 
tab; 

109 

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

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

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

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

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

115 
 add_term_consts_typs_rm thy (t $ u, tab) = 

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

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

118 
 add_term_consts_typs_rm thy (_, tab) = tab; 

119 

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

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

122 

123 
val null_const_tab : const_typ list list Symtab.table = 

124 
foldl add_standard_const Symtab.empty standard_consts; 

125 

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

127 

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

129 
takes the given theory into account.*) 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

130 
fun const_prop_of theory_const th = 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

131 
if theory_const then 
24287  132 
let val name = Context.theory_name (theory_of_thm th) 
133 
val t = Const (name ^ ". 1", HOLogic.boolT) 

134 
in t $ prop_of th end 

135 
else prop_of th; 

136 

137 
(**** Constant / Type Frequencies ****) 

138 

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

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

141 
a linear ordering on type const_typ list.*) 

142 

143 
local 

144 

145 
fun cons_nr CTVar = 0 

146 
 cons_nr (CType _) = 1; 

147 

148 
in 

149 

150 
fun const_typ_ord TU = 

151 
case TU of 

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

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

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

155 

156 
end; 

157 

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

159 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

160 
fun count_axiom_consts theory_const thy ((thm,_), tab) = 
24287  161 
let fun count_const (a, T, tab) = 
162 
let val (c, cts) = const_with_typ thy (a,T) 

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

164 
Symtab.map_default (c, CTtab.empty) 

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

166 
end 

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

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

169 
 count_term_consts (t $ u, tab) = 

170 
count_term_consts (t, count_term_consts (u, tab)) 

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

172 
 count_term_consts (_, tab) = tab 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

173 
in count_term_consts (const_prop_of theory_const thm, tab) end; 
24287  174 

175 

176 
(**** Actual Filtering Code ****) 

177 

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

179 
fun const_frequency ctab (c, cts) = 

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

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

182 
in List.foldl add 0 pairs end; 

183 

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

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

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

186 
w + weight_fn (real (const_frequency ctab (c,T))); 
24287  187 

188 
(*Relevant constants are weighted according to frequency, 

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

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

191 
fun clause_weight ctab gctyps consts_typs = 

192 
let val rel = filter (uni_mem gctyps) consts_typs 

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

194 
in 

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

196 
end; 

197 

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

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

200 

201 
fun consts_typs_of_term thy t = 

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

203 
in Symtab.fold add_expand_pairs tab [] end; 

204 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

205 
fun pair_consts_typs_axiom theory_const thy (thm,name) = 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

206 
((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm))); 
24287  207 

208 
exception ConstFree; 

209 
fun dest_ConstFree (Const aT) = aT 

210 
 dest_ConstFree (Free aT) = aT 

211 
 dest_ConstFree _ = raise ConstFree; 

212 

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

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

215 
let val tm = prop_of thm 

216 
fun defs lhs rhs = 

217 
let val (rator,args) = strip_comb lhs 

218 
val ct = const_with_typ thy (dest_ConstFree rator) 

219 
in forall is_Var args andalso uni_mem gctypes ct andalso 

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

221 
end 

222 
handle ConstFree => false 

223 
in 

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

225 
defs lhs rhs andalso 

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

227 
 _ => false 

228 
end; 

229 

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

231 

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

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

234 

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

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

236 
fun take_best max_new (newpairs : (annotd_cls*real) list) = 
24287  237 
let val nnew = length newpairs 
238 
in 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

239 
if nnew <= max_new then (map #1 newpairs, []) 
24287  240 
else 
241 
let val cls = sort compare_pairs newpairs 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

242 
val accepted = List.take (cls, max_new) 
24287  243 
in 
244 
Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

245 
", exceeds the limit of " ^ Int.toString (max_new))); 
24287  246 
Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); 
247 
Output.debug (fn () => "Actually passed: " ^ 

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

249 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

250 
(map #1 accepted, map #1 (List.drop (cls, max_new))) 
24287  251 
end 
252 
end; 

253 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

254 
fun relevant_clauses max_new thy ctab p rel_consts = 
24287  255 
let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) 
256 
 relevant (newpairs,rejects) [] = 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

257 
let val (newrels,more_rejects) = take_best max_new newpairs 
24287  258 
val new_consts = List.concat (map #2 newrels) 
259 
val rel_consts' = foldl add_const_typ_table rel_consts new_consts 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

260 
val newp = p + (1.0p) / convergence 
24287  261 
in 
262 
Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels))); 

263 
(map #1 newrels) @ 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

264 
(relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects)) 
24287  265 
end 
266 
 relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = 

267 
let val weight = clause_weight ctab rel_consts consts_typs 

268 
in 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

269 
if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts) 
24287  270 
then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 
271 
" passes: " ^ Real.toString weight)); 

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

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

274 
end 

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

276 
relevant ([],[]) 

277 
end; 

278 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

279 
fun relevance_filter max_new theory_const thy axioms goals = 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

280 
if run_relevance_filter andalso pass_mark >= 0.1 
24287  281 
then 
282 
let val _ = Output.debug (fn () => "Start of relevance filtering"); 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

283 
val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms 
24287  284 
val goal_const_tab = get_goal_consts_typs thy goals 
285 
val _ = Output.debug (fn () => ("Initial constants: " ^ 

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

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

287 
val rels = relevant_clauses max_new thy const_tab (pass_mark) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

288 
goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms) 
24287  289 
in 
290 
Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels))); 

291 
rels 

292 
end 

293 
else axioms; 

294 

295 
(***************************************************************) 

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

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

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

298 

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

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

300 

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

303 
val whitelist = [subsetI]; 

21588  304 

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

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

306 

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

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

308 

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

309 
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

310 

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

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

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

313 
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

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

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

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

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

318 
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

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

320 

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

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

322 
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

323 

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

324 
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

325 
 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

326 
 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

327 
 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

328 
 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

329 
 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

330 

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

333 

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

335 

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

336 
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

337 

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

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

339 

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

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

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

342 
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

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

344 

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

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

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

348 
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

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

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

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

354 

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

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

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

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

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

360 
in 
21588  361 
app (ignore o Polyhash.peekInsert ht) ax_clauses; 
362 
filter (not o known) c_clauses 

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

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

364 

26675  365 
fun valid_facts facts = 
26691
520c99e0b9a0
valid_facts: more elementary version using Facts.fold_static;
wenzelm
parents:
26675
diff
changeset

366 
Facts.fold_static (fn (name, ths) => 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

367 
if run_blacklist_filter andalso is_package_def name then I 
26691
520c99e0b9a0
valid_facts: more elementary version using Facts.fold_static;
wenzelm
parents:
26675
diff
changeset

368 
else 
520c99e0b9a0
valid_facts: more elementary version using Facts.fold_static;
wenzelm
parents:
26675
diff
changeset

369 
let val xname = Facts.extern facts name in 
520c99e0b9a0
valid_facts: more elementary version using Facts.fold_static;
wenzelm
parents:
26675
diff
changeset

370 
if NameSpace.is_hidden xname then I 
520c99e0b9a0
valid_facts: more elementary version using Facts.fold_static;
wenzelm
parents:
26675
diff
changeset

371 
else cons (xname, filter_out ResAxioms.bad_for_atp ths) 
520c99e0b9a0
valid_facts: more elementary version using Facts.fold_static;
wenzelm
parents:
26675
diff
changeset

372 
end) facts []; 
26675  373 

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

375 
let 
26675  376 
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); 
26278  377 
val local_facts = ProofContext.facts_of ctxt; 
26675  378 
in valid_facts global_facts @ valid_facts local_facts end; 
21224  379 

21588  380 
fun multi_name a (th, (n,pairs)) = 
21224  381 
(n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) 
382 

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

383 
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

384 
 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

385 
 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

386 

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

387 
(*Ignore blacklisted basenames*) 
21588  388 
fun add_multi_names ((a, ths), pairs) = 
24854  389 
if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

390 
else add_single_names ((a, ths), pairs); 
21224  391 

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

392 
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

393 

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

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

396 
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

397 
val ht = mk_clause_table 900 (*ht for blacklisted theorems*) 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

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

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

400 
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

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

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

403 
end; 
21224  404 

26928  405 
fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false) 
21224  406 
 check_named (_,th) = true; 
19894  407 

26928  408 
fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th); 
22193  409 

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

410 
(* get lemmas from claset, simpset, atpset and extra supplied rules *) 
21588  411 
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894  412 
let val included_thms = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

413 
if include_all 
21588  414 
then (tap (fn ths => Output.debug 
22130  415 
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) 
21588  416 
(name_thm_pairs ctxt)) 
417 
else 

418 
let val claset_thms = 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

419 
if include_claset then ResAxioms.claset_rules_of ctxt 
21588  420 
else [] 
421 
val simpset_thms = 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

422 
if include_simpset then ResAxioms.simpset_rules_of ctxt 
21588  423 
else [] 
424 
val atpset_thms = 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

425 
if include_atpset then ResAxioms.atpset_rules_of ctxt 
21588  426 
else [] 
22193  427 
val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) 
21588  428 
in claset_thms @ simpset_thms @ atpset_thms end 
429 
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

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

435 

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

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

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

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

439 

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

440 
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

441 

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

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

443 
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

444 

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

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

446 
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

447 
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

448 

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

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

450 
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

451 
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

452 

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

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

454 
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

455 
 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

456 

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

457 
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

458 

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

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

460 
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

461 
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

462 
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

463 
 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

464 
 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

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

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

467 

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

468 
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

469 
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

470 

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

471 

19194  472 
(***************************************************************) 
473 
(* ATP invocation methods setup *) 

474 
(***************************************************************) 

475 

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

476 
(*Ensures that no higherorder theorems "leak out"*) 
24958  477 
fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls 
478 
 restrict_to_logic thy false cls = cls; 

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

479 

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

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

481 

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

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

483 
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

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

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

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

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

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

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

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

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

492 

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

493 
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

494 

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

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

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

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

499 
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

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

501 

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

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

503 
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

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

505 

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

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

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

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

509 

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

510 
(*True if the term contains a variable whose (atomic) type is in the given list.*) 
21588  511 
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

512 
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

513 
 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

514 
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

515 

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

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

517 
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

518 
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

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

521 

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

522 
fun unwanted t = 
24958  523 
is_taut t orelse has_typed_var unwanted_types t orelse 
524 
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)); 

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

525 

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

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

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

528 
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

529 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

530 
(* TODO: problem file for *one* subgoal would be sufficient *) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

531 
(*Write out problem files for each subgoal. 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

532 
Argument probfile generates filenames from subgoalnumber 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

533 
Argument writer is either a tptp_write_file or dfg_write_file from ResHolClause 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

534 
Arguments max_new and theory_const are booleans controlling relevance_filter 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

535 
(necessary for different provers) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

536 
*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

537 
fun write_problem_files writer max_new theory_const probfile (ctxt, chain_ths, th) = 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

538 
let val goals = Thm.prems_of th 
17717  539 
val thy = ProofContext.theory_of ctxt 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20446
diff
changeset

540 
fun get_neg_subgoals [] _ = [] 
22865  541 
 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

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

543 
val goal_cls = get_neg_subgoals goals 1 
25243  544 
handle THM ("assume: variables", _, _) => 
545 
error "Sledgehammer: Goal contains type variables (TVars)" 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

546 
val isFO = case linkup_logic_mode of 
24958  547 
Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls)) 
548 
 Fol => true 

549 
 Hol => false 

24546  550 
val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths 
27178
c8ddb3000743
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
26928
diff
changeset

551 
val included_cls = included_thms > ResAxioms.cnf_rules_pairs thy > make_unique 
24958  552 
> restrict_to_logic thy isFO 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

553 
> remove_unwanted_clauses 
27178
c8ddb3000743
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
26928
diff
changeset

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

555 
(*clauses relevant to goal gl*) 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

556 
val axcls_list = map (fn ngcls => white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of ngcls)) goal_cls 
20526
756c4f1fd04c
Extended the blacklist with higherorder theorems. Restructured. Added checks to
paulson
parents:
20457
diff
changeset

557 
fun write_all [] [] _ = [] 
21588  558 
 write_all (ccls::ccls_list) (axcls::axcls_list) k = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

559 
let val fname = File.platform_path (probfile k) 
20868
724ab9896068
Improved detection of identical clauses, also in the conjecture
paulson
parents:
20854
diff
changeset

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

562 
val ccls = subtract_cls ccls axcls 
26928  563 
val _ = app (fn th => Output.debug (fn _ => Display.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

564 
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

565 
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

566 
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

567 
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

568 
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

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

24958  572 
val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) [] 
21888  573 
val thm_names = Vector.fromList clnames 
20870  574 
in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end 
575 
val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1) 

19194  576 
in 
20870  577 
(filenames, thm_names_list) 
19194  578 
end; 
15644  579 

15347  580 
end; 