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. <a href="http://opentheory.gilith.com/opentheory/packages/lazy-list-0.3/lazy-list-0.3.html">http://opentheory.gilith.com/opentheory/packages/lazy-list-0.3/lazy-list-0.3.html</a> <div class="gmail_quote">On Thu, Jan 19, 2012 at 11:38 AM, Ramana Kumar <<a href="mailto:ramana.kumar@gmail.com">ramana.kumar@gmail.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div class="gmail_quote"><div class="im">On Thu, Jan 19, 2012 at 11:11 AM, Joe Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> 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. </blockquote></div><div> 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... </div><div><div class="h5"><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> Cheers, Joe <div><div> On Thu, Jan 19, 2012 at 12:19 AM, Ramana Kumar <<a href="mailto:ramana.kumar@gmail.com" target="_blank">ramana.kumar@gmail.com</a>> 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 > <<a href="mailto:Michael.Norrish@nicta.com.au" target="_blank">Michael.Norrish@nicta.com.au</a>> 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 >> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> >> > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> > _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> </div></div></blockquote></div></div></div> </blockquote></div>