Re: [isabelle] Rounding negative fractions in Isabelle
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
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)
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