[isabelle] Rounding negative fractions in Isabelle



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



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