[isabelle-dev] Quotient and typedef

[Florian Haftmann]

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.

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)

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.

Hopefully this clarifies my intention.

I'm looking forward to your opinion.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111208/81b0bff7/attachment.asc>