summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Nitpick_Examples/Record_Nits.thy

changeset 33197 | de6285ebcc05 |

child 34083 | 652719832159 |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Fri Oct 23 18:59:24 2009 +0200 1.3 @@ -0,0 +1,84 @@ 1.4 +(* Title: HOL/Nitpick_Examples/Record_Nits.thy 1.5 + Author: Jasmin Blanchette, TU Muenchen 1.6 + Copyright 2009 1.7 + 1.8 +Examples featuring Nitpick applied to records. 1.9 +*) 1.10 + 1.11 +header {* Examples Featuring Nitpick Applied to Records *} 1.12 + 1.13 +theory Record_Nits 1.14 +imports Main 1.15 +begin 1.16 + 1.17 +record point2d = 1.18 + xc :: int 1.19 + yc :: int 1.20 + 1.21 +lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>" 1.22 +nitpick [expect = none] 1.23 +sorry 1.24 + 1.25 +lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>" 1.26 +nitpick [expect = genuine] 1.27 +oops 1.28 + 1.29 +lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p" 1.30 +nitpick [expect = genuine] 1.31 +oops 1.32 + 1.33 +lemma "p\<lparr>xc := x, yc := y\<rparr> = p" 1.34 +nitpick [expect = genuine] 1.35 +oops 1.36 + 1.37 +record point3d = point2d + 1.38 + zc :: int 1.39 + 1.40 +lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>" 1.41 +nitpick [expect = none] 1.42 +sorry 1.43 + 1.44 +lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>" 1.45 +nitpick [expect = genuine] 1.46 +oops 1.47 + 1.48 +lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>" 1.49 +nitpick [expect = genuine] 1.50 +oops 1.51 + 1.52 +lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p" 1.53 +nitpick [expect = genuine] 1.54 +oops 1.55 + 1.56 +lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p" 1.57 +nitpick [expect = genuine] 1.58 +oops 1.59 + 1.60 +record point4d = point3d + 1.61 + wc :: int 1.62 + 1.63 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>" 1.64 +nitpick [expect = none] 1.65 +sorry 1.66 + 1.67 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>" 1.68 +nitpick [expect = genuine] 1.69 +oops 1.70 + 1.71 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>" 1.72 +nitpick [expect = genuine] 1.73 +oops 1.74 + 1.75 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>" 1.76 +nitpick [expect = genuine] 1.77 +oops 1.78 + 1.79 +lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p" 1.80 +nitpick [expect = genuine] 1.81 +oops 1.82 + 1.83 +lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p" 1.84 +nitpick [expect = genuine] 1.85 +oops 1.86 + 1.87 +end