[isabelle-dev] Quotient example with partiality?

[Lukas Bulwahn]

On 11/29/2011 06:21 AM, Cezary Kaliszyk wrote:
> When developing the quotient package we included the infrastructure
> for defining quotient types with partial equivalence relations, however
> since one of the main uses was supposed to be nominal (where its
> always reflexive) we did not test the partial functionality too much.
>
> The idea of using the quotient package with partial equivalence relations
> is that two changes need to be done:
>
> First if the user specifies 'partial:' in the quotient_type definition,
> the obligation to prove changes from 'equivp' to 'part_equivp'. Which
> is simpler,
> but then less lifting can be done automatically (to be more precise, some
> of the theorems that allow for automatic regularization do hold only for
> reflexive equivalence relations).
Hi Cezary,

could you add this explanation for the partial option to the existing 
IsarRef documentation of quotient types to make sure that this piece of 
knowledge is not just archived here?


Lukas