### Abstract

This entry presents a general library for undirected graph theory - enabling reasoning on simple graphs and undirected graphs with loops. It primarily is inspired by Noschinski's basic ugraph definition in the Girth Chromatic Entry, however generalises it in a number of ways and significantly expands on the range of basic graph theory definitions formalised. Notably, this library removes the constraint of vertices being a type synonym with the natural numbers which causes issues in more complex mathematical reasoning using graphs, such as the Balog Szemeredi Gowers theorem which this library is used for. Secondly this library also presents a locale-centric approach, enabling more concise, flexible, and reusable modelling of different types of graphs. Using this approach enables easy links to be made with more expansive formalisations of other combinatorial structures, such as incidence systems, as well as various types of formal representations of graphs. Further inspiration is also taken from Noschinski's Directed Graph library for some proofs and definitions on walks, paths and cycles, however these are much simplified using the set based representation of graphs, and also extended on in this formalisation.

### License

BSD License

### History

August 18, 2023
  Renamed incident to vincident (vertex incident) and order to gorder to enable inheritance from design theory library

### Topics

- Mathematics/Graph theory

### Session Undirected_Graph_Theory

- Undirected_Graph_Basics
- Undirected_Graph_Walks
- Connectivity
- Girth_Independence
- Graph_Triangles
- Bipartite_Graphs
- Graph_Theory_Relations
- Undirected_Graphs_Root

### Depends on

- Combinatorial Design Theory
- A Probabilistic Proof of the Girth-Chromatic Number Theorem

### Used by

- Derandomization with Conditional Expectations
- Hypergraphs
- Tree Enumeration
- The Balog–Szemerédi–Gowers Theorem

## Cite

×

Undirected_Graph_Theory-AFP

    @article{Undirected_Graph_Theory-AFP,
      author  = {Chelsea Edmonds},
      title   = {Undirected Graph Theory},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Undirected_Graph_Theory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Oct 1, 2022 : Isabelle2021-1