*To*: Ramana Kumar <rk436 at cam.ac.uk>, John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] graph theory in isabelle - nominal?*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Mon, 30 Jan 2012 23:20:14 +1100*Accept-language*: en-US*Acceptlanguage*: en-US*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAMej=25Jo3+zSvFAEqhBRCHDm4ssOz7O_5Acak=nJTbrZHJagQ@mail.gmail.com>*References*: <12454106-4B8B-4F3A-B226-A2F02EA4044B@cam.ac.uk> <CAMej=26a_-=mzZF_uAuuH0JcjfF-Y8QY6CdWVnDuVO-YhYEUDw@mail.gmail.com> <A716DCAC-864D-447B-82A6-FD66E28FBA36@cam.ac.uk>, <CAMej=25Jo3+zSvFAEqhBRCHDm4ssOz7O_5Acak=nJTbrZHJagQ@mail.gmail.com>*Thread-index*: AczfLAaWBWG+38CuSWK3CrQF50aAEwAHHdN/*Thread-topic*: [isabelle] graph theory in isabelle - nominal?

My two cents worth: it might make more sense to use the quotient package than the nominal package. Your intuition is that graph equality should be naming-independent. Define graphs as sets of pairs in some big-enough naming alphabet (naturals, strings, unspecified type 'a ...) and quotient by the equivalence relation of bijective renaming. That should give you a new type whose notion of equality matches your intuition. You may then have a bit of work to do to define the syntax and operations you need within the new type. I've never used the quotient package and don't know how much it will help you here. I think you could, for instance, define your disjoint union operator on the pairwise representation (easy) then lift it to an operator in the graph type by showing it respects the equivalence relation (tool support desirable). This is quite a different approach to Lars' so the relative merits should be thought about. Yours, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

**References**:**[isabelle] graph theory in isabelle - nominal?***From:*John Wickerson

**Re: [isabelle] graph theory in isabelle - nominal?***From:*Ramana Kumar

**Re: [isabelle] graph theory in isabelle - nominal?***From:*John Wickerson

**Re: [isabelle] graph theory in isabelle - nominal?***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] soundness of Isabelle/HOL
- Next by Date: Re: [isabelle] soundness of Isabelle/HOL
- Previous by Thread: Re: [isabelle] graph theory in isabelle - nominal?
- Next by Thread: Re: [isabelle] graph theory in isabelle - nominal?
- Cl-isabelle-users January 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