Isabelle

[Isabelle logo]

Isabelle is a popular generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).

[Cambridge] [Munich] This page provides general information on Isabelle, more details are available on the local Isabelle pages at Cambridge and Munich. See there for information on projects done with Isabelle, mailing list archives, research papers, the Isabelle bibliography, and Isabelle workshops and courses.

Obtaining Isabelle

The latest version is Isabelle98-1, it is available from several mirror sites.

What is Isabelle?

Isabelle can be viewed from two main perspectives. On the one hand it may serve as a generic framework for rapid prototyping of deductive systems. On the other hand, major existing logics like Isabelle/HOL provide a theorem proving environment ready to use for sizable applications.

Isabelle's Logics

The Isabelle distribution includes a large body of object logics and other examples (see the Isabelle theory library).
Isabelle/HOL
is a version of classical higher-order logic resembling that of the HOL System.
Isabelle/HOLCF
adds Scott's Logic for Computable Functions (domain theory) to HOL.
Isabelle/FOL
provides basic classical and intuitionistic first-order logic. It is polymorphic.
Isabelle/ZF
offers a formulation of Zermelo-Fraenkel set theory on top of FOL.

Isabelle/HOL is currently the best developed object logic, including an extensive library of (concrete) mathematics, and various packages for advanced definitional concepts (like (co-)inductive sets and types, well-founded recursion etc.). The distribution also includes some large applications, for example correctness proofs of cryptographic protocols (HOL/Auth) or communication protocols (HOLCF/IOA).

Isabelle/ZF provides another starting point for applications, with a slightly less developed library. Its definitional packages are similar to those of Isabelle/HOL. Untyped ZF provides more advanced constructions for sets than simply-typed HOL.

There are a few minor object logics that may serve as further examples: CTT is an extensional version of Martin-Löf's Type Theory, Cube is Barendregt's Lambda Cube. There are also some sequent calculus examples under Sequents, including modal and linear logics. Again see the Isabelle theory library for other examples.

Defining Logics

Logics are not hard-wired into Isabelle, but formulated within Isabelle's meta logic: Isabelle/Pure. There are quite a lot of syntactic and deductive tools available in generic Isabelle. Thus defining new logics or extending existing ones basically works as follows:
  1. declare concrete syntax (via mixfix grammar and syntax macros),
  2. declare abstract syntax (as higher-order constants),
  3. declare inference rules (as meta-logical propositions),
  4. instantiate generic automatic proof tools (simplifier, classical tableau prover etc.),
  5. manually code special proof procedures (via tacticals or hand-written ML).
The first three steps above are fully declarative and involve no ML programming at all. Thus one already gets a decent deductive environment based on primitive inferences (by employing the built-in mechanisms of Isabelle/Pure, in particular higher-order unification and resolution). For sizable applications some degree of automated reasoning is essential. Instantiating existing tools like the classical tableau prover involves only minimal ML-based setup. One may also write arbitrary proof procedures or even theory extension packages in ML, without breaching system soundness (Isabelle follows the well-known LCF system approach to achieve a secure system).

Mailing list

Use the mailing list isabelle-users@cl.cam.ac.uk to discuss problems and results. (Why not subscribe?)