more theorems

--- a/src/HOL/Library/Type_Length.thy	Thu Apr 16 08:09:30 2020 +0200
+++ b/src/HOL/Library/Type_Length.thy	Thu Apr 16 08:09:31 2020 +0200
@@ -107,4 +107,14 @@
   \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
   by (auto simp add: not_le dest: less_2_cases)
 
+context linordered_idom
+begin
+
+lemma two_less_eq_exp_length [simp]:
+  \<open>2 \<le> 2 ^ LENGTH('b::len)\<close>
+  using mult_left_mono [of 1 \<open>2 ^ (LENGTH('b::len) - 1)\<close> 2]
+		  by (cases \<open>LENGTH('b::len)\<close>) simp_all
+
 end
+
+end

--- a/src/HOL/Parity.thy	Thu Apr 16 08:09:30 2020 +0200
+++ b/src/HOL/Parity.thy	Thu Apr 16 08:09:31 2020 +0200
@@ -1218,6 +1218,10 @@
   \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + of_bool (odd a))\<close>
   by (cases n) (simp_all add: take_bit_Suc)
 
+lemma take_bit_Suc_0 [simp]:
+  \<open>take_bit (Suc 0) a = a mod 2\<close>
+  by (simp add: take_bit_eq_mod)
+
 lemma take_bit_of_0 [simp]:
   "take_bit n 0 = 0"
   by (simp add: take_bit_eq_mod)
@@ -1536,6 +1540,24 @@
     for k :: int
   by (simp add: take_bit_eq_mod)
 
+lemma take_bit_minus_small_eq:
+  \<open>take_bit n (- k) = 2 ^ n - k\<close> if \<open>0 < k\<close> \<open>k \<le> 2 ^ n\<close> for k :: int
+proof -
+  define m where \<open>m = nat k\<close>
+  with that have \<open>k = int m\<close> and \<open>0 < m\<close> and \<open>m \<le> 2 ^ n\<close>
+    by simp_all
+  have \<open>(2 ^ n - m) mod 2 ^ n = 2 ^ n - m\<close>
+    using \<open>0 < m\<close> by simp
+  then have \<open>int ((2 ^ n - m) mod 2 ^ n) = int (2 ^ n - m)\<close>
+    by simp
+  then have \<open>(2 ^ n - int m) mod 2 ^ n = 2 ^ n - int m\<close>
+    using \<open>m \<le> 2 ^ n\<close> by (simp only: of_nat_mod of_nat_diff) simp
+  with \<open>k = int m\<close> have \<open>(2 ^ n - k) mod 2 ^ n = 2 ^ n - k\<close>
+    by simp
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
 lemma drop_bit_push_bit_int:
   \<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int
   by (cases \<open>m \<le> n\<close>) (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc