[opentheory-users] article format wording about constants

[Ramana Kumar]

On Sat, Jan 15, 2011 at 9:41 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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.

This is not true in HOL4.
The following does not raise Bind:

val P = mk_var("P",``:'a list -> bool list -> bool``)
val va = mk_var("v",``:'a list``)
val vb = mk_var("v",``:bool list``)
val Pvv = list_mk_comb(P,[va,vb])
val Pvv = mk_thm([],Pvv)
val false = let
  val (_,[va,vb]) = strip_comb(concl Pvv)
in va = vb end
val Pvv' = INST_TYPE [alpha|->bool] Pvv
val true = let
  val (_,[va,vb]) = strip_comb(concl Pvv')
in va = vb end


>
> 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
>>
>