22 val no_fact_override : fact_override |
22 val no_fact_override : fact_override |
23 val fact_from_ref : |
23 val fact_from_ref : |
24 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table |
24 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table |
25 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list |
25 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list |
26 val backquote_thm : Proof.context -> thm -> string |
26 val backquote_thm : Proof.context -> thm -> string |
|
27 val is_bad_for_atps : bool -> thm -> bool |
|
28 val is_concealed_or_backlisted_or_something : |
|
29 Proof.context -> bool -> Facts.T -> string -> bool |
27 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
30 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
28 val build_all_names : |
31 val build_all_names : |
29 (thm -> string) -> ('a * thm) list -> string Symtab.table |
32 (thm -> string) -> ('a * thm) list -> string Symtab.table |
30 val maybe_instantiate_inducts : |
33 val maybe_instantiate_inducts : |
31 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
34 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
230 in |
233 in |
231 is_boring_prop [] (prop_of th) andalso |
234 is_boring_prop [] (prop_of th) andalso |
232 not (Thm.eq_thm_prop (@{thm ext}, th)) |
235 not (Thm.eq_thm_prop (@{thm ext}, th)) |
233 end |
236 end |
234 |
237 |
235 fun is_theorem_bad_for_atps ho_atp th = |
238 fun is_bad_for_atps ho_atp th = |
236 let val t = prop_of th in |
239 let val t = prop_of th in |
237 is_formula_too_complex ho_atp t orelse |
240 is_formula_too_complex ho_atp t orelse |
238 exists_type type_has_top_sort t orelse exists_technical_const t orelse |
241 exists_type type_has_top_sort t orelse exists_technical_const t orelse |
239 exists_low_level_class_const t orelse is_that_fact th |
242 exists_low_level_class_const t orelse is_that_fact th |
240 end |
243 end |
|
244 |
|
245 fun is_concealed_or_backlisted_or_something ctxt ho_atp facts name = |
|
246 Facts.is_concealed facts name orelse |
|
247 not (can (Proof_Context.get_thms ctxt) name) orelse |
|
248 (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse |
|
249 exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp) |
241 |
250 |
242 fun hackish_string_for_term ctxt = |
251 fun hackish_string_for_term ctxt = |
243 with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces |
252 with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces |
244 |
253 |
245 (* This is a terrible hack. Free variables are sometimes coded as "M__" when |
254 (* This is a terrible hack. Free variables are sometimes coded as "M__" when |
420 fun add_facts global foldx facts = |
429 fun add_facts global foldx facts = |
421 foldx (fn (name0, ths) => |
430 foldx (fn (name0, ths) => |
422 if not really_all andalso |
431 if not really_all andalso |
423 name0 <> "" andalso |
432 name0 <> "" andalso |
424 forall (not o member Thm.eq_thm_prop add_ths) ths andalso |
433 forall (not o member Thm.eq_thm_prop add_ths) ths andalso |
425 (Facts.is_concealed facts name0 orelse |
434 is_concealed_or_backlisted_or_something ctxt ho_atp facts name0 then |
426 not (can (Proof_Context.get_thms ctxt) name0) orelse |
|
427 (not (Config.get ctxt ignore_no_atp) andalso |
|
428 is_package_def name0) orelse |
|
429 exists (fn s => String.isSuffix s name0) |
|
430 (multi_base_blacklist ctxt ho_atp)) then |
|
431 I |
435 I |
432 else |
436 else |
433 let |
437 let |
434 val n = length ths |
438 val n = length ths |
435 val multi = n > 1 |
439 val multi = n > 1 |
442 #> fold_rev (fn th => fn (j, (multis, unis)) => |
446 #> fold_rev (fn th => fn (j, (multis, unis)) => |
443 (j - 1, |
447 (j - 1, |
444 if not (member Thm.eq_thm_prop add_ths th) andalso |
448 if not (member Thm.eq_thm_prop add_ths th) andalso |
445 is_likely_tautology_or_too_meta th orelse |
449 is_likely_tautology_or_too_meta th orelse |
446 (not really_all andalso |
450 (not really_all andalso |
447 is_theorem_bad_for_atps ho_atp th) then |
451 is_bad_for_atps ho_atp th) then |
448 (multis, unis) |
452 (multis, unis) |
449 else |
453 else |
450 let |
454 let |
451 val new = |
455 val new = |
452 (((fn () => |
456 (((fn () => |