# HG changeset patch
# User haftmann
# Date 1701193166 0
# Node ID a91050cd5c93cd297fa30b1a5b23ed902be11874
# Parent  7ab8b3f1d84b3bc53f6965f83bad09a71cb1ef8e
de-duplicated specification of class ring_bit_operations

diff -r 7ab8b3f1d84b -r a91050cd5c93 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sun Nov 26 21:06:47 2023 +0000
+++ b/src/HOL/Bit_Operations.thy	Tue Nov 28 17:39:26 2023 +0000
@@ -652,43 +652,6 @@
   \<open>possible_bit TYPE(int) n\<close>
   by (simp add: possible_bit_def)
 
-lemma bit_not_int_iff':
-  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
-proof (induction n arbitrary: k)
-  case 0
-  show ?case
-    by (simp add: bit_0)
-next
-  case (Suc n)
-  have \<open>- k - 1 = - (k + 2) + 1\<close>
-    by simp
-  also have \<open>(- (k + 2) + 1) div 2 = - (k div 2) - 1\<close>
-  proof (cases \<open>even k\<close>)
-    case True
-    then have \<open>- k div 2 = - (k div 2)\<close>
-      by rule (simp flip: mult_minus_right)
-    with True show ?thesis
-      by simp
-  next
-    case False
-    have \<open>4 = 2 * (2::int)\<close>
-      by simp
-    also have \<open>2 * 2 div 2 = (2::int)\<close>
-      by (simp only: nonzero_mult_div_cancel_left)
-    finally have *: \<open>4 div 2 = (2::int)\<close> .
-    from False obtain l where k: \<open>k = 2 * l + 1\<close> ..
-    then have \<open>- k - 2 = 2 * - (l + 2) + 1\<close>
-      by simp
-    then have \<open>(- k - 2) div 2 + 1 = - (k div 2) - 1\<close>
-      by (simp flip: mult_minus_right add: *) (simp add: k)
-    with False show ?thesis
-      by simp
-  qed
-  finally have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close> .
-  with Suc show ?case
-    by (simp add: bit_Suc)
-qed
-
 lemma bit_nat_iff [bit_simps]:
   \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
 proof (cases \<open>k \<ge> 0\<close>)
@@ -1353,8 +1316,7 @@
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
   fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
-  assumes not_rec: \<open>NOT a = of_bool (even a) + 2 * NOT (a div 2)\<close>
-  assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
+  assumes not_eq_complement: \<open>NOT a = - a - 1\<close>
 begin
 
 text \<open>
@@ -1368,17 +1330,21 @@
   \<open>(- 1) mod 2 = 1\<close>
   by (simp add: mod_2_eq_odd)
 
-lemma not_eq_complement:
-  \<open>NOT a = - a - 1\<close>
-  using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp
-
 lemma minus_eq_not_plus_1:
   \<open>- a = NOT a + 1\<close>
   using not_eq_complement [of a] by simp
 
+lemma minus_eq_not_minus_1:
+  \<open>- a = NOT (a - 1)\<close>
+  using not_eq_complement [of \<open>a - 1\<close>] by simp (simp add: algebra_simps)
+
+lemma not_rec:
+  \<open>NOT a = of_bool (even a) + 2 * NOT (a div 2)\<close>
+  by (simp add: not_eq_complement algebra_simps mod_2_eq_odd flip: minus_mod_eq_mult_div)
+
 lemma even_not_iff [simp]:
   \<open>even (NOT a) \<longleftrightarrow> odd a\<close>
-  by (simp add: not_rec [of a])
+  by (simp add: not_eq_complement)
 
 lemma bit_not_iff [bit_simps]:
   \<open>bit (NOT a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit a n\<close>
@@ -1822,17 +1788,24 @@
 definition flip_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>flip_bit n k = k XOR push_bit n 1\<close> for k :: int
 
+lemma not_int_div_2:
+  \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
+  by (simp add: not_int_def)
+
 lemma bit_not_int_iff:
-  \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
-  for k :: int
-  by (simp add: bit_not_int_iff' not_int_def)
+  \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
+proof (rule sym, induction n arbitrary: k)
+  case 0
+  then show ?case
+    by (simp add: bit_0 not_int_def)
+next
+  case (Suc n)
+  then show ?case
+    by (simp add: bit_Suc not_int_div_2)
+qed
 
 instance proof
   fix k l :: int and m n :: nat
-  show \<open>- k = NOT (k - 1)\<close>
-    by (simp add: not_int_def)
-  show \<open>NOT k = of_bool (even k) + 2 * NOT (k div 2)\<close>
-    by (auto simp add: not_int_def elim: oddE)
   show \<open>unset_bit 0 k = 2 * (k div 2)\<close>
     by (rule bit_eqI)
       (auto simp add: unset_bit_int_def push_bit_int_def and_int.bit_iff bit_not_int_iff bit_simps simp flip: bit_Suc)
@@ -1840,7 +1813,7 @@
     by (rule bit_eqI)
       (auto simp add: unset_bit_int_def push_bit_int_def and_int.bit_iff bit_not_int_iff bit_simps mod_2_eq_odd even_bit_succ_iff bit_0 simp flip: bit_Suc)
 qed (fact and_int.rec or_int.rec xor_int.rec mask_int_def set_bit_int_def flip_bit_int_def
-  push_bit_int_def drop_bit_int_def take_bit_int_def)+
+  push_bit_int_def drop_bit_int_def take_bit_int_def not_int_def)+
 
 end
 
@@ -1929,10 +1902,6 @@
 
 end
 
-lemma not_int_div_2:
-  \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
-  by (simp add: not_int_def)
-
 lemma take_bit_int_less_exp [simp]:
   \<open>take_bit n k < 2 ^ n\<close> for k :: int
   by (simp add: take_bit_eq_mod)
@@ -3850,6 +3819,10 @@
   \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
   by (fact bit_push_bit_iff')
 
+lemma bit_not_int_iff':
+  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
+  by (simp flip: not_eq_complement add: bit_simps)
+
 no_notation
   not  (\<open>NOT\<close>)
     and "and"  (infixr \<open>AND\<close> 64)
diff -r 7ab8b3f1d84b -r a91050cd5c93 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Nov 26 21:06:47 2023 +0000
+++ b/src/HOL/Code_Numeral.thy	Tue Nov 28 17:39:26 2023 +0000
@@ -352,8 +352,8 @@
     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
     even_mask_div_iff even_mult_exp_div_exp_iff
-    and_rec or_rec xor_rec mask_eq_exp_minus_1 not_rec
-    set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def not_rec minus_eq_not_minus_1)+
+    and_rec or_rec xor_rec mask_eq_exp_minus_1
+    set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def not_eq_complement)+
 
 end
 
diff -r 7ab8b3f1d84b -r a91050cd5c93 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Nov 26 21:06:47 2023 +0000
+++ b/src/HOL/Library/Word.thy	Tue Nov 28 17:39:26 2023 +0000
@@ -997,15 +997,8 @@
 
 instance proof
   fix v w :: \<open>'a word\<close> and n m :: nat
-  show \<open>NOT v = of_bool (even v) + 2 * NOT (v div 2)\<close>
-    apply transfer
-    apply (rule bit_eqI)
-    apply (auto simp add: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
-     apply (metis Suc_pred bit_0 not_gr_zero)
-    using odd_bit_iff_bit_pred apply blast
-    done
-  show \<open>- v = NOT (v - 1)\<close>
-    by transfer (simp add: minus_eq_not_minus_1)
+  show \<open>NOT v = - v - 1\<close>
+    by transfer (simp add: not_eq_complement)
   show \<open>v AND w = of_bool (odd v \<and> odd w) + 2 * (v div 2 AND w div 2)\<close>
     apply transfer
     apply (rule bit_eqI)
diff -r 7ab8b3f1d84b -r a91050cd5c93 src/HOL/Library/Z2.thy
--- a/src/HOL/Library/Z2.thy	Sun Nov 26 21:06:47 2023 +0000
+++ b/src/HOL/Library/Z2.thy	Tue Nov 28 17:39:26 2023 +0000
@@ -155,9 +155,8 @@
 
 instance
   apply standard
-  apply simp_all
-  apply (simp only: Z2.bit_eq_iff even_add)
-  apply simp
+      apply simp_all
+  apply (simp only: Z2.bit_eq_iff even_add even_zero refl)
   done
 
 end
@@ -169,10 +168,8 @@
   where [simp]: \<open>bit_bit b n \<longleftrightarrow> odd b \<and> n = 0\<close>
 
 instance
-  apply standard
-              apply auto
-  apply (metis bit.exhaust of_bool_eq(2))
-  done
+  by standard
+    (auto intro: Abs_bit_induct simp add: Abs_bit_eq_of_bool)
 
 end
 
@@ -219,10 +216,7 @@
 end
 
 instance
-  apply standard
-             apply auto
-  apply (simp only: Z2.bit_eq_iff even_add even_zero)
-  done
+  by standard auto
 
 end