src/HOL/Nitpick_Examples/Manual_Nits.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 66453 cc19f7ca2ed6 child 67346 1f1d85393d70 permissions -rw-r--r--
tuned: each session has at most one defining entry;
1 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
2     Author:     Jasmin Blanchette, TU Muenchen
5 Examples from the Nitpick manual.
6 *)
8 section \<open>Examples from the Nitpick Manual\<close>
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 HOL.Real "HOL-Library.Quotient_Product"
16 begin
18 section \<open>2. First Steps\<close>
20 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
23 subsection \<open>2.1. Propositional Logic\<close>
25 lemma "P \<longleftrightarrow> Q"
26 nitpick [expect = genuine]
27 apply auto
28 nitpick [expect = genuine] 1
29 nitpick [expect = genuine] 2
30 oops
33 subsection \<open>2.2. Type Variables\<close>
35 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
36 nitpick [verbose, expect = genuine]
37 oops
40 subsection \<open>2.3. Constants\<close>
42 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
43 nitpick [show_consts, expect = genuine]
44 nitpick [dont_specialize, show_consts, expect = genuine]
45 oops
47 lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
48 nitpick [expect = none]
49 nitpick [card 'a = 1-50, expect = none]
50 (* sledgehammer *)
51 by (metis the_equality)
54 subsection \<open>2.4. Skolemization\<close>
56 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
57 nitpick [expect = genuine]
58 oops
60 lemma "\<exists>x. \<forall>f. f x = x"
61 nitpick [expect = genuine]
62 oops
64 lemma "refl r \<Longrightarrow> sym r"
65 nitpick [expect = genuine]
66 oops
69 subsection \<open>2.5. Natural Numbers and Integers\<close>
71 lemma "\<lbrakk>i \<le> j; n \<le> (m::int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
72 nitpick [expect = genuine]
73 nitpick [binary_ints, bits = 16, expect = genuine]
74 oops
76 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
77 nitpick [card nat = 100, expect = potential]
78 oops
80 lemma "P Suc"
81 nitpick [expect = none]
82 oops
84 lemma "P (op +::nat\<Rightarrow>nat\<Rightarrow>nat)"
85 nitpick [card nat = 1, expect = genuine]
86 nitpick [card nat = 2, expect = none]
87 oops
90 subsection \<open>2.6. Inductive Datatypes\<close>
92 lemma "hd (xs @ [y, y]) = hd xs"
93 nitpick [expect = genuine]
94 nitpick [show_consts, show_types, expect = genuine]
95 oops
97 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
98 nitpick [show_types, expect = genuine]
99 oops
102 subsection \<open>2.7. Typedefs, Records, Rationals, and Reals\<close>
104 definition "three = {0::nat, 1, 2}"
105 typedef three = three
106   unfolding three_def by blast
108 definition A :: three where "A \<equiv> Abs_three 0"
109 definition B :: three where "B \<equiv> Abs_three 1"
110 definition C :: three where "C \<equiv> Abs_three 2"
112 lemma "\<lbrakk>A \<in> X; B \<in> X\<rbrakk> \<Longrightarrow> c \<in> X"
113 nitpick [show_types, expect = genuine]
114 oops
116 fun my_int_rel where
117 "my_int_rel (x, y) (u, v) = (x + v = u + y)"
119 quotient_type my_int = "nat \<times> nat" / my_int_rel
120 by (auto simp add: equivp_def fun_eq_iff)
122 definition add_raw where
123 "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
125 quotient_definition "add::my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
126 unfolding add_raw_def by auto
128 lemma "add x y = add x x"
129 nitpick [show_types, expect = genuine]
130 oops
132 ML \<open>
133 fun my_int_postproc _ _ _ T (Const _ \$ (Const _ \$ t1 \$ t2)) =
134     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
135                          - snd (HOLogic.dest_number t2))
136   | my_int_postproc _ _ _ _ t = t
137 \<close>
139 declaration \<open>
140 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
141 \<close>
143 lemma "add x y = add x x"
144 nitpick [show_types]
145 oops
147 record point =
148   Xcoord :: int
149   Ycoord :: int
151 lemma "Xcoord (p::point) = Xcoord (q::point)"
152 nitpick [show_types, expect = genuine]
153 oops
155 lemma "4 * x + 3 * (y::real) \<noteq> 1 / 2"
156 nitpick [show_types, expect = genuine]
157 oops
160 subsection \<open>2.8. Inductive and Coinductive Predicates\<close>
162 inductive even where
163 "even 0" |
164 "even n \<Longrightarrow> even (Suc (Suc n))"
166 lemma "\<exists>n. even n \<and> even (Suc n)"
167 nitpick [card nat = 50, unary_ints, verbose, expect = potential]
168 oops
170 lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
171 nitpick [card nat = 50, unary_ints, expect = genuine]
172 oops
174 inductive even' where
175 "even' (0::nat)" |
176 "even' 2" |
177 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
179 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
180 nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine]
181 oops
183 lemma "even' (n - 2) \<Longrightarrow> even' n"
184 nitpick [card nat = 10, show_consts, expect = genuine]
185 oops
187 coinductive nats where
188 "nats (x::nat) \<Longrightarrow> nats x"
190 lemma "nats = (\<lambda>n. n \<in> {0, 1, 2, 3, 4})"
191 nitpick [card nat = 10, show_consts, expect = genuine]
192 oops
194 inductive odd where
195 "odd 1" |
196 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
198 lemma "odd n \<Longrightarrow> odd (n - 2)"
199 nitpick [card nat = 4, show_consts, expect = genuine]
200 oops
203 subsection \<open>2.9. Coinductive Datatypes\<close>
205 codatatype 'a llist = LNil | LCons 'a "'a llist"
207 primcorec iterates where
208 "iterates f a = LCons a (iterates f (f a))"
210 lemma "xs \<noteq> LCons a xs"
211 nitpick [expect = genuine]
212 oops
214 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
215 nitpick [verbose, expect = genuine]
216 oops
218 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
219 nitpick [bisim_depth = -1, show_types, expect = quasi_genuine]
220 nitpick [card = 1-5, expect = none]
221 sorry
224 subsection \<open>2.10. Boxing\<close>
226 datatype tm = Var nat | Lam tm | App tm tm
228 primrec lift where
229 "lift (Var j) k = Var (if j < k then j else j + 1)" |
230 "lift (Lam t) k = Lam (lift t (k + 1))" |
231 "lift (App t u) k = App (lift t k) (lift u k)"
233 primrec loose where
234 "loose (Var j) k = (j \<ge> k)" |
235 "loose (Lam t) k = loose t (Suc k)" |
236 "loose (App t u) k = (loose t k \<or> loose u k)"
238 primrec subst\<^sub>1 where
239 "subst\<^sub>1 \<sigma> (Var j) = \<sigma> j" |
240 "subst\<^sub>1 \<sigma> (Lam t) =
241  Lam (subst\<^sub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
242 "subst\<^sub>1 \<sigma> (App t u) = App (subst\<^sub>1 \<sigma> t) (subst\<^sub>1 \<sigma> u)"
244 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>1 \<sigma> t = t"
245 nitpick [verbose, expect = genuine]
246 nitpick [eval = "subst\<^sub>1 \<sigma> t", expect = genuine]
247 (* nitpick [dont_box, expect = unknown] *)
248 oops
250 primrec subst\<^sub>2 where
251 "subst\<^sub>2 \<sigma> (Var j) = \<sigma> j" |
252 "subst\<^sub>2 \<sigma> (Lam t) =
253  Lam (subst\<^sub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
254 "subst\<^sub>2 \<sigma> (App t u) = App (subst\<^sub>2 \<sigma> t) (subst\<^sub>2 \<sigma> u)"
256 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>2 \<sigma> t = t"
257 nitpick [card = 1-5, expect = none]
258 sorry
261 subsection \<open>2.11. Scope Monotonicity\<close>
263 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
264 nitpick [verbose, expect = genuine]
265 oops
267 lemma "\<exists>g. \<forall>x::'b. g (f x) = x \<Longrightarrow> \<forall>y::'a. \<exists>x. y = f x"
268 nitpick [mono, expect = none]
269 nitpick [expect = genuine]
270 oops
273 subsection \<open>2.12. Inductive Properties\<close>
275 inductive_set reach where
276 "(4::nat) \<in> reach" |
277 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
278 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
280 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
281 (* nitpick *)
282 apply (induct set: reach)
283   apply auto
284  nitpick [card = 1-4, bits = 1-4, expect = none]
285  apply (thin_tac "n \<in> reach")
286  nitpick [expect = genuine]
287 oops
289 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
290 (* nitpick *)
291 apply (induct set: reach)
292   apply auto
293  nitpick [card = 1-4, bits = 1-4, expect = none]
294  apply (thin_tac "n \<in> reach")
295  nitpick [expect = genuine]
296 oops
298 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
299 by (induct set: reach) arith+
302 section \<open>3. Case Studies\<close>
304 nitpick_params [max_potential = 0]
307 subsection \<open>3.1. A Context-Free Grammar\<close>
309 datatype alphabet = a | b
311 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
312   "[] \<in> S\<^sub>1"
313 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
314 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"
315 | "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1"
316 | "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
317 | "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
319 theorem S\<^sub>1_sound:
320 "w \<in> S\<^sub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
321 nitpick [expect = genuine]
322 oops
324 inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where
325   "[] \<in> S\<^sub>2"
326 | "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2"
327 | "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2"
328 | "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2"
329 | "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2"
330 | "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
332 theorem S\<^sub>2_sound:
333 "w \<in> S\<^sub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
334 nitpick [expect = genuine]
335 oops
337 inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
338   "[] \<in> S\<^sub>3"
339 | "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3"
340 | "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3"
341 | "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3"
342 | "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3"
343 | "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
345 theorem S\<^sub>3_sound:
346 "w \<in> S\<^sub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
347 nitpick [card = 1-5, expect = none]
348 sorry
350 theorem S\<^sub>3_complete:
351 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
352 nitpick [expect = genuine]
353 oops
355 inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where
356   "[] \<in> S\<^sub>4"
357 | "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4"
358 | "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4"
359 | "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4"
360 | "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4"
361 | "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4"
362 | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
364 theorem S\<^sub>4_sound:
365 "w \<in> S\<^sub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
366 nitpick [card = 1-5, expect = none]
367 sorry
369 theorem S\<^sub>4_complete:
370 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
371 nitpick [card = 1-5, expect = none]
372 sorry
374 theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
375 "w \<in> S\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
376 "w \<in> A\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
377 "w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
378 nitpick [card = 1-5, expect = none]
379 sorry
382 subsection \<open>3.2. AA Trees\<close>
384 datatype 'a aa_tree = \<Lambda> | N "'a::linorder" nat "'a aa_tree" "'a aa_tree"
386 primrec data where
387 "data \<Lambda> = undefined" |
388 "data (N x _ _ _) = x"
390 primrec dataset where
391 "dataset \<Lambda> = {}" |
392 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
394 primrec level where
395 "level \<Lambda> = 0" |
396 "level (N _ k _ _) = k"
398 primrec left where
399 "left \<Lambda> = \<Lambda>" |
400 "left (N _ _ t\<^sub>1 _) = t\<^sub>1"
402 primrec right where
403 "right \<Lambda> = \<Lambda>" |
404 "right (N _ _ _ t\<^sub>2) = t\<^sub>2"
406 fun wf where
407 "wf \<Lambda> = True" |
408 "wf (N _ k t u) =
409  (if t = \<Lambda> then
410     k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
411   else
412     wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
414 fun skew where
415 "skew \<Lambda> = \<Lambda>" |
416 "skew (N x k t u) =
417  (if t \<noteq> \<Lambda> \<and> k = level t then
418     N (data t) k (left t) (N x k (right t) u)
419   else
420     N x k t u)"
422 fun split where
423 "split \<Lambda> = \<Lambda>" |
424 "split (N x k t u) =
425  (if u \<noteq> \<Lambda> \<and> k = level (right u) then
426     N (data u) (Suc k) (N x k t (left u)) (right u)
427   else
428     N x k t u)"
430 theorem dataset_skew_split:
431 "dataset (skew t) = dataset t"
432 "dataset (split t) = dataset t"
433 nitpick [card = 1-5, expect = none]
434 sorry
436 theorem wf_skew_split:
437 "wf t \<Longrightarrow> skew t = t"
438 "wf t \<Longrightarrow> split t = t"
439 nitpick [card = 1-5, expect = none]
440 sorry
442 primrec insort\<^sub>1 where
443 "insort\<^sub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
444 "insort\<^sub>1 (N y k t u) x =
445  (* (split \<circ> skew) *) (N y k (if x < y then insort\<^sub>1 t x else t)
446                              (if x > y then insort\<^sub>1 u x else u))"
448 theorem wf_insort\<^sub>1: "wf t \<Longrightarrow> wf (insort\<^sub>1 t x)"
449 nitpick [expect = genuine]
450 oops
452 theorem wf_insort\<^sub>1_nat: "wf t \<Longrightarrow> wf (insort\<^sub>1 t (x::nat))"
453 nitpick [eval = "insort\<^sub>1 t x", expect = genuine]
454 oops
456 primrec insort\<^sub>2 where
457 "insort\<^sub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
458 "insort\<^sub>2 (N y k t u) x =
459  (split \<circ> skew) (N y k (if x < y then insort\<^sub>2 t x else t)
460                        (if x > y then insort\<^sub>2 u x else u))"
462 theorem wf_insort\<^sub>2: "wf t \<Longrightarrow> wf (insort\<^sub>2 t x)"
463 nitpick [card = 1-5, expect = none]
464 sorry
466 theorem dataset_insort\<^sub>2: "dataset (insort\<^sub>2 t x) = {x} \<union> dataset t"
467 nitpick [card = 1-5, expect = none]
468 sorry
470 end