[opentheory-users] Type variables

[Rob Arthan]

Joe,

On reflection, I think it would be far too complicated to have axiom or thm do type instantiation.  At the moment, what I am doing is reading the base package translating its definitions into the the ProofPower definitions (or theorems derived from them) and I can easily instantiate the definitions to give exactly what is asked for as I process them. Mapping HOL Light type variable names into ProofPower ones sounds like a good idea too.

Regards,

Rob.

On 2 Dec 2013, at 06:01, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Rob,
> 
> It might perhaps be a nice feature if the "axiom" command didn't just match alpha-equivalent theorems, but was able to rename/instantiate type and free term variables too. However, that seems like a lot to ask of an article reader, and in any case it wouldn't solve the problem of processing type variables when reading articles exported from another theorem prover with different conventions.
> 
> There was some discussion on the list a while back about standardizing names for type variables:
> 
> http://www.gilith.com/opentheory/mailing-list/2011-September/000114.html
> 
> The best solution seems to be for the OpenTheory standard theory library to adopt one convention (currently capital letters, like HOL Light), and for other theorem provers to convert them to their local convention as part of reading/writing articles (e.g., HOL4 would map A to 'a, B to 'b, etc.)
> 
> I have added a note about this to the documentation for the varType command in the article format:
> 
> http://www.gilith.com/research/opentheory/article.html#varTypeCommand
> 
> Cheers,
> 
> Joe
> 
> 
> 
> On Fri, Nov 29, 2013 at 3:23 PM, Rob Arthan <rda at lemma-one.com> wrote:
> The OpenTheory "thm" command  allows for an alpha-conversion to get the variable names in a theorem exactly right. The description doesn't say anything about type instantiation, so presumably type variable names have to be right already. Perhaps it should allow type variable renaming too, because the choice of type variable names in definitions of existing constants (like the quantifiers) is going to be implementation-dependent. Unfortunately, this is a little tricky to specify and implement because "thm" also allows the inferred theorem to have fewer assumptions than the target theorem. 
> 
> On this topic, the Gilith OpenTheory Repo seems to use HOL Light type variable names (A, B, C etc.) that can't be parsed in HOL4 or ProofPower. In any case, if "thm" doesn't allow for type variable renaming, then the documentation needs to say what type variables have been used.
> 
> 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