# HG changeset patch # User huffman # Date 1333454977 -7200 # Node ID 5e5ca36692b32c34d43e7321c5b542d460ccfa84 # Parent 56d72c9232818ef63acb9c555cef83c8cd3a9a27 add floor/ceiling lemmas suggested by René Thiemann diff -r 56d72c923281 -r 5e5ca36692b3 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Tue Apr 03 08:55:06 2012 +0200 +++ b/src/HOL/Archimedean_Field.thy Tue Apr 03 14:09:37 2012 +0200 @@ -194,6 +194,9 @@ lemma floor_of_nat [simp]: "floor (of_nat n) = int n" using floor_of_int [of "of_nat n"] by simp +lemma le_floor_add: "floor x + floor y \ floor (x + y)" + by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le) + text {* Floor with numerals *} lemma floor_zero [simp]: "floor 0 = 0" @@ -340,6 +343,9 @@ lemma ceiling_of_nat [simp]: "ceiling (of_nat n) = int n" using ceiling_of_int [of "of_nat n"] by simp +lemma ceiling_add_le: "ceiling (x + y) \ ceiling x + ceiling y" + by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling) + text {* Ceiling with numerals *} lemma ceiling_zero [simp]: "ceiling 0 = 0"