Modular Reasoning in Isabelle

Front Cover
University of Cambridge, Computer Laboratory, 1999 - Logic programming languages - 128 pages
0 Reviews
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 module 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 Isabelle version 98-1. However, this concept is alone 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 [sigma]-types and [pi]-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."

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.


Sylows Theorem

5 other sections not shown

Common terms and phrases

Bibliographic information