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