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 clasimpset_rule_table_of : Proof.context -> status Termtab.table
27 val maybe_instantiate_inducts :
28 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
29 -> (((unit -> string) * 'a) * thm) list
30 val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
31 val all_facts_of : theory -> status Termtab.table -> fact list
32 val nearly_all_facts :
33 Proof.context -> bool -> fact_override -> unit Symtab.table
34 -> status Termtab.table -> thm list -> term list -> term -> fact list
37 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
40 open ATP_Problem_Generate
42 open Sledgehammer_Util
44 type fact = ((unit -> string) * stature) * thm
47 {add : (Facts.ref * Attrib.src list) list,
48 del : (Facts.ref * Attrib.src list) list,
51 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
53 (* experimental features *)
55 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
56 val instantiate_inducts =
57 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
59 val no_fact_override = {add = [], del = [], only = false}
61 fun needs_quoting reserved s =
62 Symtab.defined reserved s orelse
63 exists (not o Lexicon.is_identifier) (Long_Name.explode s)
65 fun make_name reserved multi j name =
66 (name |> needs_quoting reserved name ? quote) ^
67 (if multi then "(" ^ string_of_int j ^ ")" else "")
69 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
70 | explode_interval max (Facts.From i) = i upto i + max - 1
71 | explode_interval _ (Facts.Single i) = [i]
74 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
76 (* unfolding these can yield really huge terms *)
77 val risky_defs = @{thms Bit0_def Bit1_def}
79 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
80 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
81 | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
82 | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
83 | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
84 | is_rec_def _ = false
86 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
87 fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
89 fun scope_of_thm global assms chained_ths th =
90 if is_chained chained_ths th then Chained
91 else if global then Global
92 else if is_assum assms th then Assum
95 val may_be_induction =
96 exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
97 body_type T = @{typ bool}
100 fun status_of_thm css_table name th =
101 (* FIXME: use structured name *)
102 if (String.isSubstring ".induct" name orelse
103 String.isSubstring ".inducts" name) andalso
104 may_be_induction (prop_of th) then
106 else case Termtab.lookup css_table (prop_of th) of
107 SOME status => status
110 fun stature_of_thm global assms chained_ths css_table name th =
111 (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
113 fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
115 val ths = Attrib.eval_thms ctxt [xthm]
117 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
121 Facts.Fact s => backquote s ^ bracket
122 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
123 | Facts.Named ((name, _), NONE) =>
124 make_name reserved (length ths > 1) (j + 1) name ^ bracket
125 | Facts.Named ((name, _), SOME intervals) =>
126 make_name reserved true
127 (nth (maps (explode_interval (length ths)) intervals) j) name ^
131 |-> fold (fn th => fn (j, rest) =>
132 let val name = nth_name j in
133 (j + 1, ((name, stature_of_thm false [] chained_ths
134 css_table name th), th) :: rest)
139 (* Reject theorems with names like "List.filter.filter_list_def" or
140 "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
141 fun is_package_def a =
142 let val names = Long_Name.explode a in
143 (length names > 2 andalso not (hd names = "local") andalso
144 String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
147 (* FIXME: put other record thms here, or declare as "no_atp" *)
148 fun multi_base_blacklist ctxt ho_atp =
149 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
150 "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
152 |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
153 append ["induct", "inducts"]
156 val max_lambda_nesting = 3 (*only applies if not ho_atp*)
158 fun term_has_too_many_lambdas max (t1 $ t2) =
159 exists (term_has_too_many_lambdas max) [t1, t2]
160 | term_has_too_many_lambdas max (Abs (_, _, t)) =
161 max = 0 orelse term_has_too_many_lambdas (max - 1) t
162 | term_has_too_many_lambdas _ _ = false
164 (* Don't count nested lambdas at the level of formulas, since they are
166 fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
167 | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
168 formula_has_too_many_lambdas false (T :: Ts) t
169 | formula_has_too_many_lambdas _ Ts t =
170 if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
171 exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
173 term_has_too_many_lambdas max_lambda_nesting t
175 (* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
177 val max_apply_depth = 15
179 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
180 | apply_depth (Abs (_, _, t)) = apply_depth t
183 fun is_formula_too_complex ho_atp t =
184 apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
186 (* FIXME: Extend to "Meson" and "Metis" *)
187 val exists_sledgehammer_const =
188 exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
190 (* FIXME: make more reliable *)
191 val exists_low_level_class_const =
192 exists_Const (fn (s, _) =>
193 s = @{const_name equal_class.equal} orelse
194 String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
196 fun is_metastrange_theorem th =
197 case head_of (concl_of th) of
198 Const (s, _) => (s <> @{const_name Trueprop} andalso
199 s <> @{const_name "=="})
202 fun is_that_fact th =
203 String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
204 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
205 | _ => false) (prop_of th)
207 fun is_theorem_bad_for_atps ho_atp thm =
208 is_metastrange_theorem thm orelse
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 clasimpset_rule_table_of ctxt =
245 val thy = Proof_Context.theory_of ctxt
246 val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
247 fun add stature normalizers get_th =
250 val th = rule |> get_th
252 th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
254 fold (fn normalize => Termtab.update (normalize t, stature))
257 val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
258 ctxt |> claset_of |> Classical.rep_cs
259 val intros = Item_Net.content safeIs @ Item_Net.content hazIs
260 (* Add once it is used:
262 Item_Net.content safeEs @ Item_Net.content hazEs
263 |> map Classical.classical_rule
265 val simps = ctxt |> simpset_of |> dest_ss |> #simps
266 val specs = ctxt |> Spec_Rules.get
267 val (rec_defs, nonrec_defs) =
268 specs |> filter (curry (op =) Spec_Rules.Equational o fst)
270 |> filter_out (member Thm.eq_thm_prop risky_defs)
271 |> List.partition (is_rec_def o prop_of)
273 specs |> filter (member (op =) [Spec_Rules.Inductive,
274 Spec_Rules.Co_Inductive] o fst)
277 Termtab.empty |> add Simp [atomize] snd simps
278 |> add Simp [] I rec_defs
279 |> add Def [] I nonrec_defs
280 (* Add once it is used:
281 |> add Elim [] I elims
283 |> add Intro [] I intros
284 |> add Inductive [] I spec_intros
288 Termtab.fold (cons o snd)
289 (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
291 fun struct_induct_rule_on th =
292 case Logic.strip_horn (prop_of th) of
293 (prems, @{const Trueprop}
294 $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
295 if not (is_TVar ind_T) andalso length prems > 1 andalso
296 exists (exists_subterm (curry (op aconv) p)) prems andalso
297 not (exists (exists_subterm (curry (op aconv) a)) prems) then
303 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
305 fun varify_noninducts (t as Free (s, T)) =
306 if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
307 | varify_noninducts t = t
309 concl_prop |> map_aterms varify_noninducts |> close_form
310 |> lambda (Free ind_x)
311 |> hackish_string_for_term ctxt
313 ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
314 stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
317 fun type_match thy (T1, T2) =
318 (Sign.typ_match thy (T2, T1) Vartab.empty; true)
319 handle Type.TYPE_MATCH => false
321 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
322 case struct_induct_rule_on th of
323 SOME (p_name, ind_T) =>
324 let val thy = Proof_Context.theory_of ctxt in
325 stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
326 |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
330 fun external_frees t =
331 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
333 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
334 if Config.get ctxt instantiate_inducts then
336 val thy = Proof_Context.theory_of ctxt
338 (hyp_ts |> filter_out (null o external_frees), concl_t)
339 |> Logic.list_implies |> Object_Logic.atomize_term thy
340 val ind_stmt_xs = external_frees ind_stmt
341 in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
345 fun maybe_filter_no_atps ctxt =
346 not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
348 fun all_facts ctxt ho_atp reserved add_ths chained_ths css_table =
350 val thy = Proof_Context.theory_of ctxt
351 val global_facts = Global_Theory.facts_of thy
352 val local_facts = Proof_Context.facts_of ctxt
353 val named_locals = local_facts |> Facts.dest_static []
354 val assms = Assumption.all_assms_of ctxt
355 fun is_good_unnamed_local th =
356 not (Thm.has_name_hint th) andalso
357 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
359 union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
360 |> filter is_good_unnamed_local |> map (pair "" o single)
362 Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
363 fun add_facts global foldx facts =
364 foldx (fn (name0, ths) =>
365 if name0 <> "" andalso
366 forall (not o member Thm.eq_thm_prop add_ths) ths andalso
367 (Facts.is_concealed facts name0 orelse
368 not (can (Proof_Context.get_thms ctxt) name0) orelse
369 (not (Config.get ctxt ignore_no_atp) andalso
370 is_package_def name0) orelse
371 exists (fn s => String.isSuffix s name0)
372 (multi_base_blacklist ctxt ho_atp)) then
376 val multi = length ths > 1
378 backquote o hackish_string_for_term ctxt o close_form o prop_of
380 case try (Proof_Context.get_thms ctxt) a of
382 | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
385 #> fold (fn th => fn (j, (multis, unis)) =>
387 if not (member Thm.eq_thm_prop add_ths th) andalso
388 is_theorem_bad_for_atps ho_atp th then
397 [Facts.extern ctxt facts name0,
398 Name_Space.extern ctxt full_space name0]
399 |> find_first check_thms
401 |> make_name reserved multi j),
402 stature_of_thm global assms chained_ths
403 css_table name0 th), th)
405 if multi then (new :: multis, unis)
406 else (multis, new :: unis)
411 (* The single-name theorems go after the multiple-name ones, so that single
412 names are preferred when both are available. *)
413 ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
414 |> add_facts true Facts.fold_static global_facts global_facts
418 fun all_facts_of thy css_table =
419 let val ctxt = Proof_Context.init_global thy in
420 all_facts ctxt false Symtab.empty [] [] css_table
421 |> rev (* try to restore the original order of facts, for MaSh *)
424 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
426 if only andalso null add then
432 |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
435 maps (map (fn ((name, stature), th) => ((K name, stature), th))
436 o fact_from_ref ctxt reserved chained_ths css_table) add
438 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
439 all_facts ctxt ho_atp reserved add chained_ths css_table
440 |> filter_out (member Thm.eq_thm_prop del o snd)
441 |> maybe_filter_no_atps ctxt
444 |> maybe_instantiate_inducts ctxt hyp_ts concl_t