# HG changeset patch
# User wenzelm
# Date 1705237153 -3600
# Node ID 12e049905c0d0bdf1390730cfa13e7eec53158b4
# Parent  8205977e9e2c9b3bb5a7ccd41ddf26fd8a96883e# Parent  50cd283a72187d0c5b2feceb47b54eb9c5d062f6
merged

diff -r 50cd283a7218 -r 12e049905c0d src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sun Jan 14 13:14:35 2024 +0100
+++ b/src/HOL/Bit_Operations.thy	Sun Jan 14 13:59:13 2024 +0100
@@ -10,13 +10,13 @@
 subsection \<open>Abstract bit structures\<close>
 
 class semiring_bits = semiring_parity +
-  assumes bits_induct [case_names stable rec]:
+  assumes bit_induct [case_names stable rec]:
     \<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 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)
@@ -123,7 +133,7 @@
 
 lemma bit_iff_idd_imp_stable:
   \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close>
-using that proof (induction a rule: bits_induct)
+using that proof (induction a rule: bit_induct)
   case (stable a)
   then show ?case
     by simp
@@ -192,7 +202,7 @@
     then show ?thesis
       by (rule that[unfolded possible_bit_def])
   qed
-  then show ?thesis proof (induction a arbitrary: b rule: bits_induct)
+  then show ?thesis proof (induction a arbitrary: b rule: bit_induct)
     case (stable a)
     from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
       by (simp add: bit_0)
@@ -3719,7 +3729,7 @@
 
       \<^item> Equality rule: @{thm bit_eqI [where ?'a = int, no_vars]}
 
-      \<^item> Induction rule: @{thm bits_induct [where ?'a = int, no_vars]}
+      \<^item> Induction rule: @{thm bit_induct [where ?'a = int, no_vars]}
 
   \<^item> Typical operations are characterized as follows:
 
diff -r 50cd283a7218 -r 12e049905c0d src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Jan 14 13:14:35 2024 +0100
+++ b/src/HOL/Code_Numeral.thy	Sun Jan 14 13:59:13 2024 +0100
@@ -348,8 +348,8 @@
   is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_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
+  (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
     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
@@ -1107,8 +1107,8 @@
   is take_bit .
 
 instance by (standard; transfer)
-  (fact bit_eq_rec bits_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
+  (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
     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)+
diff -r 50cd283a7218 -r 12e049905c0d src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Jan 14 13:14:35 2024 +0100
+++ b/src/HOL/Library/Word.thy	Sun Jan 14 13:59:13 2024 +0100
@@ -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>