Fix examples/vector given changes in 562bb66

HOL-Theorem-Prover · Jun 3, 2024 · a103738 · a103738
1 parent 1253e33
commit a103738
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 10 deletions.
diff --git a/examples/vector/determinantScript.sml b/examples/vector/determinantScript.sml
@@ -13,14 +13,15 @@ open arithmeticTheory combinTheory pred_setTheory pairTheory boolTheory
      PairedLambda pred_setLib fcpTheory fcpLib tautLib numLib realTheory
      realLib InductiveDefinition hurdUtils cardinalTheory;
 
-open permutesTheory iterateTheory vectorTheory vectorLib matrixTheory;
+open permutesTheory iterateTheory vectorTheory vectorLib matrixTheory
+     real_sigmaTheory
 
 open Q;
 
 val _ = new_theory "determinant";
 
-Overload PRODUCT[local]  = “iterate$product”
-Overload SUM[local]      = “iterate$Sum”
+Overload PRODUCT[local]  = “real_sigma$product”
+Overload SUM[local]      = “real_sigma$Sum”
 Overload SWAP[local]     = “permutes$swap”
 Overload INVERSE[local]  = “permutes$inverse”
 Overload PERMUTES[local] = “permutes$permutes”
@@ -33,9 +34,9 @@ Overload COLUMN[local]   = “matrix$column”
 Overload COLUMNS[local]  = “matrix$columns”
 Overload VECTOR_0[local] = “vector$vec 0”
 
-val SUM_EQ       = iterateTheory.SUM_EQ';
-val SUM_EQ_0     = iterateTheory.SUM_EQ_0';
-val SUM_ADD      = iterateTheory.SUM_ADD';
+val SUM_EQ       = real_sigmaTheory.SUM_EQ';
+val SUM_EQ_0     = real_sigmaTheory.SUM_EQ_0';
+val SUM_ADD      = real_sigmaTheory.SUM_ADD';
 val SWAP_DEF     = permutesTheory.swap_def;
 val PERMUTES_DEF = permutesTheory.permutes;
 val VSUM_DEF     = vectorTheory.vsum_def;

diff --git a/examples/vector/matrixScript.sml b/examples/vector/matrixScript.sml
@@ -470,7 +470,7 @@ QED
 (* Slightly gruesome lemmas: better to define sums over vectors really...    *)
 (* ------------------------------------------------------------------------- *)
 
-Overload SUM[local] = “iterate$Sum”
+Overload SUM[local] = “real_sigma$Sum”
 Overload ADJOINT[local] = “adjoint”
 
 Theorem VECTOR_COMPONENTWISE :

diff --git a/examples/vector/vectorLib.sml b/examples/vector/vectorLib.sml
@@ -4,7 +4,7 @@ struct
 open HolKernel Parse boolLib bossLib;
 
 open pred_setTheory realTheory realLib iterateTheory RealArith fcpTheory fcpLib
-     tautLib vectorTheory;
+     tautLib vectorTheory real_sigmaTheory;
 
 (* tactics and decision procedures *)
 

diff --git a/examples/vector/vectorScript.sml b/examples/vector/vectorScript.sml
@@ -113,7 +113,7 @@ val _ = prefer_real();
 (* Infixl 600 is the same as "*", "INTER" and "*_c", etc. *)
 val _ = set_fixity "dot"  (Infixl 600); (* was: Infixr 20 (HOL-Light) *)
 
-Overload SUM[local] = “iterate$Sum”; (* see iterateTheory.sum_def *)
+Overload SUM[local] = “real_sigma$Sum”; (* see iterateTheory.sum_def *)
 
 (* NOTE: The original definition of ‘dot’ in HOL-Light is
 
@@ -140,7 +140,7 @@ QED
 (* A naive proof procedure to lift really trivial arithmetic stuff from R.   *)
 (* ------------------------------------------------------------------------- *)
 
-Theorem SUM_EQ[local] = iterateTheory.SUM_EQ'
+Theorem SUM_EQ[local] = real_sigmaTheory.SUM_EQ'
 
 val VECTOR_ARITH_TAC =
     rpt GEN_TAC