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
```
```     3     Copyright   2009
```
```     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
```
```    14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
```
```    15
```
```    16 record point2d =
```
```    17   xc :: int
```
```    18   yc :: int
```
```    19
```
```    20 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
```
```    21 nitpick [expect = none]
```
```    22 sorry
```
```    23
```
```    24 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
```
```    25 nitpick [expect = genuine]
```
```    26 oops
```
```    27
```
```    28 lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
```
```    29 nitpick [expect = genuine]
```
```    30 oops
```
```    31
```
```    32 lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
```
```    33 nitpick [expect = genuine]
```
```    34 oops
```
```    35
```
```    36 record point3d = point2d +
```
```    37   zc :: int
```
```    38
```
```    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
```
```    42
```
```    43 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
```
```    44 nitpick [expect = genuine]
```
```    45 oops
```
```    46
```
```    47 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
```
```    48 nitpick [expect = genuine]
```
```    49 oops
```
```    50
```
```    51 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
```
```    52 nitpick [expect = genuine]
```
```    53 oops
```
```    54
```
```    55 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
```
```    56 nitpick [expect = genuine]
```
```    57 oops
```
```    58
```
```    59 record point4d = point3d +
```
```    60   wc :: int
```
```    61
```
```    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
```
```    65
```
```    66 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
```
```    67 nitpick [expect = genuine]
```
```    68 oops
```
```    69
```
```    70 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
```
```    71 nitpick [expect = genuine]
```
```    72 oops
```
```    73
```
```    74 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
```
```    75 nitpick [expect = genuine]
```
```    76 oops
```
```    77
```
```    78 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
```
```    79 nitpick [expect = genuine]
```
```    80 oops
```
```    81
```
```    82 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
```
```    83 nitpick [expect = genuine]
```
```    84 oops
```
```    85
```
```    86 end
```