# HG changeset patch
# User haftmann
# Date 1580580637 -3600
# Node ID 96d126844adc22692440d51104c6bcd3791ff1fb
# Parent  839bf7d74faef1d11a573937de2cbf397cecd699
more theorems

diff -r 839bf7d74fae -r 96d126844adc src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/Euclidean_Division.thy	Sat Feb 01 19:10:37 2020 +0100
@@ -1933,7 +1933,7 @@
     by (simp add: of_nat_mod)
 qed
 
-lemma range_mod_exp:
+lemma mask_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>)
diff -r 839bf7d74fae -r 96d126844adc src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/Parity.thy	Sat Feb 01 19:10:37 2020 +0100
@@ -150,6 +150,19 @@
 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   by (induct n) auto
 
+lemma mask_eq_sum_exp:
+  \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
+proof -
+  have *: \<open>{q. q < Suc m} = insert m {q. q < m}\<close> for m
+    by auto
+  have \<open>2 ^ n = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1\<close>
+    by (induction n) (simp_all add: ac_simps mult_2 *)
+  then have \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1 - 1\<close>
+    by simp
+  then show ?thesis
+    by simp
+qed
+
 end
 
 class ring_parity = ring + semiring_parity
@@ -398,6 +411,43 @@
   qed
 qed
 
+context semiring_parity
+begin
+
+lemma even_sum_iff:
+  \<open>even (sum f A) \<longleftrightarrow> even (card {a\<in>A. odd (f a)})\<close> if \<open>finite A\<close>
+using that proof (induction A)
+  case empty
+  then show ?case
+    by simp
+next
+  case (insert a A)
+  moreover have \<open>{b \<in> insert a A. odd (f b)} = (if odd (f a) then {a} else {}) \<union> {b \<in> A. odd (f b)}\<close>
+    by auto
+  ultimately show ?case
+    by simp
+qed
+
+lemma even_prod_iff:
+  \<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close>
+  using that by (induction A) simp_all
+
+lemma even_mask_iff [simp]:
+  \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
+proof (cases \<open>n = 0\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have \<open>{a. a = 0 \<and> a < n} = {0}\<close>
+    by auto
+  then show ?thesis
+    by (auto simp add: mask_eq_sum_exp even_sum_iff)
+qed
+
+end
+
 
 subsection \<open>Parity and powers\<close>
 
@@ -1162,6 +1212,38 @@
 
 end
 
+lemma bit_push_bit_iff_nat:
+  \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat
+proof (cases \<open>m \<le> n\<close>)
+  case True
+  then obtain r where \<open>n = m + r\<close>
+    using le_Suc_ex by blast
+  with True show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
+next
+  case False
+  then obtain r where \<open>m = Suc (n + r)\<close>
+    using less_imp_Suc_add not_le by blast
+  with False show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
+qed
+
+lemma bit_push_bit_iff_int:
+  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
+proof (cases \<open>m \<le> n\<close>)
+  case True
+  then obtain r where \<open>n = m + r\<close>
+    using le_Suc_ex by blast
+  with True show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
+next
+  case False
+  then obtain r where \<open>m = Suc (n + r)\<close>
+    using less_imp_Suc_add not_le by blast
+  with False show ?thesis
+    by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
+qed
+
 class unique_euclidean_semiring_with_bit_shifts =
   unique_euclidean_semiring_with_nat + semiring_bit_shifts
 begin
@@ -1174,9 +1256,9 @@
   \<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:
+lemma take_bit_of_mask:
   \<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close>
-  by (simp add: take_bit_eq_mod range_mod_exp)
+  by (simp add: take_bit_eq_mod mask_mod_exp)
 
 lemma push_bit_eq_0_iff [simp]:
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
@@ -1230,6 +1312,39 @@
   "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
   by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
 
+lemma bit_of_nat_iff_bit [simp]:
+  \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
+proof -
+  have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
+    by simp
+  also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
+    by (simp add: of_nat_div)
+  finally show ?thesis
+    by (simp add: bit_def semiring_bits_class.bit_def)
+qed
+
+lemma of_nat_push_bit:
+  \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
+  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+
+lemma of_nat_drop_bit:
+  \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
+  by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
+
+lemma of_nat_take_bit:
+  \<open>of_nat (take_bit m n) = take_bit m (of_nat n)\<close>
+  by (simp add: take_bit_eq_mod semiring_bit_shifts_class.take_bit_eq_mod of_nat_mod)
+
+lemma bit_push_bit_iff_of_nat_iff:
+  \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
+proof -
+  from bit_push_bit_iff_nat
+  have \<open>bit (of_nat (push_bit m r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
+    by simp
+  then show ?thesis
+    by (simp add: of_nat_push_bit)
+qed
+
 end
 
 instance nat :: unique_euclidean_semiring_with_bit_shifts ..
diff -r 839bf7d74fae -r 96d126844adc src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/ex/Bit_Operations.thy	Sat Feb 01 19:10:37 2020 +0100
@@ -9,40 +9,16 @@
     Main
 begin
 
-lemma bit_push_bit_eq_int:
-  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
-proof (cases \<open>m \<le> n\<close>)
-  case True
-  then obtain q where \<open>n = m + q\<close>
-    using le_Suc_ex by blast
-  with True show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add)
-next
-  case False
-  then obtain q where \<open>m = Suc (n + q)\<close>
-    using less_imp_Suc_add not_le by blast
-  with False show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add)
-qed
-
 context semiring_bits
 begin
 
-(*lemma range_rec:
-  \<open>2 ^ Suc n - 1 = 1 + 2 * (2 ^ n - 1)\<close>
+(*lemma even_mask_div_iff:
+  \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
   sorry
 
-lemma even_range_div_iff:
-  \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
-  sorry*)
-
-(*lemma even_range_iff [simp]:
-  \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close>
-  by (induction n) (simp_all only: range_rec, simp_all)
-
-lemma bit_range_iff:
+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_range_div_iff not_le)*)
+  by (simp add: bit_def even_mask_div_iff not_le)*)
 
 end
 
@@ -129,6 +105,30 @@
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
   by (simp add: flip_bit_def)
 
+lemma zero_and_eq [simp]:
+  "0 AND a = 0"
+  by (simp add: bit_eq_iff bit_and_iff)
+
+lemma and_zero_eq [simp]:
+  "a AND 0 = 0"
+  by (simp add: bit_eq_iff bit_and_iff)
+
+lemma zero_or_eq [simp]:
+  "0 OR a = a"
+  by (simp add: bit_eq_iff bit_or_iff)
+
+lemma or_zero_eq [simp]:
+  "a OR 0 = a"
+  by (simp add: bit_eq_iff bit_or_iff)
+
+lemma zero_xor_eq [simp]:
+  "0 XOR a = a"
+  by (simp add: bit_eq_iff bit_xor_iff)
+
+lemma xor_zero_eq [simp]:
+  "a XOR 0 = a"
+  by (simp add: bit_eq_iff bit_xor_iff)
+
 lemma take_bit_and [simp]:
   \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
@@ -209,6 +209,10 @@
     done
 qed
 
+lemma push_bit_minus:
+  \<open>push_bit n (- a) = - push_bit n a\<close>
+  by (simp add: push_bit_eq_mult)
+
 lemma take_bit_not_take_bit:
   \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
@@ -327,14 +331,6 @@
 declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_nat_and_eq [simp]:
-  "0 AND n = 0" for n :: nat
-  by simp
-
-lemma and_zero_nat_eq [simp]:
-  "n AND 0 = 0" for n :: nat
-  by simp
-
 global_interpretation or_nat: zip_nat "(\<or>)"
   defines or_nat = or_nat.F
   by standard auto
@@ -348,14 +344,6 @@
 declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_nat_or_eq [simp]:
-  "0 OR n = n" for n :: nat
-  by simp
-
-lemma or_zero_nat_eq [simp]:
-  "n OR 0 = n" for n :: nat
-  by simp
-
 global_interpretation xor_nat: zip_nat "(\<noteq>)"
   defines xor_nat = xor_nat.F
   by standard auto
@@ -363,14 +351,6 @@
 declare xor_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_nat_xor_eq [simp]:
-  "0 XOR n = n" for n :: nat
-  by simp
-
-lemma xor_zero_nat_eq [simp]:
-  "n XOR 0 = n" for n :: nat
-  by simp
-
 instance proof
   fix m n q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
@@ -678,22 +658,6 @@
     by (simp add: and_int.self)
 qed
 
-lemma zero_int_and_eq [simp]:
-  "0 AND k = 0" for k :: int
-  by simp
-
-lemma and_zero_int_eq [simp]:
-  "k AND 0 = 0" for k :: int
-  by simp
-
-lemma minus_int_and_eq [simp]:
-  "- 1 AND k = k" for k :: int
-  by simp
-
-lemma and_minus_int_eq [simp]:
-  "k AND - 1 = k" for k :: int
-  by simp
-
 global_interpretation or_int: zip_int "(\<or>)"
   defines or_int = or_int.F
   by standard
@@ -707,22 +671,6 @@
     by (simp add: or_int.self)
 qed
 
-lemma zero_int_or_eq [simp]:
-  "0 OR k = k" for k :: int
-  by simp
-
-lemma and_zero_or_eq [simp]:
-  "k OR 0 = k" for k :: int
-  by simp
-
-lemma minus_int_or_eq [simp]:
-  "- 1 OR k = - 1" for k :: int
-  by simp
-
-lemma or_minus_int_eq [simp]:
-  "k OR - 1 = - 1" for k :: int
-  by simp
-
 global_interpretation xor_int: zip_int "(\<noteq>)"
   defines xor_int = xor_int.F
   by standard
@@ -730,42 +678,6 @@
 declare xor_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
   \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
 
-lemma zero_int_xor_eq [simp]:
-  "0 XOR k = k" for k :: int
-  by simp
-
-lemma and_zero_xor_eq [simp]:
-  "k XOR 0 = k" for k :: int
-  by simp
-
-lemma minus_int_xor_eq [simp]:
-  "- 1 XOR k = complement k" for k :: int
-  by simp
-
-lemma xor_minus_int_eq [simp]:
-  "k XOR - 1 = complement k" for k :: int
-  by simp
-
-lemma not_div_2:
-  "NOT k div 2 = NOT (k div 2)"
-  for k :: int
-  by (simp add: complement_div_2 not_int_def)
-
-lemma not_int_simps [simp]:
-  "NOT 0 = (- 1 :: int)"
-  "NOT (- 1) = (0 :: int)"
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
-  by (auto simp add: not_int_def elim: oddE)
-
-lemma not_one_int [simp]:
-  "NOT 1 = (- 2 :: int)"
-  by simp
-
-lemma even_not_iff [simp]:
-  "even (NOT k) \<longleftrightarrow> odd k"
-    for k :: int
-  by (simp add: not_int_def)
-
 lemma bit_not_iff_int:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
     for k :: int
@@ -810,12 +722,28 @@
 
 end
 
+lemma not_div_2:
+  "NOT k div 2 = NOT (k div 2)" for k :: int
+  by (simp add: complement_div_2 not_int_def)
+
+lemma not_int_rec [simp]:
+  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+  by (auto simp add: not_int_def elim: oddE)
+
+lemma not_one_int [simp]:
+  "NOT 1 = (- 2 :: int)"
+  by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
+
+lemma even_not_int_iff [simp]:
+  "even (NOT k) \<longleftrightarrow> odd k" for k :: int
+  using bit_not_iff [of k 0] by auto
+
 lemma one_and_int_eq [simp]:
-  "1 AND k = k mod 2" for k :: int
-  by (simp add: bit_eq_iff bit_and_iff mod2_eq_if) (auto simp add: bit_1_iff)
+  "1 AND k = of_bool (odd k)" for k :: int
+  by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
 
 lemma and_one_int_eq [simp]:
-  "k AND 1 = k mod 2" for k :: int
+  "k AND 1 = of_bool (odd k)" for k :: int
   using one_and_int_eq [of 1] by (simp add: ac_simps)
 
 lemma one_or_int_eq [simp]:
diff -r 839bf7d74fae -r 96d126844adc src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/ex/Word.thy	Sat Feb 01 19:10:37 2020 +0100
@@ -546,11 +546,11 @@
     n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close>
   by transfer
     (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_eq_int)
+      simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
 
-(*lemma even_range_div_iff_word:
+(*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_range even_range_div_iff)*)
+  by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)*)
 
 instance word :: (len) semiring_bits
 proof