Re: [isabelle] Theory of labeled, directed graphs in Isabelle



Hi Simon,

> I'm looking for a graph theory in Isabelle that supports directed graphs
> with labeled edges. Has anybody already done such a development or knows
> some good pointers on how to model these?

I recently formalized such graphs for some work I did on termination.
You can find it in recent development snapshots
(HOL/Library/Graphs.thy). But since I created this for a particular task
(representing size-change graphs in termination proofs) it is probably
not very well developed, and I don't know if it fits your needs.

My graphs are basically just relations with a new constructor wrapped
around them:

datatype ('n, 'e) graph = Graph "('n * 'e * 'n) set"

This means that the set of nodes is assumed to be the whole type, which
is not what everybody wants, I suppose... Also, since they can be
infinite and so on, they are rather abstract (as opposed to concrete
data structures for efficient computation).

Operations on graphs are a certain composition, addition (which is just
union) and transitive closure. There is also a notion of (finite and
infinite) path.

What is the application you have in mind?

Alex






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