[opentheory-users] the Unwanted namespace

[Joe Hurd]

The current procedure for eliminating Unwanted.id constants only works
when they're applied to arguments, so even if you remove them from
assumptions and theorems they might still be present inside proofs.

Really the trick is to get rid of Unwanted constants from assumptions
and theorems (since constants that are only present inside proofs are
trapped and can never escape to their environment). So Michael's
solution of replacing the point-free version of theorems containing
Unwanted constants with point-full versions should work just fine,
though on an ad-hoc basis.

Cheers,

Joe

On Thu, Jan 19, 2012 at 12:19 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>