Re: [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.

ProposedLibraryExtensions.thy
Description: Binary data

On Sep 21, 2013, at 1:12 AM, Lawrence Paulson <l...@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 <cog...@kestrel.edu> wrote: A theory of indexed products, modeled via maps and also modeled via functions.

smime.p7s
Description: S/MIME cryptographic signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev