1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
3 Author: Jasmin Blanchette, TU Muenchen
5 Sledgehammer fact handling.
8 signature SLEDGEHAMMER_FACT =
10 type status = ATP_Problem_Generate.status
11 type stature = ATP_Problem_Generate.stature
13 type fact = ((unit -> string) * stature) * thm
16 {add : (Facts.ref * Attrib.src list) list,
17 del : (Facts.ref * Attrib.src list) list,
20 val ignore_no_atp : bool Config.T
21 val instantiate_inducts : bool Config.T
22 val no_fact_override : fact_override
24 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
25 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
26 val is_likely_tautology_or_too_meta : thm -> bool
27 val backquote_thm : thm -> string
28 val clasimpset_rule_table_of : Proof.context -> status Termtab.table
29 val maybe_instantiate_inducts :
30 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
31 -> (((unit -> string) * 'a) * thm) list
32 val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
33 val all_facts_of : Proof.context -> status Termtab.table -> fact list
34 val nearly_all_facts :
35 Proof.context -> bool -> fact_override -> unit Symtab.table
36 -> status Termtab.table -> thm list -> term list -> term -> fact list
39 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
42 open ATP_Problem_Generate
44 open Sledgehammer_Util
46 type fact = ((unit -> string) * stature) * thm
49 {add : (Facts.ref * Attrib.src list) list,
50 del : (Facts.ref * Attrib.src list) list,
53 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
55 (* experimental features *)
57 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
58 val instantiate_inducts =
59 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
61 val no_fact_override = {add = [], del = [], only = false}
63 fun needs_quoting reserved s =
64 Symtab.defined reserved s orelse
65 exists (not o Lexicon.is_identifier) (Long_Name.explode s)
67 fun make_name reserved multi j name =
68 (name |> needs_quoting reserved name ? quote) ^
69 (if multi then "(" ^ string_of_int j ^ ")" else "")
71 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
72 | explode_interval max (Facts.From i) = i upto i + max - 1
73 | explode_interval _ (Facts.Single i) = [i]
76 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
78 (* unfolding these can yield really huge terms *)
79 val risky_defs = @{thms Bit0_def Bit1_def}
81 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
82 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
83 | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
84 | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
85 | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
86 | is_rec_def _ = false
88 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
89 fun is_chained chained = member Thm.eq_thm_prop chained
91 fun scope_of_thm global assms chained th =
92 if is_chained chained th then Chained
93 else if global then Global
94 else if is_assum assms th then Assum
97 val may_be_induction =
98 exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
99 body_type T = @{typ bool}
102 fun status_of_thm css name th =
103 (* FIXME: use structured name *)
104 if (String.isSubstring ".induct" name orelse
105 String.isSubstring ".inducts" name) andalso
106 may_be_induction (prop_of th) then
108 else case Termtab.lookup css (prop_of th) of
109 SOME status => status
112 fun stature_of_thm global assms chained css name th =
113 (scope_of_thm global assms chained th, status_of_thm css name th)
115 fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
117 val ths = Attrib.eval_thms ctxt [xthm]
119 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
123 Facts.Fact s => backquote s ^ bracket
124 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
125 | Facts.Named ((name, _), NONE) =>
126 make_name reserved (length ths > 1) (j + 1) name ^ bracket
127 | Facts.Named ((name, _), SOME intervals) =>
128 make_name reserved true
129 (nth (maps (explode_interval (length ths)) intervals) j) name ^
131 fun add_nth th (j, rest) =
132 let val name = nth_name j in
133 (j + 1, ((name, stature_of_thm false [] chained css name th), th)
136 in (0, []) |> fold add_nth ths |> snd end
138 (* Reject theorems with names like "List.filter.filter_list_def" or
139 "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
140 fun is_package_def a =
141 let val names = Long_Name.explode a in
142 (length names > 2 andalso not (hd names = "local") andalso
143 String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
146 (* FIXME: put other record thms here, or declare as "no_atp" *)
147 fun multi_base_blacklist ctxt ho_atp =
148 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
149 "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
151 |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
152 append ["induct", "inducts"]
155 val max_lambda_nesting = 3 (*only applies if not ho_atp*)
157 fun term_has_too_many_lambdas max (t1 $ t2) =
158 exists (term_has_too_many_lambdas max) [t1, t2]
159 | term_has_too_many_lambdas max (Abs (_, _, t)) =
160 max = 0 orelse term_has_too_many_lambdas (max - 1) t
161 | term_has_too_many_lambdas _ _ = false
163 (* Don't count nested lambdas at the level of formulas, since they are
165 fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
166 | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
167 formula_has_too_many_lambdas false (T :: Ts) t
168 | formula_has_too_many_lambdas _ Ts t =
169 if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
170 exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
172 term_has_too_many_lambdas max_lambda_nesting t
174 (* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
176 val max_apply_depth = 15
178 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
179 | apply_depth (Abs (_, _, t)) = apply_depth t
182 fun is_formula_too_complex ho_atp t =
183 apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
185 (* FIXME: Extend to "Meson" and "Metis" *)
186 val exists_sledgehammer_const =
187 exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
189 (* FIXME: make more reliable *)
190 val exists_low_level_class_const =
191 exists_Const (fn (s, _) =>
192 s = @{const_name equal_class.equal} orelse
193 String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
195 fun is_metastrange_theorem th =
196 case head_of (concl_of th) of
197 Const (s, _) => (s <> @{const_name Trueprop} andalso
198 s <> @{const_name "=="})
201 fun is_that_fact th =
202 String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
203 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
204 | _ => false) (prop_of th)
206 fun is_theorem_bad_for_atps ho_atp thm =
207 is_metastrange_theorem thm orelse
208 let val t = prop_of thm in
209 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
210 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
214 fun is_likely_tautology_or_too_meta th =
216 val is_boring_const = member (op =) atp_widely_irrelevant_consts
217 fun is_boring_bool t =
218 not (exists_Const (not o is_boring_const o fst) t) orelse
219 exists_type (exists_subtype (curry (op =) @{typ prop})) t
220 fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
221 | is_boring_prop (@{const "==>"} $ t $ u) =
222 is_boring_prop t andalso is_boring_prop u
223 | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
224 is_boring_prop t andalso is_boring_prop u
225 | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
226 is_boring_bool t andalso is_boring_bool u
227 | is_boring_prop _ = true
229 is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
232 fun hackish_string_for_term thy t =
233 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
234 (print_mode_value ())) (Syntax.string_of_term_global thy) t
235 |> String.translate (fn c => if Char.isPrint c then str c else "")
238 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
239 they are displayed as "M" and we want to avoid clashes with these. But
240 sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
241 prefixes of all free variables. In the worse case scenario, where the fact
242 won't be resolved correctly, the user can fix it manually, e.g., by naming
243 the fact in question. Ideally we would need nothing of it, but backticks
244 simply don't work with schematic variables. *)
245 fun all_prefixes_of s =
246 map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
249 (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
250 |> fold (fn ((s, i), T) => fn (t', taken) =>
251 let val s' = singleton (Name.variant_list taken) s in
252 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
253 else Logic.all_const) T
254 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
257 (Term.add_vars t [] |> sort_wrt (fst o fst))
260 fun backquote_term thy t =
262 |> hackish_string_for_term thy
265 fun backquote_thm th = backquote_term (theory_of_thm th) (prop_of th)
267 fun clasimpset_rule_table_of ctxt =
269 val thy = Proof_Context.theory_of ctxt
270 val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
271 fun add stature normalizers get_th =
274 val th = rule |> get_th
276 th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
278 fold (fn normalize => Termtab.update (normalize t, stature))
281 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
282 ctxt |> claset_of |> Classical.rep_cs
283 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
284 (* Add once it is used:
286 Item_Net.content safeEs @ Item_Net.content hazEs
287 |> map Classical.classical_rule
289 val simps = ctxt |> simpset_of |> dest_ss |> #simps
290 val specs = ctxt |> Spec_Rules.get
291 val (rec_defs, nonrec_defs) =
292 specs |> filter (curry (op =) Spec_Rules.Equational o fst)
294 |> filter_out (member Thm.eq_thm_prop risky_defs)
295 |> List.partition (is_rec_def o prop_of)
297 specs |> filter (member (op =) [Spec_Rules.Inductive,
298 Spec_Rules.Co_Inductive] o fst)
301 Termtab.empty |> add Simp [atomize] snd simps
302 |> add Simp [] I rec_defs
303 |> add Def [] I nonrec_defs
304 (* Add once it is used:
305 |> add Elim [] I elims
307 |> add Intro [] I intros
308 |> add Inductive [] I spec_intros
312 Termtab.fold (cons o snd)
313 (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
315 fun struct_induct_rule_on th =
316 case Logic.strip_horn (prop_of th) of
317 (prems, @{const Trueprop}
318 $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
319 if not (is_TVar ind_T) andalso length prems > 1 andalso
320 exists (exists_subterm (curry (op aconv) p)) prems andalso
321 not (exists (exists_subterm (curry (op aconv) a)) prems) then
327 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
329 val thy = Proof_Context.theory_of ctxt
330 fun varify_noninducts (t as Free (s, T)) =
331 if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
332 | varify_noninducts t = t
334 concl_prop |> map_aterms varify_noninducts |> close_form
335 |> lambda (Free ind_x)
336 |> hackish_string_for_term thy
338 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
339 stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
342 fun type_match thy (T1, T2) =
343 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
344 handle Type.TYPE_MATCH => false
346 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
347 case struct_induct_rule_on th of
348 SOME (p_name, ind_T) =>
349 let val thy = Proof_Context.theory_of ctxt in
350 stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
351 |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
355 fun external_frees t =
356 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
358 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
359 if Config.get ctxt instantiate_inducts then
361 val thy = Proof_Context.theory_of ctxt
363 (hyp_ts |> filter_out (null o external_frees), concl_t)
364 |> Logic.list_implies |> Object_Logic.atomize_term thy
365 val ind_stmt_xs = external_frees ind_stmt
366 in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
370 fun maybe_filter_no_atps ctxt =
371 not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
373 fun all_facts ctxt ho_atp reserved add_ths chained css =
375 val thy = Proof_Context.theory_of ctxt
376 val global_facts = Global_Theory.facts_of thy
377 val local_facts = Proof_Context.facts_of ctxt
378 val named_locals = local_facts |> Facts.dest_static []
379 val assms = Assumption.all_assms_of ctxt
380 fun is_good_unnamed_local th =
381 not (Thm.has_name_hint th) andalso
382 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
384 union Thm.eq_thm_prop (Facts.props local_facts) chained
385 |> filter is_good_unnamed_local |> map (pair "" o single)
387 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
388 fun add_facts global foldx facts =
389 foldx (fn (name0, ths) =>
390 if name0 <> "" andalso
391 forall (not o member Thm.eq_thm_prop add_ths) ths andalso
392 (Facts.is_concealed facts name0 orelse
393 not (can (Proof_Context.get_thms ctxt) name0) orelse
394 (not (Config.get ctxt ignore_no_atp) andalso
395 is_package_def name0) orelse
396 exists (fn s => String.isSuffix s name0)
397 (multi_base_blacklist ctxt ho_atp)) then
401 val multi = length ths > 1
403 case try (Proof_Context.get_thms ctxt) a of
405 | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
408 #> fold (fn th => fn (j, (multis, unis)) =>
410 if not (member Thm.eq_thm_prop add_ths th) andalso
411 is_theorem_bad_for_atps ho_atp th then
420 [Facts.extern ctxt facts name0,
421 Name_Space.extern ctxt full_space name0]
422 |> find_first check_thms
424 |> make_name reserved multi j),
425 stature_of_thm global assms chained css name0
428 if multi then (new :: multis, unis)
429 else (multis, new :: unis)
434 (* The single-name theorems go after the multiple-name ones, so that single
435 names are preferred when both are available. *)
436 ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
437 |> add_facts true Facts.fold_static global_facts global_facts
441 fun all_facts_of ctxt css =
442 all_facts ctxt false Symtab.empty [] [] css
443 |> rev (* partly restore the original order of facts, for MaSh *)
445 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
447 if only andalso null add then
453 |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
456 maps (map (fn ((name, stature), th) => ((K name, stature), th))
457 o fact_from_ref ctxt reserved chained css) add
459 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
460 all_facts ctxt ho_atp reserved add chained css
461 |> filter_out (is_likely_tautology_or_too_meta o snd)
462 |> filter_out (member Thm.eq_thm_prop del o snd)
463 |> maybe_filter_no_atps ctxt
466 |> maybe_instantiate_inducts ctxt hyp_ts concl_t