[isabelle-dev] Algebra and number theory in Isabelle/HOL

[Lawrence Paulson]

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.

Larry

> 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.
> 
> Cheers,
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> <Agenda_Algebra.thy>_______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev