# HG changeset patch
# User haftmann
# Date 1580580640 -3600
# Node ID 65ffe9e910d49857169788f271cbabb86c40a9a6
# Parent  96d126844adc22692440d51104c6bcd3791ff1fb
more specific class assumptions

diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Code_Numeral.thy
--- 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
 
diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Euclidean_Division.thy
--- 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
 
 
diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Parity.thy
--- 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 +
diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/ex/Bit_Operations.thy
--- 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
 
diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/ex/Word.thy
--- 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