[opentheory-users] the Unwanted namespace

[Ramana Kumar]

To my mild surprise, logging the proof of the point-free theorem worked.
That is, if I make sure the theorem with an unapplied Unwanted.id is logged
with a proof (while logging the lazy list theory), then process the
resulting article with opentheory, the resulting package doesn't define
Unwanted.id and doesn't require any axioms.
I've uploaded the new version of the lazy list package, which now appears
to define and prove just the right things.
http://opentheory.gilith.com/opentheory/packages/lazy-list-0.3/lazy-list-0.3.html

On Thu, Jan 19, 2012 at 11:38 AM, Ramana Kumar <ramana.kumar at gmail.com>wrote:

>
>
> On Thu, Jan 19, 2012 at 11:11 AM, Joe Hurd <joe at gilith.com> wrote:
>
>> 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.
>>
>
> I don't think that's what he suggested. Rather it was to provide a proof
> of the point-free version. I'm about to try saving such a proof in a
> separate package and then listing that package as a "requires:" to see what
> happens...
>
>
>>
>> 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
>> >
>>
>> _______________________________________________
>> 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/f29fccba/attachment.htm>