From 3b47d895fadbbce577dd7443aaa2d9f961619129 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 20 Oct 2024 13:14:44 +0100
Subject: [PATCH] Define word_exp in consistent style

Removed the non-tail-recursive version since that is not particularly
useful.
---
 src/n-bit/wordsScript.sml | 85 +++++----------------------------------
 1 file changed, 9 insertions(+), 76 deletions(-)

diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index 3e71d500b0..f2fc343839 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -311,11 +311,15 @@ val word_rem_def = Define`
 
 val word_L2_def = Define `word_L2 = word_mul word_L word_L`
 
+val word_exp_def = Define`
+  word_exp (v:'a word) (w: 'a word) = n2w (w2n v ** w2n w): 'a word`
+
 val () = List.app (fn (s, t) => Parse.overload_on (s, Parse.Term t))
   [("+", `$word_add`),
    ("-", `$word_sub`),
    ("numeric_negate", `$word_2comp`),
    ("*", `$word_mul`),
+   ("**", `$word_exp`),
    ("CARRY_OUT", `\a b c. FST (SND (add_with_carry (a,b,c)))`),
    ("OVERFLOW",  `\a b c. SND (SND (add_with_carry (a,b,c)))`)]
 
@@ -4923,73 +4927,6 @@ 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_EQ]
-  \\ 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
@@ -5012,10 +4949,12 @@ Termination
   \\ 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
+Theorem word_exp_tailrec:
+  word_exp b e = word_exp_tailrec b e 1w
 Proof
-  recInduct word_exp_tailrec_ind
+  `!b e a. word_exp_tailrec b e a = n2w $ w2n a * w2n b ** w2n e`
+  suffices_by rw[word_exp_def]
+  \\ recInduct word_exp_tailrec_ind
   \\ rpt strip_tac
   \\ simp[Once word_exp_tailrec_def]
   \\ IF_CASES_TAC \\ gs[]
@@ -5056,12 +4995,6 @@ Proof
   \\ 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
    ------------------------------------------------------------------------- *)