--- a/src/HOL/Divides.thy Sat Jul 11 18:19:08 2020 +0200
+++ b/src/HOL/Divides.thy Sat Jul 11 18:09:08 2020 +0000
@@ -753,6 +753,32 @@
thus ?lhs by simp
qed
+lemma take_bit_greater_eq:
+ \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
+proof -
+ have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
+ proof (cases \<open>k > - (2 ^ n)\<close>)
+ case False
+ then have \<open>k + 2 ^ n \<le> 0\<close>
+ by simp
+ also note take_bit_nonnegative
+ finally show ?thesis .
+ next
+ case True
+ with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
+ by simp_all
+ then show ?thesis
+ by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
+ qed
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_less_eq:
+ \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
+ using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
+ by (simp add: take_bit_eq_mod)
+
subsection \<open>Numeral division with a pragmatic type class\<close>
--- a/src/HOL/Library/Bit_Operations.thy Sat Jul 11 18:19:08 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy Sat Jul 11 18:09:08 2020 +0000
@@ -9,43 +9,6 @@
Main
begin
-subsection \<open>Preliminiaries\<close> \<comment> \<open>TODO move\<close>
-
-lemma take_bit_int_less_exp:
- \<open>take_bit n k < 2 ^ n\<close> for k :: int
- by (simp add: take_bit_eq_mod)
-
-lemma take_bit_Suc_from_most:
- \<open>take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\<close> for k :: int
- by (simp only: take_bit_eq_mod power_Suc2) (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one zmod_zmult2_eq)
-
-lemma take_bit_greater_eq:
- \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
-proof -
- have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
- proof (cases \<open>k > - (2 ^ n)\<close>)
- case False
- then have \<open>k + 2 ^ n \<le> 0\<close>
- by simp
- also note take_bit_nonnegative
- finally show ?thesis .
- next
- case True
- with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
- by simp_all
- then show ?thesis
- by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
- qed
- then show ?thesis
- by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_less_eq:
- \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
- using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
- by (simp add: take_bit_eq_mod)
-
-
subsection \<open>Bit operations\<close>
class semiring_bit_operations = semiring_bit_shifts +
--- a/src/HOL/Parity.thy Sat Jul 11 18:19:08 2020 +0200
+++ b/src/HOL/Parity.thy Sat Jul 11 18:09:08 2020 +0000
@@ -1648,6 +1648,10 @@
\<open>drop_bit n (- 1 :: int) = - 1\<close>
by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
+lemma take_bit_Suc_from_most:
+ \<open>take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\<close> for k :: int
+ by (simp only: take_bit_eq_mod power_Suc2) (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one zmod_zmult2_eq)
+
lemma take_bit_minus:
\<open>take_bit n (- take_bit n k) = take_bit n (- k)\<close>
for k :: int
@@ -1663,6 +1667,10 @@
for k :: int
by (simp add: take_bit_eq_mod)
+lemma take_bit_int_less_exp:
+ \<open>take_bit n k < 2 ^ n\<close> for k :: int
+ by (simp add: take_bit_eq_mod)
+
lemma (in ring_1) of_nat_nat_take_bit_eq [simp]:
\<open>of_nat (nat (take_bit n k)) = of_int (take_bit n k)\<close>
by simp