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