*To*: Zhe Hou <zhe.hou at hotmail.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Rounding negative fractions in Isabelle*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 1 Oct 2015 18:12:50 +0200*In-reply-to*: <SNT407-EAS100FCEFEF7FA7A34E451C0DE44C0@phx.gbl>*References*: <SNT407-EAS100FCEFEF7FA7A34E451C0DE44C0@phx.gbl>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

Hi Zhe,

Best, Andreas On 01/10/15 05:09, Zhe Hou 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

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

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