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