src/HOL/ex/Quickcheck_Examples.thy
 author haftmann Wed Mar 12 19:38:14 2008 +0100 (2008-03-12) changeset 26265 4b63b9e9b10d parent 25891 1bd12187a96e child 28314 053419cefd3c permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
```     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 imports Main begin
```
```    10
```
```    11 text {*
```
```    12 The 'quickcheck' command allows to find counterexamples by evaluating
```
```    13 formulae under an assignment of free variables to random values.
```
```    14 In contrast to 'refute', it can deal with inductive datatypes,
```
```    15 but cannot handle quantifiers.
```
```    16 *}
```
```    17
```
```    18 subsection {* Lists *}
```
```    19
```
```    20 theorem "map g (map f xs) = map (g o f) xs"
```
```    21   quickcheck
```
```    22   oops
```
```    23
```
```    24 theorem "map g (map f xs) = map (f o g) xs"
```
```    25   quickcheck
```
```    26   oops
```
```    27
```
```    28 theorem "rev (xs @ ys) = rev ys @ rev xs"
```
```    29   quickcheck
```
```    30   oops
```
```    31
```
```    32 theorem "rev (xs @ ys) = rev xs @ rev ys"
```
```    33   quickcheck
```
```    34   oops
```
```    35
```
```    36 theorem "rev (rev xs) = xs"
```
```    37   quickcheck
```
```    38   oops
```
```    39
```
```    40 theorem "rev xs = xs"
```
```    41   quickcheck
```
```    42   oops
```
```    43
```
```    44 text {* An example involving functions inside other data structures *}
```
```    45
```
```    46 consts app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a"
```
```    47
```
```    48 primrec
```
```    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 consts
```
```    61   occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
```
```    62 primrec
```
```    63   "occurs a [] = 0"
```
```    64   "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
```
```    65
```
```    66 consts
```
```    67   del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    68 primrec
```
```    69   "del1 a [] = []"
```
```    70   "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
```
```    71
```
```    72 text {* A lemma, you'd think to be true from our experience with delAll *}
```
```    73 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    74   -- {* Wrong. Precondition needed.*}
```
```    75   quickcheck
```
```    76   oops
```
```    77
```
```    78 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    79   quickcheck
```
```    80     -- {* Also wrong.*}
```
```    81   oops
```
```    82
```
```    83 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    84   quickcheck
```
```    85   apply (induct_tac xs)
```
```    86   apply auto
```
```    87     -- {* Correct! *}
```
```    88   done
```
```    89
```
```    90 consts
```
```    91   replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    92 primrec
```
```    93   "replace a b [] = []"
```
```    94   "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
```
```    95                             else (x#(replace a b xs)))"
```
```    96
```
```    97 lemma "occurs a xs = occurs b (replace a b xs)"
```
```    98   quickcheck
```
```    99   -- {* Wrong. Precondition needed.*}
```
```   100   oops
```
```   101
```
```   102 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
```
```   103   quickcheck
```
```   104   apply (induct_tac xs)
```
```   105   apply auto
```
```   106   done
```
```   107
```
```   108
```
```   109 subsection {* Trees *}
```
```   110
```
```   111 datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
```
```   112
```
```   113 consts
```
```   114   leaves :: "'a tree \<Rightarrow> 'a list"
```
```   115 primrec
```
```   116   "leaves Twig = []"
```
```   117   "leaves (Leaf a) = [a]"
```
```   118   "leaves (Branch l r) = (leaves l) @ (leaves r)"
```
```   119
```
```   120 consts
```
```   121   plant :: "'a list \<Rightarrow> 'a tree"
```
```   122 primrec
```
```   123   "plant [] = Twig "
```
```   124   "plant (x#xs) = Branch (Leaf x) (plant xs)"
```
```   125
```
```   126 consts
```
```   127   mirror :: "'a tree \<Rightarrow> 'a tree"
```
```   128 primrec
```
```   129   "mirror (Twig) = Twig "
```
```   130   "mirror (Leaf a) = Leaf a "
```
```   131   "mirror (Branch l r) = Branch (mirror r) (mirror l)"
```
```   132
```
```   133 theorem "plant (rev (leaves xt)) = mirror xt"
```
```   134   quickcheck
```
```   135     --{* Wrong! *}
```
```   136   oops
```
```   137
```
```   138 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
```
```   139   quickcheck
```
```   140     --{* Wrong! *}
```
```   141   oops
```
```   142
```
```   143 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
```
```   144
```
```   145 consts
```
```   146   inOrder :: "'a ntree \<Rightarrow> 'a list"
```
```   147 primrec
```
```   148   "inOrder (Tip a)= [a]"
```
```   149   "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
```
```   150
```
```   151 consts
```
```   152   root :: "'a ntree \<Rightarrow> 'a"
```
```   153 primrec
```
```   154   "root (Tip a) = a"
```
```   155   "root (Node f x y) = f"
```
```   156
```
```   157 theorem "hd(inOrder xt) = root xt"
```
```   158   quickcheck
```
```   159     --{* Wrong! *}
```
```   160   oops
```
```   161
```
```   162 end
```