Audience
- Frédéric Boulanger
- Chantal Keller
- Safouan Taha
- Frédéric Tuong
- Benoît Valiron
- Burkhart Wolff
- Lina Ye
Isabelle Kernel
Burkhart
- The Kernel of Isabelle
The kernel design of Isabelle (which has many elements in common with other interactive theorem proving systems belonging to the "Family of LCF-style provers" (HOL, HOL4, ProofPower, HOL-Light, Coq, Isabelle, Agda, ... but not PVS nor ACL2)) having their roots in an implementation of "Stanford LCF" and its re-implementation in SML (which was historically designed for this purpose) in "Edinburg LCF".
The design allows for a small-trusted kernel and user-programmed, but logically safe extensions.
Fact: there are nowadays two kernels in Isabelle:
- Micro-kernel: existing since the beginning (Larry Pawson first Isabelle versions from 1987). It provides infrastructure for types, terms, theories, theorems. The kernel also provides for efficiency reasons acces to to the unification (which could be considered outside). Tactics and tacticals, parsers, etc. are already in "user-land" of the kernel.
- Nano-kernel: existing roughly since Isabelle2005. Provides the notion of "context" which comes in two flavors- the "global" context and the "proof-contexts". Contexts are a kind of container, with an ID and a notion of inheritage (which is checked to be non-cyclic). Notion of "slots": there is a functor that allows for type-safe extensions of contexts with user-defined data. The Nano-Kernel provides the infra-structure for building, tracking, and merging contexts. The Micro-Kernel is at some point "registered" in the Nano-Kernel.
- The "classical" Micro-Kernel (contained in the SML structure "Thm" and below.) establishes the notions
- type, (providing type-variables 'α, schematic type variables '?α, type constructors (_⇒_, _set, _list), type classes as constraints of type-variables))
- term, (λ-terms with constant symbols, free variables, bound variables, schematic variables)
- syntax and theory (=global context), and the notions of certified types and certified term in a theory.
- theorems (thm's), i.e. an abstract data-type that protects in the initial concept a triple written: Γ ⊢'-Θ φ with Γ a list of formulas (the "local context"), a theory Θ (the "global context") and a formula φ.
A theory is roughly a pair (Σ, A) of a signature ("syntax") and a list of axioms A. An initial theory "Pure" is defined providing syntax for the core Pure-operators (constants) _⟹_, _≡_, ⋀ (!!). Formulas are terms of type "prop" also provided by Pure. Besides the ones for equality, Pure has no axioms. It however have a number of built-in "rules", i.e. operations on thm's provided by the Micro-Kernel.
The rules are the following. The usual intuitionistic first-order logical rules:
{$\displaystyle\frac{A\in\Theta}{\vdash A}$}(axiom) {$\ \ \ $} {$\displaystyle\frac{}{A\vdash A}$}(assume) {$\ \ \ $} {$\displaystyle\frac{\Gamma\vdash B[x]\ \ x \not\in \Gamma}{\Gamma\vdash ⋀x.B[x]}$}(⋀-intro) {$\ \ \ $} {$\displaystyle\frac{\Gamma\vdash ⋀x.B[x]}{\Gamma\vdash B[a]}$}(⋀-elim)
{$\ \ \ $}
{$\displaystyle\frac{\Gamma\vdash B}{\Gamma\setminus \{A\}\vdash A⟹B}$}(⟹-intro) {$\ \ \ $} {$\displaystyle\frac{\Gamma_1\vdash A⟹B\ \ \Gamma_2\vdash A}{\Gamma_1\Gamma_2\vdash B}$}(⟹-elim)
and four rules to deal with schematic variables:
{$\displaystyle\frac{\Gamma\vdash B[\alpha]\ \ \alpha \not\in \Gamma}{\Gamma\vdash B[?\alpha]}$} {$\ \ \ $} {$\displaystyle\frac{\Gamma\vdash B[x]\ \ x \not\in \Gamma}{\Gamma\vdash B[?x]}$} (generalize)
{$\ \ \ $}
{$\displaystyle\frac{\Gamma\vdash B[?\alpha]}{\Gamma\vdash B[\alpha]}$} {$\ \ \ $} {$\displaystyle\frac{\Gamma\vdash B[?x]}{\Gamma\vdash B[x]}$} (instantiate)
The axioms for equality read as follows:
- {$(\lambda x.b[x])a ≡ b[a]\ \ \ $} ({$\beta$}-conversion)
- {$x ≡ x\ \ \ $} (reflexivity)
- {$x ≡ y ⟹ P x ≡ P y\ \ \ $} (substitution)
- {$(⋀x.f x ≡ g x) ⟹ f ≡ g\ \ \ $} (extensionality)
- {$(A ⟹ B) ⟹ (B ⟹ A) ⟹ A ≡ B\ \ \ $} (logical equivalence)
A more detailed view can be found in the "Isabelle/Isar implementation Manual", Chapter 2.3, pp 67 ff.
It is a characterizing feature of Isabelle that global contexts are explicit data-structures and not some implicit "state" of the Top-level of the underlying ML environment (as in HOL4 or HOL-Light).
This paves the way for a kernel operation Thm.transfer which implements the meta-level inference:
Θ ⊑ Θ' and Γ ⊢Θ φ implique Γ ⊢Θ' φ
Other Kernel-Interences are:
- axiom
- assume
- ⋀ - intro
- ⋀ - elim
- ⟹ - intro
- ⟹ - elim
- generalize
- instantiate
which are described in the "Isabelle/Isar implementation Manual", Chapter 2.3.1., and correspond to operations provided by the Thm-structure representing the Mikro-Kernel.
The Kernel is purely functional, and its explicit handling of theories as contexts allows to view it as a re-entrant "transaction machine"; this aspect made the massive, fine-grained parallelism of recent Isabelle versions possible.
- Seeking for more parallisation, Makarius Wenzel transformed the "classic" Mikro-Kernel into the "parallelized" version (around 2007). See "Parallel Proof Checking in Isabelle/Isar" of 2009 (p5 for the modified rules)
Key elements of this --- in bu's opinion --- most substantial modification of the Kernel since 1987 are:
- Extension of the notion of "thm" by an additional component Π called "promises", a thm becomes s.th. like: Π, Γ ⊢Θ φ.
- Extension of the set of Kernel inferences by two more base inferences:
- promise (spawn off a proof-context for an own, in parallel checkable proof)
- fulfil (join / collect a spawned off result and instantiate it in the current context).
In order to understand the importance of this modification, recall that that there are HOL-formulas whose validity depends on the instantiation on schematic type variables. Consider:
∃ f ::('?α ⇒ '?α). inj f ∧ ¬ sur f (this is NOT parsable, but presentable in Isabelle Kernel Terms)
If we could have this formula in the assumptions Γ, we could immediately produce logical contradictions; instantiate '?α once by bool and once by ind (the infinite type). For this reason, LCF-designs exclude the use of schematic variables in the assumptions; they are only allowed when exporting an established thm to the global context and must be instantiated when imported in a concrete proof context.
Wenzels extensions override this fundamental restriction of LCF Kernels.