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. <div class="gmail_quote">On Thu, Jan 19, 2012 at 5:24 AM, Michael Norrish <<a href="mailto:Michael.Norrish@nicta.com.au">Michael.Norrish@nicta.com.au</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div class="im">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).) </div>Ah, that's interesting. <div class="im"> >> 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)). </div>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">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> </blockquote></div>