[isabelle-dev] Some proposed extensions to the Isabelle library

[Alessandro Coglio]

Hello,

The attached file contains a fairly heterogeneous collection of potential extensions to the Isabelle library, which I've been developing as part of some projects that I'm working on. I think that other Isabelle users may find them useful.

Please let me know if you'd rather receive these in smaller chunks, if anything needs more explanations, if anything should be changed to conform to Isabelle library styles/conventions, etc.

I also have a general question about library vs. AFP. There seem to be clear cases of things that should go into the library (e.g. new theorems on lists or sets) and clear cases of things that should go into the AFP (e.g. a theory of context-free grammars). But some cases are less clear to me; for example, while lattices are in the library, I noticed that categories are in the AFP (well, categories are used much less frequently than lattices, so perhaps that's a criterion). More concretely, I've been working on a couple of developments (not included in the attached file) that I can imagine going into either place:
A theory of indexed products, modeled via maps and also modeled via functions.
A theory of ranges over orders/lattices, part of which use the indexed products mentioned above.
Does anybody have any guidance? Out of curiosity, have theories ever moved between library and AFP, in either direction?

Thank you in advance and best regards.



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130920/2f562a48/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ProposedLibraryExtensions.thy
Type: application/octet-stream
Size: 22258 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130920/2f562a48/attachment-0001.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130920/2f562a48/attachment-0003.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2095 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130920/2f562a48/attachment-0001.p7s>