# HG changeset patch
# User haftmann
# Date 1599294747 0
# Node ID 12e94c2ff6c5cac4b212b11a95e8507da1f2af87
# Parent  7fc0e882851ce59bbc652b2d4917012c23a2fc9d
generalized

diff -r 7fc0e882851c -r 12e94c2ff6c5 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Fri Sep 04 17:32:42 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy	Sat Sep 05 08:32:27 2020 +0000
@@ -95,6 +95,30 @@
   \<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)
 
+lemma push_bit_and [simp]:
+  \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff)
+
+lemma push_bit_or [simp]:
+  \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff)
+
+lemma push_bit_xor [simp]:
+  \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff)
+
+lemma drop_bit_and [simp]:
+  \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff)
+
+lemma drop_bit_or [simp]:
+  \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff)
+
+lemma drop_bit_xor [simp]:
+  \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
+
 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)
@@ -135,6 +159,10 @@
   by (rule bit_eqI)
     (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
 
+lemma disjunctive_add:
+  \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+  by (rule bit_eqI) (use that in \<open>simp add: bit_disjunctive_add_iff bit_or_iff\<close>)
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
@@ -191,25 +219,18 @@
   by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
 
 sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
-  apply standard
-  apply (simp add: bit_eq_iff bit_and_iff)
-  apply (auto simp add: exp_eq_0_imp_not_bit bit_exp_iff)
-  done
+  by standard (rule bit_eqI, simp add: bit_and_iff)
 
 sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
   rewrites \<open>bit.xor = (XOR)\<close>
 proof -
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
-    apply standard
-         apply (simp_all add: bit_eq_iff)
-       apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
-    done
+    by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)
   show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
     by standard
   show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
-    apply (simp add: fun_eq_iff bit_eq_iff bit.xor_def)
-    apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_xor_iff exp_eq_0_imp_not_bit)
-    done
+    by (rule ext, rule ext, rule bit_eqI)
+      (auto simp add: bit.xor_def bit_and_iff bit_or_iff bit_xor_iff bit_not_iff)
 qed
 
 lemma and_eq_not_not_or:
@@ -228,6 +249,17 @@
   \<open>NOT (a - b) = NOT a + b\<close>
   using not_add_distrib [of a \<open>- b\<close>] by simp
 
+lemma disjunctive_diff:
+  \<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
+proof -
+  have \<open>NOT a + b = NOT a OR b\<close>
+    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
+  then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
+    by simp
+  then show ?thesis
+    by (simp add: not_add_distrib)
+qed
+
 lemma push_bit_minus:
   \<open>push_bit n (- a) = - push_bit n a\<close>
   by (simp add: push_bit_eq_mult)
@@ -238,9 +270,9 @@
 
 lemma take_bit_not_iff:
   "take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b"
-  apply (simp add: bit_eq_iff bit_not_iff bit_take_bit_iff)
-  apply (simp add: bit_exp_iff)
-  apply (use local.exp_eq_0_imp_not_bit in blast)
+  apply (simp add: bit_eq_iff)
+  apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
+  apply (use exp_eq_0_imp_not_bit in blast)
   done
 
 lemma mask_eq_take_bit_minus_one:
@@ -519,40 +551,6 @@
 
 end
 
-lemma disjunctive_add:
-  \<open>k + l = k OR l\<close> if \<open>\<And>n. \<not> bit k n \<or> \<not> bit l n\<close> for k l :: int
-  \<comment> \<open>TODO: may integrate (indirectly) into \<^class>\<open>semiring_bits\<close> premises\<close>
-proof (rule bit_eqI)
-  fix n
-  from that have \<open>bit (k + l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-  proof (induction n arbitrary: k l)
-    case 0
-    from this [of 0] show ?case
-      by auto
-  next
-    case (Suc n)
-    have \<open>bit ((k + l) div 2) n \<longleftrightarrow> bit (k div 2 + l div 2) n\<close>
-      using Suc.prems [of 0] div_add1_eq [of k l] by auto
-    also have \<open>bit (k div 2 + l div 2) n \<longleftrightarrow> bit (k div 2) n \<or> bit (l div 2) n\<close>
-      by (rule Suc.IH) (use Suc.prems in \<open>simp flip: bit_Suc\<close>)
-    finally show ?case
-      by (simp add: bit_Suc)
-  qed
-  also have \<open>\<dots> \<longleftrightarrow> bit (k OR l) n\<close>
-    by (simp add: bit_or_iff)
-  finally show \<open>bit (k + l) n \<longleftrightarrow> bit (k OR l) n\<close> .
-qed
-
-lemma disjunctive_diff:
-  \<open>k - l = k AND NOT l\<close> if \<open>\<And>n. bit l n \<Longrightarrow> bit k n\<close> for k l :: int
-proof -
-  have \<open>NOT k + l = NOT k OR l\<close>
-    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
-  then have \<open>NOT (NOT k + l) = NOT (NOT k OR l)\<close>
-    by simp
-  then show ?thesis
-    by (simp add: not_add_distrib)
-qed
 
 lemma mask_nonnegative_int [simp]:
   \<open>mask n \<ge> (0::int)\<close>
@@ -1129,7 +1127,7 @@
   (let l = take_bit (Suc n) k
    in if bit l n then l - (push_bit n 2) else l)\<close>
 proof -
-  have *: \<open>(take_bit (Suc n) k) - 2 * 2 ^ n = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
+  have *: \<open>take_bit (Suc n) k - 2 * 2 ^ n = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
     apply (subst disjunctive_add [symmetric])
     apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff bit_take_bit_iff)
     apply (simp flip: minus_exp_eq_not_mask)
@@ -1362,38 +1360,9 @@
 
       \<^item> Bit concatenation: @{thm concat_bit_def [no_vars]}
 
-      \<^item> Truncation centered towards \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]}
+      \<^item> Signed truncation, or modulus centered around \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]}
 
       \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 \<close>
 
-context semiring_bit_operations
-begin
-
-lemma push_bit_and [simp]:
-  \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff)
-
-lemma push_bit_or [simp]:
-  \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff)
-
-lemma push_bit_xor [simp]:
-  \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff)
-
-lemma drop_bit_and [simp]:
-  \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff)
-
-lemma drop_bit_or [simp]:
-  \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff)
-
-lemma drop_bit_xor [simp]:
-  \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
-
 end
-
-end
diff -r 7fc0e882851c -r 12e94c2ff6c5 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Sep 04 17:32:42 2020 +0100
+++ b/src/HOL/Parity.thy	Sat Sep 05 08:32:27 2020 +0000
@@ -990,6 +990,40 @@
     by simp_all
 qed
 
+lemma bit_disjunctive_add_iff:
+  \<open>bit (a + b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+  if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+proof (cases \<open>2 ^ n = 0\<close>)
+  case True
+  then show ?thesis
+    by (simp add: exp_eq_0_imp_not_bit)
+next
+  case False
+  with that show ?thesis proof (induction n arbitrary: a b)
+    case 0
+    from "0.prems"(1) [of 0] show ?case
+      by auto
+  next
+    case (Suc n)
+    from Suc.prems(1) [of 0] have even: \<open>even a \<or> even b\<close>
+      by auto
+    have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
+      using Suc.prems(1) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
+    from Suc.prems(2) have \<open>2 * 2 ^ n \<noteq> 0\<close> \<open>2 ^ n \<noteq> 0\<close>
+      by (auto simp add: mult_2)
+    have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
+      using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
+    also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
+      using even by (auto simp add: algebra_simps mod2_eq_if)
+    finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
+      using \<open>2 * 2 ^ n \<noteq> 0\<close> by simp (simp flip: bit_Suc add: bit_double_iff)
+    also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
+      using bit \<open>2 ^ n \<noteq> 0\<close> by (rule Suc.IH)
+    finally show ?case
+      by (simp add: bit_Suc)
+  qed
+qed
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
diff -r 7fc0e882851c -r 12e94c2ff6c5 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Sep 04 17:32:42 2020 +0100
+++ b/src/HOL/Word/Word.thy	Sat Sep 05 08:32:27 2020 +0000
@@ -4172,7 +4172,7 @@
   apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
   apply (auto dest: bit_imp_le_length)
    apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
-  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' bit_imp_le_length div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
+  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
   done
 
 lemma word_rot_lr [simp]:
@@ -4181,7 +4181,7 @@
   apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
   apply (auto dest: bit_imp_le_length)
    apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
-  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' bit_imp_le_length div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
+  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
   done
 
 lemma word_rot_gal: