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