Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <19533.9304211148@frogland.inmos.co.uk>
Subject: Suggested additions to definition functions
To: info-hol@ted.cs.uidaho.edu (info-hol mailing list)
Date: Wed, 21 Apr 1993 12:48:53 +0100 (BST)
Content-Type: text
Content-Length: 3971

Over the last couple days I have taken Phil Windley's datatype
package and converted it into hol90. It seems to be quite useful
apart from one problem - the underlying define_type mechanism
leaves a large number of definitions in the theory file that
never get used. 

From the users point of view the only useful output from define_type is
the recursive type axiom, however, in producing this HOL has to produce
the type definition for the type and definitions of all the constructors
and these get stuck in the theory file. For small types this perhaps
isn't an issue, but I defined an enumerated type of 16 elements and
by the time you get to the last constructor there are 15 INL's in
the definition.

My suggestion is that there are some addition definition functions that
will make the definition (i.e. declare the relevant constant(s)), return
the theorem but not store it in the theory file. The functions required
are

	make_new_type_definition
	make_type_bijections
	make_new_specification
	make_new_definition
	make_new_infix_definition
	make_new_binder_definition

and in addition probably a make_definition which does the same
checking as store_definition to ensure we're creating kosher definitions
Then define_type is modified to use these function instead of the original
ones that store the definitions.

I did the relevant mods in my hol90 sources here and rebuilt the
system. Now the datatype functions work as before except that the
theory gets none of the extra definitions added. (N.b. for hol88 users
remember that also each time a definition is stored into the theory
that the theory file is written and this time can add up especially if
you had 16 constructor definitions to emit)

This situtation is in fact an example of a more general issue which is
the orthogonality between defining something and storing its
definition. As I have described at present everytime you make a
definition then that definition is recorded in the theory file but as I
have also shown this is not always desirable. Clearly the constant 
declaration needs to be recorded but the actual defining theorem does
not.

This leads to a more radical suggestion in which the these two concepts
are more directly separated. Already with hol90 a theory is represented
by a .hol_sig file which contains the constants and types that it
declares and its ancestry and a .hol_thms file which contains all its
theorems, definitions and axioms. However, at present, these are linked
together (i.e. you always have thry.hol_sig and thry.hol_thms).
Perhaps, these should be seperated further - the .hol_sig would be used
as at present to define the constants and ancestry of a theory, but
also you could have a number of theorem-store files into which you can
save theorems. These theorem-store files would still record what theory
they are relative to (i.e. the current theory when they are opened) and
theorems from them could be used whenever that theory is in the current
ancestry. The benefit of this is that you can structure the theorems in
a theory more - e.g. one file for all the important definitions and
theorems and another for extra lemmas developed along the way that  may
be useful later, and also a library can store a set of theorems it
needs to preprove without the need to add a theory into the theory path
(e.g. the pair library could store all the theorems it proves and uses
in a theorem store relative to the HOL theory which then could be
opened when the package is loaded without the need to and a pair_lib
theory to the ancestry as would be required at present).

What does anyone think about these ideas?

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley