src/HOL/Nitpick_Examples/Manual_Nits.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 46162 1148fab5104e child 47092 fa3538d6004b permissions -rw-r--r--
1 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
2     Author:     Jasmin Blanchette, TU Muenchen
5 Examples from the Nitpick manual.
6 *)
8 header {* Examples from the Nitpick Manual *}
10 (* The "expect" arguments to Nitpick in this theory and the other example
11    theories are there so that the example can also serve as a regression test
12    suite. *)
14 theory Manual_Nits
15 imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
16 begin
18 chapter {* 2. First Steps *}
20 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
22 subsection {* 2.1. Propositional Logic *}
24 lemma "P \<longleftrightarrow> Q"
25 nitpick [expect = genuine]
26 apply auto
27 nitpick [expect = genuine] 1
28 nitpick [expect = genuine] 2
29 oops
31 subsection {* 2.2. Type Variables *}
33 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
34 nitpick [verbose, expect = genuine]
35 oops
37 subsection {* 2.3. Constants *}
39 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
40 nitpick [show_consts, expect = genuine]
41 nitpick [dont_specialize, show_consts, expect = genuine]
42 oops
44 lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
45 nitpick [expect = none]
46 nitpick [card 'a = 1\<emdash>50, expect = none]
47 (* sledgehammer *)
48 by (metis the_equality)
50 subsection {* 2.4. Skolemization *}
52 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
53 nitpick [expect = genuine]
54 oops
56 lemma "\<exists>x. \<forall>f. f x = x"
57 nitpick [expect = genuine]
58 oops
60 lemma "refl r \<Longrightarrow> sym r"
61 nitpick [expect = genuine]
62 oops
64 subsection {* 2.5. Natural Numbers and Integers *}
66 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
67 nitpick [expect = genuine]
68 nitpick [binary_ints, bits = 16, expect = genuine]
69 oops
71 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
72 nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine]
73 oops
75 lemma "P Suc"
76 nitpick [expect = none]
77 oops
79 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
80 nitpick [card nat = 1, expect = genuine]
81 nitpick [card nat = 2, expect = none]
82 oops
84 subsection {* 2.6. Inductive Datatypes *}
86 lemma "hd (xs @ [y, y]) = hd xs"
87 nitpick [expect = genuine]
88 nitpick [show_consts, show_datatypes, expect = genuine]
89 oops
91 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
92 nitpick [show_datatypes, expect = genuine]
93 oops
95 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
97 typedef three = "{0\<Colon>nat, 1, 2}"
98 by blast
100 definition A :: three where "A \<equiv> Abs_three 0"
101 definition B :: three where "B \<equiv> Abs_three 1"
102 definition C :: three where "C \<equiv> Abs_three 2"
104 lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X"
105 nitpick [show_datatypes, expect = genuine]
106 oops
108 fun my_int_rel where
109 "my_int_rel (x, y) (u, v) = (x + v = u + y)"
111 quotient_type my_int = "nat \<times> nat" / my_int_rel
112 by (auto simp add: equivp_def fun_eq_iff)
115 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
120 nitpick [show_datatypes, expect = genuine]
121 oops
123 ML {*
124 fun my_int_postproc _ _ _ T (Const _ \$ (Const _ \$ t1 \$ t2)) =
125     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
126                          - snd (HOLogic.dest_number t2))
127   | my_int_postproc _ _ _ _ t = t
128 *}
130 declaration {*
131 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
132 *}
135 nitpick [show_datatypes]
136 oops
138 record point =
139   Xcoord :: int
140   Ycoord :: int
142 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
143 nitpick [show_datatypes, expect = genuine]
144 oops
146 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
147 nitpick [show_datatypes, expect = genuine]
148 oops
150 subsection {* 2.8. Inductive and Coinductive Predicates *}
152 inductive even where
153 "even 0" |
154 "even n \<Longrightarrow> even (Suc (Suc n))"
156 lemma "\<exists>n. even n \<and> even (Suc n)"
157 nitpick [card nat = 50, unary_ints, verbose, expect = potential]
158 oops
160 lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
161 nitpick [card nat = 50, unary_ints, expect = genuine]
162 oops
164 inductive even' where
165 "even' (0\<Colon>nat)" |
166 "even' 2" |
167 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
169 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
170 nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
171 oops
173 lemma "even' (n - 2) \<Longrightarrow> even' n"
174 nitpick [card nat = 10, show_consts, expect = genuine]
175 oops
177 coinductive nats where
178 "nats (x\<Colon>nat) \<Longrightarrow> nats x"
180 lemma "nats = (\<lambda>n. n \<in> {0, 1, 2, 3, 4})"
181 nitpick [card nat = 10, show_consts, expect = genuine]
182 oops
184 inductive odd where
185 "odd 1" |
186 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
188 lemma "odd n \<Longrightarrow> odd (n - 2)"
189 nitpick [card nat = 4, show_consts, expect = genuine]
190 oops
192 subsection {* 2.9. Coinductive Datatypes *}
194 (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
195    we cannot rely on its presence, we expediently provide our own
196    axiomatization. The examples also work unchanged with Lochbihler's
197    "Coinductive_List" theory. *)
199 (* BEGIN LAZY LIST SETUP *)
200 definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
202 typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
203 unfolding llist_def by auto
205 definition LNil where
206 "LNil = Abs_llist (Inl [])"
207 definition LCons where
208 "LCons y ys = Abs_llist (case Rep_llist ys of
209                            Inl ys' \<Rightarrow> Inl (y # ys')
210                          | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
212 axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
214 lemma iterates_def [nitpick_simp]:
215 "iterates f a = LCons a (iterates f (f a))"
216 sorry
218 declaration {*
219 Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
220     (map dest_Const [@{term LNil}, @{term LCons}])
221 *}
222 (* END LAZY LIST SETUP *)
224 lemma "xs \<noteq> LCons a xs"
225 nitpick [expect = genuine]
226 oops
228 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
229 nitpick [verbose, expect = genuine]
230 oops
232 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
233 nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine]
234 nitpick [card = 1\<emdash>5, expect = none]
235 sorry
237 subsection {* 2.10. Boxing *}
239 datatype tm = Var nat | Lam tm | App tm tm
241 primrec lift where
242 "lift (Var j) k = Var (if j < k then j else j + 1)" |
243 "lift (Lam t) k = Lam (lift t (k + 1))" |
244 "lift (App t u) k = App (lift t k) (lift u k)"
246 primrec loose where
247 "loose (Var j) k = (j \<ge> k)" |
248 "loose (Lam t) k = loose t (Suc k)" |
249 "loose (App t u) k = (loose t k \<or> loose u k)"
251 primrec subst\<^isub>1 where
252 "subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
253 "subst\<^isub>1 \<sigma> (Lam t) =
254  Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
255 "subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
257 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
258 nitpick [verbose, expect = genuine]
259 nitpick [eval = "subst\<^isub>1 \<sigma> t", expect = genuine]
260 (* nitpick [dont_box, expect = unknown] *)
261 oops
263 primrec subst\<^isub>2 where
264 "subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
265 "subst\<^isub>2 \<sigma> (Lam t) =
266  Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
267 "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
269 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
270 nitpick [card = 1\<emdash>5, expect = none]
271 sorry
273 subsection {* 2.11. Scope Monotonicity *}
275 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
276 nitpick [verbose, expect = genuine]
277 oops
279 lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
280 nitpick [mono, expect = none]
281 nitpick [expect = genuine]
282 oops
284 subsection {* 2.12. Inductive Properties *}
286 inductive_set reach where
287 "(4\<Colon>nat) \<in> reach" |
288 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
289 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
291 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
292 (* nitpick *)
293 apply (induct set: reach)
294   apply auto
295  nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
296  apply (thin_tac "n \<in> reach")
297  nitpick [expect = genuine]
298 oops
300 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
301 (* nitpick *)
302 apply (induct set: reach)
303   apply auto
304  nitpick [card = 1\<emdash>4, bits = 1\<emdash>4, expect = none]
305  apply (thin_tac "n \<in> reach")
306  nitpick [expect = genuine]
307 oops
309 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
310 by (induct set: reach) arith+
312 datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
314 primrec labels where
315 "labels (Leaf a) = {a}" |
316 "labels (Branch t u) = labels t \<union> labels u"
318 primrec swap where
319 "swap (Leaf c) a b =
320  (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
321 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
323 lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
324 (* nitpick *)
325 proof (induct t)
326   case Leaf thus ?case by simp
327 next
328   case (Branch t u) thus ?case
329   (* nitpick *)
330   nitpick [non_std, show_all, expect = genuine]
331 oops
333 lemma "labels (swap t a b) =
334        (if a \<in> labels t then
335           if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
336         else
337           if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
338 (* nitpick *)
339 proof (induct t)
340   case Leaf thus ?case by simp
341 next
342   case (Branch t u) thus ?case
343   nitpick [non_std, card = 1\<emdash>4, expect = none]
344   by auto
345 qed
347 section {* 3. Case Studies *}
349 nitpick_params [max_potential = 0]
351 subsection {* 3.1. A Context-Free Grammar *}
353 datatype alphabet = a | b
355 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
356   "[] \<in> S\<^isub>1"
357 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
358 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
359 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
360 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
361 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
363 theorem S\<^isub>1_sound:
364 "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
365 nitpick [expect = genuine]
366 oops
368 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
369   "[] \<in> S\<^isub>2"
370 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
371 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
372 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
373 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
374 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
376 theorem S\<^isub>2_sound:
377 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
378 nitpick [expect = genuine]
379 oops
381 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
382   "[] \<in> S\<^isub>3"
383 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
384 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
385 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
386 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
387 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
389 theorem S\<^isub>3_sound:
390 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
391 nitpick [card = 1\<emdash>5, expect = none]
392 sorry
394 theorem S\<^isub>3_complete:
395 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
396 nitpick [expect = genuine]
397 oops
399 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
400   "[] \<in> S\<^isub>4"
401 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
402 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
403 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
404 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
405 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
406 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
408 theorem S\<^isub>4_sound:
409 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
410 nitpick [card = 1\<emdash>5, expect = none]
411 sorry
413 theorem S\<^isub>4_complete:
414 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
415 nitpick [card = 1\<emdash>5, expect = none]
416 sorry
418 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
419 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
420 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
421 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
422 nitpick [card = 1\<emdash>5, expect = none]
423 sorry
425 subsection {* 3.2. AA Trees *}
427 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
429 primrec data where
430 "data \<Lambda> = undefined" |
431 "data (N x _ _ _) = x"
433 primrec dataset where
434 "dataset \<Lambda> = {}" |
435 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
437 primrec level where
438 "level \<Lambda> = 0" |
439 "level (N _ k _ _) = k"
441 primrec left where
442 "left \<Lambda> = \<Lambda>" |
443 "left (N _ _ t\<^isub>1 _) = t\<^isub>1"
445 primrec right where
446 "right \<Lambda> = \<Lambda>" |
447 "right (N _ _ _ t\<^isub>2) = t\<^isub>2"
449 fun wf where
450 "wf \<Lambda> = True" |
451 "wf (N _ k t u) =
452  (if t = \<Lambda> then
453     k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
454   else
455     wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
457 fun skew where
458 "skew \<Lambda> = \<Lambda>" |
459 "skew (N x k t u) =
460  (if t \<noteq> \<Lambda> \<and> k = level t then
461     N (data t) k (left t) (N x k (right t) u)
462   else
463     N x k t u)"
465 fun split where
466 "split \<Lambda> = \<Lambda>" |
467 "split (N x k t u) =
468  (if u \<noteq> \<Lambda> \<and> k = level (right u) then
469     N (data u) (Suc k) (N x k t (left u)) (right u)
470   else
471     N x k t u)"
473 theorem dataset_skew_split:
474 "dataset (skew t) = dataset t"
475 "dataset (split t) = dataset t"
476 nitpick [card = 1\<emdash>5, expect = none]
477 sorry
479 theorem wf_skew_split:
480 "wf t \<Longrightarrow> skew t = t"
481 "wf t \<Longrightarrow> split t = t"
482 nitpick [card = 1\<emdash>5, expect = none]
483 sorry
485 primrec insort\<^isub>1 where
486 "insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
487 "insort\<^isub>1 (N y k t u) x =
488  (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
489                              (if x > y then insort\<^isub>1 u x else u))"
491 theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
492 nitpick [expect = genuine]
493 oops
495 theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
496 nitpick [eval = "insort\<^isub>1 t x", expect = genuine]
497 oops
499 primrec insort\<^isub>2 where
500 "insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
501 "insort\<^isub>2 (N y k t u) x =
502  (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
503                        (if x > y then insort\<^isub>2 u x else u))"
505 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
506 nitpick [card = 1\<emdash>5, expect = none]
507 sorry
509 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
510 nitpick [card = 1\<emdash>5, expect = none]
511 sorry
513 end