Added a few more word and arithmetic lemmas:

        INT_REM_UNIQUE
        WORD_SHL_SUBWORD
        WORD_SUBWORD_AS_USHR
        WORD_UMAX
        WORD_UMAX_SYM
        WORD_UMAX_ASSOC
        WORD_UMIN
        WORD_UMIN_SYM
        WORD_UMIN_ASSOC
        WORD_USHR_AS_SUBWORD

CHANGES

@@ -8,6 +8,52 @@
   * page: https://github.com/jrh13/hol-light/commits/master         *
   * *****************************************************************
 
+Wed  9th Oct 2021       int.ml
+
+Added a natural integer analog of MOD_UNIQUE:
+
+  INT_REM_UNIQUE =
+    |- !m n p.
+         m rem n = p <=>
+         (n = &0 /\ m = p \/ &0 <= p /\ p < abs n) /\ (m == p) (mod n)
+
+Tue  8th Oct 2021       Library/words.ml
+
+Added a few trivial theorems about unsigned word max/min:
+
+  WORD_UMAX =
+    |- !x y. word_umax x y = (if val x <= val y then y else x)
+
+  WORD_UMAX_ASSOC =
+    |- !x y z. word_umax x (word_umax y z) = word_umax (word_umax x y) z
+
+  WORD_UMAX_SYM =
+    |- !x y. word_umax x y = word_umax y x
+
+  WORD_UMIN =
+    |- !x y. word_umin x y = (if val x <= val y then x else y)
+
+  WORD_UMIN_ASSOC =
+    |- !x y z. word_umin x (word_umin y z) = word_umin (word_umin x y) z
+
+  WORD_UMIN_SYM =
+    |- !x y. word_umin x y = word_umin y x
+
+Fri 20th Aug 2021       Library/words.ml
+
+Added three more word lemmas connecting shifts and subwords:
+
+  WORD_SHL_SUBWORD =
+    |- !x d l.
+           dimindex(:N) <= l + d
+           ==> word_shl (word_subword x (0,l)) d = word_shl x d
+
+  WORD_SUBWORD_AS_USHR =
+    |- !x k l. dimindex(:N) <= k + l ==> word_subword x (k,l) = word_ushr x k
+
+  WORD_USHR_AS_SUBWORD =
+    |- !x k. word_ushr x k = word_subword x (k,dimindex(:N) - k)
+
 Fri 30th Jul 2021       Library/words.ml
 
 Made the trivial generalization to WORD_ARITH / WORD_ARITH_TAC of also

Library/words.ml

@@ -1992,6 +1992,19 @@ let VAL_WORD_UMAX = prove
   REWRITE_TAC[ARITH_RULE `MAX x y < n <=> x < n /\ y < n`] THEN
   REWRITE_TAC[VAL_BOUND]);;
 
+let WORD_UMAX = prove
+ (`!x y:N word. word_umax x y = if val x <= val y then y else x`,
+  REPEAT GEN_TAC THEN COND_CASES_TAC THEN
+  ASM_REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_UMAX; MAX]);;
+
+let WORD_UMAX_SYM = prove
+ (`!x y:N word. word_umax x y = word_umax y x`,
+  REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_UMAX] THEN ARITH_TAC);;
+
+let WORD_UMAX_ASSOC = prove
+ (`!x y z:N word. word_umax x (word_umax y z) = word_umax (word_umax x y) z`,
+  REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_UMAX] THEN ARITH_TAC);;
+
 let IVAL_WORD_IMAX = prove
  (`!x y:(N)word.
         ival(word_imax x y) = max (ival x) (ival y)`,
@@ -2013,6 +2026,19 @@ let VAL_WORD_UMIN = prove
   REWRITE_TAC[ARITH_RULE `MIN x y < n <=> x < n \/ y < n`] THEN
   REWRITE_TAC[VAL_BOUND]);;
 
+let WORD_UMIN = prove
+ (`!x y:N word. word_umin x y = if val x <= val y then x else y`,
+  REPEAT GEN_TAC THEN COND_CASES_TAC THEN
+  ASM_REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_UMIN; MIN]);;
+
+let WORD_UMIN_SYM = prove
+ (`!x y:N word. word_umin x y = word_umin y x`,
+  REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_UMIN] THEN ARITH_TAC);;
+
+let WORD_UMIN_ASSOC = prove
+ (`!x y z:N word. word_umin x (word_umin y z) = word_umin (word_umin x y) z`,
+  REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_UMIN] THEN ARITH_TAC);;
+
 let IVAL_WORD_IMIN = prove
  (`!x y:(N)word.
         ival(word_imin x y) = min (ival x) (ival y)`,
@@ -3076,6 +3102,31 @@ let WORD_SUBWORD_JOIN_AS_SHL = prove
    [REWRITE_TAC[GSYM EXP_ADD] THEN AP_TERM_TAC THEN ASM_ARITH_TAC;
     SIMP_TAC[GSYM MULT_ASSOC; DIV_MULT; EXP_EQ_0; ARITH_EQ]]);;
 
+let WORD_SUBWORD_AS_USHR = prove
+ (`!(x:N word) k l.
+        dimindex(:N) <= k + l ==> word_subword x (k,l) = word_ushr x k`,
+  REPEAT STRIP_TAC THEN REWRITE_TAC[word_subword; word_ushr] THEN
+  AP_TERM_TAC THEN MATCH_MP_TAC MOD_LT THEN
+  SIMP_TAC[RDIV_LT_EQ; EXP_EQ_0; ARITH_EQ; GSYM EXP_ADD] THEN
+  W(MP_TAC o PART_MATCH lhand VAL_BOUND o lhand o snd) THEN
+  MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] LTE_TRANS) THEN
+  ASM_REWRITE_TAC[LE_EXP] THEN ARITH_TAC);;
+
+let WORD_USHR_AS_SUBWORD = prove
+ (`!(x:N word) k. word_ushr x k = word_subword x (k,dimindex (:N) - k)`,
+  REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
+  MATCH_MP_TAC WORD_SUBWORD_AS_USHR THEN ARITH_TAC);;
+
+let WORD_SHL_SUBWORD = prove
+ (`!(x:N word) d l.
+        dimindex(:N) <= l + d
+        ==> word_shl (word_subword x (0,l)) d = word_shl x d`,
+  REPEAT STRIP_TAC THEN REWRITE_TAC[word_shl; word_subword] THEN
+  REWRITE_TAC[GSYM VAL_EQ; VAL_WORD; EXP; DIV_1] THEN
+  CONV_TAC MOD_DOWN_CONV THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
+  REWRITE_TAC[GSYM MOD_MULT2; GSYM EXP_ADD; MOD_MOD_EXP_MIN] THEN
+  ASM_SIMP_TAC[ARITH_RULE `n <= l + d ==> MIN (d + l) n = n`]);;
+
 let WORD_SUBWORD_AND = prove
  (`!(x:M word) y pos len.
         word_subword (word_and x y) (pos,len) :N word =

database.ml

@@ -1213,6 +1213,7 @@ theorems :=
 "INT_REM_REM_MUL",INT_REM_REM_MUL;
 "INT_REM_RNEG",INT_REM_RNEG;
 "INT_REM_UNIQ",INT_REM_UNIQ;
+"INT_REM_UNIQUE",INT_REM_UNIQUE;
 "INT_REM_ZERO",INT_REM_ZERO;
 "INT_RNEG_UNIQ",INT_RNEG_UNIQ;
 "INT_SGN",INT_SGN;

int.ml

@@ -1577,6 +1577,17 @@ let INT_REM_EQ_SELF = prove
   REWRITE_TAC[INT_REM_DIV; INT_ARITH `m - x:int = m <=> x = &0`] THEN
   REWRITE_TAC[INT_DIV_EQ_0; INT_ENTIRE] THEN INT_ARITH_TAC);;
 
+let INT_REM_UNIQUE = prove
+ (`!m n p. m rem n = p <=>
+           (n = &0 /\ m = p \/ &0 <= p /\ p < abs n) /\ (m == p) (mod n)`,
+  REPEAT GEN_TAC THEN ASM_CASES_TAC `n:int = &0` THENL
+   [ASM_REWRITE_TAC[INT_REM_0; INT_ABS_0; INT_LET_ANTISYM] THEN
+    CONV_TAC INTEGER_RULE;
+    EQ_TAC THENL
+     [DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_SIMP_TAC[INT_DIVISION] THEN
+      REWRITE_TAC[GSYM INT_REM_EQ; INT_REM_REM];
+      ASM_SIMP_TAC[GSYM INT_REM_EQ; INT_REM_EQ_SELF]]]);;
+
 let INT_DIV_REM = prove
  (`!m n p. &0 <= n ==> (m div n) rem p = (m rem (n * p)) div n`,
   REPEAT GEN_TAC THEN ASM_CASES_TAC `n:int = &0` THEN