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