[isabelle] graph theory in isabelle - nominal?
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)
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  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,
>  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