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