# HG changeset patch
# User hoelzl
# Date 1334752145 -7200
# Node ID a6b76247534d5f142d30418f99b67595bc7ec1ef
# Parent  f3f0e06549c2b0771ce7c1c44b74c661c1415a8d
add ceiling_diff_floor_le_1

diff -r f3f0e06549c2 -r a6b76247534d src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Thu Apr 19 12:28:10 2012 +0200
+++ b/src/HOL/Archimedean_Field.thy	Wed Apr 18 14:29:05 2012 +0200
@@ -446,6 +446,17 @@
 lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   using ceiling_diff_of_int [of x 1] by simp
 
+lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
+proof -
+  have "of_int \<lceil>x\<rceil> - 1 < x" 
+    using ceiling_correct[of x] by simp
+  also have "x < of_int \<lfloor>x\<rfloor> + 1"
+    using floor_correct[of x] by simp_all
+  finally have "of_int (\<lceil>x\<rceil> - \<lfloor>x\<rfloor>) < (of_int 2::'a)"
+    by simp
+  then show ?thesis
+    unfolding of_int_less_iff by simp
+qed
 
 subsection {* Negation *}