[Prev][Next][Index][Thread]
new Isabelle available by ftp
ISABELLE-93
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.
[Compatibility note: This simplifier is much faster and easier to use than
Isabelle-92's. Congruence rules are no longer required! The old
simplifier remains available for the time being because it is more general
than the new one.]
* 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\"of'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.
Isabelle-93 includes extensive documentation, on the subdirectory Doc:
* "Introduction to Isabelle" explains the basic concepts at length, and
gives examples. (71 pages)
* "The Isabelle Reference Manual" documents nearly all most of Isabelle's
facilities, apart from particular object-logics. (85 pages)
* "Isabelle's Object-Logics" describes the various logics supplied with
Isabelle. It also describes how to define new logics. (166 pages)
* "A Fixedpoint Approach to Implementing (Co)Inductive Definitions"
describes the induction/coinductive definition package for ZF. (31 pages)
---------------------------------------------------------------------------
Isabelle-93 is available by anonymous ftp from the University of Cambridge.
Instructions:
* Connect to host ftp.cl.cam.ac.uk [128.232.0.56]
* Use login id "ftp" with your internet address as password
* put ftp in BINARY MODE ("binary")
* go to directory ml (by typing "cd ml")
* "get" the file Isabelle93.tar.gz from that directory.
Here is a sample dialog:
ftp
ftp> open ftp.cl.cam.ac.uk
Name: ftp
Password: <your internet address>
ftp> binary
ftp> cd ml
ftp> get Isabelle93.tar.gz
ftp> quit
Isabelle-93 is also available from the Technical University of Munich.
Connect to host ftp.informatik.tu-muenchen.de [131.159.0.198]; go to
directory local/lehrstuhl/nipkow.
The addresses 128.232.0.56 and 131.159.0.198 are correct as of 12/93
but are subject to change over time. The names ftp.cl.cam.ac.uk and
ftp.informatik.tu-muenchen.de are permanent.
---------------------------------------------------------------------------
The file Isabelle93.tar.gz should be gunzipped, then extracted using tar:
gunzip -c Isabelle93.tar.gz | tar xf -
[gunzip is a GNU compression utility and is available from the usual sites.]
This will create the directory Isabelle93, which should contain 13
subdirectories; its total size is about 3 megabytes.
The file COPYRIGHT contains the Copyright notice and Disclaimer of Warranty.
The file README contains instructions for compiling Isabelle.
Unfortunately, Isabelle-93 is NOT upwards compatible with its predecessor.
See Doc/CHANGES-93.txt for advice, particularly on converting to the new
simplifier.
---------------------------------------------------------------------------
Lawrence C Paulson E-mail: Larry.Paulson@cl.cam.ac.uk
Computer Laboratory Phone: +44-223-334600
University of Cambridge Fax: +44-223-334678
Pembroke Street
Cambridge CB2 3QG
England
Tobias Nipkow E-mail: Tobias.Nipkow@informatik.tu-muenchen.de
Institut f\"ur Informatik Phone: +49-89-21052690
TU M\"unchen Fax: +49-89-21058183
80290 M\"unchen
Germany