[isabelle] 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.