Re: [isabelle] Division-ring for fields

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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.