Local Theory Specifications in Isabelle/Isar
Local Theory Specifications in Isabelle/Isar
复制标题
Isabelle/Isar 中的局域理论规范
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Wenzel
中科院分区：
文献类型：
--
作者：
Florian Haftmann;M. Wenzel
证明助理Isabelle最近获得了一个“局部理论”概念，它将结构化规范的各种机制集成到一个公共框架中。我们显式地将局部理论“目标”(即由参数和假设组成的固定公理规范)与其由任意定义扩展组成的“主体”分开。根据Hindley-Milner的说法，身体元素可以递增地添加，并允许局部多态。我们本地理论的基础牢牢地建立在现有的伊莎贝尔/伊萨尔原理之上，而不必发明新的逻辑或模演算。
可以在通用基础设施内实现特定的目标上下文和主体元素。这导致用户可以使用很大的规范习惯用法组合空间。在这里，我们介绍区域设置、类型类和类实例化的目标。可供选择的主体元素包括原语定义和定理、归纳谓词和集合以及递归函数。移植这样的现有定义包相当简单，并且允许在各种目标上下文中重用复杂的工具。例如，可以根据区域设置参数和假设来定义递归函数，或者归纳谓词定义可以在类型类实例化中提供见证。
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.