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,

Jeremy

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,
	Florian






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