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