Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Message-Id: <199305191536.AA05573@panther.cs.uidaho.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: HOL90 style question
In-Reply-To: Your message of Wed, 19 May 93 11:08:56 -0400. <9305191508.AA07266@sparta.oracorp.com>
Date: Wed, 19 May 93 08:36:02 -0700
From: Phil Windley <windley@panther.cs.uidaho.edu>


On Wed, 19 May 93 11:08:56 EDT, shb@oracorp.com wrote:
+------------
| Still, I know that using axioms is generally considered bad form, and
| had previously made a conscientious effort to avoid them.  Is there
| another technique for straightforwardly noting assumptions about
| undefined functions without using axioms?  If not, and if new_axiom
| really is the best tool for the job I used it for, shouldn't HOL90 have
| its own version of new_axiom, without requiring reference to HOL88?

Two possibilities (which is correct depends on your situation):

1.) use new_specification (this is HOL88, I guess its in HOL90 as well).
new_specification let's you define a constant with particular properties if
you can show that such a constant exists.

2.) use abstract theories (David Sheppard has a port for HOL90).  Abstract
theories allow you to axiomatize a theory over a set of properties on a set
of constants.  Later, the theory can be used by producing a structure
has the required properties.

--phil--