[isabelle-dev] Quotient example with partiality?
bulwahn at in.tum.de
Mon Nov 28 19:34:40 CET 2011
On 11/28/2011 07:25 PM, Florian Haftmann wrote:
> Hi all,
> I'm asking myself the question how one would define rational numbers
> using the quotient package. The key issue is that the equivalence
> relation here is partial, ruling out denominators of value zero. In the
> Isabelle reference manual I can find »partial:« in a syntax diagram but
> not any concrete example in the distribution.
> The reason why I ask is that I want to understand if *every* typedef
> specification can be written as quotient type specification (in a
> straightforward manner). If yes, quotient_type could replace typedef in
> user space in general, and many recent requests for adjusting the
> user-space behavior of typedef would then rather apply to quotient_type.
Actually, the quotient package does more than an simple type definition.
It also defines some further constants.
>> many recent requests for adjusting the user-space behavior of typedef would then rather apply to quotient_type.
Also, I do not see the clear advantage how the suggested change would
make the adjustments simpler.
I would rather imagine that the quotient_type command could be
assimilated by extending the typedef command to enable to hook the pre-
and post processing of quotient type into typedef.
More information about the isabelle-dev