<div dir="ltr">Hi Ramana,<div><br></div><div>I'd never read that note by Rob, and it's very clear and persuasive. Although I have a natural resistance to changing the article file format in any way, the proposed primitive constant definition mechanism does seem to offer an improvement in expressivity at a modest cost of being more complicated to explain.</div>
<div><br></div><div>I would consider changing the OpenTheory logical kernel to support it, particularly if HOL4 or ProofPower incorporated it as the primitive constant definition mechanism, but I'd be interested to hear what John has to say about it.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 25, 2014 at 1:38 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello OpenTheory!<br>
<br>
There has been some activity recently considering Rob Arthan's<br>
proposal for HOL Constant Definition Done Right [1]. For those<br>
unfamiliar, that proposal includes a rule for introducing new<br>
constants by conservative extension with a (potentially loose)<br>
specification, and it subsumes the functionality of the new_definition<br>
and new_specification rules currently implemented in the various HOL<br>
provers.<br>
<br>
The rule has a host of benefits detailed in the paper. My aim here is<br>
to encourage OpenTheory and HOL Light to adopt it as well - or at<br>
least to invite discussion on that possibility.<br>
<br>
As I understand it, work is being done to implement this new rule in<br>
HOL4 and ProofPower, as a replacement for the primitive rule for<br>
defining a new constant by an equation. Of course, as it stands, this<br>
breaks compatibility with OpenTheory, since the new rule cannot be<br>
reduced to the definitional mechanisms provided in OpenTheory.<br>
<br>
It would be wonderful to maintain the possibility of proof export,<br>
hence my invitation to consider the new rule for OpenTheory.<br>
<br>
Cheers,<br>
Ramana<br>
<br>
[1] <a href="http://www.lemma-one.com/papers/hcddr.pdf" target="_blank">http://www.lemma-one.com/papers/hcddr.pdf</a><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/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>