<div dir="ltr">Hi Rob,<div><br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">

<div><div><div><blockquote type="cite"><div dir="ltr"><div>One of the design goals of OpenTheory is to have very precisely defined standards, to maximize compatibility between tools that implement them, and even though I can see the conceptual unity of your proposed "spec" command it doesn't give precise enough instructions as to what the reader should do for my taste.</div>

</div></blockquote></div><div>I thought it was precise. The reader must introduce the new types and constants and make the sequence become axioms. The only implementation-defined aspect is that it can use the justification to do this theory extension conservatively if it knows how. However, ...</div>

</div></div></div></blockquote><div><br></div><div>I think this point has become moot, but I wanted to add one thing: I can imagine article readers that are not connected to a theorem prover (e.g., a compiler reading a HOL definition of a program and then compiling it to native code). So I would really like the file format to be as brain-dead as possible, to encourage these applications.</div>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div><div><blockquote type="cite"><div dir="ltr">
<div>Instead I have sketched out the spec for a draft "defineConstList" command</div><div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html#defineConstListCommand" target="_blank">http://www.gilith.com/research/opentheory/article.html#defineConstListCommand</a><br>

</div></div></blockquote><div><br></div></div>… I can’t complain! The above is what I (and, I guess, Ramana) had in mind originally. However, that still leaves me with the problem of the other thread, which amounts to the fact that I do not see a practical way of implementing a reader that can make use of the Gilith OpenTheory Repo. I will expand on that in the other thread.</div>

</div></div></blockquote><div><br></div><div>I can see your point about integrating the base package into a theorem prover, and I confess I have not done enough eating of my own dogfood in this regard. It's been on my TODO list for a long time to take a fresh version of HOL Light and implement an OpenTheory reader so that a user can type something like</div>
<div><br></div><div>import-theories ["base", "natural-prime"];;</div><div><br></div><div>and it would read in these theories and give them a context where the exported symbols have been defined and the theorems have been proved, grafting as naturally as possible onto the existing HOL Light theories. Then whatever theorems the user proves can be exported with theory meta-data</div>
<div><br></div><div>required: base</div><div>required: natural-prime</div><div><br></div><div>and the dependencies checked when the dependencies evolve. But I simply haven't got around to it...</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div>I am happy with the derived rules. By a fortunate coincidence, you have put the parameters to trans and proveHyp on the stack in the same order as I do in my writer.</div></div>
</div></blockquote><div><br></div><div>Excellent.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div>For proveHyp (and deductAntisym) it might be helpful to say explicitly that the rules do not fail if the formula phi is not present in Delta.</div>
</div></div></blockquote><div><br></div><div>Thanks, that's a good suggestion. I've added the documentation to both commands.</div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div>
</div></div>