# HG changeset patch
# User haftmann
# Date 1594490948 0
# Node ID 08348e364739b0b76d6bcba9e4a8a1bad4b2f0aa
# Parent  45865bb06182f2a0c8905291a9bef0e63db3bb5e
more thms

diff -r 45865bb06182 -r 08348e364739 src/HOL/Divides.thy
--- 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>
 
diff -r 45865bb06182 -r 08348e364739 src/HOL/Library/Bit_Operations.thy
--- 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 +
diff -r 45865bb06182 -r 08348e364739 src/HOL/Parity.thy
--- 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