# HG changeset patch
# User wenzelm
# Date 1706705096 -3600
# Node ID 9f031b8bc880f1f0b90c516860f9979ebcced502
# Parent  8ef205d9fd224bfea0bde05df24e3caa1a7d4841# Parent  0631dfc0db078697a6a0fcbfbb446efeb09a833d
merged

diff -r 0631dfc0db07 -r 9f031b8bc880 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Wed Jan 31 12:43:06 2024 +0100
+++ b/src/HOL/Bit_Operations.thy	Wed Jan 31 13:44:56 2024 +0100
@@ -14,8 +14,7 @@
     \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
      \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
         \<Longrightarrow> P a\<close>
-  assumes even_half_succ_eq [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
-    and half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
+  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>
diff -r 0631dfc0db07 -r 9f031b8bc880 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jan 31 12:43:06 2024 +0100
+++ b/src/HOL/Library/Word.thy	Wed Jan 31 13:44:56 2024 +0100
@@ -668,7 +668,8 @@
 end
 
 instance word :: (len) semiring_parity
-  by (standard; transfer) (simp_all add: mod_2_eq_odd)
+  by (standard; transfer)
+    (auto simp add: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
 
 lemma word_bit_induct [case_names zero even odd]:
   \<open>P a\<close> if word_zero: \<open>P 0\<close>
@@ -837,11 +838,6 @@
   show \<open>0 div a = 0\<close>
     for a :: \<open>'a word\<close>
     by transfer simp
-  show \<open>(1 + a) div 2 = a div 2\<close>
-    if \<open>even a\<close>
-    for a :: \<open>'a word\<close>
-    using that by transfer
-      (auto dest: le_Suc_ex simp add: take_bit_Suc elim!: evenE)
   show \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
     for a :: \<open>'a word\<close> and m n :: nat
     apply transfer
diff -r 0631dfc0db07 -r 9f031b8bc880 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Jan 31 12:43:06 2024 +0100
+++ b/src/HOL/Parity.thy	Wed Jan 31 13:44:56 2024 +0100
@@ -14,6 +14,7 @@
 class semiring_parity = comm_semiring_1 + semiring_modulo +
   assumes mod_2_eq_odd: \<open>a mod 2 = of_bool (\<not> 2 dvd a)\<close>
     and odd_one [simp]: \<open>\<not> 2 dvd 1\<close>
+    and even_half_succ_eq [simp]: \<open>2 dvd a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
 begin
 
 abbreviation even :: "'a \<Rightarrow> bool"
@@ -32,7 +33,7 @@
 end
 
 instance nat :: semiring_parity
-  by standard (simp_all add: dvd_eq_mod_eq_0)
+  by standard (auto simp add: dvd_eq_mod_eq_0)
 
 instance int :: ring_parity
   by standard (auto simp add: dvd_eq_mod_eq_0)
@@ -855,6 +856,8 @@
     then show False
       by simp
   qed
+  show \<open>(1 + a) div 2 = a div 2\<close> if \<open>2 dvd a\<close> for a
+    using that by auto
 qed
 
 lemma even_succ_div_two [simp]: