# HG changeset patch
# User haftmann
# Date 1659028489 -7200
# Node ID 40af1efeadeeca49c2f0cf8da95eaaeedade0152
# Parent  ff0aceed8923a67b0a54c5340653e816f6da8a59
More lemmas.

diff -r ff0aceed8923 -r 40af1efeadee src/HOL/ex/Word_Lsb_Msb.thy
--- a/src/HOL/ex/Word_Lsb_Msb.thy	Thu Jul 28 16:50:15 2022 +0200
+++ b/src/HOL/ex/Word_Lsb_Msb.thy	Thu Jul 28 19:14:49 2022 +0200
@@ -130,6 +130,15 @@
   \<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)
 
+definition signed_drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>signed_drop_bit n w = drop_bit n w
+    OR (of_bool (bit w (word_length TYPE('a) - Suc 0)) * NOT (mask (word_length TYPE('a) - Suc n)))\<close>
+
+lemma msb_signed_drop_bit_iff [simp]:
+  \<open>msb (signed_drop_bit n w) \<longleftrightarrow> msb w\<close>
+  by (simp add: signed_drop_bit_def bit_simps not_le not_less)
+    (simp add: msb_def)
+
 end
 
 end