Hi Manuel, > I also vote for b). I would also like to add that I ran into situations > where I required the notation of an inverse element in a ring. I defined > this as "ring_inv x = 1 div x". For instance, on int, we have "ring_inv > 1 = 1" and "ring_inv (-1) = -1" and everything else is basically > ill-defined, because 1 and -1 are the only units in ℤ. > > Using "inverse" for this would be an idea, since ring_inv and inverse > are equivalent on fields anyway, but that, I think, would also > automatically introduce a rather useless "/" for all rings, which we > probably do not want.
indeed your work on rings inspired me to introduce a unified division.
My idea is to have a type class based on (semi)rings which adds the
necessary algebraic notion to formulate euclidean rings. Somewhere in
the typeclass hierarchy should be a proper fork in order not to pollute
rings with field-specific notions like »/« and vice versa (e.g.
is_unit). Of course you can define all those logically consistenty in
the »wrong« structures, but they do not make much sense.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
