# HG changeset patch
# User haftmann
# Date 1660888146 0
# Node ID 647879691c1c3866d2639c786c32abd619d81b0e
# Parent  48d0320357449414e9591059303d4454ddbd92c7
streamlined theorems and sections

diff -r 48d032035744 -r 647879691c1c src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Wed Aug 17 20:37:16 2022 +0000
+++ b/src/HOL/Bit_Operations.thy	Fri Aug 19 05:49:06 2022 +0000
@@ -7,15 +7,6 @@
   imports Presburger Groups_List
 begin
 
-lemma half_nonnegative_int_iff [simp]:
-  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-  by auto
-
-lemma half_negative_int_iff [simp]:
-  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by auto
-
-
 subsection \<open>Abstract bit structures\<close>
 
 class semiring_bits = semiring_parity +
diff -r 48d032035744 -r 647879691c1c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Aug 17 20:37:16 2022 +0000
+++ b/src/HOL/Divides.thy	Fri Aug 19 05:49:06 2022 +0000
@@ -282,6 +282,39 @@
 declare split_zdiv [of _ _ "numeral k", arith_split] for k
 declare split_zmod [of _ _ "numeral k", arith_split] for k
 
+lemma half_nonnegative_int_iff [simp]:
+  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+  by auto
+
+lemma half_negative_int_iff [simp]:
+  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by auto
+
+lemma zdiv_eq_0_iff:
+  "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
+  for i k :: int
+proof
+  assume ?L
+  moreover have "?L \<longrightarrow> ?R"
+    by (rule split_zdiv [THEN iffD2]) simp
+  ultimately show ?R
+    by blast
+next
+  assume ?R then show ?L
+    by auto
+qed
+
+lemma zmod_trivial_iff:
+  fixes i k :: int
+  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
+proof -
+  have "i mod k = i \<longleftrightarrow> i div k = 0"
+    using div_mult_mod_eq [of i k] by safe auto
+  with zdiv_eq_0_iff
+  show ?thesis
+    by simp
+qed
+
 
 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
@@ -348,30 +381,6 @@
   unfolding mult_2 [symmetric] add.commute [of _ 1]
   by (rule pos_zmod_mult_2, simp)
 
-lemma zdiv_eq_0_iff:
-  "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
-  for i k :: int
-proof
-  assume ?L
-  moreover have "?L \<longrightarrow> ?R"
-    by (rule split_zdiv [THEN iffD2]) simp
-  ultimately show ?R
-    by blast
-next
-  assume ?R then show ?L
-    by auto
-qed
-
-lemma zmod_trivial_iff:
-  fixes i k :: int
-  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
-proof -
-  have "i mod k = i \<longleftrightarrow> i div k = 0"
-    using div_mult_mod_eq [of i k] by safe auto
-  with zdiv_eq_0_iff
-  show ?thesis
-    by simp
-qed
 
   
 subsubsection \<open>Quotients of Signs\<close>
@@ -459,7 +468,6 @@
   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
   using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k] by arith
 
-
 lemma neg_imp_zdiv_nonneg_iff:
   fixes a::int
   assumes "b < 0" 
@@ -492,6 +500,28 @@
 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 \<Longrightarrow> m mod k \<le> m"
   by (rule split_zmod[THEN iffD2]) (fastforce dest: q_pos_lemma intro: split_mult_pos_le)
 
+lemma sgn_div_eq_sgn_mult:
+  \<open>sgn (k div l) = of_bool (k div l \<noteq> 0) * sgn (k * l)\<close>
+  for k l :: int
+proof (cases \<open>k div l = 0\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  have \<open>0 \<le> \<bar>k\<bar> div \<bar>l\<bar>\<close>
+    by (cases \<open>l = 0\<close>) (simp_all add: pos_imp_zdiv_nonneg_iff)
+  then have \<open>\<bar>k\<bar> div \<bar>l\<bar> \<noteq> 0 \<longleftrightarrow> 0 < \<bar>k\<bar> div \<bar>l\<bar>\<close>
+    by (simp add: less_le)
+  also have \<open>\<dots> \<longleftrightarrow> \<bar>k\<bar> \<ge> \<bar>l\<bar>\<close>
+    using False nonneg1_imp_zdiv_pos_iff by auto
+  finally have *: \<open>\<bar>k\<bar> div \<bar>l\<bar> \<noteq> 0 \<longleftrightarrow> \<bar>l\<bar> \<le> \<bar>k\<bar>\<close> .
+  show ?thesis
+    using \<open>0 \<le> \<bar>k\<bar> div \<bar>l\<bar>\<close> False
+  by (auto simp add: div_eq_div_abs [of k l] div_eq_sgn_abs [of k l]
+    sgn_mult sgn_1_pos sgn_1_neg sgn_eq_0_iff nonneg1_imp_zdiv_pos_iff * dest: sgn_not_eq_imp)
+qed
+
 
 subsubsection \<open>Further properties\<close>
 
diff -r 48d032035744 -r 647879691c1c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Wed Aug 17 20:37:16 2022 +0000
+++ b/src/HOL/Euclidean_Division.thy	Fri Aug 19 05:49:06 2022 +0000
@@ -1494,9 +1494,11 @@
 qed
 
 
-subsection \<open>Euclidean division on \<^typ>\<open>int\<close>\<close>
+subsection \<open>Elementary euclidean division on \<^typ>\<open>int\<close>\<close>
 
-instantiation int :: normalization_semidom
+subsubsection \<open>Basic instantiation\<close>
+
+instantiation int :: "{normalization_semidom, idom_modulo}"
 begin
 
 definition normalize_int :: \<open>int \<Rightarrow> int\<close>
@@ -1514,6 +1516,14 @@
     - of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> l \<noteq> 0 \<and> n \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m))\<close>
   by (simp add: divide_int_def sgn_mult nat_mult_distrib abs_mult sgn_eq_0_iff ac_simps)
 
+definition modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k mod l = sgn k * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+
+lemma modulo_int_unfold:
+  \<open>(sgn k * int m) mod (sgn l * int n) =
+    sgn k * int (m mod (of_bool (l \<noteq> 0) * n)) + (sgn l * int n) * of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m)\<close>
+  by (auto simp add: modulo_int_def sgn_mult abs_mult)
+
 instance proof
   fix k :: int show "k div 0 = 0"
   by (simp add: divide_int_def)
@@ -1527,24 +1537,18 @@
   with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
     by (simp only: divide_int_unfold)
       (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
+next
+  fix k l :: int
+  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
+    by (blast intro: int_sgnE elim: that)
+  then show "k div l * l + k mod l = k"
+    by (simp add: divide_int_unfold modulo_int_unfold algebra_simps modulo_nat_def of_nat_diff)
 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
 
 end
 
-lemma div_abs_eq_div_nat:
-  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
-  by (auto simp add: divide_int_def)
 
-lemma div_eq_div_abs:
-  \<open>k div l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)
-    - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
-  for k l :: int
-  by (simp add: divide_int_def [of k l] div_abs_eq_div_nat)
-
-lemma div_abs_eq:
-  \<open>\<bar>k\<bar> div \<bar>l\<bar> = sgn k * sgn l * (k div l + of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
-  for k l :: int
-  by (simp add: div_eq_div_abs [of k l] ac_simps)
+subsubsection \<open>Algebraic foundations\<close>
 
 lemma coprime_int_iff [simp]:
   "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
@@ -1604,26 +1608,23 @@
   for a b :: int
   by (drule coprime_common_divisor [of _ _ x]) simp_all
 
-instantiation int :: idom_modulo
-begin
+
+subsubsection \<open>Basic conversions\<close>
 
-definition modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>k mod l = sgn k * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+lemma div_abs_eq_div_nat:
+  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
+  by (auto simp add: divide_int_def)
 
-lemma modulo_int_unfold:
-  \<open>(sgn k * int m) mod (sgn l * int n) =
-    sgn k * int (m mod (of_bool (l \<noteq> 0) * n)) + (sgn l * int n) * of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m)\<close>
-  by (auto simp add: modulo_int_def sgn_mult abs_mult)
+lemma div_eq_div_abs:
+  \<open>k div l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)
+    - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: divide_int_def [of k l] div_abs_eq_div_nat)
 
-instance proof
-  fix k l :: int
-  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
-    by (blast intro: int_sgnE elim: that)
-  then show "k div l * l + k mod l = k"
-    by (simp add: divide_int_unfold modulo_int_unfold algebra_simps modulo_nat_def of_nat_diff)
-qed
-
-end
+lemma div_abs_eq:
+  \<open>\<bar>k\<bar> div \<bar>l\<bar> = sgn k * sgn l * (k div l + of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
+  for k l :: int
+  by (simp add: div_eq_div_abs [of k l] ac_simps)
 
 lemma mod_abs_eq_div_nat:
   "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
@@ -1639,6 +1640,35 @@
   for k l :: int
   by (auto simp: mod_eq_mod_abs [of k l])
 
+lemma div_sgn_abs_cancel:
+  fixes k l v :: int
+  assumes "v \<noteq> 0"
+  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
+  using assms by (simp add: sgn_mult abs_mult sgn_0_0
+    divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"] flip: div_abs_eq_div_nat)
+
+lemma div_eq_sgn_abs:
+  fixes k l v :: int
+  assumes "sgn k = sgn l"
+  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
+  using assms by (auto simp add: div_abs_eq)
+
+lemma div_dvd_sgn_abs:
+  fixes k l :: int
+  assumes "l dvd k"
+  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
+  using assms by (auto simp add: div_abs_eq ac_simps)
+
+lemma div_noneq_sgn_abs:
+  fixes k l :: int
+  assumes "l \<noteq> 0"
+  assumes "sgn k \<noteq> sgn l"
+  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
+  using assms by (auto simp add: div_abs_eq ac_simps sgn_0_0 dest!: sgn_not_eq_imp)
+
+
+subsubsection \<open>Euclidean division\<close>
+
 instantiation int :: unique_euclidean_ring
 begin
 
@@ -1742,133 +1772,6 @@
 
 end
 
-lemma div_sgn_abs_cancel:
-  fixes k l v :: int
-  assumes "v \<noteq> 0"
-  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-  using assms by (simp add: sgn_mult abs_mult sgn_0_0 of_nat_div divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"])
-
-lemma pos_mod_bound [simp]:
-  "k mod l < l" if "l > 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain n where "l = sgn 1 * int n"
-    by (cases l) simp_all
-  moreover from this that have "n > 0"
-    by simp
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold)
-      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_pos)
-qed
-
-lemma neg_mod_bound [simp]:
-  "l < k mod l" if "l < 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
-    by (cases l) simp_all
-  moreover define n where "n = Suc q"
-  then have "Suc q = n"
-    by simp
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold)
-      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_neg)
-qed
-
-lemma pos_mod_sign [simp]:
-  "0 \<le> k mod l" if "l > 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain n where "l = sgn 1 * int n"
-    by (cases l) auto
-  moreover from this that have "n > 0"
-    by simp
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold) (auto simp add: sgn_1_pos)
-qed
-
-lemma neg_mod_sign [simp]:
-  "k mod l \<le> 0" if "l < 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
-    by (cases l) simp_all
-  moreover define n where "n = Suc q"
-  then have "Suc q = n"
-    by simp
-  moreover have \<open>int (m mod n) \<le> int n\<close>
-    using \<open>Suc q = n\<close> by simp
-  then have \<open>sgn s * int (m mod n) \<le> int n\<close>
-    by (cases s \<open>0::int\<close> rule: linorder_cases) simp_all
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold) auto
-qed
-
-lemma div_pos_pos_trivial [simp]:
-  "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
-  using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
-
-lemma mod_pos_pos_trivial [simp]:
-  "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
-  using that by (simp add: mod_eq_self_iff_div_eq_0)
-
-lemma div_neg_neg_trivial [simp]:
-  "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
-  using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
-
-lemma mod_neg_neg_trivial [simp]:
-  "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
-  using that by (simp add: mod_eq_self_iff_div_eq_0)
-
-lemma div_pos_neg_trivial:
-  "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
-proof (cases \<open>l = - k\<close>)
-  case True
-  with that show ?thesis
-    by (simp add: divide_int_def)
-next
-  case False
-  show ?thesis
-    apply (rule div_eqI [of _ "k + l"])
-    using False that apply (simp_all add: division_segment_int_def)
-    done
-qed
-
-lemma mod_pos_neg_trivial:
-  "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
-proof (cases \<open>l = - k\<close>)
-  case True
-  with that show ?thesis
-    by (simp add: divide_int_def)
-next
-  case False
-  show ?thesis
-    apply (rule mod_eqI [of _ _ \<open>- 1\<close>])
-    using False that apply (simp_all add: division_segment_int_def)
-    done
-qed
-
-text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
-  because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
-
-text \<open>Distributive laws for function \<open>nat\<close>.\<close>
-
-lemma nat_div_distrib:
-  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> x\<close>
-  using that by (simp add: divide_int_def sgn_if)
-
-lemma nat_div_distrib':
-  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> y\<close>
-  using that by (simp add: divide_int_def sgn_if)
-
-lemma nat_mod_distrib: \<comment> \<open>Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't\<close>
-  \<open>nat (x mod y) = nat x mod nat y\<close> if \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
-  using that by (simp add: modulo_int_def sgn_if)
-
 
 subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
 
@@ -2135,25 +2038,123 @@
 instance int :: unique_euclidean_ring_with_nat
   by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np)
 
-lemma div_eq_sgn_abs:
-  fixes k l v :: int
-  assumes "sgn k = sgn l"
-  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
-  using assms by (auto simp add: divide_int_def [of k l] of_nat_div)
+
+subsection \<open>More on euclidean division on \<^typ>\<open>int\<close>\<close>
+
+subsubsection \<open>Trivial reduction steps\<close>
+
+lemma div_pos_pos_trivial [simp]:
+  "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
+  using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
+
+lemma mod_pos_pos_trivial [simp]:
+  "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
+  using that by (simp add: mod_eq_self_iff_div_eq_0)
+
+lemma div_neg_neg_trivial [simp]:
+  "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
+  using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
+
+lemma mod_neg_neg_trivial [simp]:
+  "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
+  using that by (simp add: mod_eq_self_iff_div_eq_0)
+
+lemma div_pos_neg_trivial:
+  "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
+proof (cases \<open>l = - k\<close>)
+  case True
+  with that show ?thesis
+    by (simp add: divide_int_def)
+next
+  case False
+  show ?thesis
+    apply (rule div_eqI [of _ "k + l"])
+    using False that apply (simp_all add: division_segment_int_def)
+    done
+qed
+
+lemma mod_pos_neg_trivial:
+  "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
+proof (cases \<open>l = - k\<close>)
+  case True
+  with that show ?thesis
+    by (simp add: divide_int_def)
+next
+  case False
+  show ?thesis
+    apply (rule mod_eqI [of _ _ \<open>- 1\<close>])
+    using False that apply (simp_all add: division_segment_int_def)
+    done
+qed
+
+text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
+  because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
+
+
+subsubsection \<open>Borders\<close>
 
-lemma div_dvd_sgn_abs:
-  fixes k l :: int
-  assumes "l dvd k"
-  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
-  using assms by (auto simp add: divide_int_def [of k l] of_nat_div)
+lemma pos_mod_bound [simp]:
+  "k mod l < l" if "l > 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain n where "l = sgn 1 * int n"
+    by (cases l) simp_all
+  moreover from this that have "n > 0"
+    by simp
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold)
+      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_pos)
+qed
+
+lemma neg_mod_bound [simp]:
+  "l < k mod l" if "l < 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
+    by (cases l) simp_all
+  moreover define n where "n = Suc q"
+  then have "Suc q = n"
+    by simp
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold)
+      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_neg)
+qed
 
-lemma div_noneq_sgn_abs:
-  fixes k l :: int
-  assumes "l \<noteq> 0"
-  assumes "sgn k \<noteq> sgn l"
-  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
-  using assms
-  by (simp only: divide_int_def [of k l]) (auto simp add: of_nat_div sgn_0_0 dest!: sgn_not_eq_imp)
+lemma pos_mod_sign [simp]:
+  "0 \<le> k mod l" if "l > 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain n where "l = sgn 1 * int n"
+    by (cases l) auto
+  moreover from this that have "n > 0"
+    by simp
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold) (auto simp add: sgn_1_pos)
+qed
+
+lemma neg_mod_sign [simp]:
+  "k mod l \<le> 0" if "l < 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
+    by (cases l) simp_all
+  moreover define n where "n = Suc q"
+  then have "Suc q = n"
+    by simp
+  moreover have \<open>int (m mod n) \<le> int n\<close>
+    using \<open>Suc q = n\<close> by simp
+  then have \<open>sgn s * int (m mod n) \<le> int n\<close>
+    by (cases s \<open>0::int\<close> rule: linorder_cases) simp_all
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold) auto
+qed
+
+
+subsubsection \<open>Algebraic rewrites\<close>
 
 lemma zdiv_zmult2_eq:
   \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
@@ -2167,6 +2168,18 @@
     using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
+lemma zdiv_zmult2_eq':
+  \<open>k div (l * j) = ((sgn j * k) div l) div \<bar>j\<bar>\<close> for k l j :: int
+proof -
+  have \<open>k div (l * j) = (sgn j * k) div (sgn j * (l * j))\<close>
+    by (simp add: sgn_0_0)
+  also have \<open>sgn j * (l * j) = l * \<bar>j\<bar>\<close>
+    by (simp add: mult.left_commute [of _ l] abs_sgn) (simp add: ac_simps)
+  also have \<open>(sgn j * k) div (l * \<bar>j\<bar>) = ((sgn j * k) div l) div \<bar>j\<bar>\<close>
+    by (simp add: zdiv_zmult2_eq)
+  finally show ?thesis .
+qed
+
 lemma zmod_zmult2_eq:
   \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
 proof (cases \<open>b \<ge> 0\<close>)
@@ -2179,6 +2192,9 @@
     using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
+
+subsubsection \<open>Distributive laws for conversions.\<close>
+
 lemma zdiv_int:
   "int (a div b) = int a div int b"
   by (fact of_nat_div)
@@ -2187,6 +2203,18 @@
   "int (a mod b) = int a mod int b"
   by (fact of_nat_mod)
 
+lemma nat_div_distrib:
+  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> x\<close>
+  using that by (simp add: divide_int_def sgn_if)
+
+lemma nat_div_distrib':
+  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> y\<close>
+  using that by (simp add: divide_int_def sgn_if)
+
+lemma nat_mod_distrib: \<comment> \<open>Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't\<close>
+  \<open>nat (x mod y) = nat x mod nat y\<close> if \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
+  using that by (simp add: modulo_int_def sgn_if)
+
 
 subsection \<open>Code generation\<close>
 
diff -r 48d032035744 -r 647879691c1c src/HOL/Library/Signed_Division.thy
--- a/src/HOL/Library/Signed_Division.thy	Wed Aug 17 20:37:16 2022 +0000
+++ b/src/HOL/Library/Signed_Division.thy	Fri Aug 19 05:49:06 2022 +0000
@@ -7,23 +7,6 @@
   imports Main
 begin
 
-lemma sgn_div_eq_sgn_mult:
-  \<open>sgn (a div b) = sgn (a * b)\<close>
-  if \<open>a div b \<noteq> 0\<close> for a b :: int
-proof -
-  have \<open>0 \<le> \<bar>a\<bar> div \<bar>b\<bar>\<close>
-    by (cases \<open>b = 0\<close>) (simp_all add: pos_imp_zdiv_nonneg_iff)
-  then have \<open>\<bar>a\<bar> div \<bar>b\<bar> \<noteq> 0 \<longleftrightarrow> 0 < \<bar>a\<bar> div \<bar>b\<bar>\<close>
-    by (simp add: less_le)
-  also have \<open>\<dots> \<longleftrightarrow> \<bar>a\<bar> \<ge> \<bar>b\<bar>\<close>
-    using that nonneg1_imp_zdiv_pos_iff by auto
-  finally have *: \<open>\<bar>a\<bar> div \<bar>b\<bar> \<noteq> 0 \<longleftrightarrow> \<bar>b\<bar> \<le> \<bar>a\<bar>\<close> .
-  show ?thesis
-    using \<open>0 \<le> \<bar>a\<bar> div \<bar>b\<bar>\<close> that
-  by (auto simp add: div_eq_div_abs [of a b] div_eq_sgn_abs [of a b]
-    sgn_mult sgn_1_pos sgn_1_neg sgn_eq_0_iff nonneg1_imp_zdiv_pos_iff * dest: sgn_not_eq_imp)
-qed
-
 class signed_division = comm_semiring_1_cancel +
   fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>sdiv\<close> 70)
   and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)