@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ [Mosaic users: please open the URL http://www.cl.cam.ac.uk/Research/HVG/isabelle.html ] ISABELLE 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-94, is significantly faster than Isabelle-93 and has several other improvements. 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. * 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 the HOL System * Zermelo-Fraenkel set theory * an extensional version of Martin-Lvf's Type Theory * two versions of the Logic for Computable Functions: LCF and HOLCF * the classical first-order sequent calculus LK * the modal logics T, S4, and S43 * the Lambda Cube Isabelle's Zermelo-Fraenkel set theory derives general theories of recursive functions and data structures (including mutually recursive trees and forests, infinite lists and infinitely-branching trees). Higher-order logic has similar features. Both logics are sufficiently developed to support high-level proofs, and come with several large examples. Isabelle includes extensive documentation: * "A Gentle Introduction to Isabelle" is a short tutorial. * "Introduction to Isabelle" explains the basic concepts at length, and gives examples. * "The Isabelle Reference Manual" documents nearly all most of Isabelle's facilities, apart from particular object-logics. * "Isabelle's Object-Logics" describes the various logics supplied with Isabelle. * "A Fixedpoint Approach to Implementing (Co)inductive Definitions" describes the induction/coinductive definition package for ZF. HOW TO GET ISABELLE Isabelle is distributed in source format by anonymous ftp from the University of Cambridge. Instructions: * Connect to host ftp.cl.cam.ac.uk * 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 Isabelle94.tar.gz from that directory. * "get" the following files, which are the documentation: isabelle_tutor.dvi.gz : "A Gentle Introduction to Isabelle" intro.dvi.gz : "Introduction to Isabelle" logics.dvi.gz : "Isabelle's Object-Logics" ref.dvi.gz : "The Isabelle Reference Manual" ind-defs.dvi.gz : "A Fixedpoint Approach to (Co)inductive Definitions" Isabelle is also available from the Technical University of Munich. Connect to host ftp.informatik.tu-muenchen.de; go to directory local/lehrstuhl/nipkow. The file Isabelle94.tar.gz should be gunzipped, then extracted using tar: gunzip -c Isabelle94.tar.gz | tar xf - --------------------------------------------------------------------------- CHANGES FROM ISABELLE-93 * The simplifier is even faster than before. * HOL supports (co)inductive definitions, datatype and primitive recursive functions, with a nice syntax. * ZF supports (co)inductive definitions and (co)datatypes, which may use infinite branching. There are new theories of order type, cardinals and AC * More flexible theory structure, with a new "defs" section for definitions * Incompatibility: the name of the theory file must now be identical to the name of the actual theory, and need not be in lower case. A perl script is provided to rename existing theory files. --------------------------------------------------------------------------- CHANGES FROM ISABELLE-92 * 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, Isabelle now provides a comprehensive inductive and coinductive definition package using least and greatest fixedpoints. ------------------------------------------------------------------------------- Lawrence C. Paulson Computer Laboratory University of Cambridge Pembroke Street Cambridge CB2 3QG England E-mail: Larry.Paulson@cl.cam.ac.uk Tobias Nipkow Institut f|r Informatik TU M|nchen 80290 M|nchen Germany E-mail: Tobias.Nipkow@informatik.tu-muenchen.de