Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 31 May 1993 13:38:27 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05068; Mon, 31 May 93 05:31:15 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05063; Mon, 31 May 93 05:31:06 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 31 May 1993 13:31:11 +0100 To: info-hol@ted.cs.uidaho.edu Subject: New "Reduction relations" contrib entry Date: Mon, 31 May 93 13:31:01 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:130780:930531123116"@cl.cam.ac.uk> A new contrib directory, and associated compressed tarfile, have been added to the Cambridge FTP area. Both HOL88 and hol90 versions are there. The READ-ME file is appended below to give an idea of the contents. John. %============================================================================% % DIRECTORY: reduct % % % % DESCRIPTION: General theorems about reflexive/symmetric/transitive % % closure of binary relations ("rstc.ml" / "rstc.sml"). % % % % Some basic theorems about confluence and termination of % % abstract reduction relations ("reduct.ml" / "reduct.sml"). % % % % AUTHOR: John Harrison % % University of Cambridge Computer Laboratory % % New Museums Site % % Pembroke Street % % Cambridge CB2 3QG % % England. % % jrh@cl.cam.ac.uk % % % % DATE: 31st May 1993 % %============================================================================% The file "rstc.[s]ml" is a general theory of reflexive, symmetric and transitive closures of arbitrary binary relations (represented as curried functions of type ":*->*->bool"). All distinct combinations of these closures are defined, and a fairly extensive set of theorems proved about each. Although only a few of these are defined using the inductive definitions package (and some of those gratuitously), induction and cases theorems of the standard form are derived, to allow use of the standard rule induction tactics. The file "reduct.[s]ml" is a basic theory of abstract reduction relations (again the nature of the relations is arbitrary). This is far from complete, but provides some potentially useful theorems, e.g. Newman's Lemma (weak confluence /\ strong normalization ==> confluence). The files have been tested in HOL88 v2.01 and hol90.5 as appropriate, and appear to work. Any bug reports or suggestions for improvements should be sent by email to me at jrh@cl.cam.ac.uk. John Harrison, 31st May 1993.