Monoid theory moved from examples/algebra to src/algebra (core library)

[binghe]

Hi,

The abstract algebra work (under examples/algebra, etc.) by (Joseph) Hing-Lun Chan is an important contribution to HOL4. The present huge PR moves this work (up to monoid, only) into the core library, under a new directory "src/algebra".

Perhaps It's impossible to review all code changes (50k+ additions, 58k- deletions) in the commits. Below is just a summary of ideas behind those changes:

• No theorem is removed unless it's duplicate with those already in core theories.
• The following new core theories (under "src/algebra") are added, by combining small theories which was in examples/algebra/lib and examples/fermat:
  1. numberTheory: theorems about numbers that involves new definitions beyond arithmeticTheory, gcdTheory, etc.
  2. combinatoricsTheory: definitions and theorems usually considered as part of "Combinatorics" (e.g. the necklaceTheory and the original combinatoricsTheory under examples/fermat)
  3. primeTheory: theorems about prime numbers which depends on combinatoricsTheory.
     • monoidTheory is added as a combined theory of all theories under examples/algebra/monoid except for the one depending on real numbers.
     • real_algebraTheory is added (under "src/real") with the monoid of real numbers (for now). This theory will collect other algebra objects based on real numbers, in the future.
     • Many theorems (at last 10k lines of code) were moved from "examples/algebra/lib" to other existing theories (arithmetic, divides, gcd, gcdset, list, rich_list, pred_set, bag, etc.) to enrich these theories with more supporting theorems. In the future, we should keep polishing the new theories under "src/algebra" to move some small theorems to upstream theories.
     • There's a theorem SNOC_LAST_FRONT (⊢ ∀l. l ≠ [] ⇒ SNOC (LAST l) (FRONT l) = l)recently added into rich_listTheory but is conflict with another similar theorem from examples/algebra. I give the algebra materials the higher priority and renamed my theorem to SNOC_OF_LAST_FRONT. (NOTE: this change is now reverted. The similar theorem from algebra materials is now called SNOC_LAST_FRONT', which is used only 4 times in polyWeakScript.sml.)
• The original algebra work contains some small overloads (such as SQ = \n. n * n, HALF, TWICE, etc.) which I consider not very necessary. I have changed them to temp_overload_on() without touching their proofs.
• The two local directories "examples/algebra/lib" and "examples/algebra/monoid" can be deleted after this PR as they are empty now.

Once the present PR gets merged, the next steps would be moving also the groupTheory and ringTheory, etc. (after theory combinations) to "src/algebra", and then start making connections to other existing theories.

Chun Tian

[binghe]

On a second thought, the name change of SNOC_LAST_FRONT (in listTheory) should be reverted for better backward compatibility (important if this PR is not going to merge before T1 release), and in this way all changes in examples/lambda can be reverted too, reduced the total number of changed lists in the PR branch.

[binghe]

Per our offline discussions, the new files under src/algebra are moved into src/algebra/base (for number, prime and combinatorics) and src/algebra/construction (for monoid and the small jcLib). The directory "src/algebra" itself depends on the two subdirectories and will be reserved for the algebraTheory containing the (combined) type-based algebra formalizations.

[mn200]

Thanks!