src/HOL/Archimedean_Field.thy
changeset 47592 a6b76247534d
parent 47307 5e5ca36692b3
child 54281 b01057e72233
     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Apr 19 12:28:10 2012 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Wed Apr 18 14:29:05 2012 +0200
     1.3 @@ -446,6 +446,17 @@
     1.4  lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
     1.5    using ceiling_diff_of_int [of x 1] by simp
     1.6  
     1.7 +lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
     1.8 +proof -
     1.9 +  have "of_int \<lceil>x\<rceil> - 1 < x" 
    1.10 +    using ceiling_correct[of x] by simp
    1.11 +  also have "x < of_int \<lfloor>x\<rfloor> + 1"
    1.12 +    using floor_correct[of x] by simp_all
    1.13 +  finally have "of_int (\<lceil>x\<rceil> - \<lfloor>x\<rfloor>) < (of_int 2::'a)"
    1.14 +    by simp
    1.15 +  then show ?thesis
    1.16 +    unfolding of_int_less_iff by simp
    1.17 +qed
    1.18  
    1.19  subsection {* Negation *}
    1.20