What is Isabelle?

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.

A bluffer's glance at Isabelle

Isabelle Screenshot

The most widespread instance of Isabelle nowadays is Isabelle/HOL, providing a higher-order logic theorem proving environment ready to use for sizable applications. Anyway, most capabilities mentioned here are not restricted to Isabelle/HOL in particular but may be instantiated for arbitrary calculi.

Isabelle/HOL includes powerful specification tools, e.g. for datatypes, inductive definitions and functions with complex pattern matching.

Proofs are conducted in the structured proof language Isar, allowing for proof text naturally understandable for both humans and computers.

For proofs, Isabelle incorporates some tools to improve the user's productivity. In particular, Isabelle's classical reasoner can perform long chains of reasoning steps to prove formulas. The simplifier can reason with and about equations. Linear arithmetic facts are proved automatically, various algebraic decision procedures are provided. External first-order provers can be invoked through sledgehammer.

Abstract specifications are supported by a module system (aka locales), of with type classes are a special case.

Isabelle provides excellent notational support: new notations can be introduced, using normal mathematical symbols. Definitions and proofs may include LaTeX source, from which Isabelle can automatically generate typeset documents.

Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml and Haskell.

Ample documentation is available, including a Tutorial published by Springer-Verlag.

Isabelle comes with a large theory library of formally verified mathematics, including elementary number theory (for example, Gauss's law of quadratic reciprocity), analysis (basic properties of limits, derivatives and integrals), algebra (up to Sylow's theorem) and set theory (the relative consistency of the Axiom of Choice). Also provided are numerous examples arising from research into formal verification. A vast collection of applications is accessible via the Archive of Formal Proofs, stemming both from mathematics and software engineering.

Isabelle is closely integrated with the Emacs-based ProofGeneral user interface (preview in QuickTime format or in PDF).

Isabelle may serve as a generic framework for rapid prototyping of deductive systems. These are formulated within Isabelle's meta logic Isabelle/Pure, which is suitable for a variety of formal calculi (e.g. axiomatic set theory). Instantiating the generic infrastructure to a particular calculus usually requires only minimal setup in the Isabelle system language ML. One may also write arbitrary proof procedures or even theory extension packages in ML, without breaking system soundness (Isabelle follows the well-known LCF system approach to achieve a secure system).