804 |
804 |
805 lemma "P (rec_BitList nil bit0 bit1 x)" |
805 lemma "P (rec_BitList nil bit0 bit1 x)" |
806 refute [expect = potential] |
806 refute [expect = potential] |
807 oops |
807 oops |
808 |
808 |
809 datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree" |
|
810 |
|
811 lemma "P (x::'a BinTree)" |
|
812 refute [expect = potential] |
|
813 oops |
|
814 |
|
815 lemma "\<forall>x::'a BinTree. P x" |
|
816 refute [expect = potential] |
|
817 oops |
|
818 |
|
819 lemma "P (Node (Leaf x) (Leaf y))" |
|
820 refute [expect = potential] |
|
821 oops |
|
822 |
|
823 lemma "rec_BinTree l n (Leaf x) = l x" |
|
824 refute [maxsize = 1, expect = none] |
|
825 (* The "maxsize = 1" tests are a bit pointless: for some formulae |
|
826 below, refute will find no countermodel simply because this |
|
827 size makes involved terms undefined. Unfortunately, any |
|
828 larger size already takes too long. *) |
|
829 by simp |
|
830 |
|
831 lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)" |
|
832 refute [maxsize = 1, expect = none] |
|
833 by simp |
|
834 |
|
835 lemma "P (rec_BinTree l n x)" |
|
836 refute [expect = potential] |
|
837 oops |
|
838 |
|
839 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)" |
|
840 refute [expect = potential] |
|
841 oops |
|
842 |
|
843 text {* Mutually recursive datatypes *} |
|
844 |
|
845 datatype_new |
|
846 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" and |
|
847 'a bexp = Equal "'a aexp" "'a aexp" |
|
848 |
|
849 lemma "P (x::'a aexp)" |
|
850 refute [expect = potential] |
|
851 oops |
|
852 |
|
853 lemma "\<forall>x::'a aexp. P x" |
|
854 refute [expect = potential] |
|
855 oops |
|
856 |
|
857 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))" |
|
858 refute [expect = potential] |
|
859 oops |
|
860 |
|
861 lemma "P (x::'a bexp)" |
|
862 refute [expect = potential] |
|
863 oops |
|
864 |
|
865 lemma "\<forall>x::'a bexp. P x" |
|
866 refute [expect = potential] |
|
867 oops |
|
868 |
|
869 lemma "rec_aexp number ite equal (Number x) = number x" |
|
870 refute [maxsize = 1, expect = none] |
|
871 by simp |
|
872 |
|
873 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)" |
|
874 refute [maxsize = 1, expect = none] |
|
875 by simp |
|
876 |
|
877 lemma "P (rec_aexp number ite equal x)" |
|
878 refute [expect = potential] |
|
879 oops |
|
880 |
|
881 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)" |
|
882 refute [expect = potential] |
|
883 oops |
|
884 |
|
885 lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)" |
|
886 refute [maxsize = 1, expect = none] |
|
887 by simp |
|
888 |
|
889 lemma "P (rec_bexp number ite equal x)" |
|
890 refute [expect = potential] |
|
891 oops |
|
892 |
|
893 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)" |
|
894 refute [expect = potential] |
|
895 oops |
|
896 |
|
897 datatype_new |
|
898 X = A | B X | C Y and |
|
899 Y = D X | E Y | F |
|
900 |
|
901 lemma "P (x::X)" |
|
902 refute [expect = potential] |
|
903 oops |
|
904 |
|
905 lemma "P (y::Y)" |
|
906 refute [expect = potential] |
|
907 oops |
|
908 |
|
909 lemma "P (B (B A))" |
|
910 refute [expect = potential] |
|
911 oops |
|
912 |
|
913 lemma "P (B (C F))" |
|
914 refute [expect = potential] |
|
915 oops |
|
916 |
|
917 lemma "P (C (D A))" |
|
918 refute [expect = potential] |
|
919 oops |
|
920 |
|
921 lemma "P (C (E F))" |
|
922 refute [expect = potential] |
|
923 oops |
|
924 |
|
925 lemma "P (D (B A))" |
|
926 refute [expect = potential] |
|
927 oops |
|
928 |
|
929 lemma "P (D (C F))" |
|
930 refute [expect = potential] |
|
931 oops |
|
932 |
|
933 lemma "P (E (D A))" |
|
934 refute [expect = potential] |
|
935 oops |
|
936 |
|
937 lemma "P (E (E F))" |
|
938 refute [expect = potential] |
|
939 oops |
|
940 |
|
941 lemma "P (C (D (C F)))" |
|
942 refute [expect = potential] |
|
943 oops |
|
944 |
|
945 lemma "rec_X a b c d e f A = a" |
|
946 refute [maxsize = 2, expect = none] |
|
947 by simp |
|
948 |
|
949 lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)" |
|
950 refute [maxsize = 1, expect = none] |
|
951 by simp |
|
952 |
|
953 lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)" |
|
954 refute [maxsize = 1, expect = none] |
|
955 by simp |
|
956 |
|
957 lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)" |
|
958 refute [maxsize = 1, expect = none] |
|
959 by simp |
|
960 |
|
961 lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)" |
|
962 refute [maxsize = 1, expect = none] |
|
963 by simp |
|
964 |
|
965 lemma "rec_Y a b c d e f F = f" |
|
966 refute [maxsize = 2, expect = none] |
|
967 by simp |
|
968 |
|
969 lemma "P (rec_X a b c d e f x)" |
|
970 refute [expect = potential] |
|
971 oops |
|
972 |
|
973 lemma "P (rec_Y a b c d e f y)" |
|
974 refute [expect = potential] |
|
975 oops |
|
976 |
|
977 text {* Other datatype examples *} |
|
978 |
|
979 text {* Indirect recursion is implemented via mutual recursion. *} |
|
980 |
|
981 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option" |
|
982 |
|
983 lemma "P (x::XOpt)" |
|
984 refute [expect = potential] |
|
985 oops |
|
986 |
|
987 lemma "P (CX None)" |
|
988 refute [expect = potential] |
|
989 oops |
|
990 |
|
991 lemma "P (CX (Some (CX None)))" |
|
992 refute [expect = potential] |
|
993 oops |
|
994 |
|
995 lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" |
|
996 refute [maxsize = 1, expect = none] |
|
997 by simp |
|
998 |
|
999 lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))" |
|
1000 refute [maxsize = 1, expect = none] |
|
1001 by simp |
|
1002 |
|
1003 lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1" |
|
1004 refute [maxsize = 2, expect = none] |
|
1005 by simp |
|
1006 |
|
1007 lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" |
|
1008 refute [maxsize = 1, expect = none] |
|
1009 by simp |
|
1010 |
|
1011 lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2" |
|
1012 refute [maxsize = 2, expect = none] |
|
1013 by simp |
|
1014 |
|
1015 lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" |
|
1016 refute [maxsize = 1, expect = none] |
|
1017 by simp |
|
1018 |
|
1019 lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)" |
|
1020 refute [expect = potential] |
|
1021 oops |
|
1022 |
|
1023 lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)" |
|
1024 refute [expect = potential] |
|
1025 oops |
|
1026 |
|
1027 lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)" |
|
1028 refute [expect = potential] |
|
1029 oops |
|
1030 |
|
1031 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option" |
|
1032 |
|
1033 lemma "P (x::'a YOpt)" |
|
1034 refute [expect = potential] |
|
1035 oops |
|
1036 |
|
1037 lemma "P (CY None)" |
|
1038 refute [expect = potential] |
|
1039 oops |
|
1040 |
|
1041 lemma "P (CY (Some (\<lambda>a. CY None)))" |
|
1042 refute [expect = potential] |
|
1043 oops |
|
1044 |
|
1045 lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)" |
|
1046 refute [maxsize = 1, expect = none] |
|
1047 by simp |
|
1048 |
|
1049 lemma "rec_YOpt_2 cy n s None = n" |
|
1050 refute [maxsize = 2, expect = none] |
|
1051 by simp |
|
1052 |
|
1053 lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))" |
|
1054 refute [maxsize = 1, expect = none] |
|
1055 by simp |
|
1056 |
|
1057 lemma "P (rec_YOpt_1 cy n s x)" |
|
1058 refute [expect = potential] |
|
1059 oops |
|
1060 |
|
1061 lemma "P (rec_YOpt_2 cy n s x)" |
|
1062 refute [expect = potential] |
|
1063 oops |
|
1064 |
|
1065 datatype_new Trie = TR "Trie list" |
|
1066 datatype_compat Trie |
|
1067 |
|
1068 abbreviation "rec_Trie_1 \<equiv> compat_Trie.rec_n2m_Trie" |
|
1069 abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.rec_n2m_Trie_list" |
|
1070 |
|
1071 lemma "P (x::Trie)" |
|
1072 refute [expect = potential] |
|
1073 oops |
|
1074 |
|
1075 lemma "\<forall>x::Trie. P x" |
|
1076 refute [expect = potential] |
|
1077 oops |
|
1078 |
|
1079 lemma "P (TR [TR []])" |
|
1080 refute [expect = potential] |
|
1081 oops |
|
1082 |
|
1083 lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)" |
|
1084 refute [maxsize = 1, expect = none] |
|
1085 by simp |
|
1086 |
|
1087 lemma "rec_Trie_2 tr nil cons [] = nil" |
|
1088 refute [maxsize = 3, expect = none] |
|
1089 by simp |
|
1090 |
|
1091 lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)" |
|
1092 refute [maxsize = 1, expect = none] |
|
1093 by simp |
|
1094 |
|
1095 lemma "P (rec_Trie_1 tr nil cons x)" |
|
1096 refute [expect = potential] |
|
1097 oops |
|
1098 |
|
1099 lemma "P (rec_Trie_2 tr nil cons x)" |
|
1100 refute [expect = potential] |
|
1101 oops |
|
1102 |
|
1103 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree" |
|
1104 |
|
1105 lemma "P (x::InfTree)" |
|
1106 refute [expect = potential] |
|
1107 oops |
|
1108 |
|
1109 lemma "\<forall>x::InfTree. P x" |
|
1110 refute [expect = potential] |
|
1111 oops |
|
1112 |
|
1113 lemma "P (Node (\<lambda>n. Leaf))" |
|
1114 refute [expect = potential] |
|
1115 oops |
|
1116 |
|
1117 lemma "rec_InfTree leaf node Leaf = leaf" |
|
1118 refute [maxsize = 2, expect = none] |
|
1119 by simp |
|
1120 |
|
1121 lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))" |
|
1122 refute [maxsize = 1, expect = none] |
|
1123 by simp |
|
1124 |
|
1125 lemma "P (rec_InfTree leaf node x)" |
|
1126 refute [expect = potential] |
|
1127 oops |
|
1128 |
|
1129 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda" |
|
1130 |
|
1131 lemma "P (x::'a lambda)" |
|
1132 refute [expect = potential] |
|
1133 oops |
|
1134 |
|
1135 lemma "\<forall>x::'a lambda. P x" |
|
1136 refute [expect = potential] |
|
1137 oops |
|
1138 |
|
1139 lemma "P (Lam (\<lambda>a. Var a))" |
|
1140 refute [expect = potential] |
|
1141 oops |
|
1142 |
|
1143 lemma "rec_lambda var app lam (Var x) = var x" |
|
1144 refute [maxsize = 1, expect = none] |
|
1145 by simp |
|
1146 |
|
1147 lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)" |
|
1148 refute [maxsize = 1, expect = none] |
|
1149 by simp |
|
1150 |
|
1151 lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))" |
|
1152 refute [maxsize = 1, expect = none] |
|
1153 by simp |
|
1154 |
|
1155 lemma "P (rec_lambda v a l x)" |
|
1156 refute [expect = potential] |
|
1157 oops |
|
1158 |
|
1159 text {* Taken from "Inductive datatypes in HOL", p.8: *} |
|
1160 |
|
1161 datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list" |
|
1162 datatype 'c U = E "('c, 'c U) T" |
|
1163 |
|
1164 lemma "P (x::'c U)" |
|
1165 refute [expect = potential] |
|
1166 oops |
|
1167 |
|
1168 lemma "\<forall>x::'c U. P x" |
|
1169 refute [expect = potential] |
|
1170 oops |
|
1171 |
|
1172 lemma "P (E (C (\<lambda>a. True)))" |
|
1173 refute [expect = potential] |
|
1174 oops |
|
1175 |
|
1176 lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)" |
|
1177 refute [maxsize = 1, expect = none] |
|
1178 by simp |
|
1179 |
|
1180 lemma "rec_U_2 e c d nil cons (C x) = c x" |
|
1181 refute [maxsize = 1, expect = none] |
|
1182 by simp |
|
1183 |
|
1184 lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)" |
|
1185 refute [maxsize = 1, expect = none] |
|
1186 by simp |
|
1187 |
|
1188 lemma "rec_U_3 e c d nil cons [] = nil" |
|
1189 refute [maxsize = 2, expect = none] |
|
1190 by simp |
|
1191 |
|
1192 lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)" |
|
1193 refute [maxsize = 1, expect = none] |
|
1194 by simp |
|
1195 |
|
1196 lemma "P (rec_U_1 e c d nil cons x)" |
|
1197 refute [expect = potential] |
|
1198 oops |
|
1199 |
|
1200 lemma "P (rec_U_2 e c d nil cons x)" |
|
1201 refute [expect = potential] |
|
1202 oops |
|
1203 |
|
1204 lemma "P (rec_U_3 e c d nil cons x)" |
|
1205 refute [expect = potential] |
|
1206 oops |
|
1207 |
|
1208 (*****************************************************************************) |
809 (*****************************************************************************) |
1209 |
810 |
1210 subsubsection {* Examples involving special functions *} |
811 subsubsection {* Examples involving special functions *} |
1211 |
812 |
1212 lemma "card x = 0" |
813 lemma "card x = 0" |