src/HOL/ex/Quickcheck_Examples.thy
changeset 14592 dd1a2905ea73
child 16417 9bc16273c2d4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Apr 16 18:09:24 2004 +0200
     1.3 @@ -0,0 +1,148 @@
     1.4 +(*  Title:      HOL/ex/Quickcheck_Examples.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer
     1.7 +    Copyright   2004 TU Muenchen
     1.8 +*)
     1.9 +
    1.10 +header {* Examples for the 'quickcheck' command *}
    1.11 +
    1.12 +theory Quickcheck_Examples = Main:
    1.13 +
    1.14 +text {*
    1.15 +The 'quickcheck' command allows to find counterexamples by evaluating
    1.16 +formulae under an assignment of free variables to random values.
    1.17 +In contrast to 'refute', it can deal with inductive datatypes,
    1.18 +but cannot handle quantifiers.
    1.19 +*}
    1.20 +
    1.21 +subsection {* Lists *}
    1.22 +
    1.23 +theorem "map g (map f xs) = map (g o f) xs"
    1.24 +  quickcheck
    1.25 +  oops
    1.26 +
    1.27 +theorem "map g (map f xs) = map (f o g) xs"
    1.28 +  quickcheck
    1.29 +  oops
    1.30 +
    1.31 +theorem "rev (xs @ ys) = rev ys @ rev xs"
    1.32 +  quickcheck
    1.33 +  oops
    1.34 +
    1.35 +theorem "rev (xs @ ys) = rev xs @ rev ys"
    1.36 +  quickcheck
    1.37 +  oops
    1.38 +
    1.39 +theorem "rev (rev xs) = xs"
    1.40 +  quickcheck
    1.41 +  oops
    1.42 +
    1.43 +theorem "rev xs = xs"
    1.44 +  quickcheck
    1.45 +  oops
    1.46 +
    1.47 +consts
    1.48 +  occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
    1.49 +primrec
    1.50 +  "occurs a [] = 0"
    1.51 +  "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
    1.52 +
    1.53 +consts
    1.54 +  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.55 +primrec
    1.56 +  "del1 a [] = []"
    1.57 +  "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
    1.58 +
    1.59 +(* A lemma, you'd think to be true from our experience with delAll*)
    1.60 +lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
    1.61 +  -- {* Wrong. Precondition needed.*}
    1.62 +  quickcheck
    1.63 +  oops
    1.64 +
    1.65 +lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    1.66 +  quickcheck
    1.67 +    -- {* Also wrong.*}
    1.68 +  oops
    1.69 +
    1.70 +lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    1.71 +  quickcheck
    1.72 +  apply (induct_tac xs)  
    1.73 +  apply auto
    1.74 +    -- {* Correct! *}
    1.75 +  done
    1.76 +
    1.77 +consts
    1.78 +  replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.79 +primrec
    1.80 +  "replace a b [] = []"
    1.81 +  "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
    1.82 +                            else (x#(replace a b xs)))"
    1.83 +
    1.84 +lemma "occurs a xs = occurs b (replace a b xs)"
    1.85 +  quickcheck
    1.86 +  -- {* Wrong. Precondition needed.*}
    1.87 +  oops
    1.88 +
    1.89 +lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
    1.90 +  quickcheck
    1.91 +  apply (induct_tac xs)  
    1.92 +  apply auto
    1.93 +  done
    1.94 +
    1.95 +
    1.96 +subsection {* Trees *}
    1.97 +
    1.98 +datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
    1.99 +
   1.100 +consts
   1.101 +  leaves :: "'a tree \<Rightarrow> 'a list"
   1.102 +primrec
   1.103 +  "leaves Twig = []"
   1.104 +  "leaves (Leaf a) = [a]"
   1.105 +  "leaves (Branch l r) = (leaves l) @ (leaves r)"
   1.106 +
   1.107 +consts
   1.108 +  plant :: "'a list \<Rightarrow> 'a tree"
   1.109 +primrec
   1.110 +  "plant [] = Twig "
   1.111 +  "plant (x#xs) = Branch (Leaf x) (plant xs)"
   1.112 +
   1.113 +consts
   1.114 +  mirror :: "'a tree \<Rightarrow> 'a tree"
   1.115 +primrec
   1.116 +  "mirror (Twig) = Twig "
   1.117 +  "mirror (Leaf a) = Leaf a "
   1.118 +  "mirror (Branch l r) = Branch (mirror r) (mirror l)"
   1.119 +
   1.120 +theorem "plant (rev (leaves xt)) = mirror xt"
   1.121 +  quickcheck
   1.122 +    --{* Wrong! *} 
   1.123 +  oops
   1.124 +
   1.125 +theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
   1.126 +  quickcheck
   1.127 +    --{* Wrong! *} 
   1.128 +  oops
   1.129 +
   1.130 +datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
   1.131 +
   1.132 +consts
   1.133 +  inOrder :: "'a ntree \<Rightarrow> 'a list"
   1.134 +primrec
   1.135 +  "inOrder (Tip a)= [a]"
   1.136 +  "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
   1.137 +
   1.138 +consts
   1.139 +  root :: "'a ntree \<Rightarrow> 'a"
   1.140 +primrec
   1.141 +  "root (Tip a) = a"
   1.142 +  "root (Node f x y) = f"
   1.143 +
   1.144 +theorem "hd(inOrder xt) = root xt"
   1.145 +  quickcheck
   1.146 +    --{* Wrong! *} 
   1.147 +  oops
   1.148 +
   1.149 +end
   1.150 +
   1.151 +