Re: [isabelle] Floor and ceiling



Am 03/04/2012 14:55, schrieb René Thiemann:
> 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)

Disn't you have auto-quickcheck on? ;-)

Tobias

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