# HG changeset patch
# User haftmann
# Date 1705262575 0
# Node ID 62d8c6c08fb25c5d02a93c457e1ba8f3cf857e75
# Parent  47272fac86d81da8eb7ddc1df63aaea6ade84c66
consolidated lemma name

diff -r 47272fac86d8 -r 62d8c6c08fb2 NEWS
--- 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 ***
 
diff -r 47272fac86d8 -r 62d8c6c08fb2 src/HOL/Bit_Operations.thy
--- 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>
diff -r 47272fac86d8 -r 62d8c6c08fb2 src/HOL/Code_Numeral.thy
--- 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)+