| author | wenzelm |
| Fri, 03 Aug 2012 13:55:51 +0200 | |
| changeset 48660 | 730ca503e955 |
| parent 48046 | 359bec38a4ee |
| child 48812 | 9509fc5485b2 |
| permissions | -rw-r--r-- |
| 33197 | 1 |
(* Title: HOL/Nitpick_Examples/Record_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
| 45035 | 3 |
Copyright 2009-2011 |
| 33197 | 4 |
|
5 |
Examples featuring Nitpick applied to records. |
|
6 |
*) |
|
7 |
||
8 |
header {* Examples Featuring Nitpick Applied to Records *}
|
|
9 |
||
10 |
theory Record_Nits |
|
11 |
imports Main |
|
12 |
begin |
|
13 |
||
| 42959 | 14 |
nitpick_params [verbose, card = 1\<emdash>6, 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:
33197
diff
changeset
|
16 |
|
| 33197 | 17 |
record point2d = |
18 |
xc :: int |
|
19 |
yc :: int |
|
20 |
||
|
48046
359bec38a4ee
temporarily comment out nitpick examples broken by changes to Int.thy
huffman
parents:
45035
diff
changeset
|
21 |
(* FIXME: Invalid intermediate term |
| 33197 | 22 |
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>" |
23 |
nitpick [expect = none] |
|
24 |
sorry |
|
25 |
||
26 |
lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>" |
|
27 |
nitpick [expect = genuine] |
|
28 |
oops |
|
29 |
||
30 |
lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p" |
|
31 |
nitpick [expect = genuine] |
|
32 |
oops |
|
33 |
||
34 |
lemma "p\<lparr>xc := x, yc := y\<rparr> = p" |
|
35 |
nitpick [expect = genuine] |
|
36 |
oops |
|
37 |
||
38 |
record point3d = point2d + |
|
39 |
zc :: int |
|
40 |
||
41 |
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>" |
|
42 |
nitpick [expect = none] |
|
43 |
sorry |
|
44 |
||
45 |
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>" |
|
46 |
nitpick [expect = genuine] |
|
47 |
oops |
|
48 |
||
49 |
lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>" |
|
50 |
nitpick [expect = genuine] |
|
51 |
oops |
|
52 |
||
53 |
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p" |
|
54 |
nitpick [expect = genuine] |
|
55 |
oops |
|
56 |
||
57 |
lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p" |
|
58 |
nitpick [expect = genuine] |
|
59 |
oops |
|
60 |
||
61 |
record point4d = point3d + |
|
62 |
wc :: int |
|
63 |
||
64 |
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>" |
|
65 |
nitpick [expect = none] |
|
66 |
sorry |
|
67 |
||
68 |
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>" |
|
69 |
nitpick [expect = genuine] |
|
70 |
oops |
|
71 |
||
72 |
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>" |
|
73 |
nitpick [expect = genuine] |
|
74 |
oops |
|
75 |
||
76 |
lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>" |
|
77 |
nitpick [expect = genuine] |
|
78 |
oops |
|
79 |
||
80 |
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p" |
|
81 |
nitpick [expect = genuine] |
|
82 |
oops |
|
83 |
||
84 |
lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p" |
|
85 |
nitpick [expect = genuine] |
|
86 |
oops |
|
|
48046
359bec38a4ee
temporarily comment out nitpick examples broken by changes to Int.thy
huffman
parents:
45035
diff
changeset
|
87 |
*) |
| 33197 | 88 |
|
89 |
end |