Return-Path: Received: from RI.CMU.EDU by A.GP.CS.CMU.EDU id aa21986; 16 Dec 93 9:40:13 EST Received: from swan.cl.cam.ac.uk by RI.CMU.EDU id aa29094; 16 Dec 93 9:39:15 EST Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 16 Dec 1993 14:36:11 +0000 To: logic@cs.cornell.edu, lprolog@cis.upenn.edu, types@dcs.gla.ac.uk, isabelle-users@cl.cam.ac.uk, proof-sci@cs.chalmers.se, info-hol@cs.uidaho.edu, theorem-provers@mc.lcs.mit.edu Subject: new Isabelle available by ftp Date: Thu, 16 Dec 93 14:36:02 +0000 From: Lawrence C Paulson Message-ID: <"swan.cl.cam.:186640:931216143818"@cl.cam.ac.uk> 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: 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 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