src/HOL/Archimedean_Field.thy
changeset 47307 5e5ca36692b3
parent 47108 2a1953f0d20d
child 47592 a6b76247534d
     1.1 --- a/src/HOL/Archimedean_Field.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Apr 03 14:09:37 2012 +0200
     1.3 @@ -194,6 +194,9 @@
     1.4  lemma floor_of_nat [simp]: "floor (of_nat n) = int n"
     1.5    using floor_of_int [of "of_nat n"] by simp
     1.6  
     1.7 +lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
     1.8 +  by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
     1.9 +
    1.10  text {* Floor with numerals *}
    1.11  
    1.12  lemma floor_zero [simp]: "floor 0 = 0"
    1.13 @@ -340,6 +343,9 @@
    1.14  lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n"
    1.15    using ceiling_of_int [of "of_nat n"] by simp
    1.16  
    1.17 +lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
    1.18 +  by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
    1.19 +
    1.20  text {* Ceiling with numerals *}
    1.21  
    1.22  lemma ceiling_zero [simp]: "ceiling 0 = 0"