[opentheory-users] article reader for HOL4

[Joe Hurd]

Hi Ramana,

I think this description you have here is quite accurate: I only have
a few minor places where I might improve it.

> In
> that case when the article defines/proves something, the reader just supplies
> its existing constant/theorem.

The reader is only supposed to provide existing things to meet input
type operators, constants and assumptions. So for example you would
never read the base-1.0 theory into HOL4, because it already has
definitions for the Boolean operators. However, it might make sense to
read in the theory list-replicate-1.0 which defines and proves
properties about a list replicate function (assuming that HOL4 doesn't
already define this function). It might also make sense to read in the
theory list-map-thm-1.0, which doesn't define anything, but proves a
bunch of theorems about the list map function.

> Axioms are theorems about the defined constants that the article needs to use
> but doesn't prove.

Axioms are simply assumptions made about type operators and constants
that the article defines, and can be safely ignored because HOL4
already has versions of them for its own definitions of Booleans and
natural numbers.

Does that help?

Cheers,

Joe