Towards Mechanised Proofs in Double-Pushout Graph Transformation

TL;DR

This paper formalizes the double-pushout graph transformation approach within Isabelle/HOL, enabling machine-checked proofs to verify properties like pushouts and their uniqueness, thus supporting rigorous analysis of graph transformation systems.

Contribution

It provides the first formalization of the double-pushout approach in a proof assistant, including proofs of key properties like pushouts and their uniqueness.

Findings

Formalization of graphs, morphisms, and rules in Isabelle/HOL

Proof that deletions and gluings are pushouts

Proof of pushout uniqueness up to isomorphism

Abstract

We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition of direct derivations based on deletion and gluing. We then formalise graph pushouts and prove with Isabelle's help that both deletions and gluings are pushouts. We also prove that pushouts are unique up to isomorphism. The formalisation comprises around 2000 lines of source text. Our motivation is to pave the way for rigorous, machine-checked proofs in the theory of the double-pushout approach, and to lay the foundations for verifying graph transformation systems and rule-based graph programs by interactive theorem proving.