Theory 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"
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"

lemma div_mult_self4 [simp]:
assumes "b ≠ 0"
shows "(b * c + a) div b = c + a div b"

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"
also from False div_mult_self1 [of b a c] have
"… = (c + a div b) * b + (a + c * b) mod b"
finally have "a = a div b * b + (a + c * b) mod b"
then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
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"

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

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

assumes "b ≠ 0"
shows "(b + a) div b = a div b + 1"

assumes "b ≠ 0"
shows "(a + b) div b = a div b + 1"

"(b + a) mod b = a mod b"

"(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
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]

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)›
then show ?thesis using *
qed

named_theorems 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

"(a + b mod c) mod c = (a + b) mod c"

"(a mod c + b mod c) mod c = (a + b) mod c"

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"
also have "… = (f i + (∑i∈A. f i) mod a) mod a"
finally show ?case
qed simp_all

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
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"

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"
also have "… = (f i * ((∏i∈A. f i) mod a)) mod a"
finally show ?case
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
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"
with Suc show ?case
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›
then have ‹a ^ m div a ^ n = (a ^ m * 1) div (a ^ m * a ^ Suc q)›
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"
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
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]

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
next
assume ?Q
then obtain d where d: "a - b = c * d" ..
then have "a = c * d + b"
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"
then obtain d where "a - b = c * d" ..
then have "b = a + c * - d"
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›
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
next
case euclidean_relation
then have ‹¬ b dvd a›
have ‹a mod b + (b * c + b * (a div b)) = b * c + ((a div b) * b + a mod b)›
with ‹b ≠ 0› have *: ‹a mod b + (b * c + b * (a div b)) = b * c + a›
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
next
case euclidean_relation
then have ‹b ≠ 0› ‹a mod b ≠ 0›
have ‹c * (a mod b) + b * (c * (a div b)) = c * ((a div b) * b + a mod b)›
with ‹b ≠ 0› have *: ‹c * (a mod b) + b * (c * (a div b)) = c * a›
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›
then have ‹?C + ?A = a * (b mod c)›
then have ‹?B + (?C + ?A) = a * (c * (b div c) + (b mod c))›
also have ‹… = a * b›
finally show ?thesis
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
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

‹(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)›
also have ‹?A + ?D = (a mod c + b mod c) mod c + ?D›
also have ‹… = a mod c + b mod c›
finally have ‹?A + (?B + (?C + ?D)) = (a mod c + ?B) + (b mod c + ?C)›
then show ?thesis
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
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›

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"
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"
moreover from ‹n ≠ 0› have "Max {k. k * n ≤ m} < Suc (m div n)"
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
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)"
with ‹r < n› that show False
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
next
case euclidean_relation
with that show ?case
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›
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
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
)
›

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

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]

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
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

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
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"
with ‹0 < n› show ?thesis
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"
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))"

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

lemma div_eq_0_iff:
"m div n = 0 ⟷ m < n ∨ n = 0" for m n :: nat

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

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)"

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"

"(m + m) div 2 = m" for m :: nat

"(m + m) mod 2 = 0" for m :: nat

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
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)›
moreover have ‹m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)›
ultimately have ‹m mod n + n * (m div n mod q) < n * q›
by simp
then show ?case
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"
then show ?thesis
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
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
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)›
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›
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
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
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›
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"

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.›

"m div Suc (Suc (Suc n)) = m div (3 + n)"

"m mod Suc (Suc (Suc n)) = m mod (3 + n)"

"Suc (Suc (Suc m)) div n = (3 + m) div n"

"Suc (Suc (Suc m)) mod n = (3 + m) mod n"

Suc_div_eq_add3_div [of _ "numeral v"] for v

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"
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"
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 * ```