<div dir="ltr">Hi Rob,<div><br></div><div>1. Let me first explain the info options, which could probably do with being renamed for clarity.</div><div><br></div><div>opentheory info --article outputs a proof from assumptions to theorems, and is the main way for users to generate articles from theory packages</div>
<div><br></div><div>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.</div>
<div><br></div><div>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).</div>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div><div>
<br></div><div>However, you can use the opentheory tool to list all the 'leaf' theory packages inside base, using the following magic incantation:</div><div><br></div><div>opentheory list --dependency-order '(Identity - IncludedBy) (Includes* base)'<br>
</div><div><br></div><div>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.</div>
<div><br></div><div>I hope that helps clear things up a bit.</div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Dec 4, 2013 at 1:06 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Joe,<br>
<div><div class="h5"><br>
On 4 Dec 2013, at 00:15, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br>
<br>
> Hi Rob,<br>
><br>
> > 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:<br>

><br>
> > !xy?x y. xy = (x, y)<br>
><br>
> > !x y. fst(x, y) = x<br>
><br>
> > !x y. snd(x, y) = y<br>
><br>
> 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.<br>

><br>
> 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.<br>

><br>
<br>
</div></div>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".<br>

<br>
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).<br>

<br>
Regards,<br>
<br>
Rob.<br>
<div class="HOEnZb"><div class="h5">_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br></div>