<div dir="ltr"><div><div>Hello Florian.<br></div><div><br></div><div>This work sounds very interesting. Just a few comments:<br><br></div>*
 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.<br><br></div><div>* In the first assumption of the factorial_semiring class, maybe is "a is not an unit" instead of "a is not 1"?<br><br></div><div>*
 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).<br><br></div><div>* 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 /.<br><br></div><div>I would be glad to help in everything you consider.<br></div><div><br></div>Best,<br>Jose</div><div class="gmail_extra"><br><div class="gmail_quote">2014-11-09 21:47 GMT+01:00 Florian Haftmann <span dir="ltr"><<a href="mailto:florian.haftmann@informatik.tu-muenchen.de" target="_blank">florian.haftmann@informatik.tu-muenchen.de</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">The attached theory contains notes and a sketeched agenda to promote<br>
further algebra and number theory in Isabelle/HOL, esp. concerning gcd,<br>
div and mod – according to my current understanding of the whole matter.<br>
<br>
I am looking forward to comments, and maybe contributors.<br>
<br>
Personally, I will not put much time into this the next weeks but will<br>
come back to it as soon as appropriate.<br>
<br>
Cheers,<br>
        Florian<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
<br>
PGP available:<br>
<a href="http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de" target="_blank">http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de</a><br>
</font></span></blockquote></div><br></div>