Re: [isabelle] Rounding negative fractions in Isabelle

Hi Zhe,

Larry and Florian already wrote about why division on integers in Isabelle is defined the way it is. If you want a different behaviour for division, you must define your own division operator. Fortunately, you can achieve this probably quite easily by doing a few case distinctions on the sign of the operands. In my AFP entry JinjaThreads, I have done something similar for division and modulo on fixed-size integers ('a word), because the division operation in HOL-Word did not match the sign rules of Java. Have a look at the theory JinjaThreads/Common/BinOp.thy (search for word_sdiv); maybe this gives you some inspiration.


On 01/10/15 05:09, Zhe Hou wrote:

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.