[isabelle-dev] Euclidean Ring

[Manuel Eberl]

On 27/06/15 09:06, Florian Haftmann wrote:
> What about: »a = unit_factor a * normalize a«
Sounds reasonable.

> 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. 
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?

> (Btw. a formalisation of the Gaussian integers could
> be a nice student project.)
I coud have sworn we had a formalisation of Gaussian integers somewhere,
but I cannot seem to find it anymore. Perhaps I am wrong.

> See (EF1) in https://en.wikipedia.org/wiki/Euclidean_domain#Definition –
> 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.
That is not entirely true. Your weaker assumption allows for a slightly
simpler instantiation, but my previous instantiation for polynomials used

definition [simp]: "euclidean_size_poly p \<equiv>
      (if p = 0 then 0 else degree p + 1)"

(see https://github.com/3of8/isabellehol_gcd/blob/master/Polynomial.thy
and also the other files on that Github repository)


Cheers,

Manuel



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150627/ed793fc8/attachment-0002.html>