Algebra materials moved to core theories (up to monoid)

HOL-Theorem-Prover · Apr 21, 2024 · 6bd26f3 · 6bd26f3
1 parent 12c611b
commit 6bd26f3
Show file tree

Hide file tree

Showing 127 changed files with 53,027 additions and 52,544 deletions.
diff --git a/examples/algebra/Holmakefile b/examples/algebra/Holmakefile
@@ -1,2 +1,2 @@
 CLINE_OPTIONS = -r
-INCLUDES = lib monoid group ring field polynomial multipoly linear finitefield
+INCLUDES = group ring field polynomial multipoly linear finitefield
diff --git a/examples/algebra/aat/Holmakefile b/examples/algebra/aat/Holmakefile
@@ -1 +1 @@
-INCLUDES = ../monoid
+INCLUDES = $(HOLDIR)/src/algebra
diff --git a/examples/algebra/aat/aatmonoidScript.sml b/examples/algebra/aat/aatmonoidScript.sml
@@ -1,6 +1,6 @@
 open HolKernel Parse boolLib bossLib;
 
-open monoidTheory monoidOrderTheory transferTheory transferLib
+open monoidTheory transferTheory transferLib
 
 val _ = new_theory "aatmonoid";
 

diff --git a/examples/algebra/field/Holmakefile b/examples/algebra/field/Holmakefile
@@ -1,2 +1 @@
-PRE_INCLUDES = ../ring
-INCLUDES = ../lib ../monoid ../group
+INCLUDES = $(HOLDIR)/src/algebra ../ring ../group
diff --git a/examples/algebra/field/fieldBinomialScript.sml b/examples/algebra/field/fieldBinomialScript.sml
@@ -12,39 +12,23 @@ val _ = new_theory "fieldBinomial";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
 (* open dependent theories *)
-open pred_setTheory listTheory arithmeticTheory;
-
-(* val _ = load "binomialTheory"; *)
-open binomialTheory;
-open dividesTheory;
+open pred_setTheory listTheory arithmeticTheory numberTheory combinatoricsTheory
+     dividesTheory;
 
-(* Get dependent theories local *)
-(* (* val _ = load "groupTheory"; *) *)
-(* (* val _ = load "groupInstancesTheory"; *) *)
-(* (* val _ = load "ringTheory"; *) *)
-(* val _ = load "fieldMapTheory"; *)
 open fieldTheory;
 open ringTheory;
 open groupTheory;
 open monoidTheory;
 
-open monoidMapTheory groupMapTheory ringMapTheory fieldMapTheory;
+open groupMapTheory ringMapTheory fieldMapTheory;
 
 (* val _ = load "ringBinomialTheory"; *)
 open ringBinomialTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory;
-
-
 (* ------------------------------------------------------------------------- *)
 (* Field Binomial Documentation                                              *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/algebra/field/fieldIdealScript.sml b/examples/algebra/field/fieldIdealScript.sml
@@ -12,11 +12,12 @@ val _ = new_theory "fieldIdeal";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
+open pred_setTheory arithmeticTheory gcdsetTheory numberTheory
+     combinatoricsTheory;
+
 (* Get dependent theories local *)
 (* (* val _ = load "monoidTheory"; *) *)
 (* (* val _ = load "groupTheory"; *) *)
@@ -33,15 +34,6 @@ open ringIdealTheory quotientRingTheory;
 (* val _ = load "fieldTheory"; *)
 open fieldTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory;
-
-(* open dependent theories *)
-open pred_setTheory arithmeticTheory;
-
-
 (* ------------------------------------------------------------------------- *)
 (* Ideals in Field Documentation                                             *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/algebra/field/fieldInstancesScript.sml b/examples/algebra/field/fieldInstancesScript.sml
@@ -16,37 +16,21 @@ GF(p) -- Galois Field of order prime p.
 (* add all dependent libraries for script *)
 open HolKernel boolLib bossLib Parse;
 
+open pred_setTheory arithmeticTheory dividesTheory gcdTheory numberTheory
+     combinatoricsTheory;
+
 (* declare new theory at start *)
 val _ = new_theory "fieldInstances";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* Get dependent theories local *)
-(* (* val _ = load "groupTheory"; *) *)
-(* val _ = load "fieldMapTheory"; *)
 open monoidTheory groupTheory ringTheory fieldTheory;
-open groupOrderTheory monoidOrderTheory;
-
-open monoidMapTheory groupMapTheory ringMapTheory fieldMapTheory;
-
-(* val _ = load "ringInstancesTheory"; *)
-(* (* val _ = load "groupInstancesTheory"; -- in ringInstancesTheory *) *)
-open monoidInstancesTheory groupInstancesTheory ringInstancesTheory;
-
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory;
-
-(* open dependent theories *)
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open pred_setTheory arithmeticTheory dividesTheory gcdTheory;
-
+open groupOrderTheory;
+open groupMapTheory ringMapTheory fieldMapTheory;
+open groupInstancesTheory ringInstancesTheory;
 
 (* ------------------------------------------------------------------------- *)
 (* Field Instances Documentation                                              *)

diff --git a/examples/algebra/field/fieldMapScript.sml b/examples/algebra/field/fieldMapScript.sml
@@ -12,38 +12,24 @@ val _ = new_theory "fieldMap";
 
 (* ------------------------------------------------------------------------- *)
 
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* Get dependent theories local *)
-(* (* val _ = load "monoidTheory"; *) *)
-(* (* val _ = load "groupTheory"; *) *)
-(* (* val _ = load "ringTheory"; *) *)
-(* val _ = load "fieldOrderTheory"; *)
+open pred_setTheory arithmeticTheory dividesTheory gcdTheory gcdsetTheory
+     numberTheory combinatoricsTheory;
+
 open monoidTheory groupTheory;
-open monoidOrderTheory groupOrderTheory;
+open groupOrderTheory;
 open ringTheory ringUnitTheory integralDomainTheory;
 open fieldTheory fieldOrderTheory;
 
 (* val _ = load "ringDividesTheory"; *)
 open ringDividesTheory;
 
 (* val _ = load "ringMapTheory"; *)
-open monoidMapTheory groupMapTheory ringMapTheory;
+open groupMapTheory ringMapTheory;
 open quotientGroupTheory subgroupTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory;
-
-(* open dependent theories *)
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open pred_setTheory arithmeticTheory dividesTheory gcdTheory;
-
-
 (* ------------------------------------------------------------------------- *)
 (* Field Maps Documentation                                                  *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/algebra/field/fieldOrderScript.sml b/examples/algebra/field/fieldOrderScript.sml
@@ -12,40 +12,20 @@ val _ = new_theory "fieldOrder";
 
 (* ------------------------------------------------------------------------- *)
 
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
 (* open dependent theories *)
-open pred_setTheory listTheory arithmeticTheory;
+open pred_setTheory listTheory arithmeticTheory dividesTheory gcdTheory
+     gcdsetTheory numberTheory combinatoricsTheory primeTheory;
 
-(* Get dependent theories local *)
-(* (* val _ = load "groupTheory"; *) *)
-(* (* val _ = load "groupInstancesTheory"; *) *)
-(* (* val _ = load "ringTheory"; *) *)
-(* val _ = load "fieldTheory"; *)
 open fieldTheory;
 open integralDomainTheory;
 open ringTheory;
 open groupTheory;
 open monoidTheory;
 
-(* val _ = load "groupOrderTheory"; *)
-open monoidOrderTheory groupOrderTheory;
-open subgroupTheory;
-
-(* val _ = load "groupCyclicTheory"; *)
-open groupCyclicTheory;
-
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *)
-open helperNumTheory helperSetTheory helperFunctionTheory;
-open dividesTheory gcdTheory;
-
-open GaussTheory;
-
+open groupOrderTheory subgroupTheory groupCyclicTheory;
 
 (* ------------------------------------------------------------------------- *)
 (* Order of Elements in a Field Documentation                                *)

diff --git a/examples/algebra/field/fieldProductScript.sml b/examples/algebra/field/fieldProductScript.sml
@@ -12,23 +12,13 @@ val _ = new_theory "fieldProduct";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
 (* open dependent theories *)
-open pred_setTheory listTheory arithmeticTheory;
-
-(* val _ = load "binomialTheory"; *)
-open binomialTheory;
-open dividesTheory;
+open pred_setTheory listTheory arithmeticTheory dividesTheory numberTheory
+     combinatoricsTheory;
 
-(* Get dependent theories local *)
-(* (* val _ = load "groupTheory"; *) *)
-(* (* val _ = load "groupInstancesTheory"; *) *)
-(* (* val _ = load "ringTheory"; *) *)
-(* val _ = load "fieldTheory"; *)
 open fieldTheory;
 open ringTheory;
 open groupTheory;
@@ -38,12 +28,6 @@ open monoidTheory;
 open groupProductTheory;
 open subgroupTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory;
-
-
 (* ------------------------------------------------------------------------- *)
 (* Product of a set of Field elements Documentation                          *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/algebra/field/fieldRealScript.sml b/examples/algebra/field/fieldRealScript.sml
@@ -1,8 +1,10 @@
 (* ------------------------------------------------------------------------- *)
 (* The field of reals.                                                       *)
 (* ------------------------------------------------------------------------- *)
-open HolKernel boolLib bossLib Parse
-     groupTheory fieldTheory ringRealTheory groupRealTheory
+
+open HolKernel boolLib bossLib Parse;
+
+open groupTheory fieldTheory ringRealTheory groupRealTheory;
 
 val _ = new_theory"fieldReal";
 

diff --git a/examples/algebra/field/fieldScript.sml b/examples/algebra/field/fieldScript.sml
@@ -23,33 +23,19 @@ val _ = new_theory "field";
 
 (* ------------------------------------------------------------------------- *)
 
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* Get dependent theories local *)
-(* (* val _ = load "monoidTheory"; *) *)
-(* (* val _ = load "groupTheory"; *) *)
-(* (* val _ = load "ringTheory"; *) *)
-(* val _ = load "integralDomainTheory"; *)
+open pred_setTheory arithmeticTheory dividesTheory gcdTheory gcdsetTheory
+     numberTheory combinatoricsTheory;
+
 open monoidTheory groupTheory ringTheory ringUnitTheory integralDomainTheory;
-open monoidOrderTheory groupOrderTheory;
+open groupOrderTheory;
 open subgroupTheory; (* for field subgroups *)
 
 (* val _ = load "ringDividesTheory"; *)
 open ringDividesTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-open helperNumTheory helperSetTheory;
-
-(* open dependent theories *)
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open pred_setTheory arithmeticTheory dividesTheory gcdTheory;
-
-
 (* ------------------------------------------------------------------------- *)
 (* Field Documentation                                                       *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/algebra/field/fieldUnitScript.sml b/examples/algebra/field/fieldUnitScript.sml
@@ -12,8 +12,6 @@ val _ = new_theory "fieldUnit";
 
 (* ------------------------------------------------------------------------- *)
 
-
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
@@ -26,7 +24,6 @@ open pred_setTheory;
 open ringTheory fieldTheory;
 open ringDividesTheory ringUnitTheory;
 
-
 (* ------------------------------------------------------------------------- *)
 (* Field Units Documentation                                                 *)
 (* ------------------------------------------------------------------------- *)

diff --git a/examples/algebra/finitefield/Holmakefile b/examples/algebra/finitefield/Holmakefile
@@ -1,2 +1 @@
-PRE_INCLUDES = ../ring
-INCLUDES = ../lib ../monoid ../group ../field ../polynomial ../linear  
+INCLUDES = ../ring ../group ../field ../polynomial ../linear
diff --git a/examples/algebra/finitefield/ffAdvancedScript.sml b/examples/algebra/finitefield/ffAdvancedScript.sml
@@ -12,34 +12,19 @@ val _ = new_theory "ffAdvanced";
 
 (* ------------------------------------------------------------------------- *)
 
-
 (* val _ = load "jcLib"; *)
 open jcLib;
 
-(* Get dependent theories local *)
+(* open dependent theories *)
+open pred_setTheory arithmeticTheory dividesTheory gcdTheory numberTheory
+     combinatoricsTheory primeTheory;
 
 (* val _ = load "ffBasicTheory"; *)
 open ffBasicTheory;
 
 (* val _ = load "FiniteVSpaceTheory"; *)
 open VectorSpaceTheory FiniteVSpaceTheory;
 
-(* Get dependent theories in lib *)
-(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
-(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *)
-open helperNumTheory helperSetTheory helperFunctionTheory;
-
-(* open dependent theories *)
-open pred_setTheory arithmeticTheory;
-(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
-(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
-open dividesTheory gcdTheory;
-
-(* (* val _ = load "groupInstancesTheory"; -- in ringInstancesTheory *) *)
-(* (* val _ = load "ringInstancesTheory"; *) *)
-(* (* val _ = load "fieldInstancesTheory"; *) *)
-(* (* val _ = load "fieldTheory"; *) *)
 open monoidTheory groupTheory ringTheory fieldTheory;
 
 open groupInstancesTheory ringInstancesTheory;
@@ -57,22 +42,17 @@ open polyModuloRingTheory;
 open polyFieldModuloTheory;
 open polyIrreducibleTheory;
 
-open monoidMapTheory groupMapTheory ringMapTheory fieldMapTheory;
+open groupMapTheory ringMapTheory fieldMapTheory;
 open ringDividesTheory;
 open ringIdealTheory;
 open ringUnitTheory;
 open subgroupTheory;
 open quotientGroupTheory;
 
 open groupCyclicTheory;
-open monoidOrderTheory;
 open groupOrderTheory;
 open fieldOrderTheory;
 
-(* val _ = load "logPowerTheory"; *)
-open logPowerTheory; (* for perfect_power *)
-
-
 (* ------------------------------------------------------------------------- *)
 (* Finite Field Advanced Documentation                                       *)
 (* ------------------------------------------------------------------------- *)