author  wenzelm 
Wed, 29 Oct 2014 11:19:27 +0100  
changeset 58813  625d04d4fd2a 
parent 58310  91ea607a34d8 
child 58889  5b7a9633cfa8 
permissions  rwrr 
46879  1 
(* Title: HOL/Quickcheck_Examples/Quickcheck_Examples.thy 
40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

2 
Author: Stefan Berghofer, Lukas Bulwahn 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

3 
Copyright 2004  2010 TU Muenchen 
14592  4 
*) 
5 

6 
header {* Examples for the 'quickcheck' command *} 

7 

28314  8 
theory Quickcheck_Examples 
57645  9 
imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset" 
28314  10 
begin 
14592  11 

12 
text {* 

13 
The 'quickcheck' command allows to find counterexamples by evaluating 

40654  14 
formulae. 
15 
Currently, there are two different exploration schemes: 

16 
 random testing: this is incomplete, but explores the search space faster. 

17 
 exhaustive testing: this is complete, but increasing the depth leads to 

18 
exponentially many assignments. 

19 

20 
quickcheck can handle quantifiers on finite universes. 

21 

14592  22 
*} 
23 

43803  24 
declare [[quickcheck_timeout = 3600]] 
25 

14592  26 
subsection {* Lists *} 
27 

28 
theorem "map g (map f xs) = map (g o f) xs" 

40917  29 
quickcheck[random, expect = no_counterexample] 
30 
quickcheck[exhaustive, size = 3, expect = no_counterexample] 

14592  31 
oops 
32 

33 
theorem "map g (map f xs) = map (f o g) xs" 

40917  34 
quickcheck[random, expect = counterexample] 
35 
quickcheck[exhaustive, expect = counterexample] 

14592  36 
oops 
37 

38 
theorem "rev (xs @ ys) = rev ys @ rev xs" 

40917  39 
quickcheck[random, expect = no_counterexample] 
40 
quickcheck[exhaustive, expect = no_counterexample] 

42087
5e236f6ef04f
changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
bulwahn
parents:
41231
diff
changeset

41 
quickcheck[exhaustive, size = 1000, timeout = 0.1] 
14592  42 
oops 
43 

44 
theorem "rev (xs @ ys) = rev xs @ rev ys" 

40917  45 
quickcheck[random, expect = counterexample] 
46 
quickcheck[exhaustive, expect = counterexample] 

14592  47 
oops 
48 

49 
theorem "rev (rev xs) = xs" 

40917  50 
quickcheck[random, expect = no_counterexample] 
51 
quickcheck[exhaustive, expect = no_counterexample] 

14592  52 
oops 
53 

54 
theorem "rev xs = xs" 

42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

55 
quickcheck[tester = random, finite_types = true, report = false, expect = counterexample] 
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

56 
quickcheck[tester = random, finite_types = false, report = false, expect = counterexample] 
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

57 
quickcheck[tester = random, finite_types = true, report = true, expect = counterexample] 
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

58 
quickcheck[tester = random, finite_types = false, report = true, expect = counterexample] 
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

59 
quickcheck[tester = exhaustive, finite_types = true, expect = counterexample] 
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

60 
quickcheck[tester = exhaustive, finite_types = false, expect = counterexample] 
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

61 
oops 
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42087
diff
changeset

62 

14592  63 

25891  64 
text {* An example involving functions inside other data structures *} 
65 

28314  66 
primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where 
25891  67 
"app [] x = x" 
28314  68 
 "app (f # fs) x = app fs (f x)" 
25891  69 

70 
lemma "app (fs @ gs) x = app gs (app fs x)" 

40917  71 
quickcheck[random, expect = no_counterexample] 
47348
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

72 
quickcheck[exhaustive, size = 2, expect = no_counterexample] 
25891  73 
by (induct fs arbitrary: x) simp_all 
74 

75 
lemma "app (fs @ gs) x = app fs (app gs x)" 

40917  76 
quickcheck[random, expect = counterexample] 
77 
quickcheck[exhaustive, expect = counterexample] 

25891  78 
oops 
79 

28314  80 
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where 
14592  81 
"occurs a [] = 0" 
28314  82 
 "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" 
14592  83 

28314  84 
primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
14592  85 
"del1 a [] = []" 
28314  86 
 "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" 
14592  87 

25891  88 
text {* A lemma, you'd think to be true from our experience with delAll *} 
14592  89 
lemma "Suc (occurs a (del1 a xs)) = occurs a xs" 
90 
 {* Wrong. Precondition needed.*} 

40917  91 
quickcheck[random, expect = counterexample] 
92 
quickcheck[exhaustive, expect = counterexample] 

14592  93 
oops 
94 

95 
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" 

40917  96 
quickcheck[random, expect = counterexample] 
97 
quickcheck[exhaustive, expect = counterexample] 

14592  98 
 {* Also wrong.*} 
99 
oops 

100 

101 
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" 

40917  102 
quickcheck[random, expect = no_counterexample] 
103 
quickcheck[exhaustive, expect = no_counterexample] 

28314  104 
by (induct xs) auto 
14592  105 

28314  106 
primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
14592  107 
"replace a b [] = []" 
28314  108 
 "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
14592  109 
else (x#(replace a b xs)))" 
110 

111 
lemma "occurs a xs = occurs b (replace a b xs)" 

40917  112 
quickcheck[random, expect = counterexample] 
113 
quickcheck[exhaustive, expect = counterexample] 

14592  114 
 {* Wrong. Precondition needed.*} 
115 
oops 

116 

117 
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)" 

40917  118 
quickcheck[random, expect = no_counterexample] 
119 
quickcheck[exhaustive, expect = no_counterexample] 

28314  120 
by (induct xs) simp_all 
14592  121 

122 

123 
subsection {* Trees *} 

124 

58310  125 
datatype 'a tree = Twig  Leaf 'a  Branch "'a tree" "'a tree" 
14592  126 

28314  127 
primrec leaves :: "'a tree \<Rightarrow> 'a list" where 
14592  128 
"leaves Twig = []" 
28314  129 
 "leaves (Leaf a) = [a]" 
130 
 "leaves (Branch l r) = (leaves l) @ (leaves r)" 

14592  131 

28314  132 
primrec plant :: "'a list \<Rightarrow> 'a tree" where 
14592  133 
"plant [] = Twig " 
28314  134 
 "plant (x#xs) = Branch (Leaf x) (plant xs)" 
14592  135 

28314  136 
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where 
14592  137 
"mirror (Twig) = Twig " 
28314  138 
 "mirror (Leaf a) = Leaf a " 
139 
 "mirror (Branch l r) = Branch (mirror r) (mirror l)" 

14592  140 

141 
theorem "plant (rev (leaves xt)) = mirror xt" 

40917  142 
quickcheck[random, expect = counterexample] 
143 
quickcheck[exhaustive, expect = counterexample] 

14592  144 
{* Wrong! *} 
145 
oops 

146 

147 
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt" 

40917  148 
quickcheck[random, expect = counterexample] 
149 
quickcheck[exhaustive, expect = counterexample] 

14592  150 
{* Wrong! *} 
151 
oops 

152 

58310  153 
datatype 'a ntree = Tip "'a"  Node "'a" "'a ntree" "'a ntree" 
14592  154 

28314  155 
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where 
14592  156 
"inOrder (Tip a)= [a]" 
28314  157 
 "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" 
14592  158 

28314  159 
primrec root :: "'a ntree \<Rightarrow> 'a" where 
14592  160 
"root (Tip a) = a" 
28314  161 
 "root (Node f x y) = f" 
14592  162 

28314  163 
theorem "hd (inOrder xt) = root xt" 
40917  164 
quickcheck[random, expect = counterexample] 
165 
quickcheck[exhaustive, expect = counterexample] 

166 
{* Wrong! *} 

14592  167 
oops 
168 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

169 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

170 
subsection {* Exhaustive Testing beats Random Testing *} 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

171 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

172 
text {* Here are some examples from mutants from the List theory 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

173 
where exhaustive testing beats random testing *} 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

174 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

175 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

176 
"[] ~= xs ==> hd xs = last (x # xs)" 
40917  177 
quickcheck[random] 
178 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

179 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

180 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

181 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

182 
assumes "!!i. [ i < n; i < length xs ] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)" 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

183 
shows "drop n xs = takeWhile P xs" 
40917  184 
quickcheck[random, iterations = 10000, quiet] 
185 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

186 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

187 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

188 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

189 
"i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<xs. i < length ys]" 
40917  190 
quickcheck[random, iterations = 10000] 
191 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

192 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

193 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

194 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

195 
"i < n  m ==> f (lcm m i) = map f [m..<n] ! i" 
40917  196 
quickcheck[random, iterations = 10000, finite_types = false] 
197 
quickcheck[exhaustive, finite_types = false, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

198 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

199 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

200 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

201 
"i < n  m ==> f (lcm m i) = map f [m..<n] ! i" 
40917  202 
quickcheck[random, iterations = 10000, finite_types = false] 
203 
quickcheck[exhaustive, finite_types = false, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

204 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

205 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

206 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

207 
"ns ! k < length ns ==> k <= listsum ns" 
40917  208 
quickcheck[random, iterations = 10000, finite_types = false, quiet] 
209 
quickcheck[exhaustive, finite_types = false, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

210 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

211 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

212 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

213 
"[ ys = x # xs1; zs = xs1 @ xs ] ==> ys @ zs = x # xs" 
40917  214 
quickcheck[random, iterations = 10000] 
215 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

216 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

217 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

218 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

219 
"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs" 
40917  220 
quickcheck[random, iterations = 10000] 
221 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

222 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

223 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

224 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

225 
"i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []" 
40917  226 
quickcheck[random, iterations = 10000] 
227 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

228 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

229 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

230 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

231 
"[ sorted (rev (map length xs)); i < length xs ] ==> xs ! i = map (%ys. ys ! i) [ys<remdups xs. i < length ys]" 
40917  232 
quickcheck[random] 
233 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

234 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

235 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

236 
lemma 
44189
4a80017c733f
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
huffman
parents:
43909
diff
changeset

237 
"[ sorted (rev (map length xs)); i < length xs ] ==> xs ! i = map (%ys. ys ! i) [ys<List.transpose xs. length ys \<in> {..<i}]" 
40917  238 
quickcheck[random] 
239 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

240 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

241 

03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

242 
lemma 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

243 
"(ys = zs) = (xs @ ys = splice xs zs)" 
40917  244 
quickcheck[random] 
245 
quickcheck[exhaustive, expect = counterexample] 

40645
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

246 
oops 
03ce94672ee6
adding test cases for smallcheck and adding examples where exhaustive testing is more successful
bulwahn
parents:
37929
diff
changeset

247 

46672
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

248 
subsection {* Random Testing beats Exhaustive Testing *} 
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

249 

3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

250 
lemma mult_inj_if_coprime_nat: 
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

251 
"inj_on f A \<Longrightarrow> inj_on g B 
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

252 
\<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)" 
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

253 
quickcheck[exhaustive] 
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

254 
quickcheck[random] 
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

255 
oops 
3fc49e6998da
adding an example where random beats exhaustive testing
bulwahn
parents:
46585
diff
changeset

256 

41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

257 
subsection {* Examples with quantifiers *} 
40654  258 

259 
text {* 

260 
These examples show that we can handle quantifiers. 

261 
*} 

262 

263 
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)" 

40917  264 
quickcheck[random, expect = counterexample] 
265 
quickcheck[exhaustive, expect = counterexample] 

40654  266 
oops 
267 

268 
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)" 

40917  269 
quickcheck[random, expect = counterexample] 
40654  270 
quickcheck[expect = counterexample] 
271 
oops 

272 

273 
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)" 

40917  274 
quickcheck[random, expect = counterexample] 
40654  275 
quickcheck[expect = counterexample] 
276 
oops 

277 

45118
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

278 

46397  279 
subsection {* Examples with sets *} 
280 

281 
lemma 

282 
"{} = A Un  A" 

283 
quickcheck[exhaustive, expect = counterexample] 

284 
oops 

285 

46421
5ab496224729
adding a quickcheck example about functions and sets
bulwahn
parents:
46397
diff
changeset

286 
lemma 
5ab496224729
adding a quickcheck example about functions and sets
bulwahn
parents:
46397
diff
changeset

287 
"[ bij_betw f A B; bij_betw f C D ] ==> bij_betw f (A Un C) (B Un D)" 
5ab496224729
adding a quickcheck example about functions and sets
bulwahn
parents:
46397
diff
changeset

288 
quickcheck[exhaustive, expect = counterexample] 
5ab496224729
adding a quickcheck example about functions and sets
bulwahn
parents:
46397
diff
changeset

289 
oops 
5ab496224729
adding a quickcheck example about functions and sets
bulwahn
parents:
46397
diff
changeset

290 

46397  291 

45118
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

292 
subsection {* Examples with relations *} 
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

293 

7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

294 
lemma 
46348
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

295 
"acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)" 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

296 
quickcheck[exhaustive, expect = counterexample] 
45118
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

297 
oops 
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

298 

7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

299 
lemma 
46348
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

300 
"acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)" 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

301 
quickcheck[exhaustive, expect = counterexample] 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

302 
oops 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

303 

ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

304 
(* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *) 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

305 
lemma 
45118
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

306 
"(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S" 
46348
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

307 
(*quickcheck[exhaustive, expect = counterexample]*) 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

308 
oops 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

309 

ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

310 
lemma 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

311 
"wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)" 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

312 
quickcheck[exhaustive, expect = counterexample] 
45118
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

313 
oops 
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

314 

46348
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

315 
lemma 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

316 
"wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)" 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

317 
quickcheck[exhaustive, expect = counterexample] 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

318 
oops 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

319 

ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

320 
lemma 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

321 
"wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)" 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

322 
quickcheck[exhaustive, expect = counterexample] 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

323 
oops 
ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

324 

ee5009212793
adding some more examples for quickcheck; replaced FIXME comments
bulwahn
parents:
46344
diff
changeset

325 

46337  326 
subsection {* Examples with the descriptive operator *} 
327 

328 
lemma 

329 
"(THE x. x = a) = b" 

330 
quickcheck[random, expect = counterexample] 

331 
quickcheck[exhaustive, expect = counterexample] 

332 
oops 

333 

46169  334 
subsection {* Examples with Multisets *} 
335 

336 
lemma 

337 
"X + Y = Y + (Z :: 'a multiset)" 

338 
quickcheck[random, expect = counterexample] 

339 
quickcheck[exhaustive, expect = counterexample] 

340 
oops 

341 

342 
lemma 

343 
"X  Y = Y  (Z :: 'a multiset)" 

344 
quickcheck[random, expect = counterexample] 

345 
quickcheck[exhaustive, expect = counterexample] 

346 
oops 

347 

348 
lemma 

349 
"N + M  N = (N::'a multiset)" 

350 
quickcheck[random, expect = counterexample] 

351 
quickcheck[exhaustive, expect = counterexample] 

352 
oops 

45118
7462f287189a
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
bulwahn
parents:
44189
diff
changeset

353 

41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

354 
subsection {* Examples with numerical types *} 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

355 

2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

356 
text {* 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

357 
Quickcheck supports the common types nat, int, rat and real. 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

358 
*} 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

359 

2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

360 
lemma 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

361 
"(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z" 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

362 
quickcheck[exhaustive, size = 10, expect = counterexample] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

363 
quickcheck[random, size = 10] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

364 
oops 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

365 

2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

366 
lemma 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

367 
"(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z" 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

368 
quickcheck[exhaustive, size = 10, expect = counterexample] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

369 
quickcheck[random, size = 10] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

370 
oops 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

371 

2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

372 
lemma 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

373 
"(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z" 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

374 
quickcheck[exhaustive, size = 10, expect = counterexample] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

375 
quickcheck[random, size = 10] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

376 
oops 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

377 

45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

378 
lemma "(x :: rat) >= 0" 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

379 
quickcheck[random, expect = counterexample] 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

380 
quickcheck[exhaustive, expect = counterexample] 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

381 
oops 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

382 

41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

383 
lemma 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

384 
"(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z" 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

385 
quickcheck[exhaustive, size = 10, expect = counterexample] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

386 
quickcheck[random, size = 10] 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

387 
oops 
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
40917
diff
changeset

388 

45507
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

389 
lemma "(x :: real) >= 0" 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

390 
quickcheck[random, expect = counterexample] 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

391 
quickcheck[exhaustive, expect = counterexample] 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

392 
oops 
6975db7fd6f0
improved generators for rational numbers to generate negative numbers;
bulwahn
parents:
45441
diff
changeset

393 

43734
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

394 
subsubsection {* floor and ceiling functions *} 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

395 

ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

396 
lemma 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

397 
"floor x + floor y = floor (x + y :: rat)" 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

398 
quickcheck[expect = counterexample] 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

399 
oops 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

400 

ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

401 
lemma 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

402 
"floor x + floor y = floor (x + y :: real)" 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

403 
quickcheck[expect = counterexample] 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

404 
oops 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

405 

ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

406 
lemma 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

407 
"ceiling x + ceiling y = ceiling (x + y :: rat)" 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

408 
quickcheck[expect = counterexample] 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

409 
oops 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

410 

ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

411 
lemma 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

412 
"ceiling x + ceiling y = ceiling (x + y :: real)" 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

413 
quickcheck[expect = counterexample] 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

414 
oops 
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

415 

45927
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

416 
subsection {* Examples with abstract types *} 
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

417 

e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

418 
lemma 
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

419 
"Dlist.length (Dlist.remove x xs) = Dlist.length xs  1" 
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

420 
quickcheck[exhaustive] 
45942  421 
quickcheck[random] 
45927
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

422 
oops 
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

423 

e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

424 
lemma 
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

425 
"Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1" 
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

426 
quickcheck[exhaustive] 
45942  427 
quickcheck[random] 
45927
e0305e4f02c9
adding quickcheck generator for distinct lists; adding examples
bulwahn
parents:
45765
diff
changeset

428 
oops 
43734
ea147bec4f72
adding quickcheck examples for evaluating floor and ceiling functions
bulwahn
parents:
42696
diff
changeset

429 

42696
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

430 
subsection {* Examples with Records *} 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

431 

7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

432 
record point = 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

433 
xpos :: nat 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

434 
ypos :: nat 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

435 

7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

436 
lemma 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

437 
"xpos r = xpos r' ==> r = r'" 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

438 
quickcheck[exhaustive, expect = counterexample] 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

439 
quickcheck[random, expect = counterexample] 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

440 
oops 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

441 

58310  442 
datatype colour = Red  Green  Blue 
42696
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

443 

7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

444 
record cpoint = point + 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

445 
colour :: colour 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

446 

7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

447 
lemma 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

448 
"xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'" 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

449 
quickcheck[exhaustive, expect = counterexample] 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

450 
quickcheck[random, expect = counterexample] 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

451 
oops 
7c7ca3fc7ce5
adding examples for invoking quickcheck with records
bulwahn
parents:
42434
diff
changeset

452 

42434
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

453 
subsection {* Examples with locales *} 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

454 

1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

455 
locale Truth 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

456 

1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

457 
context Truth 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

458 
begin 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

459 

1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

460 
lemma "False" 
46344
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

461 
quickcheck[exhaustive, expect = counterexample] 
42434
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

462 
oops 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

463 

14592  464 
end 
42434
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

465 

1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

466 
interpretation Truth . 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

467 

1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

468 
context Truth 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

469 
begin 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

470 

1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

471 
lemma "False" 
43890  472 
quickcheck[exhaustive, expect = counterexample] 
42434
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

473 
oops 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

474 

1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

475 
end 
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

476 

46344
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

477 
locale antisym = 
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

478 
fixes R 
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

479 
assumes "R x y > R y x > x = y" 
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

480 

47348
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

481 
interpretation equal : antisym "op =" by default simp 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

482 
interpretation order_nat : antisym "op <= :: nat => _ => _" by default simp 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

483 

9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

484 
lemma (in antisym) 
46344
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

485 
"R x y > R y z > R x z" 
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

486 
quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample] 
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

487 
quickcheck[exhaustive, expect = counterexample] 
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

488 
oops 
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

489 

47348
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

490 
declare [[quickcheck_locale = "interpret"]] 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

491 

9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

492 
lemma (in antisym) 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

493 
"R x y > R y z > R x z" 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

494 
quickcheck[exhaustive, expect = no_counterexample] 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

495 
oops 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

496 

9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

497 
declare [[quickcheck_locale = "expand"]] 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

498 

9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

499 
lemma (in antisym) 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

500 
"R x y > R y z > R x z" 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

501 
quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample] 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

502 
quickcheck[exhaustive, expect = counterexample] 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

503 
oops 
9a82999ebbd6
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
bulwahn
parents:
46879
diff
changeset

504 

46344
b6fbdd3d0915
corrected expectation; added an example for quickcheck
bulwahn
parents:
46337
diff
changeset

505 

45441
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

506 
subsection {* Examples with HOL quantifiers *} 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

507 

fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

508 
lemma 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

509 
"\<forall> xs ys. xs = [] > xs = ys" 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

510 
quickcheck[exhaustive, expect = counterexample] 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

511 
oops 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

512 

fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

513 
lemma 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

514 
"ys = [] > (\<forall>xs. xs = [] > xs = y # ys)" 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

515 
quickcheck[exhaustive, expect = counterexample] 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

516 
oops 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

517 

fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

518 
lemma 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

519 
"\<forall>xs. (\<exists> ys. ys = []) > xs = ys" 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

520 
quickcheck[exhaustive, expect = counterexample] 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

521 
oops 
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

522 

45684
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

523 
subsection {* Examples with underspecified/partial functions *} 
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

524 

3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

525 
lemma 
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

526 
"xs = [] ==> hd xs \<noteq> x" 
45762
daf57640d4df
the reporting random testing also returns if the counterexample is genuine or potentially spurious
bulwahn
parents:
45720
diff
changeset

527 
quickcheck[exhaustive, expect = no_counterexample] 
daf57640d4df
the reporting random testing also returns if the counterexample is genuine or potentially spurious
bulwahn
parents:
45720
diff
changeset

528 
quickcheck[random, report = false, expect = no_counterexample] 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

529 
quickcheck[random, report = true, expect = no_counterexample] 
45684
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

530 
oops 
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

531 

3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

532 
lemma 
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

533 
"xs = [] ==> hd xs = x" 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

534 
quickcheck[exhaustive, expect = no_counterexample] 
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

535 
quickcheck[random, report = false, expect = no_counterexample] 
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

536 
quickcheck[random, report = true, expect = no_counterexample] 
45684
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

537 
oops 
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

538 

3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

539 
lemma "xs = [] ==> hd xs = x ==> x = y" 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

540 
quickcheck[exhaustive, expect = no_counterexample] 
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

541 
quickcheck[random, report = false, expect = no_counterexample] 
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

542 
quickcheck[random, report = true, expect = no_counterexample] 
45684
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

543 
oops 
3d6ee9c7d7ef
adding a exceptionsafe term reification step in quickcheck; adding examples
bulwahn
parents:
45507
diff
changeset

544 

45689
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

545 
text {* with the simple testing scheme *} 
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

546 

58813  547 
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation 
45689
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

548 
declare [[quickcheck_full_support = false]] 
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

549 

4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

550 
lemma 
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

551 
"xs = [] ==> hd xs \<noteq> x" 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

552 
quickcheck[exhaustive, expect = no_counterexample] 
45689
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

553 
oops 
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

554 

4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

555 
lemma 
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

556 
"xs = [] ==> hd xs = x" 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

557 
quickcheck[exhaustive, expect = no_counterexample] 
45689
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

558 
oops 
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

559 

4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

560 
lemma "xs = [] ==> hd xs = x ==> x = y" 
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45762
diff
changeset

561 
quickcheck[exhaustive, expect = no_counterexample] 
45689
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

562 
oops 
4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

563 

4c25ba9f3c23
adding examples for the potential counterexamples in the simple scheme
bulwahn
parents:
45684
diff
changeset

564 
declare [[quickcheck_full_support = true]] 
45441
fb4ac1dd4fde
adding some test cases for preprocessing and narrowing
bulwahn
parents:
45118
diff
changeset

565 

48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

566 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

567 
subsection {* Equality Optimisation *} 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

568 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

569 
lemma 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

570 
"f x = y ==> y = (0 :: nat)" 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

571 
quickcheck 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

572 
oops 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

573 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

574 
lemma 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

575 
"y = f x ==> y = (0 :: nat)" 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

576 
quickcheck 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

577 
oops 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

578 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

579 
lemma 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

580 
"f y = zz # zzs ==> zz = (0 :: nat) \<and> zzs = []" 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

581 
quickcheck 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

582 
oops 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

583 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

584 
lemma 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

585 
"f y = x # x' # xs ==> x = (0 :: nat) \<and> x' = 0 \<and> xs = []" 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

586 
quickcheck 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

587 
oops 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

588 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

589 
lemma 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

590 
"x = f x \<Longrightarrow> x = (0 :: nat)" 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

591 
quickcheck 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

592 
oops 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

593 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

594 
lemma 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

595 
"f y = x # x # xs ==> x = (0 :: nat) \<and> xs = []" 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

596 
quickcheck 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

597 
oops 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

598 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

599 
lemma 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

600 
"m1 k = Some v \<Longrightarrow> (m1 ++ m2) k = Some v" 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

601 
quickcheck 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

602 
oops 
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

603 

44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47348
diff
changeset

604 

42434
1914fd5d7c0e
adding examples for Quickcheck used within locales
bulwahn
parents:
42159
diff
changeset

605 
end 