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.