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