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