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
wenzelm@46879
     1
(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
bulwahn@40645
     2
    Author:     Stefan Berghofer, Lukas Bulwahn
bulwahn@40645
     3
    Copyright   2004 - 2010 TU Muenchen
berghofe@14592
     4
*)
berghofe@14592
     5
wenzelm@63167
     6
section \<open>Examples for the 'quickcheck' command\<close>
berghofe@14592
     7
haftmann@28314
     8
theory Quickcheck_Examples
wenzelm@57645
     9
imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
haftmann@28314
    10
begin
berghofe@14592
    11
wenzelm@63167
    12
text \<open>
berghofe@14592
    13
The 'quickcheck' command allows to find counterexamples by evaluating
bulwahn@40654
    14
formulae.
bulwahn@40654
    15
Currently, there are two different exploration schemes:
bulwahn@40654
    16
- random testing: this is incomplete, but explores the search space faster.
bulwahn@40654
    17
- exhaustive testing: this is complete, but increasing the depth leads to
bulwahn@40654
    18
  exponentially many assignments.
bulwahn@40654
    19
bulwahn@40654
    20
quickcheck can handle quantifiers on finite universes.
bulwahn@40654
    21
wenzelm@63167
    22
\<close>
berghofe@14592
    23
bulwahn@43803
    24
declare [[quickcheck_timeout = 3600]]
bulwahn@43803
    25
wenzelm@63167
    26
subsection \<open>Lists\<close>
berghofe@14592
    27
berghofe@14592
    28
theorem "map g (map f xs) = map (g o f) xs"
bulwahn@40917
    29
  quickcheck[random, expect = no_counterexample]
bulwahn@40917
    30
  quickcheck[exhaustive, size = 3, expect = no_counterexample]
berghofe@14592
    31
  oops
berghofe@14592
    32
berghofe@14592
    33
theorem "map g (map f xs) = map (f o g) xs"
bulwahn@40917
    34
  quickcheck[random, expect = counterexample]
bulwahn@40917
    35
  quickcheck[exhaustive, expect = counterexample]
berghofe@14592
    36
  oops
berghofe@14592
    37
berghofe@14592
    38
theorem "rev (xs @ ys) = rev ys @ rev xs"
bulwahn@40917
    39
  quickcheck[random, expect = no_counterexample]
bulwahn@40917
    40
  quickcheck[exhaustive, expect = no_counterexample]
bulwahn@42087
    41
  quickcheck[exhaustive, size = 1000, timeout = 0.1]
berghofe@14592
    42
  oops
berghofe@14592
    43
berghofe@14592
    44
theorem "rev (xs @ ys) = rev xs @ rev ys"
bulwahn@40917
    45
  quickcheck[random, expect = counterexample]
bulwahn@40917
    46
  quickcheck[exhaustive, expect = counterexample]
berghofe@14592
    47
  oops
berghofe@14592
    48
berghofe@14592
    49
theorem "rev (rev xs) = xs"
bulwahn@40917
    50
  quickcheck[random, expect = no_counterexample]
bulwahn@40917
    51
  quickcheck[exhaustive, expect = no_counterexample]
berghofe@14592
    52
  oops
berghofe@14592
    53
berghofe@14592
    54
theorem "rev xs = xs"
bulwahn@42159
    55
  quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
bulwahn@42159
    56
  quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
bulwahn@42159
    57
  quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
bulwahn@42159
    58
  quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
bulwahn@42159
    59
  quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
bulwahn@42159
    60
  quickcheck[tester = exhaustive, finite_types = false, expect = counterexample]
bulwahn@42159
    61
oops
bulwahn@42159
    62
berghofe@14592
    63
wenzelm@63167
    64
text \<open>An example involving functions inside other data structures\<close>
berghofe@25891
    65
haftmann@28314
    66
primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
berghofe@25891
    67
  "app [] x = x"
haftmann@28314
    68
  | "app (f # fs) x = app fs (f x)"
berghofe@25891
    69
berghofe@25891
    70
lemma "app (fs @ gs) x = app gs (app fs x)"
bulwahn@40917
    71
  quickcheck[random, expect = no_counterexample]
bulwahn@47348
    72
  quickcheck[exhaustive, size = 2, expect = no_counterexample]
berghofe@25891
    73
  by (induct fs arbitrary: x) simp_all
berghofe@25891
    74
berghofe@25891
    75
lemma "app (fs @ gs) x = app fs (app gs x)"
bulwahn@40917
    76
  quickcheck[random, expect = counterexample]
bulwahn@40917
    77
  quickcheck[exhaustive, expect = counterexample]
berghofe@25891
    78
  oops
berghofe@25891
    79
haftmann@28314
    80
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
berghofe@14592
    81
  "occurs a [] = 0"
haftmann@28314
    82
  | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
berghofe@14592
    83
haftmann@28314
    84
primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
berghofe@14592
    85
  "del1 a [] = []"
haftmann@28314
    86
  | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
berghofe@14592
    87
wenzelm@63167
    88
text \<open>A lemma, you'd think to be true from our experience with delAll\<close>
berghofe@14592
    89
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
wenzelm@63167
    90
  \<comment> \<open>Wrong. Precondition needed.\<close>
bulwahn@40917
    91
  quickcheck[random, expect = counterexample]
bulwahn@40917
    92
  quickcheck[exhaustive, expect = counterexample]
berghofe@14592
    93
  oops
berghofe@14592
    94
berghofe@14592
    95
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
bulwahn@40917
    96
  quickcheck[random, expect = counterexample]
bulwahn@40917
    97
  quickcheck[exhaustive, expect = counterexample]
wenzelm@63167
    98
    \<comment> \<open>Also wrong.\<close>
berghofe@14592
    99
  oops
berghofe@14592
   100
berghofe@14592
   101
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
bulwahn@40917
   102
  quickcheck[random, expect = no_counterexample]
bulwahn@40917
   103
  quickcheck[exhaustive, expect = no_counterexample]
haftmann@28314
   104
  by (induct xs) auto
berghofe@14592
   105
haftmann@28314
   106
primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
berghofe@14592
   107
  "replace a b [] = []"
haftmann@28314
   108
  | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
berghofe@14592
   109
                            else (x#(replace a b xs)))"
berghofe@14592
   110
berghofe@14592
   111
lemma "occurs a xs = occurs b (replace a b xs)"
bulwahn@40917
   112
  quickcheck[random, expect = counterexample]
bulwahn@40917
   113
  quickcheck[exhaustive, expect = counterexample]
wenzelm@63167
   114
  \<comment> \<open>Wrong. Precondition needed.\<close>
berghofe@14592
   115
  oops
berghofe@14592
   116
berghofe@14592
   117
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
bulwahn@40917
   118
  quickcheck[random, expect = no_counterexample]
bulwahn@40917
   119
  quickcheck[exhaustive, expect = no_counterexample]
haftmann@28314
   120
  by (induct xs) simp_all
berghofe@14592
   121
berghofe@14592
   122
wenzelm@63167
   123
subsection \<open>Trees\<close>
berghofe@14592
   124
blanchet@58310
   125
datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
berghofe@14592
   126
haftmann@28314
   127
primrec leaves :: "'a tree \<Rightarrow> 'a list" where
berghofe@14592
   128
  "leaves Twig = []"
haftmann@28314
   129
  | "leaves (Leaf a) = [a]"
haftmann@28314
   130
  | "leaves (Branch l r) = (leaves l) @ (leaves r)"
berghofe@14592
   131
haftmann@28314
   132
primrec plant :: "'a list \<Rightarrow> 'a tree" where
berghofe@14592
   133
  "plant [] = Twig "
haftmann@28314
   134
  | "plant (x#xs) = Branch (Leaf x) (plant xs)"
berghofe@14592
   135
haftmann@28314
   136
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
berghofe@14592
   137
  "mirror (Twig) = Twig "
haftmann@28314
   138
  | "mirror (Leaf a) = Leaf a "
haftmann@28314
   139
  | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
berghofe@14592
   140
berghofe@14592
   141
theorem "plant (rev (leaves xt)) = mirror xt"
bulwahn@40917
   142
  quickcheck[random, expect = counterexample]
bulwahn@40917
   143
  quickcheck[exhaustive, expect = counterexample]
wenzelm@63167
   144
    \<comment>\<open>Wrong!\<close> 
berghofe@14592
   145
  oops
berghofe@14592
   146
berghofe@14592
   147
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
bulwahn@40917
   148
  quickcheck[random, expect = counterexample]
bulwahn@40917
   149
  quickcheck[exhaustive, expect = counterexample]
wenzelm@63167
   150
    \<comment>\<open>Wrong!\<close> 
berghofe@14592
   151
  oops
berghofe@14592
   152
blanchet@58310
   153
datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
berghofe@14592
   154
haftmann@28314
   155
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
berghofe@14592
   156
  "inOrder (Tip a)= [a]"
haftmann@28314
   157
  | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
berghofe@14592
   158
haftmann@28314
   159
primrec root :: "'a ntree \<Rightarrow> 'a" where
berghofe@14592
   160
  "root (Tip a) = a"
haftmann@28314
   161
  | "root (Node f x y) = f"
berghofe@14592
   162
haftmann@28314
   163
theorem "hd (inOrder xt) = root xt"
bulwahn@40917
   164
  quickcheck[random, expect = counterexample]
bulwahn@40917
   165
  quickcheck[exhaustive, expect = counterexample]
wenzelm@63167
   166
  \<comment>\<open>Wrong!\<close> 
berghofe@14592
   167
  oops
berghofe@14592
   168
bulwahn@40645
   169
wenzelm@63167
   170
subsection \<open>Exhaustive Testing beats Random Testing\<close>
bulwahn@40645
   171
wenzelm@63167
   172
text \<open>Here are some examples from mutants from the List theory
wenzelm@63167
   173
where exhaustive testing beats random testing\<close>
bulwahn@40645
   174
bulwahn@40645
   175
lemma
bulwahn@40645
   176
  "[] ~= xs ==> hd xs = last (x # xs)"
bulwahn@40917
   177
quickcheck[random]
bulwahn@40917
   178
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   179
oops
bulwahn@40645
   180
bulwahn@40645
   181
lemma
bulwahn@40645
   182
  assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
bulwahn@40645
   183
  shows "drop n xs = takeWhile P xs"
bulwahn@40917
   184
quickcheck[random, iterations = 10000, quiet]
bulwahn@40917
   185
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   186
oops
bulwahn@40645
   187
bulwahn@40645
   188
lemma
bulwahn@40645
   189
  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
bulwahn@40917
   190
quickcheck[random, iterations = 10000]
bulwahn@40917
   191
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   192
oops
bulwahn@40645
   193
bulwahn@40645
   194
lemma
bulwahn@40645
   195
  "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
bulwahn@40917
   196
quickcheck[random, iterations = 10000, finite_types = false]
bulwahn@40917
   197
quickcheck[exhaustive, finite_types = false, expect = counterexample]
bulwahn@40645
   198
oops
bulwahn@40645
   199
bulwahn@40645
   200
lemma
bulwahn@40645
   201
  "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
bulwahn@40917
   202
quickcheck[random, iterations = 10000, finite_types = false]
bulwahn@40917
   203
quickcheck[exhaustive, finite_types = false, expect = counterexample]
bulwahn@40645
   204
oops
bulwahn@40645
   205
bulwahn@40645
   206
lemma
nipkow@63882
   207
  "ns ! k < length ns ==> k <= sum_list ns"
bulwahn@40917
   208
quickcheck[random, iterations = 10000, finite_types = false, quiet]
bulwahn@40917
   209
quickcheck[exhaustive, finite_types = false, expect = counterexample]
bulwahn@40645
   210
oops
bulwahn@40645
   211
bulwahn@40645
   212
lemma
bulwahn@40645
   213
  "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
bulwahn@40917
   214
quickcheck[random, iterations = 10000]
bulwahn@40917
   215
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   216
oops
bulwahn@40645
   217
bulwahn@40645
   218
lemma
bulwahn@40645
   219
"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
bulwahn@40917
   220
quickcheck[random, iterations = 10000]
bulwahn@40917
   221
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   222
oops
bulwahn@40645
   223
bulwahn@40645
   224
lemma
bulwahn@40645
   225
  "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
bulwahn@40917
   226
quickcheck[random, iterations = 10000]
bulwahn@40917
   227
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   228
oops
bulwahn@40645
   229
bulwahn@40645
   230
lemma
bulwahn@40645
   231
  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
bulwahn@40917
   232
quickcheck[random]
bulwahn@40917
   233
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   234
oops
bulwahn@40645
   235
bulwahn@40645
   236
lemma
huffman@44189
   237
  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
bulwahn@40917
   238
quickcheck[random]
bulwahn@40917
   239
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   240
oops
bulwahn@40645
   241
bulwahn@40645
   242
lemma
bulwahn@40645
   243
  "(ys = zs) = (xs @ ys = splice xs zs)"
bulwahn@40917
   244
quickcheck[random]
bulwahn@40917
   245
quickcheck[exhaustive, expect = counterexample]
bulwahn@40645
   246
oops
bulwahn@40645
   247
wenzelm@63167
   248
subsection \<open>Random Testing beats Exhaustive Testing\<close>
bulwahn@46672
   249
bulwahn@46672
   250
lemma mult_inj_if_coprime_nat:
bulwahn@46672
   251
  "inj_on f A \<Longrightarrow> inj_on g B
bulwahn@46672
   252
   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
bulwahn@46672
   253
quickcheck[exhaustive]
bulwahn@46672
   254
quickcheck[random]
bulwahn@46672
   255
oops
bulwahn@46672
   256
wenzelm@63167
   257
subsection \<open>Examples with quantifiers\<close>
bulwahn@40654
   258
wenzelm@63167
   259
text \<open>
bulwahn@40654
   260
  These examples show that we can handle quantifiers.
wenzelm@63167
   261
\<close>
bulwahn@40654
   262
bulwahn@40654
   263
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
bulwahn@40917
   264
  quickcheck[random, expect = counterexample]
bulwahn@40917
   265
  quickcheck[exhaustive, expect = counterexample]
bulwahn@40654
   266
oops
bulwahn@40654
   267
bulwahn@40654
   268
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
bulwahn@40917
   269
  quickcheck[random, expect = counterexample]
bulwahn@40654
   270
  quickcheck[expect = counterexample]
bulwahn@40654
   271
oops
bulwahn@40654
   272
wenzelm@63901
   273
lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
bulwahn@40917
   274
  quickcheck[random, expect = counterexample]
bulwahn@40654
   275
  quickcheck[expect = counterexample]
bulwahn@40654
   276
oops
bulwahn@40654
   277
bulwahn@45118
   278
wenzelm@63167
   279
subsection \<open>Examples with sets\<close>
bulwahn@46397
   280
bulwahn@46397
   281
lemma
bulwahn@46397
   282
  "{} = A Un - A"
bulwahn@46397
   283
quickcheck[exhaustive, expect = counterexample]
bulwahn@46397
   284
oops
bulwahn@46397
   285
bulwahn@46421
   286
lemma
bulwahn@46421
   287
  "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
bulwahn@46421
   288
quickcheck[exhaustive, expect = counterexample]
bulwahn@46421
   289
oops
bulwahn@46421
   290
bulwahn@46397
   291
wenzelm@63167
   292
subsection \<open>Examples with relations\<close>
bulwahn@45118
   293
bulwahn@45118
   294
lemma
bulwahn@46348
   295
  "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)"
bulwahn@46348
   296
quickcheck[exhaustive, expect = counterexample]
bulwahn@45118
   297
oops
bulwahn@45118
   298
bulwahn@45118
   299
lemma
bulwahn@46348
   300
  "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)"
bulwahn@46348
   301
quickcheck[exhaustive, expect = counterexample]
bulwahn@46348
   302
oops
bulwahn@46348
   303
bulwahn@46348
   304
(* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *)
bulwahn@46348
   305
lemma
bulwahn@45118
   306
  "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
bulwahn@46348
   307
(*quickcheck[exhaustive, expect = counterexample]*)
bulwahn@46348
   308
oops
bulwahn@46348
   309
bulwahn@46348
   310
lemma
bulwahn@46348
   311
  "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)"
bulwahn@46348
   312
quickcheck[exhaustive, expect = counterexample]
bulwahn@45118
   313
oops
bulwahn@45118
   314
bulwahn@46348
   315
lemma
bulwahn@46348
   316
  "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)"
bulwahn@46348
   317
quickcheck[exhaustive, expect = counterexample]
bulwahn@46348
   318
oops
bulwahn@46348
   319
bulwahn@46348
   320
lemma
bulwahn@46348
   321
  "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)"
bulwahn@46348
   322
quickcheck[exhaustive, expect = counterexample]
bulwahn@46348
   323
oops
bulwahn@46348
   324
bulwahn@46348
   325
wenzelm@63167
   326
subsection \<open>Examples with the descriptive operator\<close>
bulwahn@46337
   327
bulwahn@46337
   328
lemma
bulwahn@46337
   329
  "(THE x. x = a) = b"
bulwahn@46337
   330
quickcheck[random, expect = counterexample]
bulwahn@46337
   331
quickcheck[exhaustive, expect = counterexample]
bulwahn@46337
   332
oops
bulwahn@46337
   333
wenzelm@63167
   334
subsection \<open>Examples with Multisets\<close>
bulwahn@46169
   335
bulwahn@46169
   336
lemma
bulwahn@46169
   337
  "X + Y = Y + (Z :: 'a multiset)"
bulwahn@46169
   338
quickcheck[random, expect = counterexample]
bulwahn@46169
   339
quickcheck[exhaustive, expect = counterexample]
bulwahn@46169
   340
oops
bulwahn@46169
   341
bulwahn@46169
   342
lemma
bulwahn@46169
   343
  "X - Y = Y - (Z :: 'a multiset)"
bulwahn@46169
   344
quickcheck[random, expect = counterexample]
bulwahn@46169
   345
quickcheck[exhaustive, expect = counterexample]
bulwahn@46169
   346
oops
bulwahn@46169
   347
bulwahn@46169
   348
lemma
bulwahn@46169
   349
  "N + M - N = (N::'a multiset)"
bulwahn@46169
   350
quickcheck[random, expect = counterexample]
bulwahn@46169
   351
quickcheck[exhaustive, expect = counterexample]
bulwahn@46169
   352
oops
bulwahn@45118
   353
wenzelm@63167
   354
subsection \<open>Examples with numerical types\<close>
bulwahn@41231
   355
wenzelm@63167
   356
text \<open>
bulwahn@41231
   357
Quickcheck supports the common types nat, int, rat and real.
wenzelm@63167
   358
\<close>
bulwahn@41231
   359
bulwahn@41231
   360
lemma
bulwahn@41231
   361
  "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
bulwahn@41231
   362
quickcheck[exhaustive, size = 10, expect = counterexample]
bulwahn@41231
   363
quickcheck[random, size = 10]
bulwahn@41231
   364
oops
bulwahn@41231
   365
bulwahn@41231
   366
lemma
bulwahn@41231
   367
  "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
bulwahn@41231
   368
quickcheck[exhaustive, size = 10, expect = counterexample]
bulwahn@41231
   369
quickcheck[random, size = 10]
bulwahn@41231
   370
oops
bulwahn@41231
   371
bulwahn@41231
   372
lemma
bulwahn@41231
   373
  "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
bulwahn@41231
   374
quickcheck[exhaustive, size = 10, expect = counterexample]
bulwahn@41231
   375
quickcheck[random, size = 10]
bulwahn@41231
   376
oops
bulwahn@41231
   377
bulwahn@45507
   378
lemma "(x :: rat) >= 0"
bulwahn@45507
   379
quickcheck[random, expect = counterexample]
bulwahn@45507
   380
quickcheck[exhaustive, expect = counterexample]
bulwahn@45507
   381
oops
bulwahn@45507
   382
bulwahn@41231
   383
lemma
bulwahn@41231
   384
  "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
bulwahn@41231
   385
quickcheck[exhaustive, size = 10, expect = counterexample]
bulwahn@41231
   386
quickcheck[random, size = 10]
bulwahn@41231
   387
oops
bulwahn@41231
   388
bulwahn@45507
   389
lemma "(x :: real) >= 0"
bulwahn@45507
   390
quickcheck[random, expect = counterexample]
bulwahn@45507
   391
quickcheck[exhaustive, expect = counterexample]
bulwahn@45507
   392
oops
bulwahn@45507
   393
wenzelm@63167
   394
subsubsection \<open>floor and ceiling functions\<close>
bulwahn@43734
   395
wenzelm@61942
   396
lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: rat\<rfloor>"
bulwahn@43734
   397
quickcheck[expect = counterexample]
bulwahn@43734
   398
oops
bulwahn@43734
   399
wenzelm@61942
   400
lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: real\<rfloor>"
bulwahn@43734
   401
quickcheck[expect = counterexample]
bulwahn@43734
   402
oops
bulwahn@43734
   403
wenzelm@61942
   404
lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: rat\<rceil>"
bulwahn@43734
   405
quickcheck[expect = counterexample]
bulwahn@43734
   406
oops
bulwahn@43734
   407
wenzelm@61942
   408
lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: real\<rceil>"
bulwahn@43734
   409
quickcheck[expect = counterexample]
bulwahn@43734
   410
oops
bulwahn@43734
   411
wenzelm@63167
   412
subsection \<open>Examples with abstract types\<close>
bulwahn@45927
   413
bulwahn@45927
   414
lemma
bulwahn@45927
   415
  "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
bulwahn@45927
   416
quickcheck[exhaustive]
bulwahn@45942
   417
quickcheck[random]
bulwahn@45927
   418
oops
bulwahn@45927
   419
bulwahn@45927
   420
lemma
bulwahn@45927
   421
  "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
bulwahn@45927
   422
quickcheck[exhaustive]
bulwahn@45942
   423
quickcheck[random]
bulwahn@45927
   424
oops
bulwahn@43734
   425
wenzelm@63167
   426
subsection \<open>Examples with Records\<close>
bulwahn@42696
   427
bulwahn@42696
   428
record point =
bulwahn@42696
   429
  xpos :: nat
bulwahn@42696
   430
  ypos :: nat
bulwahn@42696
   431
bulwahn@42696
   432
lemma
bulwahn@42696
   433
  "xpos r = xpos r' ==> r = r'"
bulwahn@42696
   434
quickcheck[exhaustive, expect = counterexample]
bulwahn@42696
   435
quickcheck[random, expect = counterexample]
bulwahn@42696
   436
oops
bulwahn@42696
   437
blanchet@58310
   438
datatype colour = Red | Green | Blue
bulwahn@42696
   439
bulwahn@42696
   440
record cpoint = point +
bulwahn@42696
   441
  colour :: colour
bulwahn@42696
   442
bulwahn@42696
   443
lemma
bulwahn@42696
   444
  "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
bulwahn@42696
   445
quickcheck[exhaustive, expect = counterexample]
bulwahn@42696
   446
quickcheck[random, expect = counterexample]
bulwahn@42696
   447
oops
bulwahn@42696
   448
wenzelm@63167
   449
subsection \<open>Examples with locales\<close>
bulwahn@42434
   450
bulwahn@42434
   451
locale Truth
bulwahn@42434
   452
bulwahn@42434
   453
context Truth
bulwahn@42434
   454
begin
bulwahn@42434
   455
bulwahn@42434
   456
lemma "False"
bulwahn@46344
   457
quickcheck[exhaustive, expect = counterexample]
bulwahn@42434
   458
oops
bulwahn@42434
   459
berghofe@14592
   460
end
bulwahn@42434
   461
bulwahn@42434
   462
interpretation Truth .
bulwahn@42434
   463
bulwahn@42434
   464
context Truth
bulwahn@42434
   465
begin
bulwahn@42434
   466
bulwahn@42434
   467
lemma "False"
bulwahn@43890
   468
quickcheck[exhaustive, expect = counterexample]
bulwahn@42434
   469
oops
bulwahn@42434
   470
bulwahn@42434
   471
end
bulwahn@42434
   472
bulwahn@46344
   473
locale antisym =
bulwahn@46344
   474
  fixes R
bulwahn@46344
   475
  assumes "R x y --> R y x --> x = y"
bulwahn@46344
   476
wenzelm@61169
   477
interpretation equal : antisym "op =" by standard simp
wenzelm@61169
   478
interpretation order_nat : antisym "op <= :: nat => _ => _" by standard simp
bulwahn@47348
   479
bulwahn@47348
   480
lemma (in antisym)
bulwahn@46344
   481
  "R x y --> R y z --> R x z"
bulwahn@46344
   482
quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
bulwahn@46344
   483
quickcheck[exhaustive, expect = counterexample]
bulwahn@46344
   484
oops
bulwahn@46344
   485
bulwahn@47348
   486
declare [[quickcheck_locale = "interpret"]]
bulwahn@47348
   487
bulwahn@47348
   488
lemma (in antisym)
bulwahn@47348
   489
  "R x y --> R y z --> R x z"
bulwahn@47348
   490
quickcheck[exhaustive, expect = no_counterexample]
bulwahn@47348
   491
oops
bulwahn@47348
   492
bulwahn@47348
   493
declare [[quickcheck_locale = "expand"]]
bulwahn@47348
   494
bulwahn@47348
   495
lemma (in antisym)
bulwahn@47348
   496
  "R x y --> R y z --> R x z"
bulwahn@47348
   497
quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
bulwahn@47348
   498
quickcheck[exhaustive, expect = counterexample]
bulwahn@47348
   499
oops
bulwahn@47348
   500
bulwahn@46344
   501
wenzelm@63167
   502
subsection \<open>Examples with HOL quantifiers\<close>
bulwahn@45441
   503
bulwahn@45441
   504
lemma
bulwahn@45441
   505
  "\<forall> xs ys. xs = [] --> xs = ys"
bulwahn@45441
   506
quickcheck[exhaustive, expect = counterexample]
bulwahn@45441
   507
oops
bulwahn@45441
   508
bulwahn@45441
   509
lemma
bulwahn@45441
   510
  "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
bulwahn@45441
   511
quickcheck[exhaustive, expect = counterexample]
bulwahn@45441
   512
oops
bulwahn@45441
   513
bulwahn@45441
   514
lemma
bulwahn@45441
   515
  "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
bulwahn@45441
   516
quickcheck[exhaustive, expect = counterexample]
bulwahn@45441
   517
oops
bulwahn@45441
   518
wenzelm@63167
   519
subsection \<open>Examples with underspecified/partial functions\<close>
bulwahn@45684
   520
bulwahn@45684
   521
lemma
bulwahn@45684
   522
  "xs = [] ==> hd xs \<noteq> x"
bulwahn@45762
   523
quickcheck[exhaustive, expect = no_counterexample]
bulwahn@45762
   524
quickcheck[random, report = false, expect = no_counterexample]
bulwahn@45765
   525
quickcheck[random, report = true, expect = no_counterexample]
bulwahn@45684
   526
oops
bulwahn@45684
   527
bulwahn@45684
   528
lemma
bulwahn@45684
   529
  "xs = [] ==> hd xs = x"
bulwahn@45765
   530
quickcheck[exhaustive, expect = no_counterexample]
bulwahn@45765
   531
quickcheck[random, report = false, expect = no_counterexample]
bulwahn@45765
   532
quickcheck[random, report = true, expect = no_counterexample]
bulwahn@45684
   533
oops
bulwahn@45684
   534
bulwahn@45684
   535
lemma "xs = [] ==> hd xs = x ==> x = y"
bulwahn@45765
   536
quickcheck[exhaustive, expect = no_counterexample]
bulwahn@45765
   537
quickcheck[random, report = false, expect = no_counterexample]
bulwahn@45765
   538
quickcheck[random, report = true, expect = no_counterexample]
bulwahn@45684
   539
oops
bulwahn@45684
   540
wenzelm@63167
   541
text \<open>with the simple testing scheme\<close>
bulwahn@45689
   542
wenzelm@58813
   543
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
bulwahn@45689
   544
declare [[quickcheck_full_support = false]]
bulwahn@45689
   545
bulwahn@45689
   546
lemma
bulwahn@45689
   547
  "xs = [] ==> hd xs \<noteq> x"
bulwahn@45765
   548
quickcheck[exhaustive, expect = no_counterexample]
bulwahn@45689
   549
oops
bulwahn@45689
   550
bulwahn@45689
   551
lemma
bulwahn@45689
   552
  "xs = [] ==> hd xs = x"
bulwahn@45765
   553
quickcheck[exhaustive, expect = no_counterexample]
bulwahn@45689
   554
oops
bulwahn@45689
   555
bulwahn@45689
   556
lemma "xs = [] ==> hd xs = x ==> x = y"
bulwahn@45765
   557
quickcheck[exhaustive, expect = no_counterexample]
bulwahn@45689
   558
oops
bulwahn@45689
   559
bulwahn@45689
   560
declare [[quickcheck_full_support = true]]
bulwahn@45441
   561
bulwahn@48013
   562
wenzelm@63167
   563
subsection \<open>Equality Optimisation\<close>
bulwahn@48013
   564
bulwahn@48013
   565
lemma
bulwahn@48013
   566
  "f x = y ==> y = (0 :: nat)"
bulwahn@48013
   567
quickcheck
bulwahn@48013
   568
oops
bulwahn@48013
   569
bulwahn@48013
   570
lemma
bulwahn@48013
   571
  "y = f x ==> y = (0 :: nat)"
bulwahn@48013
   572
quickcheck
bulwahn@48013
   573
oops
bulwahn@48013
   574
bulwahn@48013
   575
lemma
bulwahn@48013
   576
  "f y = zz # zzs ==> zz = (0 :: nat) \<and> zzs = []"
bulwahn@48013
   577
quickcheck
bulwahn@48013
   578
oops
bulwahn@48013
   579
bulwahn@48013
   580
lemma
bulwahn@48013
   581
  "f y = x # x' # xs ==> x = (0 :: nat) \<and> x' = 0 \<and> xs = []"
bulwahn@48013
   582
quickcheck
bulwahn@48013
   583
oops
bulwahn@48013
   584
bulwahn@48013
   585
lemma
bulwahn@48013
   586
  "x = f x \<Longrightarrow> x = (0 :: nat)"
bulwahn@48013
   587
quickcheck
bulwahn@48013
   588
oops
bulwahn@48013
   589
bulwahn@48013
   590
lemma
bulwahn@48013
   591
  "f y = x # x # xs ==> x = (0 :: nat) \<and> xs = []"
bulwahn@48013
   592
quickcheck
bulwahn@48013
   593
oops
bulwahn@48013
   594
bulwahn@48013
   595
lemma
bulwahn@48013
   596
  "m1 k = Some v \<Longrightarrow> (m1 ++ m2) k = Some v"
bulwahn@48013
   597
quickcheck
bulwahn@48013
   598
oops
bulwahn@48013
   599
bulwahn@48013
   600
bulwahn@42434
   601
end