--- a/src/HOL/Bit_Operations.thy Sat Jan 13 19:50:12 2024 +0000
+++ b/src/HOL/Bit_Operations.thy Sat Jan 13 19:50:15 2024 +0000
@@ -15,8 +15,8 @@
\<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 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 bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
and even_succ_div_2 [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>
@@ -35,10 +35,6 @@
differently wrt. code generation.
\<close>
-lemma bits_div_by_0 [simp]:
- \<open>a div 0 = 0\<close>
- by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)
-
lemma bits_1_div_2 [simp]:
\<open>1 div 2 = 0\<close>
using even_succ_div_2 [of 0] by simp
@@ -83,6 +79,20 @@
\<open>0 mod a = 0\<close>
using div_mult_mod_eq [of 0 a] by simp
+lemma mod_exp_div_exp_eq_0 [simp]:
+ \<open>a mod 2 ^ n div 2 ^ n = 0\<close>
+proof (induction n arbitrary: a)
+ case 0
+ then show ?case
+ by simp
+next
+ case (Suc n)
+ then have \<open>a div 2 ^ 1 mod 2 ^ n div 2 ^ n = 0\<close> .
+ then show ?case
+ using div_exp_eq [of _ 1 n] div_exp_mod_exp_eq [of a 1 n]
+ by simp
+qed
+
lemma bit_0:
\<open>bit a 0 \<longleftrightarrow> odd a\<close>
by (simp add: bit_iff_odd)
--- a/src/HOL/Code_Numeral.thy Sat Jan 13 19:50:12 2024 +0000
+++ b/src/HOL/Code_Numeral.thy Sat Jan 13 19:50:15 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_1 bits_mod_div_trivial even_succ_div_2
+ bits_div_0 bits_div_by_0 bits_div_by_1 even_succ_div_2
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_1 bits_mod_div_trivial even_succ_div_2
+ bits_div_0 bits_div_by_0 bits_div_by_1 even_succ_div_2
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)+
--- a/src/HOL/Library/Word.thy Sat Jan 13 19:50:12 2024 +0000
+++ b/src/HOL/Library/Word.thy Sat Jan 13 19:50:15 2024 +0000
@@ -831,16 +831,12 @@
show \<open>0 div a = 0\<close>
for a :: \<open>'a word\<close>
by transfer simp
+ show \<open>a div 0 = 0\<close>
+ for a :: \<open>'a word\<close>
+ by transfer simp
show \<open>a div 1 = a\<close>
for a :: \<open>'a word\<close>
by transfer simp
- show \<open>a mod b div b = 0\<close>
- for a b :: \<open>'a word\<close>
- apply transfer
- apply (simp add: take_bit_eq_mod)
- apply (smt (verit, best) Euclidean_Rings.pos_mod_bound Euclidean_Rings.pos_mod_sign div_int_pos_iff
- nonneg1_imp_zdiv_pos_iff zero_less_power zmod_le_nonneg_dividend)
- done
show \<open>(1 + a) div 2 = a div 2\<close>
if \<open>even a\<close>
for a :: \<open>'a word\<close>