--- a/src/HOL/Bit_Operations.thy Sun Feb 11 12:52:14 2024 +0000
+++ b/src/HOL/Bit_Operations.thy Mon Feb 12 09:30:22 2024 +0000
@@ -885,6 +885,10 @@
qed
qed
+lemma funpow_double_eq_push_bit:
+ \<open>times 2 ^^ n = push_bit n\<close>
+ by (induction n) (simp_all add: fun_eq_iff push_bit_double ac_simps)
+
lemma div_push_bit_of_1_eq_drop_bit:
\<open>a div push_bit n 1 = drop_bit n a\<close>
by (simp add: push_bit_eq_mult drop_bit_eq_div)
@@ -1318,6 +1322,10 @@
\<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 decr_eq_not_minus:
+ \<open>a - 1 = NOT (- a)\<close>
+ using not_eq_complement [of \<open>- a\<close>] by simp
+
lemma even_not_iff [simp]:
\<open>even (NOT a) \<longleftrightarrow> odd a\<close>
by (simp add: not_eq_complement)
@@ -1365,6 +1373,10 @@
\<open>bit (- 2) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n > 0\<close>
by (simp add: bit_minus_iff bit_1_iff)
+lemma bit_decr_iff:
+ \<open>bit (a - 1) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit (- a) n\<close>
+ by (simp add: decr_eq_not_minus bit_not_iff)
+
lemma bit_not_iff_eq:
\<open>bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
by (simp add: bit_simps possible_bit_def)
@@ -2688,6 +2700,17 @@
\<open>bit (numeral (Num.Bit1 m)) 0\<close>
by (simp add: bit_0)
+lemma bit_numeral_Bit0_iff:
+ \<open>bit (numeral (num.Bit0 m)) n
+ \<longleftrightarrow> possible_bit TYPE('a) n \<and> n > 0 \<and> bit (numeral m) (n - 1)\<close>
+ by (simp only: numeral_Bit0_eq_double [of m] bit_simps) simp
+
+lemma bit_numeral_Bit1_Suc_iff:
+ \<open>bit (numeral (num.Bit1 m)) (Suc n)
+ \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> bit (numeral m) n\<close>
+ using even_bit_succ_iff [of \<open>2 * numeral m\<close> \<open>Suc n\<close>]
+ by (simp only: numeral_Bit1_eq_inc_double [of m] bit_simps) simp
+
end
context ring_bit_operations
@@ -2701,6 +2724,26 @@
\<open>bit (- numeral (Num.Bit1 m)) 0\<close>
by (simp add: bit_0)
+lemma bit_minus_numeral_Bit0_Suc_iff:
+ \<open>bit (- numeral (num.Bit0 m)) (Suc n)
+ \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> bit (- numeral m) n\<close>
+ by (simp only: numeral_Bit0_eq_double [of m] minus_mult_right bit_simps) auto
+
+lemma bit_minus_numeral_Bit1_Suc_iff:
+ \<open>bit (- numeral (num.Bit1 m)) (Suc n)
+ \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> \<not> bit (numeral m) n\<close>
+ by (simp only: numeral_Bit1_eq_inc_double [of m] minus_add_distrib minus_mult_right add_uminus_conv_diff
+ bit_decr_iff bit_double_iff)
+ auto
+
+lemma bit_numeral_BitM_0 [simp]:
+ \<open>bit (numeral (Num.BitM m)) 0\<close>
+ by (simp only: numeral_BitM bit_decr_iff not_bit_minus_numeral_Bit0_0) simp
+
+lemma bit_numeral_BitM_Suc_iff:
+ \<open>bit (numeral (Num.BitM m)) (Suc n) \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> \<not> bit (- numeral m) n\<close>
+ by (simp_all only: numeral_BitM bit_decr_iff bit_minus_numeral_Bit0_Suc_iff) auto
+
end
context linordered_euclidean_semiring_bit_operations
--- a/src/HOL/Library/Word.thy Sun Feb 11 12:52:14 2024 +0000
+++ b/src/HOL/Library/Word.thy Mon Feb 12 09:30:22 2024 +0000
@@ -3297,6 +3297,14 @@
lemmas word_eq_numeral_iff_iszero [simp] =
eq_numeral_iff_iszero [where 'a="'a::len word"]
+lemma word_less_eq_imp_half_less_eq:
+ \<open>v div 2 \<le> w div 2\<close> if \<open>v \<le> w\<close> for v w :: \<open>'a::len word\<close>
+ using that by (simp add: word_le_nat_alt unat_div div_le_mono)
+
+lemma word_half_less_imp_less_eq:
+ \<open>v \<le> w\<close> if \<open>v div 2 < w div 2\<close> for v w :: \<open>'a::len word\<close>
+ using that linorder_linear word_less_eq_imp_half_less_eq by fastforce
+
subsection \<open>Word and nat\<close>
--- a/src/HOL/Num.thy Sun Feb 11 12:52:14 2024 +0000
+++ b/src/HOL/Num.thy Mon Feb 12 09:30:22 2024 +0000
@@ -564,6 +564,14 @@
"a + (a + b) = 2 * a + b"
by (simp add: mult_2 ac_simps)
+lemma numeral_Bit0_eq_double:
+ \<open>numeral (num.Bit0 n) = 2 * numeral n\<close>
+ by (simp add: mult_2) (simp add: numeral_Bit0)
+
+lemma numeral_Bit1_eq_inc_double:
+ \<open>numeral (num.Bit1 n) = 2 * numeral n + 1\<close>
+ by (simp add: mult_2) (simp add: numeral_Bit1)
+
end