*To*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>, Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Division-ring for fields*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sun, 26 Apr 2015 17:20:33 +0200*In-reply-to*: <9EB8C0C4-581B-43FA-9D86-A6A774230027@exchange.uibk.ac.at>*Organization*: TU Munich*References*: <9EB8C0C4-581B-43FA-9D86-A6A774230027@exchange.uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Hi RenÃ, > I have some algorithm which work on division rings (e.g., for computing the determinant of a matrix). > > However I sometimes also want to apply the same algorithm for fields, which is in principle easy since I just > have to define âdivâ as â/â and âmodâ as â% x y. if y = 0 then x else 0â. Now my question is, whether there is a better way, > than manually putting all common classes manually into div_ring as follows. > > class ring_div_field = field + div + > assumes div: "(op div :: 'a â 'a â 'a) = op /" > and mod: "(x :: 'a) mod y = (if y = 0 then x else 0)" > begin > > subclass ring_div > by (unfold_locales, auto simp: div mod field_simps) > > end currently, there is no better way. I plan to establish a common class for a division partially specified as inverse operation of multiplication, which is later on specialised both towards division with remainder as well as division in fields. This will happen somewhere after the next release. I got entangled into long-overseen problems with abbreviations in type classes before tackling the central element, the universal division operation. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Division-ring for fields***From:*Thiemann, Rene

- Previous by Date: Re: [isabelle] RC-1 – ad 8bd5999133d4 – »code_deps needs cycles«
- Next by Date: [isabelle] Session with more than one parent
- Previous by Thread: [isabelle] Division-ring for fields
- Next by Thread: [isabelle] Well-foundedness of Relational Composition
- Cl-isabelle-users April 2015 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