# HG changeset patch
# User bulwahn
# Date 1330157263 -3600
# Node ID 3fc49e6998dae92c3a7d963155a64e97b43ae87a
# Parent  3a40ea076230a16b8e1dd52cdff83574ef04cb6c
adding an example where random beats exhaustive testing

diff -r 3a40ea076230 -r 3fc49e6998da src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sat Feb 25 09:07:41 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sat Feb 25 09:07:43 2012 +0100
@@ -245,6 +245,15 @@
 quickcheck[exhaustive, expect = counterexample]
 oops
 
+subsection {* Random Testing beats Exhaustive Testing *}
+
+lemma mult_inj_if_coprime_nat:
+  "inj_on f A \<Longrightarrow> inj_on g B
+   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
+quickcheck[exhaustive]
+quickcheck[random]
+oops
+
 subsection {* Examples with quantifiers *}
 
 text {*