equal
deleted
inserted
replaced
141 |
141 |
142 ML {* |
142 ML {* |
143 val preproc_timeout = seconds 5.0 |
143 val preproc_timeout = seconds 5.0 |
144 val mono_timeout = seconds 1.0 |
144 val mono_timeout = seconds 1.0 |
145 |
145 |
146 fun all_unconcealed_theorems_of thy = |
|
147 let val facts = Global_Theory.facts_of thy in |
|
148 Facts.fold_static |
|
149 (fn (name, ths) => |
|
150 if Facts.is_concealed facts name then I |
|
151 else append (map (`(Thm.get_name_hint)) ths)) |
|
152 facts [] |
|
153 end |
|
154 |
|
155 fun is_forbidden_theorem name = |
146 fun is_forbidden_theorem name = |
156 length (Long_Name.explode name) <> 2 orelse |
147 length (Long_Name.explode name) <> 2 orelse |
157 String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse |
148 String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse |
158 String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse |
149 String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse |
159 String.isSuffix "_def" name orelse |
150 String.isSuffix "_def" name orelse |
161 |
152 |
162 fun theorems_of thy = |
153 fun theorems_of thy = |
163 filter (fn (name, th) => |
154 filter (fn (name, th) => |
164 not (is_forbidden_theorem name) andalso |
155 not (is_forbidden_theorem name) andalso |
165 (theory_of_thm th, thy) |> pairself Context.theory_name |> op =) |
156 (theory_of_thm th, thy) |> pairself Context.theory_name |> op =) |
166 (all_unconcealed_theorems_of thy) |
157 (Global_Theory.all_thms_of thy true) |
167 |
158 |
168 fun check_formulas tsp = |
159 fun check_formulas tsp = |
169 let |
160 let |
170 fun is_type_actually_monotonic T = |
161 fun is_type_actually_monotonic T = |
171 Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp |
162 Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp |