A Modular First Formalisation of Combinatorial Design Theory

TL;DR

This paper introduces a modular, locale-based formalisation of combinatorial design theory in Isabelle, enabling flexible and concise specifications and proofs of design properties and theorems.

Contribution

It presents the first modular formalisation of combinatorial designs using locales in Isabelle, enhancing usability and adaptability of the library.

Findings

Library includes formal definitions and proofs for key design properties.

Locale-centric approach effectively specifies various design types and hierarchies.

The formalisation is concise, adaptable, and demonstrates the utility of locales in mathematical structures.

Abstract

Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using Isabelle and assesses the usability of a locale-centric approach to formalisations of mathematical structures. We demonstrate how locales can be used to specify numerous types of designs and their hierarchy. The resulting library, which is concise and adaptable, includes formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs.