# HG changeset patch
# User haftmann
# Date 1707730222 0
# Node ID b14c4cb37d99a1035780b480090a76183d808377
# Parent  9dee3b4fdb063b69ceb4378da94f951f76b50fa5
more lemmas

diff -r 9dee3b4fdb06 -r b14c4cb37d99 src/HOL/Bit_Operations.thy
--- 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
diff -r 9dee3b4fdb06 -r b14c4cb37d99 src/HOL/Library/Word.thy
--- 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>
 
diff -r 9dee3b4fdb06 -r b14c4cb37d99 src/HOL/Num.thy
--- 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