[isabelle] graph theory in isabelle - nominal?



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.