[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.