Re: [isabelle] Defining equality for a new type



Dear John,
Equality is not something you get to define. It already exists, at all types already introduce and those yet to be formally introduced. Polymorphism doesn't mean you get to define it at each type whatever way you please. It means that is has been defined, or otherwise introduced, in a way that is uniform at all types. Among other things, it is a relation satisfying

HOL.subst: [|?s = ?t; ?P ?s |] ==> ?P ?t

no matter what type ?s and ?t have.

If you create a new type (which is what I'm guessing you really want to do), then two elements in the new type are equal iff their representations in the underlying model are equal. I don't quite understand the definition of the type you are trying to create, but it sounds to me like you really want to have an underlying model that starts with (some collection of) sets of something (pairs?) and that you then want to define an equivalence relation on those sets, and then your model would be (some of) the equivalence classes.
---Elsa

On 9/7/12 10:20 AM, 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.