Formalisation of Hall’s Theorem for Countable Infinite Graphs

This work presents two formalisations in Isabelle/HOL of the extension of Hall’s marriage theorem for finite graphs to countable infinite graphs. The proofs use a formalisation of the authors’ countable set-theoretical version of Hall’s theorem, which was proved using a formalisation in Isabelle/HOL of the compactness theorem for propositional logic by dealing with finite families of sets through the well-known marriage-condition characterisation. The first formalisation focuses on maintaining specifications and proofs as closely as possible to textbook proofs. The second one states the theorem directly in terms of the existence of perfect matchings over finite and infinite graphs, profiting from the conciseness of Isabelle/HOL locales’ technology. The development contributes to mechanising countable infinite versions of properties equivalent to Hall’s marriage theorem in contexts other than set theory.