author | haftmann |
Sun, 19 Feb 2012 15:30:35 +0100 | |
changeset 46553 | 50a7e97fe653 |
parent 45035 | 60d2c03d5c70 |
child 54633 | 86e0b402994c |
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 |
||
8 |
header {* Examples Featuring Nitpick Applied to Datatypes *} |
|
9 |
||
10 |
theory Datatype_Nits |
|
11 |
imports Main |
|
12 |
begin |
|
13 |
||
42959 | 14 |
nitpick_params [verbose, card = 1\<emdash>8, max_potential = 0, |
42208
02513eb26eb7
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
krauss
parents:
41278
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 |
|
33197 | 17 |
primrec rot where |
34126 | 18 |
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" | |
19 |
"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" | |
|
20 |
"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" | |
|
21 |
"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" | |
|
22 |
"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" | |
|
33197 | 23 |
"rot NibbleF = Nibble0" |
24 |
||
25 |
lemma "rot n \<noteq> n" |
|
42959 | 26 |
nitpick [card = 1\<emdash>8,16, verbose, expect = none] |
33197 | 27 |
sorry |
28 |
||
29 |
lemma "rot Nibble2 \<noteq> Nibble3" |
|
30 |
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
|
31 |
nitpick [card = 2, max Nibble4 = 0, expect = genuine] |
33197 | 32 |
nitpick [card = 2, max Nibble2 = 0, expect = none] |
33 |
oops |
|
34 |
||
33199 | 35 |
lemma "(rot ^^ 15) n \<noteq> n" |
33197 | 36 |
nitpick [card = 17, expect = none] |
37 |
sorry |
|
38 |
||
33199 | 39 |
lemma "(rot ^^ 15) n = n" |
33197 | 40 |
nitpick [card = 17, expect = genuine] |
41 |
oops |
|
42 |
||
33199 | 43 |
lemma "(rot ^^ 16) n = n" |
33197 | 44 |
nitpick [card = 17, expect = none] |
45 |
oops |
|
46 |
||
47 |
datatype ('a, 'b) pd = Pd "'a \<times> 'b" |
|
48 |
||
49 |
fun fs where |
|
50 |
"fs (Pd (a, _)) = a" |
|
51 |
||
52 |
fun sn where |
|
53 |
"sn (Pd (_, b)) = b" |
|
54 |
||
55 |
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
|
56 |
nitpick [card = 12, expect = none] |
33197 | 57 |
sorry |
58 |
||
59 |
lemma "fs (Pd p) = snd p" |
|
60 |
nitpick [expect = genuine] |
|
61 |
oops |
|
62 |
||
63 |
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
|
64 |
nitpick [card = 12, expect = none] |
33197 | 65 |
sorry |
66 |
||
67 |
lemma "sn (Pd p) = fst p" |
|
68 |
nitpick [expect = genuine] |
|
69 |
oops |
|
70 |
||
71 |
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
|
72 |
nitpick [expect = none] |
33197 | 73 |
sorry |
74 |
||
75 |
lemma "fs (Pd ((a, b), (c, d))) = (c, d)" |
|
76 |
nitpick [expect = genuine] |
|
77 |
oops |
|
78 |
||
79 |
datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b" |
|
80 |
||
81 |
fun app where |
|
82 |
"app (Fn f) x = f x" |
|
83 |
||
84 |
lemma "app (Fn g) y = g y" |
|
40410
8adcdd2c5805
make Nitpick datatype tests faster to make timeout less likely
blanchet
parents:
40341
diff
changeset
|
85 |
nitpick [expect = none] |
33197 | 86 |
sorry |
87 |
||
88 |
lemma "app (Fn g) y = g' y" |
|
89 |
nitpick [expect = genuine] |
|
90 |
oops |
|
91 |
||
92 |
lemma "app (Fn g) y = g y'" |
|
93 |
nitpick [expect = genuine] |
|
94 |
oops |
|
95 |
||
96 |
end |