Skip to content

Commit

Permalink
Remove some unused or redundant theorems from algebra/lib/helperNum
Browse files Browse the repository at this point in the history 
LESS_NOT_EQ causes most changes elsewhere as this is an alias for
prim_recTheory.LESS_NOT_EQ, so the other files pick up open-s of that
theory.
  • Loading branch information
@mn200
mn200 committed Nov 11, 2021
1 parent 4bf0acf commit 983ad16
Show file tree
Hide file tree
Showing 16 changed files with 24 additions and 315 deletions.
12 changes: 1 addition & 11 deletions examples/AKS/compute/computeParamScript.sml
View file
Expand Up @@ -12,36 +12,26 @@ val _ = new_theory "computeParam";

(* ------------------------------------------------------------------------- *)


(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)
(* val _ = load "computeOrderTheory"; *)
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 *)
(* (* 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 prim_recTheory pred_setTheory listTheory arithmeticTheory;
open dividesTheory gcdTheory;

(* (* val _ = load "GaussTheory"; *) *)
open GaussTheory; (* for phi_pos *)
(* (* val _ = load "EulerTheory"; *) *)
open EulerTheory; (* for residue_def *)
(* (* val _ = load "triangleTheory"; *) *)
open triangleTheory; (* for list_lcm_pos *)


Expand Down
17 changes: 1 addition & 16 deletions examples/AKS/theories/AKScleanScript.sml
View file
Expand Up @@ -12,16 +12,9 @@ val _ = new_theory "AKSclean";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)

(* val _ = load "AKSimprovedTheory"; *)
open AKSimprovedTheory;
open AKSrevisedTheory;
open AKStheoremTheory;
Expand All @@ -30,24 +23,18 @@ open AKSsetsTheory;
open AKSintroTheory;
open AKSshiftTheory;

(* val _ = load "countAKSTheory"; *)
open countAKSTheory; (* for aks0_eq_aks *)

(* open dependent theories *)
open pred_setTheory listTheory arithmeticTheory;
open prim_recTheory pred_setTheory listTheory arithmeticTheory;

(* 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 dividesTheory gcdTheory;
open logPowerTheory;

(* (* val _ = load "fieldInstancesTheory"; *) *)
open fieldInstancesTheory;
open ringInstancesTheory;
open groupInstancesTheory; (* for Estar_group *)
Expand All @@ -59,15 +46,13 @@ open polyRingModuloTheory; (* for poly_mod_ring_has_monomials *)
open polyFieldModuloTheory; (* for poly_mod_prod_group *)
open polyIrreducibleTheory; (* for poly_irreducible_poly *)

(* (* val _ = load "computeRingTheory"; *) *)
open computeBasicTheory;
open computeOrderTheory;
open computePolyTheory;
open computeRingTheory;
open computeParamTheory;
open computeAKSTheory;

(* (* val _ = load "GaussTheory"; *) *)
open GaussTheory; (* for phi_le *)


Expand Down
36 changes: 1 addition & 35 deletions examples/AKS/theories/AKSimprovedScript.sml
View file
Expand Up @@ -12,15 +12,9 @@ val _ = new_theory "AKSimproved";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)
(* val _ = load "AKSrevisedTheory"; *)
open AKSrevisedTheory;
open AKStheoremTheory;
open AKSmapsTheory;
Expand All @@ -29,36 +23,22 @@ open AKSintroTheory;
open AKSshiftTheory;

(* Get polynomial theory of Ring *)
(* (* val _ = load "polyWeakTheory"; *) *)
(* (* val _ = load "polyRingTheory"; *) *)
(* (* val _ = load "polyDivisionTheory"; *) *)
(* (* val _ = load "polyBinomialTheory"; *) *)
(* (* val _ = load "polyMapTheory"; *) *)
open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
open polyDivisionTheory polyBinomialTheory polyEvalTheory;

(* (* val _ = load "polyMonicTheory"; *) *)
open polyMonicTheory;

(* (* val _ = load "polyFieldTheory"; *) *)
(* (* val _ = load "polyFieldDivisionTheory"; *) *)
(* (* val _ = load "polyFieldModuloTheory"; *) *)
open polyFieldDivisionTheory;
open polyFieldModuloTheory;
open polyRingModuloTheory;
open polyIrreducibleTheory;
open polyMapTheory;

(* (* val _ = load "polyRootTheory"; *) *)
open polyRootTheory;
open polyDividesTheory;
open polyProductTheory;
open polyGCDTheory;

(* (* val _ = load "monoidTheory"; *) *)
(* (* val _ = load "groupTheory"; *) *)
(* (* val _ = load "ringTheory"; *) *)
(* (* val _ = load "ringUnitTheory"; *) *)
open monoidTheory groupTheory ringTheory fieldTheory;

open subgroupTheory;
Expand All @@ -68,51 +48,37 @@ open fieldMapTheory;
open ringUnitTheory;

(* open dependent theories *)
open pred_setTheory listTheory arithmeticTheory;
open prim_recTheory pred_setTheory listTheory arithmeticTheory;

(* 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 dividesTheory gcdTheory;

(* (* val _ = load "triangleTheory"; *) *)
(* (* val _ = load "binomialTheory"; *) *)
open triangleTheory;
open binomialTheory;

(* (* val _ = load "ringBinomialTheory"; *) *)
open ringBinomialTheory;
open ringDividesTheory;

(* (* val _ = load "fieldInstancesTheory"; *) *)
open monoidInstancesTheory;
open groupInstancesTheory;
open ringInstancesTheory;
open fieldInstancesTheory;
open groupOrderTheory;
open monoidOrderTheory;

(* (* val _ = load "groupCyclicTheory"; *) *)
open groupCyclicTheory;

(* (* val _ = load "fieldBinomialTheory"; *) *)
open fieldBinomialTheory;

(* (* val _ = load "fieldIdealTheory"; *) *)
open fieldIdealTheory;

(* (* val _ = load "fieldOrderTheory"; *) *)
open fieldOrderTheory;

(* (* val _ = load "fieldProductTheory"; *) *)
open fieldProductTheory;

(* val _ = load "computeAKSTheory"; *)
open logPowerTheory;
open computeBasicTheory;
open computeOrderTheory;
Expand Down
32 changes: 1 addition & 31 deletions examples/AKS/theories/AKSmapsScript.sml
View file
Expand Up @@ -12,52 +12,30 @@ val _ = new_theory "AKSmaps";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)
(* val _ = load "AKSsetsTheory"; *)
open AKSsetsTheory;
open AKSintroTheory;

(* For SQRT n and LOG2 n *)
(* val _ = load "logPowerTheory"; *)
open logPowerTheory;

(* (* val _ = load "monoidTheory"; *) *)
(* (* val _ = load "groupTheory"; *) *)
(* (* val _ = load "ringTheory"; *) *)
(* (* val _ = load "ringUnitTheory"; *) *)
open monoidTheory groupTheory ringTheory ringUnitTheory;

(* (* val _ = load "fieldTheory"; *) *)
open fieldTheory;

(* Get polynomial theory of Ring *)
(* (* val _ = load "polyWeakTheory"; *) *)
(* (* val _ = load "polyRingTheory"; *) *)
(* (* val _ = load "polyDivisionTheory"; *) *)
(* (* val _ = load "polyBinomialTheory"; *) *)
open polynomialTheory polyWeakTheory polyRingTheory polyDivisionTheory;
open polyBinomialTheory polyEvalTheory;

(* (* val _ = load "polyDividesTheory"; *) *)
open polyDividesTheory;
open polyMonicTheory;

(* (* val _ = load "polyRootTheory"; *) *)
open polyRootTheory;

(* (* val _ = load "polyProductTheory"; *) *)
open polyProductTheory;

(* (* val _ = load "polyFieldTheory"; *) *)
(* (* val _ = load "polyFieldDivisionTheory"; *) *)
(* (* val _ = load "polyFieldModuloTheory"; *) *)
open polyFieldTheory;
open polyFieldDivisionTheory;
open polyFieldModuloTheory;
Expand All @@ -69,31 +47,23 @@ open subgroupTheory;
open groupOrderTheory;

(* open dependent theories *)
open pred_setTheory listTheory arithmeticTheory;
open prim_recTheory pred_setTheory listTheory arithmeticTheory;

(* Get dependent theories in lib *)
(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *)
(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *)
open helperNumTheory helperSetTheory helperFunctionTheory;

(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *)
(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *)
open dividesTheory gcdTheory;

open GaussTheory; (* for phi_eq_0 *)

(* (* val _ = load "ringBinomialTheory"; *) *)
open binomialTheory;
open ringBinomialTheory;

(* (* val _ = load "fieldInstancesTheory"; *) *)
open monoidInstancesTheory;
open groupInstancesTheory;
open ringInstancesTheory;
open fieldInstancesTheory;

(* (* val _ = load "ffUnityTheory"; *) *)
open ffBasicTheory;
open ffAdvancedTheory;
open ffPolyTheory;
Expand Down
25 changes: 1 addition & 24 deletions examples/AKS/theories/AKSrevisedScript.sml
View file
Expand Up @@ -12,15 +12,9 @@ val _ = new_theory "AKSrevised";

(* ------------------------------------------------------------------------- *)



(* val _ = load "jcLib"; *)
open jcLib;

(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *)

(* Get dependent theories local *)
(* val _ = load "AKStheoremTheory"; *)
open AKStheoremTheory;
open AKSmapsTheory;
open AKSsetsTheory;
Expand All @@ -30,7 +24,6 @@ open logPowerTheory;
open computeParamTheory;

(* Get polynomial theory of Ring *)
(* (* val _ = load "polyMapTheory"; *) *)
open polynomialTheory polyWeakTheory polyRingTheory polyFieldTheory;
open polyDivisionTheory polyBinomialTheory polyEvalTheory;
open polyMonicTheory;
Expand All @@ -49,64 +42,48 @@ open fieldMapTheory;
open ringUnitTheory;

(* open dependent theories *)
open pred_setTheory listTheory arithmeticTheory;
open prim_recTheory pred_setTheory listTheory arithmeticTheory;

(* 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 dividesTheory gcdTheory;

(* (* val _ = load "triangleTheory"; *) *)
(* (* val _ = load "binomialTheory"; *) *)
open triangleTheory;
open binomialTheory;

(* (* val _ = load "ringBinomialTheory"; *) *)
open ringBinomialTheory;
open ringDividesTheory;

(* (* val _ = load "fieldInstancesTheory"; *) *)
open monoidInstancesTheory;
open groupInstancesTheory;
open ringInstancesTheory;
open fieldInstancesTheory;
open groupOrderTheory;
open monoidOrderTheory;

(* (* val _ = load "groupCyclicTheory"; *) *)
open groupCyclicTheory;

(* (* val _ = load "fieldBinomialTheory"; *) *)
open fieldBinomialTheory;

(* (* val _ = load "fieldIdealTheory"; *) *)
open fieldIdealTheory;

(* (* val _ = load "fieldOrderTheory"; *) *)
open fieldOrderTheory;

(* val _ = load "fieldProductTheory"; *)
open fieldProductTheory;

(* (* val _ = load "ffUnityTheory"; *) *)
open ffBasicTheory;
open ffAdvancedTheory;
open ffPolyTheory;
open ffUnityTheory;
open ffCycloTheory;

(* (* val _ = load "ffExistTheory"; *) *)
open ffExistTheory;
open ffConjugateTheory;
open ffMasterTheory;
open ffMinimalTheory;

(* (* val _ = load "GaussTheory"; *) *)
open GaussTheory;


Expand Down

0 comments on commit 983ad16

Please sign in to comment.