src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author blanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 53512 b9bc867e49f6
parent 53511 3ea6b9461c55
child 53513 1082a6fb36c6
permissions -rw-r--r--
slight 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 instantiate_inducts : bool Config.T
    22   val no_fact_override : fact_override
    23   val fact_of_ref :
    24     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    25     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    26   val backquote_thm : Proof.context -> thm -> string
    27   val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
    28   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    29   val build_name_tables :
    30     (thm -> string) -> ('a * thm) list
    31     -> string Symtab.table * string Symtab.table
    32   val maybe_instantiate_inducts :
    33     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    34     -> (((unit -> string) * 'a) * thm) list
    35   val fact_of_raw_fact : raw_fact -> fact
    36   val all_facts :
    37     Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
    38     -> status Termtab.table -> raw_fact list
    39   val nearly_all_facts :
    40     Proof.context -> bool -> fact_override -> unit Symtab.table
    41     -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
    42 end;
    43 
    44 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    45 struct
    46 
    47 open ATP_Util
    48 open ATP_Problem_Generate
    49 open Metis_Tactic
    50 open Sledgehammer_Util
    51 
    52 type raw_fact = ((unit -> string) * stature) * thm
    53 type fact = (string * stature) * thm
    54 
    55 type fact_override =
    56   {add : (Facts.ref * Attrib.src list) list,
    57    del : (Facts.ref * Attrib.src list) list,
    58    only : bool}
    59 
    60 (* experimental feature *)
    61 val instantiate_inducts =
    62   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    63 
    64 val no_fact_override = {add = [], del = [], only = false}
    65 
    66 fun needs_quoting reserved s =
    67   Symtab.defined reserved s orelse
    68   exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
    69 
    70 fun make_name reserved multi j name =
    71   (name |> needs_quoting reserved name ? quote) ^
    72   (if multi then "(" ^ string_of_int j ^ ")" else "")
    73 
    74 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    75   | explode_interval max (Facts.From i) = i upto i + max - 1
    76   | explode_interval _ (Facts.Single i) = [i]
    77 
    78 val backquote =
    79   raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
    80 
    81 (* unfolding these can yield really huge terms *)
    82 val risky_defs = @{thms Bit0_def Bit1_def}
    83 
    84 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    85 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    86   | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    87   | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    88   | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    89   | is_rec_def _ = false
    90 
    91 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
    92 fun is_chained chained = member Thm.eq_thm_prop chained
    93 
    94 fun scope_of_thm global assms chained th =
    95   if is_chained chained th then Chained
    96   else if global then Global
    97   else if is_assum assms th then Assum
    98   else Local
    99 
   100 val may_be_induction =
   101   exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   102                      body_type T = @{typ bool}
   103                    | _ => false)
   104 
   105 fun normalize_vars t =
   106   let
   107     fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
   108       | normT (TVar (z as (_, S))) =
   109         (fn ((knownT, nT), accum) =>
   110             case find_index (equal z) knownT of
   111               ~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
   112             | j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum)))
   113       | normT (T as TFree _) = pair T
   114     fun norm (t $ u) = norm t ##>> norm u #>> op $
   115       | norm (Const (s, T)) = normT T #>> curry Const s
   116       | norm (Var (z as (_, T))) =
   117         normT T
   118         #> (fn (T, (accumT, (known, n))) =>
   119                case find_index (equal z) known of
   120                  ~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
   121                | j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n))))
   122       | norm (Abs (_, T, t)) =
   123         norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
   124       | norm (Bound j) = pair (Bound j)
   125       | norm (Free (s, T)) = normT T #>> curry Free s
   126   in fst (norm t (([], 0), ([], 0))) end
   127 
   128 fun status_of_thm css name th =
   129   let val t = normalize_vars (prop_of th) in
   130     (* FIXME: use structured name *)
   131     if String.isSubstring ".induct" name andalso may_be_induction t then
   132       Induction
   133     else case Termtab.lookup css t of
   134       SOME status => status
   135     | NONE =>
   136       let val concl = Logic.strip_imp_concl t in
   137         case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
   138           SOME lrhss =>
   139           let
   140             val prems = Logic.strip_imp_prems t
   141             val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
   142           in
   143             Termtab.lookup css t' |> the_default General
   144           end
   145         | NONE => General
   146       end
   147   end
   148 
   149 fun stature_of_thm global assms chained css name th =
   150   (scope_of_thm global assms chained th, status_of_thm css name th)
   151 
   152 fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
   153   let
   154     val ths = Attrib.eval_thms ctxt [xthm]
   155     val bracket =
   156       map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   157       |> implode
   158     fun nth_name j =
   159       case xref of
   160         Facts.Fact s => backquote s ^ bracket
   161       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   162       | Facts.Named ((name, _), NONE) =>
   163         make_name reserved (length ths > 1) (j + 1) name ^ bracket
   164       | Facts.Named ((name, _), SOME intervals) =>
   165         make_name reserved true
   166                  (nth (maps (explode_interval (length ths)) intervals) j) name ^
   167         bracket
   168     fun add_nth th (j, rest) =
   169       let val name = nth_name j in
   170         (j + 1, ((name, stature_of_thm false [] chained css name th), th)
   171                 :: rest)
   172       end
   173   in (0, []) |> fold add_nth ths |> snd end
   174 
   175 (* Reject theorems with names like "List.filter.filter_list_def" or
   176   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
   177 fun is_package_def s =
   178   let val ss = Long_Name.explode s in
   179     length ss > 2 andalso not (hd ss = "local") andalso
   180     exists (fn suf => String.isSuffix suf s)
   181            ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
   182   end
   183 
   184 (* FIXME: put other record thms here, or declare as "no_atp" *)
   185 fun multi_base_blacklist ctxt ho_atp =
   186   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
   187    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
   188    "weak_case_cong", "nat_of_char_simps", "nibble.simps",
   189    "nibble.distinct"]
   190   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
   191         append ["induct", "inducts"]
   192   |> map (prefix Long_Name.separator)
   193 
   194 (* 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 is_technical_const (s, _) =
   203   exists (fn pref => String.isPrefix pref s) technical_prefixes
   204 
   205 (* FIXME: make more reliable *)
   206 val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
   207 fun is_low_level_class_const (s, _) =
   208   s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
   209 
   210 val sep_that = Long_Name.separator ^ Obtain.thatN
   211 
   212 fun is_that_fact th =
   213   String.isSuffix sep_that (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 [] t andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
   239     exists_Const (is_technical_const orf is_low_level_class_const) t orelse
   240     is_that_fact th
   241   end
   242 
   243 fun is_blacklisted_or_something ctxt ho_atp =
   244   let
   245     val blist = multi_base_blacklist ctxt ho_atp
   246     fun is_blisted name =
   247       is_package_def name orelse exists (fn s => String.isSuffix s name) blist
   248   in is_blisted end
   249 
   250 fun hackish_string_of_term ctxt =
   251   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   252 
   253 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   254    they are displayed as "M" and we want to avoid clashes with these. But
   255    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   256    prefixes of all free variables. In the worse case scenario, where the fact
   257    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   258    name to the offending fact. *)
   259 fun all_prefixes_of s =
   260   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   261 
   262 fun close_form t =
   263   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   264   |> fold (fn ((s, i), T) => fn (t', taken) =>
   265               let val s' = singleton (Name.variant_list taken) s in
   266                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   267                   else Logic.all_const) T
   268                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   269                  s' :: taken)
   270               end)
   271           (Term.add_vars t [] |> sort_wrt (fst o fst))
   272   |> fst
   273 
   274 fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
   275 fun backquote_thm ctxt = backquote_term ctxt o prop_of
   276 
   277 (* gracefully handle huge background theories *)
   278 val max_simps_for_clasimpset = 10000
   279 
   280 fun clasimpset_rule_table_of ctxt =
   281   let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
   282     if length simps >= max_simps_for_clasimpset then
   283       Termtab.empty
   284     else
   285       let
   286         fun add stature th =
   287           Termtab.update (normalize_vars (prop_of th), stature)
   288         val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   289           ctxt |> claset_of |> Classical.rep_cs
   290         val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   291 (* Add once it is used:
   292         val elims =
   293           Item_Net.content safeEs @ Item_Net.content hazEs
   294           |> map Classical.classical_rule
   295 *)
   296         val specs = ctxt |> Spec_Rules.get
   297         val (rec_defs, nonrec_defs) =
   298           specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   299                 |> maps (snd o snd)
   300                 |> filter_out (member Thm.eq_thm_prop risky_defs)
   301                 |> List.partition (is_rec_def o prop_of)
   302         val spec_intros =
   303           specs |> filter (member (op =) [Spec_Rules.Inductive,
   304                                           Spec_Rules.Co_Inductive] o fst)
   305                 |> maps (snd o snd)
   306       in
   307         Termtab.empty |> fold (add Simp o snd) simps
   308                       |> fold (add Rec_Def) rec_defs
   309                       |> fold (add Non_Rec_Def) nonrec_defs
   310 (* Add once it is used:
   311                       |> fold (add Elim) elims
   312 *)
   313                       |> fold (add Intro) intros
   314                       |> fold (add Inductive) spec_intros
   315       end
   316   end
   317 
   318 fun normalize_eq (t as @{const Trueprop}
   319         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   320     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   321     else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
   322   | normalize_eq (t as @{const Trueprop} $ (@{const Not}
   323         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   324     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   325     else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
   326   | normalize_eq t = t
   327 
   328 val normalize_eq_vars = normalize_eq #> normalize_vars
   329 
   330 fun if_thm_before th th' =
   331   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   332 
   333 (* Hack: Conflate the facts about a class as seen from the outside with the
   334    corresponding low-level facts, so that MaSh can learn from the low-level
   335    proofs. *)
   336 fun un_class_ify s =
   337   case first_field "_class" s of
   338     SOME (pref, suf) => [s, pref ^ suf]
   339   | NONE => [s]
   340 
   341 fun build_name_tables name_of facts =
   342   let
   343     fun cons_thm (_, th) =
   344       Termtab.cons_list (normalize_eq_vars (prop_of th), th)
   345     fun add_plain canon alias =
   346       Symtab.update (Thm.get_name_hint alias,
   347                      name_of (if_thm_before canon alias))
   348     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
   349     fun add_inclass (name, target) =
   350       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
   351     val prop_tab = fold cons_thm facts Termtab.empty
   352     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
   353     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   354   in (plain_name_tab, inclass_name_tab) end
   355 
   356 fun keyed_distinct key_of xs =
   357   let val tab = fold (Termtab.default o `key_of) xs Termtab.empty in
   358     Termtab.fold (cons o snd) tab []
   359   end
   360 
   361 fun hashed_keyed_distinct hash_of key_of xs =
   362   let
   363     val ys = map (`hash_of) xs
   364     val sorted_ys = sort (int_ord o pairself fst) ys
   365     val grouped_ys = AList.coalesce (op =) sorted_ys
   366   in maps (keyed_distinct key_of o snd) grouped_ys end
   367 
   368 fun struct_induct_rule_on th =
   369   case Logic.strip_horn (prop_of th) of
   370     (prems, @{const Trueprop}
   371             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
   372     if not (is_TVar ind_T) andalso length prems > 1 andalso
   373        exists (exists_subterm (curry (op aconv) p)) prems andalso
   374        not (exists (exists_subterm (curry (op aconv) a)) prems) then
   375       SOME (p_name, ind_T)
   376     else
   377       NONE
   378   | _ => NONE
   379 
   380 val instantiate_induct_timeout = seconds 0.01
   381 
   382 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   383   let
   384     fun varify_noninducts (t as Free (s, T)) =
   385         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
   386       | varify_noninducts t = t
   387     val p_inst =
   388       concl_prop |> map_aterms varify_noninducts |> close_form
   389                  |> lambda (Free ind_x)
   390                  |> hackish_string_of_term ctxt
   391   in
   392     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   393       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
   394   end
   395 
   396 fun type_match thy (T1, T2) =
   397   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   398   handle Type.TYPE_MATCH => false
   399 
   400 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   401   case struct_induct_rule_on th of
   402     SOME (p_name, ind_T) =>
   403     let val thy = Proof_Context.theory_of ctxt in
   404       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   405               |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   406                      (instantiate_induct_rule ctxt stmt p_name ax)))
   407     end
   408   | NONE => [ax]
   409 
   410 fun external_frees t =
   411   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   412 
   413 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   414   if Config.get ctxt instantiate_inducts then
   415     let
   416       val thy = Proof_Context.theory_of ctxt
   417       val ind_stmt =
   418         (hyp_ts |> filter_out (null o external_frees), concl_t)
   419         |> Logic.list_implies |> Object_Logic.atomize_term thy
   420       val ind_stmt_xs = external_frees ind_stmt
   421     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   422   else
   423     I
   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     val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
   443     fun add_facts global foldx facts =
   444       foldx (fn (name0, ths) =>
   445         if name0 <> "" andalso
   446            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   447            (Facts.is_concealed facts name0 orelse
   448             (not generous andalso is_blacklisted_or_something name0)) then
   449           I
   450         else
   451           let
   452             val n = length ths
   453             val multi = n > 1
   454             fun check_thms a =
   455               case try (Proof_Context.get_thms ctxt) a of
   456                 NONE => false
   457               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   458           in
   459             pair n
   460             #> fold_rev (fn th => fn (j, accum) =>
   461                    (j - 1,
   462                     if not (member Thm.eq_thm_prop add_ths th) andalso
   463                        is_likely_tautology_too_meta_or_too_technical th then
   464                       accum
   465                     else
   466                       let
   467                         val new =
   468                           (((fn () =>
   469                                 if name0 = "" then
   470                                   backquote_thm ctxt th
   471                                 else
   472                                   [Facts.extern ctxt facts name0,
   473                                    Name_Space.extern ctxt full_space name0]
   474                                   |> distinct (op =)
   475                                   |> find_first check_thms
   476                                   |> the_default name0
   477                                   |> make_name reserved multi j),
   478                              stature_of_thm global assms chained css name0 th),
   479                            th)
   480                       in
   481                         accum |> (if multi then apsnd else apfst) (cons new)
   482                       end)) ths
   483             #> snd
   484           end)
   485   in
   486     (* The single-theorem names go before the multiple-theorem ones (e.g.,
   487        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
   488        available. *)
   489     `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   490           |> add_facts true Facts.fold_static global_facts global_facts
   491           |> op @
   492   end
   493 
   494 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   495                      concl_t =
   496   if only andalso null add then
   497     []
   498   else
   499     let
   500       val chained =
   501         chained
   502         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   503     in
   504       (if only then
   505          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   506                o fact_of_ref ctxt reserved chained css) add
   507        else
   508          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   509            all_facts ctxt false ho_atp reserved add chained css
   510            |> filter_out
   511                   ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
   512            |> hashed_keyed_distinct (size_of_term o prop_of o snd)
   513                   (normalize_eq_vars o prop_of o snd)
   514          end)
   515       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   516     end
   517 
   518 end;