[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

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.

Cheers,

Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131204/b18415f6/attachment.html>