Email Gateway (Aug 18 2022 at 19:02): Email Gateway (Aug 18 2022 at 19:02):From: Christian Urban <urbanc@in.tum.de>
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
it.
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,
Christian
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:
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?)
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
Last updated: Apr 25 2024 at 20:15 UTC