# [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

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.