src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author blanchet
Tue Oct 15 15:26:58 2013 +0200 (2013-10-15 ago)
changeset 54112 9c0f464d1854
parent 54092 1e2585f56509
child 54142 5f3c1b445253
permissions -rw-r--r--
drop only real duplicates, not subsumed facts -- this confuses MaSh
     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   val drop_duplicate_facts: theory -> raw_fact list -> raw_fact list
    43 end;
    44 
    45 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    46 struct
    47 
    48 open ATP_Util
    49 open ATP_Problem_Generate
    50 open Metis_Tactic
    51 open Sledgehammer_Util
    52 
    53 type raw_fact = ((unit -> string) * stature) * thm
    54 type fact = (string * stature) * thm
    55 
    56 type fact_override =
    57   {add : (Facts.ref * Attrib.src list) list,
    58    del : (Facts.ref * Attrib.src list) list,
    59    only : bool}
    60 
    61 (* gracefully handle huge background theories *)
    62 val max_facts_for_duplicates = 50000
    63 val max_facts_for_duplicate_matching = 25000
    64 val max_facts_for_complex_check = 25000
    65 val max_simps_for_clasimpset = 10000
    66 
    67 (* experimental feature *)
    68 val instantiate_inducts =
    69   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    70 
    71 val no_fact_override = {add = [], del = [], only = false}
    72 
    73 fun needs_quoting reserved s =
    74   Symtab.defined reserved s orelse
    75   exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
    76 
    77 fun make_name reserved multi j name =
    78   (name |> needs_quoting reserved name ? quote) ^
    79   (if multi then "(" ^ string_of_int j ^ ")" else "")
    80 
    81 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    82   | explode_interval max (Facts.From i) = i upto i + max - 1
    83   | explode_interval _ (Facts.Single i) = [i]
    84 
    85 val backquote =
    86   raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
    87 
    88 (* unfolding these can yield really huge terms *)
    89 val risky_defs = @{thms Bit0_def Bit1_def}
    90 
    91 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    92 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    93   | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    94   | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    95   | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    96   | is_rec_def _ = false
    97 
    98 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
    99 fun is_chained chained = member Thm.eq_thm_prop chained
   100 
   101 fun scope_of_thm global assms chained th =
   102   if is_chained chained th then Chained
   103   else if global then Global
   104   else if is_assum assms th then Assum
   105   else Local
   106 
   107 val may_be_induction =
   108   exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   109                      body_type T = @{typ bool}
   110                    | _ => false)
   111 
   112 (* TODO: get rid of *)
   113 fun normalize_vars t =
   114   let
   115     fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
   116       | normT (TVar (z as (_, S))) =
   117         (fn ((knownT, nT), accum) =>
   118             case find_index (equal z) knownT of
   119               ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
   120             | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
   121       | normT (T as TFree _) = pair T
   122     fun norm (t $ u) = norm t ##>> norm u #>> op $
   123       | norm (Const (s, T)) = normT T #>> curry Const s
   124       | norm (Var (z as (_, T))) =
   125         normT T
   126         #> (fn (T, (accumT, (known, n))) =>
   127                case find_index (equal z) known of
   128                  ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
   129                | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
   130       | norm (Abs (_, T, t)) =
   131         norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
   132       | norm (Bound j) = pair (Bound j)
   133       | norm (Free (s, T)) = normT T #>> curry Free s
   134   in fst (norm t (([], 0), ([], 0))) end
   135 
   136 fun status_of_thm css name th =
   137   if Termtab.is_empty css then
   138     General
   139   else
   140     let val t = prop_of th in
   141       (* FIXME: use structured name *)
   142       if String.isSubstring ".induct" name andalso may_be_induction t then
   143         Induction
   144       else
   145         let val t = normalize_vars t in
   146           case Termtab.lookup css t of
   147             SOME status => status
   148           | NONE =>
   149             let val concl = Logic.strip_imp_concl t in
   150               case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
   151                 SOME lrhss =>
   152                 let
   153                   val prems = Logic.strip_imp_prems t
   154                   val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
   155                 in
   156                   Termtab.lookup css t' |> the_default General
   157                 end
   158               | NONE => General
   159             end
   160         end
   161     end
   162 
   163 fun stature_of_thm global assms chained css name th =
   164   (scope_of_thm global assms chained th, status_of_thm css name th)
   165 
   166 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
   167   let
   168     val ths = Attrib.eval_thms ctxt [xthm]
   169     val bracket =
   170       map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   171       |> implode
   172     fun nth_name j =
   173       case xref of
   174         Facts.Fact s => backquote s ^ bracket
   175       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   176       | Facts.Named ((name, _), NONE) =>
   177         make_name reserved (length ths > 1) (j + 1) name ^ bracket
   178       | Facts.Named ((name, _), SOME intervals) =>
   179         make_name reserved true
   180                  (nth (maps (explode_interval (length ths)) intervals) j) name ^
   181         bracket
   182     fun add_nth th (j, rest) =
   183       let val name = nth_name j in
   184         (j + 1, ((name, stature_of_thm false [] chained css name th), th)
   185                 :: rest)
   186       end
   187   in (0, []) |> fold add_nth ths |> snd end
   188 
   189 (* Reject theorems with names like "List.filter.filter_list_def" or
   190   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
   191 fun is_package_def s =
   192   let val ss = Long_Name.explode s in
   193     length ss > 2 andalso not (hd ss = "local") andalso
   194     exists (fn suf => String.isSuffix suf s)
   195            ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
   196   end
   197 
   198 (* FIXME: put other record thms here, or declare as "no_atp" *)
   199 fun multi_base_blacklist ctxt ho_atp =
   200   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
   201    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
   202    "weak_case_cong", "nat_of_char_simps", "nibble.simps",
   203    "nibble.distinct"]
   204   |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ?
   205         append ["induct", "inducts"]
   206   |> map (prefix Long_Name.separator)
   207 
   208 (* The maximum apply depth of any "metis" call in "Metis_Examples" (on
   209    2007-10-31) was 11. *)
   210 val max_apply_depth = 18
   211 
   212 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   213   | apply_depth (Abs (_, _, t)) = apply_depth t
   214   | apply_depth _ = 0
   215 
   216 fun is_too_complex t = apply_depth t > max_apply_depth
   217 
   218 (* FIXME: Ad hoc list *)
   219 val technical_prefixes =
   220   ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
   221    "Limited_Sequence", "Meson", "Metis", "Nitpick",
   222    "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
   223    "Random_Sequence", "Sledgehammer", "SMT"]
   224   |> map (suffix Long_Name.separator)
   225 
   226 fun is_technical_const (s, _) =
   227   exists (fn pref => String.isPrefix pref s) technical_prefixes
   228 
   229 (* FIXME: make more reliable *)
   230 val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
   231 fun is_low_level_class_const (s, _) =
   232   s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
   233 
   234 val sep_that = Long_Name.separator ^ Obtain.thatN
   235 
   236 val skolem_thesis = Name.skolem Auto_Bind.thesisN
   237 
   238 fun is_that_fact th =
   239   exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (prop_of th)
   240   andalso String.isSuffix sep_that (Thm.get_name_hint th)
   241 
   242 datatype interest = Deal_Breaker | Interesting | Boring
   243 
   244 fun combine_interests Deal_Breaker _ = Deal_Breaker
   245   | combine_interests _ Deal_Breaker = Deal_Breaker
   246   | combine_interests Interesting _ = Interesting
   247   | combine_interests _ Interesting = Interesting
   248   | combine_interests Boring Boring = Boring
   249 
   250 fun is_likely_tautology_too_meta_or_too_technical th =
   251   let
   252     fun is_interesting_subterm (Const (s, _)) =
   253         not (member (op =) atp_widely_irrelevant_consts s)
   254       | is_interesting_subterm (Free _) = true
   255       | is_interesting_subterm _ = false
   256     fun interest_of_bool t =
   257       if exists_Const (is_technical_const orf is_low_level_class_const orf
   258                        type_has_top_sort o snd) t then
   259         Deal_Breaker
   260       else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse
   261               not (exists_subterm is_interesting_subterm t) then
   262         Boring
   263       else
   264         Interesting
   265     fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t
   266       | interest_of_prop Ts (@{const "==>"} $ t $ u) =
   267         combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
   268       | interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   269         if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
   270       | interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   271         interest_of_prop Ts (t $ eta_expand Ts u 1)
   272       | interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   273         combine_interests (interest_of_bool t) (interest_of_bool u)
   274       | interest_of_prop _ _ = Deal_Breaker
   275     val t = prop_of th
   276   in
   277     (interest_of_prop [] t <> Interesting andalso
   278      not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
   279     is_that_fact th
   280   end
   281 
   282 fun is_blacklisted_or_something ctxt ho_atp =
   283   let
   284     val blist = multi_base_blacklist ctxt ho_atp
   285     fun is_blisted name =
   286       is_package_def name orelse exists (fn s => String.isSuffix s name) blist
   287   in is_blisted end
   288 
   289 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   290    they are displayed as "M" and we want to avoid clashes with these. But
   291    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   292    prefixes of all free variables. In the worse case scenario, where the fact
   293    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   294    name to the offending fact. *)
   295 fun all_prefixes_of s =
   296   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   297 
   298 fun close_form t =
   299   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   300   |> fold (fn ((s, i), T) => fn (t', taken) =>
   301               let val s' = singleton (Name.variant_list taken) s in
   302                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   303                   else Logic.all_const) T
   304                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   305                  s' :: taken)
   306               end)
   307           (Term.add_vars t [] |> sort_wrt (fst o fst))
   308   |> fst
   309 
   310 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
   311 fun backquote_thm ctxt = backquote_term ctxt o prop_of
   312 
   313 (* TODO: rewrite to use nets and/or to reuse existing data structures *)
   314 fun clasimpset_rule_table_of ctxt =
   315   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
   316     if length simps >= max_simps_for_clasimpset then
   317       Termtab.empty
   318     else
   319       let
   320         fun add stature th =
   321           Termtab.update (normalize_vars (prop_of th), stature)
   322         val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   323           ctxt |> claset_of |> Classical.rep_cs
   324         val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   325 (* Add once it is used:
   326         val elims =
   327           Item_Net.content safeEs @ Item_Net.content hazEs
   328           |> map Classical.classical_rule
   329 *)
   330         val specs = ctxt |> Spec_Rules.get
   331         val (rec_defs, nonrec_defs) =
   332           specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   333                 |> maps (snd o snd)
   334                 |> filter_out (member Thm.eq_thm_prop risky_defs)
   335                 |> List.partition (is_rec_def o prop_of)
   336         val spec_intros =
   337           specs |> filter (member (op =) [Spec_Rules.Inductive,
   338                                           Spec_Rules.Co_Inductive] o fst)
   339                 |> maps (snd o snd)
   340       in
   341         Termtab.empty |> fold (add Simp o snd) simps
   342                       |> fold (add Rec_Def) rec_defs
   343                       |> fold (add Non_Rec_Def) nonrec_defs
   344 (* Add once it is used:
   345                       |> fold (add Elim) elims
   346 *)
   347                       |> fold (add Intro) intros
   348                       |> fold (add Inductive) spec_intros
   349       end
   350   end
   351 
   352 fun normalize_eq (@{const Trueprop} $ (t as (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   353     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else t0 $ t2 $ t1
   354   | normalize_eq (@{const Trueprop} $ (t as @{const Not}
   355         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   356     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1)
   357   | normalize_eq (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
   358     (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
   359     |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)
   360   | normalize_eq t = t
   361 
   362 fun if_thm_before th th' =
   363   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   364 
   365 (* Hack: Conflate the facts about a class as seen from the outside with the
   366    corresponding low-level facts, so that MaSh can learn from the low-level
   367    proofs. *)
   368 fun un_class_ify s =
   369   case first_field "_class" s of
   370     SOME (pref, suf) => [s, pref ^ suf]
   371   | NONE => [s]
   372 
   373 fun build_name_tables name_of facts =
   374   let
   375     fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (prop_of th)), th)
   376     fun add_plain canon alias =
   377       Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias))
   378     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
   379     fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name)
   380     val prop_tab = fold cons_thm facts Termtab.empty
   381     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
   382     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   383   in (plain_name_tab, inclass_name_tab) end
   384 
   385 fun fact_distinct eq facts =
   386   fold (fn fact as (_, th) =>
   387       Net.insert_term_safe (eq o pairself (normalize_eq o prop_of o snd))
   388         (normalize_eq (prop_of th), fact))
   389     facts Net.empty
   390   |> Net.entries
   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 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) => fn accum =>
   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           accum
   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             snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_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                              |> find_first check_thms
   507                              |> the_default name0
   508                              |> make_name reserved multi j),
   509                         stature_of_thm global assms chained css name0 th),
   510                       th)
   511                  in
   512                    if multi then (uni_accum, new :: multi_accum)
   513                    else (new :: uni_accum, multi_accum)
   514                  end)) ths (n, accum))
   515           end)
   516   in
   517     (* The single-theorem names go before the multiple-theorem ones (e.g.,
   518        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
   519        available. *)
   520     `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   521           |> add_facts true Facts.fold_static global_facts global_facts
   522           |> op @
   523   end
   524 
   525 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   526                      concl_t =
   527   if only andalso null add then
   528     []
   529   else
   530     let
   531       val thy = Proof_Context.theory_of ctxt
   532       val chained =
   533         chained
   534         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   535     in
   536       (if only then
   537          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   538                o fact_of_ref ctxt reserved chained css) add
   539        else
   540         (* The "fact_distinct" call would have cleaner semantics if it called "Pattern.equiv"
   541            instead of "Pattern.matches", but it would also be slower and less precise.
   542            "Pattern.matches" throws out theorems that are strict instances of other theorems, but
   543            only if the instance is met after the general version. *)
   544          let
   545            val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
   546            val facts =
   547              all_facts ctxt false ho_atp reserved add chained css
   548              |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
   549          in
   550            facts
   551          end)
   552       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   553     end
   554 
   555 fun drop_duplicate_facts thy facts =
   556   let val num_facts = length facts in
   557     facts |> num_facts <= max_facts_for_duplicates
   558       ? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv
   559           else Pattern.matches thy o swap)
   560   end
   561 
   562 end;