[opentheory-users] the Unwanted namespace

[Ramana Kumar]

On Wed, Jan 18, 2012 at 10:22 PM, Michael Norrish <
Michael.Norrish at nicta.com.au> wrote:

> 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)
>

Correct. It gets listed as an import dependency implicitly (they are all
implicit) because it gets used during a proof (and isn't proved itself).


>
> 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.
>

Yes. (Except for two minor details: there will be no occurrences of
Unwanted afterwards, even internally, and it is the proofs that are
rewritten (rather than just theorem/import/axiom statements).)


> 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.
>

Yes that seems like a good solution to me, but I think it means looking for
this theorem specifically as a special case in the exporter, right?
Actually it could be as general as: if a theorem, after translating
constants to OT namespace, contains any not-fully-applied Unwanted.ids,
then lookup a proof for the theorem in a special database, otherwise
proceed as normal. (As normal would be logging the proof if it's attached
to the theorem, otherwise treat it as an axiom. The problem above is that
the theorem doesn't have a proof attached when logging llist, since it was
proved in an earlier theory (i.e. it's a DISK_THM)).


>
> Michael
>
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120118/14f3e149/attachment.htm>