Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Tue, 1 Sep 1992 12:22:50 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05853;
          Tue, 1 Sep 92 04:13:22 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05848;
          Tue, 1 Sep 92 04:13:12 -0700
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Tue, 1 Sep 1992 12:11:46 +0100
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl, juan%panther@it.unige.dist.carla
Subject: Inductive Definitions Report.
Date: Tue, 01 Sep 92 12:11:40 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.468:01.08.92.11.11.50"@cl.cam.ac.uk>


Juanito Camilleri and I have prepared a technical report describing 
a collection of case studies using the HOL inductive definitions
package. The report reference is

    J. Camilleri and T. Melham,
    Reasoning with Inductively Defined Relations
    in the HOL Theorem Prover, Technical Report 
    No. 265, University of Cambridge Computer
    Laboratory (August 1992).

    ABSTRACT. Inductively defined relations are among the
    basic mathematical tools of computer science. Examples
    include evaluation and computation relations in
    structural operational semantics, labelled transition
    relations in process algebra semantics,
    inductively-defined typing judgements, and proof
    systems in general.  This paper describes a set of HOL
    theorem-proving tools for reasoning about such
    inductively defined relations.  We also describe a
    suite of worked examples using these tools.

If you are interested in a copy, just send me an email message and
I'll send you one by post.

The HOL source code for the case studies is also available and will
be installed in the contrib directory of version 2.01.  I will also
arrange for it to be made available (in the next day or two) from the
Cambridge ftp machine ftp.cl.cam.ac.uk (128.232.0.56) in the 
directory "hol".  The file will be called rule-induction.tar.Z.

Tom