--- a/src/HOL/Code_Numeral.thy Sat Feb 01 19:10:37 2020 +0100
+++ b/src/HOL/Code_Numeral.thy Sat Feb 01 19:10:40 2020 +0100
@@ -299,7 +299,8 @@
instance by (standard; transfer)
(fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
- exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
+ exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
+ even_mask_div_iff)+
end
@@ -995,7 +996,8 @@
instance by (standard; transfer)
(fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
- exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
+ exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
+ even_mask_div_iff)+
end
--- a/src/HOL/Euclidean_Division.thy Sat Feb 01 19:10:37 2020 +0100
+++ b/src/HOL/Euclidean_Division.thy Sat Feb 01 19:10:40 2020 +0100
@@ -327,6 +327,26 @@
using div_plus_div_distrib_dvd_left [of c b a]
by (simp add: ac_simps)
+lemma sum_div_partition:
+ \<open>(\<Sum>a\<in>A. f a) div b = (\<Sum>a\<in>A \<inter> {a. b dvd f a}. f a div b) + (\<Sum>a\<in>A \<inter> {a. \<not> b dvd f a}. f a) div b\<close>
+ if \<open>finite A\<close>
+proof -
+ have \<open>A = A \<inter> {a. b dvd f a} \<union> A \<inter> {a. \<not> b dvd f a}\<close>
+ by auto
+ then have \<open>(\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A \<inter> {a. b dvd f a} \<union> A \<inter> {a. \<not> b dvd f a}. f a)\<close>
+ by simp
+ also have \<open>\<dots> = (\<Sum>a\<in>A \<inter> {a. b dvd f a}. f a) + (\<Sum>a\<in>A \<inter> {a. \<not> b dvd f a}. f a)\<close>
+ using \<open>finite A\<close> by (auto intro: sum.union_inter_neutral)
+ finally have *: \<open>sum f A = sum f (A \<inter> {a. b dvd f a}) + sum f (A \<inter> {a. \<not> b dvd f a})\<close> .
+ define B where B: \<open>B = A \<inter> {a. b dvd f a}\<close>
+ with \<open>finite A\<close> have \<open>finite B\<close> and \<open>a \<in> B \<Longrightarrow> b dvd f a\<close> for a
+ by simp_all
+ then have \<open>(\<Sum>a\<in>B. f a) div b = (\<Sum>a\<in>B. f a div b)\<close> and \<open>b dvd (\<Sum>a\<in>B. f a)\<close>
+ by induction (simp_all add: div_plus_div_distrib_dvd_left)
+ then show ?thesis using *
+ by (simp add: B div_plus_div_distrib_dvd_left)
+qed
+
named_theorems mod_simps
text \<open>Addition respects modular equivalence.\<close>
@@ -442,6 +462,26 @@
by (simp add: mod_mult_left_eq mod_mult_right_eq)
qed
+lemma power_diff_power_eq:
+ \<open>a ^ m div a ^ n = (if n \<le> m then a ^ (m - n) else 1 div a ^ (n - m))\<close>
+ if \<open>a \<noteq> 0\<close>
+proof (cases \<open>n \<le> m\<close>)
+ case True
+ with that power_diff [symmetric, of a n m] show ?thesis by simp
+next
+ case False
+ then obtain q where n: \<open>n = m + Suc q\<close>
+ by (auto simp add: not_le dest: less_imp_Suc_add)
+ then have \<open>a ^ m div a ^ n = (a ^ m * 1) div (a ^ m * a ^ Suc q)\<close>
+ by (simp add: power_add ac_simps)
+ moreover from that have \<open>a ^ m \<noteq> 0\<close>
+ by simp
+ ultimately have \<open>a ^ m div a ^ n = 1 div a ^ Suc q\<close>
+ by (subst (asm) div_mult_mult1) simp
+ with False n show ?thesis
+ by simp
+qed
+
end
--- a/src/HOL/Parity.thy Sat Feb 01 19:10:37 2020 +0100
+++ b/src/HOL/Parity.thy Sat Feb 01 19:10:40 2020 +0100
@@ -411,6 +411,10 @@
qed
qed
+lemma mask_eq_sum_exp_nat:
+ \<open>2 ^ n - Suc 0 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
+ using mask_eq_sum_exp [where ?'a = nat] by simp
+
context semiring_parity
begin
@@ -573,6 +577,43 @@
end
+context unique_euclidean_semiring_with_nat
+begin
+
+lemma even_mask_div_iff':
+ \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
+proof -
+ have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close>
+ by (simp only: of_nat_div) (simp add: of_nat_diff)
+ also have \<open>\<dots> \<longleftrightarrow> even ((2 ^ m - Suc 0) div 2 ^ n)\<close>
+ by simp
+ also have \<open>\<dots> \<longleftrightarrow> m \<le> n\<close>
+ proof (cases \<open>m \<le> n\<close>)
+ case True
+ then show ?thesis
+ by (simp add: Suc_le_lessD)
+ next
+ case False
+ then obtain r where r: \<open>m = n + Suc r\<close>
+ using less_imp_Suc_add by fastforce
+ from r have \<open>{q. q < m} \<inter> {q. 2 ^ n dvd (2::nat) ^ q} = {q. n \<le> q \<and> q < m}\<close>
+ by (auto simp add: dvd_power_iff_le)
+ moreover from r have \<open>{q. q < m} \<inter> {q. \<not> 2 ^ n dvd (2::nat) ^ q} = {q. q < n}\<close>
+ by (auto simp add: dvd_power_iff_le)
+ moreover from False have \<open>{q. n \<le> q \<and> q < m \<and> q \<le> n} = {n}\<close>
+ by auto
+ then have \<open>odd ((\<Sum>a\<in>{q. n \<le> q \<and> q < m}. 2 ^ a div (2::nat) ^ n) + sum ((^) 2) {q. q < n} div 2 ^ n)\<close>
+ by (simp_all add: euclidean_semiring_cancel_class.power_diff_power_eq semiring_parity_class.even_sum_iff not_less mask_eq_sum_exp_nat [symmetric])
+ ultimately have \<open>odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)\<close>
+ by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all
+ with False show ?thesis
+ by (simp add: mask_eq_sum_exp_nat)
+ qed
+ finally show ?thesis .
+qed
+
+end
+
subsection \<open>Instance for \<^typ>\<open>int\<close>\<close>
@@ -627,6 +668,7 @@
and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
and bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+ and even_mask_div_iff: \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
@@ -881,6 +923,9 @@
apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin)
apply (simp add: mult.commute)
done
+ show \<open>even ((2 ^ m - (1::nat)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::nat) \<or> m \<le> n\<close>
+ for m n :: nat
+ using even_mask_div_iff' [where ?'a = nat, of m n] by simp
qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
lemma int_bit_induct [case_names zero minus even odd]:
@@ -994,6 +1039,9 @@
apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
apply (simp add: ac_simps)
done
+ show \<open>even ((2 ^ m - (1::int)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::int) \<or> m \<le> n\<close>
+ for m n :: nat
+ using even_mask_div_iff' [where ?'a = int, of m n] by simp
qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
class semiring_bit_shifts = semiring_bits +
--- a/src/HOL/ex/Bit_Operations.thy Sat Feb 01 19:10:37 2020 +0100
+++ b/src/HOL/ex/Bit_Operations.thy Sat Feb 01 19:10:40 2020 +0100
@@ -12,13 +12,9 @@
context semiring_bits
begin
-(*lemma even_mask_div_iff:
- \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
- sorry
-
lemma bit_mask_iff:
\<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
- by (simp add: bit_def even_mask_div_iff not_le)*)
+ by (simp add: bit_def even_mask_div_iff not_le)
end
--- a/src/HOL/ex/Word.thy Sat Feb 01 19:10:37 2020 +0100
+++ b/src/HOL/ex/Word.thy Sat Feb 01 19:10:40 2020 +0100
@@ -548,10 +548,6 @@
(auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
-(*lemma even_mask_div_iff_word:
- \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a::len word) \<or> m \<le> n\<close>
- by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)*)
-
instance word :: (len) semiring_bits
proof
show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
@@ -618,6 +614,9 @@
show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
for a :: "'a word" and m n :: nat
by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
+ show \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close>
+ for m n :: nat
+ by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)
qed
context