Fixed (and confirmed) OpenTheory builds and exports after DIV/MOD changes

[binghe]

Hi,

This PR continues #1115, in which HOL4 now allows division-by-zero in DIV and MOD.

By renaming the old DIV and MOD into OT_DIV and OT_MOD, it's now quite easy to fix the OpenTheory builds (--otknl), by just minor changes on symbol mapping. (NOTE: I also removed the infix setting of OT_DIV and OT_MOD, because they look ugly as infix operators.)

Now the div and mod operators are not OT's but belongs to the arithmetic package. I can see the following new OT theorems in hol-base:

⊦ ∀m n. arithmetic.DIV m n = if n = 0 then 0 else m div n
⊦ ∀m n. arithmetic.MOD m n = if n = 0 then m else m mod n
⊦ arithmetic.DIV k 0 = 0
⊦ arithmetic.MOD k 0 = k

while OpenTheory's original versions (Number.Natural.div and Number.Natural.mod, part of OT's own base package) is this:

⊦ ∀m n. ¬(n = 0) ⇒ (m div n) * n + m mod n = m

After long time building and installing (using the command sequence in #1121), I've built again the 900MB huge standalone OT article containing everything up to the Law of Large Numbers (in examples/probability) [1]. I confirm there's no "leaking" assumptions except for the 3 very axioms. Thus the OT build is still working. Below is a summary of all inference instructions involved (note the number of axioms is 3):

Inference rules:
eqMp ............... 6,087,228
subst .............. 5,162,407
deductAntisym ...... 4,940,216
appThm ............. 1,376,946
betaConv ............. 633,835
absThm ............... 418,810
trans ................ 398,677
refl ................. 206,898
sym .................. 173,239
assume ............... 140,593
proveHyp .............. 14,507
defineConst ............ 1,078
defineConstList ........... 72
defineTypeOp .............. 23
axiom ...................... 3
Total ............. 19,554,532

[1] https://www.dropbox.com/s/kbsgaw9w9wjhp17/hol4-large-numbers-1.1b.7z?dl=0

[mn200]

Thanks for this: it's nice to see OpenTheory continuing to work!