Local Theory Specifications in Isabelle/Isar

Abstract

The proof assistant Isabelle has recently acquired a “local theory” concept that integrates a variety of mechanisms for structured specifications into a common framework. We explicitly separate a local theory “target”, i.e. a fixed axiomatic specification consisting of parameters and assumptions, from its “body” consisting of arbitrary definitional extensions. Body elements may be added incrementally, and admit local polymorphism according to Hindley-Milner. The foundations of our local theories rest firmly on existing Isabelle/Isar principles, without having to invent new logics or module calculi.

Specific target contexts and body elements may be implemented within the generic infrastructure. This results in a large combinatorial space of specification 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 definitional packages is reasonably simple, and allows to re-use sophisticated tools in a variety of target contexts. For example, a recursive function may be defined depending on locale parameters and assumptions, or an inductive predicate definition may provide the witness in a type-class instantiation.