--- 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