1049 |
1049 |
1050 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)" |
1050 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)" |
1051 nitpick [expect = none] |
1051 nitpick [expect = none] |
1052 sorry |
1052 sorry |
1053 |
1053 |
|
1054 lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0" |
|
1055 nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] |
|
1056 nitpick [card nat = 14, full_descrs, unary_ints, expect = potential] (* unfortunate *) |
|
1057 oops |
|
1058 |
|
1059 lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0" |
|
1060 nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] |
|
1061 nitpick [card nat = 14, full_descrs, unary_ints, expect = none] |
|
1062 sorry |
|
1063 |
|
1064 lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12" |
|
1065 nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] |
|
1066 nitpick [card nat = 14, full_descrs, unary_ints, expect = none] |
|
1067 sorry |
|
1068 |
|
1069 lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12" |
|
1070 nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] |
|
1071 oops |
|
1072 |
|
1073 lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13" |
|
1074 nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] |
|
1075 oops |
|
1076 |
|
1077 lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0" |
|
1078 nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] |
|
1079 nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] |
|
1080 oops |
|
1081 |
|
1082 lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0" |
|
1083 nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] |
|
1084 nitpick [card nat = 14, full_descrs, unary_ints, expect = none] |
|
1085 oops |
|
1086 |
|
1087 lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12" |
|
1088 nitpick [card nat = 4, full_descrs, unary_ints, expect = potential] |
|
1089 nitpick [card nat = 14, full_descrs, unary_ints, expect = none] |
|
1090 sorry |
|
1091 |
|
1092 lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12" |
|
1093 nitpick [card nat = 14, full_descrs, unary_ints, expect = genuine] |
|
1094 oops |
|
1095 |
|
1096 lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13" |
|
1097 nitpick [card nat = 14, full_descrs, unary_ints, expect = none] |
|
1098 sorry |
|
1099 |
1054 subsection {* Destructors and Recursors *} |
1100 subsection {* Destructors and Recursors *} |
1055 |
1101 |
1056 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)" |
1102 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)" |
1057 nitpick [card = 2, expect = none] |
1103 nitpick [card = 2, expect = none] |
1058 by auto |
1104 by auto |