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