[opentheory-users] New principle of constant definition

[Rob Arthan]

Joe,

On 5 Nov 2014, at 22:49, Joe Leslie-Hurd <joe at gilith.com> 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":
> 
> http://www.lemma-one.com/papers/hcddr.pdf

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.