adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
authorbulwahn
Mon Oct 03 14:43:15 2011 +0200 (2011-10-03 ago)
changeset 451187462f287189a
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
     1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Oct 03 14:43:14 2011 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Oct 03 14:43:15 2011 +0200
     1.3 @@ -266,6 +266,20 @@
     1.4    quickcheck[expect = counterexample]
     1.5  oops
     1.6  
     1.7 +
     1.8 +subsection {* Examples with relations *}
     1.9 +
    1.10 +lemma
    1.11 +  "acyclic R ==> acyclic S ==> acyclic (R Un S)"
    1.12 +quickcheck[expect = counterexample]
    1.13 +oops
    1.14 +
    1.15 +lemma
    1.16 +  "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
    1.17 +quickcheck[expect = counterexample]
    1.18 +oops
    1.19 +
    1.20 +
    1.21  subsection {* Examples with numerical types *}
    1.22  
    1.23  text {*