<div dir="ltr">Hi Rob,<div><br></div><div>I thought about your comments, and I take your point that even though OpenTheory uses theory boundaries to enforce abstraction there are some compelling reasons to support a definition principle such as your new proposed mechanism that has better abstraction properties.</div>
<div><br></div><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><br></div><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">http://www.gilith.com/research/opentheory/article.html#defineConstListCommand</a><br>
</div><div><br></div><div>which is intended to match your proposed definition mechanism. Writers using this command will almost certainly need to save the new constants to the dictionary to build new terms, hence the need for another new command to take apart lists:</div>
<div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html#hdTlCommand">http://www.gilith.com/research/opentheory/article.html#hdTlCommand</a><br></div><div><br></div><div>which is simply the inverse of cons.</div>
<div><br></div><div>I was reluctant before now to introduce any derived inference rules, because another design goal of OpenTheory is to make it as simple as possible to implement readers. However, I have convinced myself that this is not an issue, because you can convert a version 6 article into a logically equivalent version 5 article, and so a reader can always perform this preprocessing step to avoid dealing with derived rules.</div>
<div><br></div><div>Following this new line of thinking, I have introduced some extra derived rules</div><div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html#symCommand">http://www.gilith.com/research/opentheory/article.html#symCommand</a><br>
</div><div><a href="http://www.gilith.com/research/opentheory/article.html#transCommand">http://www.gilith.com/research/opentheory/article.html#transCommand</a><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html#proveHypCommand">http://www.gilith.com/research/opentheory/article.html#proveHypCommand</a><br>
</div><div><br></div><div>that only depend on equality, and if writers choose to make use of them will hopefully help to compress the resulting article files.</div><div><br></div><div>Please take a look at the new version 6 draft standard and let me know what you think:</div>
<div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html">http://www.gilith.com/research/opentheory/article.html</a><br></div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br>
</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Mar 15, 2014 at 6:30 AM, 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"><div style="word-wrap:break-word">Joe,<div><br><div><div class=""><div>On 14 Mar 2014, at 21:35, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote:</div>
<br><blockquote type="cite"><div dir="ltr">I have thought about this some more, and I believe I have answered my own questions.<div><br></div><div>1. The proposed definition mechanism is not more expressive than new_definition, because it can be simulated by first defining c_1 = t_1, ..., c_n = t_n, instantiating the given theorem with the substitution [c_1/v_1, ..., c_n/v_n], and then using the definition theorems of the c_i to prove the hypotheses.</div>
</div></blockquote><br></div><div>It doesn’t claim to be more expressive. What it is designed to offer is abstraction. The OpenTheory kernel has a different way of hiding representation details, but HOL4, HOL Light, ProofPower and the OpenTheory article format don’t have that option.</div>
<div class=""><br><blockquote type="cite"><div dir="ltr"><div> So I think the best thing is to keep the OpenTheory defineConst mechanism, and "compile" the proposed definition mechanism using the above scheme.</div>

<div><br></div></div></blockquote></div>But that means that the article format can’t express the desired abstraction in a way that can be ported from one system to another. That seems like a major shortfall to me.</div><div>
<br></div><div>My proposal for OpenTheory would be a new command, called “spec” say, which would actually provide the functionality of new_type, new_const, new_axiom, new_specification, gen_new_specification and new_type_definition in their HOL4, ProofPower and HOL Light guises. (Here gen_new_specification is the new principle from HOL Constant Definition Done Right.) “spec" would have four parameters:</div>
<div><br></div><div>(1) a list of type name/arity pairs identifying new types to be introduced;</div><div>(2) a list of constant name/type pairs identifying new constants to be introduced (the types in list (1) may appear in the types of these constants);</div>
<div>(3) A list of sequents giving new axioms to be introduced (the types in list (1) and the constants in list (2) may appear in these sequence);</div><div>(4) a list of objects, which constitute a “justification” for the new axiom.</div>
<div><br></div><div>(4) would be empty for new_axiom, new_const or new_type. It would give the input theorem for new_specification, gen_new_specification and new_type_definition.</div><div><br></div><div>A reader would analyse the parameters to figure out the best way to introduce the types and constants and so derive the required axioms. Recognising the various new_XYZ forms that I listed above and allowing for the differences between systems is easy and the reader can always fall back on a combination of new_type, new_const and new_axiom (or some kind of cheat).</div>
<div><br></div><div>By making parameter (4) a list of objects, the “spec” command is general enough to accommodate any conceivable extension to the definitional mechanisms without changing the article format.</div><div><br>
</div><div>The “spec” also makes the article format support higher levels of abstraction. For example, it would let the Gilith OpenTheory repo describe the types and constants in the base package (and others) in a way that is easy to import. The pair type for example, would be introduced by a spec command that introduces the type constructor “x", the constants “,”, “fst” and “snd” and with the theorems that characterize the type in terms of these constants as the new axioms. The justification could be a string like “primitive” to hint to a reader that it should already have the types and constants. This declarative approach would make the base package a really useful resource (solving the problems discussed in this thread: <a href="http://www.gilith.com/opentheory/mailing-list/2013-December/000329.html" target="_blank">[opentheory-users] Importing from the Gilith OpenTheory Repo</a>).</div>
<div><br></div><div><div class=""><blockquote type="cite"><div dir="ltr"><div>2. I think my simplification is bogus because defining the c_i in terms of c can fail because of the type variable condition.</div><div><br></div>
</div></blockquote></div>That is correct.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div><br></div></div><br>_______________________________________________<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>
<br></blockquote></div><br></div>