src/HOL/Nitpick_Examples/Refute_Nits.thy
 author wenzelm Mon Jan 11 21:21:02 2016 +0100 (2016-01-11) changeset 62145 5b946c81dfbf parent 61337 4645502c3c64 child 63167 0909deb8059b permissions -rw-r--r--
eliminated old defs;
1 (*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
2     Author:     Jasmin Blanchette, TU Muenchen
5 Refute examples adapted to Nitpick.
6 *)
8 section {* Refute Examples Adapted to Nitpick *}
10 theory Refute_Nits
11 imports Main
12 begin
14 nitpick_params [verbose, card = 1-6, max_potential = 0,
15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
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::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::'a\<Rightarrow>'b) = g"
100 nitpick [expect = genuine]
101 oops
103 lemma "(f::('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::('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 definition "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
248 "trans P \<equiv> (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
250 definition
251 "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
252 "subset P Q \<equiv> (ALL x y. P x y \<longrightarrow> Q x y)"
254 definition
255 "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
256 "trans_closure P Q \<equiv> (subset Q P) \<and> (trans P) \<and> (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
258 lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
259 nitpick [expect = genuine]
260 oops
262 text {* ``The union of transitive closures is equal to the transitive closure of unions.'' *}
264 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)
265  \<longrightarrow> trans_closure TP P
266  \<longrightarrow> trans_closure TR R
267  \<longrightarrow> (T x y = (TP x y \<or> TR x y))"
268 nitpick [expect = genuine]
269 oops
271 text {* ``Every surjective function is invertible.'' *}
273 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
274 nitpick [expect = genuine]
275 oops
277 text {* ``Every invertible function is surjective.'' *}
279 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
280 nitpick [expect = genuine]
281 oops
283 text {* ``Every point is a fixed point of some function.'' *}
285 lemma "\<exists>f. f x = x"
286 nitpick [card = 1-7, expect = none]
287 apply (rule_tac x = "\<lambda>x. x" in exI)
288 apply simp
289 done
291 text {* Axiom of Choice: first an incorrect version *}
293 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
294 nitpick [expect = genuine]
295 oops
297 text {* And now two correct ones *}
299 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
300 nitpick [card = 1-4, expect = none]
302 done
304 lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
305 nitpick [card = 1-3, expect = none]
306 apply auto
307  apply (simp add: ex1_implies_ex choice)
308 apply (fast intro: ext)
309 done
311 subsubsection {* Metalogic *}
313 lemma "\<And>x. P x"
314 nitpick [expect = genuine]
315 oops
317 lemma "f x \<equiv> g x"
318 nitpick [expect = genuine]
319 oops
321 lemma "P \<Longrightarrow> Q"
322 nitpick [expect = genuine]
323 oops
325 lemma "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"
326 nitpick [expect = genuine]
327 oops
329 lemma "(x \<equiv> Pure.all) \<Longrightarrow> False"
330 nitpick [expect = genuine]
331 oops
333 lemma "(x \<equiv> (op \<equiv>)) \<Longrightarrow> False"
334 nitpick [expect = genuine]
335 oops
337 lemma "(x \<equiv> (op \<Longrightarrow>)) \<Longrightarrow> False"
338 nitpick [expect = genuine]
339 oops
341 subsubsection {* Schematic Variables *}
343 schematic_goal "?P"
344 nitpick [expect = none]
345 apply auto
346 done
348 schematic_goal "x = ?y"
349 nitpick [expect = none]
350 apply auto
351 done
353 subsubsection {* Abstractions *}
355 lemma "(\<lambda>x. x) = (\<lambda>x. y)"
356 nitpick [expect = genuine]
357 oops
359 lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
360 nitpick [expect = genuine]
361 oops
363 lemma "(\<lambda>x. x) = (\<lambda>y. y)"
364 nitpick [expect = none]
365 apply simp
366 done
368 subsubsection {* Sets *}
370 lemma "P (A::'a set)"
371 nitpick [expect = genuine]
372 oops
374 lemma "P (A::'a set set)"
375 nitpick [expect = genuine]
376 oops
378 lemma "{x. P x} = {y. P y}"
379 nitpick [expect = none]
380 apply simp
381 done
383 lemma "x \<in> {x. P x}"
384 nitpick [expect = genuine]
385 oops
387 lemma "P (op \<in>)"
388 nitpick [expect = genuine]
389 oops
391 lemma "P (op \<in> x)"
392 nitpick [expect = genuine]
393 oops
395 lemma "P Collect"
396 nitpick [expect = genuine]
397 oops
399 lemma "A Un B = A Int B"
400 nitpick [expect = genuine]
401 oops
403 lemma "(A Int B) Un C = (A Un C) Int B"
404 nitpick [expect = genuine]
405 oops
407 lemma "Ball A P \<longrightarrow> Bex A P"
408 nitpick [expect = genuine]
409 oops
411 subsubsection {* @{const undefined} *}
413 lemma "undefined"
414 nitpick [expect = genuine]
415 oops
417 lemma "P undefined"
418 nitpick [expect = genuine]
419 oops
421 lemma "undefined x"
422 nitpick [expect = genuine]
423 oops
425 lemma "undefined undefined"
426 nitpick [expect = genuine]
427 oops
429 subsubsection {* @{const The} *}
431 lemma "The P"
432 nitpick [expect = genuine]
433 oops
435 lemma "P The"
436 nitpick [expect = genuine]
437 oops
439 lemma "P (The P)"
440 nitpick [expect = genuine]
441 oops
443 lemma "(THE x. x=y) = z"
444 nitpick [expect = genuine]
445 oops
447 lemma "Ex P \<longrightarrow> P (The P)"
448 nitpick [expect = genuine]
449 oops
451 subsubsection {* @{const Eps} *}
453 lemma "Eps P"
454 nitpick [expect = genuine]
455 oops
457 lemma "P Eps"
458 nitpick [expect = genuine]
459 oops
461 lemma "P (Eps P)"
462 nitpick [expect = genuine]
463 oops
465 lemma "(SOME x. x=y) = z"
466 nitpick [expect = genuine]
467 oops
469 lemma "Ex P \<longrightarrow> P (Eps P)"
470 nitpick [expect = none]
471 apply (auto simp add: someI)
472 done
474 subsubsection {* Operations on Natural Numbers *}
476 lemma "(x::nat) + y = 0"
477 nitpick [expect = genuine]
478 oops
480 lemma "(x::nat) = x + x"
481 nitpick [expect = genuine]
482 oops
484 lemma "(x::nat) - y + y = x"
485 nitpick [expect = genuine]
486 oops
488 lemma "(x::nat) = x * x"
489 nitpick [expect = genuine]
490 oops
492 lemma "(x::nat) < x + y"
493 nitpick [card = 1, expect = genuine]
494 oops
496 text {* \<times> *}
498 lemma "P (x::'a\<times>'b)"
499 nitpick [expect = genuine]
500 oops
502 lemma "\<forall>x::'a\<times>'b. P x"
503 nitpick [expect = genuine]
504 oops
506 lemma "P (x, y)"
507 nitpick [expect = genuine]
508 oops
510 lemma "P (fst x)"
511 nitpick [expect = genuine]
512 oops
514 lemma "P (snd x)"
515 nitpick [expect = genuine]
516 oops
518 lemma "P Pair"
519 nitpick [expect = genuine]
520 oops
522 lemma "P (case x of Pair a b \<Rightarrow> f a b)"
523 nitpick [expect = genuine]
524 oops
526 subsubsection {* Subtypes (typedef), typedecl *}
528 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
530 definition "myTdef = insert (undefined::'a) (undefined::'a set)"
532 typedef 'a myTdef = "myTdef :: 'a set"
533 unfolding myTdef_def by auto
535 lemma "(x::'a myTdef) = y"
536 nitpick [expect = genuine]
537 oops
539 typedecl myTdecl
541 definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
543 typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
544 unfolding T_bij_def by auto
546 lemma "P (f::(myTdecl myTdef) T_bij)"
547 nitpick [expect = genuine]
548 oops
550 subsubsection {* Inductive Datatypes *}
552 text {* unit *}
554 lemma "P (x::unit)"
555 nitpick [expect = genuine]
556 oops
558 lemma "\<forall>x::unit. P x"
559 nitpick [expect = genuine]
560 oops
562 lemma "P ()"
563 nitpick [expect = genuine]
564 oops
566 lemma "P (case x of () \<Rightarrow> u)"
567 nitpick [expect = genuine]
568 oops
570 text {* option *}
572 lemma "P (x::'a option)"
573 nitpick [expect = genuine]
574 oops
576 lemma "\<forall>x::'a option. P x"
577 nitpick [expect = genuine]
578 oops
580 lemma "P None"
581 nitpick [expect = genuine]
582 oops
584 lemma "P (Some x)"
585 nitpick [expect = genuine]
586 oops
588 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
589 nitpick [expect = genuine]
590 oops
592 text {* + *}
594 lemma "P (x::'a+'b)"
595 nitpick [expect = genuine]
596 oops
598 lemma "\<forall>x::'a+'b. P x"
599 nitpick [expect = genuine]
600 oops
602 lemma "P (Inl x)"
603 nitpick [expect = genuine]
604 oops
606 lemma "P (Inr x)"
607 nitpick [expect = genuine]
608 oops
610 lemma "P Inl"
611 nitpick [expect = genuine]
612 oops
614 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
615 nitpick [expect = genuine]
616 oops
618 text {* Non-recursive datatypes *}
620 datatype T1 = A | B
622 lemma "P (x::T1)"
623 nitpick [expect = genuine]
624 oops
626 lemma "\<forall>x::T1. P x"
627 nitpick [expect = genuine]
628 oops
630 lemma "P A"
631 nitpick [expect = genuine]
632 oops
634 lemma "P B"
635 nitpick [expect = genuine]
636 oops
638 lemma "rec_T1 a b A = a"
639 nitpick [expect = none]
640 apply simp
641 done
643 lemma "rec_T1 a b B = b"
644 nitpick [expect = none]
645 apply simp
646 done
648 lemma "P (rec_T1 a b x)"
649 nitpick [expect = genuine]
650 oops
652 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
653 nitpick [expect = genuine]
654 oops
656 datatype 'a T2 = C T1 | D 'a
658 lemma "P (x::'a T2)"
659 nitpick [expect = genuine]
660 oops
662 lemma "\<forall>x::'a T2. P x"
663 nitpick [expect = genuine]
664 oops
666 lemma "P D"
667 nitpick [expect = genuine]
668 oops
670 lemma "rec_T2 c d (C x) = c x"
671 nitpick [expect = none]
672 apply simp
673 done
675 lemma "rec_T2 c d (D x) = d x"
676 nitpick [expect = none]
677 apply simp
678 done
680 lemma "P (rec_T2 c d x)"
681 nitpick [expect = genuine]
682 oops
684 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
685 nitpick [expect = genuine]
686 oops
688 datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
690 lemma "P (x::('a, 'b) T3)"
691 nitpick [expect = genuine]
692 oops
694 lemma "\<forall>x::('a, 'b) T3. P x"
695 nitpick [expect = genuine]
696 oops
698 lemma "P E"
699 nitpick [expect = genuine]
700 oops
702 lemma "rec_T3 e (E x) = e x"
703 nitpick [card = 1-4, expect = none]
704 apply simp
705 done
707 lemma "P (rec_T3 e x)"
708 nitpick [expect = genuine]
709 oops
711 lemma "P (case x of E f \<Rightarrow> e f)"
712 nitpick [expect = genuine]
713 oops
715 text {* Recursive datatypes *}
717 text {* nat *}
719 lemma "P (x::nat)"
720 nitpick [expect = genuine]
721 oops
723 lemma "\<forall>x::nat. P x"
724 nitpick [expect = genuine]
725 oops
727 lemma "P (Suc 0)"
728 nitpick [expect = genuine]
729 oops
731 lemma "P Suc"
732 nitpick [card = 1-7, expect = none]
733 oops
735 lemma "rec_nat zero suc 0 = zero"
736 nitpick [expect = none]
737 apply simp
738 done
740 lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
741 nitpick [expect = none]
742 apply simp
743 done
745 lemma "P (rec_nat zero suc x)"
746 nitpick [expect = genuine]
747 oops
749 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
750 nitpick [expect = genuine]
751 oops
753 text {* 'a list *}
755 lemma "P (xs::'a list)"
756 nitpick [expect = genuine]
757 oops
759 lemma "\<forall>xs::'a list. P xs"
760 nitpick [expect = genuine]
761 oops
763 lemma "P [x, y]"
764 nitpick [expect = genuine]
765 oops
767 lemma "rec_list nil cons [] = nil"
768 nitpick [card = 1-5, expect = none]
769 apply simp
770 done
772 lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
773 nitpick [card = 1-5, expect = none]
774 apply simp
775 done
777 lemma "P (rec_list nil cons xs)"
778 nitpick [expect = genuine]
779 oops
781 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
782 nitpick [expect = genuine]
783 oops
785 lemma "(xs::'a list) = ys"
786 nitpick [expect = genuine]
787 oops
789 lemma "a # xs = b # xs"
790 nitpick [expect = genuine]
791 oops
793 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
795 lemma "P (x::BitList)"
796 nitpick [expect = genuine]
797 oops
799 lemma "\<forall>x::BitList. P x"
800 nitpick [expect = genuine]
801 oops
803 lemma "P (Bit0 (Bit1 BitListNil))"
804 nitpick [expect = genuine]
805 oops
807 lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
808 nitpick [expect = none]
809 apply simp
810 done
812 lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
813 nitpick [expect = none]
814 apply simp
815 done
817 lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
818 nitpick [expect = none]
819 apply simp
820 done
822 lemma "P (rec_BitList nil bit0 bit1 x)"
823 nitpick [expect = genuine]
824 oops
826 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
828 lemma "P (x::'a BinTree)"
829 nitpick [expect = genuine]
830 oops
832 lemma "\<forall>x::'a BinTree. P x"
833 nitpick [expect = genuine]
834 oops
836 lemma "P (Node (Leaf x) (Leaf y))"
837 nitpick [expect = genuine]
838 oops
840 lemma "rec_BinTree l n (Leaf x) = l x"
841 nitpick [expect = none]
842 apply simp
843 done
845 lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
846 nitpick [card = 1-5, expect = none]
847 apply simp
848 done
850 lemma "P (rec_BinTree l n x)"
851 nitpick [expect = genuine]
852 oops
854 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
855 nitpick [expect = genuine]
856 oops
858 text {* Mutually recursive datatypes *}
860 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
861  and 'a bexp = Equal "'a aexp" "'a aexp"
863 lemma "P (x::'a aexp)"
864 nitpick [expect = genuine]
865 oops
867 lemma "\<forall>x::'a aexp. P x"
868 nitpick [expect = genuine]
869 oops
871 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
872 nitpick [expect = genuine]
873 oops
875 lemma "P (x::'a bexp)"
876 nitpick [expect = genuine]
877 oops
879 lemma "\<forall>x::'a bexp. P x"
880 nitpick [expect = genuine]
881 oops
883 lemma "rec_aexp number ite equal (Number x) = number x"
884 nitpick [card = 1-3, expect = none]
885 apply simp
886 done
888 lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
889 nitpick [card = 1-3, expect = none]
890 apply simp
891 done
893 lemma "P (rec_aexp number ite equal x)"
894 nitpick [expect = genuine]
895 oops
897 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
898 nitpick [expect = genuine]
899 oops
901 lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
902 nitpick [card = 1-3, expect = none]
903 apply simp
904 done
906 lemma "P (rec_bexp number ite equal x)"
907 nitpick [expect = genuine]
908 oops
910 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
911 nitpick [expect = genuine]
912 oops
914 datatype X = A | B X | C Y and Y = D X | E Y | F
916 lemma "P (x::X)"
917 nitpick [expect = genuine]
918 oops
920 lemma "P (y::Y)"
921 nitpick [expect = genuine]
922 oops
924 lemma "P (B (B A))"
925 nitpick [expect = genuine]
926 oops
928 lemma "P (B (C F))"
929 nitpick [expect = genuine]
930 oops
932 lemma "P (C (D A))"
933 nitpick [expect = genuine]
934 oops
936 lemma "P (C (E F))"
937 nitpick [expect = genuine]
938 oops
940 lemma "P (D (B A))"
941 nitpick [expect = genuine]
942 oops
944 lemma "P (D (C F))"
945 nitpick [expect = genuine]
946 oops
948 lemma "P (E (D A))"
949 nitpick [expect = genuine]
950 oops
952 lemma "P (E (E F))"
953 nitpick [expect = genuine]
954 oops
956 lemma "P (C (D (C F)))"
957 nitpick [expect = genuine]
958 oops
960 lemma "rec_X a b c d e f A = a"
961 nitpick [card = 1-5, expect = none]
962 apply simp
963 done
965 lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
966 nitpick [card = 1-5, expect = none]
967 apply simp
968 done
970 lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
971 nitpick [card = 1-5, expect = none]
972 apply simp
973 done
975 lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
976 nitpick [card = 1-5, expect = none]
977 apply simp
978 done
980 lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
981 nitpick [card = 1-5, expect = none]
982 apply simp
983 done
985 lemma "rec_Y a b c d e f F = f"
986 nitpick [card = 1-5, expect = none]
987 apply simp
988 done
990 lemma "P (rec_X a b c d e f x)"
991 nitpick [expect = genuine]
992 oops
994 lemma "P (rec_Y a b c d e f y)"
995 nitpick [expect = genuine]
996 oops
998 text {* Other datatype examples *}
1000 text {* Indirect recursion is implemented via mutual recursion. *}
1002 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
1004 lemma "P (x::XOpt)"
1005 nitpick [expect = genuine]
1006 oops
1008 lemma "P (CX None)"
1009 nitpick [expect = genuine]
1010 oops
1012 lemma "P (CX (Some (CX None)))"
1013 nitpick [expect = genuine]
1014 oops
1016 lemma "P (rec_X cx dx n1 s1 n2 s2 x)"
1017 nitpick [expect = genuine]
1018 oops
1020 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
1022 lemma "P (x::'a YOpt)"
1023 nitpick [expect = genuine]
1024 oops
1026 lemma "P (CY None)"
1027 nitpick [expect = genuine]
1028 oops
1030 lemma "P (CY (Some (\<lambda>a. CY None)))"
1031 nitpick [expect = genuine]
1032 oops
1034 datatype Trie = TR "Trie list"
1036 lemma "P (x::Trie)"
1037 nitpick [expect = genuine]
1038 oops
1040 lemma "\<forall>x::Trie. P x"
1041 nitpick [expect = genuine]
1042 oops
1044 lemma "P (TR [TR []])"
1045 nitpick [expect = genuine]
1046 oops
1048 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
1050 lemma "P (x::InfTree)"
1051 nitpick [expect = genuine]
1052 oops
1054 lemma "\<forall>x::InfTree. P x"
1055 nitpick [expect = genuine]
1056 oops
1058 lemma "P (Node (\<lambda>n. Leaf))"
1059 nitpick [expect = genuine]
1060 oops
1062 lemma "rec_InfTree leaf node Leaf = leaf"
1063 nitpick [card = 1-3, expect = none]
1064 apply simp
1065 done
1067 lemma "rec_InfTree leaf node (Node g) = node ((\<lambda>InfTree. (InfTree, rec_InfTree leaf node InfTree)) \<circ> g)"
1068 nitpick [card = 1-3, expect = none]
1069 apply simp
1070 done
1072 lemma "P (rec_InfTree leaf node x)"
1073 nitpick [expect = genuine]
1074 oops
1076 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
1078 lemma "P (x::'a lambda)"
1079 nitpick [expect = genuine]
1080 oops
1082 lemma "\<forall>x::'a lambda. P x"
1083 nitpick [expect = genuine]
1084 oops
1086 lemma "P (Lam (\<lambda>a. Var a))"
1087 nitpick [card = 1-5, expect = none]
1088 nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
1089 oops
1091 lemma "rec_lambda var app lam (Var x) = var x"
1092 nitpick [card = 1-3, expect = none]
1093 apply simp
1094 done
1096 lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
1097 nitpick [card = 1-3, expect = none]
1098 apply simp
1099 done
1101 lemma "rec_lambda var app lam (Lam x) = lam ((\<lambda>lambda. (lambda, rec_lambda var app lam lambda)) \<circ> x)"
1102 nitpick [card = 1-3, expect = none]
1103 apply simp
1104 done
1106 lemma "P (rec_lambda v a l x)"
1107 nitpick [expect = genuine]
1108 oops
1110 text {* Taken from "Inductive datatypes in HOL", p. 8: *}
1112 datatype (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
1113 datatype 'c U = E "('c, 'c U) T"
1115 lemma "P (x::'c U)"
1116 nitpick [expect = genuine]
1117 oops
1119 lemma "\<forall>x::'c U. P x"
1120 nitpick [expect = genuine]
1121 oops
1123 lemma "P (E (C (\<lambda>a. True)))"
1124 nitpick [expect = genuine]
1125 oops
1127 subsubsection {* Records *}
1129 record ('a, 'b) point =
1130   xpos :: 'a
1131   ypos :: 'b
1133 lemma "(x::('a, 'b) point) = y"
1134 nitpick [expect = genuine]
1135 oops
1137 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
1138   ext :: 'c
1140 lemma "(x::('a, 'b, 'c) extpoint) = y"
1141 nitpick [expect = genuine]
1142 oops
1144 subsubsection {* Inductively Defined Sets *}
1146 inductive_set undefinedSet :: "'a set" where
1147 "undefined \<in> undefinedSet"
1149 lemma "x \<in> undefinedSet"
1150 nitpick [expect = genuine]
1151 oops
1153 inductive_set evenCard :: "'a set set"
1154 where
1155 "{} \<in> evenCard" |
1156 "\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
1158 lemma "S \<in> evenCard"
1159 nitpick [expect = genuine]
1160 oops
1162 inductive_set
1163 even :: "nat set"
1164 and odd :: "nat set"
1165 where
1166 "0 \<in> even" |
1167 "n \<in> even \<Longrightarrow> Suc n \<in> odd" |
1168 "n \<in> odd \<Longrightarrow> Suc n \<in> even"
1170 lemma "n \<in> odd"
1171 nitpick [expect = genuine]
1172 oops
1174 consts f :: "'a \<Rightarrow> 'a"
1176 inductive_set a_even :: "'a set" and a_odd :: "'a set" where
1177 "undefined \<in> a_even" |
1178 "x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
1179 "x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
1181 lemma "x \<in> a_odd"
1182 nitpick [expect = genuine]
1183 oops
1185 subsubsection {* Examples Involving Special Functions *}
1187 lemma "card x = 0"
1188 nitpick [expect = genuine]
1189 oops
1191 lemma "finite x"
1192 nitpick [expect = none]
1193 oops
1195 lemma "xs @ [] = ys @ []"
1196 nitpick [expect = genuine]
1197 oops
1199 lemma "xs @ ys = ys @ xs"
1200 nitpick [expect = genuine]
1201 oops
1203 lemma "f (lfp f) = lfp f"
1204 nitpick [card = 2, expect = genuine]
1205 oops
1207 lemma "f (gfp f) = gfp f"
1208 nitpick [card = 2, expect = genuine]
1209 oops
1211 lemma "lfp f = gfp f"
1212 nitpick [card = 2, expect = genuine]
1213 oops
1217 text {* A type class without axioms: *}
1219 class classA
1221 lemma "P (x::'a::classA)"
1222 nitpick [expect = genuine]
1223 oops
1225 text {* An axiom with a type variable (denoting types which have at least two elements): *}
1227 class classC =
1228   assumes classC_ax: "\<exists>x y. x \<noteq> y"
1230 lemma "P (x::'a::classC)"
1231 nitpick [expect = genuine]
1232 oops
1234 lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
1235 nitpick [expect = none]
1236 sorry
1238 text {* A type class for which a constant is defined: *}
1240 class classD =
1241   fixes classD_const :: "'a \<Rightarrow> 'a"
1242   assumes classD_ax: "classD_const (classD_const x) = classD_const x"
1244 lemma "P (x::'a::classD)"
1245 nitpick [expect = genuine]
1246 oops
1248 text {* A type class with multiple superclasses: *}
1250 class classE = classC + classD
1252 lemma "P (x::'a::classE)"
1253 nitpick [expect = genuine]
1254 oops
1256 text {* OFCLASS: *}
1258 lemma "OFCLASS('a::type, type_class)"
1259 nitpick [expect = none]
1260 apply intro_classes
1261 done
1263 lemma "OFCLASS('a::classC, type_class)"
1264 nitpick [expect = none]
1265 apply intro_classes
1266 done
1268 lemma "OFCLASS('a::type, classC_class)"
1269 nitpick [expect = genuine]
1270 oops
1274 consts inverse :: "'a \<Rightarrow> 'a"
1277 begin
1278   definition "inverse (b::bool) \<equiv> \<not> b"
1279 end
1282 begin
1283   definition "inverse (S::'a set) \<equiv> -S"
1284 end
1286 overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
1287 begin
1288   definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
1289 end
1291 lemma "inverse b"
1292 nitpick [expect = genuine]
1293 oops
1295 lemma "P (inverse (S::'a set))"
1296 nitpick [expect = genuine]
1297 oops
1299 lemma "P (inverse (p::'a\<times>'b))"
1300 nitpick [expect = genuine]
1301 oops
1303 end