# HG changeset patch
# User nipkow
# Date 1588936802 -7200
# Node ID 3ef1418d64a6fee7c90ec756869028a093fd8c90
# Parent  214b48a1937be66b6af4a32cbc110f1e09b61bf1# Parent  95d2d5e60419c5b571ca84e8c95ed636a60adfbb
merged

diff -r 95d2d5e60419 -r 3ef1418d64a6 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri May 08 13:19:55 2020 +0200
+++ b/src/HOL/Parity.thy	Fri May 08 13:20:02 2020 +0200
@@ -934,6 +934,10 @@
   qed
 qed
 
+lemma bit_mod_2_iff [simp]:
+  \<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
+  by (cases a rule: parity_cases) (simp_all add: bit_def)
+
 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)
@@ -1204,7 +1208,7 @@
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_Suc:
-  \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
+  \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close>
 proof -
   have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close>
     using even_succ_mod_exp [of \<open>2 * (a div 2)\<close> \<open>Suc n\<close>]
@@ -1215,7 +1219,7 @@
 qed
 
 lemma take_bit_rec:
-  \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + of_bool (odd a))\<close>
+  \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + a mod 2)\<close>
   by (cases n) (simp_all add: take_bit_Suc)
 
 lemma take_bit_Suc_0 [simp]:
@@ -1442,7 +1446,7 @@
 
 lemma take_bit_Suc_bit1 [simp]:
   \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_Suc numeral_Bit1_div_2)
+  by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
 
 lemma take_bit_numeral_bit0 [simp]:
   \<open>take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2\<close>
@@ -1450,7 +1454,7 @@
 
 lemma take_bit_numeral_bit1 [simp]:
   \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_rec numeral_Bit1_div_2)
+  by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
 
 lemma take_bit_of_nat:
   "take_bit n (of_nat m) = of_nat (take_bit n m)"
diff -r 95d2d5e60419 -r 3ef1418d64a6 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri May 08 13:19:55 2020 +0200
+++ b/src/HOL/Set_Interval.thy	Fri May 08 13:20:02 2020 +0200
@@ -2087,7 +2087,7 @@
     = (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2"
     by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc)
   finally show ?case
-    using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc)
+    using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc mod_2_eq_odd)
 qed
 
 end
diff -r 95d2d5e60419 -r 3ef1418d64a6 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri May 08 13:19:55 2020 +0200
+++ b/src/HOL/String.thy	Fri May 08 13:20:02 2020 +0200
@@ -90,7 +90,7 @@
     also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
       by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
     finally show ?thesis
-      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps)
+      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps mod_2_eq_odd)
   qed
 qed
 
diff -r 95d2d5e60419 -r 3ef1418d64a6 src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Fri May 08 13:19:55 2020 +0200
+++ b/src/HOL/ex/Bit_Lists.thy	Fri May 08 13:20:02 2020 +0200
@@ -79,9 +79,9 @@
 lemma n_bits_of_eq_iff:
   "n_bits_of n a = n_bits_of n b \<longleftrightarrow> take_bit n a = take_bit n b"
   apply (induction n arbitrary: a b)
-   apply (auto elim!: evenE oddE simp add: take_bit_Suc)
-   apply (metis dvd_triv_right even_plus_one_iff)
-  apply (metis dvd_triv_right even_plus_one_iff)
+   apply (auto elim!: evenE oddE simp add: take_bit_Suc mod_2_eq_odd)
+    apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
+   apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
   done
 
 lemma take_n_bits_of [simp]:
@@ -98,7 +98,7 @@
 
 lemma unsigned_of_bits_n_bits_of [simp]:
   "unsigned_of_bits (n_bits_of n a) = take_bit n a"
-  by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc)
+  by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc mod_2_eq_odd)
 
 end
 
diff -r 95d2d5e60419 -r 3ef1418d64a6 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Fri May 08 13:19:55 2020 +0200
+++ b/src/HOL/ex/Bit_Operations.thy	Fri May 08 13:20:02 2020 +0200
@@ -37,6 +37,18 @@
 sublocale xor: comm_monoid \<open>(XOR)\<close> 0
   by standard (auto simp add: bit_eq_iff bit_xor_iff)
 
+lemma even_and_iff:
+  \<open>even (a AND b) \<longleftrightarrow> even a \<or> even b\<close>
+  using bit_and_iff [of a b 0] by auto
+
+lemma even_or_iff:
+  \<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close>
+  using bit_or_iff [of a b 0] by auto
+
+lemma even_xor_iff:
+  \<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close>
+  using bit_xor_iff [of a b 0] by auto
+
 lemma zero_and_eq [simp]:
   "0 AND a = 0"
   by (simp add: bit_eq_iff bit_and_iff)
@@ -46,26 +58,26 @@
   by (simp add: bit_eq_iff bit_and_iff)
 
 lemma one_and_eq [simp]:
-  "1 AND a = of_bool (odd a)"
+  "1 AND a = a mod 2"
   by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
 
 lemma and_one_eq [simp]:
-  "a AND 1 = of_bool (odd a)"
+  "a AND 1 = a mod 2"
   using one_and_eq [of a] by (simp add: ac_simps)
 
-lemma one_or_eq [simp]:
+lemma one_or_eq:
   "1 OR a = a + of_bool (even a)"
   by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff)
 
-lemma or_one_eq [simp]:
+lemma or_one_eq:
   "a OR 1 = a + of_bool (even a)"
   using one_or_eq [of a] by (simp add: ac_simps)
 
-lemma one_xor_eq [simp]:
+lemma one_xor_eq:
   "1 XOR a = a + of_bool (even a) - of_bool (odd a)"
   by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE)
 
-lemma xor_one_eq [simp]:
+lemma xor_one_eq:
   "a XOR 1 = a + of_bool (even a) - of_bool (odd a)"
   using one_xor_eq [of a] by (simp add: ac_simps)
 
@@ -81,6 +93,41 @@
   \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
 
+definition mask :: \<open>nat \<Rightarrow> 'a\<close>
+  where mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
+
+lemma bit_mask_iff:
+  \<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
+  by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
+
+lemma even_mask_iff:
+  \<open>even (mask n) \<longleftrightarrow> n = 0\<close>
+  using bit_mask_iff [of n 0] by auto
+
+lemma mask_0 [simp, code]:
+  \<open>mask 0 = 0\<close>
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma mask_Suc_exp [code]:
+  \<open>mask (Suc n) = 2 ^ n OR mask n\<close>
+  by (rule bit_eqI)
+    (auto simp add: bit_or_iff bit_mask_iff bit_exp_iff not_less le_less_Suc_eq)
+
+lemma mask_Suc_double:
+  \<open>mask (Suc n) = 2 * mask n OR 1\<close>
+proof (rule bit_eqI)
+  fix q
+  assume \<open>2 ^ q \<noteq> 0\<close>
+  show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (2 * mask n OR 1) q\<close>
+    by (cases q)
+      (simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2)
+qed
+
+lemma take_bit_eq_mask [code]:
+  \<open>take_bit n a = a AND mask n\<close>
+  by (rule bit_eqI)
+    (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
@@ -226,7 +273,7 @@
       (cases m, simp_all add: bit_Suc)
 qed
 
-lemma set_bit_Suc [simp]:
+lemma set_bit_Suc:
   \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
 proof (rule bit_eqI)
   fix m
@@ -257,7 +304,7 @@
       (cases m, simp_all add: bit_Suc)
 qed
 
-lemma unset_bit_Suc [simp]:
+lemma unset_bit_Suc:
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
 proof (rule bit_eqI)
   fix m
@@ -286,7 +333,7 @@
       (cases m, simp_all add: bit_Suc)
 qed
 
-lemma flip_bit_Suc [simp]:
+lemma flip_bit_Suc:
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
 proof (rule bit_eqI)
   fix m
@@ -533,26 +580,26 @@
   by (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
 
 lemma Suc_0_and_eq [simp]:
-  \<open>Suc 0 AND n = of_bool (odd n)\<close>
+  \<open>Suc 0 AND n = n mod 2\<close>
   using one_and_eq [of n] by simp
 
 lemma and_Suc_0_eq [simp]:
-  \<open>n AND Suc 0 = of_bool (odd n)\<close>
+  \<open>n AND Suc 0 = n mod 2\<close>
   using and_one_eq [of n] by simp
 
-lemma Suc_0_or_eq [simp]:
+lemma Suc_0_or_eq:
   \<open>Suc 0 OR n = n + of_bool (even n)\<close>
   using one_or_eq [of n] by simp
 
-lemma or_Suc_0_eq [simp]:
+lemma or_Suc_0_eq:
   \<open>n OR Suc 0 = n + of_bool (even n)\<close>
   using or_one_eq [of n] by simp
 
-lemma Suc_0_xor_eq [simp]:
+lemma Suc_0_xor_eq:
   \<open>Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\<close>
   using one_xor_eq [of n] by simp
 
-lemma xor_Suc_0_eq [simp]:
+lemma xor_Suc_0_eq:
   \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
   using xor_one_eq [of n] by simp
 
@@ -679,7 +726,7 @@
 
       \<^item> Singleton \<^term>\<open>n\<close>th bit: \<^term>\<open>(2 :: int) ^ n\<close>
 
-      \<^item> Bit mask upto bit \<^term>\<open>n\<close>: \<^term>\<open>(2 :: int) ^ n - 1\<close>
+      \<^item> Bit mask upto bit \<^term>\<open>n\<close>: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]}}
 
       \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]}
 
diff -r 95d2d5e60419 -r 3ef1418d64a6 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Fri May 08 13:19:55 2020 +0200
+++ b/src/HOL/ex/Word.thy	Fri May 08 13:20:02 2020 +0200
@@ -592,7 +592,8 @@
   show \<open>(1 + a) div 2 = a div 2\<close>
     if \<open>even a\<close>
     for a :: \<open>'a word\<close>
-    using that by transfer (auto dest: le_Suc_ex simp add: take_bit_Suc)
+    using that by transfer
+      (auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE)
   show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
     for m n :: nat
     by transfer (simp, simp add: exp_div_exp_eq)