diff -r eed4ca224c9c -r 74a4776f7a22 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sat Nov 18 19:23:56 2023 +0100
+++ b/src/HOL/Bit_Operations.thy	Sun Nov 19 15:45:22 2023 +0000
@@ -715,9 +715,9 @@
     and push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
     and drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
     and take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  assumes bit_and_iff [bit_simps]: \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
-    and bit_or_iff [bit_simps]: \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
-    and bit_xor_iff [bit_simps]: \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+  assumes and_rec: \<open>a AND b = of_bool (odd a \<and> odd b) + 2 * ((a div 2) AND (b div 2))\<close>
+    and or_rec: \<open>a OR b = of_bool (odd a \<or> odd b) + 2 * ((a div 2) OR (b div 2))\<close>
+    and xor_rec: \<open>a XOR b = of_bool (odd a \<noteq> odd b) + 2 * ((a div 2) XOR (b div 2))\<close>
     and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
     and set_bit_eq_or: \<open>set_bit n a = a OR push_bit n 1\<close>
     and bit_unset_bit_iff [bit_simps]: \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
@@ -743,6 +743,48 @@
   differently wrt. code generation.
 \<close>
 
+lemma bit_and_iff [bit_simps]:
+  \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+proof (induction n arbitrary: a b)
+  case 0
+  show ?case
+    by (simp add: bit_0 and_rec [of a b] even_bit_succ_iff)
+next
+  case (Suc n)
+  from Suc [of \<open>a div 2\<close> \<open>b div 2\<close>]
+  show ?case
+    by (simp add: and_rec [of a b] bit_Suc)
+      (auto simp flip: bit_Suc simp add: bit_double_iff dest: bit_imp_possible_bit)
+qed
+
+lemma bit_or_iff [bit_simps]:
+  \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+proof (induction n arbitrary: a b)
+  case 0
+  show ?case
+    by (simp add: bit_0 or_rec [of a b] even_bit_succ_iff)
+next
+  case (Suc n)
+  from Suc [of \<open>a div 2\<close> \<open>b div 2\<close>]
+  show ?case
+    by (simp add: or_rec [of a b] bit_Suc)
+      (auto simp flip: bit_Suc simp add: bit_double_iff dest: bit_imp_possible_bit)
+qed
+
+lemma bit_xor_iff [bit_simps]:
+  \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+proof (induction n arbitrary: a b)
+  case 0
+  show ?case
+    by (simp add: bit_0 xor_rec [of a b] even_bit_succ_iff)
+next
+  case (Suc n)
+  from Suc [of \<open>a div 2\<close> \<open>b div 2\<close>]
+  show ?case
+    by (simp add: xor_rec [of a b] bit_Suc)
+      (auto simp flip: bit_Suc simp add: bit_double_iff dest: bit_imp_possible_bit)
+qed
+
 sublocale "and": semilattice \<open>(AND)\<close>
   by standard (auto simp add: bit_eq_iff bit_and_iff)
 
@@ -1606,12 +1648,12 @@
   fix k l :: int and m n :: nat
   show \<open>- k = NOT (k - 1)\<close>
     by (simp add: not_int_def)
-  show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
-    by (fact bit_and_int_iff)
-  show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-    by (fact bit_or_int_iff)
-  show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
-    by (fact bit_xor_int_iff)
+  show \<open>k AND l = of_bool (odd k \<and> odd l) + 2 * (k div 2 AND l div 2)\<close>
+    by (fact and_int_rec)
+  show \<open>k OR l = of_bool (odd k \<or> odd l) + 2 * (k div 2 OR l div 2)\<close>
+    by (fact or_int_rec)
+  show \<open>k XOR l = of_bool (odd k \<noteq> odd l) + 2 * (k div 2 XOR l div 2)\<close>
+    by (fact xor_int_rec)
   show \<open>bit (unset_bit m k) n \<longleftrightarrow> bit k n \<and> m \<noteq> n\<close>
   proof -
     have \<open>unset_bit m k = k AND NOT (push_bit m 1)\<close>
@@ -2376,12 +2418,12 @@
 
 instance proof
   fix m n q :: nat
-  show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
-    by (simp add: and_nat_def bit_simps)
-  show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
-    by (simp add: or_nat_def bit_simps)
-  show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
-    by (simp add: xor_nat_def bit_simps)
+  show \<open>m AND n = of_bool (odd m \<and> odd n) + 2 * (m div 2 AND n div 2)\<close>
+    by (simp add: and_nat_def and_rec [of \<open>int m\<close> \<open>int n\<close>] nat_add_distrib of_nat_div)
+  show \<open>m OR n = of_bool (odd m \<or> odd n) + 2 * (m div 2 OR n div 2)\<close>
+    by (simp add: or_nat_def or_rec [of \<open>int m\<close> \<open>int n\<close>] nat_add_distrib of_nat_div)
+  show \<open>m XOR n = of_bool (odd m \<noteq> odd n) + 2 * (m div 2 XOR n div 2)\<close>
+    by (simp add: xor_nat_def xor_rec [of \<open>int m\<close> \<open>int n\<close>] nat_add_distrib of_nat_div)
   show \<open>bit (unset_bit m n) q \<longleftrightarrow> bit n q \<and> m \<noteq> q\<close>
     by (simp add: unset_bit_nat_def bit_simps)
 qed (simp_all add: mask_nat_def set_bit_nat_def flip_bit_nat_def push_bit_nat_def drop_bit_nat_def take_bit_nat_def)