equal
deleted
inserted
replaced
243 "(ys = zs) = (xs @ ys = splice xs zs)" |
243 "(ys = zs) = (xs @ ys = splice xs zs)" |
244 quickcheck[random] |
244 quickcheck[random] |
245 quickcheck[exhaustive, expect = counterexample] |
245 quickcheck[exhaustive, expect = counterexample] |
246 oops |
246 oops |
247 |
247 |
|
248 subsection {* Random Testing beats Exhaustive Testing *} |
|
249 |
|
250 lemma mult_inj_if_coprime_nat: |
|
251 "inj_on f A \<Longrightarrow> inj_on g B |
|
252 \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)" |
|
253 quickcheck[exhaustive] |
|
254 quickcheck[random] |
|
255 oops |
|
256 |
248 subsection {* Examples with quantifiers *} |
257 subsection {* Examples with quantifiers *} |
249 |
258 |
250 text {* |
259 text {* |
251 These examples show that we can handle quantifiers. |
260 These examples show that we can handle quantifiers. |
252 *} |
261 *} |