Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 5 Oct 1993 15:14:36 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA21510; Tue, 5 Oct 93 07:06:24 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA21506; Tue, 5 Oct 93 07:06:22 -0700 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 5 Oct 1993 15:05:59 +0100 To: isabelle-users@cl.cam.ac.uk, proof-sci@cs.chalmers.se, logic@cs.cornell.edu, types@dcs.gla.ac.uk, info-hol@cs.uidaho.edu Subject: paper available Date: Tue, 05 Oct 93 15:05:50 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:154360:931005140619"@cl.cam.ac.uk> The following report is available by anonymous ftp from the University of Cambridge. Larry Paulson Set Theory for Verification: II. Induction and Recursion A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski Theorem over a suitable set. Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion. Recursive data structures are expressed by applying the Knaster-Tarski Theorem to a set that is closed under Cartesian product and disjoint sum. Worked examples include the transitive closure of a relation, lists, variable-branching trees and mutually recursive trees and forests. The Schr\"oder-Bernstein Theorem and the soundness of propositional logic are proved in Isabelle sessions. FTP 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 reports (by typing "cd reports") * "get" the file TR312-lcp-set-II.ps.gz from that directory. TR312-lcp-set-II.ps.gz is a gzip'ed Postscript file, and should be unpacked using the Gnu utility gunzip. Part I of the report is available as TR271-lcp-set-theory.dvi.Z from the same directory, but the final version is on directory ml (not reports) and consists of two files: set-I.dvi.Z (text only) and set-I.fig.ps.Z (figures).