diff -r 02fbb93d5b01 -r c49564b6eb0f src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Apr 20 07:51:06 2025 +0200
+++ b/src/HOL/Library/Word.thy	Sun Apr 20 11:42:13 2025 +0200
@@ -511,6 +511,27 @@
   by transfer simp
 
 
+subsection \<open>Elementary case distinctions\<close>
+
+lemma word_length_one [case_names zero minus_one length_beyond]:
+  fixes w :: \<open>'a::len word\<close>
+  obtains (zero) \<open>LENGTH('a) = Suc 0\<close> \<open>w = 0\<close>
+  | (minus_one) \<open>LENGTH('a) = Suc 0\<close> \<open>w = - 1\<close>
+  | (length_beyond) \<open>2 \<le> LENGTH('a)\<close>
+proof (cases \<open>2 \<le> LENGTH('a)\<close>)
+  case True
+  with length_beyond show ?thesis .
+next
+  case False
+  then have \<open>LENGTH('a) = Suc 0\<close>
+    by simp
+  then have \<open>w = 0 \<or> w = - 1\<close>
+    by transfer auto
+  with \<open>LENGTH('a) = Suc 0\<close> zero minus_one show ?thesis
+    by blast
+qed
+
+
 subsubsection \<open>Basic ordering\<close>
 
 instantiation word :: (len) linorder