src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 63901 4ce989e962e0 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
executable domain membership checks
```     1 (*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
```
```     2     Author:     Stefan Berghofer, Lukas Bulwahn
```
```     3     Copyright   2004 - 2010 TU Muenchen
```
```     4 *)
```
```     5
```
```     6 section \<open>Examples for the 'quickcheck' command\<close>
```
```     7
```
```     8 theory Quickcheck_Examples
```
```     9 imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
```
```    10 begin
```
```    11
```
```    12 text \<open>
```
```    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 \<close>
```
```    23
```
```    24 declare [[quickcheck_timeout = 3600]]
```
```    25
```
```    26 subsection \<open>Lists\<close>
```
```    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 \<open>An example involving functions inside other data structures\<close>
```
```    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 = 2, 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 \<open>A lemma, you'd think to be true from our experience with delAll\<close>
```
```    89 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    90   \<comment> \<open>Wrong. Precondition needed.\<close>
```
```    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     \<comment> \<open>Also wrong.\<close>
```
```    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   \<comment> \<open>Wrong. Precondition needed.\<close>
```
```   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 \<open>Trees\<close>
```
```   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     \<comment>\<open>Wrong!\<close>
```
```   145   oops
```
```   146
```
```   147 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
```
```   148   quickcheck[random, expect = counterexample]
```
```   149   quickcheck[exhaustive, expect = counterexample]
```
```   150     \<comment>\<open>Wrong!\<close>
```
```   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   \<comment>\<open>Wrong!\<close>
```
```   167   oops
```
```   168
```
```   169
```
```   170 subsection \<open>Exhaustive Testing beats Random Testing\<close>
```
```   171
```
```   172 text \<open>Here are some examples from mutants from the List theory
```
```   173 where exhaustive testing beats random testing\<close>
```
```   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 <= sum_list 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 \<open>Random Testing beats Exhaustive Testing\<close>
```
```   249
```
```   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
```
```   256
```
```   257 subsection \<open>Examples with quantifiers\<close>
```
```   258
```
```   259 text \<open>
```
```   260   These examples show that we can handle quantifiers.
```
```   261 \<close>
```
```   262
```
```   263 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
```
```   264   quickcheck[random, expect = counterexample]
```
```   265   quickcheck[exhaustive, expect = counterexample]
```
```   266 oops
```
```   267
```
```   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
```
```   272
```
```   273 lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
```
```   274   quickcheck[random, expect = counterexample]
```
```   275   quickcheck[expect = counterexample]
```
```   276 oops
```
```   277
```
```   278
```
```   279 subsection \<open>Examples with sets\<close>
```
```   280
```
```   281 lemma
```
```   282   "{} = A Un - A"
```
```   283 quickcheck[exhaustive, expect = counterexample]
```
```   284 oops
```
```   285
```
```   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
```
```   290
```
```   291
```
```   292 subsection \<open>Examples with relations\<close>
```
```   293
```
```   294 lemma
```
```   295   "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)"
```
```   296 quickcheck[exhaustive, expect = counterexample]
```
```   297 oops
```
```   298
```
```   299 lemma
```
```   300   "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)"
```
```   301 quickcheck[exhaustive, expect = counterexample]
```
```   302 oops
```
```   303
```
```   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
```
```   309
```
```   310 lemma
```
```   311   "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)"
```
```   312 quickcheck[exhaustive, expect = counterexample]
```
```   313 oops
```
```   314
```
```   315 lemma
```
```   316   "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)"
```
```   317 quickcheck[exhaustive, expect = counterexample]
```
```   318 oops
```
```   319
```
```   320 lemma
```
```   321   "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)"
```
```   322 quickcheck[exhaustive, expect = counterexample]
```
```   323 oops
```
```   324
```
```   325
```
```   326 subsection \<open>Examples with the descriptive operator\<close>
```
```   327
```
```   328 lemma
```
```   329   "(THE x. x = a) = b"
```
```   330 quickcheck[random, expect = counterexample]
```
```   331 quickcheck[exhaustive, expect = counterexample]
```
```   332 oops
```
```   333
```
```   334 subsection \<open>Examples with Multisets\<close>
```
```   335
```
```   336 lemma
```
```   337   "X + Y = Y + (Z :: 'a multiset)"
```
```   338 quickcheck[random, expect = counterexample]
```
```   339 quickcheck[exhaustive, expect = counterexample]
```
```   340 oops
```
```   341
```
```   342 lemma
```
```   343   "X - Y = Y - (Z :: 'a multiset)"
```
```   344 quickcheck[random, expect = counterexample]
```
```   345 quickcheck[exhaustive, expect = counterexample]
```
```   346 oops
```
```   347
```
```   348 lemma
```
```   349   "N + M - N = (N::'a multiset)"
```
```   350 quickcheck[random, expect = counterexample]
```
```   351 quickcheck[exhaustive, expect = counterexample]
```
```   352 oops
```
```   353
```
```   354 subsection \<open>Examples with numerical types\<close>
```
```   355
```
```   356 text \<open>
```
```   357 Quickcheck supports the common types nat, int, rat and real.
```
```   358 \<close>
```
```   359
```
```   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
```
```   365
```
```   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
```
```   371
```
```   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
```
```   377
```
```   378 lemma "(x :: rat) >= 0"
```
```   379 quickcheck[random, expect = counterexample]
```
```   380 quickcheck[exhaustive, expect = counterexample]
```
```   381 oops
```
```   382
```
```   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
```
```   388
```
```   389 lemma "(x :: real) >= 0"
```
```   390 quickcheck[random, expect = counterexample]
```
```   391 quickcheck[exhaustive, expect = counterexample]
```
```   392 oops
```
```   393
```
```   394 subsubsection \<open>floor and ceiling functions\<close>
```
```   395
```
```   396 lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: rat\<rfloor>"
```
```   397 quickcheck[expect = counterexample]
```
```   398 oops
```
```   399
```
```   400 lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: real\<rfloor>"
```
```   401 quickcheck[expect = counterexample]
```
```   402 oops
```
```   403
```
```   404 lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: rat\<rceil>"
```
```   405 quickcheck[expect = counterexample]
```
```   406 oops
```
```   407
```
```   408 lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: real\<rceil>"
```
```   409 quickcheck[expect = counterexample]
```
```   410 oops
```
```   411
```
```   412 subsection \<open>Examples with abstract types\<close>
```
```   413
```
```   414 lemma
```
```   415   "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
```
```   416 quickcheck[exhaustive]
```
```   417 quickcheck[random]
```
```   418 oops
```
```   419
```
```   420 lemma
```
```   421   "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
```
```   422 quickcheck[exhaustive]
```
```   423 quickcheck[random]
```
```   424 oops
```
```   425
```
```   426 subsection \<open>Examples with Records\<close>
```
```   427
```
```   428 record point =
```
```   429   xpos :: nat
```
```   430   ypos :: nat
```
```   431
```
```   432 lemma
```
```   433   "xpos r = xpos r' ==> r = r'"
```
```   434 quickcheck[exhaustive, expect = counterexample]
```
```   435 quickcheck[random, expect = counterexample]
```
```   436 oops
```
```   437
```
```   438 datatype colour = Red | Green | Blue
```
```   439
```
```   440 record cpoint = point +
```
```   441   colour :: colour
```
```   442
```
```   443 lemma
```
```   444   "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
```
```   445 quickcheck[exhaustive, expect = counterexample]
```
```   446 quickcheck[random, expect = counterexample]
```
```   447 oops
```
```   448
```
```   449 subsection \<open>Examples with locales\<close>
```
```   450
```
```   451 locale Truth
```
```   452
```
```   453 context Truth
```
```   454 begin
```
```   455
```
```   456 lemma "False"
```
```   457 quickcheck[exhaustive, expect = counterexample]
```
```   458 oops
```
```   459
```
```   460 end
```
```   461
```
```   462 interpretation Truth .
```
```   463
```
```   464 context Truth
```
```   465 begin
```
```   466
```
```   467 lemma "False"
```
```   468 quickcheck[exhaustive, expect = counterexample]
```
```   469 oops
```
```   470
```
```   471 end
```
```   472
```
```   473 locale antisym =
```
```   474   fixes R
```
```   475   assumes "R x y --> R y x --> x = y"
```
```   476
```
```   477 interpretation equal : antisym "op =" by standard simp
```
```   478 interpretation order_nat : antisym "op <= :: nat => _ => _" by standard simp
```
```   479
```
```   480 lemma (in antisym)
```
```   481   "R x y --> R y z --> R x z"
```
```   482 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
```
```   483 quickcheck[exhaustive, expect = counterexample]
```
```   484 oops
```
```   485
```
```   486 declare [[quickcheck_locale = "interpret"]]
```
```   487
```
```   488 lemma (in antisym)
```
```   489   "R x y --> R y z --> R x z"
```
```   490 quickcheck[exhaustive, expect = no_counterexample]
```
```   491 oops
```
```   492
```
```   493 declare [[quickcheck_locale = "expand"]]
```
```   494
```
```   495 lemma (in antisym)
```
```   496   "R x y --> R y z --> R x z"
```
```   497 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
```
```   498 quickcheck[exhaustive, expect = counterexample]
```
```   499 oops
```
```   500
```
```   501
```
```   502 subsection \<open>Examples with HOL quantifiers\<close>
```
```   503
```
```   504 lemma
```
```   505   "\<forall> xs ys. xs = [] --> xs = ys"
```
```   506 quickcheck[exhaustive, expect = counterexample]
```
```   507 oops
```
```   508
```
```   509 lemma
```
```   510   "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
```
```   511 quickcheck[exhaustive, expect = counterexample]
```
```   512 oops
```
```   513
```
```   514 lemma
```
```   515   "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
```
```   516 quickcheck[exhaustive, expect = counterexample]
```
```   517 oops
```
```   518
```
```   519 subsection \<open>Examples with underspecified/partial functions\<close>
```
```   520
```
```   521 lemma
```
```   522   "xs = [] ==> hd xs \<noteq> x"
```
```   523 quickcheck[exhaustive, expect = no_counterexample]
```
```   524 quickcheck[random, report = false, expect = no_counterexample]
```
```   525 quickcheck[random, report = true, expect = no_counterexample]
```
```   526 oops
```
```   527
```
```   528 lemma
```
```   529   "xs = [] ==> hd xs = x"
```
```   530 quickcheck[exhaustive, expect = no_counterexample]
```
```   531 quickcheck[random, report = false, expect = no_counterexample]
```
```   532 quickcheck[random, report = true, expect = no_counterexample]
```
```   533 oops
```
```   534
```
```   535 lemma "xs = [] ==> hd xs = x ==> x = y"
```
```   536 quickcheck[exhaustive, expect = no_counterexample]
```
```   537 quickcheck[random, report = false, expect = no_counterexample]
```
```   538 quickcheck[random, report = true, expect = no_counterexample]
```
```   539 oops
```
```   540
```
```   541 text \<open>with the simple testing scheme\<close>
```
```   542
```
```   543 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
```
```   544 declare [[quickcheck_full_support = false]]
```
```   545
```
```   546 lemma
```
```   547   "xs = [] ==> hd xs \<noteq> x"
```
```   548 quickcheck[exhaustive, expect = no_counterexample]
```
```   549 oops
```
```   550
```
```   551 lemma
```
```   552   "xs = [] ==> hd xs = x"
```
```   553 quickcheck[exhaustive, expect = no_counterexample]
```
```   554 oops
```
```   555
```
```   556 lemma "xs = [] ==> hd xs = x ==> x = y"
```
```   557 quickcheck[exhaustive, expect = no_counterexample]
```
```   558 oops
```
```   559
```
```   560 declare [[quickcheck_full_support = true]]
```
```   561
```
```   562
```
```   563 subsection \<open>Equality Optimisation\<close>
```
```   564
```
```   565 lemma
```
```   566   "f x = y ==> y = (0 :: nat)"
```
```   567 quickcheck
```
```   568 oops
```
```   569
```
```   570 lemma
```
```   571   "y = f x ==> y = (0 :: nat)"
```
```   572 quickcheck
```
```   573 oops
```
```   574
```
```   575 lemma
```
```   576   "f y = zz # zzs ==> zz = (0 :: nat) \<and> zzs = []"
```
```   577 quickcheck
```
```   578 oops
```
```   579
```
```   580 lemma
```
```   581   "f y = x # x' # xs ==> x = (0 :: nat) \<and> x' = 0 \<and> xs = []"
```
```   582 quickcheck
```
```   583 oops
```
```   584
```
```   585 lemma
```
```   586   "x = f x \<Longrightarrow> x = (0 :: nat)"
```
```   587 quickcheck
```
```   588 oops
```
```   589
```
```   590 lemma
```
```   591   "f y = x # x # xs ==> x = (0 :: nat) \<and> xs = []"
```
```   592 quickcheck
```
```   593 oops
```
```   594
```
```   595 lemma
```
```   596   "m1 k = Some v \<Longrightarrow> (m1 ++ m2) k = Some v"
```
```   597 quickcheck
```
```   598 oops
```
```   599
```
```   600
```
```   601 end
```