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