[isabelle] New AFP entry: Graph Theory
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP entry: Graph Theory
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Thu, 02 May 2013 05:27:27 +0200
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130328 Thunderbird/17.0.5
This development provides a formalization of directed graphs, supporting
(labelled) multi-edges and infinite graphs. A polymorphic edge type allows edges
to be treated as pairs of vertices, if multi-edges are not required. Formalized
properties are i.a. walks (and related concepts), connectedness and subgraphs
and basic properties of isomorphisms.
This formalization is used to prove characterizations of Euler Trails, Shortest
Paths and Kuratowski subgraphs.
This archive was generated by a fusion of
Pipermail (Mailman edition) and