139 end |
139 end |
140 in (0, []) |> fold add_nth ths |> snd end |
140 in (0, []) |> fold add_nth ths |> snd end |
141 |
141 |
142 (* Reject theorems with names like "List.filter.filter_list_def" or |
142 (* Reject theorems with names like "List.filter.filter_list_def" or |
143 "Accessible_Part.acc.defs", as these are definitions arising from packages. *) |
143 "Accessible_Part.acc.defs", as these are definitions arising from packages. *) |
144 fun is_package_def a = |
144 fun is_package_def s = |
145 let val names = Long_Name.explode a in |
145 let val ss = Long_Name.explode s in |
146 (length names > 2 andalso not (hd names = "local") andalso |
146 length ss > 2 andalso not (hd ss = "local") andalso |
147 String.isSuffix "_def" a) orelse String.isSuffix "_defs" a |
147 exists (fn suf => String.isSuffix suf s) |
|
148 ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"] |
148 end |
149 end |
149 |
150 |
150 (* FIXME: put other record thms here, or declare as "no_atp" *) |
151 (* FIXME: put other record thms here, or declare as "no_atp" *) |
151 fun multi_base_blacklist ctxt ho_atp = |
152 fun multi_base_blacklist ctxt ho_atp = |
152 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", |
153 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", |
187 apply_depth t > max_apply_depth orelse |
188 apply_depth t > max_apply_depth orelse |
188 (not ho_atp andalso formula_has_too_many_lambdas [] t) |
189 (not ho_atp andalso formula_has_too_many_lambdas [] t) |
189 |
190 |
190 (* FIXME: Ad hoc list *) |
191 (* FIXME: Ad hoc list *) |
191 val technical_prefixes = |
192 val technical_prefixes = |
192 ["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson", |
193 ["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence", |
193 "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck", |
194 "Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", |
194 "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", |
195 "Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing", |
195 "Sledgehammer", "SMT"] |
196 "Random_Sequence", "Sledgehammer", "SMT"] |
196 |> map (suffix Long_Name.separator) |
197 |> map (suffix Long_Name.separator) |
197 |
198 |
198 fun has_technical_prefix s = |
199 fun has_technical_prefix s = |
199 exists (fn pref => String.isPrefix pref s) technical_prefixes |
200 exists (fn pref => String.isPrefix pref s) technical_prefixes |
200 val exists_technical_const = exists_Const (has_technical_prefix o fst) |
201 val exists_technical_const = exists_Const (has_technical_prefix o fst) |