[opentheory-users] numerals

[Ramana Kumar]

On Tue, Sep 6, 2011 at 10:41 PM, Joe Hurd <joe at gilith.com> wrote:
> 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.

Indeed you may even be able to omit step 2 if there is a
"compatibility package" sitting above base that defines bit2.
There is, in general, a mismatch between the standard library and the
theorems you might actually use in producing some HOL4 theory.
For example, the standard library defines "Data.List.replicate", which
isn't in HOL4 but could easily be defined with GENLIST.
GENLIST isn't in the standard library, but could easily be defined on top of it.
Since multiple HOL4 theories might use GENLIST, it might make sense
for them both to depend on a package defining it that in turn only
depends on the standard base.

Now the same goes for the constants bit0, bit1, and bit2. HOL4 doesn't
have bit0 and OpenTheory doesn't have bit2, but they can both be
defined where they are missing. Indeed if we read the base package
into HOL4 (matching up constants where possible), things like bit0 and
replicate will get defined, and it might be a good idea to do that.
The problem with numerals is that you might want to subsequently
remove bit0 (or bit2) from your theorems if you have special
infrastructure for pretty-printing. But the same can hold in theory
for other constants - maybe you have an excellent library of facts
about GENLIST and want to use it after reading in a theory that uses
replicate. A solution is to prove the appropriate equivalence then
rewrite to the desired form. I don't see a way around doing a bit of
work to that effect, and I don't think it's a bad piece of work to be
doing... but may others imagine different usage?

>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>