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
     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