[opentheory-users] article format wording about constants

[Ramana Kumar]

On Sat, Jan 15, 2011 at 9:13 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>> What does the phrase "with definition ..." mean in the article format spec?
>> In my opinion it doesn't add anything except potential confusion.
>
> I agree that the "with definition ..." language is more confusing than
> helpful, and I've removed it from the article format spec.
>
>> However, notice the asymmetry: const takes 1 argument, constTerm takes
>> 2, but var takes 2 arguments and varTerm takes 1. Surely constants
>> should act more like variables?
>
> This asymmetry is deliberate, and reflects a fundamental difference of
> constants and variables. Constants are determined just by their name,
> but variables are determined by their name and type. This is
> illustrated by the theorems
>
> |- !(v : 'a list) (v : bool list). P (v : 'a list) (v : bool list)
>
> |- P (c : 'a list) (c : bool list)
>
> Applying the type instantiation ('a |-> bool) to both results in
>
> |- !(v : bool list) (v' : bool list). P (v : bool list) (v' : bool list)
>
> |- P (c : bool list) (c : bool list)
>
> where the two constants have been identified, but the two variables
> have been kept separate.

So why does constTerm take 2 arguments instead of just 1?
Is it just to allow you to instantiate type variables that might be in
the constant on the stack?

>
>> Also, it's not clear whether a "new constant" with the same name as a
>> previously defined constant is allowed. I presume so.
>
> This is left to the system, which must be careful to disallow
>
> define `c = T`
> define `c = F`
> prove `T = F`
>
> I believe all of the HOL theorem provers maintain a symbol table of
> constants, and will not allow redefinitions with the same name. The
> logical kernel of the opentheory tool stores the definition with the
> constant, so will happily allow redefinitions with the same name
> (because the two "c" constants above will be treated as different
> constants).

HOL4 allows redefinitions with the same name and marks the old
constant as "old"; only constants that aren't so marked can appear in
any saved theory segment, but while developing a segment it enables
one to redefine the same constant many times. You wouldn't be able to
prove `T = F` as above, though, because the theorem equating `c = T`
would be turned into `OLDc = T` when `c` is redefined, effectively
making the old one a different constant. This is similar to
opentheory, except the marks don't know anything about the definition
of the constant, they're essentially just timestamps.

So I think if while recording an OpenTheory article from HOL4 if you
redefine a constant, the right thing will happen: both systems will
treat the new constant as different from the old, even though it has
the same name.

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>