# [isabelle] Division-ring for fields

*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>
*Subject*: [isabelle] Division-ring for fields
*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
*Date*: Fri, 24 Apr 2015 13:04:32 +0000
*Accept-language*: de-DE, de-AT, en-US
*Thread-index*: AQHQfo81yQvh/3JnS0eO5hxLx8qEyA==
*Thread-topic*: Division-ring for fields

Dear all,
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
instantiation rat :: ring_div_field
begin
definition "div_rat = (op / :: rat â rat â rat)"
definition "mod_rat (x :: rat) (y :: rat) = (if y = 0 then x else 0)"
instance
by (intro_classes, auto simp: div_rat_def mod_rat_def)
end
instantiation real :: ring_div_field
begin
definition "div_real = (op / :: real â real â real)"
definition "mod_real (x :: real) (y :: real) = (if y = 0 then x else 0)"
instance
by (intro_classes, auto simp: div_real_def mod_real_def)
end
instantiation complex :: ring_div_field
begin
definition "div_complex = (op / :: complex â complex â complex)"
definition "mod_complex (x :: complex) (y :: complex) = (if y = 0 then x else 0)"
instance
by (intro_classes, auto simp: div_complex_def mod_complex_def)
end
Best regards,
RenÃ

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