adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
authorbulwahn
Mon, 03 Oct 2011 14:43:15 +0200
changeset 45118 7462f287189a
parent 45117 3911cf09899a
child 45119 055c6ff9c5c3
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Oct 03 14:43:14 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Oct 03 14:43:15 2011 +0200
@@ -266,6 +266,20 @@
   quickcheck[expect = counterexample]
 oops
 
+
+subsection {* Examples with relations *}
+
+lemma
+  "acyclic R ==> acyclic S ==> acyclic (R Un S)"
+quickcheck[expect = counterexample]
+oops
+
+lemma
+  "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
+quickcheck[expect = counterexample]
+oops
+
+
 subsection {* Examples with numerical types *}
 
 text {*