src/HOL/ex/Quickcheck_Examples.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 28336 a8edf4c69a79 child 37914 49b908e43d61 permissions -rw-r--r--
```     1 (*  Title:      HOL/ex/Quickcheck_Examples.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Stefan Berghofer
```
```     4     Copyright   2004 TU Muenchen
```
```     5 *)
```
```     6
```
```     7 header {* Examples for the 'quickcheck' command *}
```
```     8
```
```     9 theory Quickcheck_Examples
```
```    10 imports Main
```
```    11 begin
```
```    12
```
```    13 text {*
```
```    14 The 'quickcheck' command allows to find counterexamples by evaluating
```
```    15 formulae under an assignment of free variables to random values.
```
```    16 In contrast to 'refute', it can deal with inductive datatypes,
```
```    17 but cannot handle quantifiers.
```
```    18 *}
```
```    19
```
```    20 subsection {* Lists *}
```
```    21
```
```    22 theorem "map g (map f xs) = map (g o f) xs"
```
```    23   quickcheck
```
```    24   oops
```
```    25
```
```    26 theorem "map g (map f xs) = map (f o g) xs"
```
```    27   quickcheck
```
```    28   oops
```
```    29
```
```    30 theorem "rev (xs @ ys) = rev ys @ rev xs"
```
```    31   quickcheck
```
```    32   oops
```
```    33
```
```    34 theorem "rev (xs @ ys) = rev xs @ rev ys"
```
```    35   quickcheck
```
```    36   oops
```
```    37
```
```    38 theorem "rev (rev xs) = xs"
```
```    39   quickcheck
```
```    40   oops
```
```    41
```
```    42 theorem "rev xs = xs"
```
```    43   quickcheck
```
```    44   oops
```
```    45
```
```    46 text {* An example involving functions inside other data structures *}
```
```    47
```
```    48 primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```    49   "app [] x = x"
```
```    50   | "app (f # fs) x = app fs (f x)"
```
```    51
```
```    52 lemma "app (fs @ gs) x = app gs (app fs x)"
```
```    53   quickcheck
```
```    54   by (induct fs arbitrary: x) simp_all
```
```    55
```
```    56 lemma "app (fs @ gs) x = app fs (app gs x)"
```
```    57   quickcheck
```
```    58   oops
```
```    59
```
```    60 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
```
```    61   "occurs a [] = 0"
```
```    62   | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
```
```    63
```
```    64 primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
```
```    65   "del1 a [] = []"
```
```    66   | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
```
```    67
```
```    68 text {* A lemma, you'd think to be true from our experience with delAll *}
```
```    69 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    70   -- {* Wrong. Precondition needed.*}
```
```    71   quickcheck
```
```    72   oops
```
```    73
```
```    74 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    75   quickcheck
```
```    76     -- {* Also wrong.*}
```
```    77   oops
```
```    78
```
```    79 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    80   quickcheck
```
```    81   by (induct xs) auto
```
```    82
```
```    83 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
```
```    84   "replace a b [] = []"
```
```    85   | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
```
```    86                             else (x#(replace a b xs)))"
```
```    87
```
```    88 lemma "occurs a xs = occurs b (replace a b xs)"
```
```    89   quickcheck
```
```    90   -- {* Wrong. Precondition needed.*}
```
```    91   oops
```
```    92
```
```    93 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
```
```    94   quickcheck
```
```    95   by (induct xs) simp_all
```
```    96
```
```    97
```
```    98 subsection {* Trees *}
```
```    99
```
```   100 datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
```
```   101
```
```   102 primrec leaves :: "'a tree \<Rightarrow> 'a list" where
```
```   103   "leaves Twig = []"
```
```   104   | "leaves (Leaf a) = [a]"
```
```   105   | "leaves (Branch l r) = (leaves l) @ (leaves r)"
```
```   106
```
```   107 primrec plant :: "'a list \<Rightarrow> 'a tree" where
```
```   108   "plant [] = Twig "
```
```   109   | "plant (x#xs) = Branch (Leaf x) (plant xs)"
```
```   110
```
```   111 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
```
```   112   "mirror (Twig) = Twig "
```
```   113   | "mirror (Leaf a) = Leaf a "
```
```   114   | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
```
```   115
```
```   116 theorem "plant (rev (leaves xt)) = mirror xt"
```
```   117   quickcheck
```
```   118     --{* Wrong! *}
```
```   119   oops
```
```   120
```
```   121 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
```
```   122   quickcheck
```
```   123     --{* Wrong! *}
```
```   124   oops
```
```   125
```
```   126 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
```
```   127
```
```   128 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
```
```   129   "inOrder (Tip a)= [a]"
```
```   130   | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
```
```   131
```
```   132 primrec root :: "'a ntree \<Rightarrow> 'a" where
```
```   133   "root (Tip a) = a"
```
```   134   | "root (Node f x y) = f"
```
```   135
```
```   136 theorem "hd (inOrder xt) = root xt"
```
```   137   quickcheck
```
```   138     --{* Wrong! *}
```
```   139   oops
```
```   140
```
```   141 end
```