Re: [isabelle] Defining equality for a new type



Sorry, I messed up my counterexample. I meant:

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

but

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

John

On 7 Sep 2012, at 17:24, John Wickerson wrote:

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