src/HOL/ex/Quickcheck_Examples.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 44189 4a80017c733f child 45118 7462f287189a permissions -rw-r--r--
new isCont theorems;
simplify some proofs.
```     1 (*  Title:      HOL/ex/Quickcheck_Examples.thy
```
```     2     Author:     Stefan Berghofer, Lukas Bulwahn
```
```     3     Copyright   2004 - 2010 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 header {* Examples for the 'quickcheck' command *}
```
```     7
```
```     8 theory Quickcheck_Examples
```
```     9 imports Complex_Main
```
```    10 begin
```
```    11
```
```    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.
```
```    19
```
```    20 quickcheck can handle quantifiers on finite universes.
```
```    21
```
```    22 *}
```
```    23
```
```    24 declare [[quickcheck_timeout = 3600]]
```
```    25
```
```    26 subsection {* Lists *}
```
```    27
```
```    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
```
```    32
```
```    33 theorem "map g (map f xs) = map (f o g) xs"
```
```    34   quickcheck[random, expect = counterexample]
```
```    35   quickcheck[exhaustive, expect = counterexample]
```
```    36   oops
```
```    37
```
```    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
```
```    43
```
```    44 theorem "rev (xs @ ys) = rev xs @ rev ys"
```
```    45   quickcheck[random, expect = counterexample]
```
```    46   quickcheck[exhaustive, expect = counterexample]
```
```    47   oops
```
```    48
```
```    49 theorem "rev (rev xs) = xs"
```
```    50   quickcheck[random, expect = no_counterexample]
```
```    51   quickcheck[exhaustive, expect = no_counterexample]
```
```    52   oops
```
```    53
```
```    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
```
```    62
```
```    63
```
```    64 text {* An example involving functions inside other data structures *}
```
```    65
```
```    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)"
```
```    69
```
```    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
```
```    74
```
```    75 lemma "app (fs @ gs) x = app fs (app gs x)"
```
```    76   quickcheck[random, expect = counterexample]
```
```    77   quickcheck[exhaustive, expect = counterexample]
```
```    78   oops
```
```    79
```
```    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)"
```
```    83
```
```    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))"
```
```    87
```
```    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
```
```    94
```
```    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
```
```   100
```
```   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
```
```   105
```
```   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)))"
```
```   110
```
```   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
```
```   116
```
```   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
```
```   121
```
```   122
```
```   123 subsection {* Trees *}
```
```   124
```
```   125 datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
```
```   126
```
```   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)"
```
```   131
```
```   132 primrec plant :: "'a list \<Rightarrow> 'a tree" where
```
```   133   "plant [] = Twig "
```
```   134   | "plant (x#xs) = Branch (Leaf x) (plant xs)"
```
```   135
```
```   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)"
```
```   140
```
```   141 theorem "plant (rev (leaves xt)) = mirror xt"
```
```   142   quickcheck[random, expect = counterexample]
```
```   143   quickcheck[exhaustive, expect = counterexample]
```
```   144     --{* Wrong! *}
```
```   145   oops
```
```   146
```
```   147 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
```
```   148   quickcheck[random, expect = counterexample]
```
```   149   quickcheck[exhaustive, expect = counterexample]
```
```   150     --{* Wrong! *}
```
```   151   oops
```
```   152
```
```   153 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
```
```   154
```
```   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)"
```
```   158
```
```   159 primrec root :: "'a ntree \<Rightarrow> 'a" where
```
```   160   "root (Tip a) = a"
```
```   161   | "root (Node f x y) = f"
```
```   162
```
```   163 theorem "hd (inOrder xt) = root xt"
```
```   164   quickcheck[random, expect = counterexample]
```
```   165   quickcheck[exhaustive, expect = counterexample]
```
```   166   --{* Wrong! *}
```
```   167   oops
```
```   168
```
```   169
```
```   170 subsection {* Exhaustive Testing beats Random Testing *}
```
```   171
```
```   172 text {* Here are some examples from mutants from the List theory
```
```   173 where exhaustive testing beats random testing *}
```
```   174
```
```   175 lemma
```
```   176   "[] ~= xs ==> hd xs = last (x # xs)"
```
```   177 quickcheck[random]
```
```   178 quickcheck[exhaustive, expect = counterexample]
```
```   179 oops
```
```   180
```
```   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
```
```   187
```
```   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
```
```   193
```
```   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
```
```   199
```
```   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
```
```   205
```
```   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
```
```   211
```
```   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
```
```   217
```
```   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
```
```   223
```
```   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
```
```   229
```
```   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
```
```   235
```
```   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
```
```   241
```
```   242 lemma
```
```   243   "(ys = zs) = (xs @ ys = splice xs zs)"
```
```   244 quickcheck[random]
```
```   245 quickcheck[exhaustive, expect = counterexample]
```
```   246 oops
```
```   247
```
```   248 subsection {* Examples with quantifiers *}
```
```   249
```
```   250 text {*
```
```   251   These examples show that we can handle quantifiers.
```
```   252 *}
```
```   253
```
```   254 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
```
```   255   quickcheck[random, expect = counterexample]
```
```   256   quickcheck[exhaustive, expect = counterexample]
```
```   257 oops
```
```   258
```
```   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
```
```   263
```
```   264 lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
```
```   265   quickcheck[random, expect = counterexample]
```
```   266   quickcheck[expect = counterexample]
```
```   267 oops
```
```   268
```
```   269 subsection {* Examples with numerical types *}
```
```   270
```
```   271 text {*
```
```   272 Quickcheck supports the common types nat, int, rat and real.
```
```   273 *}
```
```   274
```
```   275 lemma
```
```   276   "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
```
```   277 quickcheck[exhaustive, size = 10, expect = counterexample]
```
```   278 quickcheck[random, size = 10]
```
```   279 oops
```
```   280
```
```   281 lemma
```
```   282   "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
```
```   283 quickcheck[exhaustive, size = 10, expect = counterexample]
```
```   284 quickcheck[random, size = 10]
```
```   285 oops
```
```   286
```
```   287 lemma
```
```   288   "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
```
```   289 quickcheck[exhaustive, size = 10, expect = counterexample]
```
```   290 quickcheck[random, size = 10]
```
```   291 oops
```
```   292
```
```   293 lemma
```
```   294   "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
```
```   295 quickcheck[exhaustive, size = 10, expect = counterexample]
```
```   296 quickcheck[random, size = 10]
```
```   297 oops
```
```   298
```
```   299 subsubsection {* floor and ceiling functions *}
```
```   300
```
```   301 lemma
```
```   302   "floor x + floor y = floor (x + y :: rat)"
```
```   303 quickcheck[expect = counterexample]
```
```   304 oops
```
```   305
```
```   306 lemma
```
```   307   "floor x + floor y = floor (x + y :: real)"
```
```   308 quickcheck[expect = counterexample]
```
```   309 oops
```
```   310
```
```   311 lemma
```
```   312   "ceiling x + ceiling y = ceiling (x + y :: rat)"
```
```   313 quickcheck[expect = counterexample]
```
```   314 oops
```
```   315
```
```   316 lemma
```
```   317   "ceiling x + ceiling y = ceiling (x + y :: real)"
```
```   318 quickcheck[expect = counterexample]
```
```   319 oops
```
```   320
```
```   321
```
```   322 subsection {* Examples with Records *}
```
```   323
```
```   324 record point =
```
```   325   xpos :: nat
```
```   326   ypos :: nat
```
```   327
```
```   328 lemma
```
```   329   "xpos r = xpos r' ==> r = r'"
```
```   330 quickcheck[exhaustive, expect = counterexample]
```
```   331 quickcheck[random, expect = counterexample]
```
```   332 oops
```
```   333
```
```   334 datatype colour = Red | Green | Blue
```
```   335
```
```   336 record cpoint = point +
```
```   337   colour :: colour
```
```   338
```
```   339 lemma
```
```   340   "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
```
```   341 quickcheck[exhaustive, expect = counterexample]
```
```   342 quickcheck[random, expect = counterexample]
```
```   343 oops
```
```   344
```
```   345 subsection {* Examples with locales *}
```
```   346
```
```   347 locale Truth
```
```   348
```
```   349 context Truth
```
```   350 begin
```
```   351
```
```   352 lemma "False"
```
```   353 quickcheck[exhaustive, expect = no_counterexample]
```
```   354 oops
```
```   355
```
```   356 end
```
```   357
```
```   358 interpretation Truth .
```
```   359
```
```   360 context Truth
```
```   361 begin
```
```   362
```
```   363 lemma "False"
```
```   364 quickcheck[exhaustive, expect = counterexample]
```
```   365 oops
```
```   366
```
```   367 end
```
```   368
```
```   369 end
```