<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Joe,<div><br><div><div>On 4 Dec 2013, at 17:53, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">...</div></blockquote><blockquote type="cite"><div dir="ltr"><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></blockquote><blockquote type="cite"><div dir="ltr"><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></blockquote></div><br></div><div>I am now trying to follow this procedure and am having one or two problems.</div><div><br></div><div>The packages natural-numeral and natural-dest seem to be exceptions to the rule that all the definition live in packages with names of the form XYZ-def.</div><div><br></div><div>The packages don’t seem to come out in dependency order. E.g., the first few leaf packages in the natural package come out like this:</div><div><br></div><div>natural-add-def-1.18<br>natural-add-sub-def-1.3<br>natural-add-sub-thm-1.3<br>natural-add-thm-1.47<br>natural-def-1.23<br><br></div><div>But the definition of addition in natural-add-def depends on suc from natural-def.</div><div><br></div><div>When you say “the remaining theory packages in the list can be converted to an article using opentheory info —article”, do you mean that I can create a single article for them all? If so how do I do it? (opentheory info seem only to support a single INPUT.)</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>