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