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.haftm...@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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
