extreal_baseTheory (in src/real)

[binghe]

Hi,

This is the extreal_baseTheory (in src/real) we discussed in the comments of #1126. It depends on iterateTheory with the only the basic extreal operators (+, -, ~, *, /, pow, sqrt, abs, max and min) and related theorems. I didn't move EXTREAL_SUM_IMAGE and EXTREAL_PROD_IMAGE but this is indeed possible (in the future).

The code changes didn't break anything which depends on the existing extrealTheory, which still exports all theorems moved to extreal_baseTheory. To implement this behavior, there's a long list of names at the end of extrealScript.sml. I think we can keep this list for a while, until most of the user code start to open extreal_baseTheory.

All theorems in the new extreal_baseTheory are changed to modern syntax. Theorems are re-grouped and re-ordered by their key operators. I slightly modified the statements of a few rewriting rules (nothing should be broken), some proofs are simplified. Finally, the OpenTheory related definitions are also updated (but I haven't tested the full build yet, which requires long time waiting.)

Now the remaining extrealTheory contains mostly advanced part (sup, inf, sequence limits, and other set-theoretic staff). I believe the parallelism of HOL builds is also slightly improved.

Regards,

Chun Tian

P.S. in util_probTheory, the dependencies are cleaned up. A theorem IN_o (~= pred_setTheory.IN_PREIMAGE) is deleted because it's not used in the rest of probability scripts, and this theorem has another copy in examples/miller for its local use.

[mn200]

Thanks for this!