Re: [isabelle] graph theory in isabelle - nominal?



On 29.01.2012 14:24, John Wickerson wrote:
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?)

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 end nodes).

It is not yet part of the Isabelle distribution. For the time being, you can find it at (look at the master branch):

  http://www21.in.tum.de/~noschinl/git/?p=graph-formalization.git

However, I don't provide an operation for disjoint union of graphs.

  -- Lars





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