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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
