# HG changeset patch
# User bulwahn
# Date 1327687728 -3600
# Node ID ee500921279317aa1f2f1c8b2c32668d7685d7c3
# Parent  54870ad19af454d96c54b2a777463eb7937c24bc
adding some more examples for quickcheck; replaced FIXME comments

diff -r 54870ad19af4 -r ee5009212793 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Fri Jan 27 17:22:05 2012 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Jan 27 19:08:48 2012 +0100
@@ -270,15 +270,37 @@
 subsection {* Examples with relations *}
 
 lemma
-  "acyclic R ==> acyclic S ==> acyclic (R Un S)"
-(* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *)
+  "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
+  "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+(* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *)
+lemma
   "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
-(* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *)
+(*quickcheck[exhaustive, expect = counterexample]*)
+oops
+
+lemma
+  "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
 oops
 
+lemma
+  "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+  "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+
 subsection {* Examples with the descriptive operator *}
 
 lemma