[opentheory-users] New principle of constant definition

[Joe Leslie-Hurd]

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

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

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.

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?

Cheers,

Joe