src/HOL/ex/Quickcheck_Examples.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 14592 dd1a2905ea73
child 17388 495c799df31d
permissions -rw-r--r--
migrated theory headers to new format
     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
   147 
   148