Florian Haftmann (itestra GmbH), Makarius Wenzel
Local Theory Specifications in Isabelle/Isar
Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008
Abstract
The proof assistant Isabelle has recently acquired a "local theory" concept that integrates a variety of mechanisms for structured speci fications into a common framework. We explicitly separate a local theory "target", i.e. a fixed axiomatic speci fication consisting of parameters and assumptions, from its "body" consisting of arbitrary defi nitional extensions. Body elements may be added incrementally, and admit local polymorphism according to Hindley-Milner. The foundations of our local theories rest fi rmly on existing Isabelle/Isar principles, without having to invent new logics or module calculi.
Specifi c target contexts and body elements may be implemented within the generic infrastructure. This results in a large combinatorial space of specifi cation idioms available to the user. Here we introduce targets for locales, type-classes, and class instantiations. The available selection of body elements covers primitive definitions and theorems, inductive predicates and sets, and recursive functions. Porting such existing de finitional packages is reasonably simple, and allows to re-use sophisticated tools in a variety of target contexts. For example, a recursive function may be de fined depending on locale parameters and assumptions, or an
inductive predicate defi nition may provide the witness in a type-class
instantiation.
