[isabelle] graph theory in isabelle - nominal?

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 

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,

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

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