205 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN |
205 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN |
206 | _ => false) (prop_of th) |
206 | _ => false) (prop_of th) |
207 |
207 |
208 fun is_likely_tautology_or_too_meta th = |
208 fun is_likely_tautology_or_too_meta th = |
209 let |
209 let |
210 val is_boring_const = member (op =) atp_widely_irrelevant_consts |
210 fun is_interesting_subterm (Const (s, _)) = |
|
211 not (member (op =) atp_widely_irrelevant_consts s) |
|
212 | is_interesting_subterm (Free _) = true |
|
213 | is_interesting_subterm _ = false |
211 fun is_boring_bool t = |
214 fun is_boring_bool t = |
212 not (exists_Const (not o is_boring_const o fst) t) orelse |
215 not (exists_subterm is_interesting_subterm t) orelse |
213 exists_type (exists_subtype (curry (op =) @{typ prop})) t |
216 exists_type (exists_subtype (curry (op =) @{typ prop})) t |
214 fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t |
217 fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t |
215 | is_boring_prop (@{const "==>"} $ t $ u) = |
218 | is_boring_prop (@{const "==>"} $ t $ u) = |
216 is_boring_prop t andalso is_boring_prop u |
219 is_boring_prop t andalso is_boring_prop u |
217 | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = |
220 | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) = |