src/HOL/Nitpick_Examples/Record_Nits.thy
 author blanchet Mon Dec 14 10:59:46 2009 +0100 (2009-12-14) changeset 34083 652719832159 parent 33197 de6285ebcc05 child 35076 cc19e2aef17e permissions -rw-r--r--
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
1 (*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
2     Author:     Jasmin Blanchette, TU Muenchen
5 Examples featuring Nitpick applied to records.
6 *)
8 header {* Examples Featuring Nitpick Applied to Records *}
10 theory Record_Nits
11 imports Main
12 begin
14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
16 record point2d =
17   xc :: int
18   yc :: int
20 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
21 nitpick [expect = none]
22 sorry
24 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
25 nitpick [expect = genuine]
26 oops
28 lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
29 nitpick [expect = genuine]
30 oops
32 lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
33 nitpick [expect = genuine]
34 oops
36 record point3d = point2d +
37   zc :: int
39 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
40 nitpick [expect = none]
41 sorry
43 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
44 nitpick [expect = genuine]
45 oops
47 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
48 nitpick [expect = genuine]
49 oops
51 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
52 nitpick [expect = genuine]
53 oops
55 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
56 nitpick [expect = genuine]
57 oops
59 record point4d = point3d +
60   wc :: int
62 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
63 nitpick [expect = none]
64 sorry
66 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
67 nitpick [expect = genuine]
68 oops
70 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
71 nitpick [expect = genuine]
72 oops
74 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
75 nitpick [expect = genuine]
76 oops
78 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
79 nitpick [expect = genuine]
80 oops
82 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
83 nitpick [expect = genuine]
84 oops
86 end