<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Joe,<div><br><div><div>On 9 Aug 2014, at 23:28, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi Rob,<br><br>Nice catch, I've updated the article standard:<br><br><a href="http://www.gilith.com/research/opentheory/article.html#defineConstListCommand">http://www.gilith.com/research/opentheory/article.html#defineConstListCommand</a><br><br></blockquote><div><br></div>Thanks! Your update is exactly what my implementation anticipated. I think I am now</div><div>ready to go public with my (very experimental and tentative) reader and writer. The</div><div>implementation can be found at:</div><div><br></div><div><a href="https://github.com/RobArthan/pp-contrib/tree/master/src/open_theory">https://github.com/RobArthan/pp-contrib/tree/master/src/open_theory</a></div><div><br></div><div>I have included a PDF of the documentation, so you don’t need to know about</div><div>ProofPower documents to read about it.</div><div><br><blockquote type="cite">I'm back working on OpenTheory now after a break working on another<br>side-project, so hopefully the opentheory tool will soon be able to<br>process the new commands.<br><br></blockquote>Excellent news!</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br><blockquote type="cite">Cheers,<br><br>Joe<br><br>On Sat, Aug 9, 2014 at 6:35 AM, Rob Arthan <<a href="mailto:rda@lemma-one.com">rda@lemma-one.com</a>> wrote:<br><blockquote type="cite">I have just started work on upgrading my OpenTheory implementation to work<br>with recent versions of ProofPower, in which new_definition has been<br>replaced<br>by the new definitional principle gen_new_specification (as per my<br>"HOL Constant Definitions Done Right"). I think there is a problem with the<br>way the new principle is represented in the current draft version 6 of the<br>OpenTheory article format.<br><br>The new principle (called defineConstList in OpenTheory) takes an input<br>theorem of the form:<br><br> v_1 = t_1, ..., v_k = t_k |- phi<br><br>and introduces new constants c_1, ..., c_l with defining property:<br><br> |= phi[c_1/v_1, ..., c_k/v_k]<br><br>To implement this in practice you need a way of specifying the names of the<br>new constants.<br>The proposed defineConstList has as input to be the theorem as above<br>together<br>with a list of pairs (n_1, t_1), ..., (n_k, t_k) where n_i gives the name of<br>the new constant c_i.<br>Unfortunately, this parametrisation does not allow you to pair up the n_i<br>with the v_i in general,<br>because the same witness might be used for two or more constants, as in:<br><br> a = 0, b = 0, c = 0 |- a < 10 /\ b < 20 /\ c < 30<br><br>I think the t_i in the list of pairs should read v_i.<br><br>Regards,<br><br>Rob.<br><br>_______________________________________________<br>opentheory-users mailing list<br><a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>http://www.gilith.com/opentheory/mailing-list<br><br></blockquote><br>_______________________________________________<br>opentheory-users mailing list<br><a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>http://www.gilith.com/opentheory/mailing-list<br></blockquote></div><br></div></body></html>