src/HOL/ex/Quickcheck_Examples.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 45118 7462f287189a child 45441 fb4ac1dd4fde permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (*  Title:      HOL/ex/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
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 = 4, 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 '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 '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 {* Examples with quantifiers *}
250 text {*
251   These examples show that we can handle quantifiers.
252 *}
254 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
255   quickcheck[random, expect = counterexample]
256   quickcheck[exhaustive, expect = counterexample]
257 oops
259 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
260   quickcheck[random, expect = counterexample]
261   quickcheck[expect = counterexample]
262 oops
264 lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
265   quickcheck[random, expect = counterexample]
266   quickcheck[expect = counterexample]
267 oops
270 subsection {* Examples with relations *}
272 lemma
273   "acyclic R ==> acyclic S ==> acyclic (R Un S)"
274 quickcheck[expect = counterexample]
275 oops
277 lemma
278   "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
279 quickcheck[expect = counterexample]
280 oops
283 subsection {* Examples with numerical types *}
285 text {*
286 Quickcheck supports the common types nat, int, rat and real.
287 *}
289 lemma
290   "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
291 quickcheck[exhaustive, size = 10, expect = counterexample]
292 quickcheck[random, size = 10]
293 oops
295 lemma
296   "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
297 quickcheck[exhaustive, size = 10, expect = counterexample]
298 quickcheck[random, size = 10]
299 oops
301 lemma
302   "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
303 quickcheck[exhaustive, size = 10, expect = counterexample]
304 quickcheck[random, size = 10]
305 oops
307 lemma
308   "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
309 quickcheck[exhaustive, size = 10, expect = counterexample]
310 quickcheck[random, size = 10]
311 oops
313 subsubsection {* floor and ceiling functions *}
315 lemma
316   "floor x + floor y = floor (x + y :: rat)"
317 quickcheck[expect = counterexample]
318 oops
320 lemma
321   "floor x + floor y = floor (x + y :: real)"
322 quickcheck[expect = counterexample]
323 oops
325 lemma
326   "ceiling x + ceiling y = ceiling (x + y :: rat)"
327 quickcheck[expect = counterexample]
328 oops
330 lemma
331   "ceiling x + ceiling y = ceiling (x + y :: real)"
332 quickcheck[expect = counterexample]
333 oops
336 subsection {* Examples with Records *}
338 record point =
339   xpos :: nat
340   ypos :: nat
342 lemma
343   "xpos r = xpos r' ==> r = r'"
344 quickcheck[exhaustive, expect = counterexample]
345 quickcheck[random, expect = counterexample]
346 oops
348 datatype colour = Red | Green | Blue
350 record cpoint = point +
351   colour :: colour
353 lemma
354   "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
355 quickcheck[exhaustive, expect = counterexample]
356 quickcheck[random, expect = counterexample]
357 oops
359 subsection {* Examples with locales *}
361 locale Truth
363 context Truth
364 begin
366 lemma "False"
367 quickcheck[exhaustive, expect = no_counterexample]
368 oops
370 end
372 interpretation Truth .
374 context Truth
375 begin
377 lemma "False"
378 quickcheck[exhaustive, expect = counterexample]
379 oops
381 end
383 end