*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Gcd and algebraic structures*From*: Jose Divasón <jose.divasonm at unirioja.es>*Date*: Mon, 8 Sep 2014 18:40:26 +0200*Cc*: Jose Divasón <jose.divasonm at unirioja.es>, Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <54081088.3000802@informatik.tu-muenchen.de>*References*: <CA+MUZ5sJZcbZnWkPcX8GQM4Ltr6vidDt0FJR1PXnHyVbpGG+CA@mail.gmail.com> <54019D85.10906@informatik.tu-muenchen.de> <5401DFC8.7060605@informatik.tu-muenchen.de> <5401EBC3.7090304@informatik.tu-muenchen.de> <CA+MUZ5sdu8y2O+p5prdeZoFMMOWdPuNzTroJee95QmaBNfDdTw@mail.gmail.com> <54081088.3000802@informatik.tu-muenchen.de>*Sender*: jose.divason at gmail.com

Thanks for all answers, 2014-09-04 9:11 GMT+02:00 Florian Haftmann < florian.haftmann at informatik.tu-muenchen.de>: > after studying your answers I would recommend that you should follow the > approach in HOL-Algebra, i.e. use locales with explicit carriers. > Unfortunately, we would prefer to avoid HOL-Algebra: our final goal is to formalise some well-known algorithms to obtain canonical forms of matrices over principal ideal rings (echelon forms, Hermite) and generate code of them*. To do that, we have already developed some infrastructure in the HOL-Multivariate Analysis library (and its representation of matrices) that we would like to reuse. Defining a gcd in an arbitrary ring could be cumbersome working with structures represented by type classes. Nevertheless, we are mainly interested in working on principal ideal rings, where any two elements have a gcd. Hence, gcd would be a total function, and appropriate for a type class representation. We just wanted to take the chance to implement some additional Abstract Algebra (commutative rings, integral domains) in a proper way (including operations such as gcd), but maybe we will have to reshape this goal. Fortunately, as far as we know in GCD Domain, Principal Ideal Ring, Principal Ideal Domain, Factorial Domain and Euclidean Domain, which are the structures where we plan to work, gcd is a total function. I will go on thinking about it, Best, Jose * Most of these algorithms need to compute gcds or Bézout’s identity. As far as I know, these algorithms could be defined and formalized over a principal ideal ring, but they wouldn’t be executable if we don’t provide an executable gcd function. Nevertheless, they would be executable on matrices whose coefficients belong to an euclidean domain (by means of a computable euclidean algorithm).

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

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

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

- Previous by Date: Re: [isabelle] Is it bad to instantiate "list" with custom classes to be used with "bool list"?
- Next by Date: Re: [isabelle] Counting the proof time
- Previous by Thread: Re: [isabelle] Gcd and algebraic structures
- Next by Thread: Re: [isabelle] Gcd and algebraic structures
- Cl-isabelle-users September 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