Technical reports

Modular reasoning in Isabelle

Florian Kammüller

August 1999, 128 pages

This technical report is based on a dissertation submitted April 1999 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Clare College.

Abstract

This work is concerned with modules for higher order logic theorem provers, in particular Isabelle. Modules may be used to represent abstract mathematical structures. This is typical for applications in abstract algebra. In Chapter 1, we set out with the hypothesis that for an adequate representation of abstract structures we need modules that have a representation in the logic. We identify the aspects of locality and adequacy that are connected to the idea of modules in theorem provers.

In Chapter 2, we compare systems of interactive theorem provers and their applicability to abstract algebra. Furthermore we investigate a different family of proof systems based on type theory in Section 2.4.

We validate our hypothesis by performing a large case study in group theory: a mechanization of Sylow’s theorem in Chapter 3.

Drawing from the experience gained by this large case study, we develop a concept of locales in Chapter 4 that captures local definitions, pretty printing syntax and local assumptions. This concept is implemented and released with Iasbelle version 98-1.

However, this concept alone is not sufficient to describe abstract structures. For example, structures like groups and rings need a more explicit representation as objects in the logic. A mechanization of dependent Σ-types and Π-types as typed sets in higher order logic is produced in Chapter 5 to represent structures adequately.

In Chapter 6, we test our results by applying the two concepts we developed in combination. First, we reconsider the Sylow case study. Furthermore, we demonstrate more algebraic examples. Factorization of groups, direct product of groups, and ring automorphisms are constructions that form themselves groups, which is formally proved. We also discuss the proof of the full version of Tarski’s fixed point theorem. Finally we consider how operations on modules can be realized by structures as dependent types. Locales are used in addition; we illustrate the reuse of theorems proved in a locale and the construction of a union of structures.

Full text

PDF (11.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-470,
  author =	 {Kamm{\"u}ller, Florian},
  title = 	 {{Modular reasoning in Isabelle}},
  year = 	 1999,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-470.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-470},
  number = 	 {UCAM-CL-TR-470}
}