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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
