### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Graph theory

### Session Graph_Theory

- Rtrancl_On
- Stuff
- Digraph
- Bidirected_Digraph
- Arc_Walk
- Pair_Digraph
- Digraph_Component
- Vertex_Walk
- Digraph_Component_Vwalk
- Digraph_Isomorphism
- Auxiliary
- Subdivision
- Euler
- Kuratowski
- Weighted_Graph
- Shortest_Path
- Graph_Theory

### Used by

- MLSS Decision Procedure
- Expander Graphs
- Verification of Query Optimization Algorithms
- Combinatorial Design Theory
- Planarity Certificates
- Positional Determinacy of Parity Games
- An Axiomatic Characterization of the Single-Source Shortest Path Problem

## Cite

×

Graph_Theory-AFP

    @article{Graph_Theory-AFP,
      author  = {Lars Noschinski},
      title   = {Graph Theory},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Graph_Theory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- May 2, 2013 : Isabelle2013