src/HOL/Archimedean_Field.thy
changeset 47307 5e5ca36692b3
parent 47108 2a1953f0d20d
child 47592 a6b76247534d
equal deleted inserted replaced
47306:56d72c923281 47307:5e5ca36692b3
   192   by (rule floor_unique) simp_all
   192   by (rule floor_unique) simp_all
   193 
   193 
   194 lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
   194 lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
   195   using floor_of_int [of "of_nat n"] by simp
   195   using floor_of_int [of "of_nat n"] by simp
   196 
   196 
       
   197 lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
       
   198   by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
       
   199 
   197 text {* Floor with numerals *}
   200 text {* Floor with numerals *}
   198 
   201 
   199 lemma floor_zero [simp]: "floor 0 = 0"
   202 lemma floor_zero [simp]: "floor 0 = 0"
   200   using floor_of_int [of 0] by simp
   203   using floor_of_int [of 0] by simp
   201 
   204 
   338   by (rule ceiling_unique) simp_all
   341   by (rule ceiling_unique) simp_all
   339 
   342 
   340 lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
   343 lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
   341   using ceiling_of_int [of "of_nat n"] by simp
   344   using ceiling_of_int [of "of_nat n"] by simp
   342 
   345 
       
   346 lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
       
   347   by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
       
   348 
   343 text {* Ceiling with numerals *}
   349 text {* Ceiling with numerals *}
   344 
   350 
   345 lemma ceiling_zero [simp]: "ceiling 0 = 0"
   351 lemma ceiling_zero [simp]: "ceiling 0 = 0"
   346   using ceiling_of_int [of 0] by simp
   352   using ceiling_of_int [of 0] by simp
   347 
   353