# HG changeset patch # User bulwahn # Date 1310232565 -7200 # Node ID ea147bec4f72db73bde54d88ffa7b40f54040807 # Parent a6ca7b83612fb1039dd0a4e9c9301f91b4169910 adding quickcheck examples for evaluating floor and ceiling functions diff -r a6ca7b83612f -r ea147bec4f72 src/HOL/ex/Quickcheck_Examples.thy --- a/src/HOL/ex/Quickcheck_Examples.thy Sat Jul 09 19:28:33 2011 +0200 +++ b/src/HOL/ex/Quickcheck_Examples.thy Sat Jul 09 19:29:25 2011 +0200 @@ -294,6 +294,29 @@ quickcheck[random, size = 10] oops +subsubsection {* floor and ceiling functions *} + +lemma + "floor x + floor y = floor (x + y :: rat)" +quickcheck[expect = counterexample] +oops + +lemma + "floor x + floor y = floor (x + y :: real)" +quickcheck[expect = counterexample] +oops + +lemma + "ceiling x + ceiling y = ceiling (x + y :: rat)" +quickcheck[expect = counterexample] +oops + +lemma + "ceiling x + ceiling y = ceiling (x + y :: real)" +quickcheck[expect = counterexample] +oops + + subsection {* Examples with Records *} record point =