Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <m0puMkP-000018C@tiree.research.att.com>
Date: Fri, 22 Apr 94 11:02 EDT
From: elsa@research.att.com (Elsa Gunter)
To: info-hol@cs.uidaho.edu
Subject: revised mutrec library, new nested_rec library

Dear HOL90 community:
  I have recently made some changes/extensions to the contributed
library "mutrec", which I hope will make it easier to use.  This is
still just a temporary version, which I continue to intend to replace.
In addition to revising the "mutrec" library, I have added a new
contributed library that is capable of handling the nesting of
datatypes being defined within (arbitrarily many) simple-recursive
datatype constructors (such as lists and pairs).  These contibuted
libraries can be had via anonymous ftp from

	 research.att.com:dist/ml/hol90/contrib/mutrec.tar.Z
	 research.att.com:dist/ml/hol90/contrib/nested_rec.tar.Z

Below I include the to Read_me files giving brief descriptions of the
two libraries.
				---Elsa L. Gunter
				elsa@research.att.com

(* File: mutrec/Read_me *)
Mutrec.

The contributed library "mutrec" supplies preliminary support for
making polymorphic mutually recursive datatype definitions and
mutually primitive recursive function definitions over such types.
There is a functor named MutRecTypeFunc which you apply to a
specification and it causes the six new theorems (existence,
uniqueness, induction, cases, and the one-to-oneness and distinctness
of constructors) to be bound to identifiers in the top-level
environment, and stored in the current theory under the same
names. The names of these theorems are user supplied in the input
structure, along with the specification.  The functor also defines
terms for extracting the arguments of functional constructors, and
binds these definitions, both in the theory and in the top-level
environment, to internally generated names.
  There is also a function define_mutual_functions for defining
mutually recursive functions over the datatypes.  This is a slightly
altered version from the older versions.  The new version of
define_mutual_functions has the type

val define_mutual_functions : {name:string,
                               fixities:fixity list option,
                               rec_axiom:thm,
                               def:term} -> thm

Notice that the fixities of the constructors is given by an optional
list of fixity specifications.  If you wish to only have constructors
with no special fixity status, then you may give NONE as the value for
fixities.  Otherwise, you must use a value such as
SOME[Prefix,Infix 600,...] to specify each speficic fixity status of
each constructor.  Using the value NONE is the same as using the value
SOME[Prefix,...Prefix].
  For those who used older versions, the functor MutRecDefFunc is also
supplied by this library and should be compatible with any working
examples you have.  (It has been fixed to work properly with
polymorphism.)

  There is no other documentation, other than some examples given in
the directory "example".

Send queries on this package to

			elsa@research.att.com


(* File: nested_rec/Read_me *)

Nested_rec.

The contributed library "nested_rec" supplies preliminary support for
making polymorphic mutually recursive datatype definitions which can
contain occurrences of the types being defined within previously
defined polymorphic simple recursive types, such as lists, pairs, etc.
It also provides support for mutually primitive recursive function
definitions over such types. In fact, it's behaviour is almost
identical to that of the library "mutrec".  There is a functor named
NestedRecTypeFunc which you apply to a specification and it causes the
six new theorems (existence, uniqueness, induction, cases, and the
one-to-oneness and distinctness of constructors) to be bound to
identifiers in the top-level environment, and stored in the current
theory under the same names. The names of these theorems are
user-supplied in the input structure, along with the specification.
The functor also defines terms for extracting the arguments of
functional constructors, and binds these definitions, both in the
theory and in the top-level environment, to internally generated
names.
  There is also a function define_mutual_functions (the same as
for "mutrec") for  defining mutually recursive functions over the
datatypes.  It has the type

val define_mutual_functions : {name:string,
                               fixities:fixity list option,
                               rec_axiom:thm,
                               def:term} -> thm

Notice that the fixities of the constructors is given by an optional
list of fixity specifications.  If you wish to only have constructors
with no special fixity status, then you may give NONE as the value for
fixities.  Otherwise, you must use a value such as
SOME[Prefix,Infix 600,...] to specify each speficic fixity status of
each constructor.  Using the value NONE is the same as using the value
SOME[Prefix,...Prefix].
  There is no other documentation, other than some examples given in
the directory "example".

Send queries on this package to

			elsa@research.att.com