Re: [isabelle] Operator with Pair sets

Dear Omar,

Do you want to have an operator from 'a * ('b set) to 'c * ('d set) or from ('a * 'b) set to ('c * 'd) set? The first parenthesation corresponds to what you have written, but the second version looks more like what I would expect from a "pair set". In case of the latter, the theory Relation defines a number of useful operators, e.g., composition, image, domain and range.

Hope this helps,

On 16/06/16 10:38, Omar Jasim wrote:
Deat list,

I want to ask if there is a theory state that there is an operator map from
pair set ('a x 'b set) to another pair set ('cx'd set) or I should define
it? if there are such related theories please could you give me their names.



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