word_lib: uint/cast lemmas about w - 1

Signed-off-by: Gerwin Klein <[email protected]>

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