[opentheory-users] the Unwanted namespace

[Ramana Kumar]

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/0b10c4bb/attachment.htm>