Re: [isabelle] Operations over sets in Isabelle

In fact, the operations are defined in the file "SetsAndFunctions" in Library, with useful rewrite rules for appropriately general type classes.

Best wishes,


Florian Haftmann wrote:
Hi Bogdan,

as far as I understand, you want to take the product of two sets and
then apply a binary operator on it.  This can be done using the existing
 image (`) and product operators (<*>), e.g.

	(\<lambda>(a, b). a + b) ` (A <*> N)

form the sum of two sets.

Hope this helps,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.