[opentheory-users] article reader for HOL4

[Joe Hurd]

Hi Rob,

Welcome to the list!

> ProofPower predates the invention of the bit representations used in HOL4 and HOL Light and improves upon the Classic HOL base 1 representation, by treating natural number literals as a special case in the logical kernel. Natural number literals are constants distinguished by having the right type and having names comprising a string of decimal digits. There is a built-in conversion plus_conv which proves all theorems of the form |- m + n = k where m, n and k are natural number literals.

It appears that I was correct in my assertion that all the HOL theorem
provers use different numeral representations! However, even though
ProofPower uses an infinite family of constants together with an extra
rule of inference, I don't believe it will be too hard to convert to
and from the OpenTheory scheme which defines bit0 and bit1, and uses
these constants together with natural number zero to represent
numerals. A simple proof procedure can be used to provide a
fully-expansive OpenTheory proof of the theorem

|- m + n = k

where m, n and k are OpenTheory numerals. In the opposite direction the theorems

|- bit0 m = m + m

and

|- bit1 m = bit0 m + 1

should be able to be used in conjunction with plus_conv to
post-process theorems imported into ProofPower that contain OpenTheory
numerals.

Cheers,

Joe