Some more proofs.

--- a/src/HOL/ex/Word_Lsb_Msb.thy	Thu Jul 28 12:33:20 2022 +0100
+++ b/src/HOL/ex/Word_Lsb_Msb.thy	Thu Jul 28 16:50:15 2022 +0200
@@ -5,8 +5,8 @@
 class word = ring_bit_operations +
   fixes word_length :: \<open>'a itself \<Rightarrow> nat\<close>
   assumes word_length_positive [simp]: \<open>0 < word_length TYPE('a)\<close>
-    and possible_bit_msb [simp]: \<open>possible_bit TYPE('a) (word_length TYPE('a) - Suc 0)\<close>
-    and not_possible_bit_length [simp]: \<open>\<not> possible_bit TYPE('a) (word_length TYPE('a))\<close>
+    and possible_bit_msb: \<open>possible_bit TYPE('a) (word_length TYPE('a) - Suc 0)\<close>
+    and not_possible_bit_length: \<open>\<not> possible_bit TYPE('a) (word_length TYPE('a))\<close>
 begin
 
 lemma word_length_not_0 [simp]:
@@ -14,6 +14,27 @@
   using word_length_positive
   by simp 
 
+lemma possible_bit_iff_less_word_length:
+  \<open>possible_bit TYPE('a) n \<longleftrightarrow> n < word_length TYPE('a)\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume \<open>?P\<close>
+  show ?Q
+  proof (rule ccontr)
+    assume \<open>\<not> n < word_length TYPE('a)\<close>
+    then have \<open>word_length TYPE('a) \<le> n\<close>
+      by simp
+    with \<open>?P\<close> have \<open>possible_bit TYPE('a) (word_length TYPE('a))\<close>
+      by (rule possible_bit_less_imp)
+    with not_possible_bit_length show False ..
+  qed
+next
+  assume \<open>?Q\<close>
+  then have \<open>n \<le> word_length TYPE('a) - Suc 0\<close>
+    by simp
+  with possible_bit_msb show ?P
+    by (rule possible_bit_less_imp)
+qed
+
 end
 
 instantiation word :: (len) word
@@ -46,7 +67,7 @@
 
 lemma msb_minus_1 [simp]:
   \<open>msb (- 1)\<close>
-  by (simp add: msb_def)
+  by (simp add: msb_def possible_bit_iff_less_word_length)
 
 lemma msb_1_iff [simp]:
   \<open>msb 1 \<longleftrightarrow> word_length TYPE('a) = 1\<close>
@@ -54,11 +75,11 @@
 
 lemma msb_minus_iff [simp]:
   \<open>msb (- w) \<longleftrightarrow> \<not> msb (w - 1)\<close>
-  by (simp add: msb_def bit_simps)
+  by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
 
 lemma msb_not_iff [simp]:
   \<open>msb (NOT w) \<longleftrightarrow> \<not> msb w\<close>
-  by (simp add: msb_def bit_simps)
+  by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
 
 lemma msb_and_iff [simp]:
   \<open>msb (v AND w) \<longleftrightarrow> msb v \<and> msb w\<close>
@@ -74,11 +95,11 @@
 
 lemma msb_exp_iff [simp]:                                             
   \<open>msb (2 ^ n) \<longleftrightarrow> n = word_length TYPE('a) - Suc 0\<close>
-  by (simp add: msb_def bit_simps)
+  by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
 
 lemma msb_mask_iff [simp]:
   \<open>msb (mask n) \<longleftrightarrow> word_length TYPE('a) \<le> n\<close>
-  by (simp add: msb_def bit_simps less_diff_conv2 Suc_le_eq less_Suc_eq_le)
+  by (simp add: msb_def bit_simps less_diff_conv2 Suc_le_eq less_Suc_eq_le possible_bit_iff_less_word_length)
 
 lemma msb_set_bit_iff [simp]:
   \<open>msb (set_bit n w) \<longleftrightarrow> n = word_length TYPE('a) - Suc 0 \<or> msb w\<close>
@@ -94,25 +115,20 @@
 
 lemma msb_push_bit_iff:
   \<open>msb (push_bit n w) \<longleftrightarrow> n < word_length TYPE('a) \<and> bit w (word_length TYPE('a) - Suc n)\<close>
-  by (simp add: msb_def bit_simps le_diff_conv2 Suc_le_eq)
+  by (simp add: msb_def bit_simps le_diff_conv2 Suc_le_eq possible_bit_iff_less_word_length)
 
-(*lemma msb_drop_bit_iff [simp]:
+lemma msb_drop_bit_iff [simp]:
   \<open>msb (drop_bit n w) \<longleftrightarrow> n = 0 \<and> msb w\<close>
-  apply (cases n)
-  apply simp_all
-  apply (auto simp add: msb_def bit_simps)
-  oops*)
+  by (cases n)
+    (auto simp add: msb_def bit_simps possible_bit_iff_less_word_length intro!: impossible_bit)
 
 lemma msb_take_bit_iff [simp]:
   \<open>msb (take_bit n w) \<longleftrightarrow> word_length TYPE('a) \<le> n \<and> msb w\<close>
   by (simp add: take_bit_eq_mask ac_simps)
 
-(*lemma msb_signed_take_bit_iff:
-  \<open>msb (signed_take_bit n w) \<longleftrightarrow> P w n\<close>
-  unfolding signed_take_bit_def
-  apply (simp add: signed_take_bit_def not_le)
-  apply auto
-  oops*)
+lemma msb_signed_take_bit_iff:
+  \<open>msb (signed_take_bit n w) \<longleftrightarrow> bit w (min n (word_length TYPE('a) - Suc 0))\<close>
+  by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
 
 end