8 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} |
8 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} |
9 |
9 |
10 theory Nitpick |
10 theory Nitpick |
11 imports Map Quotient SAT Record |
11 imports Map Quotient SAT Record |
12 keywords "nitpick" :: diag and "nitpick_params" :: thy_decl |
12 keywords "nitpick" :: diag and "nitpick_params" :: thy_decl |
13 uses ("Tools/Nitpick/kodkod.ML") |
|
14 ("Tools/Nitpick/kodkod_sat.ML") |
|
15 ("Tools/Nitpick/nitpick_util.ML") |
|
16 ("Tools/Nitpick/nitpick_hol.ML") |
|
17 ("Tools/Nitpick/nitpick_preproc.ML") |
|
18 ("Tools/Nitpick/nitpick_mono.ML") |
|
19 ("Tools/Nitpick/nitpick_scope.ML") |
|
20 ("Tools/Nitpick/nitpick_peephole.ML") |
|
21 ("Tools/Nitpick/nitpick_rep.ML") |
|
22 ("Tools/Nitpick/nitpick_nut.ML") |
|
23 ("Tools/Nitpick/nitpick_kodkod.ML") |
|
24 ("Tools/Nitpick/nitpick_model.ML") |
|
25 ("Tools/Nitpick/nitpick.ML") |
|
26 ("Tools/Nitpick/nitpick_isar.ML") |
|
27 ("Tools/Nitpick/nitpick_tests.ML") |
|
28 begin |
13 begin |
29 |
14 |
30 typedecl bisim_iterator |
15 typedecl bisim_iterator |
31 |
16 |
32 axiomatization unknown :: 'a |
17 axiomatization unknown :: 'a |
210 "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0" |
195 "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0" |
211 |
196 |
212 definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where |
197 definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where |
213 "of_frac q \<equiv> of_int (num q) / of_int (denom q)" |
198 "of_frac q \<equiv> of_int (num q) / of_int (denom q)" |
214 |
199 |
215 use "Tools/Nitpick/kodkod.ML" |
200 ML_file "Tools/Nitpick/kodkod.ML" |
216 use "Tools/Nitpick/kodkod_sat.ML" |
201 ML_file "Tools/Nitpick/kodkod_sat.ML" |
217 use "Tools/Nitpick/nitpick_util.ML" |
202 ML_file "Tools/Nitpick/nitpick_util.ML" |
218 use "Tools/Nitpick/nitpick_hol.ML" |
203 ML_file "Tools/Nitpick/nitpick_hol.ML" |
219 use "Tools/Nitpick/nitpick_mono.ML" |
204 ML_file "Tools/Nitpick/nitpick_mono.ML" |
220 use "Tools/Nitpick/nitpick_preproc.ML" |
205 ML_file "Tools/Nitpick/nitpick_preproc.ML" |
221 use "Tools/Nitpick/nitpick_scope.ML" |
206 ML_file "Tools/Nitpick/nitpick_scope.ML" |
222 use "Tools/Nitpick/nitpick_peephole.ML" |
207 ML_file "Tools/Nitpick/nitpick_peephole.ML" |
223 use "Tools/Nitpick/nitpick_rep.ML" |
208 ML_file "Tools/Nitpick/nitpick_rep.ML" |
224 use "Tools/Nitpick/nitpick_nut.ML" |
209 ML_file "Tools/Nitpick/nitpick_nut.ML" |
225 use "Tools/Nitpick/nitpick_kodkod.ML" |
210 ML_file "Tools/Nitpick/nitpick_kodkod.ML" |
226 use "Tools/Nitpick/nitpick_model.ML" |
211 ML_file "Tools/Nitpick/nitpick_model.ML" |
227 use "Tools/Nitpick/nitpick.ML" |
212 ML_file "Tools/Nitpick/nitpick.ML" |
228 use "Tools/Nitpick/nitpick_isar.ML" |
213 ML_file "Tools/Nitpick/nitpick_isar.ML" |
229 use "Tools/Nitpick/nitpick_tests.ML" |
214 ML_file "Tools/Nitpick/nitpick_tests.ML" |
230 |
215 |
231 setup {* |
216 setup {* |
232 Nitpick_Isar.setup #> |
217 Nitpick_Isar.setup #> |
233 Nitpick_HOL.register_ersatz_global |
218 Nitpick_HOL.register_ersatz_global |
234 [(@{const_name card}, @{const_name card'}), |
219 [(@{const_name card}, @{const_name card'}), |