# HG changeset patch
# User haftmann
# Date 1700408722 0
# Node ID 74a4776f7a222dd37dcef12c54ad18971ca2adbf
# Parent  eed4ca224c9c1030b8484c759d88e7810ab56698
operations AND, OR, XOR are specified by characteristic recursive equation

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)
diff -r eed4ca224c9c -r 74a4776f7a22 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Nov 18 19:23:56 2023 +0100
+++ b/src/HOL/Code_Numeral.thy	Sun Nov 19 15:45:22 2023 +0000
@@ -352,7 +352,7 @@
     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
-    bit_and_iff bit_or_iff bit_xor_iff mask_eq_exp_minus_1
+    and_rec or_rec xor_rec mask_eq_exp_minus_1
     set_bit_def bit_unset_bit_iff flip_bit_def bit_not_iff_eq minus_eq_not_minus_1)+
 
 end
@@ -1110,7 +1110,7 @@
   (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     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 bit_and_iff bit_or_iff bit_xor_iff
+    even_mask_div_iff even_mult_exp_div_exp_iff and_rec or_rec xor_rec
     mask_eq_exp_minus_1 set_bit_def bit_unset_bit_iff flip_bit_def)+
 
 end
diff -r eed4ca224c9c -r 74a4776f7a22 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Nov 18 19:23:56 2023 +0100
+++ b/src/HOL/Library/Word.thy	Sun Nov 19 15:45:22 2023 +0000
@@ -991,12 +991,51 @@
   is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
   by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
 
-instance apply (standard; transfer)
-  apply (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
-    bit_simps set_bit_def flip_bit_def take_bit_drop_bit
-    simp flip: drop_bit_eq_div take_bit_eq_mod)
-   apply (simp_all add: drop_bit_take_bit flip: push_bit_eq_mult)
-  done
+context
+  includes bit_operations_syntax
+begin
+
+instance proof
+  fix v w :: \<open>'a word\<close> and n m :: nat
+  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)
+    apply (auto simp add: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
+    done
+  show \<open>v OR w = of_bool (odd v \<or> odd w) + 2 * (v div 2 OR w 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)
+    done
+  show \<open>v XOR w = of_bool (odd v \<noteq> odd w) + 2 * (v div 2 XOR w div 2)\<close>
+    apply transfer
+    apply (rule bit_eqI)
+    subgoal for k l n
+      apply (cases n)
+       apply (auto simp add: even_bit_succ_iff bit_simps bit_0 even_xor_iff simp flip: bit_Suc)
+      done
+    done
+  show \<open>mask n = 2 ^ n - (1 :: 'a word)\<close>
+    by transfer (simp flip: mask_eq_exp_minus_1)
+  show \<open>set_bit n v = v OR push_bit n 1\<close>
+    by transfer (simp add: take_bit_set_bit_eq set_bit_eq_or)
+  show \<open>bit (unset_bit m v) n \<longleftrightarrow> bit v n \<and> m \<noteq> n\<close>
+    by transfer (simp add: bit_simps)
+  show \<open>flip_bit n v = v XOR push_bit n 1\<close>
+    by transfer (simp add: take_bit_flip_bit_eq flip_bit_eq_xor)
+  show \<open>push_bit n v = v * 2 ^ n\<close>
+    by transfer (simp add: push_bit_eq_mult)
+  show \<open>drop_bit n v = v div 2 ^ n\<close>
+    by transfer (simp add: drop_bit_take_bit flip: drop_bit_eq_div)
+  show \<open>take_bit n v = v mod 2 ^ n\<close>
+    by transfer (simp flip: take_bit_eq_mod)
+  show \<open>bit (NOT v) n \<longleftrightarrow> 2 ^ n \<noteq> (0 :: 'a word) \<and> \<not> bit v n\<close>
+    by transfer (auto simp add: bit_simps)
+  show \<open>- v = NOT (v - 1)\<close>
+    by transfer (simp add: minus_eq_not_minus_1)
+qed
+
+end
 
 end