[opentheory-users] definition of "new" constants?

[Ramana Kumar]

On 9 August 2015 at 19:02, Günter Rote <rote at inf.fu-berlin.de> wrote:

> Am 08.08.2015 um 03:16 schrieb Joe Leslie-Hurd:
> > Thanks for the clarification, I have added a note to defineConst and
> > defineTypeOp to spell this out:
> >
> >
> http://www.gilith.com/research/opentheory/article.html#defineConstCommand
> >
> http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand
>
> Thanks. But what is the *principal* type of the new constant?
>

HOL constants are polymorphic. But the type of every instance of a
particular constant is a type instance of one particular type. That one
type is the principal type of the constant.


> (And maybe you want to update defineConstList as well?)
>

Yes, I think an analogous note would make sense.


>
> Am 15.01.2011 um 03:16 schrieb Joe Leslie-Hurd:
> http://www.gilith.com/opentheory/mailing-list/2011-January/000080.html
> >> 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
> >
> 1. define `c = T`
> 2. define `c = F`
> 3. 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).
>
> This puzzles me.
> If I now create another "instance" of a constant with name c
> (and type bool) by a const+constTerm command, to which
> constant from among definitions 1 or 2 (if any) does it
> refer to?


Neither. The only way to get the constants from the definitions in 1 and 2
is as the objects returned by the definition commands.


> (More specifically, to which c will it be
> alpha-equivalent, when this is for example tested in
> the course of eqMP?)
>

(neither)


> And does the answer change for a constant c that was
> "created" before definitions 1 and 2?
>

No. (I'm not 100% confident of these three answers; Joe will know best.)


>
> best regards : Günter
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150809/b6c64e79/attachment.html>