--- 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)
--- 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
--- 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