Re: [isabelle] Floor and ceiling




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.