[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

Hi Rob,

1. Let me first explain the info options, which could probably do with
being renamed for clarity.

opentheory info --article outputs a proof from assumptions to theorems, and
is the main way for users to generate articles from theory packages

opentheory info --theorems (--assumptions) outputs an article file
consisting of just the theorems (assumptions) of the theory package, with
axiom proofs. It's just used for caching the theorems (assumptions) to
speed up processing later, and users shouldn't need to use these options.

2. The constants and type operators listed as defined by a theory package
only include those that appear in an exported theorem. The exact form of
the definition of these symbols is internal to the package, and is
something that users of the theory package should never need to know. In
fact the OpenTheory logical kernel is purely functional, so auxiliary
symbols such as the abs and rep functions don't even end up polluting a
global symbol table (though this might theoretically cause problems in
other HOL theorem provers that don't implement a purely functional logical
kernel).

3. The base theory package is the standard theory library, which is
supposed to be a common base implemented by all theorem provers in the HOL
family, but of course not every theorem is proved in the same form in all
HOL theorem provers, so there is a use case for importing the base theory
package.

Unfortunately there isn't a good way of generating a single article from
base that can be imported by the HOL theorem provers, because the
definitions will be mixed in with the theorems.

However, you can use the opentheory tool to list all the 'leaf' theory
packages inside base, using the following magic incantation:

opentheory list --dependency-order '(Identity - IncludedBy) (Includes*
base)'

Suppose each theorem in the *-def theory packages can be replaced with a
ProofPower theorem. The remaining theory packages in the list can be
converted to an article using opentheory info --article and imported into
ProofPower. These articles shouldn't make any definitions and their
assumptions should only consist of theorems proved by theory packages
earlier in the list. At the end of this process you would have every
theorem in the base theory package imported into ProofPower.

I hope that helps clear things up a bit.

Cheers,

Joe


On Wed, Dec 4, 2013 at 1:06 PM, Rob Arthan <rda at lemma-one.com> wrote:

> 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.
> _______________________________________________
> 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/20131204/42323167/attachment.html>