*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: [isabelle] graph theory in isabelle - nominal?*From*: Christian Urban <urbanc at in.tum.de>*Date*: Mon, 30 Jan 2012 15:01:32 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <12454106-4B8B-4F3A-B226-A2F02EA4044B@cam.ac.uk>*References*: <12454106-4B8B-4F3A-B226-A2F02EA4044B@cam.ac.uk>*Reply-to*: christian.urban at kcl.ac.uk

Hi John, If I am allowed to throw in my 2 cents. I can confirm Ramana's point: Nominal does not help you much, except it does use some general lemmas about renaming things: like if you have a set of names, rename it to something else, avoiding some third set of names. This might be still handy for you. Comfortable Barendregt-style reasoning is only supported for nominal datatypes, unfortunately. Also as Ramana and Thomas already pointed out, the quotient package might be of help to define the type of graphs you want. This might need a bit of theory-engineering to pull this off. If you make any progress with this, Cezary and I would be very interested in it. PS: Recently, we were also in need of defining the disjoint union of (named) graphs for a formalisation of automata theory and regularity of languages. We abandoned it, because it looked too ugly to us. In the end, we just used regular expressions and proved all what we wanted with them... never touching automata/graphs. ;o) Best wishes, Christian John Wickerson writes: > Hello all, > > I want to formalise a little bit of graph theory in Isabelle. (Specifically, I'm interested in directed labelled multigraphs.) In particular, I need a (disjoint) union operation on graphs. Here is a typical definition of this operation, which I've copied from a random textbook on graph theory: > > > Let G and H be two given graphs. The disjoint union of G and H, denoted by G \union H, is defined to be the graph with vertex set V(G) \union V(H), where V(G) and V(H) are made disjoint by renaming if necessary, and edge set E(G) \union E(H). > > A couple of questions: > > 1. Is there already a theory of graphs in Isabelle? (A previous message [1] on this mailing list referred to a "HOL/Library/Graphs.thy" theory, but I couldn't find a theory at that location -- perhaps it's not there any more?) > > 2. If there isn't a pre-existing theory, and I roll my own instead, does anybody have any tips on how best to go about it? The phrase "made disjoint by renaming if necessary" smells a lot like Barendregt's variable convention for the lambda-calculus. So I'm wondering if I need Nominal Isabelle to formalise graph theory -- is that the case? > > Thanks very much, > John > > -- > [1] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2007-April/msg00026.html --

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

- Previous by Date: [isabelle] Fwd: 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: [isabelle] soundness of Isabelle/HOL
- 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