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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
