[isabelle-dev] Infix syntax for division?
florian.haftmann at informatik.tu-muenchen.de
Fri Jun 5 22:36:25 CEST 2015
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev