further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
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 relevance_override =
14 {add : (Facts.ref * Attrib.src list) list,
15 del : (Facts.ref * Attrib.src list) list,
18 val ignore_no_atp : bool Config.T
19 val instantiate_inducts : bool Config.T
20 val no_relevance_override : relevance_override
22 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
23 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
25 Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
26 -> thm list -> status Termtab.table
27 -> (((unit -> string) * stature) * thm) list
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 nearly_all_facts :
34 Proof.context -> bool -> relevance_override -> thm list -> term list -> term
35 -> (((unit -> string) * stature) * thm) list
38 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
41 open ATP_Problem_Generate
43 open Sledgehammer_Util
45 type relevance_override =
46 {add : (Facts.ref * Attrib.src list) list,
47 del : (Facts.ref * Attrib.src list) list,
50 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
52 (* experimental features *)
54 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
55 val instantiate_inducts =
56 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
58 val no_relevance_override = {add = [], del = [], only = false}
60 fun needs_quoting reserved s =
61 Symtab.defined reserved s orelse
62 exists (not o Lexicon.is_identifier) (Long_Name.explode s)
64 fun make_name reserved multi j name =
65 (name |> needs_quoting reserved name ? quote) ^
66 (if multi then "(" ^ string_of_int j ^ ")" else "")
68 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
69 | explode_interval max (Facts.From i) = i upto i + max - 1
70 | explode_interval _ (Facts.Single i) = [i]
73 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
75 (* unfolding these can yield really huge terms *)
76 val risky_defs = @{thms Bit0_def Bit1_def}
78 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
79 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
80 | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
81 | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
82 | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
83 | is_rec_def _ = false
85 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
86 fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
88 fun scope_of_thm global assms chained_ths th =
89 if is_chained chained_ths th then Chained
90 else if global then Global
91 else if is_assum assms th then Assum
94 val may_be_induction =
95 exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
96 body_type T = @{typ bool}
99 fun status_of_thm css_table name th =
100 (* FIXME: use structured name *)
101 if (String.isSubstring ".induct" name orelse
102 String.isSubstring ".inducts" name) andalso
103 may_be_induction (prop_of th) then
105 else case Termtab.lookup css_table (prop_of th) of
106 SOME status => status
109 fun stature_of_thm global assms chained_ths css_table name th =
110 (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
112 fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
114 val ths = Attrib.eval_thms ctxt [xthm]
116 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
120 Facts.Fact s => backquote s ^ bracket
121 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
122 | Facts.Named ((name, _), NONE) =>
123 make_name reserved (length ths > 1) (j + 1) name ^ bracket
124 | Facts.Named ((name, _), SOME intervals) =>
125 make_name reserved true
126 (nth (maps (explode_interval (length ths)) intervals) j) name ^
130 |-> fold (fn th => fn (j, rest) =>
131 let val name = nth_name j in
132 (j + 1, ((name, stature_of_thm false [] chained_ths
133 css_table name th), th) :: rest)
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 exporter thm =
207 is_metastrange_theorem thm orelse
208 (not exporter andalso
209 let val t = prop_of thm in
210 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
211 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
215 fun hackish_string_for_term ctxt t =
216 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
217 (print_mode_value ())) (Syntax.string_of_term ctxt) t
218 |> String.translate (fn c => if Char.isPrint c then str c else "")
221 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
222 they are displayed as "M" and we want to avoid clashes with these. But
223 sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
224 prefixes of all free variables. In the worse case scenario, where the fact
225 won't be resolved correctly, the user can fix it manually, e.g., by naming
226 the fact in question. Ideally we would need nothing of it, but backticks
227 simply don't work with schematic variables. *)
228 fun all_prefixes_of s =
229 map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
232 (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
233 |> fold (fn ((s, i), T) => fn (t', taken) =>
234 let val s' = singleton (Name.variant_list taken) s in
235 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
236 else Logic.all_const) T
237 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
240 (Term.add_vars t [] |> sort_wrt (fst o fst))
243 fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
245 val thy = Proof_Context.theory_of ctxt
246 val global_facts = Global_Theory.facts_of thy
247 val local_facts = Proof_Context.facts_of ctxt
248 val named_locals = local_facts |> Facts.dest_static []
249 val assms = Assumption.all_assms_of ctxt
250 fun is_good_unnamed_local th =
251 not (Thm.has_name_hint th) andalso
252 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
254 union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
255 |> filter is_good_unnamed_local |> map (pair "" o single)
257 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
258 fun add_facts global foldx facts =
259 foldx (fn (name0, ths) =>
260 if not exporter andalso name0 <> "" andalso
261 forall (not o member Thm.eq_thm_prop add_ths) ths andalso
262 (Facts.is_concealed facts name0 orelse
263 (not (Config.get ctxt ignore_no_atp) andalso
264 is_package_def name0) orelse
265 exists (fn s => String.isSuffix s name0)
266 (multi_base_blacklist ctxt ho_atp)) then
270 val multi = length ths > 1
272 backquote o hackish_string_for_term ctxt o close_form o prop_of
274 case try (Proof_Context.get_thms ctxt) a of
276 | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
279 #> fold (fn th => fn (j, (multis, unis)) =>
281 if not (member Thm.eq_thm_prop add_ths th) andalso
282 is_theorem_bad_for_atps ho_atp exporter th then
291 [Facts.extern ctxt facts name0,
292 Name_Space.extern ctxt full_space name0,
294 |> find_first check_thms
296 make_name reserved multi j name
298 stature_of_thm global assms chained_ths
299 css_table name0 th), th)
301 if multi then (new :: multis, unis)
302 else (multis, new :: unis)
307 (* The single-name theorems go after the multiple-name ones, so that single
308 names are preferred when both are available. *)
309 ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
310 |> add_facts true Facts.fold_static global_facts global_facts
314 fun clasimpset_rule_table_of ctxt =
316 val thy = Proof_Context.theory_of ctxt
317 val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
318 fun add stature normalizers get_th =
321 val th = rule |> get_th
323 th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
325 fold (fn normalize => Termtab.update (normalize t, stature))
328 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
329 ctxt |> claset_of |> Classical.rep_cs
330 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
331 (* Add once it is used:
333 Item_Net.content safeEs @ Item_Net.content hazEs
334 |> map Classical.classical_rule
336 val simps = ctxt |> simpset_of |> dest_ss |> #simps
337 val specs = ctxt |> Spec_Rules.get
338 val (rec_defs, nonrec_defs) =
339 specs |> filter (curry (op =) Spec_Rules.Equational o fst)
341 |> filter_out (member Thm.eq_thm_prop risky_defs)
342 |> List.partition (is_rec_def o prop_of)
344 specs |> filter (member (op =) [Spec_Rules.Inductive,
345 Spec_Rules.Co_Inductive] o fst)
348 Termtab.empty |> add Simp [atomize] snd simps
349 |> add Simp [] I rec_defs
350 |> add Def [] I nonrec_defs
351 (* Add once it is used:
352 |> add Elim [] I elims
354 |> add Intro [] I intros
355 |> add Inductive [] I spec_intros
359 Termtab.fold (cons o snd)
360 (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
362 fun struct_induct_rule_on th =
363 case Logic.strip_horn (prop_of th) of
364 (prems, @{const Trueprop}
365 $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
366 if not (is_TVar ind_T) andalso length prems > 1 andalso
367 exists (exists_subterm (curry (op aconv) p)) prems andalso
368 not (exists (exists_subterm (curry (op aconv) a)) prems) then
374 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
376 fun varify_noninducts (t as Free (s, T)) =
377 if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
378 | varify_noninducts t = t
380 concl_prop |> map_aterms varify_noninducts |> close_form
381 |> lambda (Free ind_x)
382 |> hackish_string_for_term ctxt
384 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
385 stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
388 fun type_match thy (T1, T2) =
389 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
390 handle Type.TYPE_MATCH => false
392 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
393 case struct_induct_rule_on th of
394 SOME (p_name, ind_T) =>
395 let val thy = Proof_Context.theory_of ctxt in
396 stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
397 |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
401 fun external_frees t =
402 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
404 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
405 if Config.get ctxt instantiate_inducts then
407 val thy = Proof_Context.theory_of ctxt
409 (hyp_ts |> filter_out (null o external_frees), concl_t)
410 |> Logic.list_implies |> Object_Logic.atomize_term thy
411 val ind_stmt_xs = external_frees ind_stmt
412 in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
416 fun maybe_filter_no_atps ctxt =
417 not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
419 fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
420 chained_ths hyp_ts concl_t =
421 if only andalso null add then
425 val reserved = reserved_isar_keyword_table ()
426 val add_ths = Attrib.eval_thms ctxt add
427 val css_table = clasimpset_rule_table_of ctxt
430 maps (map (fn ((name, stature), th) => ((K name, stature), th))
431 o fact_from_ref ctxt reserved chained_ths css_table) add
433 all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
434 |> maybe_instantiate_inducts ctxt hyp_ts concl_t
435 |> not only ? maybe_filter_no_atps ctxt