src/HOL/ex/Quickcheck_Examples.thy
 author wenzelm Wed Sep 14 22:08:08 2005 +0200 (2005-09-14) changeset 17388 495c799df31d parent 16417 9bc16273c2d4 child 25891 1bd12187a96e permissions -rw-r--r--
tuned headers etc.;
```     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 consts
```
```    45   occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
```
```    46 primrec
```
```    47   "occurs a [] = 0"
```
```    48   "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
```
```    49
```
```    50 consts
```
```    51   del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    52 primrec
```
```    53   "del1 a [] = []"
```
```    54   "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
```
```    55
```
```    56 (* A lemma, you'd think to be true from our experience with delAll*)
```
```    57 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    58   -- {* Wrong. Precondition needed.*}
```
```    59   quickcheck
```
```    60   oops
```
```    61
```
```    62 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    63   quickcheck
```
```    64     -- {* Also wrong.*}
```
```    65   oops
```
```    66
```
```    67 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
```
```    68   quickcheck
```
```    69   apply (induct_tac xs)
```
```    70   apply auto
```
```    71     -- {* Correct! *}
```
```    72   done
```
```    73
```
```    74 consts
```
```    75   replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    76 primrec
```
```    77   "replace a b [] = []"
```
```    78   "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
```
```    79                             else (x#(replace a b xs)))"
```
```    80
```
```    81 lemma "occurs a xs = occurs b (replace a b xs)"
```
```    82   quickcheck
```
```    83   -- {* Wrong. Precondition needed.*}
```
```    84   oops
```
```    85
```
```    86 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
```
```    87   quickcheck
```
```    88   apply (induct_tac xs)
```
```    89   apply auto
```
```    90   done
```
```    91
```
```    92
```
```    93 subsection {* Trees *}
```
```    94
```
```    95 datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
```
```    96
```
```    97 consts
```
```    98   leaves :: "'a tree \<Rightarrow> 'a list"
```
```    99 primrec
```
```   100   "leaves Twig = []"
```
```   101   "leaves (Leaf a) = [a]"
```
```   102   "leaves (Branch l r) = (leaves l) @ (leaves r)"
```
```   103
```
```   104 consts
```
```   105   plant :: "'a list \<Rightarrow> 'a tree"
```
```   106 primrec
```
```   107   "plant [] = Twig "
```
```   108   "plant (x#xs) = Branch (Leaf x) (plant xs)"
```
```   109
```
```   110 consts
```
```   111   mirror :: "'a tree \<Rightarrow> 'a tree"
```
```   112 primrec
```
```   113   "mirror (Twig) = Twig "
```
```   114   "mirror (Leaf a) = Leaf a "
```
```   115   "mirror (Branch l r) = Branch (mirror r) (mirror l)"
```
```   116
```
```   117 theorem "plant (rev (leaves xt)) = mirror xt"
```
```   118   quickcheck
```
```   119     --{* Wrong! *}
```
```   120   oops
```
```   121
```
```   122 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
```
```   123   quickcheck
```
```   124     --{* Wrong! *}
```
```   125   oops
```
```   126
```
```   127 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
```
```   128
```
```   129 consts
```
```   130   inOrder :: "'a ntree \<Rightarrow> 'a list"
```
```   131 primrec
```
```   132   "inOrder (Tip a)= [a]"
```
```   133   "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
```
```   134
```
```   135 consts
```
```   136   root :: "'a ntree \<Rightarrow> 'a"
```
```   137 primrec
```
```   138   "root (Tip a) = a"
```
```   139   "root (Node f x y) = f"
```
```   140
```
```   141 theorem "hd(inOrder xt) = root xt"
```
```   142   quickcheck
```
```   143     --{* Wrong! *}
```
```   144   oops
```
```   145
```
```   146 end
```