src/HOL/Nitpick_Examples/Refute_Nits.thy
 author blanchet Mon Feb 22 19:31:00 2010 +0100 (2010-02-22) changeset 35284 9edc2bd6d2bd parent 35087 e385fa507468 child 35338 38848da259c0 permissions -rw-r--r--
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
1 (*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
2     Author:     Jasmin Blanchette, TU Muenchen
5 Refute examples adapted to Nitpick.
6 *)
10 theory Refute_Nits
11 imports Main
12 begin
14 nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
15                 timeout = 60 s]
17 lemma "P \<and> Q"
18 apply (rule conjI)
19 nitpick [expect = genuine] 1
20 nitpick [expect = genuine] 2
21 nitpick [expect = genuine]
22 nitpick [card = 5, expect = genuine]
23 nitpick [sat_solver = SAT4J, expect = genuine] 2
24 oops
26 subsection {* Examples and Test Cases *}
28 subsubsection {* Propositional logic *}
30 lemma "True"
31 nitpick [expect = none]
32 apply auto
33 done
35 lemma "False"
36 nitpick [expect = genuine]
37 oops
39 lemma "P"
40 nitpick [expect = genuine]
41 oops
43 lemma "\<not> P"
44 nitpick [expect = genuine]
45 oops
47 lemma "P \<and> Q"
48 nitpick [expect = genuine]
49 oops
51 lemma "P \<or> Q"
52 nitpick [expect = genuine]
53 oops
55 lemma "P \<longrightarrow> Q"
56 nitpick [expect = genuine]
57 oops
59 lemma "(P\<Colon>bool) = Q"
60 nitpick [expect = genuine]
61 oops
63 lemma "(P \<or> Q) \<longrightarrow> (P \<and> Q)"
64 nitpick [expect = genuine]
65 oops
67 subsubsection {* Predicate logic *}
69 lemma "P x y z"
70 nitpick [expect = genuine]
71 oops
73 lemma "P x y \<longrightarrow> P y x"
74 nitpick [expect = genuine]
75 oops
77 lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
78 nitpick [expect = genuine]
79 oops
81 subsubsection {* Equality *}
83 lemma "P = True"
84 nitpick [expect = genuine]
85 oops
87 lemma "P = False"
88 nitpick [expect = genuine]
89 oops
91 lemma "x = y"
92 nitpick [expect = genuine]
93 oops
95 lemma "f x = g x"
96 nitpick [expect = genuine]
97 oops
99 lemma "(f\<Colon>'a\<Rightarrow>'b) = g"
100 nitpick [expect = genuine]
101 oops
103 lemma "(f\<Colon>('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
104 nitpick [expect = genuine]
105 oops
107 lemma "distinct [a, b]"
108 nitpick [expect = genuine]
109 apply simp
110 nitpick [expect = genuine]
111 oops
113 subsubsection {* First-Order Logic *}
115 lemma "\<exists>x. P x"
116 nitpick [expect = genuine]
117 oops
119 lemma "\<forall>x. P x"
120 nitpick [expect = genuine]
121 oops
123 lemma "\<exists>!x. P x"
124 nitpick [expect = genuine]
125 oops
127 lemma "Ex P"
128 nitpick [expect = genuine]
129 oops
131 lemma "All P"
132 nitpick [expect = genuine]
133 oops
135 lemma "Ex1 P"
136 nitpick [expect = genuine]
137 oops
139 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
140 nitpick [expect = genuine]
141 oops
143 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
144 nitpick [expect = genuine]
145 oops
147 lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
148 nitpick [expect = genuine]
149 oops
151 text {* A true statement (also testing names of free and bound variables being identical) *}
153 lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
154 nitpick [expect = none]
155 apply fast
156 done
158 text {* "A type has at most 4 elements." *}
160 lemma "\<not> distinct [a, b, c, d, e]"
161 nitpick [expect = genuine]
162 apply simp
163 nitpick [expect = genuine]
164 oops
166 lemma "distinct [a, b, c, d]"
167 nitpick [expect = genuine]
168 apply simp
169 nitpick [expect = genuine]
170 oops
172 text {* "Every reflexive and symmetric relation is transitive." *}
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"
175 nitpick [expect = genuine]
176 oops
178 text {* The ``Drinker's theorem'' *}
180 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
181 nitpick [expect = none]
182 apply (auto simp add: ext)
183 done
185 text {* And an incorrect version of it *}
187 lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
188 nitpick [expect = genuine]
189 oops
191 text {* "Every function has a fixed point." *}
193 lemma "\<exists>x. f x = x"
194 nitpick [expect = genuine]
195 oops
197 text {* "Function composition is commutative." *}
199 lemma "f (g x) = g (f x)"
200 nitpick [expect = genuine]
201 oops
203 text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
205 lemma "((P\<Colon>('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
206 nitpick [expect = genuine]
207 oops
209 subsubsection {* Higher-Order Logic *}
211 lemma "\<exists>P. P"
212 nitpick [expect = none]
213 apply auto
214 done
216 lemma "\<forall>P. P"
217 nitpick [expect = genuine]
218 oops
220 lemma "\<exists>!P. P"
221 nitpick [expect = none]
222 apply auto
223 done
225 lemma "\<exists>!P. P x"
226 nitpick [expect = genuine]
227 oops
229 lemma "P Q \<or> Q x"
230 nitpick [expect = genuine]
231 oops
233 lemma "x \<noteq> All"
234 nitpick [expect = genuine]
235 oops
237 lemma "x \<noteq> Ex"
238 nitpick [expect = genuine]
239 oops
241 lemma "x \<noteq> Ex1"
242 nitpick [expect = genuine]
243 oops
245 text {* ``The transitive closure of an arbitrary relation is non-empty.'' *}
247 constdefs
248 "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
249 "trans P \<equiv> (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 \<equiv> (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 \<equiv> (subset Q P) \<and> (trans P) \<and> (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
255 lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
256 nitpick [expect = genuine]
257 oops
259 text {* ``The union of transitive closures is equal to the transitive closure of unions.'' *}
261 lemma "(\<forall>x y. (P x y \<or> R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y \<or> 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 \<or> TR x y))"
265 nitpick [expect = genuine]
266 oops
268 text {* ``Every surjective function is invertible.'' *}
270 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
271 nitpick [expect = genuine]
272 oops
274 text {* ``Every invertible function is surjective.'' *}
276 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
277 nitpick [expect = genuine]
278 oops
280 text {* ``Every point is a fixed point of some function.'' *}
282 lemma "\<exists>f. f x = x"
283 nitpick [card = 1\<midarrow>7, expect = none]
284 apply (rule_tac x = "\<lambda>x. x" in exI)
285 apply simp
286 done
288 text {* Axiom of Choice: first an incorrect version *}
290 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
291 nitpick [expect = genuine]
292 oops
294 text {* And now two correct ones *}
296 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
297 nitpick [card = 1-4, expect = none]
299 done
301 lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
302 nitpick [card = 1-3, expect = none]
303 apply auto
304  apply (simp add: ex1_implies_ex choice)
305 apply (fast intro: ext)
306 done
308 subsubsection {* Metalogic *}
310 lemma "\<And>x. P x"
311 nitpick [expect = genuine]
312 oops
314 lemma "f x \<equiv> g x"
315 nitpick [expect = genuine]
316 oops
318 lemma "P \<Longrightarrow> Q"
319 nitpick [expect = genuine]
320 oops
322 lemma "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"
323 nitpick [expect = genuine]
324 oops
326 lemma "(x \<equiv> all) \<Longrightarrow> False"
327 nitpick [expect = genuine]
328 oops
330 lemma "(x \<equiv> (op \<equiv>)) \<Longrightarrow> False"
331 nitpick [expect = genuine]
332 oops
334 lemma "(x \<equiv> (op \<Longrightarrow>)) \<Longrightarrow> False"
335 nitpick [expect = genuine]
336 oops
338 subsubsection {* Schematic Variables *}
340 lemma "?P"
341 nitpick [expect = none]
342 apply auto
343 done
345 lemma "x = ?y"
346 nitpick [expect = none]
347 apply auto
348 done
350 subsubsection {* Abstractions *}
352 lemma "(\<lambda>x. x) = (\<lambda>x. y)"
353 nitpick [expect = genuine]
354 oops
356 lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
357 nitpick [expect = genuine]
358 oops
360 lemma "(\<lambda>x. x) = (\<lambda>y. y)"
361 nitpick [expect = none]
362 apply simp
363 done
365 subsubsection {* Sets *}
367 lemma "P (A\<Colon>'a set)"
368 nitpick [expect = genuine]
369 oops
371 lemma "P (A\<Colon>'a set set)"
372 nitpick [expect = genuine]
373 oops
375 lemma "{x. P x} = {y. P y}"
376 nitpick [expect = none]
377 apply simp
378 done
380 lemma "x \<in> {x. P x}"
381 nitpick [expect = genuine]
382 oops
384 lemma "P (op \<in>)"
385 nitpick [expect = genuine]
386 oops
388 lemma "P (op \<in> x)"
389 nitpick [expect = genuine]
390 oops
392 lemma "P Collect"
393 nitpick [expect = genuine]
394 oops
396 lemma "A Un B = A Int B"
397 nitpick [expect = genuine]
398 oops
400 lemma "(A Int B) Un C = (A Un C) Int B"
401 nitpick [expect = genuine]
402 oops
404 lemma "Ball A P \<longrightarrow> Bex A P"
405 nitpick [expect = genuine]
406 oops
408 subsubsection {* @{const undefined} *}
410 lemma "undefined"
411 nitpick [expect = genuine]
412 oops
414 lemma "P undefined"
415 nitpick [expect = genuine]
416 oops
418 lemma "undefined x"
419 nitpick [expect = genuine]
420 oops
422 lemma "undefined undefined"
423 nitpick [expect = genuine]
424 oops
426 subsubsection {* @{const The} *}
428 lemma "The P"
429 nitpick [expect = genuine]
430 oops
432 lemma "P The"
433 nitpick [expect = genuine]
434 oops
436 lemma "P (The P)"
437 nitpick [expect = genuine]
438 oops
440 lemma "(THE x. x=y) = z"
441 nitpick [expect = genuine]
442 oops
444 lemma "Ex P \<longrightarrow> P (The P)"
445 nitpick [expect = genuine]
446 oops
448 subsubsection {* @{const Eps} *}
450 lemma "Eps P"
451 nitpick [expect = genuine]
452 oops
454 lemma "P Eps"
455 nitpick [expect = genuine]
456 oops
458 lemma "P (Eps P)"
459 nitpick [expect = genuine]
460 oops
462 lemma "(SOME x. x=y) = z"
463 nitpick [expect = genuine]
464 oops
466 lemma "Ex P \<longrightarrow> P (Eps P)"
467 nitpick [expect = none]
468 apply (auto simp add: someI)
469 done
471 subsubsection {* Operations on Natural Numbers *}
473 lemma "(x\<Colon>nat) + y = 0"
474 nitpick [expect = genuine]
475 oops
477 lemma "(x\<Colon>nat) = x + x"
478 nitpick [expect = genuine]
479 oops
481 lemma "(x\<Colon>nat) - y + y = x"
482 nitpick [expect = genuine]
483 oops
485 lemma "(x\<Colon>nat) = x * x"
486 nitpick [expect = genuine]
487 oops
489 lemma "(x\<Colon>nat) < x + y"
490 nitpick [card = 1, expect = genuine]
491 nitpick [card = 2-5, expect = genuine]
492 oops
494 text {* \<times> *}
496 lemma "P (x\<Colon>'a\<times>'b)"
497 nitpick [expect = genuine]
498 oops
500 lemma "\<forall>x\<Colon>'a\<times>'b. P x"
501 nitpick [expect = genuine]
502 oops
504 lemma "P (x, y)"
505 nitpick [expect = genuine]
506 oops
508 lemma "P (fst x)"
509 nitpick [expect = genuine]
510 oops
512 lemma "P (snd x)"
513 nitpick [expect = genuine]
514 oops
516 lemma "P Pair"
517 nitpick [expect = genuine]
518 oops
520 lemma "prod_rec f p = f (fst p) (snd p)"
521 nitpick [expect = none]
522 by (case_tac p) auto
524 lemma "prod_rec f (a, b) = f a b"
525 nitpick [expect = none]
526 by auto
528 lemma "P (prod_rec f x)"
529 nitpick [expect = genuine]
530 oops
532 lemma "P (case x of Pair a b \<Rightarrow> f a b)"
533 nitpick [expect = genuine]
534 oops
536 subsubsection {* Subtypes (typedef), typedecl *}
538 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
540 typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
541 by auto
543 lemma "(x\<Colon>'a myTdef) = y"
544 nitpick [expect = genuine]
545 oops
547 typedecl myTdecl
549 typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
550 by auto
552 lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
553 nitpick [expect = genuine]
554 oops
556 subsubsection {* Inductive Datatypes *}
558 text {* unit *}
560 lemma "P (x\<Colon>unit)"
561 nitpick [expect = genuine]
562 oops
564 lemma "\<forall>x\<Colon>unit. P x"
565 nitpick [expect = genuine]
566 oops
568 lemma "P ()"
569 nitpick [expect = genuine]
570 oops
572 lemma "unit_rec u x = u"
573 nitpick [expect = none]
574 apply simp
575 done
577 lemma "P (unit_rec u x)"
578 nitpick [expect = genuine]
579 oops
581 lemma "P (case x of () \<Rightarrow> u)"
582 nitpick [expect = genuine]
583 oops
585 text {* option *}
587 lemma "P (x\<Colon>'a option)"
588 nitpick [expect = genuine]
589 oops
591 lemma "\<forall>x\<Colon>'a option. P x"
592 nitpick [expect = genuine]
593 oops
595 lemma "P None"
596 nitpick [expect = genuine]
597 oops
599 lemma "P (Some x)"
600 nitpick [expect = genuine]
601 oops
603 lemma "option_rec n s None = n"
604 nitpick [expect = none]
605 apply simp
606 done
608 lemma "option_rec n s (Some x) = s x"
609 nitpick [expect = none]
610 apply simp
611 done
613 lemma "P (option_rec n s x)"
614 nitpick [expect = genuine]
615 oops
617 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
618 nitpick [expect = genuine]
619 oops
621 text {* + *}
623 lemma "P (x\<Colon>'a+'b)"
624 nitpick [expect = genuine]
625 oops
627 lemma "\<forall>x\<Colon>'a+'b. P x"
628 nitpick [expect = genuine]
629 oops
631 lemma "P (Inl x)"
632 nitpick [expect = genuine]
633 oops
635 lemma "P (Inr x)"
636 nitpick [expect = genuine]
637 oops
639 lemma "P Inl"
640 nitpick [expect = genuine]
641 oops
643 lemma "sum_rec l r (Inl x) = l x"
644 nitpick [expect = none]
645 apply simp
646 done
648 lemma "sum_rec l r (Inr x) = r x"
649 nitpick [expect = none]
650 apply simp
651 done
653 lemma "P (sum_rec l r x)"
654 nitpick [expect = genuine]
655 oops
657 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
658 nitpick [expect = genuine]
659 oops
661 text {* Non-recursive datatypes *}
663 datatype T1 = A | B
665 lemma "P (x\<Colon>T1)"
666 nitpick [expect = genuine]
667 oops
669 lemma "\<forall>x\<Colon>T1. P x"
670 nitpick [expect = genuine]
671 oops
673 lemma "P A"
674 nitpick [expect = genuine]
675 oops
677 lemma "P B"
678 nitpick [expect = genuine]
679 oops
681 lemma "T1_rec a b A = a"
682 nitpick [expect = none]
683 apply simp
684 done
686 lemma "T1_rec a b B = b"
687 nitpick [expect = none]
688 apply simp
689 done
691 lemma "P (T1_rec a b x)"
692 nitpick [expect = genuine]
693 oops
695 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
696 nitpick [expect = genuine]
697 oops
699 datatype 'a T2 = C T1 | D 'a
701 lemma "P (x\<Colon>'a T2)"
702 nitpick [expect = genuine]
703 oops
705 lemma "\<forall>x\<Colon>'a T2. P x"
706 nitpick [expect = genuine]
707 oops
709 lemma "P D"
710 nitpick [expect = genuine]
711 oops
713 lemma "T2_rec c d (C x) = c x"
714 nitpick [expect = none]
715 apply simp
716 done
718 lemma "T2_rec c d (D x) = d x"
719 nitpick [expect = none]
720 apply simp
721 done
723 lemma "P (T2_rec c d x)"
724 nitpick [expect = genuine]
725 oops
727 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
728 nitpick [expect = genuine]
729 oops
731 datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
733 lemma "P (x\<Colon>('a, 'b) T3)"
734 nitpick [expect = genuine]
735 oops
737 lemma "\<forall>x\<Colon>('a, 'b) T3. P x"
738 nitpick [expect = genuine]
739 oops
741 lemma "P E"
742 nitpick [expect = genuine]
743 oops
745 lemma "T3_rec e (E x) = e x"
746 nitpick [card = 1\<midarrow>4, expect = none]
747 apply simp
748 done
750 lemma "P (T3_rec e x)"
751 nitpick [expect = genuine]
752 oops
754 lemma "P (case x of E f \<Rightarrow> e f)"
755 nitpick [expect = genuine]
756 oops
758 text {* Recursive datatypes *}
760 text {* nat *}
762 lemma "P (x\<Colon>nat)"
763 nitpick [expect = genuine]
764 oops
766 lemma "\<forall>x\<Colon>nat. P x"
767 nitpick [expect = genuine]
768 oops
770 lemma "P (Suc 0)"
771 nitpick [expect = genuine]
772 oops
774 lemma "P Suc"
775 nitpick [card = 1\<midarrow>7, expect = none]
776 oops
778 lemma "nat_rec zero suc 0 = zero"
779 nitpick [expect = none]
780 apply simp
781 done
783 lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
784 nitpick [expect = none]
785 apply simp
786 done
788 lemma "P (nat_rec zero suc x)"
789 nitpick [expect = genuine]
790 oops
792 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
793 nitpick [expect = genuine]
794 oops
796 text {* 'a list *}
798 lemma "P (xs\<Colon>'a list)"
799 nitpick [expect = genuine]
800 oops
802 lemma "\<forall>xs\<Colon>'a list. P xs"
803 nitpick [expect = genuine]
804 oops
806 lemma "P [x, y]"
807 nitpick [expect = genuine]
808 oops
810 lemma "list_rec nil cons [] = nil"
811 nitpick [card = 1\<midarrow>5, expect = none]
812 apply simp
813 done
815 lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
816 nitpick [card = 1\<midarrow>5, expect = none]
817 apply simp
818 done
820 lemma "P (list_rec nil cons xs)"
821 nitpick [expect = genuine]
822 oops
824 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
825 nitpick [expect = genuine]
826 oops
828 lemma "(xs\<Colon>'a list) = ys"
829 nitpick [expect = genuine]
830 oops
832 lemma "a # xs = b # xs"
833 nitpick [expect = genuine]
834 oops
836 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
838 lemma "P (x\<Colon>BitList)"
839 nitpick [expect = genuine]
840 oops
842 lemma "\<forall>x\<Colon>BitList. P x"
843 nitpick [expect = genuine]
844 oops
846 lemma "P (Bit0 (Bit1 BitListNil))"
847 nitpick [expect = genuine]
848 oops
850 lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
851 nitpick [expect = none]
852 apply simp
853 done
855 lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
856 nitpick [expect = none]
857 apply simp
858 done
860 lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
861 nitpick [expect = none]
862 apply simp
863 done
865 lemma "P (BitList_rec nil bit0 bit1 x)"
866 nitpick [expect = genuine]
867 oops
869 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
871 lemma "P (x\<Colon>'a BinTree)"
872 nitpick [expect = genuine]
873 oops
875 lemma "\<forall>x\<Colon>'a BinTree. P x"
876 nitpick [expect = genuine]
877 oops
879 lemma "P (Node (Leaf x) (Leaf y))"
880 nitpick [expect = genuine]
881 oops
883 lemma "BinTree_rec l n (Leaf x) = l x"
884 nitpick [expect = none]
885 apply simp
886 done
888 lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
889 nitpick [card = 1\<midarrow>5, expect = none]
890 apply simp
891 done
893 lemma "P (BinTree_rec l n x)"
894 nitpick [expect = genuine]
895 oops
897 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
898 nitpick [expect = genuine]
899 oops
901 text {* Mutually recursive datatypes *}
903 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
904  and 'a bexp = Equal "'a aexp" "'a aexp"
906 lemma "P (x\<Colon>'a aexp)"
907 nitpick [expect = genuine]
908 oops
910 lemma "\<forall>x\<Colon>'a aexp. P x"
911 nitpick [expect = genuine]
912 oops
914 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
915 nitpick [expect = genuine]
916 oops
918 lemma "P (x\<Colon>'a bexp)"
919 nitpick [expect = genuine]
920 oops
922 lemma "\<forall>x\<Colon>'a bexp. P x"
923 nitpick [expect = genuine]
924 oops
926 lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
927 nitpick [card = 1\<midarrow>3, expect = none]
928 apply simp
929 done
931 lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
932 nitpick [card = 1\<midarrow>3, expect = none]
933 apply simp
934 done
936 lemma "P (aexp_bexp_rec_1 number ite equal x)"
937 nitpick [expect = genuine]
938 oops
940 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
941 nitpick [expect = genuine]
942 oops
944 lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
945 nitpick [card = 1\<midarrow>3, expect = none]
946 apply simp
947 done
949 lemma "P (aexp_bexp_rec_2 number ite equal x)"
950 nitpick [expect = genuine]
951 oops
953 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
954 nitpick [expect = genuine]
955 oops
957 datatype X = A | B X | C Y
958      and Y = D X | E Y | F
960 lemma "P (x\<Colon>X)"
961 nitpick [expect = genuine]
962 oops
964 lemma "P (y\<Colon>Y)"
965 nitpick [expect = genuine]
966 oops
968 lemma "P (B (B A))"
969 nitpick [expect = genuine]
970 oops
972 lemma "P (B (C F))"
973 nitpick [expect = genuine]
974 oops
976 lemma "P (C (D A))"
977 nitpick [expect = genuine]
978 oops
980 lemma "P (C (E F))"
981 nitpick [expect = genuine]
982 oops
984 lemma "P (D (B A))"
985 nitpick [expect = genuine]
986 oops
988 lemma "P (D (C F))"
989 nitpick [expect = genuine]
990 oops
992 lemma "P (E (D A))"
993 nitpick [expect = genuine]
994 oops
996 lemma "P (E (E F))"
997 nitpick [expect = genuine]
998 oops
1000 lemma "P (C (D (C F)))"
1001 nitpick [expect = genuine]
1002 oops
1004 lemma "X_Y_rec_1 a b c d e f A = a"
1005 nitpick [card = 1\<midarrow>5, expect = none]
1006 apply simp
1007 done
1009 lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
1010 nitpick [card = 1\<midarrow>5, expect = none]
1011 apply simp
1012 done
1014 lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
1015 nitpick [card = 1\<midarrow>5, expect = none]
1016 apply simp
1017 done
1019 lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
1020 nitpick [card = 1\<midarrow>5, expect = none]
1021 apply simp
1022 done
1024 lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
1025 nitpick [card = 1\<midarrow>5, expect = none]
1026 apply simp
1027 done
1029 lemma "X_Y_rec_2 a b c d e f F = f"
1030 nitpick [card = 1\<midarrow>5, expect = none]
1031 apply simp
1032 done
1034 lemma "P (X_Y_rec_1 a b c d e f x)"
1035 nitpick [expect = genuine]
1036 oops
1038 lemma "P (X_Y_rec_2 a b c d e f y)"
1039 nitpick [expect = genuine]
1040 oops
1042 text {* Other datatype examples *}
1044 text {* Indirect recursion is implemented via mutual recursion. *}
1046 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
1048 lemma "P (x\<Colon>XOpt)"
1049 nitpick [expect = genuine]
1050 oops
1052 lemma "P (CX None)"
1053 nitpick [expect = genuine]
1054 oops
1056 lemma "P (CX (Some (CX None)))"
1057 nitpick [expect = genuine]
1058 oops
1060 lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
1061 nitpick [card = 1\<midarrow>5, expect = none]
1062 apply simp
1063 done
1065 lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
1066 nitpick [card = 1\<midarrow>3, expect = none]
1067 apply simp
1068 done
1070 lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
1071 nitpick [card = 1\<midarrow>4, expect = none]
1072 apply simp
1073 done
1075 lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
1076 nitpick [card = 1\<midarrow>4, expect = none]
1077 apply simp
1078 done
1080 lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
1081 nitpick [card = 1\<midarrow>4, expect = none]
1082 apply simp
1083 done
1085 lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
1086 nitpick [card = 1\<midarrow>4, expect = none]
1087 apply simp
1088 done
1090 lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
1091 nitpick [expect = genuine]
1092 oops
1094 lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
1095 nitpick [expect = genuine]
1096 oops
1098 lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
1099 nitpick [expect = genuine]
1100 oops
1102 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
1104 lemma "P (x\<Colon>'a YOpt)"
1105 nitpick [expect = genuine]
1106 oops
1108 lemma "P (CY None)"
1109 nitpick [expect = genuine]
1110 oops
1112 lemma "P (CY (Some (\<lambda>a. CY None)))"
1113 nitpick [expect = genuine]
1114 oops
1116 lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
1117 nitpick [card = 1\<midarrow>2, expect = none]
1118 apply simp
1119 done
1121 lemma "YOpt_rec_2 cy n s None = n"
1122 nitpick [card = 1\<midarrow>2, expect = none]
1123 apply simp
1124 done
1126 lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
1127 nitpick [card = 1\<midarrow>2, expect = none]
1128 apply simp
1129 done
1131 lemma "P (YOpt_rec_1 cy n s x)"
1132 nitpick [expect = genuine]
1133 oops
1135 lemma "P (YOpt_rec_2 cy n s x)"
1136 nitpick [expect = genuine]
1137 oops
1139 datatype Trie = TR "Trie list"
1141 lemma "P (x\<Colon>Trie)"
1142 nitpick [expect = genuine]
1143 oops
1145 lemma "\<forall>x\<Colon>Trie. P x"
1146 nitpick [expect = genuine]
1147 oops
1149 lemma "P (TR [TR []])"
1150 nitpick [expect = genuine]
1151 oops
1153 lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
1154 nitpick [card = 1\<midarrow>4, expect = none]
1155 apply simp
1156 done
1158 lemma "Trie_rec_2 tr nil cons [] = nil"
1159 nitpick [card = 1\<midarrow>4, expect = none]
1160 apply simp
1161 done
1163 lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
1164 nitpick [card = 1\<midarrow>4, expect = none]
1165 apply simp
1166 done
1168 lemma "P (Trie_rec_1 tr nil cons x)"
1169 nitpick [card = 1, expect = genuine]
1170 oops
1172 lemma "P (Trie_rec_2 tr nil cons x)"
1173 nitpick [card = 1, expect = genuine]
1174 oops
1176 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
1178 lemma "P (x\<Colon>InfTree)"
1179 nitpick [expect = genuine]
1180 oops
1182 lemma "\<forall>x\<Colon>InfTree. P x"
1183 nitpick [expect = genuine]
1184 oops
1186 lemma "P (Node (\<lambda>n. Leaf))"
1187 nitpick [expect = genuine]
1188 oops
1190 lemma "InfTree_rec leaf node Leaf = leaf"
1191 nitpick [card = 1\<midarrow>3, expect = none]
1192 apply simp
1193 done
1195 lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
1196 nitpick [card = 1\<midarrow>3, expect = none]
1197 apply simp
1198 done
1200 lemma "P (InfTree_rec leaf node x)"
1201 nitpick [expect = genuine]
1202 oops
1204 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
1206 lemma "P (x\<Colon>'a lambda)"
1207 nitpick [expect = genuine]
1208 oops
1210 lemma "\<forall>x\<Colon>'a lambda. P x"
1211 nitpick [expect = genuine]
1212 oops
1214 lemma "P (Lam (\<lambda>a. Var a))"
1215 nitpick [card = 1\<midarrow>5, expect = none]
1216 nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
1217 oops
1219 lemma "lambda_rec var app lam (Var x) = var x"
1220 nitpick [card = 1\<midarrow>3, expect = none]
1221 apply simp
1222 done
1224 lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
1225 nitpick [card = 1\<midarrow>3, expect = none]
1226 apply simp
1227 done
1229 lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
1230 nitpick [card = 1\<midarrow>3, expect = none]
1231 apply simp
1232 done
1234 lemma "P (lambda_rec v a l x)"
1235 nitpick [expect = genuine]
1236 oops
1238 text {* Taken from "Inductive datatypes in HOL", p. 8: *}
1240 datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
1241 datatype 'c U = E "('c, 'c U) T"
1243 lemma "P (x\<Colon>'c U)"
1244 nitpick [expect = genuine]
1245 oops
1247 lemma "\<forall>x\<Colon>'c U. P x"
1248 nitpick [expect = genuine]
1249 oops
1251 lemma "P (E (C (\<lambda>a. True)))"
1252 nitpick [expect = genuine]
1253 oops
1255 lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
1256 nitpick [card = 1\<midarrow>3, expect = none]
1257 apply simp
1258 done
1260 lemma "U_rec_2 e c d nil cons (C x) = c x"
1261 nitpick [card = 1\<midarrow>3, expect = none]
1262 apply simp
1263 done
1265 lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
1266 nitpick [card = 1\<midarrow>3, expect = none]
1267 apply simp
1268 done
1270 lemma "U_rec_3 e c d nil cons [] = nil"
1271 nitpick [card = 1\<midarrow>3, expect = none]
1272 apply simp
1273 done
1275 lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
1276 nitpick [card = 1\<midarrow>3, expect = none]
1277 apply simp
1278 done
1280 lemma "P (U_rec_1 e c d nil cons x)"
1281 nitpick [expect = genuine]
1282 oops
1284 lemma "P (U_rec_2 e c d nil cons x)"
1285 nitpick [card = 1, expect = genuine]
1286 oops
1288 lemma "P (U_rec_3 e c d nil cons x)"
1289 nitpick [card = 1, expect = genuine]
1290 oops
1292 subsubsection {* Records *}
1294 record ('a, 'b) point =
1295   xpos :: 'a
1296   ypos :: 'b
1298 lemma "(x\<Colon>('a, 'b) point) = y"
1299 nitpick [expect = genuine]
1300 oops
1302 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
1303   ext :: 'c
1305 lemma "(x\<Colon>('a, 'b, 'c) extpoint) = y"
1306 nitpick [expect = genuine]
1307 oops
1309 subsubsection {* Inductively Defined Sets *}
1311 inductive_set undefinedSet :: "'a set" where
1312 "undefined \<in> undefinedSet"
1314 lemma "x \<in> undefinedSet"
1315 nitpick [expect = genuine]
1316 oops
1318 inductive_set evenCard :: "'a set set"
1319 where
1320 "{} \<in> evenCard" |
1321 "\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
1323 lemma "S \<in> evenCard"
1324 nitpick [expect = genuine]
1325 oops
1327 inductive_set
1328 even :: "nat set"
1329 and odd :: "nat set"
1330 where
1331 "0 \<in> even" |
1332 "n \<in> even \<Longrightarrow> Suc n \<in> odd" |
1333 "n \<in> odd \<Longrightarrow> Suc n \<in> even"
1335 lemma "n \<in> odd"
1336 nitpick [expect = genuine]
1337 oops
1339 consts f :: "'a \<Rightarrow> 'a"
1341 inductive_set a_even :: "'a set" and a_odd :: "'a set" where
1342 "undefined \<in> a_even" |
1343 "x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
1344 "x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
1346 lemma "x \<in> a_odd"
1347 nitpick [expect = genuine]
1348 oops
1350 subsubsection {* Examples Involving Special Functions *}
1352 lemma "card x = 0"
1353 nitpick [expect = genuine]
1354 oops
1356 lemma "finite x"
1357 nitpick [expect = none]
1358 oops
1360 lemma "xs @ [] = ys @ []"
1361 nitpick [expect = genuine]
1362 oops
1364 lemma "xs @ ys = ys @ xs"
1365 nitpick [expect = genuine]
1366 oops
1368 lemma "f (lfp f) = lfp f"
1369 nitpick [card = 2, expect = genuine]
1370 oops
1372 lemma "f (gfp f) = gfp f"
1373 nitpick [card = 2, expect = genuine]
1374 oops
1376 lemma "lfp f = gfp f"
1377 nitpick [card = 2, expect = genuine]
1378 oops
1382 text {* A type class without axioms: *}
1384 axclass classA
1386 lemma "P (x\<Colon>'a\<Colon>classA)"
1387 nitpick [expect = genuine]
1388 oops
1390 text {* The axiom of this type class does not contain any type variables: *}
1392 axclass classB
1393 classB_ax: "P \<or> \<not> P"
1395 lemma "P (x\<Colon>'a\<Colon>classB)"
1396 nitpick [expect = genuine]
1397 oops
1399 text {* An axiom with a type variable (denoting types which have at least two elements): *}
1401 axclass classC < type
1402 classC_ax: "\<exists>x y. x \<noteq> y"
1404 lemma "P (x\<Colon>'a\<Colon>classC)"
1405 nitpick [expect = genuine]
1406 oops
1408 lemma "\<exists>x y. (x\<Colon>'a\<Colon>classC) \<noteq> y"
1409 nitpick [expect = none]
1410 sorry
1412 text {* A type class for which a constant is defined: *}
1414 consts
1415 classD_const :: "'a \<Rightarrow> 'a"
1417 axclass classD < type
1418 classD_ax: "classD_const (classD_const x) = classD_const x"
1420 lemma "P (x\<Colon>'a\<Colon>classD)"
1421 nitpick [expect = genuine]
1422 oops
1424 text {* A type class with multiple superclasses: *}
1426 axclass classE < classC, classD
1428 lemma "P (x\<Colon>'a\<Colon>classE)"
1429 nitpick [expect = genuine]
1430 oops
1432 lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
1433 nitpick [expect = genuine]
1434 oops
1436 text {* OFCLASS: *}
1438 lemma "OFCLASS('a\<Colon>type, type_class)"
1439 nitpick [expect = none]
1440 apply intro_classes
1441 done
1443 lemma "OFCLASS('a\<Colon>classC, type_class)"
1444 nitpick [expect = none]
1445 apply intro_classes
1446 done
1448 lemma "OFCLASS('a, classB_class)"
1449 nitpick [expect = none]
1450 apply intro_classes
1451 apply simp
1452 done
1454 lemma "OFCLASS('a\<Colon>type, classC_class)"
1455 nitpick [expect = genuine]
1456 oops
1460 consts inverse :: "'a \<Rightarrow> 'a"