Modular structures as dependent types in isabelle

Abstract

This paper describes a method of representing algebraic structures in the theorem prover Isabelle. We use Isabelle’s higher order logic extended with set theoretic constructions. Dependent types, constructed as HOL sets, are used to represent modular structures by semantical embedding. The modules remain first class citizen of the logic. Hence, they enable adequate formalization of abstract algebraic structures and a natural proof style. Application examples drawn from abstract algebra and lattice theory — the full version of Tarski’s fixpoint theorem — validate the concept.