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