[opentheory-users] article reader for HOL4

[Joe Hurd]

Hi Ramana,

> Well although I see the usefulness of reading articles that mainly give you new
> constants/theorems that you don't already have versions of in your proof
> assistant, I think the more general approach where you might read base-1.0 into
> HOL4 is worth pursuing because base-1.0 might say just a few different or
> interesting things about basic things that HOL4 has its own versions of.  The
> most useful way to read base-1.0 in is to make it "define" your already-defined
> constants by simulating the effect of the definition (proving the necessary
> theorem whenever base-1.0 defines things slightly differently etc.). In the end
> you get a bunch of theorems many of which you already have but some of which
> you might not. And importantly, these will be in the exact right format and
> number to pass along to later opentheory articles that depend on base-1.0.

I can appreciate your reasons for wanting to import articles this way,
but (as you say) there is an additional implementation cost of
managing clashing definitions.

My comment about ignoring axioms only applies when reading articles
without clashing definitions. In your more general case I believe you
can simply treat axioms like assumptions, because the distinction
between defined and input has disappeared.

Cheers,

Joe