Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Division-ring for fields

Email Gateway (Aug 22 2022 at 09:24):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
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é

Email Gateway (Aug 22 2022 at 09:27):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

Last updated: Apr 19 2024 at 20:15 UTC