diff -r 77cbf472fcc9 -r 48d032035744 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Aug 18 09:29:11 2022 +0200
+++ b/src/HOL/Divides.thy	Wed Aug 17 20:37:16 2022 +0000
@@ -11,6 +11,43 @@
 
 subsection \<open>More on division\<close>
 
+subsubsection \<open>Laws for div and mod with Unary Minus\<close>
+
+lemma zmod_zminus1_not_zero:
+  fixes k l :: int
+  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma zmod_zminus2_not_zero:
+  fixes k l :: int
+  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma zdiv_zminus1_eq_if:
+  \<open>(- a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that sgn_not_eq_imp [of b \<open>- a\<close>]
+  by (cases \<open>a = 0\<close>) (auto simp add: div_eq_div_abs [of \<open>- a\<close> b] div_eq_div_abs [of a b] sgn_eq_0_iff)
+
+lemma zdiv_zminus2_eq_if:
+  \<open>a div (- b) = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
+
+lemma zmod_zminus1_eq_if:
+  \<open>(- a) mod b = (if a mod b = 0 then 0 else b - (a mod b))\<close>
+  for a b :: int
+  by (cases \<open>b = 0\<close>)
+    (auto simp flip: minus_div_mult_eq_mod simp add: zdiv_zminus1_eq_if algebra_simps)
+
+lemma zmod_zminus2_eq_if:
+  \<open>a mod (- b) = (if a mod b = 0 then 0 else (a mod b) - b)\<close>
+  for a b :: int
+  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
+
+
+subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
+
 inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
@@ -91,139 +128,20 @@
   using unique_quotient [of k l] unique_remainder [of k l]
   by auto
 
-lemma div_abs_eq_div_nat:
-  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
-  by (simp add: divide_int_def)
-
-lemma mod_abs_eq_div_nat:
-  "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
-  by (simp add: modulo_int_def)
-
-lemma zdiv_int:
-  "int (a div b) = int a div int b"
-  by (simp add: divide_int_def)
-
-lemma zmod_int:
-  "int (a mod b) = int a mod int b"
-  by (simp add: modulo_int_def)
-
-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>"
-proof -
-  from assms have "sgn v = - 1 \<or> sgn v = 1"
-    by (cases "v \<ge> 0") auto
-  then show ?thesis
-    using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
-    by (fastforce simp add: not_less div_abs_eq_div_nat)
-qed
-
-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>"
-proof (cases "l = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-    using div_sgn_abs_cancel [of l k l] by simp
-  then show ?thesis
-    by (simp add: sgn_mult_abs)
-qed
-
-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>)"
-proof (cases "k = 0 \<or> l = 0")
-  case True
-  then show ?thesis
-    by auto
-next
-  case False
-  then have "k \<noteq> 0" and "l \<noteq> 0"
-    by auto
-  show ?thesis
-  proof (cases "sgn l = sgn k")
-    case True
-    then show ?thesis
-      by (auto simp add: div_eq_sgn_abs)
-  next
-    case False
-    with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
-    have "sgn l * sgn k = - 1"
-      by (simp add: sgn_if split: if_splits)
-    with assms show ?thesis
-      unfolding divide_int_def [of k l]
-      by (auto simp add: zdiv_int ac_simps)
-  qed
-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: not_less zdiv_int)
-  
-
-subsubsection \<open>Laws for div and mod with Unary Minus\<close>
-
 lemma zminus1_lemma:
      "eucl_rel_int a b (q, r) ==> b \<noteq> 0
       ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
                           if r=0 then 0 else b-r)"
 by (force simp add: eucl_rel_int_iff right_diff_distrib)
 
-
-lemma zdiv_zminus1_eq_if:
-     "b \<noteq> (0::int)
-      \<Longrightarrow> (-a) div b = (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
-
-lemma zmod_zminus1_eq_if:
-     "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
-proof (cases "b = 0")
-  case False
-  then show ?thesis
-    by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
-qed auto
-
-lemma zmod_zminus1_not_zero:
-  fixes k l :: int
-  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
-lemma zmod_zminus2_not_zero:
-  fixes k l :: int
-  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
-lemma zdiv_zminus2_eq_if:
-  "b \<noteq> (0::int)
-      ==> a div (-b) =
-          (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-  by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
-
-lemma zmod_zminus2_eq_if:
-  "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
-  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
-
-
-subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
-
 lemma zdiv_mono1:
-  fixes b::int
-  assumes "a \<le> a'" "0 < b" shows "a div b \<le> a' div b"
+  \<open>a div b \<le> a' div b\<close>
+  if \<open>a \<le> a'\<close> \<open>0 < b\<close>
+  for a b b' :: int
 proof (rule unique_quotient_lemma)
   show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
-    using assms(1) by auto
-qed (use assms in auto)
+    using \<open>a \<le> a'\<close> by auto
+qed (use that in auto)
 
 lemma zdiv_mono1_neg:
   fixes b::int