--- a/src/HOL/Parity.thy Tue Jan 30 22:43:10 2024 +0100
+++ b/src/HOL/Parity.thy Mon Jan 29 20:37:03 2024 +0000
@@ -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]: