[opentheory-users] article writer for HOL4

[Ramana Kumar]

I have (almost) written an OpenTheory article writer for HOL4. (The only thing
unimplemented at the moment is type definitions.)

It uses an instrumented kernel and is heavily based on Joe's proof-logging fork
of HOL Light, and on John's original HOL Light code implementing many
"derivable but primitive" rules in the HOL4 kernel.

It has not been tested at all, and that's one reason why I'm writing:

  Is there a HOL4 theory anyone would particularly like packaged as an
  OpenTheory package?

  Are there any article readers that would benefit from testing on an article
  generated by HOL4?

I'll write more details on how to use it (which should eventually turn into
actual documentation) based on the response.

I expect some work to go into designing a package to export (indeed, better
design of composable theories is one of the advantages of using OpenTheory) so
an article-writer is only one piece of the story. But it is an important one.
Another piece is going to be how to deal with the standard theory library
within HOL4. I have some vague thoughts at the moment about a compatibility
theory importing base and exporting base plus any additional theorems in HOL4's
de facto "base" (everything up to bossLib?), so that later HOL4 theories can be
packaged on top of the standard library without explicitly only importing it.
Writing such a compatibility theory would include figuring out how to deal with
the fact that numerals are represented differently in HOL4 than in OpenTheory.
I have some ideas (well, the boring idea of just explicitly proving that there
is a semantic embedding). Also I think the design of numerals in the standard
library should be changed (will write a separate thread).

If there are any HOL Light hackers on this list who would be interested in
writing an article reader for HOL Light, I'd be very interested in
collaborating on that. I can't get HOL Light to work on my system at the
moment, so I haven't done anything yet. But I expect a lot of the ideas (and
code) from my (previously announced) article reader for HOL4 could be reused. I
think the situation at the moment is as follows (maybe this should go on the
OpenTheory website):

+-----------------+----------------+----------------+
| system          | article reader | article writer |
+-----------------+----------------+----------------+
| opentheory tool |      yes       |      yes       |
+-----------------+----------------+----------------+
| HOL Light       |      no        |      yes       |
+-----------------+----------------+----------------+
| HOL4            |      yes       |      yes       |
+-----------------+----------------+----------------+
| ProofPower      |      no        |      no        |
+-----------------+----------------+----------------+
| HOL Zero        |      no        |      no        |
+-----------------+----------------+----------------+
| Isabelle/HOL    |      yes       |      no        |
+-----------------+----------------+----------------+
(the tool is not a proof assistant, but still has to process articles)

Half way there! Until we move on to more ambitious translation possibilities...
(arguably Isabelle is beyond the scope of the original project already).