src/HOL/Nitpick_Examples/Record_Nits.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 58889 5b7a9633cfa8 child 63167 0909deb8059b permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
```     1 (*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3     Copyright   2009-2011
```
```     4
```
```     5 Examples featuring Nitpick applied to records.
```
```     6 *)
```
```     7
```
```     8 section {* Examples Featuring Nitpick Applied to Records *}
```
```     9
```
```    10 theory Record_Nits
```
```    11 imports Main
```
```    12 begin
```
```    13
```
```    14 nitpick_params [verbose, card = 1-6, max_potential = 0,
```
```    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
```
```    16
```
```    17 record point2d =
```
```    18   xc :: int
```
```    19   yc :: int
```
```    20
```
```    21 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
```
```    22 nitpick [expect = none]
```
```    23 sorry
```
```    24
```
```    25 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
```
```    26 nitpick [expect = genuine]
```
```    27 oops
```
```    28
```
```    29 lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
```
```    30 nitpick [expect = genuine]
```
```    31 oops
```
```    32
```
```    33 lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
```
```    34 nitpick [expect = genuine]
```
```    35 oops
```
```    36
```
```    37 record point3d = point2d +
```
```    38   zc :: int
```
```    39
```
```    40 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
```
```    41 nitpick [expect = none]
```
```    42 sorry
```
```    43
```
```    44 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
```
```    45 nitpick [expect = genuine]
```
```    46 oops
```
```    47
```
```    48 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
```
```    49 nitpick [expect = genuine]
```
```    50 oops
```
```    51
```
```    52 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
```
```    53 nitpick [expect = genuine]
```
```    54 oops
```
```    55
```
```    56 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
```
```    57 nitpick [expect = genuine]
```
```    58 oops
```
```    59
```
```    60 record point4d = point3d +
```
```    61   wc :: int
```
```    62
```
```    63 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
```
```    64 nitpick [expect = none]
```
```    65 sorry
```
```    66
```
```    67 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
```
```    68 nitpick [expect = genuine]
```
```    69 oops
```
```    70
```
```    71 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
```
```    72 nitpick [expect = genuine]
```
```    73 oops
```
```    74
```
```    75 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
```
```    76 nitpick [expect = genuine]
```
```    77 oops
```
```    78
```
```    79 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
```
```    80 nitpick [expect = genuine]
```
```    81 oops
```
```    82
```
```    83 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
```
```    84 nitpick [expect = genuine]
```
```    85 oops
```
```    86
```
```    87 end
```