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--
added lemmas
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@28314
     9
theory Quickcheck_Examples
haftmann@28314
    10
imports Main
haftmann@28314
    11
begin
berghofe@14592
    12
berghofe@14592
    13
text {*
berghofe@14592
    14
The 'quickcheck' command allows to find counterexamples by evaluating
berghofe@14592
    15
formulae under an assignment of free variables to random values.
berghofe@14592
    16
In contrast to 'refute', it can deal with inductive datatypes,
berghofe@14592
    17
but cannot handle quantifiers.
berghofe@14592
    18
*}
berghofe@14592
    19
berghofe@14592
    20
subsection {* Lists *}
berghofe@14592
    21
berghofe@14592
    22
theorem "map g (map f xs) = map (g o f) xs"
haftmann@28336
    23
  quickcheck
berghofe@14592
    24
  oops
berghofe@14592
    25
berghofe@14592
    26
theorem "map g (map f xs) = map (f o g) xs"
haftmann@28336
    27
  quickcheck
berghofe@14592
    28
  oops
berghofe@14592
    29
berghofe@14592
    30
theorem "rev (xs @ ys) = rev ys @ rev xs"
haftmann@28336
    31
  quickcheck
berghofe@14592
    32
  oops
berghofe@14592
    33
berghofe@14592
    34
theorem "rev (xs @ ys) = rev xs @ rev ys"
haftmann@28336
    35
  quickcheck
berghofe@14592
    36
  oops
berghofe@14592
    37
berghofe@14592
    38
theorem "rev (rev xs) = xs"
haftmann@28336
    39
  quickcheck
berghofe@14592
    40
  oops
berghofe@14592
    41
berghofe@14592
    42
theorem "rev xs = xs"
haftmann@28336
    43
  quickcheck
berghofe@14592
    44
  oops
berghofe@14592
    45
berghofe@25891
    46
text {* An example involving functions inside other data structures *}
berghofe@25891
    47
haftmann@28314
    48
primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
berghofe@25891
    49
  "app [] x = x"
haftmann@28314
    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)"
haftmann@28336
    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)"
haftmann@28336
    57
  quickcheck
berghofe@25891
    58
  oops
berghofe@25891
    59
haftmann@28314
    60
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
berghofe@14592
    61
  "occurs a [] = 0"
haftmann@28314
    62
  | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
berghofe@14592
    63
haftmann@28314
    64
primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
berghofe@14592
    65
  "del1 a [] = []"
haftmann@28314
    66
  | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
berghofe@14592
    67
berghofe@25891
    68
text {* A lemma, you'd think to be true from our experience with delAll *}
berghofe@14592
    69
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
berghofe@14592
    70
  -- {* Wrong. Precondition needed.*}
haftmann@28336
    71
  quickcheck
berghofe@14592
    72
  oops
berghofe@14592
    73
berghofe@14592
    74
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
haftmann@28336
    75
  quickcheck
berghofe@14592
    76
    -- {* Also wrong.*}
berghofe@14592
    77
  oops
berghofe@14592
    78
berghofe@14592
    79
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
haftmann@28336
    80
  quickcheck
haftmann@28314
    81
  by (induct xs) auto
berghofe@14592
    82
haftmann@28314
    83
primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
berghofe@14592
    84
  "replace a b [] = []"
haftmann@28314
    85
  | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
berghofe@14592
    86
                            else (x#(replace a b xs)))"
berghofe@14592
    87
berghofe@14592
    88
lemma "occurs a xs = occurs b (replace a b xs)"
haftmann@28336
    89
  quickcheck
berghofe@14592
    90
  -- {* Wrong. Precondition needed.*}
berghofe@14592
    91
  oops
berghofe@14592
    92
berghofe@14592
    93
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
haftmann@28336
    94
  quickcheck
haftmann@28314
    95
  by (induct xs) simp_all
berghofe@14592
    96
berghofe@14592
    97
berghofe@14592
    98
subsection {* Trees *}
berghofe@14592
    99
berghofe@14592
   100
datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
berghofe@14592
   101
haftmann@28314
   102
primrec leaves :: "'a tree \<Rightarrow> 'a list" where
berghofe@14592
   103
  "leaves Twig = []"
haftmann@28314
   104
  | "leaves (Leaf a) = [a]"
haftmann@28314
   105
  | "leaves (Branch l r) = (leaves l) @ (leaves r)"
berghofe@14592
   106
haftmann@28314
   107
primrec plant :: "'a list \<Rightarrow> 'a tree" where
berghofe@14592
   108
  "plant [] = Twig "
haftmann@28314
   109
  | "plant (x#xs) = Branch (Leaf x) (plant xs)"
berghofe@14592
   110
haftmann@28314
   111
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
berghofe@14592
   112
  "mirror (Twig) = Twig "
haftmann@28314
   113
  | "mirror (Leaf a) = Leaf a "
haftmann@28314
   114
  | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
berghofe@14592
   115
berghofe@14592
   116
theorem "plant (rev (leaves xt)) = mirror xt"
haftmann@28336
   117
  quickcheck
berghofe@14592
   118
    --{* Wrong! *} 
berghofe@14592
   119
  oops
berghofe@14592
   120
berghofe@14592
   121
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
haftmann@28336
   122
  quickcheck
berghofe@14592
   123
    --{* Wrong! *} 
berghofe@14592
   124
  oops
berghofe@14592
   125
berghofe@14592
   126
datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
berghofe@14592
   127
haftmann@28314
   128
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
berghofe@14592
   129
  "inOrder (Tip a)= [a]"
haftmann@28314
   130
  | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
berghofe@14592
   131
haftmann@28314
   132
primrec root :: "'a ntree \<Rightarrow> 'a" where
berghofe@14592
   133
  "root (Tip a) = a"
haftmann@28314
   134
  | "root (Node f x y) = f"
berghofe@14592
   135
haftmann@28314
   136
theorem "hd (inOrder xt) = root xt"
haftmann@28336
   137
  quickcheck
berghofe@14592
   138
    --{* Wrong! *} 
berghofe@14592
   139
  oops
berghofe@14592
   140
berghofe@14592
   141
end