*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Floor and ceiling*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Tue, 3 Apr 2012 14:55:37 +0200*Cc*: Brian Huffman <huffman at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F7AEBB9.6010702@in.tum.de>*References*: <93BE2881-34CB-4E7A-BFC5-7B5AC5002A1E@uibk.ac.at> <4F7AE5C3.3080402@in.tum.de> <CAAMXsibeKxsW0fyOOR42p9yMjE03BegNtMCdSjgBPf0Z891LVw@mail.gmail.com> <4F7AEBB9.6010702@in.tum.de>

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

**Follow-Ups**:**Re: [isabelle] Floor and ceiling***From:*Tobias Nipkow

**References**:**[isabelle] Floor and ceiling***From:*René Thiemann

**Re: [isabelle] Floor and ceiling***From:*Tobias Nipkow

**Re: [isabelle] Floor and ceiling***From:*Brian Huffman

**Re: [isabelle] Floor and ceiling***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Floor and ceiling
- Next by Date: Re: [isabelle] Floor and ceiling
- Previous by Thread: Re: [isabelle] Floor and ceiling
- Next by Thread: Re: [isabelle] Floor and ceiling
- Cl-isabelle-users April 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list