# HG changeset patch
# User haftmann
# Date 1707242923 0
# Node ID dafb3d343cd63c2b131bebf7d9d85e10fa55de10
# Parent  924e487288fb1070cc0d47491046597941c67cc4
more lemmas and more correct lemma names

diff -r 924e487288fb -r dafb3d343cd6 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Wed Feb 07 11:57:22 2024 +0000
+++ b/src/HOL/Bit_Operations.thy	Tue Feb 06 18:08:43 2024 +0000
@@ -17,7 +17,7 @@
   assumes half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
     and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close>
     and even_decr_exp_div_exp_iff: \<open>2 ^ n \<noteq> 0 \<Longrightarrow> even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close>
-    and even_mod_exp_diff_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
+    and even_mod_exp_div_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
   fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
   assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
 begin
@@ -80,7 +80,7 @@
 
 end
 
-lemma bit_iff_idd_imp_stable:
+lemma bit_iff_odd_imp_stable:
   \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close>
 using that proof (induction a rule: bit_induct)
   case (stable a)
@@ -182,7 +182,7 @@
     from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
       by (simp add: bit_0)
     have \<open>b div 2 = b\<close>
-    proof (rule bit_iff_idd_imp_stable)
+    proof (rule bit_iff_odd_imp_stable)
       fix n
       from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close>
         by simp
@@ -870,7 +870,7 @@
 
 lemma bit_take_bit_iff [bit_simps]:
   \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
-  by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_diff_exp_iff not_le)
+  by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_div_exp_iff not_le)
 
 lemma take_bit_Suc:
   \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
diff -r 924e487288fb -r dafb3d343cd6 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Feb 07 11:57:22 2024 +0000
+++ b/src/HOL/Code_Numeral.thy	Tue Feb 06 18:08:43 2024 +0000
@@ -349,7 +349,7 @@
 
 instance by (standard; transfer)
   (fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
-    half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_diff_exp_iff
+    half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_div_exp_iff
     bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     and_rec or_rec xor_rec mask_eq_exp_minus_1
     set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
@@ -1109,7 +1109,7 @@
 
 instance by (standard; transfer)
   (fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
-    half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_diff_exp_iff
+    half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_div_exp_iff
     bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     and_rec or_rec xor_rec mask_eq_exp_minus_1
     set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
diff -r 924e487288fb -r dafb3d343cd6 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Feb 07 11:57:22 2024 +0000
+++ b/src/HOL/Parity.thy	Tue Feb 06 18:08:43 2024 +0000
@@ -192,6 +192,14 @@
   \<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close>
   using that by (induction A) simp_all
 
+lemma even_half_maybe_succ_eq [simp]:
+  \<open>even a \<Longrightarrow> (of_bool b + a) div 2 = a div 2\<close>
+  by simp
+
+lemma even_half_maybe_succ'_eq [simp]:
+  \<open>even a \<Longrightarrow> (b mod 2 + a) div 2 = a div 2\<close>
+  by (simp add: mod2_eq_if)
+
 lemma mask_eq_sum_exp:
   \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close>
 proof -