Re: [isabelle] Floor and ceiling



Thanks for the addition and the shortening. 
(I am quite sure that I tried sledgehammer first, but perhaps at that
time I stated the wrong lemma)

René

Am 03.04.2012 um 14:23 schrieb Tobias Nipkow:

> 
> 
> Am 03/04/2012 14:17, schrieb Brian Huffman:
>> Ok, I just added the following two lemmas to Archimedean_Field.thy
>> (rev 5e5ca36692b3).
>> 
>> lemma le_floor_add: "floor x + floor y \<le> floor (x + y)"
>>  by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)
>> 
>> lemma ceiling_add_le: "ceiling (x + y) \<le> ceiling x + ceiling y"
>>  by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)
>> 
>> Tobias' proof still seemed a bit overkill in my opinion ;-)
> 
> But it took me fewer keystrokes to produce it ;-)
> 
> Tobias
> 
>> - Brian
>> 
>> On Tue, Apr 3, 2012 at 1:57 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>> 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.