src/HOL/Nitpick_Examples/Pattern_Nits.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 63167 0909deb8059b permissions -rw-r--r--
tuned: each session has at most one defining entry;
1 (*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
2     Author:     Jasmin Blanchette, TU Muenchen
5 Examples featuring Nitpick's "destroy_constrs" optimization.
6 *)
8 section \<open>Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization\<close>
10 theory Pattern_Nits
11 imports Main
12 begin
14 nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = MiniSat_JNI,
15                 max_threads = 1, timeout = 240]
17 lemma "x = (case u of () \<Rightarrow> y)"
18 nitpick [expect = genuine]
19 oops
21 lemma "x = (case b of True \<Rightarrow> x | False \<Rightarrow> y)"
22 nitpick [expect = genuine]
23 oops
25 lemma "x = (case p of (x, y) \<Rightarrow> y)"
26 nitpick [expect = genuine]
27 oops
29 lemma "x = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> n)"
30 nitpick [expect = genuine]
31 oops
33 lemma "x = (case opt of None \<Rightarrow> x | Some y \<Rightarrow> y)"
34 nitpick [expect = genuine]
35 oops
37 lemma "x = (case xs of [] \<Rightarrow> x | y # ys \<Rightarrow> y)"
38 nitpick [expect = genuine]
39 oops
41 lemma "x = (case xs of
42               [] \<Rightarrow> x
43             | y # ys \<Rightarrow>
44               (case ys of
45                  [] \<Rightarrow> x
46                | z # zs \<Rightarrow>
47                  (case z of
48                     None \<Rightarrow> x
49                   | Some p \<Rightarrow>
50                     (case p of
51                        (a, b) \<Rightarrow> b))))"
52 nitpick [expect = genuine]
53 oops
55 fun f1 where
56 "f1 x () = x"
58 lemma "x = f1 y u"
59 nitpick [expect = genuine]
60 oops
62 fun f2 where
63 "f2 x _ True = x" |
64 "f2 _ y False = y"
66 lemma "x = f2 x y b"
67 nitpick [expect = genuine]
68 oops
70 fun f3 where
71 "f3 (_, y) = y"
73 lemma "x = f3 p"
74 nitpick [expect = genuine]
75 oops
77 fun f4 where
78 "f4 x 0 = x" |
79 "f4 _ (Suc n) = n"
81 lemma "x = f4 x n"
82 nitpick [expect = genuine]
83 oops
85 fun f5 where
86 "f5 x None = x" |
87 "f5 _ (Some y) = y"
89 lemma "x = f5 x opt"
90 nitpick [expect = genuine]
91 oops
93 fun f6 where
94 "f6 x [] = x" |
95 "f6 _ (y # ys) = y"
97 lemma "x = f6 x xs"
98 nitpick [expect = genuine]
99 oops
101 fun f7 where
102 "f7 _ (y # Some (a, b) # zs) = b" |
103 "f7 x (y # None # zs) = x" |
104 "f7 x [y] = x" |
105 "f7 x [] = x"
107 lemma "x = f7 x xs"
108 nitpick [expect = genuine]
109 oops
111 lemma "u = ()"
112 nitpick [expect = none]
113 sorry
115 lemma "\<exists>y. (b::bool) = y"
116 nitpick [expect = none]
117 sorry
119 lemma "\<exists>x y. p = (x, y)"
120 nitpick [expect = none]
121 sorry
123 lemma "\<exists>x. n = Suc x"
124 nitpick [expect = genuine]
125 oops
127 lemma "\<exists>y. x = Some y"
128 nitpick [expect = genuine]
129 oops
131 lemma "\<exists>y ys. xs = y # ys"
132 nitpick [expect = genuine]
133 oops
135 lemma "\<exists>y a b zs. x = y # Some (a, b) # zs"
136 nitpick [expect = genuine]
137 oops
139 end