[isabelle] Rounding negative fractions in Isabelle
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)
As a result, I can prove the following in Isabelle (2015 version):
lemma "(18406909::int) div (- 2240) â - ((18406909::int) div (2240))"
I think this is unusual. If anyone could point me to an alternative way to do division in Isabelle, Iâd be very grateful.
This archive was generated by a fusion of
Pipermail (Mailman edition) and