HOL-Theorem-Prover · mn200 · May 10, 2024 · Apr 21, 2024 · Apr 21, 2024 · Apr 21, 2024
diff --git a/doc/next-release.md b/doc/next-release.md
@@ -26,6 +26,14 @@ Bugs fixed:
 New theories:
 -------------
 
+- `number`, `combinatorics` and `prime`: These are combined theories of materials
+   from `examples/algebra/lib`, etc. They contain some more advanced results from
+   number theory (in particular properties of prime numbers) and combinatorics.
+
+- `monoid` (and `real_algebra`): These are combined theories of materials ever in
+  `examples/algebra/monoid`. A monoid as an algebraic structure: with a carrier set,
+   a binary operation and an identity element.
+
 New tools:
 ----------
 

diff --git a/examples/AKS/compute/Holmakefile b/examples/AKS/compute/Holmakefile
@@ -1,4 +1,2 @@
-PRE_INCLUDES = ../../algebra/ring
-
-ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield
+ALGEBRA_INCLUDES = group ring field polynomial finitefield
 INCLUDES = $(patsubst %,../../algebra/%,$(ALGEBRA_INCLUDES)) 
diff --git a/examples/AKS/compute/computeAKSScript.sml b/examples/AKS/compute/computeAKSScript.sml
@@ -12,11 +12,12 @@ val _ = new_theory "computeAKS";
 
 (* ------------------------------------------------------------------------- *)
 
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
+(* open dependent theories *)
+open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
+     dividesTheory gcdTheory primeTheory;
 
 (* Get dependent theories local *)
 (* val _ = load "computeParamTheory"; *)
@@ -29,27 +30,8 @@ open computeRingTheory computePolyTheory;
 open polyWeakTheory polyRingTheory;
 open polyMonicTheory polyDivisionTheory;
 
-(*
-open helperFunctionTheory; (* for SQRT_LE *)
-open logPowerTheory; (* for ulog *)
-open ringTheory ringInstancesTheory; (* for ZN_coprime_order_alt *)
-open monoidOrderTheory;
-*)
 open ringInstancesTheory; (* for ZN_ring *)
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory;
-
-(* open dependent theories *)
-open pred_setTheory listTheory arithmeticTheory;
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open dividesTheory gcdTheory;
-open logPowerTheory;
-
-
 (* ------------------------------------------------------------------------- *)
 (* AKS Computations Documentation                                            *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/AKS/compute/computeBasicScript.sml b/examples/AKS/compute/computeBasicScript.sml
@@ -12,38 +12,18 @@ val _ = new_theory "computeBasic";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
-
-(* Get dependent theories local *)
-
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *)
-(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *)
-(* val _ = load "logPowerTheory"; *)
-open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory;
-open pred_setTheory listTheory arithmeticTheory;
-
-open logPowerTheory; (* for LOG2, SQRT, and Perfect Power, Power Free *)
-open logrootTheory;
-
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open dividesTheory gcdTheory;
-
-(* val _ = load "GaussTheory"; *)
-open EulerTheory;
-open GaussTheory;
+open pred_setTheory listTheory arithmeticTheory logrootTheory dividesTheory
+     gcdTheory gcdsetTheory numberTheory combinatoricsTheory primeTheory;
 
 (* val _ = load "whileTheory"; *)
 open whileTheory;
 
+val _ = temp_overload_on("SQ", ``\n. n * n``);
+val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
+val _ = temp_overload_on("TWICE", ``\n. 2 * n``);
 
 (* ------------------------------------------------------------------------- *)
 (* Basic Computations Documentation                                          *)

diff --git a/examples/AKS/compute/computeOrderScript.sml b/examples/AKS/compute/computeOrderScript.sml
@@ -12,46 +12,18 @@ val _ = new_theory "computeOrder";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
-
-(* Get dependent theories local *)
-
-(* open dependent theories *)
-(* val _ = load "fieldInstancesTheory"; *)
+open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
+     dividesTheory gcdTheory logrootTheory primeTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *)
-(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *)
-open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory;
-open pred_setTheory listTheory arithmeticTheory;
-
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open dividesTheory gcdTheory;
-
-(* val _ = load "fieldInstancesTheory"; *)
-open monoidInstancesTheory;
 open groupInstancesTheory;
 open ringInstancesTheory;
 open fieldInstancesTheory;
 open groupOrderTheory;
-open monoidOrderTheory;
 
-(* val _ = load "GaussTheory"; *)
-open EulerTheory;
-open GaussTheory;
-
-(* val _ = load "computeBasicTheory"; *)
 open computeBasicTheory;
-open logrootTheory logPowerTheory;
-
 
 (* ------------------------------------------------------------------------- *)
 (* Order Computations Documentation                                          *)

diff --git a/examples/AKS/compute/computeParamScript.sml b/examples/AKS/compute/computeParamScript.sml
@@ -14,26 +14,17 @@ val _ = new_theory "computeParam";
 
 open jcLib;
 
-(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
+open prim_recTheory pred_setTheory listTheory arithmeticTheory logrootTheory
+     dividesTheory gcdTheory numberTheory combinatoricsTheory primeTheory;
 
 (* Get dependent theories local *)
 open computeOrderTheory;
-open helperFunctionTheory; (* for SQRT_LE *)
-open logPowerTheory; (* for ulog *)
 open ringTheory ringInstancesTheory; (* for ZN_coprime_order_alt *)
-open monoidOrderTheory;
-
-(* Get dependent theories in lib *)
-open helperNumTheory helperSetTheory;
-
-(* open dependent theories *)
-open prim_recTheory pred_setTheory listTheory arithmeticTheory;
-open dividesTheory gcdTheory;
-
-open GaussTheory; (* for phi_pos *)
-open EulerTheory; (* for residue_def *)
-open triangleTheory; (* for list_lcm_pos *)
+open monoidTheory;
 
+val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
+val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
+val _ = temp_overload_on("TWICE", ``\n. 2 * n``);
 
 (* ------------------------------------------------------------------------- *)
 (* AKS Parameter Documentation                                               *)
@@ -67,7 +58,6 @@ open triangleTheory; (* for list_lcm_pos *)
    coprime_candidates_ne_1      |- !n m. 1 < m ==> 1 NOTIN coprime_candidates n m
    ZN_order_good_enough         |- !n m. 1 < n /\ 1 < m ==> ?k. 1 < k /\ coprime k n /\ m <= ordz k n
 
-
    Smallest Candidate
    least_prime_candidates_property    |- !n m. 1 < n /\ 0 < m ==> !h. prime h /\ coprime h n /\
                                                h < MIN_SET (prime_candidates n m) ==>
@@ -278,10 +268,6 @@ open triangleTheory; (* for list_lcm_pos *)
    param_good_range    |- !n k. (param n = good k) ==> 1 < n /\ 1 < k /\ k < n
 *)
 
-(* ------------------------------------------------------------------------- *)
-(* Helper Theorems                                                           *)
-(* ------------------------------------------------------------------------- *)
-
 (* ------------------------------------------------------------------------- *)
 (* AKS Parameter                                                             *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/AKS/compute/computePolyScript.sml b/examples/AKS/compute/computePolyScript.sml
@@ -12,27 +12,11 @@ val _ = new_theory "computePoly";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
-
-(* Get dependent theories local *)
-
-(* open dependent theories *)
-(* val _ = load "fieldInstancesTheory"; *)
-
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory helperListTheory;
-open pred_setTheory listTheory arithmeticTheory;
-
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open dividesTheory gcdTheory;
+open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory
+     combinatoricsTheory dividesTheory gcdTheory logrootTheory whileTheory;
 
 (* val _ = load "polyFieldModuloTheory"; *)
 open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
@@ -46,13 +30,10 @@ open ringBinomialTheory;
 
 (* val _ = load "computeOrderTheory"; *)
 open computeBasicTheory computeOrderTheory;
-open logrootTheory logPowerTheory;
-
-(* val _ = load "whileTheory"; *)
-open whileTheory;
-
-open rich_listTheory; (* for FRONT and LAST *)
 
+val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
+val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
+val _ = temp_overload_on("TWICE", ``\n. 2 * n``);
 
 (* ------------------------------------------------------------------------- *)
 (* Polynomial Computations Documentation                                     *)

diff --git a/examples/AKS/compute/computeRingScript.sml b/examples/AKS/compute/computeRingScript.sml
@@ -12,34 +12,11 @@ val _ = new_theory "computeRing";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
-
-(* Get dependent theories local *)
-
-(* open dependent theories *)
-(* val _ = load "fieldInstancesTheory"; *)
-
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory helperListTheory;
-open pred_setTheory listTheory arithmeticTheory;
-
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open dividesTheory gcdTheory;
-
-(*
-polyBinomial.hol  polyEval.hol    polyGCD.hol   polyRing.hol
-polyDerivative.hol  polyField.hol   polyIrreducible.hol polyRoot.hol
-polyDivides.hol   polyFieldDivision.hol polyMonic.hol   polyWeak.hol
-polyDivision.hol  polyFieldModulo.hol polyProduct.hol   polynomial.hol
-*)
+open pred_setTheory listTheory rich_listTheory arithmeticTheory numberTheory
+     combinatoricsTheory dividesTheory gcdTheory logrootTheory;
 
 (* val _ = load "polyFieldModuloTheory"; *)
 open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
@@ -53,11 +30,11 @@ open ringBinomialTheory;
 
 (* val _ = load "computePolyTheory"; *)
 open computeBasicTheory computeOrderTheory computePolyTheory;
-open logrootTheory logPowerTheory;
-
 open ringInstancesTheory;
-open rich_listTheory; (* for FRONT and LAST *)
 
+val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
+val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
+val _ = temp_overload_on("TWICE", ``\n. 2 * n``);
 
 (* ------------------------------------------------------------------------- *)
 (* Modulo Polynomial Computations in (ZN n) Ring Documentation               *)

diff --git a/examples/AKS/machine/Holmakefile b/examples/AKS/machine/Holmakefile
@@ -1,6 +1,4 @@
-PRE_INCLUDES = ../../algebra/ring
-
-ALGEBRA_INCLUDES = lib monoid group field polynomial finitefield
+ALGEBRA_INCLUDES = group ring field polynomial finitefield
 INCLUDES = $(patsubst %,../../algebra/%,$(ALGEBRA_INCLUDES)) \
            ../../simple_complexity/lib ../../simple_complexity/loop ../compute \
            $(HOLDIR)/src/monad/more_monads
diff --git a/examples/AKS/machine/countAKSScript.sml b/examples/AKS/machine/countAKSScript.sml
@@ -12,12 +12,12 @@ val _ = new_theory "countAKS";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)
+open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory
+     rich_listTheory listRangeTheory numberTheory combinatoricsTheory
+     logrootTheory pairTheory optionTheory primeTheory;
 
 (* Get dependent theories local *)
 (* val _ = load "countParamTheory"; *)
@@ -35,29 +35,11 @@ open bitsizeTheory complexityTheory;
 open loopIncreaseTheory loopDecreaseTheory;
 open loopDivideTheory loopListTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory helperListTheory;
-open helperFunctionTheory;
-
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open pred_setTheory listTheory arithmeticTheory;
-open dividesTheory gcdTheory;
-open rich_listTheory listRangeTheory;
-
-(* (* val _ = load "logPowerTheory"; *) *)
-open logrootTheory logPowerTheory;
-
-(* (* val _ = load "monadsyntax"; *) *)
 open monadsyntax;
-open pairTheory optionTheory;
 
 (* val _ = load "ringInstancesTheory"; *)
 open ringInstancesTheory; (* for ZN order *)
 
-(* val _ = load "computeAKSTheory"; *)
 open computeParamTheory computeAKSTheory;
 open computeBasicTheory; (* for power_free_check_eqn *)
 
@@ -70,6 +52,9 @@ open polynomialTheory polyWeakTheory;
 val _ = monadsyntax.enable_monadsyntax();
 val _ = monadsyntax.enable_monad "Count";
 
+val _ = temp_overload_on("SQ", ``\n. n * (n :num)``);
+val _ = temp_overload_on("HALF", ``\n. n DIV 2``);
+val _ = temp_overload_on("TWICE", ``\n. 2 * n``);
 
 (* ------------------------------------------------------------------------- *)
 (* AKS computations in monadic style Documentation                           *)