Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Sun, 26 Apr 92 12:32:24 EDT
From: hoove@com.oracorp
Message-Id: <9204261632.AA04443@euterpe.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Abstract theories, subtypes, and restricted quantification

I am interested in developing abstract theories of groups, rings,
fields, and ordered groups, rings and fields, and other objects in
HOL.  I would like to say that 

	<F,+,*,0,1> 

is a field if <F,+,0> and <F-{0},*,1> are abelian groups and *
distributes over +.  Now, it would be cleaner to develop a
theory of groups in which the group is an entire type, rather than a
subset of the type, as is done in Elsa Gunter's development in the
*group* library.  To apply the theory of groups in this form to
<F-{0},*,1> would require coordinating restricted quantification on F
with statements about the subtype generated by F-{0}.  Has anyone
tried this? has anyone an opinion about whether using subtypes is more
or less cumbersome than developing theories of algebraic structures on
a subtype of a type?  

Note that this method of building abstract theories out of big pieces
has wide application.  For instance an <F,+,*,0,1,<= > is an ordered
field if <F,+,*,0,1> is a field and <F,+,0,<= > and 
<{x:F | 0 < x},*,1,<= > are ordered abelian groups.  


Doug Hoover
hoove@oracorp.com