[opentheory-users] defineConstList

[Rob Arthan]

I have just started work on upgrading my OpenTheory implementation to work
with recent versions of ProofPower, in which new_definition has been replaced
by the new definitional principle gen_new_specification (as per my
"HOL Constant Definitions Done Right”). I think there is a problem with the
way the new principle is represented in the current draft version 6 of the
OpenTheory article format.

The new principle (called defineConstList in OpenTheory) takes an input theorem of the form:

   v_1 = t_1, …, v_k = t_k |- phi

and introduces new constants c_1, …, c_l with defining property:

   |= phi[c_1/v_1, …, c_k/v_k]

To implement this in practice you need a way of specifying the names of the new constants. 
The proposed defineConstList has as input to be the theorem as above together
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.
Unfortunately, this parametrisation does not allow you to pair up the n_i with the v_i in general,
because the same witness might be used for two or more constants, as in:

   a = 0, b = 0, c = 0 |- a < 10 /\ b < 20 /\ c < 30

I think the t_i in the list of pairs should read v_i.

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140809/ed4aa833/attachment.html>