Re: [isabelle] Code setup for Fraction_Field

> 1. I noticed that there are the type classes euclidean_ring and
> euclidean_ring_gcd. Most of the theorems about gcd which I need are in
> euclidean_ring_gcd, but not in euclidean_ring itself. Unfortunately, the
> instantiations for nat, int, etc. are only done for euclidean_ring, not for
> euclidean_ring_gcd. What are the plans for these type classes? Should I
> spend any effort on adding instances for euclidean_ring_gcd? Or will this
> become obsolete with the polishing that is still due?
Dear all,

Some months ago I noticed the same thing. As Manuel says,
euclidean_ring_gcd is just euclidean_ring + gcd = gcd_euclid (and the same
for Gcd, lcm and Lcm).

Anyway, in my AFP entry called Echelon_Form there is another variant of the
Manuel's file (see

I just slighly modified his version to move most of theorems presented in
the euclidean_ring_gcd class to the euclidean_ring one. In other file (,
the following instances were also proven:

instantiation nat :: euclidean_semiring_gcd
instantiation int :: euclidean_ring_gcd
instantiation poly :: (field) euclidean_ring
instantiation poly :: (field) euclidean_ring_gcd

Nevertheless, it's worth noting that my files are independent with respect
the Manuel's one (which is the one presented in the stardard library). In
addition, my changes were done with respect to an old version of the
Manuel's file, so probably there have been some
improvements/restructurations on his file.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.