21 val instantiate_inducts : bool Config.T |
21 val instantiate_inducts : bool Config.T |
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 is_likely_tautology_or_too_meta : thm -> bool |
26 val backquote_thm : thm -> string |
27 val backquote_thm : thm -> string |
27 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
28 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
28 val maybe_instantiate_inducts : |
29 val maybe_instantiate_inducts : |
29 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
30 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
30 -> (((unit -> string) * 'a) * thm) list |
31 -> (((unit -> string) * 'a) * thm) list |
206 is_metastrange_theorem thm orelse |
207 is_metastrange_theorem thm orelse |
207 let val t = prop_of thm in |
208 let val t = prop_of thm in |
208 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse |
209 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse |
209 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
210 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
210 is_that_fact thm |
211 is_that_fact thm |
|
212 end |
|
213 |
|
214 fun is_likely_tautology_or_too_meta th = |
|
215 let |
|
216 val is_boring_const = member (op =) atp_widely_irrelevant_consts |
|
217 fun is_boring_bool t = |
|
218 not (exists_Const (not o is_boring_const o fst) t) orelse |
|
219 exists_type (exists_subtype (curry (op =) @{typ prop})) t |
|
220 fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t |
|
221 | is_boring_prop (@{const "==>"} $ t $ u) = |
|
222 is_boring_prop t andalso is_boring_prop u |
|
223 | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = |
|
224 is_boring_prop t andalso is_boring_prop u |
|
225 | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = |
|
226 is_boring_bool t andalso is_boring_bool u |
|
227 | is_boring_prop _ = true |
|
228 in |
|
229 is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) |
211 end |
230 end |
212 |
231 |
213 fun hackish_string_for_term thy t = |
232 fun hackish_string_for_term thy t = |
214 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
233 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
215 (print_mode_value ())) (Syntax.string_of_term_global thy) t |
234 (print_mode_value ())) (Syntax.string_of_term_global thy) t |
437 maps (map (fn ((name, stature), th) => ((K name, stature), th)) |
456 maps (map (fn ((name, stature), th) => ((K name, stature), th)) |
438 o fact_from_ref ctxt reserved chained css) add |
457 o fact_from_ref ctxt reserved chained css) add |
439 else |
458 else |
440 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in |
459 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in |
441 all_facts ctxt ho_atp reserved add chained css |
460 all_facts ctxt ho_atp reserved add chained css |
|
461 |> filter_out (is_likely_tautology_or_too_meta o snd) |
442 |> filter_out (member Thm.eq_thm_prop del o snd) |
462 |> filter_out (member Thm.eq_thm_prop del o snd) |
443 |> maybe_filter_no_atps ctxt |
463 |> maybe_filter_no_atps ctxt |
444 |> uniquify |
464 |> uniquify |
445 end) |
465 end) |
446 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
466 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |