*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Gcd and algebraic structures*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 29 Aug 2014 20:15:30 +0200*In-reply-to*: <CA+MUZ5sJZcbZnWkPcX8GQM4Ltr6vidDt0FJR1PXnHyVbpGG+CA@mail.gmail.com>*References*: <CA+MUZ5sJZcbZnWkPcX8GQM4Ltr6vidDt0FJR1PXnHyVbpGG+CA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Hallo, syntactic type classes such as this are not unusual. They allow overloading of constants (such as 0, +, *, gcd, …) without restricting the way in which these constants can be used. In case of gcd, I think one could make a good argument for assuming basic facts about GCDs in the type class. Anyway, if you want to generalise the GCD, I would recommend you completely ignore the current GCD theory and the gcd type class, because it already defines a gcd on e.g. the natural numbers and the integers, and your more general formalisation will probably also yield some GCD implementation on the natural numbers and integers – resulting in a clash of these two definitions. GCDs are only unique (modulo association) in integral domains, and only guaranteed to exist in factorial rings (UIDs). Therefore, I would recommend that you introduce a predicate is_gcd a b :: 'a => 'a => 'a => bool for commutative rings in order to handle the situation of multiple (or no) GCDs. Then you can introduce a function gcd :: 'a => 'a => 'a for integral domains, yielding a normalised GCD if it exists and undefined (or 0 or 1 or whatever) otherwise, and for factorial rings, you can then actually prove that this gcd function is “total”, i.e. it always returns a GCD. For normalisation, the approach that I took in my formalisation of Euclidean rings was to define a function called normalisation_factor :: 'a => 'a, which returns a unit such that dividing any element of the ring by that unit yields the same result for all elements in the same association class, effectively normalising the element. E.g. for integers, the normalisation factor is the sign of the number; for polynomials, it is the leading coefficient. Cheers, Manuel On 29/08/14 19:53, Jose Divasón wrote: > Dear all, > > I would like to formalise some linear algebra structures, such as principal > ideal rings, principal ideal domains, unique factorization domains and so > on. > > As part of those structures, there exist some basic operations over rings > such as gcd and div, which are already implemented in the Isabelle library. > For instance, there is a class gcd in the library which has been > instantiated by int and nat: > > class gcd = zero + one + dvd + > fixes gcd :: "'a => 'a => 'a" > and lcm :: "'a => 'a => 'a" > > begin > > > > Nevertheless, this class seems to me somehow strange, because it doesn’t > fix any property about gcd and lcm, so it could be instantiated by almost > anything. > > Moreover, the notion of greatest common divisor can be properly defined in > commutative rings, and also in principal ideal rings, although in general > there need not exist just one for every pair of elements. > > My doubt is how to include that concept in the principal ideal ring class > that I’m formalising. > > I think that there are (at least) three options: > > 1.- “Forget” the gcd class that exists in the library and define gcd inside > my class: > > class pir = comm_ring_1 + assumes all_ideal_is_principal: "∀I. ideal I ⟶ > principal_ideal I" > > begin > > definition "gcd_pir a b = ....." > > end > > 2.- Define a class called “pir_gcd”, extending gcd and assuming what gcd > must satisfy. > > class pir_gcd = comm_ring_1 + gcd + assumes all_ideal_is_principal: "∀I. > ideal I ⟶ principal_ideal I" and "∀a b. gcd a b = ..." and "∀a b. lcm a b > = ..." > > 3.- Option 1 + interpretations/sublocales. > > class pir = comm_ring_1 + assumes all_ideal_is_principal: "∀I. ideal I ⟶ > principal_ideal I" > > begin > > definition "gcd_pir a b = ....." > > definition "lcm_pir a b = ....." > > interpretation gcd "0::'a" 1 "times::'a=>'a=>'a" "gcd_pir" "lcm_pir" . > > sublocale gcd "0::'a" 1 "times::'a=>'a=>'a" "gcd_pir" "lcm_pir" . > > end > > By the way, what is the difference between interpretation and sublocale in > this context? > > Which is the recommended option? At first I though that it was the last > one, but then I wondered why the second one has been used in the library > (there are two classes: semiring and semiring_div in the library instead of > only one of them). > > Thanks, > Jose

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

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