*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] graph theory in isabelle - nominal?*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Mon, 30 Jan 2012 11:33:22 +0100*In-reply-to*: <12454106-4B8B-4F3A-B226-A2F02EA4044B@cam.ac.uk>*References*: <12454106-4B8B-4F3A-B226-A2F02EA4044B@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:8.0) Gecko/20120104 Icedove/8.0

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?)

http://www21.in.tum.de/~noschinl/git/?p=graph-formalization.git However, I don't provide an operation for disjoint union of graphs. -- Lars

**References**:**[isabelle] graph theory in isabelle - nominal?***From:*John Wickerson

- Previous by Date: Re: [isabelle] soundness of Isabelle/HOL
- Next by Date: Re: [isabelle] soundness of Isabelle/HOL
- Previous by Thread: Re: [isabelle] graph theory in isabelle - nominal?
- Next by Thread: [isabelle] graph theory in isabelle - nominal?
- Cl-isabelle-users January 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list