<div class="gmail_quote">On Wed, Jan 18, 2012 at 10:22 PM, Michael Norrish <span dir="ltr"><<a href="mailto:Michael.Norrish@nicta.com.au">Michael.Norrish@nicta.com.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> <div class="im">On 15/01/12 07:48, Ramana Kumar wrote:<br> <br> > Unfortunately, that still doesn't solve the problem when a tag shows up not fully applied (like in a point-free term).<br> <br> </div>So, my understanding is that this is an issue in the following scenario:<br> <br> * the llist proof uses a point-free theorem about the 'Abbrev' constant.<br> * this theorem gets listed as an import dependency<br> * this interferes with the general desire to get rid of the constant (which is really an unwanted identity function)<br></blockquote><div><br>Correct. It gets listed as an import dependency implicitly (they are all implicit) because it gets used during a proof (and isn't proved itself).<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <br> Parenthetically, I understand the treatment of unwanted constants such as 'Abbrev' is supposed to be:<br> <br> * replace all occurrences with the Unwanted.id constant<br> * process exported theorems with the |- id x = x theorem so that occurrences in what is exported disappear<br> * similarly, process the import/axiom list so that occurrences there go away<br> * the result is an article that all systems will be happy to use, though there may still be occurrences of Unwanted internally.<br></blockquote><div></div><div><br>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).)<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> Is this right?<br> <br> 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.<br> </blockquote><div><br>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)).<br> </div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> <span class="HOEnZb"><font color="#888888"><br> Michael<br> <br> <br> <br> </font></span><br>_______________________________________________<br> opentheory-users mailing list<br> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a><br> <br></blockquote></div><br>