[opentheory-users] New principle of constant definition
joe at gilith.com
Wed Nov 5 22:49:17 UTC 2014
[I'm cc'ing the OpenTheory list because the discussion may be of
I just finished implementing the new principle of constant definition
described in your paper "HOL Constant Definition Done Right":
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
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?
More information about the opentheory-users