optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
1 (* Title: HOL/Nitpick_Examples/Datatype_Nits.thy
2 Author: Jasmin Blanchette, TU Muenchen
5 Examples featuring Nitpick applied to datatypes.
8 header {* Examples Featuring Nitpick Applied to Datatypes *}
14 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
17 "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
18 "rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" |
19 "rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" |
20 "rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" |
21 "rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" |
22 "rot NibbleF = Nibble0"
24 lemma "rot n \<noteq> n"
25 nitpick [card = 1\<midarrow>16, expect = none]
28 lemma "rot Nibble2 \<noteq> Nibble3"
29 nitpick [card = 1, expect = none]
30 nitpick [card = 2, expect = genuine]
31 nitpick [card = 2, max Nibble2 = 0, expect = none]
32 nitpick [card = 2, max Nibble3 = 0, expect = none]
35 lemma "(rot ^^ 15) n \<noteq> n"
36 nitpick [card = 17, expect = none]
39 lemma "(rot ^^ 15) n = n"
40 nitpick [card = 17, expect = genuine]
43 lemma "(rot ^^ 16) n = n"
44 nitpick [card = 17, expect = none]
47 datatype ('a, 'b) pd = Pd "'a \<times> 'b"
55 lemma "fs (Pd p) = fst p"
56 nitpick [card = 20, expect = none]
59 lemma "fs (Pd p) = snd p"
60 nitpick [expect = genuine]
63 lemma "sn (Pd p) = snd p"
64 nitpick [card = 20, expect = none]
67 lemma "sn (Pd p) = fst p"
68 nitpick [expect = genuine]
71 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
72 nitpick [card = 1\<midarrow>12, expect = none]
75 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
76 nitpick [expect = genuine]
79 datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
84 lemma "app (Fn g) y = g y"
85 nitpick [card = 1\<midarrow>12, expect = none]
88 lemma "app (Fn g) y = g' y"
89 nitpick [expect = genuine]
92 lemma "app (Fn g) y = g y'"
93 nitpick [expect = genuine]