# [isabelle] Floor and ceiling

Dear all,
I recently had to work with floor and ceiling where I was missing the following two monotonicity lemmas. Perhaps these are useful to someone else.
lemma floor_lesseq_add: "floor (x :: 'a :: floor_ceiling) + floor y \<le> floor (x + y)"
proof -
let ?f = floor
let ?i = of_int
let ?if = "\<lambda> x :: 'a. ?i (?f x)"
note fc = floor_correct
have "?f x + ?f y = ?if x + ?if y" by simp
also have "... \<le> ?f (x + y - ?if x - ?if y) + (?if x + ?if y)"
using fc[of x] fc[of y]
by (auto simp: field_simps)
also have "... = ?f (x + y)" unfolding floor_diff_of_int by simp
finally show ?thesis .
qed
lemma ceiling_lesseq_add: "ceiling (x + y) \<le> ceiling (x :: 'a :: floor_ceiling) + ceiling y" using floor_lesseq_add[of "- x" "- y"] unfolding floor_minus
using floor_minus[of "x + y"] by simp
Cheers,
René

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*