--- a/NEWS Sun Jan 14 20:55:58 2024 +0100
+++ b/NEWS Sun Jan 14 20:02:55 2024 +0000
@@ -32,6 +32,8 @@
* Streamlined specification of type class (semi)ring_parity. Minor
INCOMPATIBILITY.
+* Lemma even_succ_div_2 renamed to even_half_succ_eq. Minor INCOMPATIBILITY.
+
*** ML ***
--- a/src/HOL/Bit_Operations.thy Sun Jan 14 20:55:58 2024 +0100
+++ b/src/HOL/Bit_Operations.thy Sun Jan 14 20:02:55 2024 +0000
@@ -17,7 +17,7 @@
assumes bits_div_0 [simp]: \<open>0 div a = 0\<close>
and bits_div_by_0 [simp]: \<open>a div 0 = 0\<close>
and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
- and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+ and even_half_succ_eq [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
and even_mask_div_iff: \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
@@ -37,7 +37,7 @@
lemma bits_1_div_2 [simp]:
\<open>1 div 2 = 0\<close>
- using even_succ_div_2 [of 0] by simp
+ using even_half_succ_eq [of 0] by simp
lemma bits_1_div_exp [simp]:
\<open>1 div 2 ^ n = of_bool (n = 0)\<close>
--- a/src/HOL/Code_Numeral.thy Sun Jan 14 20:55:58 2024 +0100
+++ b/src/HOL/Code_Numeral.thy Sun Jan 14 20:02:55 2024 +0000
@@ -349,7 +349,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
- bits_div_0 bits_div_by_0 bits_div_by_1 even_succ_div_2
+ bits_div_0 bits_div_by_0 bits_div_by_1 even_half_succ_eq
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
and_rec or_rec xor_rec mask_eq_exp_minus_1
@@ -1108,7 +1108,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
- bits_div_0 bits_div_by_0 bits_div_by_1 even_succ_div_2
+ bits_div_0 bits_div_by_0 bits_div_by_1 even_half_succ_eq
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 and_rec or_rec xor_rec
mask_eq_exp_minus_1 set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def)+