[opentheory-users] article reader for HOL4

[Joe Hurd]

Hi Michael,

Yes, numerals are one step beyond a simple renaming of constant names,
and seem to be an example where every theorem prover has its own
scheme.

> I guess HOL4, red-haired step-child that it is, can special case those
> constants in any articles that it reads, and also do the appropriate inverse
> thing when writing its own articles.

I think this is the right strategy, and I even had to do this for HOL
Light, which had a NUMERAL tag around numerals and a special zero used
inside numerals. I tried to make the OpenTheory numeral scheme the
simplest possible: it uses the standard zero from the natural numbers,
two bit0 and bit1 functions, and no surrounding tag.

> What does ProofPower do for numerals?

I don't know the answer to this. Rob Arthan might, and since he isn't
on this mailing list I have cc'ed him on this message.

> Presumably this kind of translation will be beyond the capabilities of the
> meta-datato describe.

I had some success automatically detagging HOL Light theorems as I
extracted them, but switching numerals sounds a little harder.

Cheers,

Joe