[opentheory-users] the Unwanted namespace

[Michael Norrish]

On 15/01/12 07:48, Ramana Kumar wrote:

> Unfortunately, that still doesn't solve the problem when a tag shows up not fully applied (like in a point-free term).

So, my understanding is that this is an issue in the following scenario:

* the llist proof uses a point-free theorem about the 'Abbrev' constant.
* this theorem gets listed as an import dependency
* this interferes with the general desire to get rid of the constant (which is really an unwanted identity function)

Parenthetically, I understand the treatment of unwanted constants such as 'Abbrev' is supposed to be:

* replace all occurrences with the Unwanted.id constant
* process exported theorems with the |- id x = x theorem so that occurrences in what is exported disappear
* similarly, process the import/axiom list so that occurrences there go away
* the result is an article that all systems will be happy to use, though there may still be occurrences of Unwanted internally.

Is this right?

Would it be possible to augment the HOL4 exporter so that it automatically included the (fairly trivial) proof discharging the point-free theorem that gets listed as an import?  It seems to me that this is the best solution, though it's clearly very ad hoc.

Michael



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 554 bytes
Desc: OpenPGP digital signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120119/23e0c3ae/attachment.pgp>