<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;">I have just started work on upgrading my OpenTheory implementation to work<div>with recent versions of ProofPower, in which new_definition has been replaced</div><div>by the new definitional principle gen_new_specification (as per my</div><div>"HOL Constant Definitions Done Right”). I think there is a problem with the</div><div>way the new principle is represented in the current draft version 6 of the</div><div>OpenTheory article format.<div><br></div><div>The new principle (called defineConstList in OpenTheory) takes an input theorem of the form:</div><div><br></div><div> v_1 = t_1, …, v_k = t_k |- phi</div><div><br></div><div>and introduces new constants c_1, …, c_l with defining property:</div><div><br></div><div> |= phi[c_1/v_1, …, c_k/v_k]</div><div><br></div><div>To implement this in practice you need a way of specifying the names of the new constants. </div><div>The proposed defineConstList has as input to be the theorem as above together</div><div>with a list of pairs (n_1, t_1), …, (n_k, t_k) where n_i gives the name of the new constant c_i.</div><div>Unfortunately, this parametrisation does not allow you to pair up the n_i with the v_i in general,</div><div>because the same witness might be used for two or more constants, as in:</div><div><br></div><div> a = 0, b = 0, c = 0 |- a < 10 /\ b < 20 /\ c < 30</div><div><br></div><div>I think the t_i in the list of pairs should read v_i.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></div></body></html>