[opentheory-users] the Unwanted namespace

[Ramana Kumar]

Thinking about this more, I'm not sure it will work completely because the
statement of the theorem will still include Unwanted.id... So the article
might end up still defining Unwanted.id but hopefully not assuming any
axioms. In any case, I'm going to try it out and see what happens.

On Thu, Jan 19, 2012 at 5:24 AM, Michael Norrish <
Michael.Norrish at nicta.com.au> wrote:

> 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
>
>
> _______________________________________________
> 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/20120119/a06a4940/attachment-0001.htm>