*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Defining equality for a new type*From*: Elsa L Gunter <egunter at illinois.edu>*Date*: Fri, 7 Sep 2012 10:51:09 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAP0k5J5-m6=7eKprCPsu_jvGc0L7wnv_CWo91J0ABK_BD9bw6A@mail.gmail.com>*References*: <CAP0k5J5-m6=7eKprCPsu_jvGc0L7wnv_CWo91J0ABK_BD9bw6A@mail.gmail.com>*Reply-to*: egunter at illinois.edu*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:12.0) Gecko/20120428 Thunderbird/12.0.1

Dear John,

HOL.subst: [|?s = ?t; ?P ?s |] ==> ?P ?t no matter what type ?s and ?t have.

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

**References**:**[isabelle] Defining equality for a new type***From:*John Munroe

- Previous by Date: Re: [isabelle] Defining equality for a new type
- Next by Date: [isabelle] A simple lemma
- Previous by Thread: Re: [isabelle] Defining equality for a new type
- Next by Thread: [isabelle] A simple lemma
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list