# 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 =