1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy Mon Sep 22 13:56:01 2008 +0200
1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy Mon Sep 22 13:56:03 2008 +0200
1.3 @@ -6,7 +6,9 @@
1.4
1.5 header {* Examples for the 'quickcheck' command *}
1.6
1.7 -theory Quickcheck_Examples imports Main begin
1.8 +theory Quickcheck_Examples
1.9 +imports Main
1.10 +begin
1.11
1.12 text {*
1.13 The 'quickcheck' command allows to find counterexamples by evaluating
1.14 @@ -18,144 +20,121 @@
1.15 subsection {* Lists *}
1.16
1.17 theorem "map g (map f xs) = map (g o f) xs"
1.18 - quickcheck
1.19 + quickcheck []
1.20 oops
1.21
1.22 theorem "map g (map f xs) = map (f o g) xs"
1.23 - quickcheck
1.24 + quickcheck []
1.25 oops
1.26
1.27 theorem "rev (xs @ ys) = rev ys @ rev xs"
1.28 - quickcheck
1.29 + quickcheck []
1.30 oops
1.31
1.32 theorem "rev (xs @ ys) = rev xs @ rev ys"
1.33 - quickcheck
1.34 + quickcheck []
1.35 oops
1.36
1.37 theorem "rev (rev xs) = xs"
1.38 - quickcheck
1.39 + quickcheck []
1.40 oops
1.41
1.42 theorem "rev xs = xs"
1.43 - quickcheck
1.44 + quickcheck []
1.45 oops
1.46
1.47 text {* An example involving functions inside other data structures *}
1.48
1.49 -consts app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a"
1.50 -
1.51 -primrec
1.52 +primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
1.53 "app [] x = x"
1.54 - "app (f # fs) x = app fs (f x)"
1.55 + | "app (f # fs) x = app fs (f x)"
1.56
1.57 lemma "app (fs @ gs) x = app gs (app fs x)"
1.58 - quickcheck
1.59 + quickcheck []
1.60 by (induct fs arbitrary: x) simp_all
1.61
1.62 lemma "app (fs @ gs) x = app fs (app gs x)"
1.63 - quickcheck
1.64 + quickcheck []
1.65 oops
1.66
1.67 -consts
1.68 - occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
1.69 -primrec
1.70 +primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
1.71 "occurs a [] = 0"
1.72 - "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
1.73 + | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
1.74
1.75 -consts
1.76 - del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.77 -primrec
1.78 +primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.79 "del1 a [] = []"
1.80 - "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
1.81 + | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
1.82
1.83 text {* A lemma, you'd think to be true from our experience with delAll *}
1.84 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
1.85 -- {* Wrong. Precondition needed.*}
1.86 - quickcheck
1.87 + quickcheck []
1.88 oops
1.89
1.90 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
1.91 - quickcheck
1.92 + quickcheck []
1.93 -- {* Also wrong.*}
1.94 oops
1.95
1.96 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
1.97 - quickcheck
1.98 - apply (induct_tac xs)
1.99 - apply auto
1.100 - -- {* Correct! *}
1.101 - done
1.102 + quickcheck []
1.103 + by (induct xs) auto
1.104
1.105 -consts
1.106 - replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.107 -primrec
1.108 +primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.109 "replace a b [] = []"
1.110 - "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
1.111 + | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
1.112 else (x#(replace a b xs)))"
1.113
1.114 lemma "occurs a xs = occurs b (replace a b xs)"
1.115 - quickcheck
1.116 + quickcheck []
1.117 -- {* Wrong. Precondition needed.*}
1.118 oops
1.119
1.120 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
1.121 - quickcheck
1.122 - apply (induct_tac xs)
1.123 - apply auto
1.124 - done
1.125 + quickcheck []
1.126 + by (induct xs) simp_all
1.127
1.128
1.129 subsection {* Trees *}
1.130
1.131 datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
1.132
1.133 -consts
1.134 - leaves :: "'a tree \<Rightarrow> 'a list"
1.135 -primrec
1.136 +primrec leaves :: "'a tree \<Rightarrow> 'a list" where
1.137 "leaves Twig = []"
1.138 - "leaves (Leaf a) = [a]"
1.139 - "leaves (Branch l r) = (leaves l) @ (leaves r)"
1.140 + | "leaves (Leaf a) = [a]"
1.141 + | "leaves (Branch l r) = (leaves l) @ (leaves r)"
1.142
1.143 -consts
1.144 - plant :: "'a list \<Rightarrow> 'a tree"
1.145 -primrec
1.146 +primrec plant :: "'a list \<Rightarrow> 'a tree" where
1.147 "plant [] = Twig "
1.148 - "plant (x#xs) = Branch (Leaf x) (plant xs)"
1.149 + | "plant (x#xs) = Branch (Leaf x) (plant xs)"
1.150
1.151 -consts
1.152 - mirror :: "'a tree \<Rightarrow> 'a tree"
1.153 -primrec
1.154 +primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
1.155 "mirror (Twig) = Twig "
1.156 - "mirror (Leaf a) = Leaf a "
1.157 - "mirror (Branch l r) = Branch (mirror r) (mirror l)"
1.158 + | "mirror (Leaf a) = Leaf a "
1.159 + | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
1.160
1.161 theorem "plant (rev (leaves xt)) = mirror xt"
1.162 - quickcheck
1.163 + quickcheck []
1.164 --{* Wrong! *}
1.165 oops
1.166
1.167 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
1.168 - quickcheck
1.169 + quickcheck []
1.170 --{* Wrong! *}
1.171 oops
1.172
1.173 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
1.174
1.175 -consts
1.176 - inOrder :: "'a ntree \<Rightarrow> 'a list"
1.177 -primrec
1.178 +primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
1.179 "inOrder (Tip a)= [a]"
1.180 - "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
1.181 + | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
1.182
1.183 -consts
1.184 - root :: "'a ntree \<Rightarrow> 'a"
1.185 -primrec
1.186 +primrec root :: "'a ntree \<Rightarrow> 'a" where
1.187 "root (Tip a) = a"
1.188 - "root (Node f x y) = f"
1.189 + | "root (Node f x y) = f"
1.190
1.191 -theorem "hd(inOrder xt) = root xt"
1.192 - quickcheck
1.193 +theorem "hd (inOrder xt) = root xt"
1.194 + quickcheck []
1.195 --{* Wrong! *}
1.196 oops
1.197