src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author blanchet
Wed Sep 11 18:37:47 2013 +0200 (2013-09-11 ago)
changeset 53545 f7e987ef7304
parent 53533 24ce26e8af12
child 53815 e8aa538e959e
permissions -rw-r--r--
reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
     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         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 fun hackish_string_of_term ctxt =
   275   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   276 
   277 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   278    they are displayed as "M" and we want to avoid clashes with these. But
   279    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   280    prefixes of all free variables. In the worse case scenario, where the fact
   281    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   282    name to the offending fact. *)
   283 fun all_prefixes_of s =
   284   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   285 
   286 fun close_form t =
   287   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   288   |> fold (fn ((s, i), T) => fn (t', taken) =>
   289               let val s' = singleton (Name.variant_list taken) s in
   290                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   291                   else Logic.all_const) T
   292                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   293                  s' :: taken)
   294               end)
   295           (Term.add_vars t [] |> sort_wrt (fst o fst))
   296   |> fst
   297 
   298 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
   299 fun backquote_thm ctxt = backquote_term ctxt o prop_of
   300 
   301 (* gracefully handle huge background theories *)
   302 val max_simps_for_clasimpset = 10000
   303 
   304 fun clasimpset_rule_table_of ctxt =
   305   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
   306     if length simps >= max_simps_for_clasimpset then
   307       Termtab.empty
   308     else
   309       let
   310         fun add stature th =
   311           Termtab.update (normalize_vars (prop_of th), stature)
   312         val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   313           ctxt |> claset_of |> Classical.rep_cs
   314         val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   315 (* Add once it is used:
   316         val elims =
   317           Item_Net.content safeEs @ Item_Net.content hazEs
   318           |> map Classical.classical_rule
   319 *)
   320         val specs = ctxt |> Spec_Rules.get
   321         val (rec_defs, nonrec_defs) =
   322           specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   323                 |> maps (snd o snd)
   324                 |> filter_out (member Thm.eq_thm_prop risky_defs)
   325                 |> List.partition (is_rec_def o prop_of)
   326         val spec_intros =
   327           specs |> filter (member (op =) [Spec_Rules.Inductive,
   328                                           Spec_Rules.Co_Inductive] o fst)
   329                 |> maps (snd o snd)
   330       in
   331         Termtab.empty |> fold (add Simp o snd) simps
   332                       |> fold (add Rec_Def) rec_defs
   333                       |> fold (add Non_Rec_Def) nonrec_defs
   334 (* Add once it is used:
   335                       |> fold (add Elim) elims
   336 *)
   337                       |> fold (add Intro) intros
   338                       |> fold (add Inductive) spec_intros
   339       end
   340   end
   341 
   342 fun normalize_eq (t as @{const Trueprop}
   343         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   344     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   345     else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
   346   | normalize_eq (t as @{const Trueprop} $ (@{const Not}
   347         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   348     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   349     else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
   350   | normalize_eq t = t
   351 
   352 val normalize_eq_vars = normalize_eq #> normalize_vars
   353 
   354 fun if_thm_before th th' =
   355   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   356 
   357 (* Hack: Conflate the facts about a class as seen from the outside with the
   358    corresponding low-level facts, so that MaSh can learn from the low-level
   359    proofs. *)
   360 fun un_class_ify s =
   361   case first_field "_class" s of
   362     SOME (pref, suf) => [s, pref ^ suf]
   363   | NONE => [s]
   364 
   365 fun build_name_tables name_of facts =
   366   let
   367     fun cons_thm (_, th) =
   368       Termtab.cons_list (normalize_eq_vars (prop_of th), th)
   369     fun add_plain canon alias =
   370       Symtab.update (Thm.get_name_hint alias,
   371                      name_of (if_thm_before canon alias))
   372     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
   373     fun add_inclass (name, target) =
   374       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
   375     val prop_tab = fold cons_thm facts Termtab.empty
   376     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
   377     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   378   in (plain_name_tab, inclass_name_tab) end
   379 
   380 fun keyed_distinct key_of xs =
   381   let val tab = fold (Termtab.default o `key_of) xs Termtab.empty in
   382     Termtab.fold (cons o snd) tab []
   383   end
   384 
   385 fun hashed_keyed_distinct hash_of key_of xs =
   386   let
   387     val ys = map (`hash_of) xs
   388     val sorted_ys = sort (int_ord o pairself fst) ys
   389     val grouped_ys = AList.coalesce (op =) sorted_ys
   390   in maps (keyed_distinct key_of o snd) grouped_ys end
   391 
   392 fun struct_induct_rule_on th =
   393   case Logic.strip_horn (prop_of th) of
   394     (prems, @{const Trueprop}
   395             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
   396     if not (is_TVar ind_T) andalso length prems > 1 andalso
   397        exists (exists_subterm (curry (op aconv) p)) prems andalso
   398        not (exists (exists_subterm (curry (op aconv) a)) prems) then
   399       SOME (p_name, ind_T)
   400     else
   401       NONE
   402   | _ => NONE
   403 
   404 val instantiate_induct_timeout = seconds 0.01
   405 
   406 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   407   let
   408     fun varify_noninducts (t as Free (s, T)) =
   409         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
   410       | varify_noninducts t = t
   411     val p_inst =
   412       concl_prop |> map_aterms varify_noninducts |> close_form
   413                  |> lambda (Free ind_x)
   414                  |> hackish_string_of_term ctxt
   415   in
   416     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   417       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
   418   end
   419 
   420 fun type_match thy (T1, T2) =
   421   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   422   handle Type.TYPE_MATCH => false
   423 
   424 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   425   case struct_induct_rule_on th of
   426     SOME (p_name, ind_T) =>
   427     let val thy = Proof_Context.theory_of ctxt in
   428       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   429               |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   430                      (instantiate_induct_rule ctxt stmt p_name ax)))
   431     end
   432   | NONE => [ax]
   433 
   434 fun external_frees t =
   435   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   436 
   437 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   438   if Config.get ctxt instantiate_inducts then
   439     let
   440       val thy = Proof_Context.theory_of ctxt
   441       val ind_stmt =
   442         (hyp_ts |> filter_out (null o external_frees), concl_t)
   443         |> Logic.list_implies |> Object_Logic.atomize_term thy
   444       val ind_stmt_xs = external_frees ind_stmt
   445     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   446   else
   447     I
   448 
   449 fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
   450 
   451 fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
   452 
   453 (* gracefully handle huge background theories *)
   454 val max_facts_for_complex_check = 25000
   455 
   456 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   457   let
   458     val thy = Proof_Context.theory_of ctxt
   459     val global_facts = Global_Theory.facts_of thy
   460     val is_too_complex =
   461       if generous orelse
   462          fact_count global_facts >= max_facts_for_complex_check then
   463         K false
   464       else
   465         is_too_complex
   466     val local_facts = Proof_Context.facts_of ctxt
   467     val named_locals = local_facts |> Facts.dest_static []
   468     val assms = Assumption.all_assms_of ctxt
   469     fun is_good_unnamed_local th =
   470       not (Thm.has_name_hint th) andalso
   471       forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   472     val unnamed_locals =
   473       union Thm.eq_thm_prop (Facts.props local_facts) chained
   474       |> filter is_good_unnamed_local |> map (pair "" o single)
   475     val full_space =
   476       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   477     val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
   478     fun add_facts global foldx facts =
   479       foldx (fn (name0, ths) =>
   480         if name0 <> "" andalso
   481            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   482            (Facts.is_concealed facts name0 orelse
   483             (not generous andalso is_blacklisted_or_something name0)) then
   484           I
   485         else
   486           let
   487             val n = length ths
   488             val multi = n > 1
   489             fun check_thms a =
   490               case try (Proof_Context.get_thms ctxt) a of
   491                 NONE => false
   492               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   493           in
   494             pair n
   495             #> fold_rev (fn th => fn (j, accum) =>
   496                    (j - 1,
   497                     if not (member Thm.eq_thm_prop add_ths th) andalso
   498                        (is_likely_tautology_too_meta_or_too_technical th orelse
   499                         is_too_complex (prop_of th)) then
   500                       accum
   501                     else
   502                       let
   503                         val new =
   504                           (((fn () =>
   505                                 if name0 = "" then
   506                                   backquote_thm ctxt th
   507                                 else
   508                                   [Facts.extern ctxt facts name0,
   509                                    Name_Space.extern ctxt full_space name0]
   510                                   |> distinct (op =)
   511                                   |> find_first check_thms
   512                                   |> the_default name0
   513                                   |> make_name reserved multi j),
   514                              stature_of_thm global assms chained css name0 th),
   515                            th)
   516                       in
   517                         accum |> (if multi then apsnd else apfst) (cons new)
   518                       end)) ths
   519             #> snd
   520           end)
   521   in
   522     (* The single-theorem names go before the multiple-theorem ones (e.g.,
   523        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
   524        available. *)
   525     `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   526           |> add_facts true Facts.fold_static global_facts global_facts
   527           |> op @
   528   end
   529 
   530 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   531                      concl_t =
   532   if only andalso null add then
   533     []
   534   else
   535     let
   536       val chained =
   537         chained
   538         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   539     in
   540       (if only then
   541          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   542                o fact_of_ref ctxt reserved chained css) add
   543        else
   544          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   545            all_facts ctxt false ho_atp reserved add chained css
   546            |> filter_out
   547                   ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
   548            |> hashed_keyed_distinct (size_of_term o prop_of o snd)
   549                   (normalize_eq_vars o prop_of o snd)
   550          end)
   551       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   552     end
   553 
   554 end;