[isabelle-dev] Infix syntax for division?

[Manuel Eberl]

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.

Any suggestions?

Cheers,

Manuel


On 02/06/15 20:17, Florian Haftmann wrote:
> Dear all,
>
> http://isabelle.in.tum.de/reports/Isabelle/rev/838025c6e278 introduces
> type classes »(sem)idom_divide« with an explicit partial divide
> operations in integral (semi)domains, which specialises smoothly to
> field division or euclidean division later on. In _ you see how this
> allows to formulate certain results uniformly for both kind of divisions.
>
> So far, this generic division does not carry any infix syntax. Maybe it
> should, but I am uncertain which path to follow:
> a) The radical solution: there is only »_ / _« for both field division
> and euclidean division. How natural is notation like »a / b * b + a mod
> b = a« then?
> b) The conservative solution: partial division has »_ div _«, an (the
> more special) field division »_ / _«. This seems more sensible than the
> other way round since »_ div _« suggests some kind of »incompleteness«.
>
> Any opinions?
>
> Cheers,
>     Florian
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev