Paper Info
Title
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.
Year
DOI
Venue
2008
10.1007/978-3-642-02444-3_10
TYPES
Keywords
Field
DocType
existing definitional package,target context,recursive function,available selection,local theory,local theory specifications,fixed axiomatic specification,local polymorphism,arbitrary definitional extension,specific target context,body element,proof assistant,polymorphism
Programming language,Axiom,Computer science,Algorithm,Witness,Inverse synthetic aperture radar,Porting,Locale (computer software),Predicate (grammar),Recursive functions,Proof assistant
Conference
Volume
ISSN
Citations 
5497
0302-9743
16
PageRank 
References 
Authors
1.22
16
2
Name
Order
Citations
PageRank
Florian Haftmann124713.39
Makarius Wenzel227224.39