[opentheory-users] numerals

[Joe Hurd]

Hi Michael,

> I certainly wouldn't want to have to take a HOL4 calculation of some ground
> formula and then, when ready to export, have to turn that calculation into
> one that was a valid HOL Light/OpenTheory calculation.

Sorry I wasn't clear about this. Here's what I had in mind:

1. Do some numerical calculations to prove a HOL4 theorem:

|- P[bit1,bit2]

2. When exporting such a theorem, first prove a theorem of the following form:

|- P[bit1,bit2] = P'[bit0,bit1]

3. Export the theorem

|- P'[bit0,bit1]

That way the numerical calculations wouldn't have to be reproved;
there would just be a "post-processing phase" converting between
different representations of numerals.

Cheers,

Joe