*To*: Zhe Hou <zhe.hou at hotmail.com>*Subject*: Re: [isabelle] Rounding negative fractions in Isabelle*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Thu, 1 Oct 2015 09:12:55 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <SNT407-EAS100FCEFEF7FA7A34E451C0DE44C0@phx.gbl>*References*: <SNT407-EAS100FCEFEF7FA7A34E451C0DE44C0@phx.gbl>

Dear Zhe, thanks for your query. I donât have a book with me at the moment to cite, but my understanding is that mathematicians normally define the sign of the remainder to match that of the divisor. Thus 1 div 2 = 0 with remainder 1, but 1 div ~2 = -1 with remainder -1. (And -1 * -2 + -1 = 2-1 = 1.) The sources I could find online didnât seem to define division in the case of a negative divisor. However, note that -1 div 2 = -1 and -1 mod 2 = 1. When the divisor is positive, a negative remainder is definitely wrong. Standard ML was designed to follow this classical definition. Isabelleâs number theory libraries do the same. However, computer hardware designers (either because they didnât know better, or to keep circuits as simple as possible) adopted the same sign rules for division as for multiplication. Languages such as C and OCaml give you what the hardware gives you. For example, OCaml gives -1 / 2 = 0 and -1 mod 2 = -1. These answers are simply wrong. Larry Paulson > On 1 Oct 2015, at 04:09, Zhe Hou <zhe.hou at hotmail.com> wrote: > > Hi, > > I found that Isabelle doesnât round negative fractions in the way I expected. For example, I expect > > (18406909::int) div (- 2240) > > to be -8217, but Isabelle says itâs -8218. I tried it in a few other languages such as Ocaml, C++. They all reported -8217. In SML, the rounding mode IEEEReal.TO_NEGINF results in -8218. > > However, Isabelle says > > - ((18406909::int) div 2240) > > is -8217. > > As a result, I can prove the following in Isabelle (2015 version): > > lemma "(18406909::int) div (- 2240) â - ((18406909::int) div (2240))" > by auto > > I think this is unusual. If anyone could point me to an alternative way to do division in Isabelle, Iâd be very grateful. > > Thank you. > > Zhe

**Follow-Ups**:**Re: [isabelle] Rounding negative fractions in Isabelle***From:*Florian Haftmann

**References**:**[isabelle] Rounding negative fractions in Isabelle***From:*Zhe Hou

- Previous by Date: [isabelle] Rounding negative fractions in Isabelle
- Next by Date: [isabelle] using beamer in document preparation
- Previous by Thread: [isabelle] Rounding negative fractions in Isabelle
- Next by Thread: Re: [isabelle] Rounding negative fractions in Isabelle
- Cl-isabelle-users October 2015 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