*To*: Jose Divasón <jose.divasonm at unirioja.es>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Gcd and algebraic structures*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 02 Sep 2014 13:31:51 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CA+MUZ5sdu8y2O+p5prdeZoFMMOWdPuNzTroJee95QmaBNfDdTw@mail.gmail.com>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

On 02/09/14 13:07, Jose Divasón wrote: > By the way, in your formalization I have seen you fix the euclidean > size in the euclidean_semiring class. However, a Euclidean domain will > admit many different euclidean size functions (in > http://en.wikipedia.org/wiki/Euclidean_domainit is suggested that a > particular Euclidean function fis notpart of the structure of a > Euclidean domain). I am aware of that, but I saw no reason why a single sufficiently nice (i.e. fulfilling the “b ≠ 0 ⟹ f (a mod b) < f a” and "b ≠ 0 ⟹ f a ≤ f (a*b)” conditions) should not suffice. I cannot think of a circumstance in which you might require several different euclidean size functions. > Would it be possible to define that class this way? Could there be any > potential drawbacks? > > class euclidean_semiring = … + > > assumes exists_euclidean_size: "∃f::'a => nat. ∀a b. b≠0 ⟶ (∃q r. a = > b*q + r ∧ (r=0 ∨ f r < f b))" > You can do that and then define euclidean_size with Hilbert choice and get all the properties you need with exists_euclidean_size. I see no drawbacks, but, as stated before, I also don't see any real advantages that would justify it – apart from the fact that you can drop the monotonicity assumption, because if any euclidean size function exists, then a monotonic one exists. (which you'd have to prove, of course) > But if one uses this way of defining the euclidean_semiring class, > then it would not be possible to get direct executability (because the > euclidean_size would not be instantiated). Anyway, with your > definition it would be possible to work with different euclidean sizes > of the same structure if the instantiations are done in independent > files. I don’t know which option is more suitable. > I do not think that this is an issue. If I recall correctly, I never use euclidean_size in any code equations – it is only required for the termination proof of the Euclidean algorithm, and termination measures do not have to be executable. Cheers, Manuel

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

- Previous by Date: Re: [isabelle] Gcd and algebraic structures
- Next by Date: [isabelle] Isabelle/jEdit requests loading of files during shutdown
- 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