src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author blanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 53503 d2f21e305d0c
parent 53502 2eaaca796234
child 53504 9750618c32ed
permissions -rw-r--r--
stronger fact normalization
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Sledgehammer fact handling.
     6 *)
     7 
     8 signature SLEDGEHAMMER_FACT =
     9 sig
    10   type status = ATP_Problem_Generate.status
    11   type stature = ATP_Problem_Generate.stature
    12 
    13   type raw_fact = ((unit -> string) * stature) * thm
    14   type fact = (string * stature) * thm
    15 
    16   type fact_override =
    17     {add : (Facts.ref * Attrib.src list) list,
    18      del : (Facts.ref * Attrib.src list) list,
    19      only : bool}
    20 
    21   val ignore_no_atp : bool Config.T
    22   val instantiate_inducts : bool Config.T
    23   val no_fact_override : fact_override
    24   val fact_of_ref :
    25     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    26     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    27   val backquote_thm : Proof.context -> thm -> string
    28   val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
    29   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    30   val build_name_tables :
    31     (thm -> string) -> ('a * thm) list
    32     -> string Symtab.table * string Symtab.table
    33   val maybe_instantiate_inducts :
    34     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    35     -> (((unit -> string) * 'a) * thm) list
    36   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    37   val fact_of_raw_fact : raw_fact -> fact
    38   val all_facts :
    39     Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
    40     -> status Termtab.table -> raw_fact list
    41   val nearly_all_facts :
    42     Proof.context -> bool -> fact_override -> unit Symtab.table
    43     -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
    44 end;
    45 
    46 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    47 struct
    48 
    49 open ATP_Util
    50 open ATP_Problem_Generate
    51 open Metis_Tactic
    52 open Sledgehammer_Util
    53 
    54 type raw_fact = ((unit -> string) * stature) * thm
    55 type fact = (string * stature) * thm
    56 
    57 type fact_override =
    58   {add : (Facts.ref * Attrib.src list) list,
    59    del : (Facts.ref * Attrib.src list) list,
    60    only : bool}
    61 
    62 (* experimental features *)
    63 val ignore_no_atp =
    64   Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
    65 val instantiate_inducts =
    66   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    67 
    68 val no_fact_override = {add = [], del = [], only = false}
    69 
    70 fun needs_quoting reserved s =
    71   Symtab.defined reserved s orelse
    72   exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
    73 
    74 fun make_name reserved multi j name =
    75   (name |> needs_quoting reserved name ? quote) ^
    76   (if multi then "(" ^ string_of_int j ^ ")" else "")
    77 
    78 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    79   | explode_interval max (Facts.From i) = i upto i + max - 1
    80   | explode_interval _ (Facts.Single i) = [i]
    81 
    82 val backquote =
    83   raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
    84 
    85 (* unfolding these can yield really huge terms *)
    86 val risky_defs = @{thms Bit0_def Bit1_def}
    87 
    88 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    89 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    90   | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    91   | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    92   | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    93   | is_rec_def _ = false
    94 
    95 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
    96 fun is_chained chained = member Thm.eq_thm_prop chained
    97 
    98 fun scope_of_thm global assms chained th =
    99   if is_chained chained th then Chained
   100   else if global then Global
   101   else if is_assum assms th then Assum
   102   else Local
   103 
   104 val may_be_induction =
   105   exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   106                      body_type T = @{typ bool}
   107                    | _ => false)
   108 
   109 fun normalize_vars t =
   110   let
   111     fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
   112       | normT (TVar (z as (_, S))) =
   113         (fn ((knownT, nT), accum) =>
   114             case find_index (equal z) knownT of
   115               ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
   116             | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
   117       | normT (T as TFree _) = pair T
   118     fun norm (t $ u) = norm t ##>> norm u #>> op $
   119       | norm (Const (s, T)) = normT T #>> curry Const s
   120       | norm (Var (z as (_, T))) =
   121         normT T
   122         #> (fn (T, (accumT, (known, n))) =>
   123                case find_index (equal z) known of
   124                  ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
   125                | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
   126       | norm (Abs (_, T, t)) =
   127         norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
   128       | norm (Bound j) = pair (Bound j)
   129       | norm (Free (s, T)) = normT T #>> curry Free s
   130   in fst (norm t (([], 0), ([], 0))) end
   131 
   132 fun status_of_thm css name th =
   133   let val t = normalize_vars (prop_of th) in
   134     (* FIXME: use structured name *)
   135     if String.isSubstring ".induct" name andalso may_be_induction t then
   136       Induction
   137     else case Termtab.lookup css t of
   138       SOME status => status
   139     | NONE =>
   140       let val concl = Logic.strip_imp_concl t in
   141         case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
   142           SOME lrhss =>
   143           let
   144             val prems = Logic.strip_imp_prems t
   145             val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
   146           in
   147             Termtab.lookup css t' |> the_default General
   148           end
   149         | NONE => General
   150       end
   151   end
   152 
   153 fun stature_of_thm global assms chained css name th =
   154   (scope_of_thm global assms chained th, status_of_thm css name th)
   155 
   156 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
   157   let
   158     val ths = Attrib.eval_thms ctxt [xthm]
   159     val bracket =
   160       map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   161       |> implode
   162     fun nth_name j =
   163       case xref of
   164         Facts.Fact s => backquote s ^ bracket
   165       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   166       | Facts.Named ((name, _), NONE) =>
   167         make_name reserved (length ths > 1) (j + 1) name ^ bracket
   168       | Facts.Named ((name, _), SOME intervals) =>
   169         make_name reserved true
   170                  (nth (maps (explode_interval (length ths)) intervals) j) name ^
   171         bracket
   172     fun add_nth th (j, rest) =
   173       let val name = nth_name j in
   174         (j + 1, ((name, stature_of_thm false [] chained css name th), th)
   175                 :: rest)
   176       end
   177   in (0, []) |> fold add_nth ths |> snd end
   178 
   179 (* Reject theorems with names like "List.filter.filter_list_def" or
   180   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
   181 fun is_package_def s =
   182   let val ss = Long_Name.explode s in
   183     length ss > 2 andalso not (hd ss = "local") andalso
   184     exists (fn suf => String.isSuffix suf s)
   185            ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
   186   end
   187 
   188 (* FIXME: put other record thms here, or declare as "no_atp" *)
   189 fun multi_base_blacklist ctxt ho_atp =
   190   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
   191    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
   192    "weak_case_cong", "nat_of_char_simps", "nibble.simps",
   193    "nibble.distinct"]
   194   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
   195         append ["induct", "inducts"]
   196   |> map (prefix Long_Name.separator)
   197 
   198 val max_lambda_nesting = 5 (*only applies if not ho_atp*)
   199 
   200 fun term_has_too_many_lambdas max (t1 $ t2) =
   201     exists (term_has_too_many_lambdas max) [t1, t2]
   202   | term_has_too_many_lambdas max (Abs (_, _, t)) =
   203     max = 0 orelse term_has_too_many_lambdas (max - 1) t
   204   | term_has_too_many_lambdas _ _ = false
   205 
   206 (* Don't count nested lambdas at the level of formulas, since they are
   207    quantifiers. *)
   208 fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
   209     formula_has_too_many_lambdas (T :: Ts) t
   210   | formula_has_too_many_lambdas Ts t =
   211     if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
   212       exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
   213     else
   214       term_has_too_many_lambdas max_lambda_nesting t
   215 
   216 (* The maximum apply depth of any "metis" call in "Metis_Examples" (on
   217    2007-10-31) was 11. *)
   218 val max_apply_depth = 18
   219 
   220 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   221   | apply_depth (Abs (_, _, t)) = apply_depth t
   222   | apply_depth _ = 0
   223 
   224 fun is_too_complex ho_atp t =
   225   apply_depth t > max_apply_depth orelse
   226   (not ho_atp andalso formula_has_too_many_lambdas [] t)
   227 
   228 (* FIXME: Ad hoc list *)
   229 val technical_prefixes =
   230   ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
   231    "Limited_Sequence", "Meson", "Metis", "Nitpick",
   232    "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
   233    "Random_Sequence", "Sledgehammer", "SMT"]
   234   |> map (suffix Long_Name.separator)
   235 
   236 fun has_technical_prefix s =
   237   exists (fn pref => String.isPrefix pref s) technical_prefixes
   238 val exists_technical_const = exists_Const (has_technical_prefix o fst)
   239 
   240 (* FIXME: make more reliable *)
   241 val exists_low_level_class_const =
   242   exists_Const (fn (s, _) =>
   243      s = @{const_name equal_class.equal} orelse
   244      String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
   245 
   246 fun is_that_fact th =
   247   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
   248   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
   249                            | _ => false) (prop_of th)
   250 
   251 fun is_likely_tautology_too_meta_or_too_technical th =
   252   let
   253     fun is_interesting_subterm (Const (s, _)) =
   254         not (member (op =) atp_widely_irrelevant_consts s)
   255       | is_interesting_subterm (Free _) = true
   256       | is_interesting_subterm _ = false
   257     fun is_boring_bool t =
   258       not (exists_subterm is_interesting_subterm t) orelse
   259       exists_type (exists_subtype (curry (op =) @{typ prop})) t
   260     fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
   261       | is_boring_prop Ts (@{const "==>"} $ t $ u) =
   262         is_boring_prop Ts t andalso is_boring_prop Ts u
   263       | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   264         is_boring_prop (T :: Ts) t
   265       | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   266         is_boring_prop Ts (t $ eta_expand Ts u 1)
   267       | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   268         is_boring_bool t andalso is_boring_bool u
   269       | is_boring_prop _ _ = true
   270     val t = prop_of th
   271   in
   272     (is_boring_prop [] (prop_of th) andalso
   273      not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
   274     exists_type type_has_top_sort t orelse exists_technical_const t orelse
   275     exists_low_level_class_const t orelse is_that_fact th
   276   end
   277 
   278 fun is_blacklisted_or_something ctxt ho_atp name =
   279   (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
   280   exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
   281 
   282 fun hackish_string_of_term ctxt =
   283   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   284 
   285 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   286    they are displayed as "M" and we want to avoid clashes with these. But
   287    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   288    prefixes of all free variables. In the worse case scenario, where the fact
   289    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   290    name to the offending fact. *)
   291 fun all_prefixes_of s =
   292   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   293 
   294 fun close_form t =
   295   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   296   |> fold (fn ((s, i), T) => fn (t', taken) =>
   297               let val s' = singleton (Name.variant_list taken) s in
   298                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   299                   else Logic.all_const) T
   300                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   301                  s' :: taken)
   302               end)
   303           (Term.add_vars t [] |> sort_wrt (fst o fst))
   304   |> fst
   305 
   306 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
   307 fun backquote_thm ctxt = backquote_term ctxt o prop_of
   308 
   309 (* gracefully handle huge background theories *)
   310 val max_simps_for_clasimpset = 10000
   311 
   312 fun clasimpset_rule_table_of ctxt =
   313   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
   314     if length simps >= max_simps_for_clasimpset then
   315       Termtab.empty
   316     else
   317       let
   318         fun add stature th =
   319           Termtab.update (normalize_vars (prop_of th), stature)
   320         val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   321           ctxt |> claset_of |> Classical.rep_cs
   322         val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   323 (* Add once it is used:
   324         val elims =
   325           Item_Net.content safeEs @ Item_Net.content hazEs
   326           |> map Classical.classical_rule
   327 *)
   328         val specs = ctxt |> Spec_Rules.get
   329         val (rec_defs, nonrec_defs) =
   330           specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   331                 |> maps (snd o snd)
   332                 |> filter_out (member Thm.eq_thm_prop risky_defs)
   333                 |> List.partition (is_rec_def o prop_of)
   334         val spec_intros =
   335           specs |> filter (member (op =) [Spec_Rules.Inductive,
   336                                           Spec_Rules.Co_Inductive] o fst)
   337                 |> maps (snd o snd)
   338       in
   339         Termtab.empty |> fold (add Simp o snd) simps
   340                       |> fold (add Rec_Def) rec_defs
   341                       |> fold (add Non_Rec_Def) nonrec_defs
   342 (* Add once it is used:
   343                       |> fold (add Elim) elims
   344 *)
   345                       |> fold (add Intro) intros
   346                       |> fold (add Inductive) spec_intros
   347       end
   348   end
   349 
   350 fun normalize_eq (t as @{const Trueprop}
   351         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   352     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   353     else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
   354   | normalize_eq (t as @{const Trueprop} $ (@{const Not}
   355         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   356     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   357     else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
   358   | normalize_eq t = t
   359 
   360 val normalize_eq_vars = normalize_eq #> normalize_vars
   361 
   362 fun if_thm_before th th' =
   363   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   364 
   365 (* Hack: Conflate the facts about a class as seen from the outside with the
   366    corresponding low-level facts, so that MaSh can learn from the low-level
   367    proofs. *)
   368 fun un_class_ify s =
   369   case first_field "_class" s of
   370     SOME (pref, suf) => [s, pref ^ suf]
   371   | NONE => [s]
   372 
   373 fun build_name_tables name_of facts =
   374   let
   375     fun cons_thm (_, th) =
   376       Termtab.cons_list (normalize_eq_vars (prop_of th), th)
   377     fun add_plain canon alias =
   378       Symtab.update (Thm.get_name_hint alias,
   379                      name_of (if_thm_before canon alias))
   380     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
   381     fun add_inclass (name, target) =
   382       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
   383     val prop_tab = fold cons_thm facts Termtab.empty
   384     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
   385     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   386   in (plain_name_tab, inclass_name_tab) end
   387 
   388 fun uniquify facts =
   389   Termtab.fold (cons o snd)
   390       (fold (Termtab.default o `(normalize_eq_vars o prop_of o snd)) facts
   391             Termtab.empty) []
   392 
   393 fun struct_induct_rule_on th =
   394   case Logic.strip_horn (prop_of th) of
   395     (prems, @{const Trueprop}
   396             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
   397     if not (is_TVar ind_T) andalso length prems > 1 andalso
   398        exists (exists_subterm (curry (op aconv) p)) prems andalso
   399        not (exists (exists_subterm (curry (op aconv) a)) prems) then
   400       SOME (p_name, ind_T)
   401     else
   402       NONE
   403   | _ => NONE
   404 
   405 val instantiate_induct_timeout = seconds 0.01
   406 
   407 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   408   let
   409     fun varify_noninducts (t as Free (s, T)) =
   410         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
   411       | varify_noninducts t = t
   412     val p_inst =
   413       concl_prop |> map_aterms varify_noninducts |> close_form
   414                  |> lambda (Free ind_x)
   415                  |> hackish_string_of_term ctxt
   416   in
   417     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   418       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
   419   end
   420 
   421 fun type_match thy (T1, T2) =
   422   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   423   handle Type.TYPE_MATCH => false
   424 
   425 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   426   case struct_induct_rule_on th of
   427     SOME (p_name, ind_T) =>
   428     let val thy = Proof_Context.theory_of ctxt in
   429       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   430               |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   431                      (instantiate_induct_rule ctxt stmt p_name ax)))
   432     end
   433   | NONE => [ax]
   434 
   435 fun external_frees t =
   436   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   437 
   438 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   439   if Config.get ctxt instantiate_inducts then
   440     let
   441       val thy = Proof_Context.theory_of ctxt
   442       val ind_stmt =
   443         (hyp_ts |> filter_out (null o external_frees), concl_t)
   444         |> Logic.list_implies |> Object_Logic.atomize_term thy
   445       val ind_stmt_xs = external_frees ind_stmt
   446     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   447   else
   448     I
   449 
   450 fun maybe_filter_no_atps ctxt =
   451   not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
   452 
   453 fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
   454 
   455 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   456   let
   457     val thy = Proof_Context.theory_of ctxt
   458     val global_facts = Global_Theory.facts_of thy
   459     val local_facts = Proof_Context.facts_of ctxt
   460     val named_locals = local_facts |> Facts.dest_static []
   461     val assms = Assumption.all_assms_of ctxt
   462     fun is_good_unnamed_local th =
   463       not (Thm.has_name_hint th) andalso
   464       forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   465     val unnamed_locals =
   466       union Thm.eq_thm_prop (Facts.props local_facts) chained
   467       |> filter is_good_unnamed_local |> map (pair "" o single)
   468     val full_space =
   469       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   470     fun add_facts global foldx facts =
   471       foldx (fn (name0, ths) =>
   472         if name0 <> "" andalso
   473            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   474            (Facts.is_concealed facts name0 orelse
   475             not (can (Proof_Context.get_thms ctxt) name0) orelse
   476             (not generous andalso
   477              is_blacklisted_or_something ctxt ho_atp name0)) then
   478           I
   479         else
   480           let
   481             val n = length ths
   482             val multi = n > 1
   483             fun check_thms a =
   484               case try (Proof_Context.get_thms ctxt) a of
   485                 NONE => false
   486               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   487           in
   488             pair n
   489             #> fold_rev (fn th => fn (j, accum) =>
   490                    (j - 1,
   491                     if not (member Thm.eq_thm_prop add_ths th) andalso
   492                        (is_likely_tautology_too_meta_or_too_technical th orelse
   493                         (not generous andalso
   494                          is_too_complex ho_atp (prop_of th))) then
   495                       accum
   496                     else
   497                       let
   498                         val new =
   499                           (((fn () =>
   500                                 if name0 = "" then
   501                                   backquote_thm ctxt th
   502                                 else
   503                                   [Facts.extern ctxt facts name0,
   504                                    Name_Space.extern ctxt full_space name0]
   505                                   |> distinct (op =)
   506                                   |> find_first check_thms
   507                                   |> the_default name0
   508                                   |> make_name reserved multi j),
   509                              stature_of_thm global assms chained css name0 th),
   510                            th)
   511                       in
   512                         accum |> (if multi then apsnd else apfst) (cons new)
   513                       end)) ths
   514             #> snd
   515           end)
   516   in
   517     (* The single-theorem names go before the multiple-theorem ones (e.g.,
   518        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
   519        available. *)
   520     `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   521           |> add_facts true Facts.fold_static global_facts global_facts
   522           |> op @
   523   end
   524 
   525 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   526                      concl_t =
   527   if only andalso null add then
   528     []
   529   else
   530     let
   531       val chained =
   532         chained
   533         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   534     in
   535       (if only then
   536          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   537                o fact_of_ref ctxt reserved chained css) add
   538        else
   539          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   540            all_facts ctxt false ho_atp reserved add chained css
   541            |> filter_out (member Thm.eq_thm_prop del o snd)
   542            |> maybe_filter_no_atps ctxt
   543            |> uniquify
   544          end)
   545       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   546     end
   547 
   548 end;