[isabelle-dev] Quotient example with partiality?

[Lukas Bulwahn]

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.


Lukas