summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | bulwahn |

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

--- 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 {*