[opentheory-users] defineConstList

[Joe Leslie-Hurd]

Hi Rob,

Nice catch, I've updated the article standard:

http://www.gilith.com/research/opentheory/article.html#defineConstListCommand

I'm back working on OpenTheory now after a break working on another
side-project, so hopefully the opentheory tool will soon be able to
process the new commands.

Cheers,

Joe

On Sat, Aug 9, 2014 at 6:35 AM, Rob Arthan <rda at lemma-one.com> wrote:
> 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.
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>