Remaining issues of HOL's OpenTheory packaging

[binghe]

Following PR #803, I found the following remaining issues in OpenTheory packaging:

1. The recently added itself type in boolTheory introduced some new type, constant and theorems. When these theorems are used in other core theories, they become external constants and extra assumptions in the OpenTheory package, because the hol-base package doesn't package boolTheory at all, instead it tries to reuse what OpenTheory's own base package has, with a minimal fake bool theory defined in src/boss/bool_defsScript.sml. This mechanism can be seen in src/boss/hol4-base.thy:

bool {
  article: "bool_defs.ot.art"
  interpret: const "HOL4.bool_defs.LET" as "HOL4.bool.LET"
  interpret: const "HOL4.bool_defs.literal_case" as "HOL4.bool.literal_case"
  interpret: const "HOL4.bool_defs.IN" as "HOL4.bool.IN"
  interpret: const "HOL4.bool_defs.TYPE_DEFINITION" as "HOL4.bool.TYPE_DEFINITION"
  interpret: const "HOL4.bool_defs.ARB" as "HOL4.bool.ARB"

  interpret: type "HOL4.min.ind" as "ind"
  interpret: const "HOL4.min.@" as "select"
  interpret: const "HOL4.bool.!" as "Data.Bool.!"
  interpret: const "HOL4.bool.?" as "Data.Bool.?"
  interpret: const "HOL4.bool.?!" as "Data.Bool.?!"
  interpret: const "HOL4.bool.T" as "Data.Bool.T"
  interpret: const "HOL4.bool.F" as "Data.Bool.F"
  interpret: const "HOL4.bool./\\" as "Data.Bool./\\"
  interpret: const "HOL4.bool.\\/" as "Data.Bool.\\/"
  interpret: const "HOL4.min.==>" as "Data.Bool.==>"
  interpret: const "HOL4.bool.~" as "Data.Bool.~"
  interpret: const "HOL4.bool.COND" as "Data.Bool.cond"
  interpret: const "HOL4.bool.ONE_ONE" as "Function.injective"
  interpret: const "HOL4.bool.ONTO" as "Function.surjective"
}

I think it's better to not touch boolTheory any more, and move the existing itself type to other core theory files like oneTheory (as they're quite similar), which will be packaged as is. But, if one really wants to add new theorems in boolTheory, to maintain the OpenTheory compatibility, we need to also update src/boss/prove_base_assumsScript.sml adding the same theorem in.

2. Some HOL theories (e.g. real_topologyTheory) are too big to generate .ot.art files within limited memory (e.g. 16GB). This is also one reason that I file PR #804 to move some theorems out of real_topologyTheory.

3. I think HOL's OpenTheory reader (now at src/opentheory/reader/OpenTheoryReader.sml) is not a fully functional reader: it doesn't actually replay the proof steps stored in .art files, because the loaded theorems all have special tags (MK_THM?) with them. Currently it only reads out the theorem statements in *.art files.

--Chun

[binghe]

4. src/coalgebras/ltree.art cannot be converted to ltree.ot.art. See https://github.com/HOL-Theorem-Prover/HOL/pull/958#issuecomment-950878372 for more details.

NOTE: point 3 seems not true: HOL's OpenTheory reader can indeed replay proofs stored in OpenTheory articles.

[binghe]

Copied from PR #1022:

5. ordinalTheory now contain workarounds for the definition of ordDIV and ordMOD as described already. If OpenTheory (or the exporting code in HOL) gets fixed in the future, my current workaround should be reverted.
6. The newly added theorem option_case_eq' in optionTheory must have been already proved somewhere but I just cannot find it in HOL's core theory proofs. Perhaps it's actually inside a library?
7. The OpenTheory importing facility is totally broken. In src/opentheory/compat there are some sample HOL theories to try to import bool and other packages from OT and turn it into a valid HOL theory with proofs. So far I only fixed obvious mistakes due to SML structure name changes.
8. Currently there's no symbol mapping between OT's set and HOL's pred_set. There are some related mapping calls in pred_setScript.sml but I think currently all such calls do not work at all.