author haftmann Sun, 26 Jan 2020 20:35:32 +0000 changeset 71408 554385d4cf59 parent 71407 2525e28e4b8b child 71409 0bb0cb558bf9
more theorems
 src/HOL/Euclidean_Division.thy file | annotate | diff | comparison | revisions src/HOL/Parity.thy file | annotate | diff | comparison | revisions
```--- 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>
+    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)```