[opentheory-users] the Unwanted namespace

[Michael Norrish]

On 19/01/12 10:04, Ramana Kumar wrote:

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

Ah, that's interesting.

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

Yeah, the special database will presumably have to be populated with real proofs well in advance.

There probably isn't any real harm in trying to be general.  On the other hand, I don't suppose there will be a great many such theorems.

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/15550ecc/attachment.pgp>