[opentheory-users] defineConstList

[Rob Arthan]

Joe,

On 9 Aug 2014, at 23:28, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Rob,
> 
> Nice catch, I've updated the article standard:
> 
> http://www.gilith.com/research/opentheory/article.html#defineConstListCommand
> 

Thanks! Your update is exactly what my implementation anticipated. I think I am now
ready to go public with my (very experimental and tentative) reader and writer. The
implementation can be found at:

https://github.com/RobArthan/pp-contrib/tree/master/src/open_theory

I have included a PDF of the documentation, so you don’t need to know about
ProofPower documents to read about it.

> 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.
> 
Excellent news!

Regards,

Rob.

> 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
>> 
> 
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140810/1544f90a/attachment.html>