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