Via:  uk.ac.nsf; 15 May 89 13:32 BST  (UK.AC.Cam.Cl.scaup)
Date: Mon, 15 May 89 11:40:11 BST
From: Tom Melham <tfm%uk.ac.cam.cl@uk.ac.nsf>
To: info-hol <info-hol%edu.ucdavis.clover@uk.ac.nsf>
Message-Id:  <8905151141.aa28526@scaup.Cl.Cam.AC.UK>
Sender: tfm <tfm%uk.ac.cam.cl%uk.ac.nsf@edu.ucdavis.clover>
Status: R


Concerning  David Shepherd's remarks about the define_type package:

>Perhaps part of the lesson of this is that after struggling with
>"new_type_defintion" type definitions we saw "define_type" as a
>universal panacea to all our type definition problems....

The present implementation of define_type is, of course, not the universal
panacea to all type definition problems.  All it can do for you is to
construct the formal definition for any CONCRETE recursive type. This is still
a great improvement over defining these types "by hand" (if you don't believe
me, try one or two manual definitions), but it doesn't help very much with
defining ABSTRACT types (i.e. types whose values also satisfy some given set
of properties).   As David pointed out, equality on concrete types is
determined syntactically (that's why they're concrete), so you can't just add
extra axioms to force certain terms to be equal.

I'm presently working on a new package for defining certain abstract types
auomatically (finite sets are a typical example).  The details are more or
less worked out---I just have to code it efficiently in HOL.  With this new
package, Phil's type of finite sets will be described by user input that will
look something like:

     `set = EMPTY | INSERT x set
          where INSERT x (INSERT x s) = INSERT x s
          and   INSERT x (INSERT y s) = INSERT y (INSERT x s)`

The result will be a theorem characterizing this type.  I hope to get a
prototype implementation done as soon as possible, which I'd like to release
to interested parties for comments---before it's included on the distribution
tape.

Tom