*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Floor and ceiling*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 03 Apr 2012 14:59:27 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <7B563121-D5DB-48F5-AAE4-F531B38B293E@uibk.ac.at>*References*: <93BE2881-34CB-4E7A-BFC5-7B5AC5002A1E@uibk.ac.at> <4F7AE5C3.3080402@in.tum.de> <CAAMXsibeKxsW0fyOOR42p9yMjE03BegNtMCdSjgBPf0Z891LVw@mail.gmail.com> <4F7AEBB9.6010702@in.tum.de> <7B563121-D5DB-48F5-AAE4-F531B38B293E@uibk.ac.at>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2

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

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

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

- Previous by Date: Re: [isabelle] Floor and ceiling
- Next by Date: [isabelle] Receiving error by importing theory file Sum_Of_Squares
- Previous by Thread: Re: [isabelle] Floor and ceiling
- Next by Thread: [isabelle] Receiving error by importing theory file Sum_Of_Squares
- 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