In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and demonstrating their properties. We establish the uniqueness of derivations, drawing upon Rosens 1975 research, and verify the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of our formalisation approach. The paper details our methodology in employing Isabelle/HOL, including key design decisions that shaped the current iteration. We explore the technical complexities involved in applying higher-order logic, aiming to give readers an insightful perspective into the engaging aspects of working with an Interactive Theorem Prover. This work emphasizes the increasing importance of formal verification tools in clarifying complex mathematical concepts.

翻译：本文利用Isabelle/HOL开发了双推图变换基本理论的形式化框架。我们的工作包括定义核心概念（如图、态射、推出和拉回）并证明其性质。基于Rosen 1975年的研究，我们确立了推导的唯一性，并通过Ehrig和Kreowski 1976年的证明验证了Church-Rosser定理，从而展示了形式化方法的有效性。本文详细阐述了采用Isabelle/HOL的技术方法，包括塑造当前版本的关键设计决策。我们探讨了应用高阶逻辑所涉及的技术复杂性，旨在为读者提供在交互式定理证明器工作中的深刻视角。这项工作强调了形式化验证工具在澄清复杂数学概念中日益增长的重要性。