author | blanchet |
Fri, 18 Dec 2009 12:00:29 +0100 | |
changeset 34126 | 8a2c5d7aff51 |
parent 34083 | 652719832159 |
child 35076 | cc19e2aef17e |
permissions | -rw-r--r-- |
33197 | 1 |
(* Title: HOL/Nitpick_Examples/Core_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2009 |
|
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 |
||
34083
652719832159
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
blanchet
parents:
34082
diff
changeset
|
14 |
nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s] |
34082
61b7aa37f4b7
make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
blanchet
parents:
33199
diff
changeset
|
15 |
|
33197 | 16 |
subsection {* Curry in a Hurry *} |
17 |
||
18 |
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)" |
|
19 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
20 |
nitpick [card = 100, expect = none, timeout = none] |
|
21 |
by auto |
|
22 |
||
23 |
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)" |
|
24 |
nitpick [card = 2] |
|
25 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
26 |
nitpick [card = 10, expect = none] |
|
27 |
by auto |
|
28 |
||
29 |
lemma "split (curry f) = f" |
|
30 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
31 |
nitpick [card = 10, expect = none] |
|
32 |
nitpick [card = 40, expect = none] |
|
33 |
by auto |
|
34 |
||
35 |
lemma "curry (split f) = f" |
|
36 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
37 |
nitpick [card = 40, expect = none] |
|
38 |
by auto |
|
39 |
||
40 |
lemma "(split o curry) f = f" |
|
41 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
42 |
nitpick [card = 40, expect = none] |
|
43 |
by auto |
|
44 |
||
45 |
lemma "(curry o split) f = f" |
|
46 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
47 |
nitpick [card = 1000, expect = none] |
|
48 |
by auto |
|
49 |
||
50 |
lemma "(split o curry) f = (\<lambda>x. x) f" |
|
51 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
52 |
nitpick [card = 40, expect = none] |
|
53 |
by auto |
|
54 |
||
55 |
lemma "(curry o split) f = (\<lambda>x. x) f" |
|
56 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
57 |
nitpick [card = 40, expect = none] |
|
58 |
by auto |
|
59 |
||
60 |
lemma "((split o curry) f) p = ((\<lambda>x. x) f) p" |
|
61 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
62 |
nitpick [card = 40, expect = none] |
|
63 |
by auto |
|
64 |
||
65 |
lemma "((curry o split) f) x = ((\<lambda>x. x) f) x" |
|
66 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
67 |
nitpick [card = 1000, expect = none] |
|
68 |
by auto |
|
69 |
||
70 |
lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y" |
|
71 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
72 |
nitpick [card = 1000, expect = none] |
|
73 |
by auto |
|
74 |
||
75 |
lemma "split o curry = (\<lambda>x. x)" |
|
76 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
77 |
nitpick [card = 40, expect = none] |
|
78 |
apply (rule ext)+ |
|
79 |
by auto |
|
80 |
||
81 |
lemma "curry o split = (\<lambda>x. x)" |
|
82 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
83 |
nitpick [card = 100, expect = none] |
|
84 |
apply (rule ext)+ |
|
85 |
by auto |
|
86 |
||
87 |
lemma "split (\<lambda>x y. f (x, y)) = f" |
|
88 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
89 |
nitpick [card = 40, expect = none] |
|
90 |
by auto |
|
91 |
||
92 |
subsection {* Representations *} |
|
93 |
||
94 |
lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y" |
|
95 |
nitpick [expect = none] |
|
96 |
by auto |
|
97 |
||
98 |
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)" |
|
99 |
nitpick [card 'a = 35, card 'b = 34, expect = genuine] |
|
100 |
nitpick [card = 1\<midarrow>15, mono, expect = none] |
|
101 |
oops |
|
102 |
||
103 |
lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y" |
|
104 |
nitpick [card = 1, expect = genuine] |
|
105 |
nitpick [card = 2, expect = genuine] |
|
106 |
nitpick [card = 5, expect = genuine] |
|
107 |
oops |
|
108 |
||
109 |
lemma "P (\<lambda>x. x)" |
|
110 |
nitpick [card = 1, expect = genuine] |
|
111 |
nitpick [card = 5, expect = genuine] |
|
112 |
oops |
|
113 |
||
114 |
lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}" |
|
115 |
nitpick [card = 1\<midarrow>6, expect = none] |
|
116 |
nitpick [card = 20, expect = none] |
|
117 |
by auto |
|
118 |
||
119 |
lemma "fst (a, b) = a" |
|
120 |
nitpick [card = 1\<midarrow>20, expect = none] |
|
121 |
by auto |
|
122 |
||
123 |
lemma "\<exists>P. P = Id" |
|
124 |
nitpick [card = 1\<midarrow>4, expect = none] |
|
125 |
by auto |
|
126 |
||
127 |
lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*" |
|
128 |
nitpick [card = 1\<midarrow>3, expect = none] |
|
129 |
by auto |
|
130 |
||
131 |
lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*" |
|
132 |
nitpick [card = 1\<midarrow>6, expect = none] |
|
133 |
by auto |
|
134 |
||
135 |
lemma "Id (a, a)" |
|
136 |
nitpick [card = 1\<midarrow>100, expect = none] |
|
137 |
by (auto simp: Id_def Collect_def) |
|
138 |
||
139 |
lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))" |
|
34082
61b7aa37f4b7
make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
blanchet
parents:
33199
diff
changeset
|
140 |
nitpick [card = 1\<midarrow>10, expect = none] |
33197 | 141 |
by (auto simp: Id_def Collect_def) |
142 |
||
143 |
lemma "UNIV (x\<Colon>'a\<times>'a)" |
|
144 |
nitpick [card = 1\<midarrow>50, expect = none] |
|
145 |
sorry |
|
146 |
||
147 |
lemma "{} = A - A" |
|
148 |
nitpick [card = 1\<midarrow>100, expect = none] |
|
149 |
by auto |
|
150 |
||
151 |
lemma "g = Let (A \<or> B)" |
|
152 |
nitpick [card = 1, expect = none] |
|
153 |
nitpick [card = 2, expect = genuine] |
|
154 |
nitpick [card = 20, expect = genuine] |
|
155 |
oops |
|
156 |
||
157 |
lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)" |
|
158 |
nitpick [expect = none] |
|
159 |
by auto |
|
160 |
||
161 |
lemma "A \<subseteq> B" |
|
162 |
nitpick [card = 100, expect = genuine] |
|
163 |
oops |
|
164 |
||
165 |
lemma "A = {b}" |
|
166 |
nitpick [card = 100, expect = genuine] |
|
167 |
oops |
|
168 |
||
169 |
lemma "{a, b} = {b}" |
|
170 |
nitpick [card = 100, expect = genuine] |
|
171 |
oops |
|
172 |
||
173 |
lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R" |
|
174 |
nitpick [card = 1, expect = genuine] |
|
175 |
nitpick [card = 2, expect = genuine] |
|
176 |
nitpick [card = 4, expect = genuine] |
|
177 |
nitpick [card = 20, expect = genuine] |
|
178 |
nitpick [card = 10, dont_box, expect = genuine] |
|
179 |
oops |
|
180 |
||
181 |
lemma "f (g\<Colon>'a\<Rightarrow>'a) = x" |
|
182 |
nitpick [card = 3, expect = genuine] |
|
183 |
nitpick [card = 3, dont_box, expect = genuine] |
|
184 |
nitpick [card = 5, expect = genuine] |
|
185 |
nitpick [card = 10, expect = genuine] |
|
186 |
oops |
|
187 |
||
188 |
lemma "f (a, b) = x" |
|
189 |
nitpick [card = 3, expect = genuine] |
|
190 |
nitpick [card = 10, expect = genuine] |
|
191 |
nitpick [card = 16, expect = genuine] |
|
192 |
nitpick [card = 30, expect = genuine] |
|
193 |
oops |
|
194 |
||
195 |
lemma "f (a, a) = f (c, d)" |
|
196 |
nitpick [card = 4, expect = genuine] |
|
197 |
nitpick [card = 20, expect = genuine] |
|
198 |
oops |
|
199 |
||
200 |
lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True" |
|
201 |
nitpick [card = 2, expect = none] |
|
202 |
by auto |
|
203 |
||
204 |
lemma "\<exists>F. F a b = G a b" |
|
205 |
nitpick [card = 3, expect = none] |
|
206 |
by auto |
|
207 |
||
208 |
lemma "f = split" |
|
209 |
nitpick [card = 1, expect = none] |
|
210 |
nitpick [card = 2, expect = genuine] |
|
211 |
oops |
|
212 |
||
213 |
lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R" |
|
214 |
nitpick [card = 20, expect = none] |
|
215 |
by auto |
|
216 |
||
217 |
lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> |
|
218 |
A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)" |
|
219 |
nitpick [card = 1\<midarrow>50, expect = none] |
|
220 |
by auto |
|
221 |
||
222 |
lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)" |
|
223 |
nitpick [card = 3, expect = genuine] |
|
224 |
nitpick [card = 4, expect = genuine] |
|
225 |
nitpick [card = 8, expect = genuine] |
|
226 |
oops |
|
227 |
||
228 |
subsection {* Quantifiers *} |
|
229 |
||
230 |
lemma "x = y" |
|
231 |
nitpick [card 'a = 1, expect = none] |
|
232 |
nitpick [card 'a = 2, expect = genuine] |
|
233 |
nitpick [card 'a = 100, expect = genuine] |
|
234 |
nitpick [card 'a = 1000, expect = genuine] |
|
235 |
oops |
|
236 |
||
237 |
lemma "\<forall>x. x = y" |
|
238 |
nitpick [card 'a = 1, expect = none] |
|
239 |
nitpick [card 'a = 2, expect = genuine] |
|
240 |
nitpick [card 'a = 100, expect = genuine] |
|
241 |
nitpick [card 'a = 1000, expect = genuine] |
|
242 |
oops |
|
243 |
||
244 |
lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y" |
|
245 |
nitpick [card 'a = 1, expect = genuine] |
|
246 |
nitpick [card 'a = 2, expect = genuine] |
|
247 |
nitpick [card 'a = 100, expect = genuine] |
|
248 |
nitpick [card 'a = 1000, expect = genuine] |
|
249 |
oops |
|
250 |
||
251 |
lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y" |
|
252 |
nitpick [card 'a = 1\<midarrow>10, expect = none] |
|
253 |
by auto |
|
254 |
||
255 |
lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y" |
|
256 |
nitpick [card = 1\<midarrow>40, expect = none] |
|
257 |
by auto |
|
258 |
||
259 |
lemma "\<forall>x. \<exists>y. f x y = f x (g x)" |
|
260 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
261 |
by auto |
|
262 |
||
263 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)" |
|
264 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
265 |
by auto |
|
266 |
||
267 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)" |
|
268 |
nitpick [card = 1\<midarrow>2, expect = genuine] |
|
269 |
nitpick [card = 3, expect = genuine] |
|
270 |
oops |
|
271 |
||
272 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
273 |
f u v w x y z = f u (g u) w (h u w) y (k u w y)" |
|
274 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
275 |
nitpick [card = 3, expect = none] |
|
276 |
nitpick [card = 4, expect = none] |
|
277 |
sorry |
|
278 |
||
279 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
280 |
f u v w x y z = f u (g u) w (h u w y) y (k u w y)" |
|
281 |
nitpick [card = 1\<midarrow>2, expect = genuine] |
|
282 |
oops |
|
283 |
||
284 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
285 |
f u v w x y z = f u (g u w) w (h u w) y (k u w y)" |
|
286 |
nitpick [card = 1\<midarrow>2, expect = genuine] |
|
287 |
oops |
|
288 |
||
289 |
lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f. |
|
290 |
f u v w x = f u (g u) w (h u w)" |
|
291 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
292 |
sorry |
|
293 |
||
294 |
lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f. |
|
295 |
f u v w x = f u (g u w) w (h u)" |
|
296 |
nitpick [card = 1\<midarrow>2, dont_box, expect = genuine] |
|
297 |
oops |
|
298 |
||
299 |
lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f. |
|
300 |
f u v w x = f u (g u) w (h u w)" |
|
301 |
nitpick [card = 1\<midarrow>2, dont_box, expect = none] |
|
302 |
sorry |
|
303 |
||
304 |
lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f. |
|
305 |
f u v w x = f u (g u w) w (h u)" |
|
306 |
nitpick [card = 1\<midarrow>2, dont_box, expect = genuine] |
|
307 |
oops |
|
308 |
||
309 |
lemma "\<forall>x. if (\<forall>y. x = y) then False else True" |
|
310 |
nitpick [card = 1, expect = genuine] |
|
311 |
nitpick [card = 2\<midarrow>5, expect = none] |
|
312 |
oops |
|
313 |
||
314 |
lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True" |
|
315 |
nitpick [card = 1, expect = genuine] |
|
316 |
nitpick [card = 2, expect = none] |
|
317 |
oops |
|
318 |
||
319 |
lemma "\<forall>x. if (\<exists>y. x = y) then True else False" |
|
320 |
nitpick [expect = none] |
|
321 |
sorry |
|
322 |
||
323 |
lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False" |
|
324 |
nitpick [expect = none] |
|
325 |
sorry |
|
326 |
||
327 |
lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)" |
|
328 |
nitpick [expect = none] |
|
329 |
by auto |
|
330 |
||
331 |
lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))" |
|
332 |
nitpick [expect = none] |
|
333 |
by auto |
|
334 |
||
335 |
lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)" |
|
336 |
nitpick [card 'a = 1, expect = genuine] |
|
337 |
nitpick [card 'a = 2, expect = genuine] |
|
338 |
nitpick [card 'a = 3, expect = genuine] |
|
339 |
nitpick [card 'a = 4, expect = genuine] |
|
340 |
nitpick [card 'a = 5, expect = genuine] |
|
341 |
oops |
|
342 |
||
343 |
lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) |
|
344 |
else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
345 |
nitpick [expect = none] |
|
346 |
by auto |
|
347 |
||
348 |
lemma "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) |
|
349 |
else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
350 |
nitpick [expect = none] |
|
351 |
by auto |
|
352 |
||
353 |
lemma "let x = (\<forall>x. P x) in if x then x else \<not> x" |
|
354 |
nitpick [expect = none] |
|
355 |
by auto |
|
356 |
||
357 |
lemma "let x = (\<forall>x\<Colon>'a \<times> 'b. P x) in if x then x else \<not> x" |
|
358 |
nitpick [expect = none] |
|
359 |
by auto |
|
360 |
||
361 |
subsection {* Schematic Variables *} |
|
362 |
||
363 |
lemma "x = ?x" |
|
364 |
nitpick [expect = none] |
|
365 |
by auto |
|
366 |
||
367 |
lemma "\<forall>x. x = ?x" |
|
368 |
nitpick [expect = genuine] |
|
369 |
oops |
|
370 |
||
371 |
lemma "\<exists>x. x = ?x" |
|
372 |
nitpick [expect = none] |
|
373 |
by auto |
|
374 |
||
375 |
lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x" |
|
376 |
nitpick [expect = none] |
|
377 |
by auto |
|
378 |
||
379 |
lemma "\<forall>x. ?x = ?y" |
|
380 |
nitpick [expect = none] |
|
381 |
by auto |
|
382 |
||
383 |
lemma "\<exists>x. ?x = ?y" |
|
384 |
nitpick [expect = none] |
|
385 |
by auto |
|
386 |
||
387 |
subsection {* Known Constants *} |
|
388 |
||
389 |
lemma "x \<equiv> all \<Longrightarrow> False" |
|
390 |
nitpick [card = 1, expect = genuine] |
|
391 |
nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine] |
|
392 |
nitpick [card = 2, expect = genuine] |
|
393 |
nitpick [card = 8, expect = genuine] |
|
394 |
nitpick [card = 10, expect = unknown] |
|
395 |
oops |
|
396 |
||
397 |
lemma "\<And>x. f x y = f x y" |
|
398 |
nitpick [expect = none] |
|
399 |
oops |
|
400 |
||
401 |
lemma "\<And>x. f x y = f y x" |
|
402 |
nitpick [expect = genuine] |
|
403 |
oops |
|
404 |
||
405 |
lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True" |
|
406 |
nitpick [expect = none] |
|
407 |
by auto |
|
408 |
||
409 |
lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False" |
|
410 |
nitpick [expect = genuine] |
|
411 |
oops |
|
412 |
||
413 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))" |
|
414 |
nitpick [expect = none] |
|
415 |
by auto |
|
416 |
||
417 |
lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False" |
|
418 |
nitpick [card = 1, expect = genuine] |
|
419 |
nitpick [card = 2, expect = genuine] |
|
420 |
nitpick [card = 3, expect = genuine] |
|
421 |
nitpick [card = 4, expect = genuine] |
|
422 |
nitpick [card = 5, expect = genuine] |
|
423 |
nitpick [card = 100, expect = genuine] |
|
424 |
oops |
|
425 |
||
426 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))" |
|
427 |
nitpick [expect = none] |
|
428 |
by auto |
|
429 |
||
430 |
lemma "P x \<equiv> P x" |
|
431 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
432 |
by auto |
|
433 |
||
434 |
lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x" |
|
435 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
436 |
by auto |
|
437 |
||
438 |
lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x" |
|
439 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
440 |
by auto |
|
441 |
||
442 |
lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False" |
|
443 |
nitpick [expect = genuine] |
|
444 |
oops |
|
445 |
||
446 |
lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))" |
|
447 |
nitpick [expect = none] |
|
448 |
by auto |
|
449 |
||
450 |
lemma "P x \<Longrightarrow> P x" |
|
451 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
452 |
by auto |
|
453 |
||
454 |
lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False" |
|
455 |
nitpick [expect = none] |
|
456 |
by auto |
|
457 |
||
458 |
lemma "True \<Longrightarrow> False" |
|
459 |
nitpick [expect = genuine] |
|
460 |
oops |
|
461 |
||
462 |
lemma "x = Not" |
|
463 |
nitpick [expect = genuine] |
|
464 |
oops |
|
465 |
||
466 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))" |
|
467 |
nitpick [expect = none] |
|
468 |
by auto |
|
469 |
||
470 |
lemma "x = True" |
|
471 |
nitpick [expect = genuine] |
|
472 |
oops |
|
473 |
||
474 |
lemma "x = False" |
|
475 |
nitpick [expect = genuine] |
|
476 |
oops |
|
477 |
||
478 |
lemma "x = undefined" |
|
479 |
nitpick [expect = genuine] |
|
480 |
oops |
|
481 |
||
482 |
lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined" |
|
483 |
nitpick [expect = genuine] |
|
484 |
oops |
|
485 |
||
486 |
lemma "undefined = undefined" |
|
487 |
nitpick [expect = none] |
|
488 |
by auto |
|
489 |
||
490 |
lemma "f undefined = f undefined" |
|
491 |
nitpick [expect = none] |
|
492 |
by auto |
|
493 |
||
494 |
lemma "f undefined = g undefined" |
|
495 |
nitpick [card = 33, expect = genuine] |
|
496 |
oops |
|
497 |
||
498 |
lemma "\<exists>!x. x = undefined" |
|
499 |
nitpick [card = 30, expect = none] |
|
500 |
by auto |
|
501 |
||
502 |
lemma "x = All \<Longrightarrow> False" |
|
503 |
nitpick [card = 1, dont_box, expect = genuine] |
|
504 |
nitpick [card = 2, dont_box, expect = genuine] |
|
505 |
nitpick [card = 8, dont_box, expect = genuine] |
|
506 |
nitpick [card = 10, dont_box, expect = unknown] |
|
507 |
oops |
|
508 |
||
509 |
lemma "\<forall>x. f x y = f x y" |
|
510 |
nitpick [expect = none] |
|
511 |
oops |
|
512 |
||
513 |
lemma "\<forall>x. f x y = f y x" |
|
514 |
nitpick [expect = genuine] |
|
515 |
oops |
|
516 |
||
517 |
lemma "All (\<lambda>x. f x y = f x y) = True" |
|
518 |
nitpick [expect = none] |
|
519 |
by auto |
|
520 |
||
521 |
lemma "All (\<lambda>x. f x y = f x y) = False" |
|
522 |
nitpick [expect = genuine] |
|
523 |
oops |
|
524 |
||
525 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))" |
|
526 |
nitpick [expect = none] |
|
527 |
by auto |
|
528 |
||
529 |
lemma "x = Ex \<Longrightarrow> False" |
|
530 |
nitpick [card = 1, dont_box, expect = genuine] |
|
531 |
nitpick [card = 2, dont_box, expect = genuine] |
|
532 |
nitpick [card = 8, dont_box, expect = genuine] |
|
533 |
nitpick [card = 10, dont_box, expect = unknown] |
|
534 |
oops |
|
535 |
||
536 |
lemma "\<exists>x. f x y = f x y" |
|
537 |
nitpick [expect = none] |
|
538 |
oops |
|
539 |
||
540 |
lemma "\<exists>x. f x y = f y x" |
|
541 |
nitpick [expect = none] |
|
542 |
oops |
|
543 |
||
544 |
lemma "Ex (\<lambda>x. f x y = f x y) = True" |
|
545 |
nitpick [expect = none] |
|
546 |
by auto |
|
547 |
||
548 |
lemma "Ex (\<lambda>x. f x y = f y x) = True" |
|
549 |
nitpick [expect = none] |
|
550 |
by auto |
|
551 |
||
552 |
lemma "Ex (\<lambda>x. f x y = f x y) = False" |
|
553 |
nitpick [expect = genuine] |
|
554 |
oops |
|
555 |
||
556 |
lemma "Ex (\<lambda>x. f x y = f y x) = False" |
|
557 |
nitpick [expect = genuine] |
|
558 |
oops |
|
559 |
||
560 |
lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False" |
|
561 |
nitpick [expect = none] |
|
562 |
by auto |
|
563 |
||
564 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))" |
|
565 |
nitpick [expect = none] |
|
566 |
by auto |
|
567 |
||
568 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))" |
|
569 |
"I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))" |
|
570 |
nitpick [expect = none] |
|
571 |
by auto |
|
572 |
||
573 |
lemma "x = y \<Longrightarrow> y = x" |
|
574 |
nitpick [expect = none] |
|
575 |
by auto |
|
576 |
||
577 |
lemma "x = y \<Longrightarrow> f x = f y" |
|
578 |
nitpick [expect = none] |
|
579 |
by auto |
|
580 |
||
581 |
lemma "x = y \<and> y = z \<Longrightarrow> x = z" |
|
582 |
nitpick [expect = none] |
|
583 |
by auto |
|
584 |
||
585 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))" |
|
586 |
"I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))" |
|
587 |
nitpick [expect = none] |
|
588 |
by auto |
|
589 |
||
590 |
lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))" |
|
591 |
nitpick [expect = none] |
|
592 |
by auto |
|
593 |
||
594 |
lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b" |
|
595 |
nitpick [expect = none] |
|
596 |
by auto |
|
597 |
||
598 |
lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)" |
|
599 |
nitpick [expect = none] |
|
600 |
by auto |
|
601 |
||
602 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))" |
|
603 |
"I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))" |
|
604 |
nitpick [expect = none] |
|
605 |
by auto |
|
606 |
||
607 |
lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b" |
|
608 |
nitpick [expect = none] |
|
609 |
by auto |
|
610 |
||
611 |
lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b" |
|
612 |
nitpick [expect = none] |
|
613 |
by auto |
|
614 |
||
615 |
lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)" |
|
616 |
nitpick [expect = none] |
|
617 |
by auto |
|
618 |
||
619 |
lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b" |
|
620 |
nitpick [expect = none] |
|
621 |
by auto |
|
622 |
||
623 |
lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)" |
|
624 |
nitpick [expect = none] |
|
625 |
by auto |
|
626 |
||
627 |
lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" |
|
628 |
nitpick [expect = none] |
|
629 |
by auto |
|
630 |
||
631 |
lemma "(if a then b else c) = (THE d. (a \<longrightarrow> (d = b)) \<and> (\<not> a \<longrightarrow> (d = c)))" |
|
632 |
nitpick [expect = none] |
|
633 |
by auto |
|
634 |
||
635 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))" |
|
636 |
"J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))" |
|
637 |
"K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))" |
|
638 |
nitpick [expect = none] |
|
639 |
by auto |
|
640 |
||
641 |
lemma "fst (x, y) = x" |
|
642 |
nitpick [expect = none] |
|
643 |
by (simp add: fst_def) |
|
644 |
||
645 |
lemma "snd (x, y) = y" |
|
646 |
nitpick [expect = none] |
|
647 |
by (simp add: snd_def) |
|
648 |
||
649 |
lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x" |
|
650 |
nitpick [expect = none] |
|
651 |
by (simp add: fst_def) |
|
652 |
||
653 |
lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y" |
|
654 |
nitpick [expect = none] |
|
655 |
by (simp add: snd_def) |
|
656 |
||
657 |
lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x" |
|
658 |
nitpick [expect = none] |
|
659 |
by (simp add: fst_def) |
|
660 |
||
661 |
lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y" |
|
662 |
nitpick [expect = none] |
|
663 |
by (simp add: snd_def) |
|
664 |
||
665 |
lemma "fst (x\<Colon>'a\<times>'b, y) = x" |
|
666 |
nitpick [expect = none] |
|
667 |
by (simp add: fst_def) |
|
668 |
||
669 |
lemma "snd (x\<Colon>'a\<times>'b, y) = y" |
|
670 |
nitpick [expect = none] |
|
671 |
by (simp add: snd_def) |
|
672 |
||
673 |
lemma "fst (x, y\<Colon>'a\<times>'b) = x" |
|
674 |
nitpick [expect = none] |
|
675 |
by (simp add: fst_def) |
|
676 |
||
677 |
lemma "snd (x, y\<Colon>'a\<times>'b) = y" |
|
678 |
nitpick [expect = none] |
|
679 |
by (simp add: snd_def) |
|
680 |
||
681 |
lemma "fst p = (THE a. \<exists>b. p = Pair a b)" |
|
682 |
nitpick [expect = none] |
|
683 |
by (simp add: fst_def) |
|
684 |
||
685 |
lemma "snd p = (THE b. \<exists>a. p = Pair a b)" |
|
686 |
nitpick [expect = none] |
|
687 |
by (simp add: snd_def) |
|
688 |
||
689 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))" |
|
690 |
nitpick [expect = none] |
|
691 |
by auto |
|
692 |
||
693 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))" |
|
694 |
nitpick [expect = none] |
|
695 |
by auto |
|
696 |
||
697 |
lemma "fst (x, y) = snd (y, x)" |
|
698 |
nitpick [expect = none] |
|
699 |
by auto |
|
700 |
||
701 |
lemma "(x, x) \<in> Id" |
|
702 |
nitpick [expect = none] |
|
703 |
by auto |
|
704 |
||
705 |
lemma "(x, y) \<in> Id \<Longrightarrow> x = y" |
|
706 |
nitpick [expect = none] |
|
707 |
by auto |
|
708 |
||
709 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))" |
|
710 |
nitpick [expect = none] |
|
711 |
by auto |
|
712 |
||
713 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))" |
|
714 |
nitpick [expect = none] |
|
715 |
by (simp add: curry_def) |
|
716 |
||
717 |
lemma "{} = (\<lambda>x. False)" |
|
718 |
nitpick [expect = none] |
|
33199 | 719 |
by (metis Collect_def empty_def) |
33197 | 720 |
|
721 |
lemma "x \<in> {}" |
|
722 |
nitpick [expect = genuine] |
|
723 |
oops |
|
724 |
||
725 |
lemma "{a, b} = {b}" |
|
726 |
nitpick [expect = genuine] |
|
727 |
oops |
|
728 |
||
729 |
lemma "{a, b} \<noteq> {b}" |
|
730 |
nitpick [expect = genuine] |
|
731 |
oops |
|
732 |
||
733 |
lemma "{a} = {b}" |
|
734 |
nitpick [expect = genuine] |
|
735 |
oops |
|
736 |
||
737 |
lemma "{a} \<noteq> {b}" |
|
738 |
nitpick [expect = genuine] |
|
739 |
oops |
|
740 |
||
741 |
lemma "{a, b, c} = {c, b, a}" |
|
742 |
nitpick [expect = none] |
|
743 |
by auto |
|
744 |
||
745 |
lemma "UNIV = (\<lambda>x. True)" |
|
746 |
nitpick [expect = none] |
|
747 |
by (simp only: UNIV_def Collect_def) |
|
748 |
||
749 |
lemma "UNIV x = True" |
|
750 |
nitpick [expect = none] |
|
751 |
by (simp only: UNIV_def Collect_def) |
|
752 |
||
753 |
lemma "x \<notin> UNIV" |
|
754 |
nitpick [expect = genuine] |
|
755 |
oops |
|
756 |
||
757 |
lemma "op \<in> = (\<lambda>x P. P x)" |
|
758 |
nitpick [expect = none] |
|
759 |
apply (rule ext) |
|
760 |
apply (rule ext) |
|
761 |
by (simp add: mem_def) |
|
762 |
||
763 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))" |
|
764 |
nitpick [expect = none] |
|
765 |
apply (rule ext) |
|
766 |
apply (rule ext) |
|
767 |
by (simp add: mem_def) |
|
768 |
||
769 |
lemma "P x = (x \<in> P)" |
|
770 |
nitpick [expect = none] |
|
771 |
by (simp add: mem_def) |
|
772 |
||
773 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))" |
|
774 |
nitpick [expect = none] |
|
775 |
by simp |
|
776 |
||
777 |
lemma "insert = (\<lambda>x y. insert x (y \<union> y))" |
|
778 |
nitpick [expect = none] |
|
779 |
by simp |
|
780 |
||
781 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))" |
|
782 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
783 |
by auto |
|
784 |
||
785 |
lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})" |
|
786 |
nitpick [card = 1\<midarrow>3, expect = none] |
|
787 |
apply (rule ext) |
|
788 |
by auto |
|
789 |
||
790 |
lemma "(x, x) \<in> rtrancl {(y, y)}" |
|
791 |
nitpick [expect = none] |
|
792 |
by auto |
|
793 |
||
794 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))" |
|
795 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
796 |
by auto |
|
797 |
||
798 |
lemma "((x, x), (x, x)) \<in> rtrancl {}" |
|
799 |
nitpick [expect = none] |
|
800 |
by auto |
|
801 |
||
802 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))" |
|
803 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
804 |
by auto |
|
805 |
||
806 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))" |
|
807 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
808 |
by auto |
|
809 |
||
810 |
lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)" |
|
811 |
nitpick [expect = none] |
|
812 |
by auto |
|
813 |
||
814 |
lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B" |
|
815 |
nitpick [expect = none] |
|
816 |
by auto |
|
817 |
||
818 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))" |
|
819 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
820 |
by auto |
|
821 |
||
822 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))" |
|
823 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
824 |
by auto |
|
825 |
||
826 |
lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)" |
|
827 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
828 |
by auto |
|
829 |
||
830 |
lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B" |
|
831 |
nitpick [expect = none] |
|
832 |
by auto |
|
833 |
||
834 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))" |
|
835 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
836 |
by auto |
|
837 |
||
838 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))" |
|
839 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
840 |
by auto |
|
841 |
||
842 |
lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B" |
|
843 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
844 |
by auto |
|
845 |
||
846 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))" |
|
847 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
848 |
by auto |
|
849 |
||
850 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))" |
|
851 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
852 |
by auto |
|
853 |
||
854 |
lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)" |
|
855 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
856 |
by auto |
|
857 |
||
858 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))" |
|
859 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
860 |
by auto |
|
861 |
||
862 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))" |
|
863 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
864 |
by auto |
|
865 |
||
866 |
lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B" |
|
867 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
868 |
by auto |
|
869 |
||
870 |
lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B" |
|
871 |
nitpick [card = 5, expect = genuine] |
|
872 |
oops |
|
873 |
||
874 |
lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B" |
|
875 |
nitpick [expect = none] |
|
876 |
by auto |
|
877 |
||
878 |
lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))" |
|
34126 | 879 |
nitpick [card = 1\<midarrow>7, expect = none] |
33197 | 880 |
by auto |
881 |
||
882 |
lemma "A \<union> - A = UNIV" |
|
883 |
nitpick [expect = none] |
|
884 |
by auto |
|
885 |
||
886 |
lemma "A \<inter> - A = {}" |
|
887 |
nitpick [expect = none] |
|
888 |
by auto |
|
889 |
||
890 |
lemma "A = -(A\<Colon>'a set)" |
|
891 |
nitpick [card 'a = 10, expect = genuine] |
|
892 |
oops |
|
893 |
||
894 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))" |
|
34126 | 895 |
nitpick [card = 1\<midarrow>7, expect = none] |
33197 | 896 |
oops |
897 |
||
898 |
lemma "finite A" |
|
899 |
nitpick [expect = none] |
|
900 |
oops |
|
901 |
||
902 |
lemma "finite A \<Longrightarrow> finite B" |
|
903 |
nitpick [expect = none] |
|
904 |
oops |
|
905 |
||
906 |
lemma "All finite" |
|
907 |
nitpick [expect = none] |
|
908 |
oops |
|
909 |
||
910 |
subsection {* The and Eps *} |
|
911 |
||
912 |
lemma "x = The" |
|
913 |
nitpick [card = 5, expect = genuine] |
|
914 |
oops |
|
915 |
||
916 |
lemma "\<exists>x. x = The" |
|
917 |
nitpick [card = 1\<midarrow>3] |
|
918 |
by auto |
|
919 |
||
920 |
lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x" |
|
921 |
nitpick [expect = none] |
|
922 |
by auto |
|
923 |
||
924 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z" |
|
925 |
nitpick [expect = genuine] |
|
926 |
oops |
|
927 |
||
928 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y" |
|
929 |
nitpick [card = 2, expect = none] |
|
930 |
nitpick [card = 3\<midarrow>5, expect = genuine] |
|
931 |
oops |
|
932 |
||
933 |
lemma "P x \<Longrightarrow> P (The P)" |
|
934 |
nitpick [card = 1, expect = none] |
|
935 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
936 |
nitpick [card = 3\<midarrow>5, expect = genuine] |
|
937 |
nitpick [card = 8, expect = genuine] |
|
938 |
oops |
|
939 |
||
940 |
lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y" |
|
941 |
nitpick [expect = genuine] |
|
942 |
oops |
|
943 |
||
944 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))" |
|
945 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
946 |
by auto |
|
947 |
||
948 |
lemma "x = Eps" |
|
949 |
nitpick [card = 5, expect = genuine] |
|
950 |
oops |
|
951 |
||
952 |
lemma "\<exists>x. x = Eps" |
|
953 |
nitpick [card = 1\<midarrow>3, expect = none] |
|
954 |
by auto |
|
955 |
||
956 |
lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x" |
|
957 |
nitpick [expect = none] |
|
958 |
by auto |
|
959 |
||
960 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z" |
|
961 |
nitpick [expect = genuine] |
|
962 |
apply auto |
|
963 |
oops |
|
964 |
||
965 |
lemma "P x \<Longrightarrow> P (Eps P)" |
|
966 |
nitpick [card = 1\<midarrow>8, expect = none] |
|
967 |
by (metis exE_some) |
|
968 |
||
969 |
lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y" |
|
970 |
nitpick [expect = genuine] |
|
971 |
oops |
|
972 |
||
973 |
lemma "P (Eps P)" |
|
974 |
nitpick [expect = genuine] |
|
975 |
oops |
|
976 |
||
977 |
lemma "(P\<Colon>nat set) (Eps P)" |
|
978 |
nitpick [expect = genuine] |
|
979 |
oops |
|
980 |
||
981 |
lemma "\<not> P (Eps P)" |
|
982 |
nitpick [expect = genuine] |
|
983 |
oops |
|
984 |
||
985 |
lemma "\<not> (P\<Colon>nat set) (Eps P)" |
|
986 |
nitpick [expect = genuine] |
|
987 |
oops |
|
988 |
||
989 |
lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)" |
|
990 |
nitpick [expect = none] |
|
991 |
sorry |
|
992 |
||
993 |
lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)" |
|
994 |
nitpick [expect = none] |
|
995 |
sorry |
|
996 |
||
997 |
lemma "P (The P)" |
|
998 |
nitpick [expect = genuine] |
|
999 |
oops |
|
1000 |
||
1001 |
lemma "(P\<Colon>nat set) (The P)" |
|
1002 |
nitpick [expect = genuine] |
|
1003 |
oops |
|
1004 |
||
1005 |
lemma "\<not> P (The P)" |
|
1006 |
nitpick [expect = genuine] |
|
1007 |
oops |
|
1008 |
||
1009 |
lemma "\<not> (P\<Colon>nat set) (The P)" |
|
1010 |
nitpick [expect = genuine] |
|
1011 |
oops |
|
1012 |
||
1013 |
lemma "The P \<noteq> x" |
|
1014 |
nitpick [expect = genuine] |
|
1015 |
oops |
|
1016 |
||
1017 |
lemma "The P \<noteq> (x\<Colon>nat)" |
|
1018 |
nitpick [expect = genuine] |
|
1019 |
oops |
|
1020 |
||
1021 |
lemma "P x \<Longrightarrow> P (The P)" |
|
1022 |
nitpick [expect = genuine] |
|
1023 |
oops |
|
1024 |
||
1025 |
lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)" |
|
1026 |
nitpick [expect = genuine] |
|
1027 |
oops |
|
1028 |
||
1029 |
lemma "P = {x} \<Longrightarrow> P (The P)" |
|
1030 |
nitpick [expect = none] |
|
1031 |
oops |
|
1032 |
||
1033 |
lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)" |
|
1034 |
nitpick [expect = none] |
|
1035 |
oops |
|
1036 |
||
1037 |
consts Q :: 'a |
|
1038 |
||
1039 |
lemma "Q (Eps Q)" |
|
1040 |
nitpick [expect = genuine] |
|
1041 |
oops |
|
1042 |
||
1043 |
lemma "(Q\<Colon>nat set) (Eps Q)" |
|
1044 |
nitpick [expect = none] |
|
1045 |
oops |
|
1046 |
||
1047 |
lemma "\<not> Q (Eps Q)" |
|
1048 |
nitpick [expect = genuine] |
|
1049 |
oops |
|
1050 |
||
1051 |
lemma "\<not> (Q\<Colon>nat set) (Eps Q)" |
|
1052 |
nitpick [expect = genuine] |
|
1053 |
oops |
|
1054 |
||
1055 |
lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)" |
|
1056 |
nitpick [expect = none] |
|
1057 |
sorry |
|
1058 |
||
1059 |
lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)" |
|
1060 |
nitpick [expect = none] |
|
1061 |
sorry |
|
1062 |
||
1063 |
lemma "Q (The Q)" |
|
1064 |
nitpick [expect = genuine] |
|
1065 |
oops |
|
1066 |
||
1067 |
lemma "(Q\<Colon>nat set) (The Q)" |
|
1068 |
nitpick [expect = genuine] |
|
1069 |
oops |
|
1070 |
||
1071 |
lemma "\<not> Q (The Q)" |
|
1072 |
nitpick [expect = genuine] |
|
1073 |
oops |
|
1074 |
||
1075 |
lemma "\<not> (Q\<Colon>nat set) (The Q)" |
|
1076 |
nitpick [expect = genuine] |
|
1077 |
oops |
|
1078 |
||
1079 |
lemma "The Q \<noteq> x" |
|
1080 |
nitpick [expect = genuine] |
|
1081 |
oops |
|
1082 |
||
1083 |
lemma "The Q \<noteq> (x\<Colon>nat)" |
|
1084 |
nitpick [expect = genuine] |
|
1085 |
oops |
|
1086 |
||
1087 |
lemma "Q x \<Longrightarrow> Q (The Q)" |
|
1088 |
nitpick [expect = genuine] |
|
1089 |
oops |
|
1090 |
||
1091 |
lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)" |
|
1092 |
nitpick [expect = genuine] |
|
1093 |
oops |
|
1094 |
||
1095 |
lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)" |
|
1096 |
nitpick [expect = none] |
|
1097 |
oops |
|
1098 |
||
1099 |
lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)" |
|
1100 |
nitpick [expect = none] |
|
1101 |
oops |
|
1102 |
||
1103 |
subsection {* Destructors and Recursors *} |
|
1104 |
||
1105 |
lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)" |
|
1106 |
nitpick [card = 2, expect = none] |
|
1107 |
by auto |
|
1108 |
||
1109 |
lemma "bool_rec x y True = x" |
|
1110 |
nitpick [card = 2, expect = none] |
|
1111 |
by auto |
|
1112 |
||
1113 |
lemma "bool_rec x y False = y" |
|
1114 |
nitpick [card = 2, expect = none] |
|
1115 |
by auto |
|
1116 |
||
1117 |
lemma "(x\<Colon>bool) = bool_rec x x True" |
|
1118 |
nitpick [card = 2, expect = none] |
|
1119 |
by auto |
|
1120 |
||
1121 |
lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')" |
|
1122 |
nitpick [expect = none] |
|
1123 |
sorry |
|
1124 |
||
1125 |
end |