[isabelle-dev] Infix syntax for division?

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150605/70af7d5e/attachment.sig>