src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author haftmann
Thu Feb 14 15:27:10 2013 +0100 (2013-02-14 ago)
changeset 51126 df86080de4cb
parent 51004 5f2788c38127
child 51160 599ff65b85e2
permissions -rw-r--r--
reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck
     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 ignore_no_atp : bool Config.T
    22   val instantiate_inducts : bool Config.T
    23   val no_fact_override : fact_override
    24   val fact_from_ref :
    25     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    26     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    27   val backquote_thm : Proof.context -> thm -> string
    28   val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
    29   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    30   val build_name_tables :
    31     (thm -> string) -> ('a * thm) list
    32     -> string Symtab.table * string Symtab.table
    33   val maybe_instantiate_inducts :
    34     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    35     -> (((unit -> string) * 'a) * thm) list
    36   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    37   val fact_of_raw_fact : raw_fact -> fact
    38   val all_facts :
    39     Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
    40     -> status Termtab.table -> raw_fact list
    41   val nearly_all_facts :
    42     Proof.context -> bool -> fact_override -> unit Symtab.table
    43     -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
    44 end;
    45 
    46 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    47 struct
    48 
    49 open ATP_Util
    50 open ATP_Problem_Generate
    51 open Metis_Tactic
    52 open Sledgehammer_Util
    53 
    54 type raw_fact = ((unit -> string) * stature) * thm
    55 type fact = (string * stature) * thm
    56 
    57 type fact_override =
    58   {add : (Facts.ref * Attrib.src list) list,
    59    del : (Facts.ref * Attrib.src list) list,
    60    only : bool}
    61 
    62 (* experimental features *)
    63 val ignore_no_atp =
    64   Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
    65 val instantiate_inducts =
    66   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    67 
    68 val no_fact_override = {add = [], del = [], only = false}
    69 
    70 fun needs_quoting reserved s =
    71   Symtab.defined reserved s orelse
    72   exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
    73 
    74 fun make_name reserved multi j name =
    75   (name |> needs_quoting reserved name ? quote) ^
    76   (if multi then "(" ^ string_of_int j ^ ")" else "")
    77 
    78 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    79   | explode_interval max (Facts.From i) = i upto i + max - 1
    80   | explode_interval _ (Facts.Single i) = [i]
    81 
    82 val backquote =
    83   raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
    84 
    85 (* unfolding these can yield really huge terms *)
    86 val risky_defs = @{thms Bit0_def Bit1_def}
    87 
    88 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    89 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    90   | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    91   | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    92   | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    93   | is_rec_def _ = false
    94 
    95 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
    96 fun is_chained chained = member Thm.eq_thm_prop chained
    97 
    98 fun scope_of_thm global assms chained th =
    99   if is_chained chained th then Chained
   100   else if global then Global
   101   else if is_assum assms th then Assum
   102   else Local
   103 
   104 val may_be_induction =
   105   exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   106                      body_type T = @{typ bool}
   107                    | _ => false)
   108 
   109 fun status_of_thm css name th =
   110   (* FIXME: use structured name *)
   111   if (String.isSubstring ".induct" name orelse
   112       String.isSubstring ".inducts" name) andalso
   113      may_be_induction (prop_of th) then
   114     Induction
   115   else case Termtab.lookup css (prop_of th) of
   116     SOME status => status
   117   | NONE => General
   118 
   119 fun stature_of_thm global assms chained css name th =
   120   (scope_of_thm global assms chained th, status_of_thm css name th)
   121 
   122 fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
   123   let
   124     val ths = Attrib.eval_thms ctxt [xthm]
   125     val bracket =
   126       map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   127       |> implode
   128     fun nth_name j =
   129       case xref of
   130         Facts.Fact s => backquote s ^ bracket
   131       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   132       | Facts.Named ((name, _), NONE) =>
   133         make_name reserved (length ths > 1) (j + 1) name ^ bracket
   134       | Facts.Named ((name, _), SOME intervals) =>
   135         make_name reserved true
   136                  (nth (maps (explode_interval (length ths)) intervals) j) name ^
   137         bracket
   138     fun add_nth th (j, rest) =
   139       let val name = nth_name j in
   140         (j + 1, ((name, stature_of_thm false [] chained css name th), th)
   141                 :: rest)
   142       end
   143   in (0, []) |> fold add_nth ths |> snd end
   144 
   145 (* Reject theorems with names like "List.filter.filter_list_def" or
   146   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
   147 fun is_package_def s =
   148   let val ss = Long_Name.explode s in
   149     length ss > 2 andalso not (hd ss = "local") andalso
   150     exists (fn suf => String.isSuffix suf s)
   151            ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
   152   end
   153 
   154 (* FIXME: put other record thms here, or declare as "no_atp" *)
   155 fun multi_base_blacklist ctxt ho_atp =
   156   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
   157    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
   158    "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
   159    "nibble.distinct"]
   160   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
   161         append ["induct", "inducts"]
   162   |> map (prefix Long_Name.separator)
   163 
   164 val max_lambda_nesting = 5 (*only applies if not ho_atp*)
   165 
   166 fun term_has_too_many_lambdas max (t1 $ t2) =
   167     exists (term_has_too_many_lambdas max) [t1, t2]
   168   | term_has_too_many_lambdas max (Abs (_, _, t)) =
   169     max = 0 orelse term_has_too_many_lambdas (max - 1) t
   170   | term_has_too_many_lambdas _ _ = false
   171 
   172 (* Don't count nested lambdas at the level of formulas, since they are
   173    quantifiers. *)
   174 fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
   175     formula_has_too_many_lambdas (T :: Ts) t
   176   | formula_has_too_many_lambdas Ts t =
   177     if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
   178       exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
   179     else
   180       term_has_too_many_lambdas max_lambda_nesting t
   181 
   182 (* The maximum apply depth of any "metis" call in "Metis_Examples" (on
   183    2007-10-31) was 11. *)
   184 val max_apply_depth = 18
   185 
   186 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   187   | apply_depth (Abs (_, _, t)) = apply_depth t
   188   | apply_depth _ = 0
   189 
   190 fun is_too_complex ho_atp t =
   191   apply_depth t > max_apply_depth orelse
   192   (not ho_atp andalso formula_has_too_many_lambdas [] t)
   193 
   194 (* FIXME: Ad hoc list *)
   195 val technical_prefixes =
   196   ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
   197    "Limited_Sequence", "Meson", "Metis", "Nitpick",
   198    "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
   199    "Random_Sequence", "Sledgehammer", "SMT"]
   200   |> map (suffix Long_Name.separator)
   201 
   202 fun has_technical_prefix s =
   203   exists (fn pref => String.isPrefix pref s) technical_prefixes
   204 val exists_technical_const = exists_Const (has_technical_prefix o fst)
   205 
   206 (* FIXME: make more reliable *)
   207 val exists_low_level_class_const =
   208   exists_Const (fn (s, _) =>
   209      s = @{const_name equal_class.equal} orelse
   210      String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
   211 
   212 fun is_that_fact th =
   213   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
   214   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
   215                            | _ => false) (prop_of th)
   216 
   217 fun is_likely_tautology_too_meta_or_too_technical th =
   218   let
   219     fun is_interesting_subterm (Const (s, _)) =
   220         not (member (op =) atp_widely_irrelevant_consts s)
   221       | is_interesting_subterm (Free _) = true
   222       | is_interesting_subterm _ = false
   223     fun is_boring_bool t =
   224       not (exists_subterm is_interesting_subterm t) orelse
   225       exists_type (exists_subtype (curry (op =) @{typ prop})) t
   226     fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
   227       | is_boring_prop Ts (@{const "==>"} $ t $ u) =
   228         is_boring_prop Ts t andalso is_boring_prop Ts u
   229       | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   230         is_boring_prop (T :: Ts) t
   231       | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   232         is_boring_prop Ts (t $ eta_expand Ts u 1)
   233       | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   234         is_boring_bool t andalso is_boring_bool u
   235       | is_boring_prop _ _ = true
   236     val t = prop_of th
   237   in
   238     (is_boring_prop [] (prop_of th) andalso
   239      not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
   240     exists_type type_has_top_sort t orelse exists_technical_const t orelse
   241     exists_low_level_class_const t orelse is_that_fact th
   242   end
   243 
   244 fun is_blacklisted_or_something ctxt ho_atp name =
   245   (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
   246   exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
   247 
   248 fun hackish_string_for_term ctxt =
   249   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   250 
   251 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   252    they are displayed as "M" and we want to avoid clashes with these. But
   253    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   254    prefixes of all free variables. In the worse case scenario, where the fact
   255    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   256    name to the offending fact. *)
   257 fun all_prefixes_of s =
   258   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   259 
   260 fun close_form t =
   261   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   262   |> fold (fn ((s, i), T) => fn (t', taken) =>
   263               let val s' = singleton (Name.variant_list taken) s in
   264                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   265                   else Logic.all_const) T
   266                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   267                  s' :: taken)
   268               end)
   269           (Term.add_vars t [] |> sort_wrt (fst o fst))
   270   |> fst
   271 
   272 fun backquote_term ctxt t =
   273   t |> close_form
   274     |> hackish_string_for_term ctxt
   275     |> backquote
   276 
   277 fun backquote_thm ctxt th = backquote_term ctxt (prop_of th)
   278 
   279 fun clasimpset_rule_table_of ctxt =
   280   let
   281     val thy = Proof_Context.theory_of ctxt
   282     val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
   283     fun add stature normalizers get_th =
   284       fold (fn rule =>
   285                let
   286                  val th = rule |> get_th
   287                  val t =
   288                    th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
   289                in
   290                  fold (fn normalize => Termtab.update (normalize t, stature))
   291                       (I :: normalizers)
   292                end)
   293     val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   294       ctxt |> claset_of |> Classical.rep_cs
   295     val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   296 (* Add once it is used:
   297     val elims =
   298       Item_Net.content safeEs @ Item_Net.content hazEs
   299       |> map Classical.classical_rule
   300 *)
   301     val simps = ctxt |> simpset_of |> dest_ss |> #simps
   302     val specs = ctxt |> Spec_Rules.get
   303     val (rec_defs, nonrec_defs) =
   304       specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   305             |> maps (snd o snd)
   306             |> filter_out (member Thm.eq_thm_prop risky_defs)
   307             |> List.partition (is_rec_def o prop_of)
   308     val spec_intros =
   309       specs |> filter (member (op =) [Spec_Rules.Inductive,
   310                                       Spec_Rules.Co_Inductive] o fst)
   311             |> maps (snd o snd)
   312   in
   313     Termtab.empty |> add Simp [atomize] snd simps
   314                   |> add Rec_Def [] I rec_defs
   315                   |> add Non_Rec_Def [] I nonrec_defs
   316 (* Add once it is used:
   317                   |> add Elim [] I elims
   318 *)
   319                   |> add Intro [] I intros
   320                   |> add Inductive [] I spec_intros
   321   end
   322 
   323 fun normalize_eq (t as @{const Trueprop}
   324         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   325     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   326     else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
   327   | normalize_eq (t as @{const Trueprop} $ (@{const Not}
   328         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   329     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   330     else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
   331   | normalize_eq t = t
   332 
   333 val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
   334 
   335 fun if_thm_before th th' =
   336   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   337 
   338 (* Hack: Conflate the facts about a class as seen from the outside with the
   339    corresponding low-level facts, so that MaSh can learn from the low-level
   340    proofs. *)
   341 fun un_class_ify s =
   342   case first_field "_class" s of
   343     SOME (pref, suf) => [s, pref ^ suf]
   344   | NONE => [s]
   345 
   346 fun build_name_tables name_of facts =
   347   let
   348     fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
   349     fun add_plain canon alias =
   350       Symtab.update (Thm.get_name_hint alias,
   351                      name_of (if_thm_before canon alias))
   352     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
   353     fun add_inclass (name, target) =
   354       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
   355     val prop_tab = fold cons_thm facts Termtab.empty
   356     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
   357     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   358   in (plain_name_tab, inclass_name_tab) end
   359 
   360 fun uniquify facts =
   361   Termtab.fold (cons o snd)
   362       (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
   363             Termtab.empty) []
   364 
   365 fun struct_induct_rule_on th =
   366   case Logic.strip_horn (prop_of th) of
   367     (prems, @{const Trueprop}
   368             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
   369     if not (is_TVar ind_T) andalso length prems > 1 andalso
   370        exists (exists_subterm (curry (op aconv) p)) prems andalso
   371        not (exists (exists_subterm (curry (op aconv) a)) prems) then
   372       SOME (p_name, ind_T)
   373     else
   374       NONE
   375   | _ => NONE
   376 
   377 val instantiate_induct_timeout = seconds 0.01
   378 
   379 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   380   let
   381     fun varify_noninducts (t as Free (s, T)) =
   382         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
   383       | varify_noninducts t = t
   384     val p_inst =
   385       concl_prop |> map_aterms varify_noninducts |> close_form
   386                  |> lambda (Free ind_x)
   387                  |> hackish_string_for_term ctxt
   388   in
   389     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   390       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
   391   end
   392 
   393 fun type_match thy (T1, T2) =
   394   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   395   handle Type.TYPE_MATCH => false
   396 
   397 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   398   case struct_induct_rule_on th of
   399     SOME (p_name, ind_T) =>
   400     let val thy = Proof_Context.theory_of ctxt in
   401       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   402               |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   403                      (instantiate_induct_rule ctxt stmt p_name ax)))
   404     end
   405   | NONE => [ax]
   406 
   407 fun external_frees t =
   408   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   409 
   410 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   411   if Config.get ctxt instantiate_inducts then
   412     let
   413       val thy = Proof_Context.theory_of ctxt
   414       val ind_stmt =
   415         (hyp_ts |> filter_out (null o external_frees), concl_t)
   416         |> Logic.list_implies |> Object_Logic.atomize_term thy
   417       val ind_stmt_xs = external_frees ind_stmt
   418     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   419   else
   420     I
   421 
   422 fun maybe_filter_no_atps ctxt =
   423   not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
   424 
   425 fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
   426 
   427 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   428   let
   429     val thy = Proof_Context.theory_of ctxt
   430     val global_facts = Global_Theory.facts_of thy
   431     val local_facts = Proof_Context.facts_of ctxt
   432     val named_locals = local_facts |> Facts.dest_static []
   433     val assms = Assumption.all_assms_of ctxt
   434     fun is_good_unnamed_local th =
   435       not (Thm.has_name_hint th) andalso
   436       forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   437     val unnamed_locals =
   438       union Thm.eq_thm_prop (Facts.props local_facts) chained
   439       |> filter is_good_unnamed_local |> map (pair "" o single)
   440     val full_space =
   441       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   442     fun add_facts global foldx facts =
   443       foldx (fn (name0, ths) =>
   444         if name0 <> "" andalso
   445            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   446            (Facts.is_concealed facts name0 orelse
   447             not (can (Proof_Context.get_thms ctxt) name0) orelse
   448             (not generous andalso
   449              is_blacklisted_or_something ctxt ho_atp name0)) then
   450           I
   451         else
   452           let
   453             val n = length ths
   454             val multi = n > 1
   455             fun check_thms a =
   456               case try (Proof_Context.get_thms ctxt) a of
   457                 NONE => false
   458               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   459           in
   460             pair n
   461             #> fold_rev (fn th => fn (j, accum) =>
   462                    (j - 1,
   463                     if not (member Thm.eq_thm_prop add_ths th) andalso
   464                        (is_likely_tautology_too_meta_or_too_technical th orelse
   465                         (not generous andalso
   466                          is_too_complex ho_atp (prop_of th))) then
   467                       accum
   468                     else
   469                       let
   470                         val new =
   471                           (((fn () =>
   472                                 if name0 = "" then
   473                                   backquote_thm ctxt th
   474                                 else
   475                                   [Facts.extern ctxt facts name0,
   476                                    Name_Space.extern ctxt full_space name0]
   477                                   |> distinct (op =)
   478                                   |> find_first check_thms
   479                                   |> the_default name0
   480                                   |> make_name reserved multi j),
   481                              stature_of_thm global assms chained css name0 th),
   482                            th)
   483                       in
   484                         accum |> (if multi then apsnd else apfst) (cons new)
   485                       end)) ths
   486             #> snd
   487           end)
   488   in
   489     (* The single-theorem names go before the multiple-theorem ones (e.g.,
   490        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
   491        available. *)
   492     `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   493           |> add_facts true Facts.fold_static global_facts global_facts
   494           |> op @
   495   end
   496 
   497 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   498                      concl_t =
   499   if only andalso null add then
   500     []
   501   else
   502     let
   503       val chained =
   504         chained
   505         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   506     in
   507       (if only then
   508          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   509                o fact_from_ref ctxt reserved chained css) add
   510        else
   511          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   512            all_facts ctxt false ho_atp reserved add chained css
   513            |> filter_out (member Thm.eq_thm_prop del o snd)
   514            |> maybe_filter_no_atps ctxt
   515            |> uniquify
   516          end)
   517       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   518     end
   519 
   520 end;