src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author blanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 53509 cf7679195169
parent 53508 8d8f72aa5c0b
child 53510 c0982ad1281d
permissions -rw-r--r--
minor speed optimization
     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_of_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 normalize_vars t =
   110   let
   111     fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
   112       | normT (TVar (z as (_, S))) =
   113         (fn ((knownT, nT), accum) =>
   114             case find_index (equal z) knownT of
   115               ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
   116             | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
   117       | normT (T as TFree _) = pair T
   118     fun norm (t $ u) = norm t ##>> norm u #>> op $
   119       | norm (Const (s, T)) = normT T #>> curry Const s
   120       | norm (Var (z as (_, T))) =
   121         normT T
   122         #> (fn (T, (accumT, (known, n))) =>
   123                case find_index (equal z) known of
   124                  ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
   125                | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
   126       | norm (Abs (_, T, t)) =
   127         norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
   128       | norm (Bound j) = pair (Bound j)
   129       | norm (Free (s, T)) = normT T #>> curry Free s
   130   in fst (norm t (([], 0), ([], 0))) end
   131 
   132 fun status_of_thm css name th =
   133   let val t = normalize_vars (prop_of th) in
   134     (* FIXME: use structured name *)
   135     if String.isSubstring ".induct" name andalso may_be_induction t then
   136       Induction
   137     else case Termtab.lookup css t of
   138       SOME status => status
   139     | NONE =>
   140       let val concl = Logic.strip_imp_concl t in
   141         case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
   142           SOME lrhss =>
   143           let
   144             val prems = Logic.strip_imp_prems t
   145             val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
   146           in
   147             Termtab.lookup css t' |> the_default General
   148           end
   149         | NONE => General
   150       end
   151   end
   152 
   153 fun stature_of_thm global assms chained css name th =
   154   (scope_of_thm global assms chained th, status_of_thm css name th)
   155 
   156 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
   157   let
   158     val ths = Attrib.eval_thms ctxt [xthm]
   159     val bracket =
   160       map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   161       |> implode
   162     fun nth_name j =
   163       case xref of
   164         Facts.Fact s => backquote s ^ bracket
   165       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   166       | Facts.Named ((name, _), NONE) =>
   167         make_name reserved (length ths > 1) (j + 1) name ^ bracket
   168       | Facts.Named ((name, _), SOME intervals) =>
   169         make_name reserved true
   170                  (nth (maps (explode_interval (length ths)) intervals) j) name ^
   171         bracket
   172     fun add_nth th (j, rest) =
   173       let val name = nth_name j in
   174         (j + 1, ((name, stature_of_thm false [] chained css name th), th)
   175                 :: rest)
   176       end
   177   in (0, []) |> fold add_nth ths |> snd end
   178 
   179 (* Reject theorems with names like "List.filter.filter_list_def" or
   180   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
   181 fun is_package_def s =
   182   let val ss = Long_Name.explode s in
   183     length ss > 2 andalso not (hd ss = "local") andalso
   184     exists (fn suf => String.isSuffix suf s)
   185            ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
   186   end
   187 
   188 (* FIXME: put other record thms here, or declare as "no_atp" *)
   189 fun multi_base_blacklist ctxt ho_atp =
   190   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
   191    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
   192    "weak_case_cong", "nat_of_char_simps", "nibble.simps",
   193    "nibble.distinct"]
   194   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
   195         append ["induct", "inducts"]
   196   |> map (prefix Long_Name.separator)
   197 
   198 (* FIXME: Ad hoc list *)
   199 val technical_prefixes =
   200   ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
   201    "Limited_Sequence", "Meson", "Metis", "Nitpick",
   202    "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
   203    "Random_Sequence", "Sledgehammer", "SMT"]
   204   |> map (suffix Long_Name.separator)
   205 
   206 fun is_technical_const (s, _) =
   207   exists (fn pref => String.isPrefix pref s) technical_prefixes
   208 
   209 (* FIXME: make more reliable *)
   210 val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
   211 fun is_low_level_class_const (s, _) =
   212   s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
   213 
   214 val sep_that = Long_Name.separator ^ Obtain.thatN
   215 
   216 fun is_that_fact th =
   217   String.isSuffix sep_that (Thm.get_name_hint th)
   218   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
   219                            | _ => false) (prop_of th)
   220 
   221 fun is_likely_tautology_too_meta_or_too_technical th =
   222   let
   223     fun is_interesting_subterm (Const (s, _)) =
   224         not (member (op =) atp_widely_irrelevant_consts s)
   225       | is_interesting_subterm (Free _) = true
   226       | is_interesting_subterm _ = false
   227     fun is_boring_bool t =
   228       not (exists_subterm is_interesting_subterm t) orelse
   229       exists_type (exists_subtype (curry (op =) @{typ prop})) t
   230     fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
   231       | is_boring_prop Ts (@{const "==>"} $ t $ u) =
   232         is_boring_prop Ts t andalso is_boring_prop Ts u
   233       | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   234         is_boring_prop (T :: Ts) t
   235       | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   236         is_boring_prop Ts (t $ eta_expand Ts u 1)
   237       | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   238         is_boring_bool t andalso is_boring_bool u
   239       | is_boring_prop _ _ = true
   240     val t = prop_of th
   241   in
   242     (is_boring_prop [] t andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
   243     exists_Const (is_technical_const orf is_low_level_class_const) t orelse
   244     is_that_fact th
   245   end
   246 
   247 fun is_blacklisted_or_something ctxt ho_atp name =
   248   (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
   249   exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
   250 
   251 fun hackish_string_of_term ctxt =
   252   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   253 
   254 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   255    they are displayed as "M" and we want to avoid clashes with these. But
   256    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   257    prefixes of all free variables. In the worse case scenario, where the fact
   258    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   259    name to the offending fact. *)
   260 fun all_prefixes_of s =
   261   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   262 
   263 fun close_form t =
   264   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   265   |> fold (fn ((s, i), T) => fn (t', taken) =>
   266               let val s' = singleton (Name.variant_list taken) s in
   267                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   268                   else Logic.all_const) T
   269                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   270                  s' :: taken)
   271               end)
   272           (Term.add_vars t [] |> sort_wrt (fst o fst))
   273   |> fst
   274 
   275 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
   276 fun backquote_thm ctxt = backquote_term ctxt o prop_of
   277 
   278 (* gracefully handle huge background theories *)
   279 val max_simps_for_clasimpset = 10000
   280 
   281 fun clasimpset_rule_table_of ctxt =
   282   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
   283     if length simps >= max_simps_for_clasimpset then
   284       Termtab.empty
   285     else
   286       let
   287         fun add stature th =
   288           Termtab.update (normalize_vars (prop_of th), stature)
   289         val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   290           ctxt |> claset_of |> Classical.rep_cs
   291         val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   292 (* Add once it is used:
   293         val elims =
   294           Item_Net.content safeEs @ Item_Net.content hazEs
   295           |> map Classical.classical_rule
   296 *)
   297         val specs = ctxt |> Spec_Rules.get
   298         val (rec_defs, nonrec_defs) =
   299           specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   300                 |> maps (snd o snd)
   301                 |> filter_out (member Thm.eq_thm_prop risky_defs)
   302                 |> List.partition (is_rec_def o prop_of)
   303         val spec_intros =
   304           specs |> filter (member (op =) [Spec_Rules.Inductive,
   305                                           Spec_Rules.Co_Inductive] o fst)
   306                 |> maps (snd o snd)
   307       in
   308         Termtab.empty |> fold (add Simp o snd) simps
   309                       |> fold (add Rec_Def) rec_defs
   310                       |> fold (add Non_Rec_Def) nonrec_defs
   311 (* Add once it is used:
   312                       |> fold (add Elim) elims
   313 *)
   314                       |> fold (add Intro) intros
   315                       |> fold (add Inductive) spec_intros
   316       end
   317   end
   318 
   319 fun normalize_eq (t as @{const Trueprop}
   320         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   321     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   322     else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
   323   | normalize_eq (t as @{const Trueprop} $ (@{const Not}
   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 (HOLogic.mk_not (t0 $ t2 $ t1))
   327   | normalize_eq t = t
   328 
   329 val normalize_eq_vars = normalize_eq #> normalize_vars
   330 
   331 fun if_thm_before th th' =
   332   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   333 
   334 (* Hack: Conflate the facts about a class as seen from the outside with the
   335    corresponding low-level facts, so that MaSh can learn from the low-level
   336    proofs. *)
   337 fun un_class_ify s =
   338   case first_field "_class" s of
   339     SOME (pref, suf) => [s, pref ^ suf]
   340   | NONE => [s]
   341 
   342 fun build_name_tables name_of facts =
   343   let
   344     fun cons_thm (_, th) =
   345       Termtab.cons_list (normalize_eq_vars (prop_of th), th)
   346     fun add_plain canon alias =
   347       Symtab.update (Thm.get_name_hint alias,
   348                      name_of (if_thm_before canon alias))
   349     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
   350     fun add_inclass (name, target) =
   351       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
   352     val prop_tab = fold cons_thm facts Termtab.empty
   353     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
   354     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   355   in (plain_name_tab, inclass_name_tab) end
   356 
   357 fun keyed_distinct key_of xs =
   358   let val tab = fold (Termtab.default o `key_of) xs Termtab.empty in
   359     Termtab.fold (cons o snd) tab []
   360   end
   361 
   362 fun hashed_keyed_distinct hash_of key_of xs =
   363   let
   364     val ys = map (`hash_of) xs
   365     val sorted_ys = sort (int_ord o pairself fst) ys
   366     val grouped_ys = AList.coalesce (op =) sorted_ys
   367   in maps (keyed_distinct key_of o snd) grouped_ys end
   368 
   369 fun struct_induct_rule_on th =
   370   case Logic.strip_horn (prop_of th) of
   371     (prems, @{const Trueprop}
   372             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
   373     if not (is_TVar ind_T) andalso length prems > 1 andalso
   374        exists (exists_subterm (curry (op aconv) p)) prems andalso
   375        not (exists (exists_subterm (curry (op aconv) a)) prems) then
   376       SOME (p_name, ind_T)
   377     else
   378       NONE
   379   | _ => NONE
   380 
   381 val instantiate_induct_timeout = seconds 0.01
   382 
   383 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   384   let
   385     fun varify_noninducts (t as Free (s, T)) =
   386         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
   387       | varify_noninducts t = t
   388     val p_inst =
   389       concl_prop |> map_aterms varify_noninducts |> close_form
   390                  |> lambda (Free ind_x)
   391                  |> hackish_string_of_term ctxt
   392   in
   393     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   394       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
   395   end
   396 
   397 fun type_match thy (T1, T2) =
   398   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   399   handle Type.TYPE_MATCH => false
   400 
   401 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   402   case struct_induct_rule_on th of
   403     SOME (p_name, ind_T) =>
   404     let val thy = Proof_Context.theory_of ctxt in
   405       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   406               |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   407                      (instantiate_induct_rule ctxt stmt p_name ax)))
   408     end
   409   | NONE => [ax]
   410 
   411 fun external_frees t =
   412   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   413 
   414 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   415   if Config.get ctxt instantiate_inducts then
   416     let
   417       val thy = Proof_Context.theory_of ctxt
   418       val ind_stmt =
   419         (hyp_ts |> filter_out (null o external_frees), concl_t)
   420         |> Logic.list_implies |> Object_Logic.atomize_term thy
   421       val ind_stmt_xs = external_frees ind_stmt
   422     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   423   else
   424     I
   425 
   426 fun maybe_filter_no_atps ctxt =
   427   not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
   428 
   429 fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
   430 
   431 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   432   let
   433     val thy = Proof_Context.theory_of ctxt
   434     val global_facts = Global_Theory.facts_of thy
   435     val local_facts = Proof_Context.facts_of ctxt
   436     val named_locals = local_facts |> Facts.dest_static []
   437     val assms = Assumption.all_assms_of ctxt
   438     fun is_good_unnamed_local th =
   439       not (Thm.has_name_hint th) andalso
   440       forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   441     val unnamed_locals =
   442       union Thm.eq_thm_prop (Facts.props local_facts) chained
   443       |> filter is_good_unnamed_local |> map (pair "" o single)
   444     val full_space =
   445       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   446     fun add_facts global foldx facts =
   447       foldx (fn (name0, ths) =>
   448         if name0 <> "" andalso
   449            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   450            (Facts.is_concealed facts name0 orelse
   451             not (can (Proof_Context.get_thms ctxt) name0) orelse
   452             (not generous andalso
   453              is_blacklisted_or_something ctxt ho_atp name0)) then
   454           I
   455         else
   456           let
   457             val n = length ths
   458             val multi = n > 1
   459             fun check_thms a =
   460               case try (Proof_Context.get_thms ctxt) a of
   461                 NONE => false
   462               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   463           in
   464             pair n
   465             #> fold_rev (fn th => fn (j, accum) =>
   466                    (j - 1,
   467                     if not (member Thm.eq_thm_prop add_ths th) andalso
   468                        (is_likely_tautology_too_meta_or_too_technical th) then
   469                       accum
   470                     else
   471                       let
   472                         val new =
   473                           (((fn () =>
   474                                 if name0 = "" then
   475                                   backquote_thm ctxt th
   476                                 else
   477                                   [Facts.extern ctxt facts name0,
   478                                    Name_Space.extern ctxt full_space name0]
   479                                   |> distinct (op =)
   480                                   |> find_first check_thms
   481                                   |> the_default name0
   482                                   |> make_name reserved multi j),
   483                              stature_of_thm global assms chained css name0 th),
   484                            th)
   485                       in
   486                         accum |> (if multi then apsnd else apfst) (cons new)
   487                       end)) ths
   488             #> snd
   489           end)
   490   in
   491     (* The single-theorem names go before the multiple-theorem ones (e.g.,
   492        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
   493        available. *)
   494     `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   495           |> add_facts true Facts.fold_static global_facts global_facts
   496           |> op @
   497   end
   498 
   499 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   500                      concl_t =
   501   if only andalso null add then
   502     []
   503   else
   504     let
   505       val chained =
   506         chained
   507         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   508     in
   509       (if only then
   510          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   511                o fact_of_ref ctxt reserved chained css) add
   512        else
   513          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   514            all_facts ctxt false ho_atp reserved add chained css
   515            |> filter_out (member Thm.eq_thm_prop del o snd)
   516            |> maybe_filter_no_atps ctxt
   517            |> hashed_keyed_distinct (size_of_term o prop_of o snd)
   518                   (normalize_eq_vars o prop_of o snd)
   519          end)
   520       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   521     end
   522 
   523 end;