[opentheory-users] Importing from the Gilith OpenTheory Repo

[Rob Arthan]

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

> Hi Rob,
> 
> My plan was to import the base package but using the ProofPower definitions (or theorems derived from them) rather than making new definitions so that I would end up importing all the theorems about the ProofPower constants and types that I need to support the dependencies of other packages. Isn't that what you are expected to do?
> 
> That's exactly right. In fact the construction of the base theory package is designed to help with this, in the naming of the packages that make it up. Definition theorems are stored in packages named *-def (the theorems in these packages must be derived from ProofPower theorems), and the theorems in other packages are merely consequences of these definition theorems (and can either be mapped to named ProofPower theorems or simply added to the theorem database as unnamed theorems).

What I was rather hoping was that I could substitute for the definitions and axioms and then import the proofs of the theorems. If I import say pair-thm, I find it involves a lot more assumptions other than definitions.  I would have hoped that the assumptions in pair-thm would just be:

!xy?x y. xy = (x, y)

!x y. fst(x, y) = x

!x y. snd(x, y) = y


> On this topic, I note that there are a number of names in the base package in the HOLLight namespace. E.g., "HOLLight.mk_pair. Is that intentional?
> 
> That is definitely not intentional, and I even have a script that ensures that no symbols in the HOLLight namespace escape to the standard theory library. I have a feeling that I have not updated the base package on gilith for too long, and will upload the latest version when I return from my vacation next week.

 think all the names in the HOLLight namespace are related to type definitions. I look forward to seeing the updated base package.

Regards,

Rob.
 
>  
> Cheers,
> 
> Joe
> 
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list