Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
From: Rob Arthan <rda@win.icl.co.uk>
Date: Tue, 29 Aug 95 11:32:20 BST
Message-Id: <9508291032.19418.0@win.icl.co.uk>
To: Donald.Syme@cl.cam.ac.uk
Subject: Re: More on theory signatures & remaking definitions in HOL
Cc: hol2000@leopard.cs.byu.edu

Donald Syme writes: 
> 
> A while ago I suggested incorporating theory signature
> information into terms and types in order to 
> allow conflicting definitions to be
> introduced into the system while preserving system integrity.
> 
> Konrad mentioned the idea of allowing the redefiniton of a constant
> by tagging the defining theorem for the constant with a reference,
> and propogating this tag through every theorem which uses the
> definition.  However, as he later pointed out to me, this doesn't
> work, and I thought it might me worth mentioning this on hol2000
> "for the record".  The problem is that many theorems
> about a constant do not utilise the defining theorem in 
> their derivation.  For instance, you can create a theorem 
> using a constant simply usng REFL or SPEC.  Given that functions
> like REFL and SPEC are essential to HOL, then 
> the only way to stop bogus theorems is if bogus
> terms never come into existence.

The following remarks about what we do in ProofPower, which at least
allows the user to navigate freely around the theory hierarchy, may be
relevant here. I'm not actually sure what kind of feature you're
looking for to introduce conflicting definitions, but if you're happy
for the conflicting definitions to be protected from each other using
the theory hierarchy, then ProofPower will certainly let you do that.

The first remark is that you have to be precise as to what claims
you are making about the validity of values of type THM if you allow
the user to make arbitrary scope changes.

In ProofPower, each theorem is tagged with a unique identifier for the
theory which was current when it was proved. This is weaker than
the scheme that Konrad has in mind, but does everything we've felt a
strong need for in this area.

We do not claim that any value of type THM will be valid in every
scope. Indeed, if you prove a theorem in one theory and then switch to
an unrelated theory, you do invalidate the theorem in a certain sense.
The claim that we do make is that when a theorem is saved in a theory,
then that theorem will be a valid consequence of the axioms ond
definitions of the theory (and its ancestors, of course).

The checks we impose on theorems are (a) is the theory in which it was
proved in scope? and (b) are all the types and constants in it in
scope?  Check (a) is made on every inference; check (b), which detects
the problems mentioned with rules like REFL and SPEC, is only made when
a theorem is saved on a theory or when the user explicitly calls a
function to validate the theorem. The reason for not doing check (b)
very often is that it is time-consuming. The logical justification is
that introducing a new type or constant with no defining theorem is a
conservative extension; consequently, providing the theorem resulting
from some derivation does not contain any undefined constants or types,
the theorem is valid even if such constants or types have been used in
the derivation.

There doesn't seem to be any great practical disadvantage in
the ProofPower approach. In particular, the pretty-printer generally
makes it obvious when a term contains a constant which is out of
scope (by printing the constant as the antiquotation you would need
to use to reparse the term).

An idea which we didn't implement in ProofPower, but which may have
some mileage, extends this observation about conservativeness a little.
If you prove a theorem in a theory which only makes conservative
extensions (i.e., it was made without using no new_axiom), then
it's logically acceptable to save the theorem in a parent of
the theory, providing the theorem doesn't involve types and constants
which aren't in scope in the parent. This means that, if you
need to make some ad hoc definitions to make a proof easier, you don't
have to force these definitions onto the users of your theorems.
Instead you can use a child theory to hold these  definitions.
I can envisage user interface features which might make this
a fairly palatable way of handling local definitions.

Rob Arthan (rda@win.icl.co.uk)