[isabelle-dev] Quotient and typedef

[Lukas Bulwahn]

On 12/08/2011 02:35 PM, Florian Haftmann wrote:
> Dear all,
>
> since my post on quotient and partiality created some confusion, I want
> to cast some light on it from a more direct perspective.
Just a few short comments from my side:
> Concerning »typedef«, we currently have two conflicting issues:
>
> a) From a foundational perspective, we want to leave »typedef« untouched
> »as it is«
>
> b) Recently, »typedef« in userspace became more popular (again), and
> there a some awkward things about it:
> * archaic naming, which ignores contemporary namespace conventions
> * sets in the specification, which is particularly silly if predicates
> already exist (e.g. xs \<in>  {xs. distinct xs} ==>  ...)
> * technical and difficult-to-remember syntax (do you know by heart in
> which order the two morphism symbols have to be written?  where to place
> an infix syntax, or maybe even a syntax for the morphism symbols?  and
> that (open) actually denotes that no characteristic set is defined)?
> * _.eqI and _.eq_iff, theorems nowadays considered fundamental (cf.
> Library/Dlist.thy et al.), are not proved automatically
> * desire to automagically register certain type properties (e.g. for the
> emerging lifting machinery)
> * (maybe you can add more)
I do agree that there is always some confusion when using typedef, but 
to some extent, this is simply caused by the fact that we do not define 
new types on a daily basis right now.
I also noticed that I sometimes just use a datatype with one constructor 
because datatype does provide a few lemmas and I know datatype's syntax 
better than typedef's.

> None of the b) issues is pressing on its own, but in summary I consider
> them critical enough to call for a solution.
>
> My idea then is the following:
>
> 1) Leave »typedef« untouched, as (internal) foundational mechanism, for
> bootstrap reasons (datatypes prod, sum, nat), and whenever a user thinks
> she needs it.
>
> 2) Provide a more convenient user-interface for user-space »typedefs«
>
> Now, if »quotient« »as it is« can cover every typedef specification, a
> reasonable answer would be to establish »quotient« as the canonical
> user-interface for non-datatype type specifications, even for cases like
> dlist where there is no non-trivial quotient, and resolve all those b)
> issues on the quotient level.

To show that the quotient_type and its friends (quotient_definition, the 
lifting method) is useful, Cezary already provided examples of theories 
where manual quotient definitions and lemmas were replaced by 
definitions and lemmas of the quotient package, e.g., the construction 
of the integers.

In my opinion, one part of making the quotient package more visible is 
to continue to extend these examples to the point, where we can simply 
replace the manual quotient definitions and lifting (in the main images) 
by the automatic ones.


Lukas