[isabelle-dev] Algebra and number theory in Isabelle/HOL
lp15 at cam.ac.uk
Mon Nov 10 17:36:46 CET 2014
Your agenda looks impressive but very ambitious.
I noticed a remark about the treatment of signs in integer division. You mention two constraints but overlook a third: standard textbooks say that the remainder should have the same sign as the divisor, so that for example -1 mod 2 = 1 and therefore -1 div 2 = -1. Computer hardware get this wrong.
> On 9 Nov 2014, at 20:47, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> The attached theory contains notes and a sketeched agenda to promote
> further algebra and number theory in Isabelle/HOL, esp. concerning gcd,
> div and mod – according to my current understanding of the whole matter.
> I am looking forward to comments, and maybe contributors.
> Personally, I will not put much time into this the next weeks but will
> come back to it as soon as appropriate.
> PGP available:
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev