enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
1 (* Title: HOL/Nitpick_Examples/Record_Nits.thy
2 Author: Jasmin Blanchette, TU Muenchen
5 Examples featuring Nitpick applied to records.
8 header {* Examples Featuring Nitpick Applied to Records *}
14 nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
21 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
22 nitpick [expect = none]
25 lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
26 nitpick [expect = genuine]
29 lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
30 nitpick [expect = genuine]
33 lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
34 nitpick [expect = genuine]
37 record point3d = point2d +
40 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
41 nitpick [expect = none]
44 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
45 nitpick [expect = genuine]
48 lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
49 nitpick [expect = genuine]
52 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
53 nitpick [expect = genuine]
56 lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
57 nitpick [expect = genuine]
60 record point4d = point3d +
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]
67 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
68 nitpick [expect = genuine]
71 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
72 nitpick [expect = genuine]
75 lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
76 nitpick [expect = genuine]
79 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
80 nitpick [expect = genuine]
83 lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
84 nitpick [expect = genuine]