# HG changeset patch
# User haftmann
# Date 1624470211 0
# Node ID 465846b611d571d9cdb7811316fe3b5da643f0d4
# Parent  66bff50bc5f11adb68618e4adb07716b5d4fab6e
some word streamlining

diff -r 66bff50bc5f1 -r 465846b611d5 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Library/Bit_Operations.thy	Wed Jun 23 17:43:31 2021 +0000
@@ -1520,6 +1520,17 @@
   for k :: int
   by (simp add: signed_take_bit_def not_less concat_bit_def)
 
+lemma signed_take_bit_int_greater_eq_minus_exp [simp]:
+  \<open>- (2 ^ n) \<le> signed_take_bit n k\<close>
+  for k :: int
+  by (simp add: signed_take_bit_eq_take_bit_shift)
+
+lemma signed_take_bit_int_less_exp [simp]:
+  \<open>signed_take_bit n k < 2 ^ n\<close>
+  for k :: int
+  using take_bit_int_less_exp [of \<open>Suc n\<close>]
+  by (simp add: signed_take_bit_eq_take_bit_shift)
+
 lemma signed_take_bit_int_eq_self_iff:
   \<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
   for k :: int