[opentheory-users] Importing from the Gilith OpenTheory Repo

[Rob Arthan]

Joe,

On 4 Dec 2013, at 00:15, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Rob,
> 
> > 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
> 
> When I look at the assumptions of my (perhaps more recent) pair-thm theory, it has 46 assumptions, but the 3 you list above are the only ones that refer to pair type operators and constants. The rest are theorems exported by the bool package.
> 
> So if you replace the 3 pair-def theorems with ProofPower versions, and also have all the theorems from the bool theory available, then you can prove all the theorems in pair-thm. In this way you can build up all the theorems from the standard library by just replacing the *-def theorems with ProofPower versions, processing the proofs of theorems in other packages and storing them to satisfy assumptions of later packages.
> 

You make this sound like a very piecemeal process, so I am probably misunderstanding what you have in mind. Is there are an option to opentheory that will get it to create an article file that takes all the defined constants and types in a package as inputs and has a minimal set of assumptions about them and proves all the theorems? --article doesn't do this: it generates the (HOL Light) definitions of the constants and types (including the abs and rep functions which aren't defined as part of the package). --theorems generates something that tries to define T as equal to a constant named "base-1.132".

Ultimately, I think I don't understand what the base package is trying to offer. Its assumptions are the three axioms of HOL. That implies that it must define all the types defined in the package and hence must include specific abs and rep functions for the defined types amongst the constants it exports, but it doesn't. I would have expected abstract assumptions about the defined types like the three assumptions about fst, snd and (,) above to propagate up as assumptions of the base package, but they have actually become theorems (which can 't actually be derived from the stated assumptions because the abs and rep functions have (quite rightly) not been included as part of the interface).

Regards,

Rob.