*To*: Zhe Hou <zhe.hou at hotmail.com>*Subject*: Re: [isabelle] Rounding negative fractions in Isabelle*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 1 Oct 2015 17:19:34 +0200*Cc*: Larry Paulson <lp15 at cam.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <8040C4EE-FA7D-4550-A0B2-6B0369FC34DA@cam.ac.uk>*Organization*: TU Munich*References*: <SNT407-EAS100FCEFEF7FA7A34E451C0DE44C0@phx.gbl> <8040C4EE-FA7D-4550-A0B2-6B0369FC34DA@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

Hi Zhe, > 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.) that is easily made plausible: the units of a ring (in case of int, +1 and -1) form a field. In this segment you expect the conventional rules of field division to hold: +1 div +1 = +1 -1 div +1 = -1 +1 div -1 = -1 -1 div -1 = -1 And also a div b = (sgn a * abs a) div (sgn b * abs b) = (sgn a div sgn b) * (abs a div abs b) where Âabs a div abs bÂ is already explained and Âsgn a * abs aÂ follows the rules above. The sign rules for mod follow naturally using the obviously desirable facts: b <> 0 ==> a * b div b = a a div b * b + a mod b = a As far as I understand at the moment, this generalizes to each euclidean ring. So, the sign rules are computationally confusing at first sight, but make perfect sense from an algebraic point of view. Hope this helps, Florian > > 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 > > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Rounding negative fractions in Isabelle***From:*Lars Noschinski

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

**Re: [isabelle] Rounding negative fractions in Isabelle***From:*Larry Paulson

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