<br><br><div class="gmail_quote">On Thu, Jan 19, 2012 at 11:11 AM, Joe Hurd <span dir="ltr">&lt;<a href="mailto:joe@gilith.com">joe@gilith.com</a>&gt;</span> wrote:<br><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<br>
when they&#39;re applied to arguments, so even if you remove them from<br>
assumptions and theorems they might still be present inside proofs.<br>
<br>
Really the trick is to get rid of Unwanted constants from assumptions<br>
and theorems (since constants that are only present inside proofs are<br>
trapped and can never escape to their environment). So Michael&#39;s<br>
solution of replacing the point-free version of theorems containing<br>
Unwanted constants with point-full versions should work just fine,<br>
though on an ad-hoc basis.<br></blockquote><div><br>I don&#39;t think that&#39;s what he suggested. Rather it was to provide a proof of the point-free version. I&#39;m about to try saving such a proof in a separate package and then listing that package as a &quot;requires:&quot; to see what happens...<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>
Cheers,<br>
<br>
Joe<br>
<div class="HOEnZb"><div class="h5"><br>
On Thu, Jan 19, 2012 at 12:19 AM, Ramana Kumar &lt;<a href="mailto:ramana.kumar@gmail.com">ramana.kumar@gmail.com</a>&gt; wrote:<br>
&gt; Thinking about this more, I&#39;m not sure it will work completely because the<br>
&gt; statement of the theorem will still include Unwanted.id... So the article<br>
&gt; might end up still defining Unwanted.id but hopefully not assuming any<br>
&gt; axioms. In any case, I&#39;m going to try it out and see what happens.<br>
&gt;<br>
&gt; On Thu, Jan 19, 2012 at 5:24 AM, Michael Norrish<br>
&gt; &lt;<a href="mailto:Michael.Norrish@nicta.com.au">Michael.Norrish@nicta.com.au</a>&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt; On 19/01/12 10:04, Ramana Kumar wrote:<br>
&gt;&gt;<br>
&gt;&gt; &gt; Yes. (Except for two minor details: there will be no occurrences of<br>
&gt;&gt; &gt; Unwanted afterwards, even internally, and it is the proofs that are<br>
&gt;&gt; &gt; rewritten (rather than just theorem/import/axiom statements).)<br>
&gt;&gt;<br>
&gt;&gt; Ah, that&#39;s interesting.<br>
&gt;&gt;<br>
&gt;&gt; &gt;&gt; Would it be possible to augment the HOL4 exporter so that it<br>
&gt;&gt; &gt;&gt; automatically included the (fairly trivial) proof discharging the<br>
&gt;&gt; &gt;&gt; point-free theorem that gets listed as an import?  It seems to me<br>
&gt;&gt; &gt;&gt; that this is the best solution, though it&#39;s clearly very ad hoc.<br>
&gt;&gt;<br>
&gt;&gt; &gt; Yes that seems like a good solution to me, but I think it means<br>
&gt;&gt; &gt; looking for this theorem specifically as a special case in the<br>
&gt;&gt; &gt; exporter, right? Actually it could be as general as: if a theorem,<br>
&gt;&gt; &gt; after translating constants to OT namespace, contains any<br>
&gt;&gt; &gt; not-fully-applied Unwanted.ids, then lookup a proof for the theorem<br>
&gt;&gt; &gt; in a special database, otherwise proceed as normal. (As normal would<br>
&gt;&gt; &gt; be logging the proof if it&#39;s attached to the theorem, otherwise<br>
&gt;&gt; &gt; treat it as an axiom. The problem above is that the theorem doesn&#39;t<br>
&gt;&gt; &gt; have a proof attached when logging llist, since it was proved in an<br>
&gt;&gt; &gt; earlier theory (i.e. it&#39;s a DISK_THM)).<br>
&gt;&gt;<br>
&gt;&gt; Yeah, the special database will presumably have to be populated with real<br>
&gt;&gt; proofs well in advance.<br>
&gt;&gt;<br>
&gt;&gt; There probably isn&#39;t any real harm in trying to be general.  On the other<br>
&gt;&gt; hand, I don&#39;t suppose there will be a great many such theorems.<br>
&gt;&gt;<br>
&gt;&gt; Michael<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; _______________________________________________<br>
&gt;&gt; opentheory-users mailing list<br>
&gt;&gt; <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
&gt;&gt; <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a><br>
&gt;&gt;<br>
&gt;<br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; opentheory-users mailing list<br>
&gt; <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
&gt; <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a><br>
&gt;<br>
<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>
</div></div></blockquote></div><br>