src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 58148 9764b994a421 child 58310 91ea607a34d8 permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
2     Author:     Stefan Berghofer, Lukas Bulwahn
3     Copyright   2004 - 2010 TU Muenchen
4 *)
6 header {* Examples for the 'quickcheck' command *}
8 theory Quickcheck_Examples
9 imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
10 begin
12 text {*
13 The 'quickcheck' command allows to find counterexamples by evaluating
14 formulae.
15 Currently, there are two different exploration schemes:
16 - random testing: this is incomplete, but explores the search space faster.
17 - exhaustive testing: this is complete, but increasing the depth leads to
18   exponentially many assignments.
20 quickcheck can handle quantifiers on finite universes.
22 *}
24 declare [[quickcheck_timeout = 3600]]
26 subsection {* Lists *}
28 theorem "map g (map f xs) = map (g o f) xs"
29   quickcheck[random, expect = no_counterexample]
30   quickcheck[exhaustive, size = 3, expect = no_counterexample]
31   oops
33 theorem "map g (map f xs) = map (f o g) xs"
34   quickcheck[random, expect = counterexample]
35   quickcheck[exhaustive, expect = counterexample]
36   oops
38 theorem "rev (xs @ ys) = rev ys @ rev xs"
39   quickcheck[random, expect = no_counterexample]
40   quickcheck[exhaustive, expect = no_counterexample]
41   quickcheck[exhaustive, size = 1000, timeout = 0.1]
42   oops
44 theorem "rev (xs @ ys) = rev xs @ rev ys"
45   quickcheck[random, expect = counterexample]
46   quickcheck[exhaustive, expect = counterexample]
47   oops
49 theorem "rev (rev xs) = xs"
50   quickcheck[random, expect = no_counterexample]
51   quickcheck[exhaustive, expect = no_counterexample]
52   oops
54 theorem "rev xs = xs"
55   quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
56   quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
57   quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
58   quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
59   quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
60   quickcheck[tester = exhaustive, finite_types = false, expect = counterexample]
61 oops
64 text {* An example involving functions inside other data structures *}
66 primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
67   "app [] x = x"
68   | "app (f # fs) x = app fs (f x)"
70 lemma "app (fs @ gs) x = app gs (app fs x)"
71   quickcheck[random, expect = no_counterexample]
72   quickcheck[exhaustive, size = 2, expect = no_counterexample]
73   by (induct fs arbitrary: x) simp_all
75 lemma "app (fs @ gs) x = app fs (app gs x)"
76   quickcheck[random, expect = counterexample]
77   quickcheck[exhaustive, expect = counterexample]
78   oops
80 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
81   "occurs a [] = 0"
82   | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
84 primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
85   "del1 a [] = []"
86   | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
88 text {* A lemma, you'd think to be true from our experience with delAll *}
89 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
90   -- {* Wrong. Precondition needed.*}
91   quickcheck[random, expect = counterexample]
92   quickcheck[exhaustive, expect = counterexample]
93   oops
95 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
96   quickcheck[random, expect = counterexample]
97   quickcheck[exhaustive, expect = counterexample]
98     -- {* Also wrong.*}
99   oops
101 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
102   quickcheck[random, expect = no_counterexample]
103   quickcheck[exhaustive, expect = no_counterexample]
104   by (induct xs) auto
106 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
107   "replace a b [] = []"
108   | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
109                             else (x#(replace a b xs)))"
111 lemma "occurs a xs = occurs b (replace a b xs)"
112   quickcheck[random, expect = counterexample]
113   quickcheck[exhaustive, expect = counterexample]
114   -- {* Wrong. Precondition needed.*}
115   oops
117 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
118   quickcheck[random, expect = no_counterexample]
119   quickcheck[exhaustive, expect = no_counterexample]
120   by (induct xs) simp_all
123 subsection {* Trees *}
125 datatype_new 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
127 primrec leaves :: "'a tree \<Rightarrow> 'a list" where
128   "leaves Twig = []"
129   | "leaves (Leaf a) = [a]"
130   | "leaves (Branch l r) = (leaves l) @ (leaves r)"
132 primrec plant :: "'a list \<Rightarrow> 'a tree" where
133   "plant [] = Twig "
134   | "plant (x#xs) = Branch (Leaf x) (plant xs)"
136 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
137   "mirror (Twig) = Twig "
138   | "mirror (Leaf a) = Leaf a "
139   | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
141 theorem "plant (rev (leaves xt)) = mirror xt"
142   quickcheck[random, expect = counterexample]
143   quickcheck[exhaustive, expect = counterexample]
144     --{* Wrong! *}
145   oops
147 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
148   quickcheck[random, expect = counterexample]
149   quickcheck[exhaustive, expect = counterexample]
150     --{* Wrong! *}
151   oops
153 datatype_new 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
155 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
156   "inOrder (Tip a)= [a]"
157   | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
159 primrec root :: "'a ntree \<Rightarrow> 'a" where
160   "root (Tip a) = a"
161   | "root (Node f x y) = f"
163 theorem "hd (inOrder xt) = root xt"
164   quickcheck[random, expect = counterexample]
165   quickcheck[exhaustive, expect = counterexample]
166   --{* Wrong! *}
167   oops
170 subsection {* Exhaustive Testing beats Random Testing *}
172 text {* Here are some examples from mutants from the List theory
173 where exhaustive testing beats random testing *}
175 lemma
176   "[] ~= xs ==> hd xs = last (x # xs)"
177 quickcheck[random]
178 quickcheck[exhaustive, expect = counterexample]
179 oops
181 lemma
182   assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
183   shows "drop n xs = takeWhile P xs"
184 quickcheck[random, iterations = 10000, quiet]
185 quickcheck[exhaustive, expect = counterexample]
186 oops
188 lemma
189   "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
190 quickcheck[random, iterations = 10000]
191 quickcheck[exhaustive, expect = counterexample]
192 oops
194 lemma
195   "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
196 quickcheck[random, iterations = 10000, finite_types = false]
197 quickcheck[exhaustive, finite_types = false, expect = counterexample]
198 oops
200 lemma
201   "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
202 quickcheck[random, iterations = 10000, finite_types = false]
203 quickcheck[exhaustive, finite_types = false, expect = counterexample]
204 oops
206 lemma
207   "ns ! k < length ns ==> k <= listsum ns"
208 quickcheck[random, iterations = 10000, finite_types = false, quiet]
209 quickcheck[exhaustive, finite_types = false, expect = counterexample]
210 oops
212 lemma
213   "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
214 quickcheck[random, iterations = 10000]
215 quickcheck[exhaustive, expect = counterexample]
216 oops
218 lemma
219 "i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
220 quickcheck[random, iterations = 10000]
221 quickcheck[exhaustive, expect = counterexample]
222 oops
224 lemma
225   "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
226 quickcheck[random, iterations = 10000]
227 quickcheck[exhaustive, expect = counterexample]
228 oops
230 lemma
231   "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
232 quickcheck[random]
233 quickcheck[exhaustive, expect = counterexample]
234 oops
236 lemma
237   "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
238 quickcheck[random]
239 quickcheck[exhaustive, expect = counterexample]
240 oops
242 lemma
243   "(ys = zs) = (xs @ ys = splice xs zs)"
244 quickcheck[random]
245 quickcheck[exhaustive, expect = counterexample]
246 oops
248 subsection {* Random Testing beats Exhaustive Testing *}
250 lemma mult_inj_if_coprime_nat:
251   "inj_on f A \<Longrightarrow> inj_on g B
252    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
253 quickcheck[exhaustive]
254 quickcheck[random]
255 oops
257 subsection {* Examples with quantifiers *}
259 text {*
260   These examples show that we can handle quantifiers.
261 *}
263 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
264   quickcheck[random, expect = counterexample]
265   quickcheck[exhaustive, expect = counterexample]
266 oops
268 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
269   quickcheck[random, expect = counterexample]
270   quickcheck[expect = counterexample]
271 oops
273 lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
274   quickcheck[random, expect = counterexample]
275   quickcheck[expect = counterexample]
276 oops
279 subsection {* Examples with sets *}
281 lemma
282   "{} = A Un - A"
283 quickcheck[exhaustive, expect = counterexample]
284 oops
286 lemma
287   "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
288 quickcheck[exhaustive, expect = counterexample]
289 oops
292 subsection {* Examples with relations *}
294 lemma
295   "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)"
296 quickcheck[exhaustive, expect = counterexample]
297 oops
299 lemma
300   "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)"
301 quickcheck[exhaustive, expect = counterexample]
302 oops
304 (* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *)
305 lemma
306   "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
307 (*quickcheck[exhaustive, expect = counterexample]*)
308 oops
310 lemma
311   "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)"
312 quickcheck[exhaustive, expect = counterexample]
313 oops
315 lemma
316   "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)"
317 quickcheck[exhaustive, expect = counterexample]
318 oops
320 lemma
321   "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)"
322 quickcheck[exhaustive, expect = counterexample]
323 oops
326 subsection {* Examples with the descriptive operator *}
328 lemma
329   "(THE x. x = a) = b"
330 quickcheck[random, expect = counterexample]
331 quickcheck[exhaustive, expect = counterexample]
332 oops
334 subsection {* Examples with Multisets *}
336 lemma
337   "X + Y = Y + (Z :: 'a multiset)"
338 quickcheck[random, expect = counterexample]
339 quickcheck[exhaustive, expect = counterexample]
340 oops
342 lemma
343   "X - Y = Y - (Z :: 'a multiset)"
344 quickcheck[random, expect = counterexample]
345 quickcheck[exhaustive, expect = counterexample]
346 oops
348 lemma
349   "N + M - N = (N::'a multiset)"
350 quickcheck[random, expect = counterexample]
351 quickcheck[exhaustive, expect = counterexample]
352 oops
354 subsection {* Examples with numerical types *}
356 text {*
357 Quickcheck supports the common types nat, int, rat and real.
358 *}
360 lemma
361   "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
362 quickcheck[exhaustive, size = 10, expect = counterexample]
363 quickcheck[random, size = 10]
364 oops
366 lemma
367   "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
368 quickcheck[exhaustive, size = 10, expect = counterexample]
369 quickcheck[random, size = 10]
370 oops
372 lemma
373   "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
374 quickcheck[exhaustive, size = 10, expect = counterexample]
375 quickcheck[random, size = 10]
376 oops
378 lemma "(x :: rat) >= 0"
379 quickcheck[random, expect = counterexample]
380 quickcheck[exhaustive, expect = counterexample]
381 oops
383 lemma
384   "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
385 quickcheck[exhaustive, size = 10, expect = counterexample]
386 quickcheck[random, size = 10]
387 oops
389 lemma "(x :: real) >= 0"
390 quickcheck[random, expect = counterexample]
391 quickcheck[exhaustive, expect = counterexample]
392 oops
394 subsubsection {* floor and ceiling functions *}
396 lemma
397   "floor x + floor y = floor (x + y :: rat)"
398 quickcheck[expect = counterexample]
399 oops
401 lemma
402   "floor x + floor y = floor (x + y :: real)"
403 quickcheck[expect = counterexample]
404 oops
406 lemma
407   "ceiling x + ceiling y = ceiling (x + y :: rat)"
408 quickcheck[expect = counterexample]
409 oops
411 lemma
412   "ceiling x + ceiling y = ceiling (x + y :: real)"
413 quickcheck[expect = counterexample]
414 oops
416 subsection {* Examples with abstract types *}
418 lemma
419   "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
420 quickcheck[exhaustive]
421 quickcheck[random]
422 oops
424 lemma
425   "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
426 quickcheck[exhaustive]
427 quickcheck[random]
428 oops
430 subsection {* Examples with Records *}
432 record point =
433   xpos :: nat
434   ypos :: nat
436 lemma
437   "xpos r = xpos r' ==> r = r'"
438 quickcheck[exhaustive, expect = counterexample]
439 quickcheck[random, expect = counterexample]
440 oops
442 datatype_new colour = Red | Green | Blue
444 record cpoint = point +
445   colour :: colour
447 lemma
448   "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
449 quickcheck[exhaustive, expect = counterexample]
450 quickcheck[random, expect = counterexample]
451 oops
453 subsection {* Examples with locales *}
455 locale Truth
457 context Truth
458 begin
460 lemma "False"
461 quickcheck[exhaustive, expect = counterexample]
462 oops
464 end
466 interpretation Truth .
468 context Truth
469 begin
471 lemma "False"
472 quickcheck[exhaustive, expect = counterexample]
473 oops
475 end
477 locale antisym =
478   fixes R
479   assumes "R x y --> R y x --> x = y"
481 interpretation equal : antisym "op =" by default simp
482 interpretation order_nat : antisym "op <= :: nat => _ => _" by default simp
484 lemma (in antisym)
485   "R x y --> R y z --> R x z"
486 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
487 quickcheck[exhaustive, expect = counterexample]
488 oops
490 declare [[quickcheck_locale = "interpret"]]
492 lemma (in antisym)
493   "R x y --> R y z --> R x z"
494 quickcheck[exhaustive, expect = no_counterexample]
495 oops
497 declare [[quickcheck_locale = "expand"]]
499 lemma (in antisym)
500   "R x y --> R y z --> R x z"
501 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
502 quickcheck[exhaustive, expect = counterexample]
503 oops
506 subsection {* Examples with HOL quantifiers *}
508 lemma
509   "\<forall> xs ys. xs = [] --> xs = ys"
510 quickcheck[exhaustive, expect = counterexample]
511 oops
513 lemma
514   "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
515 quickcheck[exhaustive, expect = counterexample]
516 oops
518 lemma
519   "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
520 quickcheck[exhaustive, expect = counterexample]
521 oops
523 subsection {* Examples with underspecified/partial functions *}
525 lemma
526   "xs = [] ==> hd xs \<noteq> x"
527 quickcheck[exhaustive, expect = no_counterexample]
528 quickcheck[random, report = false, expect = no_counterexample]
529 quickcheck[random, report = true, expect = no_counterexample]
530 oops
532 lemma
533   "xs = [] ==> hd xs = x"
534 quickcheck[exhaustive, expect = no_counterexample]
535 quickcheck[random, report = false, expect = no_counterexample]
536 quickcheck[random, report = true, expect = no_counterexample]
537 oops
539 lemma "xs = [] ==> hd xs = x ==> x = y"
540 quickcheck[exhaustive, expect = no_counterexample]
541 quickcheck[random, report = false, expect = no_counterexample]
542 quickcheck[random, report = true, expect = no_counterexample]
543 oops
545 text {* with the simple testing scheme *}
547 setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
548 declare [[quickcheck_full_support = false]]
550 lemma
551   "xs = [] ==> hd xs \<noteq> x"
552 quickcheck[exhaustive, expect = no_counterexample]
553 oops
555 lemma
556   "xs = [] ==> hd xs = x"
557 quickcheck[exhaustive, expect = no_counterexample]
558 oops
560 lemma "xs = [] ==> hd xs = x ==> x = y"
561 quickcheck[exhaustive, expect = no_counterexample]
562 oops
564 declare [[quickcheck_full_support = true]]
567 subsection {* Equality Optimisation *}
569 lemma
570   "f x = y ==> y = (0 :: nat)"
571 quickcheck
572 oops
574 lemma
575   "y = f x ==> y = (0 :: nat)"
576 quickcheck
577 oops
579 lemma
580   "f y = zz # zzs ==> zz = (0 :: nat) \<and> zzs = []"
581 quickcheck
582 oops
584 lemma
585   "f y = x # x' # xs ==> x = (0 :: nat) \<and> x' = 0 \<and> xs = []"
586 quickcheck
587 oops
589 lemma
590   "x = f x \<Longrightarrow> x = (0 :: nat)"
591 quickcheck
592 oops
594 lemma
595   "f y = x # x # xs ==> x = (0 :: nat) \<and> xs = []"
596 quickcheck
597 oops
599 lemma
600   "m1 k = Some v \<Longrightarrow> (m1 ++ m2) k = Some v"
601 quickcheck
602 oops
605 end