[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