14350
|
1 |
(* Title: HOL/ex/Refute_Examples.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tjark Weber
|
|
4 |
Copyright 2003-2004
|
|
5 |
*)
|
|
6 |
|
|
7 |
(* See 'HOL/Refute.thy' for help. *)
|
|
8 |
|
|
9 |
header {* Examples for the 'refute' command *}
|
|
10 |
|
|
11 |
theory Refute_Examples = Main:
|
|
12 |
|
|
13 |
section {* 'refute': General usage *}
|
|
14 |
|
14455
|
15 |
lemma "P x"
|
14350
|
16 |
refute
|
|
17 |
oops
|
|
18 |
|
|
19 |
lemma "P \<and> Q"
|
|
20 |
apply (rule conjI)
|
|
21 |
refute 1 -- {* refutes @{term "P"} *}
|
|
22 |
refute 2 -- {* refutes @{term "Q"} *}
|
|
23 |
refute -- {* equivalent to 'refute 1' *}
|
14455
|
24 |
-- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
|
14465
|
25 |
refute [maxsize=5] -- {* we can override parameters ... *}
|
|
26 |
refute [satsolver="dpll"] 2 -- {* ... and specify a subgoal at the same time *}
|
14350
|
27 |
oops
|
|
28 |
|
14455
|
29 |
refute_params
|
|
30 |
|
|
31 |
section {* Examples and Test Cases *}
|
14350
|
32 |
|
|
33 |
subsection {* Propositional logic *}
|
|
34 |
|
|
35 |
lemma "True"
|
|
36 |
refute
|
|
37 |
apply auto
|
|
38 |
done
|
|
39 |
|
|
40 |
lemma "False"
|
|
41 |
refute
|
|
42 |
oops
|
|
43 |
|
|
44 |
lemma "P"
|
|
45 |
refute
|
|
46 |
oops
|
|
47 |
|
|
48 |
lemma "~ P"
|
|
49 |
refute
|
|
50 |
oops
|
|
51 |
|
|
52 |
lemma "P & Q"
|
|
53 |
refute
|
|
54 |
oops
|
|
55 |
|
|
56 |
lemma "P | Q"
|
|
57 |
refute
|
|
58 |
oops
|
|
59 |
|
|
60 |
lemma "P \<longrightarrow> Q"
|
|
61 |
refute
|
|
62 |
oops
|
|
63 |
|
|
64 |
lemma "(P::bool) = Q"
|
|
65 |
refute
|
|
66 |
oops
|
|
67 |
|
|
68 |
lemma "(P | Q) \<longrightarrow> (P & Q)"
|
|
69 |
refute
|
|
70 |
oops
|
|
71 |
|
|
72 |
subsection {* Predicate logic *}
|
|
73 |
|
14455
|
74 |
lemma "P x y z"
|
14350
|
75 |
refute
|
|
76 |
oops
|
|
77 |
|
|
78 |
lemma "P x y \<longrightarrow> P y x"
|
|
79 |
refute
|
|
80 |
oops
|
|
81 |
|
14455
|
82 |
lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
|
|
83 |
refute
|
|
84 |
oops
|
|
85 |
|
14350
|
86 |
subsection {* Equality *}
|
|
87 |
|
|
88 |
lemma "P = True"
|
|
89 |
refute
|
|
90 |
oops
|
|
91 |
|
|
92 |
lemma "P = False"
|
|
93 |
refute
|
|
94 |
oops
|
|
95 |
|
|
96 |
lemma "x = y"
|
|
97 |
refute
|
|
98 |
oops
|
|
99 |
|
|
100 |
lemma "f x = g x"
|
|
101 |
refute
|
|
102 |
oops
|
|
103 |
|
|
104 |
lemma "(f::'a\<Rightarrow>'b) = g"
|
|
105 |
refute
|
|
106 |
oops
|
|
107 |
|
|
108 |
lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
|
|
109 |
refute
|
|
110 |
oops
|
|
111 |
|
|
112 |
lemma "distinct [a,b]"
|
|
113 |
apply simp
|
|
114 |
refute
|
|
115 |
oops
|
|
116 |
|
|
117 |
subsection {* First-Order Logic *}
|
|
118 |
|
|
119 |
lemma "\<exists>x. P x"
|
|
120 |
refute
|
|
121 |
oops
|
|
122 |
|
|
123 |
lemma "\<forall>x. P x"
|
|
124 |
refute
|
|
125 |
oops
|
|
126 |
|
|
127 |
lemma "EX! x. P x"
|
|
128 |
refute
|
|
129 |
oops
|
|
130 |
|
|
131 |
lemma "Ex P"
|
|
132 |
refute
|
|
133 |
oops
|
|
134 |
|
|
135 |
lemma "All P"
|
|
136 |
refute
|
|
137 |
oops
|
|
138 |
|
|
139 |
lemma "Ex1 P"
|
|
140 |
refute
|
|
141 |
oops
|
|
142 |
|
|
143 |
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
|
|
144 |
refute
|
|
145 |
oops
|
|
146 |
|
|
147 |
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
|
|
148 |
refute
|
|
149 |
oops
|
|
150 |
|
|
151 |
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
|
|
152 |
refute
|
|
153 |
oops
|
|
154 |
|
|
155 |
text {* A true statement (also testing names of free and bound variables being identical) *}
|
|
156 |
|
|
157 |
lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
|
14462
|
158 |
refute [maxsize=2] (* [maxsize=5] works well with ZChaff *)
|
14350
|
159 |
apply fast
|
|
160 |
done
|
|
161 |
|
|
162 |
text {* "A type has at most 3 elements." *}
|
|
163 |
|
14455
|
164 |
lemma "a=b | a=c | a=d | b=c | b=d | c=d"
|
|
165 |
refute
|
|
166 |
oops
|
|
167 |
|
14350
|
168 |
lemma "\<forall>a b c d. a=b | a=c | a=d | b=c | b=d | c=d"
|
|
169 |
refute
|
|
170 |
oops
|
|
171 |
|
|
172 |
text {* "Every reflexive and symmetric relation is transitive." *}
|
|
173 |
|
|
174 |
lemma "\<lbrakk> \<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x \<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
|
14462
|
175 |
(* refute -- works well with ZChaff, but the internal solver is too slow *)
|
14350
|
176 |
oops
|
|
177 |
|
14465
|
178 |
text {* The "Drinker's theorem" ... *}
|
14350
|
179 |
|
|
180 |
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
|
14462
|
181 |
refute [maxsize=4] (* [maxsize=6] works well with ZChaff *)
|
14350
|
182 |
apply (auto simp add: ext)
|
|
183 |
done
|
|
184 |
|
14465
|
185 |
text {* ... and an incorrect version of it *}
|
14350
|
186 |
|
|
187 |
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
|
|
188 |
refute
|
|
189 |
oops
|
|
190 |
|
|
191 |
text {* "Every function has a fixed point." *}
|
|
192 |
|
|
193 |
lemma "\<exists>x. f x = x"
|
|
194 |
refute
|
|
195 |
oops
|
|
196 |
|
|
197 |
text {* "Function composition is commutative." *}
|
|
198 |
|
|
199 |
lemma "f (g x) = g (f x)"
|
|
200 |
refute
|
|
201 |
oops
|
|
202 |
|
|
203 |
text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
|
|
204 |
|
|
205 |
lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
|
|
206 |
refute
|
|
207 |
oops
|
|
208 |
|
|
209 |
subsection {* Higher-Order Logic *}
|
|
210 |
|
|
211 |
lemma "\<exists>P. P"
|
|
212 |
refute
|
|
213 |
apply auto
|
|
214 |
done
|
|
215 |
|
|
216 |
lemma "\<forall>P. P"
|
|
217 |
refute
|
|
218 |
oops
|
|
219 |
|
|
220 |
lemma "EX! P. P"
|
|
221 |
refute
|
|
222 |
apply auto
|
|
223 |
done
|
|
224 |
|
|
225 |
lemma "EX! P. P x"
|
|
226 |
refute
|
|
227 |
oops
|
|
228 |
|
|
229 |
lemma "P Q | Q x"
|
|
230 |
refute
|
|
231 |
oops
|
|
232 |
|
14455
|
233 |
lemma "P All"
|
|
234 |
refute
|
|
235 |
oops
|
|
236 |
|
|
237 |
lemma "P Ex"
|
|
238 |
refute
|
|
239 |
oops
|
|
240 |
|
|
241 |
lemma "P Ex1"
|
|
242 |
refute
|
|
243 |
oops
|
|
244 |
|
14350
|
245 |
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
|
|
246 |
|
|
247 |
constdefs
|
|
248 |
"trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
|
|
249 |
"trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
|
|
250 |
"subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
|
|
251 |
"subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
|
|
252 |
"trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
|
|
253 |
"trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
|
|
254 |
|
|
255 |
lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
|
|
256 |
refute
|
|
257 |
oops
|
|
258 |
|
|
259 |
text {* "The union of transitive closures is equal to the transitive closure of unions." *}
|
|
260 |
|
|
261 |
lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
|
|
262 |
\<longrightarrow> trans_closure TP P
|
|
263 |
\<longrightarrow> trans_closure TR R
|
|
264 |
\<longrightarrow> (T x y = (TP x y | TR x y))"
|
14462
|
265 |
(* refute -- works well with ZChaff, but the internal solver is too slow *)
|
14350
|
266 |
oops
|
|
267 |
|
|
268 |
text {* "Every surjective function is invertible." *}
|
|
269 |
|
|
270 |
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
|
|
271 |
refute
|
|
272 |
oops
|
|
273 |
|
|
274 |
text {* "Every invertible function is surjective." *}
|
|
275 |
|
|
276 |
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
|
|
277 |
refute
|
|
278 |
oops
|
|
279 |
|
|
280 |
text {* Every point is a fixed point of some function. *}
|
|
281 |
|
|
282 |
lemma "\<exists>f. f x = x"
|
14455
|
283 |
refute [maxsize=4]
|
14350
|
284 |
apply (rule_tac x="\<lambda>x. x" in exI)
|
|
285 |
apply simp
|
|
286 |
done
|
|
287 |
|
14465
|
288 |
text {* Axiom of Choice: first an incorrect version ... *}
|
14350
|
289 |
|
|
290 |
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
|
|
291 |
refute
|
|
292 |
oops
|
|
293 |
|
14465
|
294 |
text {* ... and now two correct ones *}
|
14350
|
295 |
|
|
296 |
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
|
14455
|
297 |
refute [maxsize=5]
|
14350
|
298 |
apply (simp add: choice)
|
|
299 |
done
|
|
300 |
|
|
301 |
lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
|
14462
|
302 |
refute [maxsize=3] (* [maxsize=4] works well with ZChaff *)
|
14350
|
303 |
apply auto
|
|
304 |
apply (simp add: ex1_implies_ex choice)
|
|
305 |
apply (fast intro: ext)
|
|
306 |
done
|
|
307 |
|
|
308 |
subsection {* Meta-logic *}
|
|
309 |
|
|
310 |
lemma "!!x. P x"
|
|
311 |
refute
|
|
312 |
oops
|
|
313 |
|
|
314 |
lemma "f x == g x"
|
|
315 |
refute
|
|
316 |
oops
|
|
317 |
|
|
318 |
lemma "P \<Longrightarrow> Q"
|
|
319 |
refute
|
|
320 |
oops
|
|
321 |
|
|
322 |
lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
|
|
323 |
refute
|
|
324 |
oops
|
|
325 |
|
|
326 |
subsection {* Schematic variables *}
|
|
327 |
|
|
328 |
lemma "?P"
|
|
329 |
refute
|
|
330 |
apply auto
|
|
331 |
done
|
|
332 |
|
|
333 |
lemma "x = ?y"
|
|
334 |
refute
|
|
335 |
apply auto
|
|
336 |
done
|
|
337 |
|
|
338 |
subsection {* Abstractions *}
|
|
339 |
|
|
340 |
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
|
|
341 |
refute
|
|
342 |
oops
|
|
343 |
|
|
344 |
lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
|
|
345 |
refute
|
|
346 |
oops
|
|
347 |
|
|
348 |
lemma "(\<lambda>x. x) = (\<lambda>y. y)"
|
|
349 |
refute
|
|
350 |
apply simp
|
|
351 |
done
|
|
352 |
|
|
353 |
subsection {* Sets *}
|
|
354 |
|
|
355 |
lemma "P (A::'a set)"
|
|
356 |
refute
|
|
357 |
oops
|
|
358 |
|
|
359 |
lemma "P (A::'a set set)"
|
|
360 |
refute
|
|
361 |
oops
|
|
362 |
|
|
363 |
lemma "{x. P x} = {y. P y}"
|
14462
|
364 |
refute [maxsize=2] (* [maxsize=8] works well with ZChaff *)
|
14350
|
365 |
apply simp
|
|
366 |
done
|
|
367 |
|
|
368 |
lemma "x : {x. P x}"
|
|
369 |
refute
|
|
370 |
oops
|
|
371 |
|
14455
|
372 |
lemma "P op:"
|
|
373 |
refute
|
|
374 |
oops
|
|
375 |
|
|
376 |
lemma "P (op: x)"
|
|
377 |
refute
|
|
378 |
oops
|
|
379 |
|
|
380 |
lemma "P Collect"
|
|
381 |
refute
|
|
382 |
oops
|
|
383 |
|
14350
|
384 |
lemma "A Un B = A Int B"
|
|
385 |
refute
|
|
386 |
oops
|
|
387 |
|
|
388 |
lemma "(A Int B) Un C = (A Un C) Int B"
|
|
389 |
refute
|
|
390 |
oops
|
|
391 |
|
|
392 |
lemma "Ball A P \<longrightarrow> Bex A P"
|
14455
|
393 |
refute
|
|
394 |
oops
|
|
395 |
|
|
396 |
subsection {* arbitrary *}
|
|
397 |
|
|
398 |
lemma "arbitrary"
|
|
399 |
refute
|
|
400 |
oops
|
|
401 |
|
|
402 |
lemma "P arbitrary"
|
|
403 |
refute
|
|
404 |
oops
|
|
405 |
|
|
406 |
lemma "arbitrary x"
|
|
407 |
refute
|
|
408 |
oops
|
|
409 |
|
|
410 |
lemma "arbitrary arbitrary"
|
|
411 |
refute
|
|
412 |
oops
|
|
413 |
|
|
414 |
subsection {* The *}
|
|
415 |
|
|
416 |
lemma "The P"
|
|
417 |
refute
|
|
418 |
oops
|
|
419 |
|
|
420 |
lemma "P The"
|
14350
|
421 |
refute
|
|
422 |
oops
|
|
423 |
|
14455
|
424 |
lemma "P (The P)"
|
|
425 |
refute
|
|
426 |
oops
|
|
427 |
|
|
428 |
lemma "(THE x. x=y) = z"
|
|
429 |
refute
|
|
430 |
oops
|
|
431 |
|
|
432 |
lemma "Ex P \<longrightarrow> P (The P)"
|
14462
|
433 |
(* refute -- works well with ZChaff, but the internal solver is too slow *)
|
14455
|
434 |
oops
|
|
435 |
|
|
436 |
subsection {* Eps *}
|
|
437 |
|
|
438 |
lemma "Eps P"
|
|
439 |
refute
|
|
440 |
oops
|
|
441 |
|
|
442 |
lemma "P Eps"
|
|
443 |
refute
|
|
444 |
oops
|
|
445 |
|
|
446 |
lemma "P (Eps P)"
|
|
447 |
refute
|
|
448 |
oops
|
|
449 |
|
|
450 |
lemma "(SOME x. x=y) = z"
|
|
451 |
refute
|
|
452 |
oops
|
|
453 |
|
|
454 |
lemma "Ex P \<longrightarrow> P (Eps P)"
|
14462
|
455 |
refute [maxsize=2] (* [maxsize=3] works well with ZChaff *)
|
14455
|
456 |
apply (auto simp add: someI)
|
|
457 |
done
|
|
458 |
|
|
459 |
subsection {* Inductive datatypes *}
|
14350
|
460 |
|
|
461 |
subsubsection {* unit *}
|
|
462 |
|
|
463 |
lemma "P (x::unit)"
|
|
464 |
refute
|
|
465 |
oops
|
|
466 |
|
|
467 |
lemma "\<forall>x::unit. P x"
|
|
468 |
refute
|
|
469 |
oops
|
|
470 |
|
|
471 |
lemma "P ()"
|
|
472 |
refute
|
|
473 |
oops
|
|
474 |
|
14455
|
475 |
subsubsection {* option *}
|
|
476 |
|
|
477 |
lemma "P (x::'a option)"
|
|
478 |
refute
|
|
479 |
oops
|
|
480 |
|
|
481 |
lemma "\<forall>x::'a option. P x"
|
|
482 |
refute
|
|
483 |
oops
|
|
484 |
|
|
485 |
lemma "P (Some x)"
|
|
486 |
refute
|
|
487 |
oops
|
|
488 |
|
14350
|
489 |
subsubsection {* * *}
|
|
490 |
|
|
491 |
lemma "P (x::'a*'b)"
|
14455
|
492 |
refute
|
14350
|
493 |
oops
|
|
494 |
|
|
495 |
lemma "\<forall>x::'a*'b. P x"
|
14455
|
496 |
refute
|
14350
|
497 |
oops
|
|
498 |
|
|
499 |
lemma "P (x,y)"
|
14455
|
500 |
refute
|
14350
|
501 |
oops
|
|
502 |
|
|
503 |
lemma "P (fst x)"
|
14455
|
504 |
refute
|
14350
|
505 |
oops
|
|
506 |
|
|
507 |
lemma "P (snd x)"
|
14455
|
508 |
refute
|
|
509 |
oops
|
|
510 |
|
|
511 |
lemma "P Pair"
|
|
512 |
refute
|
14350
|
513 |
oops
|
|
514 |
|
|
515 |
subsubsection {* + *}
|
|
516 |
|
|
517 |
lemma "P (x::'a+'b)"
|
14455
|
518 |
refute
|
14350
|
519 |
oops
|
|
520 |
|
|
521 |
lemma "\<forall>x::'a+'b. P x"
|
14455
|
522 |
refute
|
14350
|
523 |
oops
|
|
524 |
|
|
525 |
lemma "P (Inl x)"
|
14455
|
526 |
refute
|
14350
|
527 |
oops
|
|
528 |
|
|
529 |
lemma "P (Inr x)"
|
14455
|
530 |
refute
|
|
531 |
oops
|
|
532 |
|
|
533 |
lemma "P Inl"
|
|
534 |
refute
|
14350
|
535 |
oops
|
|
536 |
|
|
537 |
subsubsection {* Non-recursive datatypes *}
|
|
538 |
|
14455
|
539 |
datatype T1 = A | B
|
14350
|
540 |
|
|
541 |
lemma "P (x::T1)"
|
|
542 |
refute
|
|
543 |
oops
|
|
544 |
|
|
545 |
lemma "\<forall>x::T1. P x"
|
|
546 |
refute
|
|
547 |
oops
|
|
548 |
|
14455
|
549 |
lemma "P A"
|
14350
|
550 |
refute
|
|
551 |
oops
|
|
552 |
|
14455
|
553 |
datatype 'a T2 = C T1 | D 'a
|
|
554 |
|
|
555 |
lemma "P (x::'a T2)"
|
14350
|
556 |
refute
|
|
557 |
oops
|
|
558 |
|
14455
|
559 |
lemma "\<forall>x::'a T2. P x"
|
14350
|
560 |
refute
|
|
561 |
oops
|
|
562 |
|
14455
|
563 |
lemma "P D"
|
14350
|
564 |
refute
|
|
565 |
oops
|
|
566 |
|
14455
|
567 |
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
|
|
568 |
|
|
569 |
lemma "P E"
|
|
570 |
refute
|
14350
|
571 |
oops
|
|
572 |
|
|
573 |
subsubsection {* Recursive datatypes *}
|
|
574 |
|
|
575 |
datatype Nat = Zero | Suc Nat
|
|
576 |
|
|
577 |
lemma "P (x::Nat)"
|
|
578 |
oops
|
|
579 |
|
|
580 |
lemma "\<forall>x::Nat. P x"
|
|
581 |
oops
|
|
582 |
|
|
583 |
lemma "P (Suc Zero)"
|
|
584 |
oops
|
|
585 |
|
|
586 |
datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
|
|
587 |
|
|
588 |
lemma "P (x::'a BinTree)"
|
|
589 |
oops
|
|
590 |
|
|
591 |
lemma "\<forall>x::'a BinTree. P x"
|
|
592 |
oops
|
|
593 |
|
|
594 |
subsubsection {* Mutually recursive datatypes *}
|
|
595 |
|
|
596 |
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
|
|
597 |
and 'a bexp = Equal "'a aexp" "'a aexp"
|
|
598 |
|
|
599 |
lemma "P (x::'a aexp)"
|
|
600 |
oops
|
|
601 |
|
|
602 |
lemma "\<forall>x::'a aexp. P x"
|
|
603 |
oops
|
|
604 |
|
|
605 |
lemma "P (x::'a bexp)"
|
|
606 |
oops
|
|
607 |
|
|
608 |
lemma "\<forall>x::'a bexp. P x"
|
|
609 |
oops
|
|
610 |
|
|
611 |
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
|
|
612 |
oops
|
|
613 |
|
|
614 |
subsubsection {* Other datatype examples *}
|
|
615 |
|
|
616 |
datatype InfTree = Leaf | Node "Nat \<Rightarrow> InfTree"
|
|
617 |
|
|
618 |
lemma "P (x::InfTree)"
|
|
619 |
oops
|
|
620 |
|
|
621 |
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
|
|
622 |
|
|
623 |
lemma "P (x::'a lambda)"
|
|
624 |
oops
|
|
625 |
|
|
626 |
end
|