src/HOL/Archimedean_Field.thy
changeset 47592 a6b76247534d
parent 47307 5e5ca36692b3
child 54281 b01057e72233
equal deleted inserted replaced
47583:f3f0e06549c2 47592:a6b76247534d
   444   using ceiling_diff_of_int [of x "neg_numeral v"] by simp
   444   using ceiling_diff_of_int [of x "neg_numeral v"] by simp
   445 
   445 
   446 lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   446 lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   447   using ceiling_diff_of_int [of x 1] by simp
   447   using ceiling_diff_of_int [of x 1] by simp
   448 
   448 
       
   449 lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"
       
   450 proof -
       
   451   have "of_int \<lceil>x\<rceil> - 1 < x" 
       
   452     using ceiling_correct[of x] by simp
       
   453   also have "x < of_int \<lfloor>x\<rfloor> + 1"
       
   454     using floor_correct[of x] by simp_all
       
   455   finally have "of_int (\<lceil>x\<rceil> - \<lfloor>x\<rfloor>) < (of_int 2::'a)"
       
   456     by simp
       
   457   then show ?thesis
       
   458     unfolding of_int_less_iff by simp
       
   459 qed
   449 
   460 
   450 subsection {* Negation *}
   461 subsection {* Negation *}
   451 
   462 
   452 lemma floor_minus: "floor (- x) = - ceiling x"
   463 lemma floor_minus: "floor (- x) = - ceiling x"
   453   unfolding ceiling_def by simp
   464   unfolding ceiling_def by simp