[isabelle] Operations over sets in Isabelle

Dear Isabelle Users

I need to use (introduce?) operations over sets in Isabelle. For example, if operation “+” is defined for elements of sets, then we can define sum A+B as a set {c. c=a+b & a\in A & b \in B}  (for example, sum of sets {a,b,c} and {d,e} will be set {a+d, a+e, b+d, b+e, c+d, c+e}). Similarly, if we can multiply elements of set by a constant c, then we can multiply any set A by this constant with definition c*A={d. d=c*a & a\in A}. 

I need to use these operations in R^n, but they can be defined in a more general setting (in a vector space over any field).

The question is, if such operations are already defined in Isabelle? I do not want to redefine such basic concepts, if it already exists. But I cannot find something like this in the Library...

If not, is there any suggestions how exactly I should define this (for example, if such a definition exists in HOL light, it would be better to define them in Isabelle similarly). 

Also, can I use the same notations “+” and “*”? If so, how?

Bogdan Grechuk.      

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