Add new definition: word_exp

Includes a more-efficient-to-eval tail-recursive version as well as a
straightforward recursive version.

src/n-bit/wordsLib.sml

@@ -376,6 +376,7 @@ local
       Q.SPEC `^n2w n` reduce_or, reduce_xor_def, reduce_xnor_def,
       reduce_nand_def, reduce_nor_def,
       Q.SPECL [`^Na`, `^n2w n`] word_sign_extend_def,
+      word_exp_tailrec, word_exp_tailrec_def,
       word_ge_n2w, word_gt_n2w, word_hi_n2w, word_hs_n2w,
       word_le_n2w, word_lo_n2w, word_ls_n2w, word_lt_n2w,
       l2w_def, w2l_def, s2w_def, w2s_def, add_with_carry_def,

src/n-bit/wordsScript.sml

@@ -9,6 +9,7 @@ open HolKernel Parse boolLib bossLib;
 open arithmeticTheory pred_setTheory
 open bitTheory sum_numTheory fcpTheory fcpLib
 open numposrepTheory ASCIInumbersTheory
+open dividesTheory dep_rewrite
 
 val () = new_theory "words"
 val _ = set_grammar_ancestry ["ASCIInumbers", "numeral_bit", "fcp", "sum_num"]
@@ -4922,6 +4923,145 @@ val WORD_SUB_LE = Q.store_thm("WORD_SUB_LE",
   `!x:'a word y. 0w <= y /\ y <= x ==> 0w <= x - y /\ x - y <= x`,
   SIMP_TAC bool_ss [WORD_LE_SUB_UPPER,WORD_ZERO_LE_SUB])
 
+(* word_exp *)
+
+Definition word_exp_def:
+  word_exp (b: 'a word) (e: 'a word) =
+  if e = 0w then 1w else
+  if word_mod e 2w = 0w then
+    let x = word_exp b (word_div e 2w) in
+      word_mul x x
+  else word_mul b (word_exp b (e - 1w))
+Termination
+  WF_REL_TAC`measure (w2n o SND)`
+  \\ Cases_on`dimword(:'a) = 2`
+  >- ( `2w = 0w` by simp[] \\ pop_assum SUBST1_TAC \\ gs[word_mod_def] )
+  \\ `2 < dimword(:'a)`
+  by ( CCONTR_TAC
+    \\ gs[NOT_LESS, NUMERAL_LESS_THM,
+          LESS_OR_EQ, ONE_LT_dimword, ZERO_LT_dimword] )
+  \\ qx_gen_tac`e` \\ rw[]
+  \\ qspec_then`2w` mp_tac WORD_DIVISION
+  \\ impl_tac >- rw[n2w_11]
+  \\ disch_then(qspec_then`e`mp_tac)
+  \\ rewrite_tac[word_div_def, word_mul_n2w, word_lo_n2w, GSYM WORD_LO]
+  \\ `w2n e < dimword (:'a)` by simp[w2n_lt]
+  \\ `w2n e DIV 2 < dimword(:'a)` by simp[DIV_LT_X]
+  \\ Cases_on`e`
+  \\ gs[word_lo_n2w]
+End
+
+val () = Parse.overload_on("**",
+  word_exp_def |> SPEC_ALL |> concl |> lhs |> strip_comb |> fst);
+
+Theorem word_exp_EXP:
+  !b e. word_exp b e = n2w $ w2n b ** w2n e
+Proof
+  recInduct word_exp_ind
+  \\ rw[]
+  \\ simp[Once word_exp_def]
+  \\ IF_CASES_TAC >- gs[]
+  \\ Cases_on`dimword(:'a) = 2`
+  >- (
+    gs[word_mod_def, word_div_def]
+    \\ `w2n b < 2 ∧ w2n e < 2` by metis_tac[w2n_lt]
+    \\ gs[NUMERAL_LESS_THM]
+    \\ Cases_on`b` \\ gs[word_mul_n2w] )
+  \\ `2 < dimword(:'a)`
+  by (
+    CCONTR_TAC
+    \\ gs[NOT_LESS, LESS_OR_EQ, NUMERAL_LESS_THM,
+          ONE_LT_dimword, ZERO_LT_dimword] )
+  \\ `w2n e < dimword (:'a)` by simp[w2n_lt]
+  \\ `w2n e DIV 2 < dimword(:'a)` by simp[DIV_LT_X]
+  \\ Cases_on`e` \\ gs[word_mod_def, word_div_def]
+  \\ Cases_on`b` \\ gs[]
+  \\ gs[GSYM EXP_EXP_MULT, word_mul_n2w]
+  \\ DEP_REWRITE_TAC[MOD_MOD_LESS]
+  \\ gs[]
+  \\ IF_CASES_TAC \\ gs[]
+  >- (
+    AP_THM_TAC \\ AP_TERM_TAC
+    \\ DEP_REWRITE_TAC[DIVIDES_DIV, DIVIDES_MOD_0]
+    \\ simp[] )
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ rewrite_tac[GSYM word_sub_def]
+  \\ DEP_REWRITE_TAC[GSYM n2w_sub]
+  \\ Cases_on`n` \\ gs[EXP]
+QED
+
+Definition word_exp_tailrec_def:
+  word_exp_tailrec (b:'a word) (e:'a word) a =
+  if e = 0w then a else
+  if word_mod e 2w = 0w then
+    word_exp_tailrec (word_mul b b) (word_div e 2w) a
+  else
+    word_exp_tailrec b (word_sub e 1w) (word_mul b a)
+Termination
+  WF_REL_TAC`measure (w2n o FST o SND)`
+  \\ Cases_on`dimword(:'a) = 2`
+  >- ( `2w = 0w` by simp[] \\ pop_assum SUBST1_TAC \\ gs[word_mod_def] )
+  \\ `2 < dimword(:'a)`
+  by ( CCONTR_TAC
+    \\ gs[NOT_LESS, NUMERAL_LESS_THM,
+          LESS_OR_EQ, ONE_LT_dimword, ZERO_LT_dimword] )
+  \\ qx_gen_tac`e` \\ rw[]
+  \\ Cases_on`e`
+  \\ gs[word_div_def, word_mod_def, MOD_MOD_LESS]
+  \\ DEP_REWRITE_TAC[LESS_MOD]
+  \\ conj_asm2_tac \\ gs[DIV_LT_X]
+End
+
+Theorem word_exp_tailrec_EXP:
+  !b e a. word_exp_tailrec b e a = n2w $ w2n a * w2n b ** w2n e
+Proof
+  recInduct word_exp_tailrec_ind
+  \\ rpt strip_tac
+  \\ simp[Once word_exp_tailrec_def]
+  \\ IF_CASES_TAC \\ gs[]
+  \\ Cases_on`dimword(:'a) = 2`
+  >- (
+    `2w = 0w` by simp[] \\ pop_assum SUBST1_TAC
+    \\ gs[word_mod_def]
+    \\ rewrite_tac[GSYM word_sub_def]
+    \\ Cases_on`e`
+    \\ DEP_REWRITE_TAC[GSYM n2w_sub]
+    \\ conj_asm1_tac \\ gs[]
+    \\ Cases_on`n` \\ gs[EXP]
+    \\ Cases_on`a` \\ Cases_on`b`
+    \\ gs[word_mul_n2w])
+  \\ `2 < dimword(:'a)`
+  by ( CCONTR_TAC
+    \\ gs[NOT_LESS, NUMERAL_LESS_THM,
+          LESS_OR_EQ, ONE_LT_dimword, ZERO_LT_dimword] )
+  \\ Cases_on`e` \\ gs[word_mod_def, word_div_def]
+  \\ reverse IF_CASES_TAC \\ gs[MOD_MOD_LESS]
+  >- (
+    rewrite_tac[GSYM word_sub_def]
+    \\ `1 <= n` by simp[]
+    \\ asm_simp_tac std_ss [GSYM n2w_sub, w2n_n2w]
+    \\ `(n - 1) MOD dimword(:'a) = n - 1`
+    by ( DEP_REWRITE_TAC[LESS_MOD] \\ simp[] )
+    \\ pop_assum SUBST_ALL_TAC
+    \\ Cases_on`a` \\ Cases_on`b`
+    \\ gs[word_mul_n2w]
+    \\ Cases_on`n` \\ gs[EXP] )
+  \\ `(n DIV 2) MOD dimword(:'a) = n DIV 2`
+  by ( DEP_REWRITE_TAC[LESS_MOD] \\ gs[DIV_LT_X] )
+  \\ pop_assum SUBST_ALL_TAC
+  \\ Cases_on`a` \\ Cases_on`b`
+  \\ gs[word_mul_n2w]
+  \\ gs[GSYM EXP_EXP_MULT]
+  \\ DEP_REWRITE_TAC[DIVIDES_DIV]
+  \\ gs[DIVIDES_MOD_0]
+QED
+
+Theorem word_exp_tailrec:
+  word_exp b e = word_exp_tailrec b e 1w
+Proof
+  rw[word_exp_EXP, word_exp_tailrec_EXP]
+QED
+
 (* -------------------------------------------------------------------------
     More theorems
    ------------------------------------------------------------------------- *)

src/num/theories/arithmeticScript.sml

@@ -2466,6 +2466,17 @@ val MOD_LESS = Q.store_thm ("MOD_LESS",
  `!m n. 0 < n ==> m MOD n < n`,
  METIS_TAC [DIVISION]);
 
+Theorem MOD_MOD_LESS:
+  0 < y /\ y < z ==> x MOD y MOD z = x MOD y
+Proof
+  strip_tac
+  \\ irule LESS_MOD
+  \\ irule LESS_TRANS
+  \\ goal_assum(first_assum o mp_then Any mp_tac)
+  \\ irule MOD_LESS
+  \\ simp[]
+QED
+
 val ADD_MODULUS = Q.store_thm ("ADD_MODULUS",
 `(!n x. 0 < n ==> ((x + n) MOD n = x MOD n)) /\
  (!n x. 0 < n ==> ((n + x) MOD n = x MOD n))`,