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