Modular Reasoning in Isabelle
University of Cambridge, Computer Laboratory, 1999 - Logic programming languages - 128 pages
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."
What people are saying - Write a review
We haven't found any reviews in the usual places.
abstract algebra adequacy algebraic structures application assumptions axclass axioms base type bijection binop Calculus of Constructions calM card(M carrier Chapter class citizens class representation combinatorial argument concept of locales construction constructors contains declarations define dependent types derive E-types elements enable example explicit export fixed forgetful functor formulas ft Ml function global Hence higher order logic higher order structure homomorphisms II-set image structure implementation IMPS instantiation inverse Isabelle theory Isabelle's Isabelle/HOL Lagrange's theorem Larch locale constants locale definitions locale rules logic theorem provers mathematical mathematical proof max-n mechanism meta-logic modular reasoning modular structures module systems monoid normal subgroups notation notion object logics order logic theorem parameter structures polymorphism predicate pretty printing syntax proof of Sylow's PROP group G proved RelM ft represent scope Section semigroup set_r_cos G H signature struc subgroup subsets Sylow's proof Sylow's theorem syntactical theory interpretation trait type class type theory