[isabelle] Defining equality for a new type



Hi,

I'm trying to define a new type which is essentially a set of 3 pairs.
Two objects of that type are equal iff 2 of the pairs are equal. I
have a few questions:

1) If I declare that type using 'typedecl' then how do I express that
it's essentially a set of 3 pairs? 'type_synonym' doesn't seem to be
appropriate since the existing equality on sets of pairs conflicts
with my notion of equality.

2) Even if I declare a new type, does my notion of equality conflict
with any of the existing lemmas, creating a contradiction? Equality is
polymorphic, so I should be able to define it whichever way I want,
right?

Thanks a lot for your time in advance.

John





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