Re: [isabelle] graph theory in isabelle - nominal?
On 29.01.2012 14:24, John Wickerson wrote:
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  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?)
I am currently developing some a theory of graphs, which can handle
directed labelled multigraphs (graphs are as a "'a set" of vertexes, a
"'b set" of edges and two projections mapping edges to their start and
It is not yet part of the Isabelle distribution. For the time being, you
can find it at (look at the master branch):
However, I don't provide an operation for disjoint union of graphs.
This archive was generated by a fusion of
Pipermail (Mailman edition) and