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

[Jose Divasón]

Hello Florian.

This work sounds very interesting. Just a few comments:

* Take care about the names of the algebraic structures. By PIR (principal
ideal ring) some authors mean a commutative ring with identity in which
every ideal is principal, using the name PID (principal ideal domain) for
integral domains in which every ideal is principal. But other authors say
that a PIR is an integral domain in which every ideal is principal. The
same happens to Euclidean domain/Euclidean ring, Unique Factorization
Domain/Factorial ring and so on. It would be desirable to follow the same
convention for every structure.

* In the first assumption of the factorial_semiring class, maybe is "a is
not an unit" instead of "a is not 1"?

* If an operation is_prime is fixed in a factorial_semiring class, as far
as I know then it would not be possible to prove that each euclidean ring
is a factorial ring by means of subclasses (unless the euclidean_ring class
is changed). Could is_prime be a definition in the  comm_ring class? In
addition, prime and irreducible elements are defined in commutative rings
(there they are different, but in UFD they are the same).

* I haven't found if there exists a convention concerning precedence of mod
in mathematics, but in programming languages mod has the same precedence as
* and /.

I would be glad to help in everything you consider.

Best,
Jose

2014-11-09 21:47 GMT+01:00 Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de>:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141112/519504d6/attachment-0002.html>