From 0e3c760e3bf20884989cfaa9e1be631d3372b5c1 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Tue, 7 May 2024 15:48:10 -0400
Subject: [PATCH] word_lib: uint/cast lemmas about w - 1

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 lib/Word_Lib/Word_Lemmas_Internal.thy | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy
index 73159d12cff..00938009f07 100644
--- a/lib/Word_Lib/Word_Lemmas_Internal.thy
+++ b/lib/Word_Lib/Word_Lemmas_Internal.thy
@@ -838,4 +838,19 @@ lemma ucast_ucast_mask_id:
    UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) (x && mask n)) = x && mask n" for x :: "'a::len word"
   by (simp add: ucast_ucast_len[OF eq_mask_less])
 
+lemma uint_less_1_eq:
+  "0 < n \<Longrightarrow> (uint (n - 1) < m) = (uint n \<le> m)"
+  by uint_arith
+
+lemma scast_ucast_up_minus_1_ucast:
+  assumes "LENGTH('a::len) < LENGTH('b::len)"
+  assumes "0 < w"
+  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w - 1) = UCAST('a \<rightarrow> 'c::len) (w - 1)"
+  using assms
+  apply (subst scast_eq_ucast; simp)
+   apply (metis gt0_iff_gem1 msb_less_mono ucast_less_ucast_weak unsigned_0 word_upcast_neg_msb)
+  apply (smt (verit) lt1_neq0 nat_le_linear scast_ucast_simps(9) ucast_1 ucast_sub_ucast
+                     verit_comp_simplify1(3) word_le_nat_alt)
+  done
+
 end