<div dir="ltr"><div><div><div>Could someone clue me in on why defineConstList (a.k.a gen_new_specification) is necessary? From the paper, I read that it takes as input<br><br>v1 = t1, ..., vn = tn |- p<br><br></div>and produces<br><br>|- p[c1/v1, ..., cn/vn]<br><br></div>Doesn't this trivially follow from the separate definitions c1 = t1, ..., cn = tn? What is the purpose of a separate redundant axiom for this?<br><br></div>Mario<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Nov 5, 2014 at 6:21 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>
<span class=""><br>
On 5 Nov 2014, at 22:49, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br>
<br>
> Hi Rob,<br>
><br>
> [I'm cc'ing the OpenTheory list because the discussion may be of<br>
> general interest.]<br>
><br>
> I just finished implementing the new principle of constant definition<br>
> described in your paper "HOL Constant Definition Done Right":<br>
><br>
> <a href="http://www.lemma-one.com/papers/hcddr.pdf" target="_blank">http://www.lemma-one.com/papers/hcddr.pdf</a><br>
<br>
</span>Excellent!<br>
<span class=""><br>
><br>
> It all makes perfect sense to me and the instructions were<br>
> straightforward to follow, but I was wondering if you could explain<br>
> the rationale behind this constraint:<br>
><br>
> "the free variables of p must be contained in the v_i"<br>
><br>
> It seems sound to permit extra free variables, for example in the<br>
> following definition<br>
><br>
> v = 0 |- n + v = n<br>
<br>
</span>It would be sound to permit that, but I have a prejudice against<br>
free variables in defining properties, so I was deliberately requiring<br>
the user to take the universal closure w.r.t. the variable n in an<br>
example like the above, so that the resulting defining property<br>
would be a closed formula.<br>
<span class=""><br>
><br>
> Also, why "contained in" and not "exactly"? If there are extra<br>
> variables v_i that are not free in p, then it is a simple matter to<br>
> remove them from the hypotheses before calling gen_new_specification.<br>
<br>
</span>Yes, but then the rule won’t introduce the corresponding constants.<br>
I don’t think this is very important, but I didn’t want to require<br>
the user to impose a constraint on all the new constants.<br>
<span class=""><br>
><br>
> Finally, a practical point that I ran into during implementation: in<br>
> the case where the set v_i is empty (i.e., there is nothing to<br>
> define), should the input theorem simply be returned or do you<br>
> consider that an error condition?<br>
<br>
</span>The current ProofPower implementation allows the set to be empty<br>
and just stores the input theorem as a definition (of nothing) in that<br>
case. I think that is it how it is specified in the CakeML work too.<br>
Maybe Ramana could confirm that.<br>
<br>
Regards,<br>
<br>
Rob.<br>
<div class="HOEnZb"><div class="h5"><br>
<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>
</div></div></blockquote></div><br></div>