# HG changeset patch
# User haftmann
# Date 1580070932 0
# Node ID 554385d4cf59499ee20fc2eb005cf8c3b5af8d60
# Parent  2525e28e4b8b56dc355728ea27358c9a1538f80f
more theorems

diff -r 2525e28e4b8b -r 554385d4cf59 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Jan 26 20:35:31 2020 +0000
+++ b/src/HOL/Euclidean_Division.thy	Sun Jan 26 20:35:32 2020 +0000
@@ -1933,6 +1933,35 @@
     by (simp add: of_nat_mod)
 qed
 
+lemma range_mod_exp:
+  \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close>
+proof -
+  have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>)
+  proof (cases \<open>n \<le> m\<close>)
+    case True
+    then show ?thesis
+      by (simp add: Suc_le_lessD min.absorb2)
+  next
+    case False
+    then have \<open>m < n\<close>
+      by simp
+    then obtain q where n: \<open>n = Suc q + m\<close>
+      by (auto dest: less_imp_Suc_add)
+    then have \<open>min m n = m\<close>
+      by simp
+    moreover have \<open>(2::nat) ^ m \<le> 2 * 2 ^ q * 2 ^ m\<close>
+      using mult_le_mono1 [of 1 \<open>2 * 2 ^ q\<close> \<open>2 ^ m\<close>] by simp
+    with n have \<open>2 ^ n - 1 = (2 ^ Suc q - 1) * 2 ^ m + (2 ^ m - (1::nat))\<close>
+      by (simp add: monoid_mult_class.power_add algebra_simps)
+    ultimately show ?thesis
+      by (simp only: euclidean_semiring_cancel_class.mod_mult_self3) simp
+  qed
+  then have \<open>of_nat ?lhs = of_nat ?rhs\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_mod of_nat_diff)
+qed
+
 end
 
 class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
diff -r 2525e28e4b8b -r 554385d4cf59 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Jan 26 20:35:31 2020 +0000
+++ b/src/HOL/Parity.thy	Sun Jan 26 20:35:32 2020 +0000
@@ -763,6 +763,14 @@
   \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
   by (auto simp add: bit_def exp_div_exp_eq)
 
+lemma bit_1_iff:
+  \<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close>
+  using bit_exp_iff [of 0 n] by simp
+
+lemma bit_2_iff:
+  \<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close>
+  using bit_exp_iff [of 1 n] by auto
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
@@ -960,6 +968,14 @@
   differently wrt. code generation.
 \<close>
 
+lemma bit_iff_odd_drop_bit:
+  \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
+  by (simp add: bit_def drop_bit_eq_div)
+
+lemma even_drop_bit_iff_not_bit:
+  \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close>
+  by (simp add: bit_iff_odd_drop_bit)
+
 lemma bits_ident:
   "push_bit n (drop_bit n a) + take_bit n a = a"
   using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
@@ -1158,6 +1174,10 @@
   \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
   using take_bit_of_exp [of n 1] by simp
 
+lemma take_bit_of_range:
+  \<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close>
+  by (simp add: take_bit_eq_mod range_mod_exp)
+
 lemma push_bit_eq_0_iff [simp]:
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
   by (simp add: push_bit_eq_mult)