--- a/src/HOL/Library/Word.thy Sat Dec 05 20:40:24 2020 +0100
+++ b/src/HOL/Library/Word.thy Sat Dec 05 19:24:36 2020 +0000
@@ -908,6 +908,18 @@
\<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
by transfer simp
+lemma finite_bit_word [simp]:
+ \<open>finite {n. bit w n}\<close>
+ for w :: \<open>'a::len word\<close>
+proof -
+ have \<open>{n. bit w n} \<subseteq> {0..LENGTH('a)}\<close>
+ by (auto dest: bit_imp_le_length)
+ moreover have \<open>finite {0..LENGTH('a)}\<close>
+ by simp
+ ultimately show ?thesis
+ by (rule finite_subset)
+qed
+
instantiation word :: (len) semiring_bit_shifts
begin