*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Gcd and algebraic structures*From*: Jose Divasón <jose.divasonm at unirioja.es>*Date*: Fri, 29 Aug 2014 19:53:10 +0200*Sender*: jose.divason at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Gcd and algebraic structures***From:*Manuel Eberl

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

- Previous by Date: [isabelle] Final CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call, extended deadline)
- Next by Date: Re: [isabelle] Gcd and algebraic structures
- Previous by Thread: [isabelle] Final CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call, extended deadline)
- 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