*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Code setup for Fraction_Field*From*: Jose DivasÃn <jose.divasonm at unirioja.es>*Date*: Fri, 4 Sep 2015 12:44:52 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, Manuel Eberl <eberlm at in.tum.de>, prathamesh at imsc.res.in*In-reply-to*: <55E96535.7050909@inf.ethz.ch>*References*: <55DED10F.5030507@inf.ethz.ch> <55DEE024.3070504@informatik.tu-muenchen.de> <55E96535.7050909@inf.ethz.ch>*Sender*: jose.divason at gmail.com

> 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 http://afp.sourceforge.net/browser_info/current/AFP/Echelon_Form/Euclidean_Algorithm.html). 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 ( http://afp.sourceforge.net/browser_info/current/AFP/Echelon_Form/Euclidean_Algorithm_Extension.html), 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. Best, Jose

**Follow-Ups**:**Re: [isabelle] Code setup for Fraction_Field***From:*Manuel Eberl

**References**:**Re: [isabelle] Code setup for Fraction_Field***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Code setup for Fraction_Field
- Next by Date: Re: [isabelle] Code setup for Fraction_Field
- Previous by Thread: Re: [isabelle] Code setup for Fraction_Field
- Next by Thread: Re: [isabelle] Code setup for Fraction_Field
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list