[isabelle-dev] Quotient

[Florian Haftmann]

Hi all,

find attached some ideas for the future of quotient_type etc.

Time is too sparse to set everything out in detail here, but a few
corner stones:

* technical separation of lifting infrastructure (with a central role of
the »Quotient« predicate, theory Quotient_Lifting) with the
infrastructure for »defining« new types (theory Quotient_Type_Definition)

* different flavours of type definitions, represented by different locales

* helpful additional theorems for type definitions, esp. concerning code
generation

Maybe future brings an opportunity to discuss that matter.  Anyway, a
lot of that material could help to cleanup and streamline the existing
Quotient stuff in HOL a little.

Cheers,
	Florian

-- 

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: Quotient_Lifting.thy
Type: application/x-extension-thy
Size: 6638 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120218/4259a077/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Quotient_Type_Definition.thy
Type: application/x-extension-thy
Size: 11024 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120218/4259a077/attachment-0003.bin>
-------------- 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/20120218/4259a077/attachment-0001.asc>