author | haftmann |
Mon, 04 Nov 2019 20:38:15 +0000 | |
changeset 71042 | 400e9512f1d3 |
parent 63167 | 0909deb8059b |
child 74641 | 6f801e1073fa |
permissions | -rw-r--r-- |
33197 | 1 |
(* Title: HOL/Nitpick_Examples/Datatype_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
45035 | 3 |
Copyright 2009-2011 |
33197 | 4 |
|
5 |
Examples featuring Nitpick applied to datatypes. |
|
6 |
*) |
|
7 |
||
63167 | 8 |
section \<open>Examples Featuring Nitpick Applied to Datatypes\<close> |
33197 | 9 |
|
10 |
theory Datatype_Nits |
|
11 |
imports Main |
|
12 |
begin |
|
13 |
||
55893
aed17a173d16
fixed handling of 'case_prod' and other 'case' functions for interpreted types
blanchet
parents:
54680
diff
changeset
|
14 |
nitpick_params [verbose, card = 1-8, max_potential = 0, |
54680
93f6d33a754e
reverted 86e0b402994c, which was accidentally qfinish'ed and pushed
blanchet
parents:
54633
diff
changeset
|
15 |
sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |
34083
652719832159
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
blanchet
parents:
33199
diff
changeset
|
16 |
|
62597 | 17 |
datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 |
18 |
| Nibble4 | Nibble5 | Nibble6 | Nibble7 |
|
19 |
| Nibble8 | Nibble9 | NibbleA | NibbleB |
|
20 |
| NibbleC | NibbleD | NibbleE | NibbleF |
|
21 |
||
33197 | 22 |
primrec rot where |
34126 | 23 |
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" | |
24 |
"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" | |
|
25 |
"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" | |
|
26 |
"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" | |
|
27 |
"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" | |
|
33197 | 28 |
"rot NibbleF = Nibble0" |
29 |
||
30 |
lemma "rot n \<noteq> n" |
|
55893
aed17a173d16
fixed handling of 'case_prod' and other 'case' functions for interpreted types
blanchet
parents:
54680
diff
changeset
|
31 |
nitpick [card = 1-8,16, verbose, expect = none] |
33197 | 32 |
sorry |
33 |
||
34 |
lemma "rot Nibble2 \<noteq> Nibble3" |
|
35 |
nitpick [card = 1, expect = none] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
36 |
nitpick [card = 2, max Nibble4 = 0, expect = genuine] |
33197 | 37 |
nitpick [card = 2, max Nibble2 = 0, expect = none] |
38 |
oops |
|
39 |
||
33199 | 40 |
lemma "(rot ^^ 15) n \<noteq> n" |
33197 | 41 |
nitpick [card = 17, expect = none] |
42 |
sorry |
|
43 |
||
33199 | 44 |
lemma "(rot ^^ 15) n = n" |
33197 | 45 |
nitpick [card = 17, expect = genuine] |
46 |
oops |
|
47 |
||
33199 | 48 |
lemma "(rot ^^ 16) n = n" |
33197 | 49 |
nitpick [card = 17, expect = none] |
50 |
oops |
|
51 |
||
58310 | 52 |
datatype ('a, 'b) pd = Pd "'a \<times> 'b" |
33197 | 53 |
|
54 |
fun fs where |
|
55 |
"fs (Pd (a, _)) = a" |
|
56 |
||
57 |
fun sn where |
|
58 |
"sn (Pd (_, b)) = b" |
|
59 |
||
60 |
lemma "fs (Pd p) = fst p" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
61 |
nitpick [card = 12, expect = none] |
33197 | 62 |
sorry |
63 |
||
64 |
lemma "fs (Pd p) = snd p" |
|
65 |
nitpick [expect = genuine] |
|
66 |
oops |
|
67 |
||
68 |
lemma "sn (Pd p) = snd p" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
69 |
nitpick [card = 12, expect = none] |
33197 | 70 |
sorry |
71 |
||
72 |
lemma "sn (Pd p) = fst p" |
|
73 |
nitpick [expect = genuine] |
|
74 |
oops |
|
75 |
||
76 |
lemma "fs (Pd ((a, b), (c, d))) = (a, b)" |
|
40410
8adcdd2c5805
make Nitpick datatype tests faster to make timeout less likely
blanchet
parents:
40341
diff
changeset
|
77 |
nitpick [expect = none] |
33197 | 78 |
sorry |
79 |
||
80 |
lemma "fs (Pd ((a, b), (c, d))) = (c, d)" |
|
81 |
nitpick [expect = genuine] |
|
82 |
oops |
|
83 |
||
58310 | 84 |
datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b" |
33197 | 85 |
|
86 |
fun app where |
|
87 |
"app (Fn f) x = f x" |
|
88 |
||
89 |
lemma "app (Fn g) y = g y" |
|
40410
8adcdd2c5805
make Nitpick datatype tests faster to make timeout less likely
blanchet
parents:
40341
diff
changeset
|
90 |
nitpick [expect = none] |
33197 | 91 |
sorry |
92 |
||
93 |
lemma "app (Fn g) y = g' y" |
|
94 |
nitpick [expect = genuine] |
|
95 |
oops |
|
96 |
||
97 |
lemma "app (Fn g) y = g y'" |
|
98 |
nitpick [expect = genuine] |
|
99 |
oops |
|
100 |
||
101 |
end |