Enhanced INT_ARITH, INT_ARITH_TAC and ASM_INT_ARITH_TAC with better

reduction of constant-expressions and elimination of div and rem
analogous to that already present for DIV and MOD in the corresponding
natural number routines ARITH_RULE etc.

Added num-to-string conversions for arbitrary (<= 16) base and hex,
"string_of_num_nary" and "string_of_num_hex".

Added a few miscellaneous lemmas about numbers and machine words:

        BITVAL_MSB
        CONG_CASE
        INT_REM_LE
        INT_REM_LE_EQ
        INT_VAL_IWORD
        INT_VAL_IWORD_EQ
        INT_VAL_WORD_NEG
        PRIME_INT_DIVPROD_EQ
        REAL_VAL_WORD_NEG
        TWOS_COMPLEMENT

Removed a couple of effective duplicates with this renaming

        CONG_MOD_MULT -> CONG_DIVIDES_MODULUS
        INT_CONG_MOD_MULT -> INT_CONG_INT_DIVIDES_MODULUS

100/reciprocity.ml

@@ -398,7 +398,7 @@ let WILSON = prove
   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
   SUBGOAL_THEN `p divides FACT(n - 1) <=> p divides (n - 1)` SUBST1_TAC THENL
    [MATCH_MP_TAC CONG_DIVIDES THEN
-    MATCH_MP_TAC CONG_MOD_MULT THEN EXISTS_TAC `n:num` THEN
+    MATCH_MP_TAC CONG_DIVIDES_MODULUS THEN EXISTS_TAC `n:num` THEN
     ASM_REWRITE_TAC[];
     ALL_TAC] THEN
   DISCH_TAC THEN SUBGOAL_THEN `p divides 1` MP_TAC THENL

100/wilson.ml

@@ -176,7 +176,7 @@ let WILSON_EQ = prove
   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
   SUBGOAL_THEN `p divides FACT(n - 1) <=> p divides (n - 1)` SUBST1_TAC THENL
    [MATCH_MP_TAC CONG_DIVIDES THEN
-    MATCH_MP_TAC CONG_MOD_MULT THEN EXISTS_TAC `n:num` THEN
+    MATCH_MP_TAC CONG_DIVIDES_MODULUS THEN EXISTS_TAC `n:num` THEN
     ASM_REWRITE_TAC[];
     ALL_TAC] THEN
   DISCH_TAC THEN SUBGOAL_THEN `p divides 1` MP_TAC THENL

CHANGES

@@ -8,6 +8,112 @@
   * page: https://github.com/jrh13/hol-light/commits/master         *
   * *****************************************************************
 
+Tue 18th Jul 2023               Library/pocklington.ml, Library/integer.ml, 100/reciprocity.ml, 100/wilson.ml
+
+Removed a couple of effective duplicates with this renaming
+
+        CONG_MOD_MULT -> CONG_DIVIDES_MODULUS
+
+        INT_CONG_MOD_MULT -> INT_CONG_INT_DIVIDES_MODULUS
+
+Tue 18th Jul 2023               int.ml
+
+Enhanced INT_ARITH, INT_ARITH_TAC and ASM_INT_ARITH_TAC with better reduction
+of constant-expressions and elimination of div and rem analogous to that
+already present for DIV and MOD in the corresponding natural number routines
+ARITH_RULE etc. For example, the new version can handle basic lemmas like this:
+
+  let lemma = prove
+   (`abs(n) <= &2 pow 320
+     ==> let p = &2 pow 255 - &19 in
+         let q = n div &2 pow 255 in
+         let q' = if q < &0 then q - &1 else q in
+         &0 <= n - q' * p /\ n - q' * p < &2 * p`,
+  REWRITE_TAC[LET_DEF; LET_END_DEF] THEN INT_ARITH_TAC);;
+
+Mon 17th Jul 2023               lib.ml
+
+Added two trivial but handy functions to convert an integer into a
+hex string (string_of_num_hex), or a string to any base <= 16
+(string_of_num_nary), e.g.
+
+  # string_of_num_nary 2 (Int 255);;
+  val it : string = "11111111"
+  # string_of_num_nary 16 (Int 255);;
+  val it : string = "ff"
+  # string_of_num_nary 10 (Int 255);;
+  val it : string = "255"
+  #  string_of_num_hex (Int 126);;
+  val it : string = "0x7e"
+
+Mon 17th Jul 2023               Help/passim, help.ml, doc-to-help.sed
+
+Renamed all the ".doc" documentation files (used by "help" as well as
+in autogeneration of HTML and LaTeX reference documentation) to have
+the ".hlp" extension instead. This avoids complaints from tools that
+make assumptions about file type based on the extension.
+
+Thu 13th Jun 2023               Library/words.ml
+
+Added a few more miscellaneous word theorems. TWOS_COMPLEMENT is only
+really word-specific in its use of the bitval constant, but anyway is
+intended for word-oriented applications.
+
+  BITVAL_MSB =
+    |- !x. bitval(bit (dimindex(:N) - 1) x) =
+           val x DIV 2 EXP (dimindex(:N) - 1)
+
+  INT_VAL_IWORD =
+    |- !x. &0 <= x /\ x < &2 pow dimindex(:N) ==> &(val(iword x)) = x
+
+  INT_VAL_IWORD_EQ =
+    |- !x. &(val(iword x)) = x <=> &0 <= x /\ x < &2 pow dimindex(:N)
+
+  INT_VAL_WORD_NEG =
+    |- !x. &(val(word_neg x)) =
+           &2 pow dimindex(:N) * &(bitval(~(x = word 0))) - &(val x)
+
+  REAL_VAL_WORD_NEG =
+    |- !x. &(val(word_neg x)) =
+           &2 pow dimindex(:N) * &(bitval(~(x = word 0))) - &(val x)
+
+  TWOS_COMPLEMENT =
+    |- !p n x.
+           (&n == x) (mod (&2 pow p)) /\
+           ~(p = 0) /\
+           n < 2 EXP p /\
+           --(&2 pow (p - 1)) <= x /\
+           x < &2 pow (p - 1)
+           ==> (2 EXP (p - 1) <= n <=> x < &0) /\
+               n DIV 2 EXP (p - 1) = bitval(x < &0) /\
+               &n - &2 pow p * &(bitval(x < &0)) = x
+
+Wed 12th Jul 2023               int.ml
+
+Added a couple of lemmas about bounding integer remainders in terms of
+a bound on the left hand argument, a trivial but occasionally useful
+case:
+
+  INT_REM_LE =
+    |- !m n p. (n = &0 \/ &0 <= m) /\ m <= p ==> m rem n <= p
+
+  INT_REM_LE_EQ =
+    |- !m n. m rem n <= m <=> n = &0 \/ &0 <= m
+
+Tue 20th Jun 2023               Library/prime.ml, Library/pocklington.ml
+
+Added a couple of simple lemmas that both, in slightly different ways,
+help to work around the inconvenience of congruences on N with limited
+support for subtraction, one by switching into Z and one by eliminating
+an ostensible case split:
+
+  PRIME_INT_DIVPROD_EQ =
+    |- !p a b.
+          prime p ==> (&p divides a * b <=> &p divides a \/ &p divides b)
+
+  CONG_CASE =
+    |- !n a x. a < n ==> ((x == a) (mod n) <=> ?q. x = q * n + a)
+
 Wed 24th May 2023               Divstep/idivstep.ml [new file], divstep_bounds.ml
 
 Added an integer-scaled version of "divstep", which scales the delta by a

Library/integer.ml

@@ -740,10 +740,6 @@ let INT_COPRIME_LREM = prove
  (`!a b. coprime(a rem n,n) <=> coprime(a,n)`,
   MESON_TAC[INT_COPRIME_RREM; INT_COPRIME_SYM]);;
 
-let INT_CONG_MOD_MULT = prove
- (`!x y m n. (x == y) (mod n) /\ m divides n ==> (x == y) (mod m)`,
-  INTEGER_TAC);;
-
 let INT_CONG_GCD_RIGHT = prove
  (`!x y n. (x == y) (mod n) ==> gcd(n,x) = gcd(n,y)`,
   REWRITE_TAC[INT_GCD_UNIQUE; INT_GCD_POS] THEN INTEGER_TAC);;

Library/pocklington.ml

@@ -129,6 +129,13 @@ let CONG_CASES = prove
    `x + a = y + b ==> x = (b - a) + y \/ y = (a - b) + x`)) THEN
   REWRITE_TAC[GSYM LEFT_SUB_DISTRIB] THEN MESON_TAC[MULT_SYM]);;
 
+let CONG_CASE = prove
+ (`!n a x:num. a < n ==> ((x == a) (mod n) <=> ?q. x = q * n + a)`,
+  REPEAT STRIP_TAC THEN REWRITE_TAC[CONG_CASES; OR_EXISTS_THM] THEN
+  EQ_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[] THEN
+  MATCH_MP_TAC num_INDUCTION THEN SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
+  ASM_ARITH_TAC);;
+
 let CONG_MULT_LCANCEL = prove
  (`!a n x y. coprime(a,n) /\ (a * x == a * y) (mod n) ==> (x == y) (mod n)`,
   NUMBER_TAC);;
@@ -298,10 +305,6 @@ let MOD_MULT_CONG = prove
   MATCH_MP_TAC CONG_DIVIDES_MODULUS THEN EXISTS_TAC `a * b` THEN
   ASM_SIMP_TAC[CONG_MOD; MULT_EQ_0; DIVIDES_RMUL; DIVIDES_REFL]);;
 
-let CONG_MOD_MULT = prove
- (`!x y m n. (x == y) (mod n) /\ m divides n ==> (x == y) (mod m)`,
-  NUMBER_TAC);;
-
 let CONG_MOD_LT = prove
  (`!y. y < n ==> (x MOD n = y <=> (x == y) (mod n))`,
   MESON_TAC[MOD_LT; CONG; LT]);;

Library/prime.ml

@@ -650,6 +650,13 @@ let PRIME_DIVPROD_EQ = prove
  (`!p a b. prime(p) ==> (p divides (a * b) <=> p divides a \/ p divides b)`,
   MESON_TAC[PRIME_DIVPROD; DIVIDES_LMUL; DIVIDES_RMUL]);;
 
+let PRIME_INT_DIVPROD_EQ = prove
+ (`!p a b:int.
+        prime p ==> (&p divides a * b <=> &p divides a \/ &p divides b)`,
+  REWRITE_TAC[FORALL_INT_CASES; INT_MUL_LNEG; INT_MUL_RNEG; INT_NEG_NEG] THEN
+  REWRITE_TAC[INTEGER_RULE `(a:int) divides --b <=> a divides b`] THEN
+  REWRITE_TAC[GSYM num_divides; PRIME_DIVPROD_EQ; INT_OF_NUM_CLAUSES]);;
+
 let PRIME_GE_2 = prove
  (`!p. prime(p) ==> 2 <= p`,
   REWRITE_TAC[ARITH_RULE `2 <= p <=> ~(p = 0) /\ ~(p = 1)`] THEN

Library/words.ml

@@ -746,6 +746,18 @@ let MSB_INT_VAL = prove
     bit (dimindex(:N) - 1) w <=> (&2 pow (dimindex(:N) - 1)):int <= &(val w)`,
   REWRITE_TAC[INT_OF_NUM_POW; INT_OF_NUM_LE; MSB_VAL]);;
 
+let BITVAL_MSB = prove
+ (`!x:N word. bitval(bit (dimindex(:N)-1) x) =
+              val x DIV 2 EXP (dimindex(:N)-1)`,
+  GEN_TAC THEN REWRITE_TAC[MSB_VAL] THEN CONV_TAC SYM_CONV THEN
+  REWRITE_TAC[bitval] THEN COND_CASES_TAC THENL
+   [MATCH_MP_TAC(ARITH_RULE `n < 2 /\ ~(n = 0) ==> n = 1`); ALL_TAC] THEN
+  ASM_SIMP_TAC[DIV_EQ_0; EXP_EQ_0; ARITH_EQ; RDIV_LT_EQ] THEN
+  ASM_REWRITE_TAC[GSYM NOT_LE] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
+  SIMP_TAC[GSYM(CONJUNCT2 EXP); NOT_LE] THEN
+  SIMP_TAC[DIMINDEX_NONZERO; ARITH_RULE `~(n = 0) ==> SUC(n - 1) = n`] THEN
+  REWRITE_TAC[VAL_BOUND]);;
+
 let BLOCK_BITS_ZERO_ALT = prove
  (`!(x:N word) m n.
         (!i. m <= i /\ i < n ==> ~bit i x) <=>
@@ -943,6 +955,18 @@ let VAL_IVAL = prove
     ival w + &2 pow dimindex(:N) * &(bitval (bit (dimindex (:N) - 1) w))`,
   REWRITE_TAC[IVAL_VAL] THEN CONV_TAC INT_ARITH);;
 
+let INT_VAL_IWORD = prove
+ (`!x. &0 <= x /\ x < &2 pow dimindex(:N) ==> &(val(iword x:N word)) = x`,
+  SIMP_TAC[IMP_CONJ; GSYM INT_FORALL_POS] THEN
+  REWRITE_TAC[GSYM WORD_IWORD; INT_OF_NUM_CLAUSES; VAL_WORD_EQ]);;
+
+let INT_VAL_IWORD_EQ = prove
+ (`!x. &(val(iword x:N word)) = x <=>
+       &0 <= x /\ x < &2 pow dimindex(:N)`,
+  GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[INT_VAL_IWORD] THEN
+  DISCH_THEN(SUBST1_TAC o SYM) THEN
+  REWRITE_TAC[INT_OF_NUM_CLAUSES; LE_0; VAL_BOUND]);;
+
 let MSB_IVAL = prove
  (`!(w:N word).
         bit (dimindex(:N) - 1) w <=> ival w < &0`,
@@ -1188,6 +1212,34 @@ let BIT_LSB_IWORD = prove
   REWRITE_TAC[divides; GSYM EVEN_EXISTS] THEN
   REWRITE_TAC[EVEN_EXP; ARITH; DIMINDEX_NONZERO]);;
 
+let TWOS_COMPLEMENT = prove
+ (`!p n x:int.
+        (&n == x) (mod (&2 pow p)) /\
+        ~(p = 0) /\ n < 2 EXP p /\
+        --(&2 pow (p - 1)) <= x /\ x < &2 pow (p - 1)
+        ==> (2 EXP (p - 1) <= n <=> x < &0) /\
+            n DIV (2 EXP (p - 1)) = bitval(x < &0) /\
+            &n - &2 pow p * &(bitval(x < &0)) = x`,
+  MATCH_MP_TAC num_INDUCTION THEN REWRITE_TAC[] THEN
+  X_GEN_TAC `p:num` THEN DISCH_THEN(K ALL_TAC) THEN
+  REWRITE_TAC[NOT_SUC; EXP; SUC_SUB1; INT_POW] THEN
+  REPEAT GEN_TAC THEN STRIP_TAC THEN
+  SUBGOAL_THEN `n DIV 2 EXP p < 2` ASSUME_TAC THENL
+   [ASM_SIMP_TAC[RDIV_LT_EQ; EXP_EQ_0; ARITH_EQ] THEN ASM_ARITH_TAC;
+    ALL_TAC] THEN
+  REWRITE_TAC[bitval] THEN COND_CASES_TAC THEN
+  ASM_SIMP_TAC[ARITH_RULE `n < 2 ==> (n = 1 <=> ~(n = 0))`] THEN
+  SIMP_TAC[DIV_EQ_0; EXP_EQ_0; ARITH_EQ; NOT_LE; NOT_LT; CONJ_ASSOC] THEN
+  REWRITE_TAC[INT_MUL_RZERO; INT_MUL_RID; INT_EQ_SUB_RADD] THEN
+  MATCH_MP_TAC(TAUT `(q ==> p) /\ q ==> p /\ q`) THEN
+  (CONJ_TAC THENL
+    [SIMP_TAC[GSYM INT_OF_NUM_CLAUSES];
+     MATCH_MP_TAC INT_CONG_IMP_EQ THEN EXISTS_TAC `(&2:int) * &2 pow p` THEN
+     ASM_REWRITE_TAC[INT_ADD_RID; INTEGER_RULE
+      `(x:int == y + n) (mod n) <=> (x == y) (mod n)`]]) THEN
+  RULE_ASSUM_TAC(REWRITE_RULE[GSYM INT_OF_NUM_CLAUSES]) THEN
+  ASM_INT_ARITH_TAC);;
+
 (* ------------------------------------------------------------------------- *)
 (* Bit operations on `num`.                                                  *)
 (* ------------------------------------------------------------------------- *)
@@ -2214,6 +2266,24 @@ let REAL_VAL_WORD_NEG_CASES = prove
   SIMP_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_SUB; LT_IMP_LE; VAL_BOUND] THEN
   REWRITE_TAC[VAL_WORD_NEG_CASES; REAL_OF_NUM_EQ] THEN MESON_TAC[]);;
 
+let INT_VAL_WORD_NEG = prove
+ (`!x:N word. &(val(word_neg x)):int =
+              &2 pow dimindex(:N) * &(bitval(~(x = word 0))) -
+              &(val x)`,
+  GEN_TAC THEN REWRITE_TAC[INT_VAL_WORD_NEG_CASES] THEN
+  REWRITE_TAC[INT_OF_NUM_EQ; VAL_EQ_0] THEN
+  COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES; VAL_WORD_0] THEN
+  INT_ARITH_TAC);;
+
+let REAL_VAL_WORD_NEG = prove
+ (`!x:N word. &(val(word_neg x)):real =
+              &2 pow dimindex(:N) * &(bitval(~(x = word 0))) -
+              &(val x)`,
+  GEN_TAC THEN REWRITE_TAC[REAL_VAL_WORD_NEG_CASES] THEN
+  REWRITE_TAC[REAL_OF_NUM_EQ; VAL_EQ_0] THEN
+  COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES; VAL_WORD_0] THEN
+  REAL_ARITH_TAC);;
+
 let CONG_WORD_NEG = prove
  (`!x:(N)word.
         (val(word_neg x) + val x == 0) (mod (2 EXP dimindex(:N)))`,

database.ml

@@ -1230,6 +1230,8 @@ theorems :=
 "INT_REM_EQ",INT_REM_EQ;
 "INT_REM_EQ_0",INT_REM_EQ_0;
 "INT_REM_EQ_SELF",INT_REM_EQ_SELF;
+"INT_REM_LE",INT_REM_LE;
+"INT_REM_LE_EQ",INT_REM_LE_EQ;
 "INT_REM_LNEG",INT_REM_LNEG;
 "INT_REM_LT",INT_REM_LT;
 "INT_REM_MOD_SELF",INT_REM_MOD_SELF;