Renames in src/ring/src, freeing name "ring" for examples/algebra

HOL-Theorem-Prover · Jul 19, 2023 · 8726c99 · 8726c99 · binghe · Jul 20, 2023
1 parent e003580
commit 8726c99
Show file tree

Hide file tree

Showing 23 changed files with 77 additions and 108 deletions.
diff --git a/doc/next-release.md b/doc/next-release.md
@@ -202,6 +202,10 @@ Incompatibilities:
 
 *   The constant `lg` (logarithm with base 2) has moved from the `util_prob` theory to `transc`.
 
+*   The theories under `src/ring/src` have all been prefixed with the string `EVAL_` reflecting the way they are exclusively used within the system, to provide polynomial normalisation using reflection and `computeLib`.
+    This frees up the name `ring` to be used only by the material under `examples/algebra`.
+    (In the absence of this change, theories that depended on what was in `src/ring/src` could not be used in a development alongside what is in `examples/algebra`.)
+
 * * * * *
 
 <div class="footer">

diff --git a/src/integer/integerRingLib.sml b/src/integer/integerRingLib.sml
@@ -1,11 +1,6 @@
 structure integerRingLib :> integerRingLib =
 struct
 
-(*
-load "integerRingTheory";
-load "ringLib";
-*)
-
 open HolKernel Parse boolLib integerTheory integerRingTheory
 
 val num_to_int = intSyntax.int_injection;
@@ -16,10 +11,10 @@ fun is_closed_int t =
     (is_comb t andalso rator t ~~ num_to_int andalso
      numSyntax.is_numeral (rand t));
 
-val _ = ringLib.declare_ring
+val _ = EVAL_ringLib.declare_ring
     { RingThm = int_ring_thms,
       IsConst = is_closed_int,
-      Rewrites = [int_rewrites, numRingTheory.num_rewrites] };
+      Rewrites = [int_rewrites, EVAL_numRingTheory.num_rewrites] };
 
 (* dealing with subtraction: *)
 val PRE_CONV = REWRITE_CONV[int_sub]
@@ -29,8 +24,8 @@ val POST_CONV =
   REWRITE_CONV[GSYM INT_NEG_LMUL, GSYM int_sub]
 ;
 
-val INT_RING_CONV = PRE_CONV THENC ringLib.RING_CONV THENC POST_CONV;
-val INT_NORM_CONV = PRE_CONV THENC ringLib.RING_NORM_CONV THENC POST_CONV;
+val INT_RING_CONV = PRE_CONV THENC EVAL_ringLib.RING_CONV THENC POST_CONV;
+val INT_NORM_CONV = PRE_CONV THENC EVAL_ringLib.RING_NORM_CONV THENC POST_CONV;
 
 val INT_RING_TAC = CONV_TAC INT_RING_CONV
 val INT_NORM_TAC = CONV_TAC INT_NORM_CONV

diff --git a/src/integer/integerRingScript.sml b/src/integer/integerRingScript.sml
@@ -1,13 +1,4 @@
-(*
-load "ringLib";
-load "integerTheory";
-load "bossLib";
-*)
-
-open HolKernel Parse boolLib bossLib integerTheory ringTheory;
-
-infix THEN THENL THENC o;
-infix 8 by;
+open HolKernel Parse boolLib bossLib integerTheory EVAL_ringTheory;
 
 val _ = new_theory "integerRing";
 val _ = ParseExtras.temp_loose_equality()
@@ -22,7 +13,8 @@ ARW_TAC [ is_ring_def, ring_accessors, INT_0, INT_1,
           INT_ADD_ASSOC, INT_MUL_ASSOC, INT_ADD_LID, INT_MUL_LID] THEN
 MAP_FIRST MATCH_ACCEPT_TAC [ INT_ADD_SYM, INT_MUL_SYM ]);
 
-val int_ring_thms = ringLib.store_ring { Name = "int", Theory = int_is_ring };
+val int_ring_thms =
+  EVAL_ringLib.store_ring { Name = "int", Theory = int_is_ring }
 
 
 (* equations to put any expression build on + * ~ & int_0 int_1

diff --git a/src/rational/fracLib.sml b/src/rational/fracLib.sml
@@ -13,7 +13,7 @@ app load ["pairTheory", "pairLib", "integerTheory","intLib","intSyntax",
 open
         arithmeticTheory
         pairTheory pairLib integerTheory intLib intSyntax
-        ringLib integerRingTheory integerRingLib
+        EVAL_ringLib integerRingTheory integerRingLib
         intExtensionTheory intExtensionLib
         jbUtils fracTheory fracUtils fracSyntax;
 

diff --git a/src/rational/intExtensionLib.sml b/src/rational/intExtensionLib.sml
@@ -11,16 +11,10 @@ struct
 
 open HolKernel boolLib Parse bossLib;
 
-(* interactive mode
-app load ["pairTheory", "pairLib", "integerTheory","intLib",
-        "ringLib", "integerRingTheory","integerRingLib",
-        "fracTheory","fracUtils", "intExtensionTheory"];
-*)
-
 open
         arithmeticTheory
         pairTheory pairLib integerTheory intLib
-        ringLib integerRingTheory integerRingLib
+        EVAL_ringLib integerRingTheory integerRingLib
         intExtensionTheory;
 
 val ERR = mk_HOL_ERR "intExtensionLib"

diff --git a/src/rational/intExtensionScript.sml b/src/rational/intExtensionScript.sml
@@ -18,7 +18,7 @@ app load ["integerTheory","intLib",
 open
         arithmeticTheory pairTheory
         integerTheory intLib
-        ringTheory ringLib integerRingLib
+        EVAL_ringTheory EVAL_ringLib integerRingLib
         schneiderUtils;
 
 val _ = new_theory "intExtension";

diff --git a/src/rational/ratRingLib.sml b/src/rational/ratRingLib.sml
@@ -7,7 +7,7 @@ open HolKernel Parse boolLib;
 app load ["ringLib","ratTheory","ratRingTheory","ratLib"]
 *)
 
-open ringLib ratTheory ratRingTheory ratSyntax ratLib;
+open EVAL_ringLib ratTheory ratRingTheory ratSyntax ratLib;
 
 (*--------------------------------------------------------------------------
  * is_computable_frac, is_computable_rat

diff --git a/src/rational/ratRingScript.sml b/src/rational/ratRingScript.sml
@@ -14,7 +14,7 @@ app load [
 *)
 
 open
-        integerTheory ratTheory ringLib schneiderUtils;
+        integerTheory ratTheory EVAL_ringLib schneiderUtils;
 
 val _ = new_theory "ratRing";
 
@@ -23,17 +23,21 @@ val _ = new_theory "ratRing";
  *  |- is_ring (ring rat_0 rat_1 rat_add rat_mul rat_ainv)
  *--------------------------------------------------------------------------*)
 
-val RAT_IS_RING = store_thm("RAT_IS_RING",``is_ring (ring 0q 1q rat_add rat_mul rat_ainv)``,
-        RW_TAC intLib.int_ss[ ringTheory.is_ring_def, ringTheory.ring_accessors,
-                RAT_ADD_ASSOC, RAT_MUL_ASSOC,
-                RAT_ADD_LID, RAT_MUL_LID,
-                RAT_ADD_RINV,
-                RAT_RDISTRIB] THEN
-        MAP_FIRST MATCH_ACCEPT_TAC [
-                RAT_ADD_COMM, RAT_MUL_COMM
-                ] );
-
-val rat_ring_thms = ringLib.store_ring { Name = "rat", Theory = RAT_IS_RING };
+Theorem RAT_IS_RING: is_ring (ring 0q 1q rat_add rat_mul rat_ainv)
+Proof
+  RW_TAC intLib.int_ss[
+      EVAL_ringTheory.is_ring_def, EVAL_ringTheory.ring_accessors,
+      RAT_ADD_ASSOC, RAT_MUL_ASSOC,
+      RAT_ADD_LID, RAT_MUL_LID,
+      RAT_ADD_RINV,
+      RAT_RDISTRIB] THEN
+  MAP_FIRST MATCH_ACCEPT_TAC [
+      RAT_ADD_COMM, RAT_MUL_COMM
+    ]
+QED
+
+val rat_ring_thms =
+  EVAL_ringLib.store_ring { Name = "rat", Theory = RAT_IS_RING };
 
 (*==========================================================================
  * end of theory

diff --git a/src/rational/ratScript.sml b/src/rational/ratScript.sml
@@ -8,20 +8,11 @@
 
 open HolKernel boolLib Parse BasicProvers bossLib;
 
-(* interactive mode
-app load [
-        "integerTheory", "intLib",
-        "intExtensionTheory", "intExtensionLib",
-        "ringLib", "integerRingLib",
-        "fracTheory", "fracLib", "ratUtils", "jbUtils",
-        "quotient", "schneiderUtils"];
-*)
-
 open
         arithmeticTheory
         integerTheory intLib
         intExtensionTheory intExtensionLib
-        ringLib integerRingLib
+        EVAL_ringLib integerRingLib
         fracTheory fracLib ratUtils jbUtils
         quotient schneiderUtils;
 

diff --git a/src/ring/src/canonicalScript.sml → src/ring/src/EVAL_canonicalScript.sml b/src/ring/src/canonicalScript.sml → src/ring/src/EVAL_canonicalScript.sml
@@ -2,9 +2,9 @@ open HolKernel Parse boolLib;
 open BasicProvers Datatype;
 open abs_tools;
 
-val _ = new_theory "canonical";
+val _ = new_theory "EVAL_canonical";
 
-open ternaryComparisonsTheory quoteTheory;
+open ternaryComparisonsTheory EVAL_quoteTheory
 
 val sr = “sr:'a semi_ring”;
 val _ = set_assums [ “is_semi_ring ^sr” ];
@@ -14,10 +14,10 @@ val { plus_sym, plus_assoc, mult_sym, mult_assoc, distr_left,
       plus_permute, plus_rotate, mult_permute, mult_rotate, distr_right,
       plus_zero_left, plus_zero_right, mult_one_left, mult_one_right,
       mult_zero_left, mult_zero_right,... } =
-  semi_ringTheory.IMPORT
+  EVAL_semiringTheory.IMPORT
     { Vals = [sr],
       Inst = map ASSUME (get_assums()),
-      Rule = REWRITE_RULE[semi_ringTheory.semi_ring_accessors],
+      Rule = REWRITE_RULE[EVAL_semiringTheory.semi_ring_accessors],
       Rename = K NONE }
 ;
 

diff --git a/src/ring/src/numRingLib.sig → src/ring/src/EVAL_numRingLib.sig b/src/ring/src/numRingLib.sig → src/ring/src/EVAL_numRingLib.sig
@@ -1,4 +1,4 @@
-signature numRingLib =
+signature EVAL_numRingLib =
 sig
   include Abbrev
 

diff --git a/src/ring/src/numRingLib.sml → src/ring/src/EVAL_numRingLib.sml b/src/ring/src/numRingLib.sml → src/ring/src/EVAL_numRingLib.sml
@@ -1,18 +1,18 @@
-structure numRingLib :> numRingLib =
+structure EVAL_numRingLib :> EVAL_numRingLib =
 struct
 
-open boolLib numRingTheory; infix THENC;
+open boolLib EVAL_numRingTheory;
 
-val _ = ringLib.declare_ring
+val _ = EVAL_ringLib.declare_ring
     { RingThm = num_ring_thms,
       IsConst = numSyntax.is_numeral,
       Rewrites = [num_rewrites] };
 
 val NUM_RING_CONV = REWRITE_CONV [arithmeticTheory.ADD1]
-                        THENC ringLib.RING_CONV;
+                        THENC EVAL_ringLib.RING_CONV;
 
 val NUM_NORM_CONV = REWRITE_CONV [arithmeticTheory.ADD1]
-                      THENC ringLib.RING_NORM_CONV;
+                      THENC EVAL_ringLib.RING_NORM_CONV;
 
 val NUM_RING_TAC = CONV_TAC NUM_RING_CONV
 val NUM_NORM_TAC = CONV_TAC NUM_NORM_CONV;

diff --git a/src/ring/src/numRingScript.sml → src/ring/src/EVAL_numRingScript.sml b/src/ring/src/numRingScript.sml → src/ring/src/EVAL_numRingScript.sml
@@ -4,10 +4,10 @@ load "numeralTheory";
 load "bossLib";
 *)
 open HolKernel Parse boolLib bossLib
-     arithmeticTheory semi_ringTheory;
+     arithmeticTheory EVAL_semiringTheory;
 
 
-val _ = new_theory "numRing";
+val _ = new_theory "EVAL_numRing";
 
 (* num is a semi-ring: *)
 val num_semi_ring = store_thm
@@ -19,7 +19,7 @@ MATCH_ACCEPT_TAC MULT_SYM);
 
 
 val num_ring_thms =
-  ringLib.store_ring { Name = "num", Theory = num_semi_ring };
+  EVAL_ringLib.store_ring { Name = "num", Theory = num_semi_ring };
 
 
 local open numeralTheory in
@@ -30,9 +30,4 @@ val num_rewrites = save_thm("num_rewrites", LIST_CONJ
 end;
 
 
-(* Hack to avoid (semi_ring 0 1 $+ $* ) to be confused with an end
- * of comment.                      ^^^
- *)
-val _ = temp_overload_on("mult",“$* : num->num->num”);
-
 val _ = export_theory();
diff --git a/src/ring/src/quote.sig → src/ring/src/EVAL_quote.sig b/src/ring/src/quote.sig → src/ring/src/EVAL_quote.sig
@@ -1,4 +1,4 @@
-signature quote =
+signature EVAL_quote =
 sig
 
 include Abbrev

diff --git a/src/ring/src/quote.sml → src/ring/src/EVAL_quote.sml b/src/ring/src/quote.sml → src/ring/src/EVAL_quote.sml
@@ -1,12 +1,12 @@
-structure quote :> quote =
+structure EVAL_quote :> EVAL_quote =
 struct
 
-open HolKernel Parse boolLib quoteTheory;
+open HolKernel Parse boolLib EVAL_quoteTheory;
 
 structure Parse =
 struct
   open Parse
-  val (Type,Term) = parse_from_grammars quoteTheory.quote_grammars
+  val (Type,Term) = parse_from_grammars EVAL_quoteTheory.EVAL_quote_grammars
 end
 
 fun QUOTE_ERR function message =

diff --git a/src/ring/src/quoteScript.sml → src/ring/src/EVAL_quoteScript.sml b/src/ring/src/quoteScript.sml → src/ring/src/EVAL_quoteScript.sml
@@ -1,9 +1,7 @@
 open HolKernel Parse boolLib
      TotalDefn Datatype BasicProvers;
 
-infix THEN THENL;
-
-val _ = new_theory "quote";
+val _ = new_theory "EVAL_quote";
 
 open ternaryComparisonsTheory;
 

diff --git a/src/ring/src/ringLib.sig → src/ring/src/EVAL_ringLib.sig b/src/ring/src/ringLib.sig → src/ring/src/EVAL_ringLib.sig
@@ -1,4 +1,4 @@
-signature ringLib =
+signature EVAL_ringLib =
 sig
 
   include Abbrev

diff --git a/src/ring/src/ringLib.sml → src/ring/src/EVAL_ringLib.sml b/src/ring/src/ringLib.sml → src/ring/src/EVAL_ringLib.sml
@@ -1,12 +1,8 @@
-structure ringLib :> ringLib =
+structure EVAL_ringLib :> EVAL_ringLib =
 struct
 
-(*
-  app load ["ringNormTheory", "quote", "computeLib"];
-*)
-
-open HolKernel Parse boolLib ternaryComparisonsTheory quoteTheory quote
-     computeLib;
+open HolKernel Parse boolLib ternaryComparisonsTheory EVAL_quoteTheory
+     EVAL_quote computeLib;
 
 fun RING_ERR function message =
     HOL_ERR{origin_structure = "ringLib",
@@ -18,14 +14,14 @@ fun RING_ERR function message =
    between the semantic level operators and the syntactic level ones. *)
 
 fun ring_field q =
-  rhs(concl(REWRITE_CONV[ringTheory.ring_accessors] (Term q)));
+  rhs(concl(REWRITE_CONV[EVAL_ringTheory.ring_accessors] (Term q)));
 
 fun sring_field q =
-  rhs(concl(REWRITE_CONV[semi_ringTheory.semi_ring_accessors] (Term q)));
+  rhs(concl(REWRITE_CONV[EVAL_semiringTheory.semi_ring_accessors] (Term q)));
 
 fun inst_ty ty = inst [alpha |-> ty];
-local fun pmc s = prim_mk_const {Name = s, Thy = "ringNorm"}
-      fun canon_pmc s = prim_mk_const {Name = s, Thy = "canonical"}
+local fun pmc s = prim_mk_const {Name = s, Thy = "EVAL_ringNorm"}
+      fun canon_pmc s = prim_mk_const {Name = s, Thy = "EVAL_canonical"}
       val pvar = pmc "Pvar"
       val pcst = pmc "Pconst"
       val pplus = pmc "Pplus"
@@ -69,8 +65,8 @@ val find_type =
 fun is_ring_thm th =
   let val (Rator,Rand) = dest_comb (concl th) in
   case dest_thy_const Rator of
-    {Name="is_ring",Thy="ring",...} => true
-  | {Name="is_semi_ring", Thy="semi_ring",...} => false
+    {Name="is_ring",Thy="EVAL_ring",...} => true
+  | {Name="is_semi_ring", Thy="EVAL_semiring",...} => false
   | _ => raise RING_ERR "" ""
   end
   handle HOL_ERR _ => raise RING_ERR "is_ring" "mal-formed thm"
@@ -87,10 +83,10 @@ fun import_ring name th =
             canonical_sum_prod_def, canonical_sum_simplify_def,
             polynom_normalize_def, polynom_simplify_def,
             polynom_simplify_ok,... } =
-        ringNormTheory.IMPORT
+        EVAL_ringNormTheory.IMPORT
           { Vals = [ring],
             Inst = [th],
-            Rule = REWRITE_RULE[ringTheory.ring_accessors ],
+            Rule = REWRITE_RULE[EVAL_ringTheory.ring_accessors ],
             Rename = fn s => SOME(name^"_"^s) }
   in LIST_CONJ
     [ th,
@@ -115,10 +111,10 @@ fun import_semi_ring name th =
             canonical_sum_prod_def, canonical_sum_simplify_def,
             spolynom_normalize_def, spolynom_simplify_def,
             spolynomial_simplify_ok, ... } =
-        canonicalTheory.IMPORT
+        EVAL_canonicalTheory.IMPORT
           { Vals = [sring],
             Inst = [th],
-            Rule = REWRITE_RULE[semi_ringTheory.semi_ring_accessors ],
+            Rule = REWRITE_RULE[EVAL_semiringTheory.semi_ring_accessors ],
             Rename = fn s => SOME(name^"_"^s) }
   in LIST_CONJ
     [ th,