author | wenzelm |
Sat, 25 Feb 2012 12:34:56 +0100 | |
changeset 46665 | 919dfcdf6d8a |
parent 46087 | 680edc162249 |
child 54633 | 86e0b402994c |
permissions | -rw-r--r-- |
33197 | 1 |
(* Title: HOL/Nitpick_Examples/Core_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
45035 | 3 |
Copyright 2009-2011 |
33197 | 4 |
|
5 |
Examples featuring Nitpick's functional core. |
|
6 |
*) |
|
7 |
||
8 |
header {* Examples Featuring Nitpick's Functional Core *} |
|
9 |
||
10 |
theory Core_Nits |
|
11 |
imports Main |
|
12 |
begin |
|
13 |
||
42959 | 14 |
nitpick_params [verbose, card = 1\<emdash>6, unary_ints, max_potential = 0, |
42208
02513eb26eb7
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
krauss
parents:
41278
diff
changeset
|
15 |
sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] |
34082
61b7aa37f4b7
make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
blanchet
parents:
33199
diff
changeset
|
16 |
|
33197 | 17 |
subsection {* Curry in a Hurry *} |
18 |
||
19 |
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)" |
|
42959 | 20 |
nitpick [card = 1\<emdash>12, expect = none] |
33197 | 21 |
by auto |
22 |
||
23 |
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)" |
|
42959 | 24 |
nitpick [card = 1\<emdash>12, expect = none] |
33197 | 25 |
by auto |
26 |
||
27 |
lemma "split (curry f) = f" |
|
42959 | 28 |
nitpick [card = 1\<emdash>12, expect = none] |
33197 | 29 |
by auto |
30 |
||
31 |
lemma "curry (split f) = f" |
|
42959 | 32 |
nitpick [card = 1\<emdash>12, expect = none] |
33197 | 33 |
by auto |
34 |
||
35 |
lemma "split (\<lambda>x y. f (x, y)) = f" |
|
42959 | 36 |
nitpick [card = 1\<emdash>12, expect = none] |
33197 | 37 |
by auto |
38 |
||
39 |
subsection {* Representations *} |
|
40 |
||
41 |
lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y" |
|
42 |
nitpick [expect = none] |
|
43 |
by auto |
|
44 |
||
45 |
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
46 |
nitpick [card 'a = 25, card 'b = 24, expect = genuine] |
42959 | 47 |
nitpick [card = 1\<emdash>10, mono, expect = none] |
33197 | 48 |
oops |
49 |
||
50 |
lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y" |
|
51 |
nitpick [card = 1, expect = genuine] |
|
52 |
oops |
|
53 |
||
54 |
lemma "P (\<lambda>x. x)" |
|
55 |
nitpick [card = 1, expect = genuine] |
|
56 |
oops |
|
57 |
||
58 |
lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}" |
|
42959 | 59 |
nitpick [card = 1\<emdash>12, expect = none] |
33197 | 60 |
by auto |
61 |
||
62 |
lemma "fst (a, b) = a" |
|
42959 | 63 |
nitpick [card = 1\<emdash>20, expect = none] |
33197 | 64 |
by auto |
65 |
||
66 |
lemma "\<exists>P. P = Id" |
|
42959 | 67 |
nitpick [card = 1\<emdash>20, expect = none] |
33197 | 68 |
by auto |
69 |
||
70 |
lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*" |
|
46085
447cda88adfe
fixed a few more bugs in \Nitpick's new "set" support
blanchet
parents:
45970
diff
changeset
|
71 |
nitpick [card = 1\<emdash>2, expect = none] |
33197 | 72 |
by auto |
73 |
||
74 |
lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*" |
|
42959 | 75 |
nitpick [card = 1\<emdash>4, expect = none] |
33197 | 76 |
by auto |
77 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
78 |
lemma "(a, a) \<in> Id" |
42959 | 79 |
nitpick [card = 1\<emdash>50, expect = none] |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
80 |
by (auto simp: Id_def) |
33197 | 81 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
82 |
lemma "((a\<Colon>'a, b\<Colon>'a), (a, b)) \<in> Id" |
42959 | 83 |
nitpick [card = 1\<emdash>10, expect = none] |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
84 |
by (auto simp: Id_def) |
33197 | 85 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
86 |
lemma "(x\<Colon>'a\<times>'a) \<in> UNIV" |
42959 | 87 |
nitpick [card = 1\<emdash>50, expect = none] |
33197 | 88 |
sorry |
89 |
||
90 |
lemma "{} = A - A" |
|
42959 | 91 |
nitpick [card = 1\<emdash>100, expect = none] |
33197 | 92 |
by auto |
93 |
||
94 |
lemma "g = Let (A \<or> B)" |
|
95 |
nitpick [card = 1, expect = none] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
96 |
nitpick [card = 12, expect = genuine] |
33197 | 97 |
oops |
98 |
||
99 |
lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)" |
|
100 |
nitpick [expect = none] |
|
101 |
by auto |
|
102 |
||
103 |
lemma "A \<subseteq> B" |
|
104 |
nitpick [card = 100, expect = genuine] |
|
105 |
oops |
|
106 |
||
107 |
lemma "A = {b}" |
|
108 |
nitpick [card = 100, expect = genuine] |
|
109 |
oops |
|
110 |
||
111 |
lemma "{a, b} = {b}" |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
112 |
nitpick [card = 50, expect = genuine] |
33197 | 113 |
oops |
114 |
||
115 |
lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R" |
|
116 |
nitpick [card = 1, expect = genuine] |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
117 |
nitpick [card = 10, expect = genuine] |
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
118 |
nitpick [card = 5, dont_box, expect = genuine] |
33197 | 119 |
oops |
120 |
||
121 |
lemma "f (g\<Colon>'a\<Rightarrow>'a) = x" |
|
122 |
nitpick [card = 3, dont_box, expect = genuine] |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
123 |
nitpick [card = 8, expect = genuine] |
33197 | 124 |
oops |
125 |
||
126 |
lemma "f (a, b) = x" |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
127 |
nitpick [card = 10, expect = genuine] |
33197 | 128 |
oops |
129 |
||
130 |
lemma "f (a, a) = f (c, d)" |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
131 |
nitpick [card = 10, expect = genuine] |
33197 | 132 |
oops |
133 |
||
134 |
lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True" |
|
42959 | 135 |
nitpick [card = 1\<emdash>10, expect = none] |
33197 | 136 |
by auto |
137 |
||
138 |
lemma "\<exists>F. F a b = G a b" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
139 |
nitpick [card = 2, expect = none] |
33197 | 140 |
by auto |
141 |
||
142 |
lemma "f = split" |
|
143 |
nitpick [card = 2, expect = genuine] |
|
144 |
oops |
|
145 |
||
146 |
lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R" |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
147 |
nitpick [card = 15, expect = none] |
33197 | 148 |
by auto |
149 |
||
46085
447cda88adfe
fixed a few more bugs in \Nitpick's new "set" support
blanchet
parents:
45970
diff
changeset
|
150 |
lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> |
33197 | 151 |
A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)" |
42959 | 152 |
nitpick [card = 1\<emdash>25, expect = none] |
33197 | 153 |
by auto |
154 |
||
155 |
lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)" |
|
156 |
nitpick [card = 8, expect = genuine] |
|
157 |
oops |
|
158 |
||
159 |
subsection {* Quantifiers *} |
|
160 |
||
161 |
lemma "x = y" |
|
162 |
nitpick [card 'a = 1, expect = none] |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
163 |
nitpick [card 'a = 100, expect = genuine] |
33197 | 164 |
oops |
165 |
||
166 |
lemma "\<forall>x. x = y" |
|
167 |
nitpick [card 'a = 1, expect = none] |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
168 |
nitpick [card 'a = 100, expect = genuine] |
33197 | 169 |
oops |
170 |
||
171 |
lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y" |
|
172 |
nitpick [card 'a = 1, expect = genuine] |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
173 |
nitpick [card 'a = 100, expect = genuine] |
33197 | 174 |
oops |
175 |
||
176 |
lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y" |
|
42959 | 177 |
nitpick [card 'a = 1\<emdash>15, expect = none] |
33197 | 178 |
by auto |
179 |
||
180 |
lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y" |
|
42959 | 181 |
nitpick [card = 1\<emdash>15, expect = none] |
33197 | 182 |
by auto |
183 |
||
184 |
lemma "\<forall>x. \<exists>y. f x y = f x (g x)" |
|
42959 | 185 |
nitpick [card = 1\<emdash>4, expect = none] |
33197 | 186 |
by auto |
187 |
||
188 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)" |
|
42959 | 189 |
nitpick [card = 1\<emdash>4, expect = none] |
33197 | 190 |
by auto |
191 |
||
192 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)" |
|
193 |
nitpick [card = 3, expect = genuine] |
|
194 |
oops |
|
195 |
||
196 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
197 |
f u v w x y z = f u (g u) w (h u w) y (k u w y)" |
|
42959 | 198 |
nitpick [card = 1\<emdash>2, expect = none] |
33197 | 199 |
sorry |
200 |
||
201 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
202 |
f u v w x y z = f u (g u) w (h u w y) y (k u w y)" |
|
42959 | 203 |
nitpick [card = 1\<emdash>2, expect = genuine] |
33197 | 204 |
oops |
205 |
||
206 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
207 |
f u v w x y z = f u (g u w) w (h u w) y (k u w y)" |
|
42959 | 208 |
nitpick [card = 1\<emdash>2, expect = genuine] |
33197 | 209 |
oops |
210 |
||
211 |
lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f. |
|
212 |
f u v w x = f u (g u) w (h u w)" |
|
42959 | 213 |
nitpick [card = 1\<emdash>2, expect = none] |
33197 | 214 |
sorry |
215 |
||
216 |
lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f. |
|
217 |
f u v w x = f u (g u w) w (h u)" |
|
42959 | 218 |
nitpick [card = 1\<emdash>2, dont_box, expect = genuine] |
33197 | 219 |
oops |
220 |
||
221 |
lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f. |
|
222 |
f u v w x = f u (g u) w (h u w)" |
|
42959 | 223 |
nitpick [card = 1\<emdash>2, dont_box, expect = none] |
33197 | 224 |
sorry |
225 |
||
226 |
lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f. |
|
227 |
f u v w x = f u (g u w) w (h u)" |
|
42959 | 228 |
nitpick [card = 1\<emdash>2, dont_box, expect = genuine] |
33197 | 229 |
oops |
230 |
||
231 |
lemma "\<forall>x. if (\<forall>y. x = y) then False else True" |
|
232 |
nitpick [card = 1, expect = genuine] |
|
42959 | 233 |
nitpick [card = 2\<emdash>5, expect = none] |
33197 | 234 |
oops |
235 |
||
236 |
lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True" |
|
237 |
nitpick [card = 1, expect = genuine] |
|
238 |
nitpick [card = 2, expect = none] |
|
239 |
oops |
|
240 |
||
241 |
lemma "\<forall>x. if (\<exists>y. x = y) then True else False" |
|
242 |
nitpick [expect = none] |
|
243 |
sorry |
|
244 |
||
245 |
lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)" |
|
246 |
nitpick [card 'a = 1, expect = genuine] |
|
247 |
oops |
|
248 |
||
249 |
lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) |
|
250 |
else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
251 |
nitpick [expect = none] |
|
252 |
by auto |
|
253 |
||
254 |
lemma "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) |
|
255 |
else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
256 |
nitpick [expect = none] |
|
257 |
by auto |
|
258 |
||
259 |
lemma "let x = (\<forall>x. P x) in if x then x else \<not> x" |
|
260 |
nitpick [expect = none] |
|
261 |
by auto |
|
262 |
||
263 |
lemma "let x = (\<forall>x\<Colon>'a \<times> 'b. P x) in if x then x else \<not> x" |
|
264 |
nitpick [expect = none] |
|
265 |
by auto |
|
266 |
||
267 |
subsection {* Schematic Variables *} |
|
268 |
||
36319 | 269 |
schematic_lemma "x = ?x" |
33197 | 270 |
nitpick [expect = none] |
271 |
by auto |
|
272 |
||
36319 | 273 |
schematic_lemma "\<forall>x. x = ?x" |
33197 | 274 |
nitpick [expect = genuine] |
275 |
oops |
|
276 |
||
36319 | 277 |
schematic_lemma "\<exists>x. x = ?x" |
33197 | 278 |
nitpick [expect = none] |
279 |
by auto |
|
280 |
||
36319 | 281 |
schematic_lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x" |
33197 | 282 |
nitpick [expect = none] |
283 |
by auto |
|
284 |
||
36319 | 285 |
schematic_lemma "\<forall>x. ?x = ?y" |
33197 | 286 |
nitpick [expect = none] |
287 |
by auto |
|
288 |
||
36319 | 289 |
schematic_lemma "\<exists>x. ?x = ?y" |
33197 | 290 |
nitpick [expect = none] |
291 |
by auto |
|
292 |
||
293 |
subsection {* Known Constants *} |
|
294 |
||
295 |
lemma "x \<equiv> all \<Longrightarrow> False" |
|
296 |
nitpick [card = 1, expect = genuine] |
|
297 |
nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
298 |
nitpick [card = 6, expect = genuine] |
33197 | 299 |
oops |
300 |
||
301 |
lemma "\<And>x. f x y = f x y" |
|
302 |
nitpick [expect = none] |
|
303 |
oops |
|
304 |
||
305 |
lemma "\<And>x. f x y = f y x" |
|
306 |
nitpick [expect = genuine] |
|
307 |
oops |
|
308 |
||
309 |
lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True" |
|
310 |
nitpick [expect = none] |
|
311 |
by auto |
|
312 |
||
313 |
lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False" |
|
314 |
nitpick [expect = genuine] |
|
315 |
oops |
|
316 |
||
317 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))" |
|
318 |
nitpick [expect = none] |
|
319 |
by auto |
|
320 |
||
321 |
lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False" |
|
322 |
nitpick [card = 1, expect = genuine] |
|
323 |
oops |
|
324 |
||
325 |
lemma "P x \<equiv> P x" |
|
42959 | 326 |
nitpick [card = 1\<emdash>10, expect = none] |
33197 | 327 |
by auto |
328 |
||
329 |
lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x" |
|
42959 | 330 |
nitpick [card = 1\<emdash>10, expect = none] |
33197 | 331 |
by auto |
332 |
||
333 |
lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x" |
|
42959 | 334 |
nitpick [card = 1\<emdash>10, expect = none] |
33197 | 335 |
by auto |
336 |
||
337 |
lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False" |
|
338 |
nitpick [expect = genuine] |
|
339 |
oops |
|
340 |
||
341 |
lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))" |
|
342 |
nitpick [expect = none] |
|
343 |
by auto |
|
344 |
||
345 |
lemma "P x \<Longrightarrow> P x" |
|
42959 | 346 |
nitpick [card = 1\<emdash>10, expect = none] |
33197 | 347 |
by auto |
348 |
||
349 |
lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False" |
|
350 |
nitpick [expect = none] |
|
351 |
by auto |
|
352 |
||
353 |
lemma "True \<Longrightarrow> False" |
|
354 |
nitpick [expect = genuine] |
|
355 |
oops |
|
356 |
||
357 |
lemma "x = Not" |
|
358 |
nitpick [expect = genuine] |
|
359 |
oops |
|
360 |
||
361 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))" |
|
362 |
nitpick [expect = none] |
|
363 |
by auto |
|
364 |
||
365 |
lemma "x = True" |
|
366 |
nitpick [expect = genuine] |
|
367 |
oops |
|
368 |
||
369 |
lemma "x = False" |
|
370 |
nitpick [expect = genuine] |
|
371 |
oops |
|
372 |
||
373 |
lemma "x = undefined" |
|
374 |
nitpick [expect = genuine] |
|
375 |
oops |
|
376 |
||
377 |
lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined" |
|
378 |
nitpick [expect = genuine] |
|
379 |
oops |
|
380 |
||
381 |
lemma "undefined = undefined" |
|
382 |
nitpick [expect = none] |
|
383 |
by auto |
|
384 |
||
385 |
lemma "f undefined = f undefined" |
|
386 |
nitpick [expect = none] |
|
387 |
by auto |
|
388 |
||
389 |
lemma "f undefined = g undefined" |
|
390 |
nitpick [card = 33, expect = genuine] |
|
391 |
oops |
|
392 |
||
393 |
lemma "\<exists>!x. x = undefined" |
|
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
38185
diff
changeset
|
394 |
nitpick [card = 15, expect = none] |
33197 | 395 |
by auto |
396 |
||
397 |
lemma "x = All \<Longrightarrow> False" |
|
398 |
nitpick [card = 1, dont_box, expect = genuine] |
|
399 |
oops |
|
400 |
||
401 |
lemma "\<forall>x. f x y = f x y" |
|
402 |
nitpick [expect = none] |
|
403 |
oops |
|
404 |
||
405 |
lemma "\<forall>x. f x y = f y x" |
|
406 |
nitpick [expect = genuine] |
|
407 |
oops |
|
408 |
||
409 |
lemma "All (\<lambda>x. f x y = f x y) = True" |
|
410 |
nitpick [expect = none] |
|
411 |
by auto |
|
412 |
||
413 |
lemma "All (\<lambda>x. f x y = f x y) = False" |
|
414 |
nitpick [expect = genuine] |
|
415 |
oops |
|
416 |
||
417 |
lemma "x = Ex \<Longrightarrow> False" |
|
418 |
nitpick [card = 1, dont_box, expect = genuine] |
|
419 |
oops |
|
420 |
||
421 |
lemma "\<exists>x. f x y = f x y" |
|
422 |
nitpick [expect = none] |
|
423 |
oops |
|
424 |
||
425 |
lemma "\<exists>x. f x y = f y x" |
|
426 |
nitpick [expect = none] |
|
427 |
oops |
|
428 |
||
429 |
lemma "Ex (\<lambda>x. f x y = f x y) = True" |
|
430 |
nitpick [expect = none] |
|
431 |
by auto |
|
432 |
||
433 |
lemma "Ex (\<lambda>x. f x y = f y x) = True" |
|
434 |
nitpick [expect = none] |
|
435 |
by auto |
|
436 |
||
437 |
lemma "Ex (\<lambda>x. f x y = f x y) = False" |
|
438 |
nitpick [expect = genuine] |
|
439 |
oops |
|
440 |
||
441 |
lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False" |
|
442 |
nitpick [expect = none] |
|
443 |
by auto |
|
444 |
||
445 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))" |
|
446 |
nitpick [expect = none] |
|
447 |
by auto |
|
448 |
||
449 |
lemma "x = y \<Longrightarrow> y = x" |
|
450 |
nitpick [expect = none] |
|
451 |
by auto |
|
452 |
||
453 |
lemma "x = y \<Longrightarrow> f x = f y" |
|
454 |
nitpick [expect = none] |
|
455 |
by auto |
|
456 |
||
457 |
lemma "x = y \<and> y = z \<Longrightarrow> x = z" |
|
458 |
nitpick [expect = none] |
|
459 |
by auto |
|
460 |
||
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
461 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x. op \<and> (I x))" |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
462 |
"I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x y. x \<and> (I y))" |
33197 | 463 |
nitpick [expect = none] |
464 |
by auto |
|
465 |
||
466 |
lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))" |
|
467 |
nitpick [expect = none] |
|
468 |
by auto |
|
469 |
||
470 |
lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b" |
|
471 |
nitpick [expect = none] |
|
472 |
by auto |
|
473 |
||
474 |
lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)" |
|
475 |
nitpick [expect = none] |
|
476 |
by auto |
|
477 |
||
478 |
lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" |
|
479 |
nitpick [expect = none] |
|
480 |
by auto |
|
481 |
||
482 |
lemma "(if a then b else c) = (THE d. (a \<longrightarrow> (d = b)) \<and> (\<not> a \<longrightarrow> (d = c)))" |
|
483 |
nitpick [expect = none] |
|
484 |
by auto |
|
485 |
||
486 |
lemma "fst (x, y) = x" |
|
487 |
nitpick [expect = none] |
|
488 |
by (simp add: fst_def) |
|
489 |
||
490 |
lemma "snd (x, y) = y" |
|
491 |
nitpick [expect = none] |
|
492 |
by (simp add: snd_def) |
|
493 |
||
494 |
lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x" |
|
495 |
nitpick [expect = none] |
|
496 |
by (simp add: fst_def) |
|
497 |
||
498 |
lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y" |
|
499 |
nitpick [expect = none] |
|
500 |
by (simp add: snd_def) |
|
501 |
||
502 |
lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x" |
|
503 |
nitpick [expect = none] |
|
504 |
by (simp add: fst_def) |
|
505 |
||
506 |
lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y" |
|
507 |
nitpick [expect = none] |
|
508 |
by (simp add: snd_def) |
|
509 |
||
510 |
lemma "fst (x\<Colon>'a\<times>'b, y) = x" |
|
511 |
nitpick [expect = none] |
|
512 |
by (simp add: fst_def) |
|
513 |
||
514 |
lemma "snd (x\<Colon>'a\<times>'b, y) = y" |
|
515 |
nitpick [expect = none] |
|
516 |
by (simp add: snd_def) |
|
517 |
||
518 |
lemma "fst (x, y\<Colon>'a\<times>'b) = x" |
|
519 |
nitpick [expect = none] |
|
520 |
by (simp add: fst_def) |
|
521 |
||
522 |
lemma "snd (x, y\<Colon>'a\<times>'b) = y" |
|
523 |
nitpick [expect = none] |
|
524 |
by (simp add: snd_def) |
|
525 |
||
526 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))" |
|
527 |
nitpick [expect = none] |
|
528 |
by auto |
|
529 |
||
530 |
lemma "fst (x, y) = snd (y, x)" |
|
531 |
nitpick [expect = none] |
|
532 |
by auto |
|
533 |
||
534 |
lemma "(x, x) \<in> Id" |
|
535 |
nitpick [expect = none] |
|
536 |
by auto |
|
537 |
||
538 |
lemma "(x, y) \<in> Id \<Longrightarrow> x = y" |
|
539 |
nitpick [expect = none] |
|
540 |
by auto |
|
541 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
542 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = {x. I x \<in> Id}" |
33197 | 543 |
nitpick [expect = none] |
544 |
by auto |
|
545 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
546 |
lemma "{} = {x. False}" |
33197 | 547 |
nitpick [expect = none] |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
548 |
by (metis empty_def) |
33197 | 549 |
|
550 |
lemma "x \<in> {}" |
|
551 |
nitpick [expect = genuine] |
|
552 |
oops |
|
553 |
||
554 |
lemma "{a, b} = {b}" |
|
555 |
nitpick [expect = genuine] |
|
556 |
oops |
|
557 |
||
558 |
lemma "{a, b} \<noteq> {b}" |
|
559 |
nitpick [expect = genuine] |
|
560 |
oops |
|
561 |
||
562 |
lemma "{a} = {b}" |
|
563 |
nitpick [expect = genuine] |
|
564 |
oops |
|
565 |
||
566 |
lemma "{a} \<noteq> {b}" |
|
567 |
nitpick [expect = genuine] |
|
568 |
oops |
|
569 |
||
570 |
lemma "{a, b, c} = {c, b, a}" |
|
571 |
nitpick [expect = none] |
|
572 |
by auto |
|
573 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
574 |
lemma "UNIV = {x. True}" |
33197 | 575 |
nitpick [expect = none] |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
576 |
by (simp only: UNIV_def) |
33197 | 577 |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
578 |
lemma "x \<in> UNIV \<longleftrightarrow> True" |
33197 | 579 |
nitpick [expect = none] |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
580 |
by (simp only: UNIV_def mem_Collect_eq) |
33197 | 581 |
|
582 |
lemma "x \<notin> UNIV" |
|
583 |
nitpick [expect = genuine] |
|
584 |
oops |
|
585 |
||
586 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))" |
|
587 |
nitpick [expect = none] |
|
588 |
apply (rule ext) |
|
589 |
apply (rule ext) |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
590 |
by simp |
33197 | 591 |
|
592 |
lemma "insert = (\<lambda>x y. insert x (y \<union> y))" |
|
593 |
nitpick [expect = none] |
|
594 |
by simp |
|
595 |
||
596 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))" |
|
42959 | 597 |
nitpick [card = 1\<emdash>2, expect = none] |
33197 | 598 |
by auto |
599 |
||
600 |
lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})" |
|
42959 | 601 |
nitpick [card = 1\<emdash>3, expect = none] |
33197 | 602 |
apply (rule ext) |
603 |
by auto |
|
604 |
||
605 |
lemma "(x, x) \<in> rtrancl {(y, y)}" |
|
606 |
nitpick [expect = none] |
|
607 |
by auto |
|
608 |
||
609 |
lemma "((x, x), (x, x)) \<in> rtrancl {}" |
|
42959 | 610 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 611 |
by auto |
612 |
||
613 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))" |
|
42959 | 614 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 615 |
by auto |
616 |
||
617 |
lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)" |
|
618 |
nitpick [expect = none] |
|
619 |
by auto |
|
620 |
||
621 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))" |
|
42959 | 622 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 623 |
by auto |
624 |
||
625 |
lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)" |
|
42959 | 626 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 627 |
by auto |
628 |
||
629 |
lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B" |
|
42959 | 630 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 631 |
by auto |
632 |
||
633 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))" |
|
42959 | 634 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 635 |
by auto |
636 |
||
637 |
lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)" |
|
42959 | 638 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 639 |
by auto |
640 |
||
641 |
lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B" |
|
42959 | 642 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 643 |
by auto |
644 |
||
645 |
lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B" |
|
646 |
nitpick [card = 5, expect = genuine] |
|
647 |
oops |
|
648 |
||
649 |
lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B" |
|
650 |
nitpick [expect = none] |
|
651 |
by auto |
|
652 |
||
653 |
lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))" |
|
42959 | 654 |
nitpick [card = 1\<emdash>7, expect = none] |
33197 | 655 |
by auto |
656 |
||
657 |
lemma "A \<union> - A = UNIV" |
|
658 |
nitpick [expect = none] |
|
659 |
by auto |
|
660 |
||
661 |
lemma "A \<inter> - A = {}" |
|
662 |
nitpick [expect = none] |
|
663 |
by auto |
|
664 |
||
665 |
lemma "A = -(A\<Colon>'a set)" |
|
666 |
nitpick [card 'a = 10, expect = genuine] |
|
667 |
oops |
|
668 |
||
669 |
lemma "finite A" |
|
670 |
nitpick [expect = none] |
|
671 |
oops |
|
672 |
||
673 |
lemma "finite A \<Longrightarrow> finite B" |
|
674 |
nitpick [expect = none] |
|
675 |
oops |
|
676 |
||
677 |
lemma "All finite" |
|
678 |
nitpick [expect = none] |
|
679 |
oops |
|
680 |
||
681 |
subsection {* The and Eps *} |
|
682 |
||
683 |
lemma "x = The" |
|
684 |
nitpick [card = 5, expect = genuine] |
|
685 |
oops |
|
686 |
||
687 |
lemma "\<exists>x. x = The" |
|
42959 | 688 |
nitpick [card = 1\<emdash>3] |
33197 | 689 |
by auto |
690 |
||
691 |
lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x" |
|
692 |
nitpick [expect = none] |
|
693 |
by auto |
|
694 |
||
695 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z" |
|
696 |
nitpick [expect = genuine] |
|
697 |
oops |
|
698 |
||
699 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y" |
|
700 |
nitpick [card = 2, expect = none] |
|
42959 | 701 |
nitpick [card = 3\<emdash>5, expect = genuine] |
33197 | 702 |
oops |
703 |
||
704 |
lemma "P x \<Longrightarrow> P (The P)" |
|
42959 | 705 |
nitpick [card = 1\<emdash>2, expect = none] |
33197 | 706 |
nitpick [card = 8, expect = genuine] |
707 |
oops |
|
708 |
||
709 |
lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y" |
|
710 |
nitpick [expect = genuine] |
|
711 |
oops |
|
712 |
||
713 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))" |
|
42959 | 714 |
nitpick [card = 1\<emdash>5, expect = none] |
33197 | 715 |
by auto |
716 |
||
717 |
lemma "x = Eps" |
|
718 |
nitpick [card = 5, expect = genuine] |
|
719 |
oops |
|
720 |
||
721 |
lemma "\<exists>x. x = Eps" |
|
42959 | 722 |
nitpick [card = 1\<emdash>3, expect = none] |
33197 | 723 |
by auto |
724 |
||
725 |
lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x" |
|
726 |
nitpick [expect = none] |
|
727 |
by auto |
|
728 |
||
729 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z" |
|
730 |
nitpick [expect = genuine] |
|
731 |
apply auto |
|
732 |
oops |
|
733 |
||
734 |
lemma "P x \<Longrightarrow> P (Eps P)" |
|
42959 | 735 |
nitpick [card = 1\<emdash>8, expect = none] |
33197 | 736 |
by (metis exE_some) |
737 |
||
738 |
lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y" |
|
739 |
nitpick [expect = genuine] |
|
740 |
oops |
|
741 |
||
742 |
lemma "P (Eps P)" |
|
743 |
nitpick [expect = genuine] |
|
744 |
oops |
|
745 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
746 |
lemma "Eps (\<lambda>x. x \<in> P) \<in> (P\<Colon>nat set)" |
33197 | 747 |
nitpick [expect = genuine] |
748 |
oops |
|
749 |
||
750 |
lemma "\<not> P (Eps P)" |
|
751 |
nitpick [expect = genuine] |
|
752 |
oops |
|
753 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
754 |
lemma "\<not> (P \<Colon> nat \<Rightarrow> bool) (Eps P)" |
33197 | 755 |
nitpick [expect = genuine] |
756 |
oops |
|
757 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
758 |
lemma "P \<noteq> bot \<Longrightarrow> P (Eps P)" |
33197 | 759 |
nitpick [expect = none] |
760 |
sorry |
|
761 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
762 |
lemma "(P \<Colon> nat \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> P (Eps P)" |
33197 | 763 |
nitpick [expect = none] |
764 |
sorry |
|
765 |
||
766 |
lemma "P (The P)" |
|
767 |
nitpick [expect = genuine] |
|
768 |
oops |
|
769 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
770 |
lemma "(P \<Colon> nat \<Rightarrow> bool) (The P)" |
33197 | 771 |
nitpick [expect = genuine] |
772 |
oops |
|
773 |
||
774 |
lemma "\<not> P (The P)" |
|
775 |
nitpick [expect = genuine] |
|
776 |
oops |
|
777 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
778 |
lemma "\<not> (P \<Colon> nat \<Rightarrow> bool) (The P)" |
33197 | 779 |
nitpick [expect = genuine] |
780 |
oops |
|
781 |
||
782 |
lemma "The P \<noteq> x" |
|
783 |
nitpick [expect = genuine] |
|
784 |
oops |
|
785 |
||
786 |
lemma "The P \<noteq> (x\<Colon>nat)" |
|
787 |
nitpick [expect = genuine] |
|
788 |
oops |
|
789 |
||
790 |
lemma "P x \<Longrightarrow> P (The P)" |
|
791 |
nitpick [expect = genuine] |
|
792 |
oops |
|
793 |
||
794 |
lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)" |
|
795 |
nitpick [expect = genuine] |
|
796 |
oops |
|
797 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
798 |
lemma "P = {x} \<Longrightarrow> (THE x. x \<in> P) \<in> P" |
33197 | 799 |
nitpick [expect = none] |
800 |
oops |
|
801 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
802 |
lemma "P = {x\<Colon>nat} \<Longrightarrow> (THE x. x \<in> P) \<in> P" |
33197 | 803 |
nitpick [expect = none] |
804 |
oops |
|
805 |
||
806 |
consts Q :: 'a |
|
807 |
||
808 |
lemma "Q (Eps Q)" |
|
809 |
nitpick [expect = genuine] |
|
810 |
oops |
|
811 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
812 |
lemma "(Q \<Colon> nat \<Rightarrow> bool) (Eps Q)" |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35284
diff
changeset
|
813 |
nitpick [expect = none] (* unfortunate *) |
33197 | 814 |
oops |
815 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
816 |
lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (Eps Q)" |
33197 | 817 |
nitpick [expect = genuine] |
818 |
oops |
|
819 |
||
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45035
diff
changeset
|
820 |
lemma "\<not> (Q \<Colon> nat \<Rightarrow> bool) (Eps Q)" |
33197 | 821 |
nitpick [expect = genuine] |
822 |
oops |
|
823 |
||
46087 | 824 |
lemma "(Q\<Colon>'a \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> (Q\<Colon>'a \<Rightarrow> bool) (Eps Q)" |
33197 | 825 |
nitpick [expect = none] |
826 |
sorry |
|
827 |
||
46087 | 828 |
lemma "(Q\<Colon>nat \<Rightarrow> bool) \<noteq> bot \<Longrightarrow> (Q\<Colon>nat \<Rightarrow> bool) (Eps Q)" |
33197 | 829 |
nitpick [expect = none] |
830 |
sorry |
|
831 |
||
832 |
lemma "Q (The Q)" |
|
833 |
nitpick [expect = genuine] |
|
834 |
oops |
|
835 |
||
46087 | 836 |
lemma "(Q\<Colon>nat \<Rightarrow> bool) (The Q)" |
33197 | 837 |
nitpick [expect = genuine] |
838 |
oops |
|
839 |
||
840 |
lemma "\<not> Q (The Q)" |
|
841 |
nitpick [expect = genuine] |
|
842 |
oops |
|
843 |
||
46087 | 844 |
lemma "\<not> (Q\<Colon>nat \<Rightarrow> bool) (The Q)" |
33197 | 845 |
nitpick [expect = genuine] |
846 |
oops |
|
847 |
||
848 |
lemma "The Q \<noteq> x" |
|
849 |
nitpick [expect = genuine] |
|
850 |
oops |
|
851 |
||
852 |
lemma "The Q \<noteq> (x\<Colon>nat)" |
|
853 |
nitpick [expect = genuine] |
|
854 |
oops |
|
855 |
||
856 |
lemma "Q x \<Longrightarrow> Q (The Q)" |
|
857 |
nitpick [expect = genuine] |
|
858 |
oops |
|
859 |
||
860 |
lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)" |
|
861 |
nitpick [expect = genuine] |
|
862 |
oops |
|
863 |
||
46087 | 864 |
lemma "Q = (\<lambda>x\<Colon>'a. x = a) \<Longrightarrow> (Q\<Colon>'a \<Rightarrow> bool) (The Q)" |
33197 | 865 |
nitpick [expect = none] |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35284
diff
changeset
|
866 |
sorry |
33197 | 867 |
|
46087 | 868 |
lemma "Q = (\<lambda>x\<Colon>nat. x = a) \<Longrightarrow> (Q\<Colon>nat \<Rightarrow> bool) (The Q)" |
33197 | 869 |
nitpick [expect = none] |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35284
diff
changeset
|
870 |
sorry |
33197 | 871 |
|
39359 | 872 |
nitpick_params [max_potential = 1] |
37275 | 873 |
|
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
874 |
lemma "(THE j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
875 |
nitpick [card nat = 2, expect = potential] |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
876 |
nitpick [card nat = 6, expect = potential] (* unfortunate *) |
37270 | 877 |
oops |
878 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
879 |
lemma "(THE j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x \<noteq> 0" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
880 |
nitpick [card nat = 2, expect = potential] |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
881 |
nitpick [card nat = 6, expect = none] |
37270 | 882 |
sorry |
883 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
884 |
lemma "(THE j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x = 4" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
885 |
nitpick [card nat = 2, expect = potential] |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
886 |
nitpick [card nat = 6, expect = none] |
37270 | 887 |
sorry |
888 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
889 |
lemma "(THE j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
890 |
nitpick [card nat = 6, expect = genuine] |
37270 | 891 |
oops |
892 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
893 |
lemma "(THE j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4 \<or> x = 5" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
894 |
nitpick [card nat = 6, expect = genuine] |
37270 | 895 |
oops |
896 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
897 |
lemma "(SOME j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
898 |
nitpick [card nat = 2, expect = potential] |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
899 |
nitpick [card nat = 6, expect = genuine] |
37270 | 900 |
oops |
901 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
902 |
lemma "(SOME j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x \<noteq> 0" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
903 |
nitpick [card nat = 2, expect = potential] |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
904 |
nitpick [card nat = 6, expect = none] |
37270 | 905 |
oops |
906 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
907 |
lemma "(SOME j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x = 4" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
908 |
nitpick [card nat = 2, expect = potential] |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
909 |
nitpick [card nat = 6, expect = none] |
37270 | 910 |
sorry |
911 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
912 |
lemma "(SOME j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
913 |
nitpick [card nat = 6, expect = genuine] |
37270 | 914 |
oops |
915 |
||
37434
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
916 |
lemma "(SOME j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4 \<or> x = 5" |
df936eadb642
make example run a bit faster (might help atbroy102)
blanchet
parents:
37275
diff
changeset
|
917 |
nitpick [card nat = 6, expect = none] |
37270 | 918 |
sorry |
919 |
||
39359 | 920 |
nitpick_params [max_potential = 0] |
37275 | 921 |
|
33197 | 922 |
subsection {* Destructors and Recursors *} |
923 |
||
924 |
lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)" |
|
925 |
nitpick [card = 2, expect = none] |
|
926 |
by auto |
|
927 |
||
928 |
lemma "bool_rec x y True = x" |
|
929 |
nitpick [card = 2, expect = none] |
|
930 |
by auto |
|
931 |
||
932 |
lemma "bool_rec x y False = y" |
|
933 |
nitpick [card = 2, expect = none] |
|
934 |
by auto |
|
935 |
||
936 |
lemma "(x\<Colon>bool) = bool_rec x x True" |
|
937 |
nitpick [card = 2, expect = none] |
|
938 |
by auto |
|
939 |
||
940 |
lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')" |
|
941 |
nitpick [expect = none] |
|
942 |
sorry |
|
943 |
||
944 |
end |