equal
deleted
inserted
replaced
615 nitpick [expect = genuine] |
615 nitpick [expect = genuine] |
616 oops |
616 oops |
617 |
617 |
618 text {* Non-recursive datatypes *} |
618 text {* Non-recursive datatypes *} |
619 |
619 |
620 datatype_new T1 = A | B |
620 datatype T1 = A | B |
621 |
621 |
622 lemma "P (x\<Colon>T1)" |
622 lemma "P (x\<Colon>T1)" |
623 nitpick [expect = genuine] |
623 nitpick [expect = genuine] |
624 oops |
624 oops |
625 |
625 |
651 |
651 |
652 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)" |
652 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)" |
653 nitpick [expect = genuine] |
653 nitpick [expect = genuine] |
654 oops |
654 oops |
655 |
655 |
656 datatype_new 'a T2 = C T1 | D 'a |
656 datatype 'a T2 = C T1 | D 'a |
657 |
657 |
658 lemma "P (x\<Colon>'a T2)" |
658 lemma "P (x\<Colon>'a T2)" |
659 nitpick [expect = genuine] |
659 nitpick [expect = genuine] |
660 oops |
660 oops |
661 |
661 |
683 |
683 |
684 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)" |
684 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)" |
685 nitpick [expect = genuine] |
685 nitpick [expect = genuine] |
686 oops |
686 oops |
687 |
687 |
688 datatype_new ('a, 'b) T3 = E "'a \<Rightarrow> 'b" |
688 datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b" |
689 |
689 |
690 lemma "P (x\<Colon>('a, 'b) T3)" |
690 lemma "P (x\<Colon>('a, 'b) T3)" |
691 nitpick [expect = genuine] |
691 nitpick [expect = genuine] |
692 oops |
692 oops |
693 |
693 |
788 |
788 |
789 lemma "a # xs = b # xs" |
789 lemma "a # xs = b # xs" |
790 nitpick [expect = genuine] |
790 nitpick [expect = genuine] |
791 oops |
791 oops |
792 |
792 |
793 datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList |
793 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList |
794 |
794 |
795 lemma "P (x\<Colon>BitList)" |
795 lemma "P (x\<Colon>BitList)" |
796 nitpick [expect = genuine] |
796 nitpick [expect = genuine] |
797 oops |
797 oops |
798 |
798 |
821 |
821 |
822 lemma "P (rec_BitList nil bit0 bit1 x)" |
822 lemma "P (rec_BitList nil bit0 bit1 x)" |
823 nitpick [expect = genuine] |
823 nitpick [expect = genuine] |
824 oops |
824 oops |
825 |
825 |
826 datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree" |
826 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree" |
827 |
827 |
828 lemma "P (x\<Colon>'a BinTree)" |
828 lemma "P (x\<Colon>'a BinTree)" |
829 nitpick [expect = genuine] |
829 nitpick [expect = genuine] |
830 oops |
830 oops |
831 |
831 |
855 nitpick [expect = genuine] |
855 nitpick [expect = genuine] |
856 oops |
856 oops |
857 |
857 |
858 text {* Mutually recursive datatypes *} |
858 text {* Mutually recursive datatypes *} |
859 |
859 |
860 datatype_new 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" |
860 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" |
861 and 'a bexp = Equal "'a aexp" "'a aexp" |
861 and 'a bexp = Equal "'a aexp" "'a aexp" |
862 |
862 |
863 lemma "P (x\<Colon>'a aexp)" |
863 lemma "P (x\<Colon>'a aexp)" |
864 nitpick [expect = genuine] |
864 nitpick [expect = genuine] |
865 oops |
865 oops |
909 |
909 |
910 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)" |
910 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)" |
911 nitpick [expect = genuine] |
911 nitpick [expect = genuine] |
912 oops |
912 oops |
913 |
913 |
914 datatype_new X = A | B X | C Y and Y = D X | E Y | F |
914 datatype X = A | B X | C Y and Y = D X | E Y | F |
915 |
915 |
916 lemma "P (x\<Colon>X)" |
916 lemma "P (x\<Colon>X)" |
917 nitpick [expect = genuine] |
917 nitpick [expect = genuine] |
918 oops |
918 oops |
919 |
919 |
997 |
997 |
998 text {* Other datatype examples *} |
998 text {* Other datatype examples *} |
999 |
999 |
1000 text {* Indirect recursion is implemented via mutual recursion. *} |
1000 text {* Indirect recursion is implemented via mutual recursion. *} |
1001 |
1001 |
1002 datatype_new XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option" |
1002 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option" |
1003 |
1003 |
1004 lemma "P (x\<Colon>XOpt)" |
1004 lemma "P (x\<Colon>XOpt)" |
1005 nitpick [expect = genuine] |
1005 nitpick [expect = genuine] |
1006 oops |
1006 oops |
1007 |
1007 |
1015 |
1015 |
1016 lemma "P (rec_X cx dx n1 s1 n2 s2 x)" |
1016 lemma "P (rec_X cx dx n1 s1 n2 s2 x)" |
1017 nitpick [expect = genuine] |
1017 nitpick [expect = genuine] |
1018 oops |
1018 oops |
1019 |
1019 |
1020 datatype_new 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option" |
1020 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option" |
1021 |
1021 |
1022 lemma "P (x\<Colon>'a YOpt)" |
1022 lemma "P (x\<Colon>'a YOpt)" |
1023 nitpick [expect = genuine] |
1023 nitpick [expect = genuine] |
1024 oops |
1024 oops |
1025 |
1025 |
1029 |
1029 |
1030 lemma "P (CY (Some (\<lambda>a. CY None)))" |
1030 lemma "P (CY (Some (\<lambda>a. CY None)))" |
1031 nitpick [expect = genuine] |
1031 nitpick [expect = genuine] |
1032 oops |
1032 oops |
1033 |
1033 |
1034 datatype_new Trie = TR "Trie list" |
1034 datatype Trie = TR "Trie list" |
1035 |
1035 |
1036 lemma "P (x\<Colon>Trie)" |
1036 lemma "P (x\<Colon>Trie)" |
1037 nitpick [expect = genuine] |
1037 nitpick [expect = genuine] |
1038 oops |
1038 oops |
1039 |
1039 |
1043 |
1043 |
1044 lemma "P (TR [TR []])" |
1044 lemma "P (TR [TR []])" |
1045 nitpick [expect = genuine] |
1045 nitpick [expect = genuine] |
1046 oops |
1046 oops |
1047 |
1047 |
1048 datatype_new InfTree = Leaf | Node "nat \<Rightarrow> InfTree" |
1048 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree" |
1049 |
1049 |
1050 lemma "P (x\<Colon>InfTree)" |
1050 lemma "P (x\<Colon>InfTree)" |
1051 nitpick [expect = genuine] |
1051 nitpick [expect = genuine] |
1052 oops |
1052 oops |
1053 |
1053 |
1071 |
1071 |
1072 lemma "P (rec_InfTree leaf node x)" |
1072 lemma "P (rec_InfTree leaf node x)" |
1073 nitpick [expect = genuine] |
1073 nitpick [expect = genuine] |
1074 oops |
1074 oops |
1075 |
1075 |
1076 datatype_new 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda" |
1076 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda" |
1077 |
1077 |
1078 lemma "P (x\<Colon>'a lambda)" |
1078 lemma "P (x\<Colon>'a lambda)" |
1079 nitpick [expect = genuine] |
1079 nitpick [expect = genuine] |
1080 oops |
1080 oops |
1081 |
1081 |
1107 nitpick [expect = genuine] |
1107 nitpick [expect = genuine] |
1108 oops |
1108 oops |
1109 |
1109 |
1110 text {* Taken from "Inductive datatypes in HOL", p. 8: *} |
1110 text {* Taken from "Inductive datatypes in HOL", p. 8: *} |
1111 |
1111 |
1112 datatype_new (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list" |
1112 datatype (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list" |
1113 datatype_new 'c U = E "('c, 'c U) T" |
1113 datatype 'c U = E "('c, 'c U) T" |
1114 |
1114 |
1115 lemma "P (x\<Colon>'c U)" |
1115 lemma "P (x\<Colon>'c U)" |
1116 nitpick [expect = genuine] |
1116 nitpick [expect = genuine] |
1117 oops |
1117 oops |
1118 |
1118 |