Formalization of Biform Theories in Isabelle

Abstract

A biform theory is a combination of an axiomatic theory and an algorithmic theory. It is used to integrate reasoning and computation in a common theory and can include algorithms with precisely specified input-output relationships. Isabelle is one of the leading interactive theorem provers. Isabelle includes locales, a module system that uses theory morphisms to manage theory hierarchies, and that has a rich and extensive library with multiple useful proof and formalization techniques. A case study of eight biform theories of natural number arithmetic is described in the paper “Formalizing Mathematical Knowledge as a Biform Theory Graph” by J. Carette and W. M. Farmer. The biform theories form a graph linked by theory morphisms. Seven of the biform theories are in first-order logic and one is in simple type theory. The purpose of this thesis is to test how a theory graph of biform theories can be formalized in Isabelle by attempting to formalize this case study. We work with locales and sublocales in Isabelle to formalize the test case. The eight biform theories are defined as regular axiomatic theories, while the algorithms are functions defined on inductive types representing the syntax of the theories.