author | blanchet |
Mon, 22 Feb 2010 19:31:00 +0100 | |
changeset 35284 | 9edc2bd6d2bd |
parent 35078 | 6fd1052fe463 |
child 35386 | 45a4e19d3ebd |
permissions | -rw-r--r-- |
33197 | 1 |
(* Title: HOL/Nitpick_Examples/Core_Nits.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
35076
cc19e2aef17e
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents:
34126
diff
changeset
|
3 |
Copyright 2009, 2010 |
33197 | 4 |
|
5 |
Examples featuring Nitpick's functional core. |
|
6 |
*) |
|
7 |
||
8 |
header {* Examples Featuring Nitpick's Functional Core *} |
|
9 |
||
10 |
theory Core_Nits |
|
11 |
imports Main |
|
12 |
begin |
|
13 |
||
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
14 |
nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
15 |
timeout = 60 s] |
34082
61b7aa37f4b7
make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
blanchet
parents:
33199
diff
changeset
|
16 |
|
33197 | 17 |
subsection {* Curry in a Hurry *} |
18 |
||
19 |
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
20 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 21 |
by auto |
22 |
||
23 |
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
24 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 25 |
by auto |
26 |
||
27 |
lemma "split (curry f) = f" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
28 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 29 |
by auto |
30 |
||
31 |
lemma "curry (split f) = f" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
32 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 33 |
by auto |
34 |
||
35 |
lemma "(split o curry) f = f" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
36 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 37 |
by auto |
38 |
||
39 |
lemma "(curry o split) f = f" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
40 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 41 |
by auto |
42 |
||
43 |
lemma "(split o curry) f = (\<lambda>x. x) f" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
44 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 45 |
by auto |
46 |
||
47 |
lemma "(curry o split) f = (\<lambda>x. x) f" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
48 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 49 |
by auto |
50 |
||
51 |
lemma "((split o curry) f) p = ((\<lambda>x. x) f) p" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
52 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 53 |
by auto |
54 |
||
55 |
lemma "((curry o split) f) x = ((\<lambda>x. x) f) x" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
56 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 57 |
by auto |
58 |
||
59 |
lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
60 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 61 |
by auto |
62 |
||
63 |
lemma "split o curry = (\<lambda>x. x)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
64 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 65 |
apply (rule ext)+ |
66 |
by auto |
|
67 |
||
68 |
lemma "curry o split = (\<lambda>x. x)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
69 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 70 |
apply (rule ext)+ |
71 |
by auto |
|
72 |
||
73 |
lemma "split (\<lambda>x y. f (x, y)) = f" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
74 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 75 |
by auto |
76 |
||
77 |
subsection {* Representations *} |
|
78 |
||
79 |
lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y" |
|
80 |
nitpick [expect = none] |
|
81 |
by auto |
|
82 |
||
83 |
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
84 |
nitpick [card 'a = 25, card 'b = 24, expect = genuine] |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
85 |
nitpick [card = 1\<midarrow>10, mono, expect = none] |
33197 | 86 |
oops |
87 |
||
88 |
lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y" |
|
89 |
nitpick [card = 1, expect = genuine] |
|
90 |
nitpick [card = 5, expect = genuine] |
|
91 |
oops |
|
92 |
||
93 |
lemma "P (\<lambda>x. x)" |
|
94 |
nitpick [card = 1, expect = genuine] |
|
95 |
nitpick [card = 5, expect = genuine] |
|
96 |
oops |
|
97 |
||
98 |
lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
99 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 100 |
by auto |
101 |
||
102 |
lemma "fst (a, b) = a" |
|
103 |
nitpick [card = 1\<midarrow>20, expect = none] |
|
104 |
by auto |
|
105 |
||
106 |
lemma "\<exists>P. P = Id" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
107 |
nitpick [card = 1\<midarrow>20, expect = none] |
33197 | 108 |
by auto |
109 |
||
110 |
lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*" |
|
111 |
nitpick [card = 1\<midarrow>3, expect = none] |
|
112 |
by auto |
|
113 |
||
114 |
lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
115 |
nitpick [card = 1\<midarrow>4, expect = none] |
33197 | 116 |
by auto |
117 |
||
118 |
lemma "Id (a, a)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
119 |
nitpick [card = 1\<midarrow>50, expect = none] |
33197 | 120 |
by (auto simp: Id_def Collect_def) |
121 |
||
122 |
lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))" |
|
34082
61b7aa37f4b7
make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
blanchet
parents:
33199
diff
changeset
|
123 |
nitpick [card = 1\<midarrow>10, expect = none] |
33197 | 124 |
by (auto simp: Id_def Collect_def) |
125 |
||
126 |
lemma "UNIV (x\<Colon>'a\<times>'a)" |
|
127 |
nitpick [card = 1\<midarrow>50, expect = none] |
|
128 |
sorry |
|
129 |
||
130 |
lemma "{} = A - A" |
|
131 |
nitpick [card = 1\<midarrow>100, expect = none] |
|
132 |
by auto |
|
133 |
||
134 |
lemma "g = Let (A \<or> B)" |
|
135 |
nitpick [card = 1, expect = none] |
|
136 |
nitpick [card = 2, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
137 |
nitpick [card = 12, expect = genuine] |
33197 | 138 |
oops |
139 |
||
140 |
lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)" |
|
141 |
nitpick [expect = none] |
|
142 |
by auto |
|
143 |
||
144 |
lemma "A \<subseteq> B" |
|
145 |
nitpick [card = 100, expect = genuine] |
|
146 |
oops |
|
147 |
||
148 |
lemma "A = {b}" |
|
149 |
nitpick [card = 100, expect = genuine] |
|
150 |
oops |
|
151 |
||
152 |
lemma "{a, b} = {b}" |
|
153 |
nitpick [card = 100, expect = genuine] |
|
154 |
oops |
|
155 |
||
156 |
lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R" |
|
157 |
nitpick [card = 1, expect = genuine] |
|
158 |
nitpick [card = 20, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
159 |
nitpick [card = 5, dont_box, expect = genuine] |
33197 | 160 |
oops |
161 |
||
162 |
lemma "f (g\<Colon>'a\<Rightarrow>'a) = x" |
|
163 |
nitpick [card = 3, expect = genuine] |
|
164 |
nitpick [card = 3, dont_box, expect = genuine] |
|
165 |
nitpick [card = 10, expect = genuine] |
|
166 |
oops |
|
167 |
||
168 |
lemma "f (a, b) = x" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
169 |
nitpick [card = 12, expect = genuine] |
33197 | 170 |
oops |
171 |
||
172 |
lemma "f (a, a) = f (c, d)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
173 |
nitpick [card = 12, expect = genuine] |
33197 | 174 |
oops |
175 |
||
176 |
lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
177 |
nitpick [card = 1\<midarrow>12, expect = none] |
33197 | 178 |
by auto |
179 |
||
180 |
lemma "\<exists>F. F a b = G a b" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
181 |
nitpick [card = 2, expect = none] |
33197 | 182 |
by auto |
183 |
||
184 |
lemma "f = split" |
|
185 |
nitpick [card = 1, expect = none] |
|
186 |
nitpick [card = 2, expect = genuine] |
|
187 |
oops |
|
188 |
||
189 |
lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R" |
|
190 |
nitpick [card = 20, expect = none] |
|
191 |
by auto |
|
192 |
||
193 |
lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> |
|
194 |
A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
195 |
nitpick [card = 1\<midarrow>25, expect = none] |
33197 | 196 |
by auto |
197 |
||
198 |
lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)" |
|
199 |
nitpick [card = 8, expect = genuine] |
|
200 |
oops |
|
201 |
||
202 |
subsection {* Quantifiers *} |
|
203 |
||
204 |
lemma "x = y" |
|
205 |
nitpick [card 'a = 1, expect = none] |
|
206 |
nitpick [card 'a = 2, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
207 |
nitpick [card 'a = 200, expect = genuine] |
33197 | 208 |
oops |
209 |
||
210 |
lemma "\<forall>x. x = y" |
|
211 |
nitpick [card 'a = 1, expect = none] |
|
212 |
nitpick [card 'a = 2, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
213 |
nitpick [card 'a = 200, expect = genuine] |
33197 | 214 |
oops |
215 |
||
216 |
lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y" |
|
217 |
nitpick [card 'a = 1, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
218 |
nitpick [card 'a = 200, expect = genuine] |
33197 | 219 |
oops |
220 |
||
221 |
lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
222 |
nitpick [card 'a = 1\<midarrow>20, expect = none] |
33197 | 223 |
by auto |
224 |
||
225 |
lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
226 |
nitpick [card = 1\<midarrow>20, expect = none] |
33197 | 227 |
by auto |
228 |
||
229 |
lemma "\<forall>x. \<exists>y. f x y = f x (g x)" |
|
230 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
231 |
by auto |
|
232 |
||
233 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
234 |
nitpick [card = 1\<midarrow>4, expect = none] |
33197 | 235 |
by auto |
236 |
||
237 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)" |
|
238 |
nitpick [card = 3, expect = genuine] |
|
239 |
oops |
|
240 |
||
241 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
242 |
f u v w x y z = f u (g u) w (h u w) y (k u w y)" |
|
243 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
244 |
nitpick [card = 3, expect = none] |
|
245 |
sorry |
|
246 |
||
247 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
248 |
f u v w x y z = f u (g u) w (h u w y) y (k u w y)" |
|
249 |
nitpick [card = 1\<midarrow>2, expect = genuine] |
|
250 |
oops |
|
251 |
||
252 |
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z. |
|
253 |
f u v w x y z = f u (g u w) w (h u w) y (k u w y)" |
|
254 |
nitpick [card = 1\<midarrow>2, expect = genuine] |
|
255 |
oops |
|
256 |
||
257 |
lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f. |
|
258 |
f u v w x = f u (g u) w (h u w)" |
|
259 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
260 |
sorry |
|
261 |
||
262 |
lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f. |
|
263 |
f u v w x = f u (g u w) w (h u)" |
|
264 |
nitpick [card = 1\<midarrow>2, dont_box, expect = genuine] |
|
265 |
oops |
|
266 |
||
267 |
lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f. |
|
268 |
f u v w x = f u (g u) w (h u w)" |
|
269 |
nitpick [card = 1\<midarrow>2, dont_box, expect = none] |
|
270 |
sorry |
|
271 |
||
272 |
lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f. |
|
273 |
f u v w x = f u (g u w) w (h u)" |
|
274 |
nitpick [card = 1\<midarrow>2, dont_box, expect = genuine] |
|
275 |
oops |
|
276 |
||
277 |
lemma "\<forall>x. if (\<forall>y. x = y) then False else True" |
|
278 |
nitpick [card = 1, expect = genuine] |
|
279 |
nitpick [card = 2\<midarrow>5, expect = none] |
|
280 |
oops |
|
281 |
||
282 |
lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True" |
|
283 |
nitpick [card = 1, expect = genuine] |
|
284 |
nitpick [card = 2, expect = none] |
|
285 |
oops |
|
286 |
||
287 |
lemma "\<forall>x. if (\<exists>y. x = y) then True else False" |
|
288 |
nitpick [expect = none] |
|
289 |
sorry |
|
290 |
||
291 |
lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False" |
|
292 |
nitpick [expect = none] |
|
293 |
sorry |
|
294 |
||
295 |
lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)" |
|
296 |
nitpick [expect = none] |
|
297 |
by auto |
|
298 |
||
299 |
lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))" |
|
300 |
nitpick [expect = none] |
|
301 |
by auto |
|
302 |
||
303 |
lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)" |
|
304 |
nitpick [card 'a = 1, expect = genuine] |
|
305 |
nitpick [card 'a = 5, expect = genuine] |
|
306 |
oops |
|
307 |
||
308 |
lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) |
|
309 |
else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
310 |
nitpick [expect = none] |
|
311 |
by auto |
|
312 |
||
313 |
lemma "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) |
|
314 |
else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))" |
|
315 |
nitpick [expect = none] |
|
316 |
by auto |
|
317 |
||
318 |
lemma "let x = (\<forall>x. P x) in if x then x else \<not> x" |
|
319 |
nitpick [expect = none] |
|
320 |
by auto |
|
321 |
||
322 |
lemma "let x = (\<forall>x\<Colon>'a \<times> 'b. P x) in if x then x else \<not> x" |
|
323 |
nitpick [expect = none] |
|
324 |
by auto |
|
325 |
||
326 |
subsection {* Schematic Variables *} |
|
327 |
||
328 |
lemma "x = ?x" |
|
329 |
nitpick [expect = none] |
|
330 |
by auto |
|
331 |
||
332 |
lemma "\<forall>x. x = ?x" |
|
333 |
nitpick [expect = genuine] |
|
334 |
oops |
|
335 |
||
336 |
lemma "\<exists>x. x = ?x" |
|
337 |
nitpick [expect = none] |
|
338 |
by auto |
|
339 |
||
340 |
lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x" |
|
341 |
nitpick [expect = none] |
|
342 |
by auto |
|
343 |
||
344 |
lemma "\<forall>x. ?x = ?y" |
|
345 |
nitpick [expect = none] |
|
346 |
by auto |
|
347 |
||
348 |
lemma "\<exists>x. ?x = ?y" |
|
349 |
nitpick [expect = none] |
|
350 |
by auto |
|
351 |
||
352 |
subsection {* Known Constants *} |
|
353 |
||
354 |
lemma "x \<equiv> all \<Longrightarrow> False" |
|
355 |
nitpick [card = 1, expect = genuine] |
|
356 |
nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine] |
|
357 |
nitpick [card = 2, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
358 |
nitpick [card = 6, expect = genuine] |
33197 | 359 |
oops |
360 |
||
361 |
lemma "\<And>x. f x y = f x y" |
|
362 |
nitpick [expect = none] |
|
363 |
oops |
|
364 |
||
365 |
lemma "\<And>x. f x y = f y x" |
|
366 |
nitpick [expect = genuine] |
|
367 |
oops |
|
368 |
||
369 |
lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True" |
|
370 |
nitpick [expect = none] |
|
371 |
by auto |
|
372 |
||
373 |
lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False" |
|
374 |
nitpick [expect = genuine] |
|
375 |
oops |
|
376 |
||
377 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))" |
|
378 |
nitpick [expect = none] |
|
379 |
by auto |
|
380 |
||
381 |
lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False" |
|
382 |
nitpick [card = 1, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
383 |
nitpick [card = 20, expect = genuine] |
33197 | 384 |
oops |
385 |
||
386 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))" |
|
387 |
nitpick [expect = none] |
|
388 |
by auto |
|
389 |
||
390 |
lemma "P x \<equiv> P x" |
|
391 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
392 |
by auto |
|
393 |
||
394 |
lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x" |
|
395 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
396 |
by auto |
|
397 |
||
398 |
lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x" |
|
399 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
400 |
by auto |
|
401 |
||
402 |
lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False" |
|
403 |
nitpick [expect = genuine] |
|
404 |
oops |
|
405 |
||
406 |
lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))" |
|
407 |
nitpick [expect = none] |
|
408 |
by auto |
|
409 |
||
410 |
lemma "P x \<Longrightarrow> P x" |
|
411 |
nitpick [card = 1\<midarrow>10, expect = none] |
|
412 |
by auto |
|
413 |
||
414 |
lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False" |
|
415 |
nitpick [expect = none] |
|
416 |
by auto |
|
417 |
||
418 |
lemma "True \<Longrightarrow> False" |
|
419 |
nitpick [expect = genuine] |
|
420 |
oops |
|
421 |
||
422 |
lemma "x = Not" |
|
423 |
nitpick [expect = genuine] |
|
424 |
oops |
|
425 |
||
426 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))" |
|
427 |
nitpick [expect = none] |
|
428 |
by auto |
|
429 |
||
430 |
lemma "x = True" |
|
431 |
nitpick [expect = genuine] |
|
432 |
oops |
|
433 |
||
434 |
lemma "x = False" |
|
435 |
nitpick [expect = genuine] |
|
436 |
oops |
|
437 |
||
438 |
lemma "x = undefined" |
|
439 |
nitpick [expect = genuine] |
|
440 |
oops |
|
441 |
||
442 |
lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined" |
|
443 |
nitpick [expect = genuine] |
|
444 |
oops |
|
445 |
||
446 |
lemma "undefined = undefined" |
|
447 |
nitpick [expect = none] |
|
448 |
by auto |
|
449 |
||
450 |
lemma "f undefined = f undefined" |
|
451 |
nitpick [expect = none] |
|
452 |
by auto |
|
453 |
||
454 |
lemma "f undefined = g undefined" |
|
455 |
nitpick [card = 33, expect = genuine] |
|
456 |
oops |
|
457 |
||
458 |
lemma "\<exists>!x. x = undefined" |
|
459 |
nitpick [card = 30, expect = none] |
|
460 |
by auto |
|
461 |
||
462 |
lemma "x = All \<Longrightarrow> False" |
|
463 |
nitpick [card = 1, dont_box, expect = genuine] |
|
464 |
nitpick [card = 2, dont_box, expect = genuine] |
|
465 |
nitpick [card = 8, dont_box, expect = genuine] |
|
466 |
nitpick [card = 10, dont_box, expect = unknown] |
|
467 |
oops |
|
468 |
||
469 |
lemma "\<forall>x. f x y = f x y" |
|
470 |
nitpick [expect = none] |
|
471 |
oops |
|
472 |
||
473 |
lemma "\<forall>x. f x y = f y x" |
|
474 |
nitpick [expect = genuine] |
|
475 |
oops |
|
476 |
||
477 |
lemma "All (\<lambda>x. f x y = f x y) = True" |
|
478 |
nitpick [expect = none] |
|
479 |
by auto |
|
480 |
||
481 |
lemma "All (\<lambda>x. f x y = f x y) = False" |
|
482 |
nitpick [expect = genuine] |
|
483 |
oops |
|
484 |
||
485 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))" |
|
486 |
nitpick [expect = none] |
|
487 |
by auto |
|
488 |
||
489 |
lemma "x = Ex \<Longrightarrow> False" |
|
490 |
nitpick [card = 1, dont_box, expect = genuine] |
|
491 |
nitpick [card = 2, dont_box, expect = genuine] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
492 |
nitpick [card = 6, dont_box, expect = genuine] |
33197 | 493 |
nitpick [card = 10, dont_box, expect = unknown] |
494 |
oops |
|
495 |
||
496 |
lemma "\<exists>x. f x y = f x y" |
|
497 |
nitpick [expect = none] |
|
498 |
oops |
|
499 |
||
500 |
lemma "\<exists>x. f x y = f y x" |
|
501 |
nitpick [expect = none] |
|
502 |
oops |
|
503 |
||
504 |
lemma "Ex (\<lambda>x. f x y = f x y) = True" |
|
505 |
nitpick [expect = none] |
|
506 |
by auto |
|
507 |
||
508 |
lemma "Ex (\<lambda>x. f x y = f y x) = True" |
|
509 |
nitpick [expect = none] |
|
510 |
by auto |
|
511 |
||
512 |
lemma "Ex (\<lambda>x. f x y = f x y) = False" |
|
513 |
nitpick [expect = genuine] |
|
514 |
oops |
|
515 |
||
516 |
lemma "Ex (\<lambda>x. f x y = f y x) = False" |
|
517 |
nitpick [expect = genuine] |
|
518 |
oops |
|
519 |
||
520 |
lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False" |
|
521 |
nitpick [expect = none] |
|
522 |
by auto |
|
523 |
||
524 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))" |
|
525 |
nitpick [expect = none] |
|
526 |
by auto |
|
527 |
||
528 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))" |
|
529 |
"I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))" |
|
530 |
nitpick [expect = none] |
|
531 |
by auto |
|
532 |
||
533 |
lemma "x = y \<Longrightarrow> y = x" |
|
534 |
nitpick [expect = none] |
|
535 |
by auto |
|
536 |
||
537 |
lemma "x = y \<Longrightarrow> f x = f y" |
|
538 |
nitpick [expect = none] |
|
539 |
by auto |
|
540 |
||
541 |
lemma "x = y \<and> y = z \<Longrightarrow> x = z" |
|
542 |
nitpick [expect = none] |
|
543 |
by auto |
|
544 |
||
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
545 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x. op \<and> (I x))" |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
546 |
"I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x y. x \<and> (I y))" |
33197 | 547 |
nitpick [expect = none] |
548 |
by auto |
|
549 |
||
550 |
lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))" |
|
551 |
nitpick [expect = none] |
|
552 |
by auto |
|
553 |
||
554 |
lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b" |
|
555 |
nitpick [expect = none] |
|
556 |
by auto |
|
557 |
||
558 |
lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)" |
|
559 |
nitpick [expect = none] |
|
560 |
by auto |
|
561 |
||
562 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))" |
|
563 |
"I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))" |
|
564 |
nitpick [expect = none] |
|
565 |
by auto |
|
566 |
||
567 |
lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b" |
|
568 |
nitpick [expect = none] |
|
569 |
by auto |
|
570 |
||
571 |
lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b" |
|
572 |
nitpick [expect = none] |
|
573 |
by auto |
|
574 |
||
575 |
lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)" |
|
576 |
nitpick [expect = none] |
|
577 |
by auto |
|
578 |
||
579 |
lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b" |
|
580 |
nitpick [expect = none] |
|
581 |
by auto |
|
582 |
||
583 |
lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)" |
|
584 |
nitpick [expect = none] |
|
585 |
by auto |
|
586 |
||
587 |
lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))" |
|
588 |
nitpick [expect = none] |
|
589 |
by auto |
|
590 |
||
591 |
lemma "(if a then b else c) = (THE d. (a \<longrightarrow> (d = b)) \<and> (\<not> a \<longrightarrow> (d = c)))" |
|
592 |
nitpick [expect = none] |
|
593 |
by auto |
|
594 |
||
595 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))" |
|
596 |
"J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))" |
|
597 |
"K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))" |
|
598 |
nitpick [expect = none] |
|
599 |
by auto |
|
600 |
||
601 |
lemma "fst (x, y) = x" |
|
602 |
nitpick [expect = none] |
|
603 |
by (simp add: fst_def) |
|
604 |
||
605 |
lemma "snd (x, y) = y" |
|
606 |
nitpick [expect = none] |
|
607 |
by (simp add: snd_def) |
|
608 |
||
609 |
lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x" |
|
610 |
nitpick [expect = none] |
|
611 |
by (simp add: fst_def) |
|
612 |
||
613 |
lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y" |
|
614 |
nitpick [expect = none] |
|
615 |
by (simp add: snd_def) |
|
616 |
||
617 |
lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x" |
|
618 |
nitpick [expect = none] |
|
619 |
by (simp add: fst_def) |
|
620 |
||
621 |
lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y" |
|
622 |
nitpick [expect = none] |
|
623 |
by (simp add: snd_def) |
|
624 |
||
625 |
lemma "fst (x\<Colon>'a\<times>'b, y) = x" |
|
626 |
nitpick [expect = none] |
|
627 |
by (simp add: fst_def) |
|
628 |
||
629 |
lemma "snd (x\<Colon>'a\<times>'b, y) = y" |
|
630 |
nitpick [expect = none] |
|
631 |
by (simp add: snd_def) |
|
632 |
||
633 |
lemma "fst (x, y\<Colon>'a\<times>'b) = x" |
|
634 |
nitpick [expect = none] |
|
635 |
by (simp add: fst_def) |
|
636 |
||
637 |
lemma "snd (x, y\<Colon>'a\<times>'b) = y" |
|
638 |
nitpick [expect = none] |
|
639 |
by (simp add: snd_def) |
|
640 |
||
641 |
lemma "fst p = (THE a. \<exists>b. p = Pair a b)" |
|
642 |
nitpick [expect = none] |
|
643 |
by (simp add: fst_def) |
|
644 |
||
645 |
lemma "snd p = (THE b. \<exists>a. p = Pair a b)" |
|
646 |
nitpick [expect = none] |
|
647 |
by (simp add: snd_def) |
|
648 |
||
649 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))" |
|
650 |
nitpick [expect = none] |
|
651 |
by auto |
|
652 |
||
653 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))" |
|
654 |
nitpick [expect = none] |
|
655 |
by auto |
|
656 |
||
657 |
lemma "fst (x, y) = snd (y, x)" |
|
658 |
nitpick [expect = none] |
|
659 |
by auto |
|
660 |
||
661 |
lemma "(x, x) \<in> Id" |
|
662 |
nitpick [expect = none] |
|
663 |
by auto |
|
664 |
||
665 |
lemma "(x, y) \<in> Id \<Longrightarrow> x = y" |
|
666 |
nitpick [expect = none] |
|
667 |
by auto |
|
668 |
||
669 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))" |
|
670 |
nitpick [expect = none] |
|
671 |
by auto |
|
672 |
||
673 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))" |
|
674 |
nitpick [expect = none] |
|
675 |
by (simp add: curry_def) |
|
676 |
||
677 |
lemma "{} = (\<lambda>x. False)" |
|
678 |
nitpick [expect = none] |
|
33199 | 679 |
by (metis Collect_def empty_def) |
33197 | 680 |
|
681 |
lemma "x \<in> {}" |
|
682 |
nitpick [expect = genuine] |
|
683 |
oops |
|
684 |
||
685 |
lemma "{a, b} = {b}" |
|
686 |
nitpick [expect = genuine] |
|
687 |
oops |
|
688 |
||
689 |
lemma "{a, b} \<noteq> {b}" |
|
690 |
nitpick [expect = genuine] |
|
691 |
oops |
|
692 |
||
693 |
lemma "{a} = {b}" |
|
694 |
nitpick [expect = genuine] |
|
695 |
oops |
|
696 |
||
697 |
lemma "{a} \<noteq> {b}" |
|
698 |
nitpick [expect = genuine] |
|
699 |
oops |
|
700 |
||
701 |
lemma "{a, b, c} = {c, b, a}" |
|
702 |
nitpick [expect = none] |
|
703 |
by auto |
|
704 |
||
705 |
lemma "UNIV = (\<lambda>x. True)" |
|
706 |
nitpick [expect = none] |
|
707 |
by (simp only: UNIV_def Collect_def) |
|
708 |
||
709 |
lemma "UNIV x = True" |
|
710 |
nitpick [expect = none] |
|
711 |
by (simp only: UNIV_def Collect_def) |
|
712 |
||
713 |
lemma "x \<notin> UNIV" |
|
714 |
nitpick [expect = genuine] |
|
715 |
oops |
|
716 |
||
717 |
lemma "op \<in> = (\<lambda>x P. P x)" |
|
718 |
nitpick [expect = none] |
|
719 |
apply (rule ext) |
|
720 |
apply (rule ext) |
|
721 |
by (simp add: mem_def) |
|
722 |
||
723 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))" |
|
724 |
nitpick [expect = none] |
|
725 |
apply (rule ext) |
|
726 |
apply (rule ext) |
|
727 |
by (simp add: mem_def) |
|
728 |
||
729 |
lemma "P x = (x \<in> P)" |
|
730 |
nitpick [expect = none] |
|
731 |
by (simp add: mem_def) |
|
732 |
||
733 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))" |
|
734 |
nitpick [expect = none] |
|
735 |
by simp |
|
736 |
||
737 |
lemma "insert = (\<lambda>x y. insert x (y \<union> y))" |
|
738 |
nitpick [expect = none] |
|
739 |
by simp |
|
740 |
||
741 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))" |
|
742 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
743 |
by auto |
|
744 |
||
745 |
lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})" |
|
746 |
nitpick [card = 1\<midarrow>3, expect = none] |
|
747 |
apply (rule ext) |
|
748 |
by auto |
|
749 |
||
750 |
lemma "(x, x) \<in> rtrancl {(y, y)}" |
|
751 |
nitpick [expect = none] |
|
752 |
by auto |
|
753 |
||
754 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))" |
|
755 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
756 |
by auto |
|
757 |
||
758 |
lemma "((x, x), (x, x)) \<in> rtrancl {}" |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
759 |
nitpick [card = 1\<midarrow>5, expect = none] |
33197 | 760 |
by auto |
761 |
||
762 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))" |
|
763 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
764 |
by auto |
|
765 |
||
766 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))" |
|
767 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
768 |
by auto |
|
769 |
||
770 |
lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)" |
|
771 |
nitpick [expect = none] |
|
772 |
by auto |
|
773 |
||
774 |
lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B" |
|
775 |
nitpick [expect = none] |
|
776 |
by auto |
|
777 |
||
778 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))" |
|
779 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
780 |
by auto |
|
781 |
||
782 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))" |
|
783 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
784 |
by auto |
|
785 |
||
786 |
lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)" |
|
787 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
788 |
by auto |
|
789 |
||
790 |
lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B" |
|
791 |
nitpick [expect = none] |
|
792 |
by auto |
|
793 |
||
794 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))" |
|
795 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
796 |
by auto |
|
797 |
||
798 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))" |
|
799 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
800 |
by auto |
|
801 |
||
802 |
lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B" |
|
803 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
804 |
by auto |
|
805 |
||
806 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))" |
|
807 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
808 |
by auto |
|
809 |
||
810 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))" |
|
811 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
812 |
by auto |
|
813 |
||
814 |
lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)" |
|
815 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
816 |
by auto |
|
817 |
||
818 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))" |
|
819 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
820 |
by auto |
|
821 |
||
822 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))" |
|
823 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
824 |
by auto |
|
825 |
||
826 |
lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B" |
|
827 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
828 |
by auto |
|
829 |
||
830 |
lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B" |
|
831 |
nitpick [card = 5, expect = genuine] |
|
832 |
oops |
|
833 |
||
834 |
lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B" |
|
835 |
nitpick [expect = none] |
|
836 |
by auto |
|
837 |
||
838 |
lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))" |
|
34126 | 839 |
nitpick [card = 1\<midarrow>7, expect = none] |
33197 | 840 |
by auto |
841 |
||
842 |
lemma "A \<union> - A = UNIV" |
|
843 |
nitpick [expect = none] |
|
844 |
by auto |
|
845 |
||
846 |
lemma "A \<inter> - A = {}" |
|
847 |
nitpick [expect = none] |
|
848 |
by auto |
|
849 |
||
850 |
lemma "A = -(A\<Colon>'a set)" |
|
851 |
nitpick [card 'a = 10, expect = genuine] |
|
852 |
oops |
|
853 |
||
854 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))" |
|
34126 | 855 |
nitpick [card = 1\<midarrow>7, expect = none] |
33197 | 856 |
oops |
857 |
||
858 |
lemma "finite A" |
|
859 |
nitpick [expect = none] |
|
860 |
oops |
|
861 |
||
862 |
lemma "finite A \<Longrightarrow> finite B" |
|
863 |
nitpick [expect = none] |
|
864 |
oops |
|
865 |
||
866 |
lemma "All finite" |
|
867 |
nitpick [expect = none] |
|
868 |
oops |
|
869 |
||
870 |
subsection {* The and Eps *} |
|
871 |
||
872 |
lemma "x = The" |
|
873 |
nitpick [card = 5, expect = genuine] |
|
874 |
oops |
|
875 |
||
876 |
lemma "\<exists>x. x = The" |
|
877 |
nitpick [card = 1\<midarrow>3] |
|
878 |
by auto |
|
879 |
||
880 |
lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x" |
|
881 |
nitpick [expect = none] |
|
882 |
by auto |
|
883 |
||
884 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z" |
|
885 |
nitpick [expect = genuine] |
|
886 |
oops |
|
887 |
||
888 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y" |
|
889 |
nitpick [card = 2, expect = none] |
|
890 |
nitpick [card = 3\<midarrow>5, expect = genuine] |
|
891 |
oops |
|
892 |
||
893 |
lemma "P x \<Longrightarrow> P (The P)" |
|
894 |
nitpick [card = 1\<midarrow>2, expect = none] |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35078
diff
changeset
|
895 |
nitpick [card = 3, expect = genuine] |
33197 | 896 |
nitpick [card = 8, expect = genuine] |
897 |
oops |
|
898 |
||
899 |
lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y" |
|
900 |
nitpick [expect = genuine] |
|
901 |
oops |
|
902 |
||
903 |
lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))" |
|
904 |
nitpick [card = 1\<midarrow>5, expect = none] |
|
905 |
by auto |
|
906 |
||
907 |
lemma "x = Eps" |
|
908 |
nitpick [card = 5, expect = genuine] |
|
909 |
oops |
|
910 |
||
911 |
lemma "\<exists>x. x = Eps" |
|
912 |
nitpick [card = 1\<midarrow>3, expect = none] |
|
913 |
by auto |
|
914 |
||
915 |
lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x" |
|
916 |
nitpick [expect = none] |
|
917 |
by auto |
|
918 |
||
919 |
lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z" |
|
920 |
nitpick [expect = genuine] |
|
921 |
apply auto |
|
922 |
oops |
|
923 |
||
924 |
lemma "P x \<Longrightarrow> P (Eps P)" |
|
925 |
nitpick [card = 1\<midarrow>8, expect = none] |
|
926 |
by (metis exE_some) |
|
927 |
||
928 |
lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y" |
|
929 |
nitpick [expect = genuine] |
|
930 |
oops |
|
931 |
||
932 |
lemma "P (Eps P)" |
|
933 |
nitpick [expect = genuine] |
|
934 |
oops |
|
935 |
||
936 |
lemma "(P\<Colon>nat set) (Eps P)" |
|
937 |
nitpick [expect = genuine] |
|
938 |
oops |
|
939 |
||
940 |
lemma "\<not> P (Eps P)" |
|
941 |
nitpick [expect = genuine] |
|
942 |
oops |
|
943 |
||
944 |
lemma "\<not> (P\<Colon>nat set) (Eps P)" |
|
945 |
nitpick [expect = genuine] |
|
946 |
oops |
|
947 |
||
948 |
lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)" |
|
949 |
nitpick [expect = none] |
|
950 |
sorry |
|
951 |
||
952 |
lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)" |
|
953 |
nitpick [expect = none] |
|
954 |
sorry |
|
955 |
||
956 |
lemma "P (The P)" |
|
957 |
nitpick [expect = genuine] |
|
958 |
oops |
|
959 |
||
960 |
lemma "(P\<Colon>nat set) (The P)" |
|
961 |
nitpick [expect = genuine] |
|
962 |
oops |
|
963 |
||
964 |
lemma "\<not> P (The P)" |
|
965 |
nitpick [expect = genuine] |
|
966 |
oops |
|
967 |
||
968 |
lemma "\<not> (P\<Colon>nat set) (The P)" |
|
969 |
nitpick [expect = genuine] |
|
970 |
oops |
|
971 |
||
972 |
lemma "The P \<noteq> x" |
|
973 |
nitpick [expect = genuine] |
|
974 |
oops |
|
975 |
||
976 |
lemma "The P \<noteq> (x\<Colon>nat)" |
|
977 |
nitpick [expect = genuine] |
|
978 |
oops |
|
979 |
||
980 |
lemma "P x \<Longrightarrow> P (The P)" |
|
981 |
nitpick [expect = genuine] |
|
982 |
oops |
|
983 |
||
984 |
lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)" |
|
985 |
nitpick [expect = genuine] |
|
986 |
oops |
|
987 |
||
988 |
lemma "P = {x} \<Longrightarrow> P (The P)" |
|
989 |
nitpick [expect = none] |
|
990 |
oops |
|
991 |
||
992 |
lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)" |
|
993 |
nitpick [expect = none] |
|
994 |
oops |
|
995 |
||
996 |
consts Q :: 'a |
|
997 |
||
998 |
lemma "Q (Eps Q)" |
|
999 |
nitpick [expect = genuine] |
|
1000 |
oops |
|
1001 |
||
1002 |
lemma "(Q\<Colon>nat set) (Eps Q)" |
|
1003 |
nitpick [expect = none] |
|
1004 |
oops |
|
1005 |
||
1006 |
lemma "\<not> Q (Eps Q)" |
|
1007 |
nitpick [expect = genuine] |
|
1008 |
oops |
|
1009 |
||
1010 |
lemma "\<not> (Q\<Colon>nat set) (Eps Q)" |
|
1011 |
nitpick [expect = genuine] |
|
1012 |
oops |
|
1013 |
||
1014 |
lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)" |
|
1015 |
nitpick [expect = none] |
|
1016 |
sorry |
|
1017 |
||
1018 |
lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)" |
|
1019 |
nitpick [expect = none] |
|
1020 |
sorry |
|
1021 |
||
1022 |
lemma "Q (The Q)" |
|
1023 |
nitpick [expect = genuine] |
|
1024 |
oops |
|
1025 |
||
1026 |
lemma "(Q\<Colon>nat set) (The Q)" |
|
1027 |
nitpick [expect = genuine] |
|
1028 |
oops |
|
1029 |
||
1030 |
lemma "\<not> Q (The Q)" |
|
1031 |
nitpick [expect = genuine] |
|
1032 |
oops |
|
1033 |
||
1034 |
lemma "\<not> (Q\<Colon>nat set) (The Q)" |
|
1035 |
nitpick [expect = genuine] |
|
1036 |
oops |
|
1037 |
||
1038 |
lemma "The Q \<noteq> x" |
|
1039 |
nitpick [expect = genuine] |
|
1040 |
oops |
|
1041 |
||
1042 |
lemma "The Q \<noteq> (x\<Colon>nat)" |
|
1043 |
nitpick [expect = genuine] |
|
1044 |
oops |
|
1045 |
||
1046 |
lemma "Q x \<Longrightarrow> Q (The Q)" |
|
1047 |
nitpick [expect = genuine] |
|
1048 |
oops |
|
1049 |
||
1050 |
lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)" |
|
1051 |
nitpick [expect = genuine] |
|
1052 |
oops |
|
1053 |
||
1054 |
lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)" |
|
1055 |
nitpick [expect = none] |
|
1056 |
oops |
|
1057 |
||
1058 |
lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)" |
|
1059 |
nitpick [expect = none] |
|
1060 |
oops |
|
1061 |
||
1062 |
subsection {* Destructors and Recursors *} |
|
1063 |
||
1064 |
lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)" |
|
1065 |
nitpick [card = 2, expect = none] |
|
1066 |
by auto |
|
1067 |
||
1068 |
lemma "bool_rec x y True = x" |
|
1069 |
nitpick [card = 2, expect = none] |
|
1070 |
by auto |
|
1071 |
||
1072 |
lemma "bool_rec x y False = y" |
|
1073 |
nitpick [card = 2, expect = none] |
|
1074 |
by auto |
|
1075 |
||
1076 |
lemma "(x\<Colon>bool) = bool_rec x x True" |
|
1077 |
nitpick [card = 2, expect = none] |
|
1078 |
by auto |
|
1079 |
||
1080 |
lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')" |
|
1081 |
nitpick [expect = none] |
|
1082 |
sorry |
|
1083 |
||
1084 |
end |