# Re: [isabelle] Floor and ceiling

René,
I appreciate the lemma, but the proof is really a bit pedestrian.
I prefer
by (metis add_le_cancel_left floor_add_of_int le_floor_iff order_eq_refl
order_trans)
;-)
Tobias
Am 03/04/2012 12:59, schrieb René Thiemann:
> 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
>

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