*To*: cl-isabelle-users at lists.cam.ac.uk, Jose Divasón <jose.divasonm at unirioja.es>*Subject*: Re: [isabelle] Gcd and algebraic structures*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 30 Aug 2014 11:46:45 +0200*In-reply-to*: <CA+MUZ5sJZcbZnWkPcX8GQM4Ltr6vidDt0FJR1PXnHyVbpGG+CA@mail.gmail.com>*Organization*: TU Munich*References*: <CA+MUZ5sJZcbZnWkPcX8GQM4Ltr6vidDt0FJR1PXnHyVbpGG+CA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.0

Hi Jose, your are actually stumbling over the issue that HOL so far does not really provide a hierarchy of type classes for divisibility in rings (say, factorial ring, euclidean ring etc.) Here my thoughts of what can be done with reasonable effort at the moment 1) The syntactic gcd type class. Cf. also Manuel's mail. Syntactic type classes can also be seen as an instance of the traditional »worse is better« philosophy of UNIX: if you do not know how to provide the right policy, restrict yourself to provide a mechanisms while leaving the user to provide its own policy on his own. 2) A fundamental algebraic type class for GCD. IMHO this could look like: > class semiring_gcd = semiring + gcd + > assumes "gcd a b dvd a" > assumes "gcd a b dvd b" > assumes "c dvd a ⟹ c dvd b ⟹ c dvd gcd a b" > > class ring_gcd = ring + semiring_gcd Remarks: a) I strongly believe the assumptions capture the essence of gcd, whatever the underlying structure is. b) Whenever you develop type class hierarchies for ring structures, you always have a semiring (the additive structure is a monoid, not a group) and a ring. The semiring part of the hierarchy is to accommodate the natural numbers (which, in algebra, appear not be that natural after all). c) Here I have chosen »semiring«/»ring« as a base point. Maybe gcd itself suggests are more specific entry point to start with already, but I have found no argument to do so (maybe you would do after some rounds of experimenting and thinking). d) The specification implicitly states I. the a gcd exists II. that is is functional, i.e. normalising wrt. to units But it does not assume anything how this normalisation actually looks like, i.e. concrete instances are free to normalise in a specific way. 3) Specific instances for GCD in more specific algebraic structures a) e.g. for euclidean rings class euclidean_(semi)ring = … begin … definition gcd_eucl where … -- ‹definition via euclidean algorithm› … end class euclidean_(semi)ring_gcd = euclidean_(semi)ring + gcd assumes "gcd = gcd_eucl" begin subclass (semi)ring_gcd … end Note that this work has already been done by Manuel, but is not yet part of Isabelle2014. If you want to build on that, we will find a suitable way without need to participate in the ongoing Isabelle development. b) e.g. for factorial rings class factorial_(semi)ring = … begin … definition factorization :: "'a => 'a mulitset" where … … end class factorial_(semi)ring_gcd = factorial_(semi)ring + gcd assumes "gcd a b = msetprod (factorization a + factorization b)" begin subclass (semi)ring_gcd … end > By the way, what is the difference between interpretation and sublocale in > this context? »interpretation« pulls in facts into the current target context, which is closed at the final »end« – »confined interpretation«. »sublocale« establishes a permanent connection. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Gcd and algebraic structures***From:*Florian Haftmann

**References**:**[isabelle] Gcd and algebraic structures***From:*Jose Divasón

- Previous by Date: [isabelle] PDFs of Isabelle 2014 Workshop Submissions
- Next by Date: Re: [isabelle] Gcd and algebraic structures
- Previous by Thread: Re: [isabelle] Gcd and algebraic structures
- Next by Thread: Re: [isabelle] Gcd and algebraic structures
- Cl-isabelle-users August 2014 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