*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] graph theory in isabelle - nominal?*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Sun, 29 Jan 2012 14:57:55 +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>*Sender*: ramana.kumar at gmail.com

On Sun, Jan 29, 2012 at 1:24 PM, John Wickerson <jpw48 at cam.ac.uk> wrote: > > 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). > > 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? > A set-theoretic disjoint union of V(G) and V(H) might work, e.g. the graph union has nodes (True, g) where g is in G and (False, h) where h is in H, rather than explicit renaming. I wouldn't think Nominal Isabelle is an obvious candidate because there's no notion of variable binding in graphs (node names aren't variables, they're not either free or bound, etc.). (Right?) To make the disjoint union above work, I imagine your graphs would be a polymorphic record where an "'a graph" has a record field that is its node (multi)set, and nodes are elements of type "'a". If you found a way to make renaming work instead, then the node multiset could be non-polymorphic (e.g. a multiset of strings). For example you could add characters to the end of all the node names in one graph as necessary when you take a union... This could make it harder to recover the components of a union, or prove properties about unions.

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

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

- Previous by Date: [isabelle] graph theory in isabelle - nominal?
- Next by Date: Re: [isabelle] graph theory in isabelle - nominal?
- Previous by Thread: [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