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

[Alessandro Coglio]

Thank you for the pointers.

BTW, the lemmas in the Sets section were added by Christoph Kreitz based on work by Lambert Meertens (they worked with me on a project), so they should be credited if those lemmas are included in the library (I meant to mention that in the file itself, but forgot). I've attached an updated file with the subsumed lemmas removed and with the attribution added.

It looks like there could be some partial overlap between my modeled-as-functions indexed products and FuncSet. I'll look into that in more detail, and update my development as needed.





On Sep 21, 2013, at 1:12 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> Some of the results in subsection {* Sets *} may be interesting. But your product distribution laws are subsumed by the Sigma_XX_distrib{1,2} laws in Product_Type.thy.
> 
> As for indexed products, check the existing HOL/Library/FuncSet.thy for possible overlaps.
> 
> Larry
> 
> On 21 Sep 2013, at 03:08, Alessandro Coglio <coglio at kestrel.edu> wrote:
> 
>> A theory of indexed products, modeled via maps and also modeled via functions.
>> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130921/de09c33d/attachment-0004.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ProposedLibraryExtensions.thy
Type: application/octet-stream
Size: 22078 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130921/de09c33d/attachment-0002.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130921/de09c33d/attachment-0005.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2095 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130921/de09c33d/attachment.bin>