Theory HOL.Euclidean_Rings

(*  Title:      HOL/Euclidean_Rgins.thy
    Author:     Manuel Eberl, TU Muenchen
    Author:     Florian Haftmann, TU Muenchen
*)

section ‹Division in euclidean (semi)rings›

theory Euclidean_Rings
  imports Int Lattices_Big
begin

subsection ‹Euclidean (semi)rings with explicit division and remainder›

class euclidean_semiring = semidom_modulo +
  fixes euclidean_size :: "'a ⇒ nat"
  assumes size_0 [simp]: "euclidean_size 0 = 0"
  assumes mod_size_less:
    "b ≠ 0 ⟹ euclidean_size (a mod b) < euclidean_size b"
  assumes size_mult_mono:
    "b ≠ 0 ⟹ euclidean_size a ≤ euclidean_size (a * b)"
begin

lemma euclidean_size_eq_0_iff [simp]:
  "euclidean_size b = 0 ⟷ b = 0"
proof
  assume "b = 0"
  then show "euclidean_size b = 0"
    by simp
next
  assume "euclidean_size b = 0"
  show "b = 0"
  proof (rule ccontr)
    assume "b ≠ 0"
    with mod_size_less have "euclidean_size (b mod b) < euclidean_size b" .
    with ‹euclidean_size b = 0› show False
      by simp
  qed
qed

lemma euclidean_size_greater_0_iff [simp]:
  "euclidean_size b > 0 ⟷ b ≠ 0"
  using euclidean_size_eq_0_iff [symmetric, of b] by safe simp

lemma size_mult_mono': "b ≠ 0 ⟹ euclidean_size a ≤ euclidean_size (b * a)"
  by (subst mult.commute) (rule size_mult_mono)

lemma dvd_euclidean_size_eq_imp_dvd:
  assumes "a ≠ 0" and "euclidean_size a = euclidean_size b"
    and "b dvd a"
  shows "a dvd b"
proof (rule ccontr)
  assume "¬ a dvd b"
  hence "b mod a ≠ 0" using mod_0_imp_dvd [of b a] by blast
  then have "b mod a ≠ 0" by (simp add: mod_eq_0_iff_dvd)
  from ‹b dvd a› have "b dvd b mod a" by (simp add: dvd_mod_iff)
  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
    with ‹b mod a ≠ 0› have "c ≠ 0" by auto
  with ‹b mod a = b * c› have "euclidean_size (b mod a) ≥ euclidean_size b"
    using size_mult_mono by force
  moreover from ‹¬ a dvd b› and ‹a ≠ 0›
  have "euclidean_size (b mod a) < euclidean_size a"
    using mod_size_less by blast
  ultimately show False using ‹euclidean_size a = euclidean_size b›
    by simp
qed

lemma euclidean_size_times_unit:
  assumes "is_unit a"
  shows   "euclidean_size (a * b) = euclidean_size b"
proof (rule antisym)
  from assms have [simp]: "a ≠ 0" by auto
  thus "euclidean_size (a * b) ≥ euclidean_size b" by (rule size_mult_mono')
  from assms have "is_unit (1 div a)" by simp
  hence "1 div a ≠ 0" by (intro notI) simp_all
  hence "euclidean_size (a * b) ≤ euclidean_size ((1 div a) * (a * b))"
    by (rule size_mult_mono')
  also from assms have "(1 div a) * (a * b) = b"
    by (simp add: algebra_simps unit_div_mult_swap)
  finally show "euclidean_size (a * b) ≤ euclidean_size b" .
qed

lemma euclidean_size_unit:
  "is_unit a ⟹ euclidean_size a = euclidean_size 1"
  using euclidean_size_times_unit [of a 1] by simp

lemma unit_iff_euclidean_size:
  "is_unit a ⟷ euclidean_size a = euclidean_size 1 ∧ a ≠ 0"
proof safe
  assume A: "a ≠ 0" and B: "euclidean_size a = euclidean_size 1"
  show "is_unit a"
    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
qed (auto intro: euclidean_size_unit)

lemma euclidean_size_times_nonunit:
  assumes "a ≠ 0" "b ≠ 0" "¬ is_unit a"
  shows   "euclidean_size b < euclidean_size (a * b)"
proof (rule ccontr)
  assume "¬euclidean_size b < euclidean_size (a * b)"
  with size_mult_mono'[OF assms(1), of b]
    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
  have "a * b dvd b"
    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq])
       (use assms in simp_all)
  hence "a * b dvd 1 * b" by simp
  with ‹b ≠ 0› have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
  with assms(3) show False by contradiction
qed

lemma dvd_imp_size_le:
  assumes "a dvd b" "b ≠ 0"
  shows   "euclidean_size a ≤ euclidean_size b"
  using assms by (auto simp: size_mult_mono)

lemma dvd_proper_imp_size_less:
  assumes "a dvd b" "¬ b dvd a" "b ≠ 0"
  shows   "euclidean_size a < euclidean_size b"
proof -
  from assms(1) obtain c where "b = a * c" by (erule dvdE)
  hence z: "b = c * a" by (simp add: mult.commute)
  from z assms have "¬is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
  with z assms show ?thesis
    by (auto intro!: euclidean_size_times_nonunit)
qed

lemma unit_imp_mod_eq_0:
  "a mod b = 0" if "is_unit b"
  using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)

lemma mod_eq_self_iff_div_eq_0:
  "a mod b = a ⟷ a div b = 0" (is "?P ⟷ ?Q")
proof
  assume ?P
  with div_mult_mod_eq [of a b] show ?Q
    by auto
next
  assume ?Q
  with div_mult_mod_eq [of a b] show ?P
    by simp
qed

lemma coprime_mod_left_iff [simp]:
  "coprime (a mod b) b ⟷ coprime a b" if "b ≠ 0"
  by (rule iffI; rule coprimeI)
    (use that in ‹auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff›)

lemma coprime_mod_right_iff [simp]:
  "coprime a (b mod a) ⟷ coprime a b" if "a ≠ 0"
  using that coprime_mod_left_iff [of a b] by (simp add: ac_simps)

end

class euclidean_ring = idom_modulo + euclidean_semiring
begin

lemma dvd_diff_commute [ac_simps]:
  "a dvd c - b ⟷ a dvd b - c"
proof -
  have "a dvd c - b ⟷ a dvd (c - b) * - 1"
    by (subst dvd_mult_unit_iff) simp_all
  then show ?thesis
    by simp
qed

end


subsection ‹Euclidean (semi)rings with cancel rules›

class euclidean_semiring_cancel = euclidean_semiring +
  assumes div_mult_self1 [simp]: "b ≠ 0 ⟹ (a + c * b) div b = c + a div b"
  and div_mult_mult1 [simp]: "c ≠ 0 ⟹ (c * a) div (c * b) = a div b"
begin

lemma div_mult_self2 [simp]:
  assumes "b ≠ 0"
  shows "(a + b * c) div b = c + a div b"
  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)

lemma div_mult_self3 [simp]:
  assumes "b ≠ 0"
  shows "(c * b + a) div b = c + a div b"
  using assms by (simp add: add.commute)

lemma div_mult_self4 [simp]:
  assumes "b ≠ 0"
  shows "(b * c + a) div b = c + a div b"
  using assms by (simp add: add.commute)

lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
proof (cases "b = 0")
  case True then show ?thesis by simp
next
  case False
  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
    by (simp add: div_mult_mod_eq)
  also from False div_mult_self1 [of b a c] have
    "… = (c + a div b) * b + (a + c * b) mod b"
      by (simp add: algebra_simps)
  finally have "a = a div b * b + (a + c * b) mod b"
    by (simp add: add.commute [of a] add.assoc distrib_right)
  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
    by (simp add: div_mult_mod_eq)
  then show ?thesis by simp
qed

lemma mod_mult_self2 [simp]:
  "(a + b * c) mod b = a mod b"
  by (simp add: mult.commute [of b])

lemma mod_mult_self3 [simp]:
  "(c * b + a) mod b = a mod b"
  by (simp add: add.commute)

lemma mod_mult_self4 [simp]:
  "(b * c + a) mod b = a mod b"
  by (simp add: add.commute)

lemma mod_mult_self1_is_0 [simp]:
  "b * a mod b = 0"
  using mod_mult_self2 [of 0 b a] by simp

lemma mod_mult_self2_is_0 [simp]:
  "a * b mod b = 0"
  using mod_mult_self1 [of 0 a b] by simp

lemma div_add_self1:
  assumes "b ≠ 0"
  shows "(b + a) div b = a div b + 1"
  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)

lemma div_add_self2:
  assumes "b ≠ 0"
  shows "(a + b) div b = a div b + 1"
  using assms div_add_self1 [of b a] by (simp add: add.commute)

lemma mod_add_self1 [simp]:
  "(b + a) mod b = a mod b"
  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)

lemma mod_add_self2 [simp]:
  "(a + b) mod b = a mod b"
  using mod_mult_self1 [of a 1 b] by simp

lemma mod_div_trivial [simp]:
  "a mod b div b = 0"
proof (cases "b = 0")
  assume "b = 0"
  thus ?thesis by simp
next
  assume "b ≠ 0"
  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
    by (rule div_mult_self1 [symmetric])
  also have "… = a div b"
    by (simp only: mod_div_mult_eq)
  also have "… = a div b + 0"
    by simp
  finally show ?thesis
    by (rule add_left_imp_eq)
qed

lemma mod_mod_trivial [simp]:
  "a mod b mod b = a mod b"
proof -
  have "a mod b mod b = (a mod b + a div b * b) mod b"
    by (simp only: mod_mult_self1)
  also have "… = a mod b"
    by (simp only: mod_div_mult_eq)
  finally show ?thesis .
qed

lemma mod_mod_cancel:
  assumes "c dvd b"
  shows "a mod b mod c = a mod c"
proof -
  from ‹c dvd b› obtain k where "b = c * k"
    by (rule dvdE)
  have "a mod b mod c = a mod (c * k) mod c"
    by (simp only: ‹b = c * k›)
  also have "… = (a mod (c * k) + a div (c * k) * k * c) mod c"
    by (simp only: mod_mult_self1)
  also have "… = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
    by (simp only: ac_simps)
  also have "… = a mod c"
    by (simp only: div_mult_mod_eq)
  finally show ?thesis .
qed

lemma div_mult_mult2 [simp]:
  "c ≠ 0 ⟹ (a * c) div (b * c) = a div b"
  by (drule div_mult_mult1) (simp add: mult.commute)

lemma div_mult_mult1_if [simp]:
  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
  by simp_all

lemma mod_mult_mult1:
  "(c * a) mod (c * b) = c * (a mod b)"
proof (cases "c = 0")
  case True then show ?thesis by simp
next
  case False
  from div_mult_mod_eq
  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
    = c * a + c * (a mod b)" by (simp add: algebra_simps)
  with div_mult_mod_eq show ?thesis by simp
qed

lemma mod_mult_mult2:
  "(a * c) mod (b * c) = (a mod b) * c"
  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)

lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
  by (fact mod_mult_mult2 [symmetric])

lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
  by (fact mod_mult_mult1 [symmetric])

lemma dvd_mod: "k dvd m ⟹ k dvd n ⟹ k dvd (m mod n)"
  unfolding dvd_def by (auto simp add: mod_mult_mult1)

lemma div_plus_div_distrib_dvd_left:
  "c dvd a ⟹ (a + b) div c = a div c + b div c"
  by (cases "c = 0") auto

lemma div_plus_div_distrib_dvd_right:
  "c dvd b ⟹ (a + b) div c = a div c + b div c"
  using div_plus_div_distrib_dvd_left [of c b a]
  by (simp add: ac_simps)

lemma sum_div_partition:
  ‹(∑a∈A. f a) div b = (∑a∈A ∩ {a. b dvd f a}. f a div b) + (∑a∈A ∩ {a. ¬ b dvd f a}. f a) div b›
    if ‹finite A›
proof -
  have ‹A = A ∩ {a. b dvd f a} ∪ A ∩ {a. ¬ b dvd f a}›
    by auto
  then have ‹(∑a∈A. f a) = (∑a∈A ∩ {a. b dvd f a} ∪ A ∩ {a. ¬ b dvd f a}. f a)›
    by simp
  also have ‹… = (∑a∈A ∩ {a. b dvd f a}. f a) + (∑a∈A ∩ {a. ¬ b dvd f a}. f a)›
    using ‹finite A› by (auto intro: sum.union_inter_neutral)
  finally have *: ‹sum f A = sum f (A ∩ {a. b dvd f a}) + sum f (A ∩ {a. ¬ b dvd f a})› .
  define B where B: ‹B = A ∩ {a. b dvd f a}›
  with ‹finite A› have ‹finite B› and ‹a ∈ B ⟹ b dvd f a› for a
    by simp_all
  then have ‹(∑a∈B. f a) div b = (∑a∈B. f a div b)› and ‹b dvd (∑a∈B. f a)›
    by induction (simp_all add: div_plus_div_distrib_dvd_left)
  then show ?thesis using *
    by (simp add: B div_plus_div_distrib_dvd_left)
qed

named_theorems mod_simps

text ‹Addition respects modular equivalence.›

lemma mod_add_left_eq [mod_simps]:
  "(a mod c + b) mod c = (a + b) mod c"
proof -
  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
    by (simp only: div_mult_mod_eq)
  also have "… = (a mod c + b + a div c * c) mod c"
    by (simp only: ac_simps)
  also have "… = (a mod c + b) mod c"
    by (rule mod_mult_self1)
  finally show ?thesis
    by (rule sym)
qed

lemma mod_add_right_eq [mod_simps]:
  "(a + b mod c) mod c = (a + b) mod c"
  using mod_add_left_eq [of b c a] by (simp add: ac_simps)

lemma mod_add_eq:
  "(a mod c + b mod c) mod c = (a + b) mod c"
  by (simp add: mod_add_left_eq mod_add_right_eq)

lemma mod_sum_eq [mod_simps]:
  "(∑i∈A. f i mod a) mod a = sum f A mod a"
proof (induct A rule: infinite_finite_induct)
  case (insert i A)
  then have "(∑i∈insert i A. f i mod a) mod a
    = (f i mod a + (∑i∈A. f i mod a)) mod a"
    by simp
  also have "… = (f i + (∑i∈A. f i mod a) mod a) mod a"
    by (simp add: mod_simps)
  also have "… = (f i + (∑i∈A. f i) mod a) mod a"
    by (simp add: insert.hyps)
  finally show ?case
    by (simp add: insert.hyps mod_simps)
qed simp_all

lemma mod_add_cong:
  assumes "a mod c = a' mod c"
  assumes "b mod c = b' mod c"
  shows "(a + b) mod c = (a' + b') mod c"
proof -
  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
    unfolding assms ..
  then show ?thesis
    by (simp add: mod_add_eq)
qed

text ‹Multiplication respects modular equivalence.›

lemma mod_mult_left_eq [mod_simps]:
  "((a mod c) * b) mod c = (a * b) mod c"
proof -
  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
    by (simp only: div_mult_mod_eq)
  also have "… = (a mod c * b + a div c * b * c) mod c"
    by (simp only: algebra_simps)
  also have "… = (a mod c * b) mod c"
    by (rule mod_mult_self1)
  finally show ?thesis
    by (rule sym)
qed

lemma mod_mult_right_eq [mod_simps]:
  "(a * (b mod c)) mod c = (a * b) mod c"
  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)

lemma mod_mult_eq:
  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
  by (simp add: mod_mult_left_eq mod_mult_right_eq)

lemma mod_prod_eq [mod_simps]:
  "(∏i∈A. f i mod a) mod a = prod f A mod a"
proof (induct A rule: infinite_finite_induct)
  case (insert i A)
  then have "(∏i∈insert i A. f i mod a) mod a
    = (f i mod a * (∏i∈A. f i mod a)) mod a"
    by simp
  also have "… = (f i * ((∏i∈A. f i mod a) mod a)) mod a"
    by (simp add: mod_simps)
  also have "… = (f i * ((∏i∈A. f i) mod a)) mod a"
    by (simp add: insert.hyps)
  finally show ?case
    by (simp add: insert.hyps mod_simps)
qed simp_all

lemma mod_mult_cong:
  assumes "a mod c = a' mod c"
  assumes "b mod c = b' mod c"
  shows "(a * b) mod c = (a' * b') mod c"
proof -
  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
    unfolding assms ..
  then show ?thesis
    by (simp add: mod_mult_eq)
qed

text ‹Exponentiation respects modular equivalence.›

lemma power_mod [mod_simps]:
  "((a mod b) ^ n) mod b = (a ^ n) mod b"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
    by (simp add: mod_mult_right_eq)
  with Suc show ?case
    by (simp add: mod_mult_left_eq mod_mult_right_eq)
qed

lemma power_diff_power_eq:
  ‹a ^ m div a ^ n = (if n ≤ m then a ^ (m - n) else 1 div a ^ (n - m))›
    if ‹a ≠ 0›
proof (cases ‹n ≤ m›)
  case True
  with that power_diff [symmetric, of a n m] show ?thesis by simp
next
  case False
  then obtain q where n: ‹n = m + Suc q›
    by (auto simp add: not_le dest: less_imp_Suc_add)
  then have ‹a ^ m div a ^ n = (a ^ m * 1) div (a ^ m * a ^ Suc q)›
    by (simp add: power_add ac_simps)
  moreover from that have ‹a ^ m ≠ 0›
    by simp
  ultimately have ‹a ^ m div a ^ n = 1 div a ^ Suc q›
    by (subst (asm) div_mult_mult1) simp
  with False n show ?thesis
    by simp
qed

end


class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
begin

subclass idom_divide ..

lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
  using div_mult_mult1 [of "- 1" a b] by simp

lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
  using mod_mult_mult1 [of "- 1" a b] by simp

lemma div_minus_right: "a div (- b) = (- a) div b"
  using div_minus_minus [of "- a" b] by simp

lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
  using mod_minus_minus [of "- a" b] by simp

lemma div_minus1_right [simp]: "a div (- 1) = - a"
  using div_minus_right [of a 1] by simp

lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
  using mod_minus_right [of a 1] by simp

text ‹Negation respects modular equivalence.›

lemma mod_minus_eq [mod_simps]:
  "(- (a mod b)) mod b = (- a) mod b"
proof -
  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
    by (simp only: div_mult_mod_eq)
  also have "… = (- (a mod b) + - (a div b) * b) mod b"
    by (simp add: ac_simps)
  also have "… = (- (a mod b)) mod b"
    by (rule mod_mult_self1)
  finally show ?thesis
    by (rule sym)
qed

lemma mod_minus_cong:
  assumes "a mod b = a' mod b"
  shows "(- a) mod b = (- a') mod b"
proof -
  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
    unfolding assms ..
  then show ?thesis
    by (simp add: mod_minus_eq)
qed

text ‹Subtraction respects modular equivalence.›

lemma mod_diff_left_eq [mod_simps]:
  "(a mod c - b) mod c = (a - b) mod c"
  using mod_add_cong [of a c "a mod c" "- b" "- b"]
  by simp

lemma mod_diff_right_eq [mod_simps]:
  "(a - b mod c) mod c = (a - b) mod c"
  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
  by simp

lemma mod_diff_eq:
  "(a mod c - b mod c) mod c = (a - b) mod c"
  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
  by simp

lemma mod_diff_cong:
  assumes "a mod c = a' mod c"
  assumes "b mod c = b' mod c"
  shows "(a - b) mod c = (a' - b') mod c"
  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
  by simp

lemma minus_mod_self2 [simp]:
  "(a - b) mod b = a mod b"
  using mod_diff_right_eq [of a b b]
  by (simp add: mod_diff_right_eq)

lemma minus_mod_self1 [simp]:
  "(b - a) mod b = - a mod b"
  using mod_add_self2 [of "- a" b] by simp

lemma mod_eq_dvd_iff:
  "a mod c = b mod c ⟷ c dvd a - b" (is "?P ⟷ ?Q")
proof
  assume ?P
  then have "(a mod c - b mod c) mod c = 0"
    by simp
  then show ?Q
    by (simp add: dvd_eq_mod_eq_0 mod_simps)
next
  assume ?Q
  then obtain d where d: "a - b = c * d" ..
  then have "a = c * d + b"
    by (simp add: algebra_simps)
  then show ?P by simp
qed

lemma mod_eqE:
  assumes "a mod c = b mod c"
  obtains d where "b = a + c * d"
proof -
  from assms have "c dvd a - b"
    by (simp add: mod_eq_dvd_iff)
  then obtain d where "a - b = c * d" ..
  then have "b = a + c * - d"
    by (simp add: algebra_simps)
  with that show thesis .
qed

lemma invertible_coprime:
  "coprime a c" if "a * b mod c = 1"
  by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto)

end


subsection ‹Uniquely determined division›

class unique_euclidean_semiring = euclidean_semiring +
  assumes euclidean_size_mult: ‹euclidean_size (a * b) = euclidean_size a * euclidean_size b›
  fixes division_segment :: ‹'a ⇒ 'a›
  assumes is_unit_division_segment [simp]: ‹is_unit (division_segment a)›
    and division_segment_mult:
    ‹a ≠ 0 ⟹ b ≠ 0 ⟹ division_segment (a * b) = division_segment a * division_segment b›
    and division_segment_mod:
    ‹b ≠ 0 ⟹ ¬ b dvd a ⟹ division_segment (a mod b) = division_segment b›
  assumes div_bounded:
    ‹b ≠ 0 ⟹ division_segment r = division_segment b
    ⟹ euclidean_size r < euclidean_size b
    ⟹ (q * b + r) div b = q›
begin

lemma division_segment_not_0 [simp]:
  ‹division_segment a ≠ 0›
  using is_unit_division_segment [of a] is_unitE [of ‹division_segment a›] by blast

lemma euclidean_relationI [case_names by0 divides euclidean_relation]:
  ‹(a div b, a mod b) = (q, r)›
    if by0: ‹b = 0 ⟹ q = 0 ∧ r = a›
    and divides: ‹b ≠ 0 ⟹ b dvd a ⟹ r = 0 ∧ a = q * b›
    and euclidean_relation: ‹b ≠ 0 ⟹ ¬ b dvd a ⟹ division_segment r = division_segment b
      ∧ euclidean_size r < euclidean_size b ∧ a = q * b + r›
proof (cases ‹b = 0›)
  case True
  with by0 show ?thesis
    by simp
next
  case False
  show ?thesis
  proof (cases ‹b dvd a›)
    case True
    with ‹b ≠ 0› divides
    show ?thesis
      by simp
  next
    case False
    with ‹b ≠ 0› euclidean_relation
    have ‹division_segment r = division_segment b›
      ‹euclidean_size r < euclidean_size b› ‹a = q * b + r›
      by simp_all
    from ‹b ≠ 0› ‹division_segment r = division_segment b›
      ‹euclidean_size r < euclidean_size b›
    have ‹(q * b + r) div b = q›
      by (rule div_bounded)
    with ‹a = q * b + r›
    have ‹q = a div b›
      by simp
    from ‹a = q * b + r›
    have ‹a div b * b + a mod b = q * b + r›
      by (simp add: div_mult_mod_eq)
    with ‹q = a div b›
    have ‹q * b + a mod b = q * b + r›
      by simp
    then have ‹r = a mod b›
      by simp
    with ‹q = a div b›
    show ?thesis
      by simp
  qed
qed

subclass euclidean_semiring_cancel
proof
  fix a b c
  assume ‹b ≠ 0›
  have ‹((a + c * b) div b, (a + c * b) mod b) = (c + a div b, a mod b)›
  proof (induction rule: euclidean_relationI)
    case by0
    with ‹b ≠ 0›
    show ?case
      by simp
  next
    case divides
    then show ?case
      by (simp add: algebra_simps dvd_add_left_iff)
  next
    case euclidean_relation
    then have ‹¬ b dvd a›
      by (simp add: dvd_add_left_iff)
    have ‹a mod b + (b * c + b * (a div b)) = b * c + ((a div b) * b + a mod b)›
      by (simp add: ac_simps)
    with ‹b ≠ 0› have *: ‹a mod b + (b * c + b * (a div b)) = b * c + a›
      by (simp add: div_mult_mod_eq)
    from ‹¬ b dvd a› euclidean_relation show ?case
      by (simp_all add: algebra_simps division_segment_mod mod_size_less *)
  qed
  then show ‹(a + c * b) div b = c + a div b›
    by simp
next
  fix a b c
  assume ‹c ≠ 0›
  have ‹((c * a) div (c * b), (c * a) mod (c * b)) = (a div b, c * (a mod b))›
  proof (induction rule: euclidean_relationI)
    case by0
    with ‹c ≠ 0› show ?case
      by simp
  next
    case divides
    then show ?case
      by (auto simp add: algebra_simps)
  next
    case euclidean_relation
    then have ‹b ≠ 0› ‹a mod b ≠ 0›
      by (simp_all add: mod_eq_0_iff_dvd)
    have ‹c * (a mod b) + b * (c * (a div b)) = c * ((a div b) * b + a mod b)›
      by (simp add: algebra_simps)
    with ‹b ≠ 0› have *: ‹c * (a mod b) + b * (c * (a div b)) = c * a›
      by (simp add: div_mult_mod_eq)
    from ‹b ≠ 0› ‹c ≠ 0› have ‹euclidean_size c * euclidean_size (a mod b)
      < euclidean_size c * euclidean_size b›
      using mod_size_less [of b a] by simp
    with euclidean_relation ‹b ≠ 0› ‹a mod b ≠ 0› show ?case
      by (simp add: algebra_simps division_segment_mult division_segment_mod euclidean_size_mult *)
  qed
  then show ‹(c * a) div (c * b) = a div b›
    by simp
qed

lemma div_eq_0_iff:
  ‹a div b = 0 ⟷ euclidean_size a < euclidean_size b ∨ b = 0› (is "_ ⟷ ?P")
  if ‹division_segment a = division_segment b›
proof (cases ‹a = 0 ∨ b = 0›)
  case True
  then show ?thesis by auto
next
  case False
  then have ‹a ≠ 0› ‹b ≠ 0›
    by simp_all
  have ‹a div b = 0 ⟷ euclidean_size a < euclidean_size b›
  proof
    assume ‹a div b = 0›
    then have ‹a mod b = a›
      using div_mult_mod_eq [of a b] by simp
    with ‹b ≠ 0› mod_size_less [of b a]
    show ‹euclidean_size a < euclidean_size b›
      by simp
  next
    assume ‹euclidean_size a < euclidean_size b›
    have ‹(a div b, a mod b) = (0, a)›
    proof (induction rule: euclidean_relationI)
      case by0
      show ?case
        by simp
    next
      case divides
      with ‹euclidean_size a < euclidean_size b› show ?case
        using dvd_imp_size_le [of b a] ‹a ≠ 0› by simp
    next
      case euclidean_relation
      with ‹euclidean_size a < euclidean_size b› that
      show ?case
        by simp
    qed
    then show ‹a div b = 0›
      by simp
  qed
  with ‹b ≠ 0› show ?thesis
    by simp
qed

lemma div_mult1_eq:
  ‹(a * b) div c = a * (b div c) + a * (b mod c) div c›
proof -
  have *: ‹(a * b) mod c + (a * (c * (b div c)) + c * (a * (b mod c) div c)) = a * b› (is ‹?A + (?B + ?C) = _›)
  proof -
    have ‹?A = a * (b mod c) mod c›
      by (simp add: mod_mult_right_eq)
    then have ‹?C + ?A = a * (b mod c)›
      by (simp add: mult_div_mod_eq)
    then have ‹?B + (?C + ?A) = a * (c * (b div c) + (b mod c))›
      by (simp add: algebra_simps)
    also have ‹… = a * b›
      by (simp add: mult_div_mod_eq)
    finally show ?thesis
      by (simp add: algebra_simps)
  qed
  have ‹((a * b) div c, (a * b) mod c) = (a * (b div c) + a * (b mod c) div c, (a * b) mod c)›
  proof (induction rule: euclidean_relationI)
    case by0
    then show ?case by simp
  next
    case divides
    with * show ?case
      by (simp add: algebra_simps)
  next
    case euclidean_relation
    with * show ?case
      by (simp add: division_segment_mod mod_size_less algebra_simps)
  qed
  then show ?thesis
    by simp
qed

lemma div_add1_eq:
  ‹(a + b) div c = a div c + b div c + (a mod c + b mod c) div c›
proof -
  have *: ‹(a + b) mod c + (c * (a div c) + (c * (b div c) + c * ((a mod c + b mod c) div c))) = a + b›
    (is ‹?A + (?B + (?C + ?D)) = _›)
  proof -
    have ‹?A + (?B + (?C + ?D)) = ?A + ?D + (?B + ?C)›
      by (simp add: ac_simps)
    also have ‹?A + ?D = (a mod c + b mod c) mod c + ?D›
      by (simp add: mod_add_eq)
    also have ‹… = a mod c + b mod c›
      by (simp add: mod_mult_div_eq)
    finally have ‹?A + (?B + (?C + ?D)) = (a mod c + ?B) + (b mod c + ?C)›
      by (simp add: ac_simps)
    then show ?thesis
      by (simp add: mod_mult_div_eq)
  qed
  have ‹((a + b) div c, (a + b) mod c) = (a div c + b div c + (a mod c + b mod c) div c, (a + b) mod c)›
  proof (induction rule: euclidean_relationI)
    case by0
    then show ?case
      by simp
  next
    case divides
    with * show ?case
      by (simp add: algebra_simps)
  next
    case euclidean_relation
    with * show ?case
      by (simp add: division_segment_mod mod_size_less algebra_simps)
  qed
  then show ?thesis
    by simp
qed

end

class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
begin

subclass euclidean_ring_cancel ..

end


subsection ‹Division on \<^typ>‹nat››

instantiation nat :: normalization_semidom
begin

definition normalize_nat :: ‹nat ⇒ nat›
  where [simp]: ‹normalize = (id :: nat ⇒ nat)›

definition unit_factor_nat :: ‹nat ⇒ nat›
  where ‹unit_factor n = of_bool (n > 0)› for n :: nat

lemma unit_factor_simps [simp]:
  ‹unit_factor 0 = (0::nat)›
  ‹unit_factor (Suc n) = 1›
  by (simp_all add: unit_factor_nat_def)

definition divide_nat :: ‹nat ⇒ nat ⇒ nat›
  where ‹m div n = (if n = 0 then 0 else Max {k. k * n ≤ m})› for m n :: nat

instance
  by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)

end

lemma coprime_Suc_0_left [simp]:
  "coprime (Suc 0) n"
  using coprime_1_left [of n] by simp

lemma coprime_Suc_0_right [simp]:
  "coprime n (Suc 0)"
  using coprime_1_right [of n] by simp

lemma coprime_common_divisor_nat: "coprime a b ⟹ x dvd a ⟹ x dvd b ⟹ x = 1"
  for a b :: nat
  by (drule coprime_common_divisor [of _ _ x]) simp_all

instantiation nat :: unique_euclidean_semiring
begin

definition euclidean_size_nat :: ‹nat ⇒ nat›
  where [simp]: ‹euclidean_size_nat = id›

definition division_segment_nat :: ‹nat ⇒ nat›
  where [simp]: ‹division_segment n = 1› for n :: nat

definition modulo_nat :: ‹nat ⇒ nat ⇒ nat›
  where ‹m mod n = m - (m div n * n)› for m n :: nat

instance proof
  fix m n :: nat
  have ex: "∃k. k * n ≤ l" for l :: nat
    by (rule exI [of _ 0]) simp
  have fin: "finite {k. k * n ≤ l}" if "n > 0" for l
  proof -
    from that have "{k. k * n ≤ l} ⊆ {k. k ≤ l}"
      by (cases n) auto
    then show ?thesis
      by (rule finite_subset) simp
  qed
  have mult_div_unfold: "n * (m div n) = Max {l. l ≤ m ∧ n dvd l}"
  proof (cases "n = 0")
    case True
    moreover have "{l. l = 0 ∧ l ≤ m} = {0::nat}"
      by auto
    ultimately show ?thesis
      by simp
  next
    case False
    with ex [of m] fin have "n * Max {k. k * n ≤ m} = Max (times n ` {k. k * n ≤ m})"
      by (auto simp add: nat_mult_max_right intro: hom_Max_commute)
    also have "times n ` {k. k * n ≤ m} = {l. l ≤ m ∧ n dvd l}"
      by (auto simp add: ac_simps elim!: dvdE)
    finally show ?thesis
      using False by (simp add: divide_nat_def ac_simps)
  qed
  have less_eq: "m div n * n ≤ m"
    by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI)
  then show "m div n * n + m mod n = m"
    by (simp add: modulo_nat_def)
  assume "n ≠ 0"
  show "euclidean_size (m mod n) < euclidean_size n"
  proof -
    have "m < Suc (m div n) * n"
    proof (rule ccontr)
      assume "¬ m < Suc (m div n) * n"
      then have "Suc (m div n) * n ≤ m"
        by (simp add: not_less)
      moreover from ‹n ≠ 0› have "Max {k. k * n ≤ m} < Suc (m div n)"
        by (simp add: divide_nat_def)
      with ‹n ≠ 0› ex fin have "⋀k. k * n ≤ m ⟹ k < Suc (m div n)"
        by auto
      ultimately have "Suc (m div n) < Suc (m div n)"
        by blast
      then show False
        by simp
    qed
    with ‹n ≠ 0› show ?thesis
      by (simp add: modulo_nat_def)
  qed
  show "euclidean_size m ≤ euclidean_size (m * n)"
    using ‹n ≠ 0› by (cases n) simp_all
  fix q r :: nat
  show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n"
  proof -
    from that have "r < n"
      by simp
    have "k ≤ q" if "k * n ≤ q * n + r" for k
    proof (rule ccontr)
      assume "¬ k ≤ q"
      then have "q < k"
        by simp
      then obtain l where "k = Suc (q + l)"
        by (auto simp add: less_iff_Suc_add)
      with ‹r < n› that show False
        by (simp add: algebra_simps)
    qed
    with ‹n ≠ 0› ex fin show ?thesis
      by (auto simp add: divide_nat_def Max_eq_iff)
  qed
qed simp_all

end

lemma euclidean_relation_natI [case_names by0 divides euclidean_relation]:
  ‹(m div n, m mod n) = (q, r)›
    if by0: ‹n = 0 ⟹ q = 0 ∧ r = m›
    and divides: ‹n > 0 ⟹ n dvd m ⟹ r = 0 ∧ m = q * n›
    and euclidean_relation: ‹n > 0 ⟹ ¬ n dvd m ⟹ r < n ∧ m = q * n + r› for m n q r :: nat
  by (rule euclidean_relationI) (use that in simp_all)

lemma div_nat_eqI:
  ‹m div n = q› if ‹n * q ≤ m› and ‹m < n * Suc q› for m n q :: nat
proof -
  have ‹(m div n, m mod n) = (q, m - n * q)›
  proof (induction rule: euclidean_relation_natI)
    case by0
    with that show ?case
      by simp
  next
    case divides
    from ‹n dvd m› obtain s where ‹m = n * s› ..
    with ‹n > 0› that have ‹s < Suc q›
      by (simp only: mult_less_cancel1)
    with ‹m = n * s› ‹n > 0› that have ‹q = s›
      by simp
    with ‹m = n * s› show ?case
      by (simp add: ac_simps)
  next
    case euclidean_relation
    with that show ?case
      by (simp add: ac_simps)
  qed
  then show ?thesis
    by simp
qed

lemma mod_nat_eqI:
  ‹m mod n = r› if ‹r < n› and ‹r ≤ m› and ‹n dvd m - r› for m n r :: nat
proof -
  have ‹(m div n, m mod n) = ((m - r) div n, r)›
  proof (induction rule: euclidean_relation_natI)
    case by0
    with that show ?case
      by simp
  next
    case divides
    from that dvd_minus_add [of r ‹m› 1 n]
    have ‹n dvd m + (n - r)›
      by simp
    with divides have ‹n dvd n - r›
      by (simp add: dvd_add_right_iff)
    then have ‹n ≤ n - r›
      by (rule dvd_imp_le) (use ‹r < n› in simp)
    with ‹n > 0› have ‹r = 0›
      by simp
    with ‹n > 0› that show ?case
      by simp
  next
    case euclidean_relation
    with that show ?case
      by (simp add: ac_simps)
  qed
  then show ?thesis
    by simp
qed

text ‹Tool support›

ML ‹
structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
(
  val div_name = \<^const_name>‹divide›;
  val mod_name = \<^const_name>‹modulo›;
  val mk_binop = HOLogic.mk_binop;
  val dest_plus = HOLogic.dest_bin \<^const_name>‹Groups.plus› HOLogic.natT;
  val mk_sum = Arith_Data.mk_sum;
  fun dest_sum tm =
    if HOLogic.is_zero tm then []
    else
      (case try HOLogic.dest_Suc tm of
        SOME t => HOLogic.Suc_zero :: dest_sum t
      | NONE =>
          (case try dest_plus tm of
            SOME (t, u) => dest_sum t @ dest_sum u
          | NONE => [tm]));

  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};

  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
)
›

simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
  ‹K Cancel_Div_Mod_Nat.proc›

lemma div_mult_self_is_m [simp]:
  "m * n div n = m" if "n > 0" for m n :: nat
  using that by simp

lemma div_mult_self1_is_m [simp]:
  "n * m div n = m" if "n > 0" for m n :: nat
  using that by simp

lemma mod_less_divisor [simp]:
  "m mod n < n" if "n > 0" for m n :: nat
  using mod_size_less [of n m] that by simp

lemma mod_le_divisor [simp]:
  "m mod n ≤ n" if "n > 0" for m n :: nat
  using that by (auto simp add: le_less)

lemma div_times_less_eq_dividend [simp]:
  "m div n * n ≤ m" for m n :: nat
  by (simp add: minus_mod_eq_div_mult [symmetric])

lemma times_div_less_eq_dividend [simp]:
  "n * (m div n) ≤ m" for m n :: nat
  using div_times_less_eq_dividend [of m n]
  by (simp add: ac_simps)

lemma dividend_less_div_times:
  "m < n + (m div n) * n" if "0 < n" for m n :: nat
proof -
  from that have "m mod n < n"
    by simp
  then show ?thesis
    by (simp add: minus_mod_eq_div_mult [symmetric])
qed

lemma dividend_less_times_div:
  "m < n + n * (m div n)" if "0 < n" for m n :: nat
  using dividend_less_div_times [of n m] that
  by (simp add: ac_simps)

lemma mod_Suc_le_divisor [simp]:
  "m mod Suc n ≤ n"
  using mod_less_divisor [of "Suc n" m] by arith

lemma mod_less_eq_dividend [simp]:
  "m mod n ≤ m" for m n :: nat
proof (rule add_leD2)
  from div_mult_mod_eq have "m div n * n + m mod n = m" .
  then show "m div n * n + m mod n ≤ m" by auto
qed

lemma
  div_less [simp]: "m div n = 0"
  and mod_less [simp]: "m mod n = m"
  if "m < n" for m n :: nat
  using that by (auto intro: div_nat_eqI mod_nat_eqI)

lemma split_div:
  ‹P (m div n) ⟷
    (n = 0 ⟶ P 0) ∧
    (n ≠ 0 ⟶ (∀i j. j < n ∧ m = n * i + j ⟶ P i))› (is ?div)
  and split_mod:
  ‹Q (m mod n) ⟷
    (n = 0 ⟶ Q m) ∧
    (n ≠ 0 ⟶ (∀i j. j < n ∧ m = n * i + j ⟶ Q j))› (is ?mod)
  for m n :: nat
proof -
  have *: ‹R (m div n) (m mod n) ⟷
    (n = 0 ⟶ R 0 m) ∧
    (n ≠ 0 ⟶ (∀i j. j < n ∧ m = n * i + j ⟶ R i j))› for R
    by (cases ‹n = 0›) auto
  from * [of ‹λq _. P q›] show ?div .
  from * [of ‹λ_ r. Q r›] show ?mod .
qed

declare split_div [of _ _ ‹numeral n›, linarith_split] for n
declare split_mod [of _ _ ‹numeral n›, linarith_split] for n

lemma split_div':
  "P (m div n) ⟷ n = 0 ∧ P 0 ∨ (∃q. (n * q ≤ m ∧ m < n * Suc q) ∧ P q)"
proof (cases "n = 0")
  case True
  then show ?thesis
    by simp
next
  case False
  then have "n * q ≤ m ∧ m < n * Suc q ⟷ m div n = q" for q
    by (auto intro: div_nat_eqI dividend_less_times_div)
  then show ?thesis
    by auto
qed

lemma le_div_geq:
  "m div n = Suc ((m - n) div n)" if "0 < n" and "n ≤ m" for m n :: nat
proof -
  from ‹n ≤ m› obtain q where "m = n + q"
    by (auto simp add: le_iff_add)
  with ‹0 < n› show ?thesis
    by (simp add: div_add_self1)
qed

lemma le_mod_geq:
  "m mod n = (m - n) mod n" if "n ≤ m" for m n :: nat
proof -
  from ‹n ≤ m› obtain q where "m = n + q"
    by (auto simp add: le_iff_add)
  then show ?thesis
    by simp
qed

lemma div_if:
  "m div n = (if m < n ∨ n = 0 then 0 else Suc ((m - n) div n))"
  by (simp add: le_div_geq)

lemma mod_if:
  "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat
  by (simp add: le_mod_geq)

lemma div_eq_0_iff:
  "m div n = 0 ⟷ m < n ∨ n = 0" for m n :: nat
  by (simp add: div_eq_0_iff)

lemma div_greater_zero_iff:
  "m div n > 0 ⟷ n ≤ m ∧ n > 0" for m n :: nat
  using div_eq_0_iff [of m n] by auto

lemma mod_greater_zero_iff_not_dvd:
  "m mod n > 0 ⟷ ¬ n dvd m" for m n :: nat
  by (simp add: dvd_eq_mod_eq_0)

lemma div_by_Suc_0 [simp]:
  "m div Suc 0 = m"
  using div_by_1 [of m] by simp

lemma mod_by_Suc_0 [simp]:
  "m mod Suc 0 = 0"
  using mod_by_1 [of m] by simp

lemma div2_Suc_Suc [simp]:
  "Suc (Suc m) div 2 = Suc (m div 2)"
  by (simp add: numeral_2_eq_2 le_div_geq)

lemma Suc_n_div_2_gt_zero [simp]:
  "0 < Suc n div 2" if "n > 0" for n :: nat
  using that by (cases n) simp_all

lemma div_2_gt_zero [simp]:
  "0 < n div 2" if "Suc 0 < n" for n :: nat
  using that Suc_n_div_2_gt_zero [of "n - 1"] by simp

lemma mod2_Suc_Suc [simp]:
  "Suc (Suc m) mod 2 = m mod 2"
  by (simp add: numeral_2_eq_2 le_mod_geq)

lemma add_self_div_2 [simp]:
  "(m + m) div 2 = m" for m :: nat
  by (simp add: mult_2 [symmetric])

lemma add_self_mod_2 [simp]:
  "(m + m) mod 2 = 0" for m :: nat
  by (simp add: mult_2 [symmetric])

lemma mod2_gr_0 [simp]:
  "0 < m mod 2 ⟷ m mod 2 = 1" for m :: nat
proof -
  have "m mod 2 < 2"
    by (rule mod_less_divisor) simp
  then have "m mod 2 = 0 ∨ m mod 2 = 1"
    by arith
  then show ?thesis
    by auto
qed

lemma mod_Suc_eq [mod_simps]:
  "Suc (m mod n) mod n = Suc m mod n"
proof -
  have "(m mod n + 1) mod n = (m + 1) mod n"
    by (simp only: mod_simps)
  then show ?thesis
    by simp
qed

lemma mod_Suc_Suc_eq [mod_simps]:
  "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n"
proof -
  have "(m mod n + 2) mod n = (m + 2) mod n"
    by (simp only: mod_simps)
  then show ?thesis
    by simp
qed

lemma
  Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n"
  and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n"
  and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n"
  and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n"
  by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+

lemma Suc_0_mod_eq [simp]:
  "Suc 0 mod n = of_bool (n ≠ Suc 0)"
  by (cases n) simp_all

lemma div_mult2_eq:
    ‹m div (n * q) = (m div n) div q› (is ?Q)
  and mod_mult2_eq:
    ‹m mod (n * q) = n * (m div n mod q) + m mod n› (is ?R)
  for m n q :: nat
proof -
  have ‹(m div (n * q), m mod (n * q)) = ((m div n) div q, n * (m div n mod q) + m mod n)›
  proof (induction rule: euclidean_relation_natI)
    case by0
    then show ?case
      by auto
  next
    case divides
    from ‹n * q dvd m› obtain t where ‹m = n * q * t› ..
    with ‹n * q > 0› show ?case
      by (simp add: algebra_simps)
  next
    case euclidean_relation
    then have ‹n > 0› ‹q > 0›
      by simp_all
    from ‹n > 0› have ‹m mod n < n›
      by (rule mod_less_divisor)
    from ‹q > 0› have ‹m div n mod q < q›
      by (rule mod_less_divisor)
    then obtain s where ‹q = Suc (m div n mod q + s)›
      by (blast dest: less_imp_Suc_add)
    moreover have ‹m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)›
      using ‹m mod n < n› by (simp add: add_mult_distrib2)
    ultimately have ‹m mod n + n * (m div n mod q) < n * q›
      by simp
    then show ?case
      by (simp add: algebra_simps flip: add_mult_distrib2)
  qed
  then show ?Q and ?R
    by simp_all
qed

lemma div_le_mono:
  "m div k ≤ n div k" if "m ≤ n" for m n k :: nat
proof -
  from that obtain q where "n = m + q"
    by (auto simp add: le_iff_add)
  then show ?thesis
    by (simp add: div_add1_eq [of m q k])
qed

text ‹Antimonotonicity of \<^const>‹divide› in second argument›

lemma div_le_mono2:
  "k div n ≤ k div m" if "0 < m" and "m ≤ n" for m n k :: nat
using that proof (induct k arbitrary: m rule: less_induct)
  case (less k)
  show ?case
  proof (cases "n ≤ k")
    case False
    then show ?thesis
      by simp
  next
    case True
    have "(k - n) div n ≤ (k - m) div n"
      using less.prems
      by (blast intro: div_le_mono diff_le_mono2)
    also have "… ≤ (k - m) div m"
      using ‹n ≤ k› less.prems less.hyps [of "k - m" m]
      by simp
    finally show ?thesis
      using ‹n ≤ k› less.prems
      by (simp add: le_div_geq)
  qed
qed

lemma div_le_dividend [simp]:
  "m div n ≤ m" for m n :: nat
  using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all

lemma div_less_dividend [simp]:
  "m div n < m" if "1 < n" and "0 < m" for m n :: nat
using that proof (induct m rule: less_induct)
  case (less m)
  show ?case
  proof (cases "n < m")
    case False
    with less show ?thesis
      by (cases "n = m") simp_all
  next
    case True
    then show ?thesis
      using less.hyps [of "m - n"] less.prems
      by (simp add: le_div_geq)
  qed
qed

lemma div_eq_dividend_iff:
  "m div n = m ⟷ n = 1" if "m > 0" for m n :: nat
proof
  assume "n = 1"
  then show "m div n = m"
    by simp
next
  assume P: "m div n = m"
  show "n = 1"
  proof (rule ccontr)
    have "n ≠ 0"
      by (rule ccontr) (use that P in auto)
    moreover assume "n ≠ 1"
    ultimately have "n > 1"
      by simp
    with that have "m div n < m"
      by simp
    with P show False
      by simp
  qed
qed

lemma less_mult_imp_div_less:
  "m div n < i" if "m < i * n" for m n i :: nat
proof -
  from that have "i * n > 0"
    by (cases "i * n = 0") simp_all
  then have "i > 0" and "n > 0"
    by simp_all
  have "m div n * n ≤ m"
    by simp
  then have "m div n * n < i * n"
    using that by (rule le_less_trans)
  with ‹n > 0› show ?thesis
    by simp
qed

lemma div_less_iff_less_mult:
  ‹m div q < n ⟷ m < n * q› (is ‹?P ⟷ ?Q›)
  if ‹q > 0› for m n q :: nat
proof
  assume ?Q then show ?P
    by (rule less_mult_imp_div_less)
next
  assume ?P
  then obtain h where ‹n = Suc (m div q + h)›
    using less_natE by blast
  moreover have ‹m < m + (Suc h * q - m mod q)›
    using that by (simp add: trans_less_add1)
  ultimately show ?Q
    by (simp add: algebra_simps flip: minus_mod_eq_mult_div)
qed

lemma less_eq_div_iff_mult_less_eq:
  ‹m ≤ n div q ⟷ m * q ≤ n› if ‹q > 0› for m n q :: nat
  using div_less_iff_less_mult [of q n m] that by auto

lemma div_Suc:
  ‹Suc m div n = (if Suc m mod n = 0 then Suc (m div n) else m div n)›
proof (cases ‹n = 0 ∨ n = 1›)
  case True
  then show ?thesis by auto
next
  case False
  then have ‹n > 1›
    by simp
  then have ‹Suc m div n = m div n + Suc (m mod n) div n›
    using div_add1_eq [of m 1 n] by simp
  also have ‹Suc (m mod n) div n = of_bool (n dvd Suc m)›
  proof (cases ‹n dvd Suc m›)
    case False
    moreover have ‹Suc (m mod n) ≠ n›
    proof (rule ccontr)
      assume ‹¬ Suc (m mod n) ≠ n›
      then have ‹m mod n = n - Suc 0›
        by simp
      with ‹n > 1› have ‹(m + 1) mod n = 0›
        by (subst mod_add_left_eq [symmetric]) simp
      then have ‹n dvd Suc m›
        by auto
      with False show False ..
    qed
    moreover have ‹Suc (m mod n) ≤ n›
      using ‹n > 1› by (simp add: Suc_le_eq)
    ultimately show ?thesis
      by (simp add: div_eq_0_iff)
  next
    case True
    then obtain q where q: ‹Suc m = n * q› ..
    moreover have ‹q > 0› by (rule ccontr)
      (use q in simp)
    ultimately have ‹m mod n = n - Suc 0›
      using ‹n > 1› mult_le_cancel1 [of n ‹Suc 0› q]
      by (auto intro: mod_nat_eqI)
    with True ‹n > 1› show ?thesis
      by simp
  qed
  finally show ?thesis
    by (simp add: mod_greater_zero_iff_not_dvd)
qed

lemma mod_Suc:
  ‹Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))›
proof (cases ‹n = 0›)
  case True
  then show ?thesis
    by simp
next
  case False
  moreover have ‹Suc m mod n = Suc (m mod n) mod n›
    by (simp add: mod_simps)
  ultimately show ?thesis
    by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq)
qed

lemma Suc_times_mod_eq:
  "Suc (m * n) mod m = 1" if "Suc 0 < m"
  using that by (simp add: mod_Suc)

lemma Suc_times_numeral_mod_eq [simp]:
  "Suc (numeral k * n) mod numeral k = 1" if "numeral k ≠ (1::nat)"
  by (rule Suc_times_mod_eq) (use that in simp)

lemma Suc_div_le_mono [simp]:
  "m div n ≤ Suc m div n"
  by (simp add: div_le_mono)

text ‹These lemmas collapse some needless occurrences of Suc:
  at least three Sucs, since two and fewer are rewritten back to Suc again!
  We already have some rules to simplify operands smaller than 3.›

lemma div_Suc_eq_div_add3 [simp]:
  "m div Suc (Suc (Suc n)) = m div (3 + n)"
  by (simp add: Suc3_eq_add_3)

lemma mod_Suc_eq_mod_add3 [simp]:
  "m mod Suc (Suc (Suc n)) = m mod (3 + n)"
  by (simp add: Suc3_eq_add_3)

lemma Suc_div_eq_add3_div:
  "Suc (Suc (Suc m)) div n = (3 + m) div n"
  by (simp add: Suc3_eq_add_3)

lemma Suc_mod_eq_add3_mod:
  "Suc (Suc (Suc m)) mod n = (3 + m) mod n"
  by (simp add: Suc3_eq_add_3)

lemmas Suc_div_eq_add3_div_numeral [simp] =
  Suc_div_eq_add3_div [of _ "numeral v"] for v

lemmas Suc_mod_eq_add3_mod_numeral [simp] =
  Suc_mod_eq_add3_mod [of _ "numeral v"] for v

lemma (in field_char_0) of_nat_div:
  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
proof -
  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
    unfolding of_nat_add by (cases "n = 0") simp_all
  then show ?thesis
    by simp
qed

text ‹An ``induction'' law for modulus arithmetic.›

lemma mod_induct [consumes 3, case_names step]:
  "P m" if "P n" and "n < p" and "m < p"
    and step: "⋀n. n < p ⟹ P n ⟹ P (Suc n mod p)"
using ‹m < p› proof (induct m)
  case 0
  show ?case
  proof (rule ccontr)
    assume "¬ P 0"
    from ‹n < p› have "0 < p"
      by simp
    from ‹n < p› obtain m where "0 < m" and "p = n + m"
      by (blast dest: less_imp_add_positive)
    with ‹P n› have "P (p - m)"
      by simp
    moreover have "¬ P (p - m)"
    using ‹0 < m› proof (induct m)
      case 0
      then show ?case
        by simp
    next
      case (Suc m)
      show ?case
      proof
        assume P: "P (p - Suc m)"
        with ‹¬ P 0› have "Suc m < p"
          by (auto intro: ccontr)
        then have "Suc (p - Suc m) = p - m"
          by arith
        moreover from ‹0 < p› have "p - Suc m < p"
          by arith
        with P step have "P ((Suc (p - Suc m)) mod p)"
          by blast
        ultimately show False
          using ‹¬ P 0› Suc.hyps by (cases "m = 0") simp_all
      qed
    qed
    ultimately show False
      by blast
  qed
next
  case (Suc m)
  then have "m < p" and mod: "Suc m mod p = Suc m"
    by simp_all
  from ‹m < p› have "P m"
    by (rule Suc.hyps)
  with ‹m < p› have "P (Suc m mod p)"
    by (rule step)
  with mod show ?case
    by simp
qed

lemma funpow_mod_eq: ✐‹contributor ‹Lars Noschinski››
  ‹(f ^^ (m mod n)) x = (f ^^ m) x› if ‹(f ^^ n) x = x›
proof -
  have ‹(f ^^ m) x = (f ^^ (m mod n + m div n * n)) x›
    by simp
  also have ‹… = (f ^^ (m mod n)) (((f ^^ n) ^^ (m div n)) x)›
    by (simp only: funpow_add funpow_mult ac_simps) simp
  also have ‹((f ^^ n) ^^ q) x = x› for q
    by (induction q) (use ‹(f ^^ n) x = x› in simp_all)
  finally show ?thesis
    by simp
qed

lemma mod_eq_dvd_iff_nat:
  ‹m mod q = n mod q ⟷ q dvd m - n› (is ‹?P ⟷ ?Q›)
    if ‹m ≥ n› for m n q :: nat
proof
  assume ?Q
  then obtain s where ‹m - n = q * s› ..
  with that have ‹m = q * s + n›
    by simp
  then show ?P
    by simp
next
  assume ?P
  have ‹m - n = m div q * q + m mod q - (n div q * q + n mod q)›
    by simp
  also have ‹… = q * (m div q - n div q)›
    by (simp only: algebra_simps ‹?P›)
  finally show ?Q ..
qed

lemma mod_eq_iff_dvd_symdiff_nat:
  ‹m mod q = n mod q ⟷ q dvd nat ¦int m - int n¦›
  by (auto simp add: abs_if mod_eq_dvd_iff_nat nat_diff_distrib dest: sym intro: sym)

lemma mod_eq_nat1E:
  fixes m n q :: nat
  assumes "m mod q = n mod q" and "m ≥ n"
  obtains s where "m = n + q * s"
proof -
  from assms have "q dvd m - n"
    by (simp add: mod_eq_dvd_iff_nat)
  then obtain s where "m - n = q * s" ..
  with ‹m ≥ n› have "m = n + q * s"
    by simp
  with that show thesis .
qed

lemma mod_eq_nat2E:
  fixes m n q :: nat
  assumes "m mod q = n mod q" and "n ≥ m"
  obtains s where "n = m + q * s"
  using assms mod_eq_nat1E [of n q m] by (auto simp add: ac_simps)

lemma nat_mod_eq_iff:
  "(x::nat) mod n = y mod n ⟷ (∃q1 q2. x + n * q1 = y + n * q2)"  (is "?lhs = ?rhs")
proof
  assume H: "x mod n = y mod n"
  { assume xy: "x ≤ y"
    from H have th: "y mod n = x mod n" by simp
    from mod_eq_nat1E [OF th xy] obtain q where "y = x + n * q" .
    then have "x + n * q = y + n * 0"
      by simp
    then have "∃q1 q2. x + n * q1 = y + n * q2"
      by blast
  }
  moreover
  { assume xy: "y ≤ x"
    from mod_eq_nat1E [OF H xy] obtain q where "x = y + n * q" .
    then have "x + n * 0 = y + n * q"
      by simp
    then have "∃q1 q2. x + n * q1 = y + n * q2"
      by blast
  }
  ultimately show ?rhs using linear[of x y] by blast
next
  assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
  hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
  thus  ?lhs by simp
qed


subsection ‹Division on \<^typ>‹int››

text ‹
  The following specification of integer division rounds towards minus infinity
  and is advocated by Donald Knuth. See \cite{leijen01} for an overview and
  terminology of different possibilities to specify integer division;
  there division rounding towards minus infinitiy is named ``F-division''.
›

subsubsection ‹Basic instantiation›

instantiation int :: "{normalization_semidom, idom_modulo}"
begin

definition normalize_int :: ‹int ⇒ int›
  where [simp]: ‹normalize = (abs :: int ⇒ int)›

definition unit_factor_int :: ‹int ⇒ int›
  where [simp]: ‹unit_factor = (sgn :: int ⇒ int)›

definition divide_int :: ‹int ⇒ int ⇒ int›
  where ‹k div l = (sgn k * sgn l * int (nat ¦k¦ div nat ¦l¦)
    - of_bool (l ≠ 0 ∧ sgn k ≠ sgn l ∧ ¬ l dvd k))›

lemma divide_int_unfold:
  ‹(sgn k * int m) div (sgn l * int n) = (sgn k * sgn l * int (m div n)
    - of_bool ((k = 0 ⟷ m = 0) ∧ l ≠ 0 ∧ n ≠ 0 ∧ sgn k ≠ sgn l ∧ ¬ n dvd m))›
  by (simp add: divide_int_def sgn_mult nat_mult_distrib abs_mult sgn_eq_0_iff ac_simps)

definition modulo_int :: ‹int ⇒ int ⇒ int›
  where ‹k mod l = sgn k * int (nat ¦k¦ mod nat ¦l¦) + l * of_bool (sgn k ≠ sgn l ∧ ¬ l dvd k)›

lemma modulo_int_unfold:
  ‹(sgn k * int m) mod (sgn l * int n) =
    sgn k * int (m mod (of_bool (l ≠ 0) * n)) + (sgn l * int n) * of_bool ((k = 0 ⟷ m = 0) ∧ sgn k ≠ sgn l ∧ ¬ n dvd m)›
  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)
next
  fix k l :: int
  assume "l ≠ 0"
  obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m"
    by (blast intro: int_sgnE elim: that)
  then have "k * l = sgn (s * t) * int (n * m)"
    by (simp add: ac_simps sgn_mult)
  with k l ‹l ≠ 0› 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


subsubsection ‹Algebraic foundations›

lemma coprime_int_iff [simp]:
  "coprime (int m) (int n) ⟷ coprime m n" (is "?P ⟷ ?Q")
proof
  assume ?P
  show ?Q
  proof (rule coprimeI)
    fix q
    assume "q dvd m" "q dvd n"
    then have "int q dvd int m" "int q dvd int n"
      by simp_all
    with ‹?P› have "is_unit (int q)"
      by (rule coprime_common_divisor)
    then show "is_unit q"
      by simp
  qed
next
  assume ?Q
  show ?P
  proof (rule coprimeI)
    fix k
    assume "k dvd int m" "k dvd int n"
    then have "nat ¦k¦ dvd m" "nat ¦k¦ dvd n"
      by simp_all
    with ‹?Q› have "is_unit (nat ¦k¦)"
      by (rule coprime_common_divisor)
    then show "is_unit k"
      by simp
  qed
qed

lemma coprime_abs_left_iff [simp]:
  "coprime ¦k¦ l ⟷ coprime k l" for k l :: int
  using coprime_normalize_left_iff [of k l] by simp

lemma coprime_abs_right_iff [simp]:
  "coprime k ¦l¦ ⟷ coprime k l" for k l :: int
  using coprime_abs_left_iff [of l k] by (simp add: ac_simps)

lemma coprime_nat_abs_left_iff [simp]:
  "coprime (nat ¦k¦) n ⟷ coprime k (int n)"
proof -
  define m where "m = nat ¦k¦"
  then have "¦k¦ = int m"
    by simp
  moreover have "coprime k (int n) ⟷ coprime ¦k¦ (int n)"
    by simp
  ultimately show ?thesis
    by simp
qed

lemma coprime_nat_abs_right_iff [simp]:
  "coprime n (nat ¦k¦) ⟷ coprime (int n) k"
  using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps)

lemma coprime_common_divisor_int: "coprime a b ⟹ x dvd a ⟹ x dvd b ⟹ ¦x¦ = 1"
  for a b :: int
  by (drule coprime_common_divisor [of _ _ x]) simp_all


subsubsection ‹Basic conversions›

lemma div_abs_eq_div_nat:
  "¦k¦ div ¦l¦ = int (nat ¦k¦ div nat ¦l¦)"
  by (auto simp add: divide_int_def)

lemma div_eq_div_abs:
  ‹k div l = sgn k * sgn l * (¦k¦ div ¦l¦)
    - of_bool (l ≠ 0 ∧ sgn k ≠ sgn l ∧ ¬ l dvd k)›
  for k l :: int
  by (simp add: divide_int_def [of k l] div_abs_eq_div_nat)

lemma div_abs_eq:
  ‹¦k¦ div ¦l¦ = sgn k * sgn l * (k div l + of_bool (sgn k ≠ sgn l ∧ ¬ l dvd k))›
  for k l :: int
  by (simp add: div_eq_div_abs [of k l] ac_simps)

lemma mod_abs_eq_div_nat:
  "¦k¦ mod ¦l¦ = int (nat ¦k¦ mod nat ¦l¦)"
  by (simp add: modulo_int_def)

lemma mod_eq_mod_abs:
  ‹k mod l = sgn k * (¦k¦ mod ¦l¦) + l * of_bool (sgn k ≠ sgn l ∧ ¬ l dvd k)›
  for k l :: int
  by (simp add: modulo_int_def [of k l] mod_abs_eq_div_nat)

lemma mod_abs_eq:
  ‹¦k¦ mod ¦l¦ = sgn k * (k mod l - l * of_bool (sgn k ≠ sgn l ∧ ¬ l dvd k))›
  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 ≠ 0"
  shows "(sgn v * ¦k¦) div (sgn v * ¦l¦) = ¦k¦ div ¦l¦"
  using assms by (simp add: sgn_mult abs_mult sgn_0_0
    divide_int_def [of "sgn v * ¦k¦" "sgn v * ¦l¦"] 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 = ¦k¦ div ¦l¦"
  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) * (¦k¦ div ¦l¦)"
  using assms by (auto simp add: div_abs_eq ac_simps)

lemma div_noneq_sgn_abs:
  fixes k l :: int
  assumes "l ≠ 0"
  assumes "sgn k ≠ sgn l"
  shows "k div l = - (¦k¦ div ¦l¦) - of_bool (¬ l dvd k)"
  using assms by (auto simp add: div_abs_eq ac_simps sgn_0_0 dest!: sgn_not_eq_imp)


subsubsection ‹Euclidean division›

instantiation int :: unique_euclidean_ring
begin

definition euclidean_size_int :: "int ⇒ nat"
  where [simp]: "euclidean_size_int = (nat ∘ abs :: int ⇒ nat)"

definition division_segment_int :: "int ⇒ int"
  where "division_segment_int k = (if k ≥ 0 then 1 else - 1)"

lemma division_segment_eq_sgn:
  "division_segment k = sgn k" if "k ≠ 0" for k :: int
  using that by (simp add: division_segment_int_def)

lemma abs_division_segment [simp]:
  "¦division_segment k¦ = 1" for k :: int
  by (simp add: division_segment_int_def)

lemma abs_mod_less:
  "¦k mod l¦ < ¦l¦" if "l ≠ 0" for k l :: int
proof -
  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)
  with that show ?thesis
    by (auto simp add: modulo_int_unfold abs_mult mod_greater_zero_iff_not_dvd
        simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
      (simp add: sgn_0_0)
qed

lemma sgn_mod:
  "sgn (k mod l) = sgn l" if "l ≠ 0" "¬ l dvd k" for k l :: int
proof -
  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)
  with that show ?thesis
    by (auto simp add: modulo_int_unfold sgn_mult mod_greater_zero_iff_not_dvd
      simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
qed

instance proof
  fix k l :: int
  show "division_segment (k mod l) = division_segment l" if
    "l ≠ 0" and "¬ l dvd k"
    using that by (simp add: division_segment_eq_sgn dvd_eq_mod_eq_0 sgn_mod)
next
  fix l q r :: int
  obtain n m and s t
     where l: "l = sgn s * int n" and q: "q = sgn t * int m"
    by (blast intro: int_sgnE elim: that)
  assume ‹l ≠ 0›
  with l have "s ≠ 0" and "n > 0"
    by (simp_all add: sgn_0_0)
  assume "division_segment r = division_segment l"
  moreover have "r = sgn r * ¦r¦"
    by (simp add: sgn_mult_abs)
  moreover define u where "u = nat ¦r¦"
  ultimately have "r = sgn l * int u"
    using division_segment_eq_sgn ‹l ≠ 0› by (cases "r = 0") simp_all
  with l ‹n > 0› have r: "r = sgn s * int u"
    by (simp add: sgn_mult)
  assume "euclidean_size r < euclidean_size l"
  with l r ‹s ≠ 0› have "u < n"
    by (simp add: abs_mult)
  show "(q * l + r) div l = q"
  proof (cases "q = 0 ∨ r = 0")
    case True
    then show ?thesis
    proof
      assume "q = 0"
      then show ?thesis
        using l r ‹u < n› by (simp add: divide_int_unfold)
    next
      assume "r = 0"
      from ‹r = 0› have *: "q * l + r = sgn (t * s) * int (n * m)"
        using q l by (simp add: ac_simps sgn_mult)
      from ‹s ≠ 0› ‹n > 0› show ?thesis
        by (simp only: *, simp only: * q l divide_int_unfold)
          (auto simp add: sgn_mult ac_simps)
    qed
  next
    case False
    with q r have "t ≠ 0" and "m > 0" and "s ≠ 0" and "u > 0"
      by (simp_all add: sgn_0_0)
    moreover from ‹0 < m› ‹u < n› have "u ≤ m * n"
      using mult_le_less_imp_less [of 1 m u n] by simp
    ultimately have *: "q * l + r = sgn (s * t)
      * int (if t < 0 then m * n - u else m * n + u)"
      using l q r
      by (simp add: sgn_mult algebra_simps of_nat_diff)
    have "(m * n - u) div n = m - 1" if "u > 0"
      using ‹0 < m› ‹u < n› that
      by (auto intro: div_nat_eqI simp add: algebra_simps)
    moreover have "n dvd m * n - u ⟷ n dvd u"
      using ‹u ≤ m * n› dvd_diffD1 [of n "m * n" u]
      by auto
    ultimately show ?thesis
      using ‹s ≠ 0› ‹m > 0› ‹u > 0› ‹u < n› ‹u ≤ m * n›
      by (simp only: *, simp only: l q divide_int_unfold)
        (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le)
  qed
qed (use mult_le_mono2 [of 1] in ‹auto simp add: division_segment_int_def not_le zero_less_mult_iff mult_less_0_iff abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib›)

end

lemma euclidean_relation_intI [case_names by0 divides euclidean_relation]:
  ‹(k div l, k mod l) = (q, r)›
    if by0': ‹l = 0 ⟹ q = 0 ∧ r = k›
    and divides': ‹l ≠ 0 ⟹ l dvd k ⟹ r = 0 ∧ k = q * l›
    and euclidean_relation': ‹l ≠ 0 ⟹ ¬ l dvd k ⟹ sgn r = sgn l
      ∧ ¦r¦ < ¦l¦ ∧ k = q * l + r› for k l :: int
proof (induction rule: euclidean_relationI)
  case by0
  then show ?case
    by (rule by0')
next
  case divides
  then show ?case
    by (rule divides')
next
  case euclidean_relation
  with euclidean_relation' have ‹sgn r = sgn l› ‹¦r¦ < ¦l¦› ‹k = q * l + r›
    by simp_all
  from ‹sgn r = sgn l› ‹l ≠ 0› have ‹division_segment r = division_segment l›
    by (simp add: division_segment_int_def sgn_if split: if_splits)
  with ‹¦r¦ < ¦l¦› ‹k = q * l + r›
  show ?case
    by simp
qed


subsubsection ‹Trivial reduction steps›

lemma div_pos_pos_trivial [simp]:
  "k div l = 0" if "k ≥ 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 ≥ 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 ≤ 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 ≤ 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›  (is ?Q)
  and mod_pos_neg_trivial: ‹k mod l = k + l›  (is ?R)
    if ‹0 < k› and ‹k + l ≤ 0› for k l :: int
proof -
  from that have ‹l < 0›
    by simp
  have ‹(k div l, k mod l) = (- 1, k + l)›
  proof (induction rule: euclidean_relation_intI)
    case by0
    with ‹l < 0› show ?case
      by simp
  next
    case divides
    from ‹l dvd k› obtain j where ‹k = l * j› ..
    with ‹l < 0› ‹0 < k› have ‹j < 0›
      by (simp add: zero_less_mult_iff)
    moreover from ‹k + l ≤ 0› ‹k = l * j› have ‹l * (j + 1) ≤ 0›
      by (simp add: algebra_simps)
    with ‹l < 0› have ‹j + 1 ≥ 0›
      by (simp add: mult_le_0_iff)
    with ‹j < 0› have ‹j = - 1›
      by simp
    with ‹k = l * j› show ?case
      by simp
  next
    case euclidean_relation
    with ‹k + l ≤ 0› have ‹k + l < 0›
      by (auto simp add: less_le add_eq_0_iff)
    with ‹0 < k› show ?case
      by simp
  qed
  then show ?Q and ?R
    by simp_all
qed

text ‹There is neither ‹div_neg_pos_trivial› nor ‹mod_neg_pos_trivial›
  because \<^term>‹0 div l = 0› would supersede it.›


subsubsection ‹More uniqueness rules›

lemma
  fixes a b q r :: int
  assumes ‹a = b * q + r› ‹0 ≤ r› ‹r < b›
  shows int_div_pos_eq:
      ‹a div b = q› (is ?Q)
    and int_mod_pos_eq:
      ‹a mod b = r› (is ?R)
proof -
  have ‹(a div b, a mod b) = (q, r)›
    by (induction rule: euclidean_relation_intI)
      (use assms in ‹auto simp add: ac_simps dvd_add_left_iff sgn_1_pos le_less dest: zdvd_imp_le›)
  then show ?Q and ?R
    by simp_all
qed

lemma int_div_neg_eq:
  ‹a div b = q› if ‹a = b * q + r› ‹r ≤ 0› ‹b < r› for a b q r :: int
  using that int_div_pos_eq [of a ‹- b› ‹- q› ‹- r›] by simp_all

lemma int_mod_neg_eq:
  ‹a mod b = r› if ‹a = b * q + r› ‹r ≤ 0› ‹b < r› for a b q r :: int
  using that int_div_neg_eq [of a b q r] by simp


subsubsection ‹Laws for unary minus›

lemma zmod_zminus1_not_zero:
  fixes k l :: int
  shows "- k mod l ≠ 0 ⟹ k mod l ≠ 0"
  by (simp add: mod_eq_0_iff_dvd)

lemma zmod_zminus2_not_zero:
  fixes k l :: int
  shows "k mod - l ≠ 0 ⟹ k mod l ≠ 0"
  by (simp add: mod_eq_0_iff_dvd)

lemma zdiv_zminus1_eq_if:
  ‹(- a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)›
  if ‹b ≠ 0› for a b :: int
  using that sgn_not_eq_imp [of b ‹- a›]
  by (cases ‹a = 0›) (auto simp add: div_eq_div_abs [of ‹- a› b] div_eq_div_abs [of a b] sgn_eq_0_iff)

lemma zdiv_zminus2_eq_if:
  ‹a div (- b) = (if a mod b = 0 then - (a div b) else - (a div b) - 1)›
  if ‹b ≠ 0› for a b :: int
  using that by (auto simp add: zdiv_zminus1_eq_if div_minus_right)

lemma zmod_zminus1_eq_if:
  ‹(- a) mod b = (if a mod b = 0 then 0 else b - (a mod b))›
  for a b :: int
  by (cases ‹b = 0›)
    (auto simp flip: minus_div_mult_eq_mod simp add: zdiv_zminus1_eq_if algebra_simps)

lemma zmod_zminus2_eq_if:
  ‹a mod (- b) = (if a mod b = 0 then 0 else (a mod b) - b)›
  for a b :: int
  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)


subsubsection ‹Borders›

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 ≤ 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 ≤ 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 ‹int (m mod n) ≤ int n›
    using ‹Suc q = n› by simp
  then have ‹sgn s * int (m mod n) ≤ int n›
    by (cases s ‹0::int› rule: linorder_cases) simp_all
  ultimately show ?thesis
    by (simp only: modulo_int_unfold) auto
qed


subsubsection ‹Splitting Rules for div and mod›

lemma split_zdiv:
  ‹P (n div k) ⟷
    (k = 0 ⟶ P 0) ∧
    (0 < k ⟶ (∀i j. 0 ≤ j ∧ j < k ∧ n = k * i + j ⟶ P i)) ∧
    (k < 0 ⟶ (∀i j. k < j ∧ j ≤ 0 ∧ n = k * i + j ⟶ P i))› (is ?div)
  and split_zmod:
  ‹Q (n mod k) ⟷
    (k = 0 ⟶ Q n) ∧
    (0 < k ⟶ (∀i j. 0 ≤ j ∧ j < k ∧ n = k * i + j ⟶ Q j)) ∧
    (k < 0 ⟶ (∀i j. k < j ∧ j ≤ 0 ∧ n = k * i + j ⟶ Q j))› (is ?mod)
  for n k :: int
proof -
  have *: ‹R (n div k) (n mod k) ⟷
    (k = 0 ⟶ R 0 n) ∧
    (0 < k ⟶ (∀i j. 0 ≤ j ∧ j < k ∧ n = k * i + j ⟶ R i j)) ∧
    (k < 0 ⟶ (∀i j. k < j ∧ j ≤ 0 ∧ n = k * i + j ⟶ R i j))› for R
    by (cases ‹k = 0›)
      (auto simp add: linorder_class.neq_iff)
  from * [of ‹λq _. P q›] show ?div .
  from * [of ‹λ_ r. Q r›] show ?mod .
qed

text ‹Enable (lin)arith to deal with \<^const>‹divide› and \<^const>‹modulo›
  when these are applied to some constant that is of the form
  \<^term>‹numeral k›:›
declare split_zdiv [of _ _ ‹numeral n›, linarith_split] for n
declare split_zdiv [of _ _ ‹- numeral n›, linarith_split] for n
declare split_zmod [of _ _ ‹numeral n›, linarith_split] for n
declare split_zmod [of _ _ ‹- numeral n›, linarith_split] for n

lemma zdiv_eq_0_iff:
  "i div k = 0 ⟷ k = 0 ∨ 0 ≤ i ∧ i < k ∨ i ≤ 0 ∧ k < i" (is "?L = ?R")
  for i k :: int
proof
  assume ?L
  moreover have "?L ⟶ ?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 ⟷ k = 0 ∨ 0 ≤ i ∧ i < k ∨ i ≤ 0 ∧ k < i"
proof -
  have "i mod k = i ⟷ 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 ‹Algebraic rewrites›

lemma zdiv_zmult2_eq: ‹a div (b * c) = (a div b) div c›  (is ?Q)
  and zmod_zmult2_eq: ‹a mod (b * c) = b * (a div b mod c) + a mod b›  (is ?P)
  if ‹c ≥ 0› for a b c :: int
proof -
  have *: ‹(a div (b * c), a mod (b * c)) = ((a div b) div c, b * (a div b mod c) + a mod b)›
    if ‹b > 0› for a b
  proof (induction rule: euclidean_relationI)
    case by0
    then show ?case by auto
  next
    case divides
    then obtain d where ‹a = b * c * d›
      by blast
    with divides that show ?case
      by (simp add: ac_simps)
  next
    case euclidean_relation
    with ‹b > 0› ‹c ≥ 0› have ‹0 < c› ‹b > 0›
      by simp_all
    then have ‹a mod b < b›
      by simp
    moreover have ‹1 ≤ c - a div b mod c›
      using ‹c > 0› by (simp add: int_one_le_iff_zero_less)
    ultimately have ‹a mod b * 1 < b * (c - a div b mod c)›
      by (rule mult_less_le_imp_less) (use ‹b > 0› in simp_all)
    with ‹0 < b› ‹0 < c› show ?case
      by (simp add: division_segment_int_def algebra_simps flip: minus_mod_eq_mult_div)
  qed
  show ?Q
  proof (cases ‹b ≥ 0›)
    case True
    with * [of b a] show ?thesis
      by (cases ‹b = 0›) simp_all
  next
    case False
    with * [of ‹- b› ‹- a›] show ?thesis
      by simp
  qed
  show ?P
  proof (cases ‹b ≥ 0›)
    case True
    with * [of b a] show ?thesis
      by (cases ‹b = 0›) simp_all
  next
    case False
    with * [of ‹- b› ‹- a›] show ?thesis
      by simp
  qed
qed

lemma zdiv_zmult2_eq':
  ‹k div (l * j) = ((sgn j * k) div l) div ¦j¦› for k l j :: int
proof -
  have ‹k div (l * j) = (sgn j * k) div (sgn j * (l * j))›
    by (simp add: sgn_0_0)
  also have ‹sgn j * (l * j) = l * ¦j¦›
    by (simp add: mult.left_commute [of _ l] abs_sgn) (simp add: ac_simps)
  also have ‹(sgn j * k) div (l * ¦j¦) = ((sgn j * k) div l) div ¦j¦›
    by (simp add: zdiv_zmult2_eq)
  finally show ?thesis .
qed

lemma half_nonnegative_int_iff [simp]:
  ‹k div 2 ≥ 0 ⟷ k ≥ 0› for k :: int
  by auto

lemma half_negative_int_iff [simp]:
  ‹k div 2 < 0 ⟷ k < 0› for k :: int
  by auto


subsubsection ‹Distributive laws for conversions.›

lemma zdiv_int:
  ‹int (m div n) = int m div int n›
  by (cases ‹m = 0›) (auto simp add: divide_int_def)

lemma zmod_int:
  ‹int (m mod n) = int m mod int n›
  by (cases ‹m = 0›) (auto simp add: modulo_int_def)

lemma nat_div_distrib:
  ‹nat (x div y) = nat x div nat y› if ‹0 ≤ x›
  using that by (simp add: divide_int_def sgn_if)

lemma nat_div_distrib':
  ‹nat (x div y) = nat x div nat y› if ‹0 ≤ y›
  using that by (simp add: divide_int_def sgn_if)

lemma nat_mod_distrib: ― ‹Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't›
  ‹nat (x mod y) = nat x mod nat y› if ‹0 ≤ x› ‹0 ≤ y›
  using that by (simp add: modulo_int_def sgn_if)


subsubsection ‹Monotonicity in the First Argument (Dividend)›

lemma zdiv_mono1:
  ‹a div b ≤ a' div b›
    if ‹a ≤ a'› ‹0 < b›
    for a b b' :: int
proof -
  from ‹a ≤ a'› have ‹b * (a div b) + a mod b ≤ b * (a' div b) + a' mod b›
    by simp
  then have ‹b * (a div b) ≤ (a' mod b - a mod b) + b * (a' div b)›
    by (simp add: algebra_simps)
  moreover have ‹a' mod b < b + a mod b›
    by (rule less_le_trans [of _ b]) (use ‹0 < b› in simp_all)
  ultimately have ‹b * (a div b) < b * (1 + a' div b)›
    by (simp add: distrib_left)
  with ‹0 < b› have ‹a div b < 1 + a' div b›
    by (simp add: mult_less_cancel_left)
  then show ?thesis
    by simp
qed

lemma zdiv_mono1_neg:
  ‹a' div b ≤ a div b›
    if ‹a ≤ a'› ‹b < 0›
    for a a' b :: int
  using that zdiv_mono1 [of ‹- a'› ‹- a› ‹- b›] by simp


subsubsection ‹Monotonicity in the Second Argument (Divisor)›

lemma zdiv_mono2:
  ‹a div b ≤ a div b'› if ‹0 ≤ a› ‹0 < b'› ‹b' ≤ b› for a b b' :: int
proof -
  define q q' r r' where **: ‹q = a div b› ‹q' = a div b'› ‹r = a mod b› ‹r' = a mod b'›
  then have *: ‹b * q + r = b' * q' + r'› ‹0 ≤ b' * q' + r'›
    ‹r' < b'› ‹0 ≤ r› ‹0 < b'› ‹b' ≤ b›
    using that by simp_all
  have ‹0 < b' * (q' + 1)›
    using * by (simp add: distrib_left)
  with * have ‹0 ≤ q'›
    by (simp add: zero_less_mult_iff)
  moreover have ‹b * q = r' - r + b' * q'›
    using * by linarith
  ultimately have ‹b * q < b * (q' + 1)›
    using mult_right_mono * unfolding distrib_left by fastforce
  with * have ‹q ≤ q'›
    by (simp add: mult_less_cancel_left_pos)
  with ** show ?thesis
    by simp
qed

lemma zdiv_mono2_neg:
  ‹a div b' ≤ a div b› if ‹a < 0› ‹0 < b'› ‹b' ≤ b› for a b b' :: int
proof -
  define q q' r r' where **: ‹q = a div b› ‹q' = a div b'› ‹r = a mod b› ‹r' = a mod b'›
  then have *: ‹b * q + r = b' * q' + r'› ‹b' * q' + r' < 0›
    ‹r < b› ‹0 ≤ r'› ‹0 < b'› ‹b' ≤ b›
    using that by simp_all
  have ‹b' * q' < 0›
    using * by linarith
  with * have ‹q' ≤ 0›
    by (simp add: mult_less_0_iff)
  have ‹b * q' ≤ b' * q'›
    by (simp add: ‹q' ≤ 0› * mult_right_mono_neg)
  then have "b * q' < b * (q + 1)"
    using * by (simp add: distrib_left)
  then have ‹q' ≤ q›
    using * by (simp add: mult_less_cancel_left)
  then show ?thesis
    by (simp add: **)
qed


subsubsection ‹Quotients of Signs›

lemma div_eq_minus1:
  ‹0 < b ⟹ - 1 div b = - 1› for b :: int
  by (simp add: divide_int_def)

lemma zmod_minus1:
  ‹0 < b ⟹ - 1 mod b = b - 1› for b :: int
  by (auto simp add: modulo_int_def)

lemma minus_mod_int_eq:
  ‹- k mod l = l - 1 - (k - 1) mod l› if ‹l ≥ 0› for k l :: int
proof (cases ‹l = 0›)
  case True
  then show ?thesis
    by simp
next
  case False
  with that have ‹l > 0›
    by simp
  then show ?thesis
  proof (cases ‹l dvd k›)
    case True
    then obtain j where ‹k = l * j› ..
    moreover have ‹(l * j mod l - 1) mod l = l - 1›
      using ‹l > 0› by (simp add: zmod_minus1)
    then have ‹(l * j - 1) mod l = l - 1›
      by (simp only: mod_simps)
    ultimately show ?thesis
      by simp
  next
    case False
    moreover have 1: ‹0 < k mod l›
      using ‹0 < l› False le_less by fastforce
    moreover have 2: ‹k mod l < 1 + l›
      using ‹0 < l› pos_mod_bound[of l k] by linarith
    from 1 2 ‹l > 0› have ‹(k mod l - 1) mod l = k mod l - 1›
      by (simp add: zmod_trivial_iff)
    ultimately show ?thesis
      by (simp only: zmod_zminus1_eq_if)
         (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps)
  qed
qed

lemma div_neg_pos_less0:
  ‹a div b < 0› if ‹a < 0› ‹0 < b› for a b :: int
proof -
  have "a div b ≤ - 1 div b"
    using zdiv_mono1 that by auto
  also have "... ≤ -1"
    by (simp add: that(2) div_eq_minus1)
  finally show ?thesis
    by force
qed

lemma div_nonneg_neg_le0:
  ‹a div b ≤ 0› if ‹0 ≤ a› ‹b < 0› for a b :: int
  using that by (auto dest: zdiv_mono1_neg)

lemma div_nonpos_pos_le0:
  ‹a div b ≤ 0› if ‹a ≤ 0› ‹0 < b› for a b :: int
  using that by (auto dest: zdiv_mono1)

text‹Now for some equivalences of the form ‹a div b >=< 0 ⟷ …›
conditional upon the sign of ‹a› or ‹b›. There are many more.
They should all be simp rules unless that causes too much search.›

lemma pos_imp_zdiv_nonneg_iff:
  ‹0 ≤ a div b ⟷ 0 ≤ a›
  if ‹0 < b› for a b :: int
proof
  assume ‹0 ≤ a div b›
  show ‹0 ≤ a›
  proof (rule ccontr)
    assume ‹¬ 0 ≤ a›
    then have ‹a < 0›
      by simp
    then have ‹a div b < 0›
      using that by (rule div_neg_pos_less0)
    with ‹0 ≤ a div b› show False
      by simp
  qed
next
  assume "0 ≤ a"
  then have "0 div b ≤ a div b"
    using zdiv_mono1 that by blast
  then show "0 ≤ a div b"
    by auto
qed

lemma neg_imp_zdiv_nonneg_iff:
  ‹0 ≤ a div b ⟷ a ≤ 0› if ‹b < 0› for a b :: int
  using that pos_imp_zdiv_nonneg_iff [of ‹- b› ‹- a›] by simp

lemma pos_imp_zdiv_pos_iff:
  ‹0 < (i::int) div k ⟷ k ≤ i› if ‹0 < k› for i k :: int
  using that pos_imp_zdiv_nonneg_iff [of k i] zdiv_eq_0_iff [of i k] by arith

lemma pos_imp_zdiv_neg_iff:
  ‹a div b < 0 ⟷ a < 0› if ‹0 < b› for a b :: int
    ― ‹But not \<^prop>‹a div b ≤ 0 ⟷ a ≤ 0›; consider \<^prop>‹a = 1›, \<^prop>‹b = 2› when \<^prop>‹a div b = 0›.›
  using that by (simp add: pos_imp_zdiv_nonneg_iff flip: linorder_not_le)

lemma neg_imp_zdiv_neg_iff:
    ― ‹But not \<^prop>‹a div b ≤ 0 ⟷ 0 ≤ a›; consider \<^prop>‹a = - 1›, \<^prop>‹b = - 2› when \<^prop>‹a div b = 0›.›
  ‹a div b < 0 ⟷ 0 < a› if ‹b < 0› for a b :: int
  using that by (simp add: neg_imp_zdiv_nonneg_iff flip: linorder_not_le)

lemma nonneg1_imp_zdiv_pos_iff:
  ‹a div b > 0 ⟷ a ≥ b ∧ b > 0› if ‹0 ≤ a› for a b :: int
proof -
  have "0 < a div b ⟹ b ≤ a"
    using div_pos_pos_trivial[of a b] that by arith
  moreover have "0 < a div b ⟹ b > 0"
    using that div_nonneg_neg_le0[of a b] by (cases "b=0"; force)
  moreover have "b ≤ a ∧ 0 < b ⟹ 0 < a div b"
    using int_one_le_iff_zero_less[of "a div b"] zdiv_mono1[of b a b] by simp
  ultimately show ?thesis
    by blast
qed

lemma zmod_le_nonneg_dividend:
  ‹m mod k ≤ m› if ‹(m::int) ≥ 0› for m k :: int
proof -
  from that have ‹m > 0 ∨ m = 0›
    by auto
  then show ?thesis proof
    assume ‹m = 0› then show ?thesis
      by simp
  next
    assume ‹m > 0› then show ?thesis
    proof (cases k ‹0::int› rule: linorder_cases)
      case less
      moreover define l where ‹l = - k›
      ultimately have ‹l > 0›
        by simp
      with ‹m > 0› have ‹int (nat m mod nat l) ≤ m›
        by (simp flip: le_nat_iff)
      then have ‹int (nat m mod nat l) - l ≤ m›
        using ‹l > 0› by simp
      with ‹m > 0› ‹l > 0› show ?thesis
        by (simp add: modulo_int_def l_def flip: le_nat_iff)
    qed (simp_all add: modulo_int_def flip: le_nat_iff)
  qed
qed

lemma sgn_div_eq_sgn_mult:
  ‹sgn (k div l) = of_bool (k div l ≠ 0) * sgn (k * l)›
  for k l :: int
proof (cases ‹k div l = 0›)
  case True
  then show ?thesis
    by simp
next
  case False
  have ‹0 ≤ ¦k¦ div ¦l¦›
    by (cases ‹l = 0›) (simp_all add: pos_imp_zdiv_nonneg_iff)
  then have ‹¦k¦ div ¦l¦ ≠ 0 ⟷ 0 < ¦k¦ div ¦l¦›
    by (simp add: less_le)
  also have ‹… ⟷ ¦k¦ ≥ ¦l¦›
    using False nonneg1_imp_zdiv_pos_iff by auto
  finally have *: ‹¦k¦ div ¦l¦ ≠ 0 ⟷ ¦l¦ ≤ ¦k¦› .
  show ?thesis
    using ‹0 ≤ ¦k¦ div ¦l¦› 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 ‹Further properties›

lemma div_int_pos_iff:
  "k div l ≥ 0 ⟷ k = 0 ∨ l = 0 ∨ k ≥ 0 ∧ l ≥ 0
    ∨ k < 0 ∧ l < 0"
  for k l :: int
proof (cases "k = 0 ∨ l = 0")
  case False
  then have *: "k ≠ 0" "l ≠ 0"
    by auto
  then have "0 ≤ k div l ⟹ ¬ k < 0 ⟹ 0 ≤ l"
    by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq)
  then show ?thesis
   using * by (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
qed auto

lemma mod_int_pos_iff:
  ‹k mod l ≥ 0 ⟷ l dvd k ∨ l = 0 ∧ k ≥ 0 ∨ l > 0›
  for k l :: int
proof (cases "l > 0")
  case False
  then show ?thesis
    by (simp add: dvd_eq_mod_eq_0) (use neg_mod_sign [of l k] in ‹auto simp add: le_less not_less›)
qed auto

lemma abs_div:
  ‹¦x div y¦ = ¦x¦ div ¦y¦› if ‹y dvd x› for x y :: int
  using that by (cases ‹y = 0›) (auto simp add: abs_mult)

lemma int_power_div_base: ✐‹contributor ‹Matthias Daum››
  ‹k ^ m div k = k ^ (m - Suc 0)› if ‹0 < m› ‹0 < k› for k :: int
  using that by (cases m) simp_all

lemma int_div_less_self: ✐‹contributor ‹Matthias Daum››
  ‹x div k < x› if ‹0 < x› ‹1 < k› for x k :: int
proof -
  from that have ‹nat (x div k) = nat x div nat k›
    by (simp add: nat_div_distrib)
  also from that have ‹nat x div nat k < nat x›
    by simp
  finally show ?thesis
    by simp
qed


subsubsection ‹Computing ‹div› and ‹mod› by shifting›

lemma div_pos_geq:
  ‹k div l = (k - l) div l + 1› if ‹0 < l› ‹l ≤ k› for k l :: int
proof -
  have "k = (k - l) + l" by simp
  then obtain j where k: "k = j + l" ..
  with that show ?thesis by (simp add: div_add_self2)
qed

lemma mod_pos_geq:
  ‹k mod l = (k - l) mod l›  if ‹0 < l› ‹l ≤ k› for k l :: int
proof -
  have "k = (k - l) + l" by simp
  then obtain j where k: "k = j + l" ..
  with that show ?thesis by simp
qed

lemma pos_zdiv_mult_2: ‹(1 + 2 * b) div (2 * a) = b div a› (is ?Q)
  and pos_zmod_mult_2: ‹(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)› (is ?R)
  if ‹0 ≤ a› for a b :: int
proof -
  have ‹((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = (b div a, 1 + 2 * (b mod a))›
  proof (induction rule: euclidean_relation_intI)
    case by0
    then show ?case
      by simp
  next
    case divides
    have ‹2 dvd (2 * a)›
      by simp
    then have ‹2 dvd (1 + 2 * b)›
      using ‹2 * a dvd 1 + 2 * b› by (rule dvd_trans)
    then have ‹2 dvd (1 + b * 2)›
      by (simp add: ac_simps)
    then have ‹is_unit (2 :: int)›
      by simp
    then show ?case
      by simp
  next
    case euclidean_relation
    with that have ‹a > 0›
      by simp
    moreover have ‹b mod a < a›
      using ‹a > 0› by simp
    then have ‹1 + 2 * (b mod a) < 2 * a›
      by simp
    moreover have ‹2 * (b mod a) + a * (2 * (b div a)) = 2 * (b div a * a + b mod a)›
      by (simp only: algebra_simps)
    moreover have ‹0 ≤ 2 * (b mod a)›
      using ‹a > 0› by simp
    ultimately show ?case
      by (simp add: algebra_simps)
  qed
  then show ?Q and ?R
    by simp_all
qed

lemma neg_zdiv_mult_2: ‹(1 + 2 * b) div (2 * a) = (b + 1) div a› (is ?Q)
  and neg_zmod_mult_2: ‹(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1› (is ?R)
  if ‹a ≤ 0› for a b :: int
proof -
  have ‹((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = ((b + 1) div a, 2 * ((b + 1) mod a) - 1)›
  proof (induction rule: euclidean_relation_intI)
    case by0
    then show ?case
      by simp
  next
    case divides
    have ‹2 dvd (2 * a)›
      by simp
    then have ‹2 dvd (1 + 2 * b)›
      using ‹2 * a dvd 1 + 2 * b› by (rule dvd_trans)
    then have ‹2 dvd (1 + b * 2)›
      by (simp add: ac_simps)
    then have ‹is_unit (2 :: int)›
      by simp
    then show ?case
      by simp
  next
    case euclidean_relation
    with that have ‹a < 0›
      by simp
    moreover have ‹(b + 1) mod a > a›
      using ‹a < 0› by simp
    then have ‹2 * ((b + 1) mod a) > 1 + 2 * a›
      by simp
    moreover have ‹((1 + b) mod a) ≤ 0›
      using ‹a < 0› by simp
    then have ‹2 * ((1 + b) mod a) ≤ 0›
      by simp
    moreover have ‹2 * ((1 + b) mod a) + a * (2 * ((1 + b) div a)) =
      2 * ((1 + b) div a * a + (1 + b) mod a)›
      by (simp only: algebra_simps)
    ultimately show ?case
      by (simp add: algebra_simps sgn_mult abs_mult)
  qed
  then show ?Q and ?R
    by simp_all
qed

lemma zdiv_numeral_Bit0 [simp]:
  ‹numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
    numeral v div (numeral w :: int)›
  unfolding numeral.simps unfolding mult_2 [symmetric]
  by (rule div_mult_mult1) simp

lemma zdiv_numeral_Bit1 [simp]:
  ‹numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
    (numeral v div (numeral w :: int))›
  unfolding numeral.simps
  unfolding mult_2 [symmetric] add.commute [of _ 1]
  by (rule pos_zdiv_mult_2) simp

lemma zmod_numeral_Bit0 [simp]:
  ‹numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
    (2::int) * (numeral v mod numeral w)›
  unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
  unfolding mult_2 [symmetric] by (rule mod_mult_mult1)

lemma zmod_numeral_Bit1 [simp]:
  ‹numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
    2 * (numeral v mod numeral w) + (1::int)›
  unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
  unfolding mult_2 [symmetric] add.commute [of _ 1]
  by (rule pos_zmod_mult_2) simp


subsection ‹Code generation›

context
begin

qualified definition divmod_nat :: "nat ⇒ nat ⇒ nat × nat"
  where "divmod_nat m n = (m div n, m mod n)"

qualified lemma divmod_nat_if [code]:
  "divmod_nat m n = (if n = 0 ∨ m < n then (0, m) else
    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
  by (simp add: divmod_nat_def prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)

qualified lemma [code]:
  "m div n = fst (divmod_nat m n)"
  "m mod n = snd (divmod_nat m n)"
  by (simp_all add: divmod_nat_def)

end

code_identifier
  code_module Euclidean_Rings ⇀ (SML) Arith and (OCaml) Arith and (Haskell) Arith

end