<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<br>
<div class="moz-cite-prefix">On 27/06/15 09:06, Florian Haftmann
wrote:<br>
</div>
<blockquote cite="mid:558E4B5C.4020906@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">What about: »a = unit_factor a * normalize a«
</pre>
</blockquote>
Sounds reasonable.<br>
<br>
<blockquote cite="mid:558E4B5C.4020906@informatik.tu-muenchen.de"
type="cite">I still had the hope that it would be possible to
develop an abstract
specification for gcd which would form a lattice: »gcd a a = a«.
But
now I cam to realize that for Gcd :: 'a set => 'a this would
require a
complete lattice operation or such on the units, which just does
not
make any sense for polynomials over rats or reals. So I think now
it is
best if the gcd operations only target the normalized segment of
the
underlying ring, with the weaker »gcd a a = normalize a«.
The deeper reason why we deal with normalization at all is that we
have
no rewrite machinery for equivalences, otherwise »gcd a a =(dvd)=
a«
would do.
</blockquote>
Well, the problem is that the gcd/lcm are best not viewed as
operations on ring elements, but rather operations on the
equivalence classes w.r.t. association. On these, they actually form
a lattice, if I am not mistaken. Perhaps gcd/lcm on the actual ring
elements is a ‘prelattice’? Is that a thing?<br>
<br>
<blockquote cite="mid:558E4B5C.4020906@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">(Btw. a formalisation of the Gaussian integers could
be a nice student project.)
</pre>
</blockquote>
I coud have sworn we had a formalisation of Gaussian integers
somewhere, but I cannot seem to find it anymore. Perhaps I am wrong.<br>
<br>
<blockquote cite="mid:558E4B5C.4020906@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">See (EF1) in <a class="moz-txt-link-freetext" href="https://en.wikipedia.org/wiki/Euclidean_domain#Definition">https://en.wikipedia.org/wiki/Euclidean_domain#Definition</a> –
note the »either r = 0 or f(r) < f(b)«. Note »either r <--> a mod b = 0
<--> b dvd a«. Without that termination condition, you cannot prove
that polynomials are an euclidean semiring.
</pre>
</blockquote>
That is not entirely true. Your weaker assumption allows for a
slightly simpler instantiation, but my previous instantiation for
polynomials used<br>
<br>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
definition [simp]: "euclidean_size_poly p \<equiv><br>
(if p = 0 then 0 else degree p + 1)"<br>
<br>
(see
<a class="moz-txt-link-freetext" href="https://github.com/3of8/isabellehol_gcd/blob/master/Polynomial.thy">https://github.com/3of8/isabellehol_gcd/blob/master/Polynomial.thy</a>
and also the other files on that Github repository)<br>
<br>
<br>
Cheers,<br>
<br>
Manuel<br>
<br>
<br>
<br>
</body>
</html>