[isabelle-dev] Euclidean Ring
eberlm at in.tum.de
Sat Jun 27 17:31:55 CEST 2015
On 27/06/15 09:06, Florian Haftmann wrote:
> What about: »a = unit_factor a * normalize a«
> 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)"
and also the other files on that Github repository)
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev