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