Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9205071452.AA28057@easynet.crl.dec.com>
Date: Thu, 7 May 92 10:52:48 EDT
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 07-May-1992 1037" <leonard@com.dec.enet.ricks>
To: info-hol@edu.uidaho.cs.ted
Apparently-To: info-hol@ted.cs.uidaho.edu
Subject: re: discarding theory segments

Mark van de Voort asks if there's some way to discard theory segments.  As I
remember, the difficulty is that the ML environment may include theorems (that
is, ML objects of type :thm) that depend on the current theory segment.  In
order to preserve validity, the current theory must be preserved, or those
theorems must be discarded with it.  Unfortunately, there's no direct way of
finding such objects, or ridding the ML environment of them.

I think there's a fairly simple solution, but I haven't thought about theories
enough to know if it actually works.  The idea is that the current theory in
ML memory has a version number, and the ML abstract objects called theorems also
include version numbers.  The operation to discard a theory segment ("forget",
or "revoke", or "rescind", or something) must not only remove the specified
segments from the current theory, but must also increment the current theory's
version number.  All primitive operations on theorems (inference rules, pretty
printing, and theorem-saving, for example) must check that the theorems they
are applied to have the current version number. 

Tim