1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
3 Author: Jasmin Blanchette, TU Muenchen
5 Sledgehammer's relevance filter.
8 signature SLEDGEHAMMER_FILTER =
10 type stature = ATP_Problem_Generate.stature
12 type relevance_fudge =
13 {local_const_multiplier : real,
14 worse_irrel_freq : real,
15 higher_order_irrel_weight : real,
16 abs_rel_weight : real,
17 abs_irrel_weight : real,
18 skolem_irrel_weight : real,
19 theory_const_rel_weight : real,
20 theory_const_irrel_weight : real,
21 chained_const_irrel_weight : real,
29 max_imperfect_exp : real,
30 threshold_divisor : real,
31 ridiculous_threshold : real}
33 type relevance_override =
34 {add : (Facts.ref * Attrib.src list) list,
35 del : (Facts.ref * Attrib.src list) list,
38 val trace : bool Config.T
39 val ignore_no_atp : bool Config.T
40 val instantiate_inducts : bool Config.T
41 val no_relevance_override : relevance_override
42 val const_names_in_fact :
43 theory -> (string * typ -> term list -> bool * term list) -> term
46 Proof.context -> unit Symtab.table -> thm list
47 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
49 Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
50 -> (((unit -> string) * stature) * thm) list
51 val nearly_all_facts :
52 Proof.context -> bool -> relevance_override -> thm list -> term list -> term
53 -> (((unit -> string) * stature) * thm) list
55 Proof.context -> real * real -> int
56 -> (string * typ -> term list -> bool * term list) -> relevance_fudge
57 -> relevance_override -> thm list -> term list -> term
58 -> (((unit -> string) * stature) * thm) list
59 -> ((string * stature) * thm) list
62 structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
65 open ATP_Problem_Generate
67 open Sledgehammer_Util
70 Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
71 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
73 (* experimental features *)
75 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
76 val instantiate_inducts =
77 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
79 type relevance_fudge =
80 {local_const_multiplier : real,
81 worse_irrel_freq : real,
82 higher_order_irrel_weight : real,
83 abs_rel_weight : real,
84 abs_irrel_weight : real,
85 skolem_irrel_weight : real,
86 theory_const_rel_weight : real,
87 theory_const_irrel_weight : real,
88 chained_const_irrel_weight : real,
96 max_imperfect_exp : real,
97 threshold_divisor : real,
98 ridiculous_threshold : real}
100 type relevance_override =
101 {add : (Facts.ref * Attrib.src list) list,
102 del : (Facts.ref * Attrib.src list) list,
105 val no_relevance_override = {add = [], del = [], only = false}
107 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
108 val abs_name = sledgehammer_prefix ^ "abs"
109 val skolem_prefix = sledgehammer_prefix ^ "sko"
110 val theory_const_suffix = Long_Name.separator ^ " 1"
112 fun needs_quoting reserved s =
113 Symtab.defined reserved s orelse
114 exists (not o Lexicon.is_identifier) (Long_Name.explode s)
116 fun make_name reserved multi j name =
117 (name |> needs_quoting reserved name ? quote) ^
118 (if multi then "(" ^ string_of_int j ^ ")" else "")
120 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
121 | explode_interval max (Facts.From i) = i upto i + max - 1
122 | explode_interval _ (Facts.Single i) = [i]
125 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
126 fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
128 val ths = Attrib.eval_thms ctxt [xthm]
130 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
134 Facts.Fact s => backquote s ^ bracket
135 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
136 | Facts.Named ((name, _), NONE) =>
137 make_name reserved (length ths > 1) (j + 1) name ^ bracket
138 | Facts.Named ((name, _), SOME intervals) =>
139 make_name reserved true
140 (nth (maps (explode_interval (length ths)) intervals) j) name ^
144 |-> fold (fn th => fn (j, rest) =>
147 (if member Thm.eq_thm_prop chained_ths th then Chained
148 else Local (* just in case *), General)), th) :: rest))
152 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
153 they are displayed as "M" and we want to avoid clashes with these. But
154 sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
155 prefixes of all free variables. In the worse case scenario, where the fact
156 won't be resolved correctly, the user can fix it manually, e.g., by naming
157 the fact in question. Ideally we would need nothing of it, but backticks
158 simply don't work with schematic variables. *)
159 fun all_prefixes_of s =
160 map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
162 (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
163 |> fold (fn ((s, i), T) => fn (t', taken) =>
164 let val s' = singleton (Name.variant_list taken) s in
165 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
166 else Logic.all_const) T
167 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
170 (Term.add_vars t [] |> sort_wrt (fst o fst))
173 fun string_for_term ctxt t =
174 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
175 (print_mode_value ())) (Syntax.string_of_term ctxt) t
176 |> String.translate (fn c => if Char.isPrint c then str c else "")
179 (** Structural induction rules **)
181 fun struct_induct_rule_on th =
182 case Logic.strip_horn (prop_of th) of
183 (prems, @{const Trueprop}
184 $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
185 if not (is_TVar ind_T) andalso length prems > 1 andalso
186 exists (exists_subterm (curry (op aconv) p)) prems andalso
187 not (exists (exists_subterm (curry (op aconv) a)) prems) then
193 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
195 fun varify_noninducts (t as Free (s, T)) =
196 if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
197 | varify_noninducts t = t
199 concl_prop |> map_aterms varify_noninducts |> close_form
200 |> lambda (Free ind_x)
201 |> string_for_term ctxt
203 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
204 stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
207 fun type_match thy (T1, T2) =
208 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
209 handle Type.TYPE_MATCH => false
211 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
212 case struct_induct_rule_on th of
213 SOME (p_name, ind_T) =>
214 let val thy = Proof_Context.theory_of ctxt in
215 stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
216 |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
220 (***************************************************************)
221 (* Relevance Filtering *)
222 (***************************************************************)
224 (*** constants with types ***)
226 fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
227 Int.max (order_of_type T1 + 1, order_of_type T2)
228 | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
229 | order_of_type _ = 0
231 (* An abstraction of Isabelle types and first-order terms *)
232 datatype pattern = PVar | PApp of string * pattern list
233 datatype ptype = PType of int * pattern list
235 fun string_for_pattern PVar = "_"
236 | string_for_pattern (PApp (s, ps)) =
237 if null ps then s else s ^ string_for_patterns ps
238 and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
239 fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
241 (*Is the second type an instance of the first one?*)
242 fun match_pattern (PVar, _) = true
243 | match_pattern (PApp _, PVar) = false
244 | match_pattern (PApp (s, ps), PApp (t, qs)) =
245 s = t andalso match_patterns (ps, qs)
246 and match_patterns (_, []) = true
247 | match_patterns ([], _) = false
248 | match_patterns (p :: ps, q :: qs) =
249 match_pattern (p, q) andalso match_patterns (ps, qs)
250 fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
252 (* Is there a unifiable constant? *)
253 fun pconst_mem f consts (s, ps) =
254 exists (curry (match_ptype o f) ps)
255 (map snd (filter (curry (op =) s o fst) consts))
256 fun pconst_hyper_mem f const_tab (s, ps) =
257 exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
259 fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
260 | pattern_for_type (TFree (s, _)) = PApp (s, [])
261 | pattern_for_type (TVar _) = PVar
263 (* Pairs a constant with the list of its type instantiations. *)
264 fun ptype thy const x =
265 (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
267 fun rich_ptype thy const (s, T) =
268 PType (order_of_type T, ptype thy const (s, T))
269 fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
271 fun string_for_hyper_pconst (s, ps) =
272 s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
274 (* Add a pconstant to the table, but a [] entry means a standard
275 connective, which we ignore.*)
276 fun add_pconst_to_table also_skolem (s, p) =
277 if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
278 else Symtab.map_default (s, [p]) (insert (op =) p)
280 fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
282 val flip = Option.map not
283 (* We include free variables, as well as constants, to handle locales. For
284 each quantifiers that must necessarily be skolemized by the automatic
285 prover, we introduce a fresh constant to simulate the effect of
287 fun do_const const x ts =
288 let val (built_in, ts) = is_built_in_const x ts in
290 ? add_pconst_to_table also_skolems (rich_pconst thy const x))
291 #> fold (do_term false) ts
293 and do_term ext_arg t =
295 (Const x, ts) => do_const true x ts
296 | (Free x, ts) => do_const false x ts
297 | (Abs (_, T, t'), ts) =>
298 ((null ts andalso not ext_arg)
299 (* Since lambdas on the right-hand side of equalities are usually
300 extensionalized later by "extensionalize_term", we don't penalize
302 ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
303 #> fold (do_term false) (t' :: ts)
304 | (_, ts) => fold (do_term false) ts
305 fun do_quantifier will_surely_be_skolemized abs_T body_t =
306 do_formula pos body_t
307 #> (if also_skolems andalso will_surely_be_skolemized then
308 add_pconst_to_table true
309 (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
312 and do_term_or_formula ext_arg T =
313 if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
314 and do_formula pos t =
316 Const (@{const_name all}, _) $ Abs (_, T, t') =>
317 do_quantifier (pos = SOME false) T t'
318 | @{const "==>"} $ t1 $ t2 =>
319 do_formula (flip pos) t1 #> do_formula pos t2
320 | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
321 do_term_or_formula false T t1 #> do_term_or_formula true T t2
322 | @{const Trueprop} $ t1 => do_formula pos t1
323 | @{const False} => I
325 | @{const Not} $ t1 => do_formula (flip pos) t1
326 | Const (@{const_name All}, _) $ Abs (_, T, t') =>
327 do_quantifier (pos = SOME false) T t'
328 | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
329 do_quantifier (pos = SOME true) T t'
330 | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
331 | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
332 | @{const HOL.implies} $ t1 $ t2 =>
333 do_formula (flip pos) t1 #> do_formula pos t2
334 | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
335 do_term_or_formula false T t1 #> do_term_or_formula true T t2
336 | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
338 do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
339 | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
340 do_quantifier (is_some pos) T t'
341 | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
342 do_quantifier (pos = SOME false) T
343 (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
344 | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
345 do_quantifier (pos = SOME true) T
346 (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
347 | (t0 as Const (_, @{typ bool})) $ t1 =>
348 do_term false t0 #> do_formula pos t1 (* theory constant *)
349 | _ => do_term false t
350 in do_formula pos end
352 (*Inserts a dummy "constant" referring to the theory name, so that relevance
353 takes the given theory into account.*)
354 fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
355 : relevance_fudge) thy_name t =
356 if exists (curry (op <) 0.0) [theory_const_rel_weight,
357 theory_const_irrel_weight] then
358 Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
362 fun theory_const_prop_of fudge th =
363 theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
365 (**** Constant / Type Frequencies ****)
367 (* A two-dimensional symbol table counts frequencies of constants. It's keyed
368 first by constant name and second by its list of type instantiations. For the
369 latter, we need a linear ordering on "pattern list". *)
373 (PVar, PVar) => EQUAL
374 | (PVar, PApp _) => LESS
375 | (PApp _, PVar) => GREATER
376 | (PApp q1, PApp q2) =>
377 prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
378 fun ptype_ord (PType p, PType q) =
379 prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
381 structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
383 fun count_fact_consts thy fudge =
385 fun do_const const (s, T) ts =
386 (* Two-dimensional table update. Constant maps to types maps to count. *)
387 PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
388 |> Symtab.map_default (s, PType_Tab.empty)
392 (Const x, ts) => do_const true x ts
393 | (Free x, ts) => do_const false x ts
394 | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
395 | (_, ts) => fold do_term ts
396 in do_term o theory_const_prop_of fudge o snd end
399 (**** Actual Filtering Code ****)
401 fun pow_int _ 0 = 1.0
403 | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
405 (*The frequency of a constant is the sum of those of all instances of its type.*)
406 fun pconst_freq match const_tab (c, ps) =
407 PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
408 (the (Symtab.lookup const_tab c)) 0
411 (* A surprising number of theorems contain only a few significant constants.
412 These include all induction rules, and other general theorems. *)
414 (* "log" seems best in practice. A constant function of one ignores the constant
415 frequencies. Rare constants give more points if they are relevant than less
417 fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
419 (* Irrelevant constants are treated differently. We associate lower penalties to
420 very rare constants and very common ones -- the former because they can't
421 lead to the inclusion of too many new facts, and the latter because they are
422 so common as to be of little interest. *)
423 fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
424 : relevance_fudge) order freq =
425 let val (k, x) = worse_irrel_freq |> `Real.ceil in
426 (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
427 else rel_weight_for order freq / rel_weight_for order k)
428 * pow_int higher_order_irrel_weight (order - 1)
431 fun multiplier_for_const_name local_const_multiplier s =
432 if String.isSubstring "." s then 1.0 else local_const_multiplier
434 (* Computes a constant's weight, as determined by its frequency. *)
435 fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
436 theory_const_weight chained_const_weight weight_for f
437 const_tab chained_const_tab (c as (s, PType (m, _))) =
440 else if String.isPrefix skolem_prefix s then
442 else if String.isSuffix theory_const_suffix s then
445 multiplier_for_const_name local_const_multiplier s
446 * weight_for m (pconst_freq (match_ptype o f) const_tab c)
447 |> (if chained_const_weight < 1.0 andalso
448 pconst_hyper_mem I chained_const_tab c then
449 curry (op *) chained_const_weight
453 fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
454 theory_const_rel_weight, ...} : relevance_fudge)
456 generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
457 theory_const_rel_weight 0.0 rel_weight_for I const_tab
460 fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
462 theory_const_irrel_weight,
463 chained_const_irrel_weight, ...})
464 const_tab chained_const_tab =
465 generic_pconst_weight local_const_multiplier abs_irrel_weight
466 skolem_irrel_weight theory_const_irrel_weight
467 chained_const_irrel_weight (irrel_weight_for fudge) swap
468 const_tab chained_const_tab
470 fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
472 | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
473 | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
474 | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
475 | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
476 | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
477 | stature_bonus _ _ = 0.0
479 fun is_odd_const_name s =
480 s = abs_name orelse String.isPrefix skolem_prefix s orelse
481 String.isSuffix theory_const_suffix s
483 fun fact_weight fudge stature const_tab relevant_consts chained_consts
485 case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
486 ||> filter_out (pconst_hyper_mem swap relevant_consts) of
489 if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
493 val irrel = irrel |> filter_out (pconst_mem swap rel)
495 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
497 ~ (stature_bonus fudge stature)
498 |> fold (curry (op +)
499 o irrel_pconst_weight fudge const_tab chained_consts) irrel
500 val res = rel_weight / (rel_weight + irrel_weight)
501 in if Real.isFinite res then res else 0.0 end
503 fun pconsts_in_fact thy is_built_in_const t =
504 Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
505 (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
508 fun pair_consts_fact thy is_built_in_const fudge fact =
509 case fact |> snd |> theory_const_prop_of fudge
510 |> pconsts_in_fact thy is_built_in_const of
512 | consts => SOME ((fact, consts), NONE)
514 val const_names_in_fact = map fst ooo pconsts_in_fact
517 (((unit -> string) * stature) * thm) * (string * ptype) list
519 fun take_most_relevant ctxt max_relevant remaining_max
520 ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
521 (candidates : (annotated_thm * real) list) =
524 Real.ceil (Math.pow (max_imperfect,
525 Math.pow (Real.fromInt remaining_max
526 / Real.fromInt max_relevant, max_imperfect_exp)))
527 val (perfect, imperfect) =
528 candidates |> sort (Real.compare o swap o pairself snd)
529 |> take_prefix (fn (_, w) => w > 0.99999)
530 val ((accepts, more_rejects), rejects) =
531 chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
533 trace_msg ctxt (fn () =>
534 "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
535 string_of_int (length candidates) ^ "): " ^
536 (accepts |> map (fn ((((name, _), _), _), weight) =>
537 name () ^ " [" ^ Real.toString weight ^ "]")
539 (accepts, more_rejects @ rejects)
542 fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
543 if Symtab.is_empty tab then
545 |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
546 (map_filter (fn ((_, (sc', _)), th) =>
547 if sc' = sc then SOME (prop_of th) else NONE) facts)
551 fun consider_arities is_built_in_const th =
553 fun aux _ _ NONE = NONE
554 | aux t args (SOME tab) =
556 t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
557 | Const (x as (s, _)) =>
558 (if is_built_in_const x args |> fst then
560 else case Symtab.lookup tab s of
561 NONE => SOME (Symtab.update (s, length args) tab)
562 | SOME n => if n = length args then SOME tab else NONE)
564 in aux (prop_of th) [] end
566 (* FIXME: This is currently only useful for polymorphic type encodings. *)
567 fun could_benefit_from_ext is_built_in_const facts =
568 fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
571 (* High enough so that it isn't wrongly considered as very relevant (e.g., for E
572 weights), but low enough so that it is unlikely to be truncated away if few
573 facts are included. *)
574 val special_fact_index = 75
576 fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
577 (fudge as {threshold_divisor, ridiculous_threshold, ...})
578 ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
580 val thy = Proof_Context.theory_of ctxt
581 val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
582 val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
583 val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
585 Symtab.empty |> fold (add_pconsts true) hyp_ts
586 |> add_pconsts false concl_t
587 |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
588 |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
589 [Chained, Assum, Local]
590 val add_ths = Attrib.eval_thms ctxt add
591 val del_ths = Attrib.eval_thms ctxt del
592 val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
593 fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
595 fun relevant [] _ [] =
596 (* Nothing has been added this iteration. *)
597 if j = 0 andalso threshold >= ridiculous_threshold then
598 (* First iteration? Try again. *)
599 iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
603 | relevant candidates rejects [] =
605 val (accepts, more_rejects) =
606 take_most_relevant ctxt max_relevant remaining_max fudge
610 |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
611 fun is_dirty (c, _) =
612 Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
613 val (hopeful_rejects, hopeless_rejects) =
614 (rejects @ hopeless, ([], []))
615 |-> fold (fn (ax as (_, consts), old_weight) =>
616 if exists is_dirty consts then
617 apfst (cons (ax, NONE))
619 apsnd (cons (ax, old_weight)))
620 |>> append (more_rejects
621 |> map (fn (ax as (_, consts), old_weight) =>
622 (ax, if exists is_dirty consts then NONE
623 else SOME old_weight)))
625 1.0 - (1.0 - threshold)
626 * Math.pow (decay, Real.fromInt (length accepts))
627 val remaining_max = remaining_max - length accepts
629 trace_msg ctxt (fn () => "New or updated constants: " ^
630 commas (rel_const_tab' |> Symtab.dest
631 |> subtract (op =) (rel_const_tab |> Symtab.dest)
632 |> map string_for_hyper_pconst));
633 map (fst o fst) accepts @
634 (if remaining_max = 0 then
637 iter (j + 1) remaining_max threshold rel_const_tab'
638 hopeless_rejects hopeful_rejects)
640 | relevant candidates rejects
641 (((ax as (((_, stature), _), fact_consts)), cached_weight)
645 case cached_weight of
647 | NONE => fact_weight fudge stature const_tab rel_const_tab
648 chained_const_tab fact_consts
650 if weight >= threshold then
651 relevant ((ax, weight) :: candidates) rejects hopeful
653 relevant candidates ((ax, weight) :: rejects) hopeful
656 trace_msg ctxt (fn () =>
657 "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
658 Real.toString threshold ^ ", constants: " ^
659 commas (rel_const_tab |> Symtab.dest
660 |> filter (curry (op <>) [] o snd)
661 |> map string_for_hyper_pconst));
662 relevant [] [] hopeful
664 fun prepend_facts ths accepts =
665 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
666 (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
668 fun insert_into_facts accepts [] = accepts
669 | insert_into_facts accepts ths =
671 val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
673 accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
674 |> take (max_relevant - length add)
675 |> chop special_fact_index
676 in bef @ add @ after end
677 fun insert_special_facts accepts =
678 [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
679 |> insert_into_facts accepts
681 facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
682 |> iter 0 max_relevant threshold0 goal_const_tab []
683 |> not (null add_ths) ? prepend_facts add_ths
684 |> insert_special_facts
685 |> tap (fn accepts => trace_msg ctxt (fn () =>
686 "Total relevant: " ^ string_of_int (length accepts)))
690 (***************************************************************)
691 (* Retrieving and filtering lemmas *)
692 (***************************************************************)
694 (*** retrieve lemmas and filter them ***)
696 (*Reject theorems with names like "List.filter.filter_list_def" or
697 "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
698 fun is_package_def a =
699 let val names = Long_Name.explode a in
700 (length names > 2 andalso not (hd names = "local") andalso
701 String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
705 Termtab.fold (cons o snd)
706 (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
708 (* FIXME: put other record thms here, or declare as "no_atp" *)
709 fun multi_base_blacklist ctxt ho_atp =
710 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
711 "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
713 |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
714 append ["induct", "inducts"]
717 val max_lambda_nesting = 3 (*only applies if not ho_atp*)
719 fun term_has_too_many_lambdas max (t1 $ t2) =
720 exists (term_has_too_many_lambdas max) [t1, t2]
721 | term_has_too_many_lambdas max (Abs (_, _, t)) =
722 max = 0 orelse term_has_too_many_lambdas (max - 1) t
723 | term_has_too_many_lambdas _ _ = false
725 (* Don't count nested lambdas at the level of formulas, since they are
727 fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
728 | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
729 formula_has_too_many_lambdas false (T :: Ts) t
730 | formula_has_too_many_lambdas _ Ts t =
731 if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
732 exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
734 term_has_too_many_lambdas max_lambda_nesting t
736 (* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
738 val max_apply_depth = 15
740 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
741 | apply_depth (Abs (_, _, t)) = apply_depth t
744 fun is_formula_too_complex ho_atp t =
745 apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
747 (* FIXME: Extend to "Meson" and "Metis" *)
748 val exists_sledgehammer_const =
749 exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
751 (* FIXME: make more reliable *)
752 val exists_low_level_class_const =
753 exists_Const (fn (s, _) =>
754 String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
756 fun is_metastrange_theorem th =
757 case head_of (concl_of th) of
758 Const (s, _) => (s <> @{const_name Trueprop} andalso
759 s <> @{const_name "=="})
762 fun is_that_fact th =
763 String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
764 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
765 | _ => false) (prop_of th)
767 (**** Predicates to detect unwanted facts (prolific or likely to cause
770 fun is_theorem_bad_for_atps ho_atp exporter thm =
771 is_metastrange_theorem thm orelse
772 (not exporter andalso
773 let val t = prop_of thm in
774 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
775 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
779 val crude_zero_vars =
780 map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
781 #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
783 fun clasimpset_rule_table_of ctxt =
785 val thy = Proof_Context.theory_of ctxt
786 val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
787 fun add stature g f =
788 fold (Termtab.update o rpair stature o g o crude_zero_vars o prop_of o f)
789 val {safeIs, safeEs, hazIs, hazEs, ...} =
790 ctxt |> claset_of |> Classical.rep_cs
791 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
793 Item_Net.content safeEs @ Item_Net.content hazEs
794 |> map Classical.classical_rule
795 val simps = ctxt |> simpset_of |> dest_ss |> #simps
797 Termtab.empty |> add Intro I I intros
798 |> add Elim I I elims
799 |> add Simp I snd simps
800 |> add Simp atomize snd simps
803 fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
805 val thy = Proof_Context.theory_of ctxt
806 val global_facts = Global_Theory.facts_of thy
807 val local_facts = Proof_Context.facts_of ctxt
808 val named_locals = local_facts |> Facts.dest_static []
809 val assms = Assumption.all_assms_of ctxt
810 fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
811 val is_chained = member Thm.eq_thm_prop chained_ths
812 val clasimpset_table = clasimpset_rule_table_of ctxt
813 fun scope_of_thm global th =
814 if is_chained th then Chained
815 else if global then Global
816 else if is_assum th then Assum
818 fun status_of_thm name th =
819 (* FIXME: use structured name *)
820 if String.isSubstring ".induct" name orelse
821 String.isSubstring ".inducts" name then
823 else case Termtab.lookup clasimpset_table (prop_of th) of
824 SOME status => status
826 fun is_good_unnamed_local th =
827 not (Thm.has_name_hint th) andalso
828 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
830 union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
831 |> filter is_good_unnamed_local |> map (pair "" o single)
833 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
834 fun add_facts global foldx facts =
835 foldx (fn (name0, ths) =>
836 if not exporter andalso name0 <> "" andalso
837 forall (not o member Thm.eq_thm_prop add_ths) ths andalso
838 (Facts.is_concealed facts name0 orelse
839 (not (Config.get ctxt ignore_no_atp) andalso
840 is_package_def name0) orelse
841 exists (fn s => String.isSuffix s name0)
842 (multi_base_blacklist ctxt ho_atp) orelse
843 String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
847 val multi = length ths > 1
849 backquote o string_for_term ctxt o close_form o prop_of
851 case try (Proof_Context.get_thms ctxt) a of
853 | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
856 #> fold (fn th => fn (j, (multis, unis)) =>
858 if not (member Thm.eq_thm_prop add_ths th) andalso
859 is_theorem_bad_for_atps ho_atp exporter th then
868 [Facts.extern ctxt facts name0,
869 Name_Space.extern ctxt full_space name0,
871 |> find_first check_thms
873 make_name reserved multi j name
875 (scope_of_thm global th,
876 status_of_thm name0 th)), th)
878 if multi then (new :: multis, unis)
879 else (multis, new :: unis)
884 (* The single-name theorems go after the multiple-name ones, so that single
885 names are preferred when both are available. *)
886 ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
887 |> add_facts true Facts.fold_static global_facts global_facts
891 fun external_frees t =
892 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
894 fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
895 chained_ths hyp_ts concl_t =
897 val thy = Proof_Context.theory_of ctxt
898 val reserved = reserved_isar_keyword_table ()
899 val add_ths = Attrib.eval_thms ctxt add
901 Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
902 |> Object_Logic.atomize_term thy
903 val ind_stmt_xs = external_frees ind_stmt
906 maps (map (fn ((name, stature), th) => ((K name, stature), th))
907 o fact_from_ref ctxt reserved chained_ths) add
909 all_facts ctxt ho_atp reserved false add_ths chained_ths)
910 |> Config.get ctxt instantiate_inducts
911 ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
912 |> (not (Config.get ctxt ignore_no_atp) andalso not only)
913 ? filter_out (No_ATPs.member ctxt o snd)
917 fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
918 fudge (override as {only, ...}) chained_ths hyp_ts concl_t
921 val thy = Proof_Context.theory_of ctxt
922 val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
923 1.0 / Real.fromInt (max_relevant + 1))
925 trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
927 (if only orelse threshold1 < 0.0 then
929 else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
930 max_relevant = 0 then
933 relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
934 fudge override facts (chained_ths |> map prop_of) hyp_ts
935 (concl_t |> theory_constify fudge (Context.theory_name thy)))
936 |> map (apfst (apfst (fn f => f ())))