Re: [isabelle] Defining equality for a new type



Hi John,

I don't think that's a good notion of equality, because it's not transitive.

{(1,2);(3,4);(5,6)} = {(1,2);(3,4);(7,8)} = {(1,2);(5,6);(7,8)}

but 

{(1,2);(3,4);(5,6)} =/= {(1,2);(5,6);(7,8)}

Best wishes,
John

On 7 Sep 2012, at 17:20, John Munroe wrote:

> 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.