Isabelle-93

Appeared in Volume 7/1, February 1994

Keywords: theorem provers.

Isabelle is a generic theorem prover. New logics are introduced by specifying their syntax and rules of inference. Proof procedures can be expressed using tactics and tacticals. The latest version, Isabelle-93, is significantly faster than Isabelle-92 and has several other improvements.

Theories may now specify rewrite rules for syntax. This eliminates most ML code from syntax definitions, and conveniently handles trivial definitions such as 1==succ(0). Theory dependencies are now recorded internally; Isabelle can auto-load a theory's ancestors. A search path variable specifies where Isabelle should look for theory files.

For ZF only, Isabelle now provides a comprehensive inductive and coinductive definition package using least and greatest fixedpoints.

Isabelle provides a high degree of automation:

A generic simplifier performs rewriting by equality relations such as = and <->. It handles conditional rewrite rules, can perform automatic case splits, and extracts rewrite rules from the context while descending into an expression.
A generic package supports classical reasoning in first-order logic, set theory, etc.

Isabelle can support a wide variety of logics, and comes with several built-in ones:

many-sorted first-order logic, constructive and classical versions
higher-order logic, similar to that of Gordon's HOL
Zermelo-Fraenkel set theory
an extensional version of Martin-Löf's Type Theory
the classical first-order sequent calculus LK
the modal logics T, S4, and S43
the Logic for Computable Functions, LCF
the Lambda Cube

Isabelle's Zermelo-Fraenkel set theory derives a theory of functions, well-founded recursion, and several recursive data structures (including mutually recursive trees and forests, as well as infinite lists). Higher-order logic has similar features. Both logics are sufficiently developed to support high-level proofs.

Unfortunately, Isabelle-93 is not upwards compatible with its predecessor. See Doc/CHANGES-93.txt for advice, particularly on converting to the new simplifier.

Isabelle-93 is available by anonymous FTP from the Univ. of Cambridge:
ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz

Isabelle-93 is also available from the Technical Univ. of Munich. Connect to:
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow

The file Isabelle93.tar.gz should be gunzipped, then extracted using tar:
gunzip -c Isabelle93.tar.gz | tar xf -

For more information contact:

Lawrence C Paulson
Computer Lab., Univ. of Cambridge
Cambridge CB2 3QG, UK
Email: Larry.Paulson@cl.cam.ac.uk
Tel: +44 223 334 600
Fax: +44 223 334 678

Tobias Nipkow
Institut für Informatik, TU München
80290 München, Germany
Email: Tobias.Nipkow@informatik.tu-muenchen.de
Tel: +49 89 21 052 690
Fax: +49 89 21 058 183