[opentheory-users] article reader for HOL4

[Ramana Kumar]

On Mon, Jan 10, 2011 at 12:30 AM, Joe Hurd <joe at gilith.com> wrote:
> 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.

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.

>
>> 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.

But you can't just ignore them because you need to really provide a theorem for
every axiom when you're reading the article, otherwise you won't get any
theorems back.

>
> Does that help?

Well, I'm glad you think my description was quite accurate :) I'm a little
confused by what you said about axioms though.

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