# Theory Euclidean_Division

theory Euclidean_Division
imports Nat_Transfer
```(*  Title:      HOL/Euclidean_Division.thy
Author:     Manuel Eberl, TU Muenchen
Author:     Florian Haftmann, TU Muenchen
*)

section ‹Uniquely determined division in euclidean (semi)rings›

theory Euclidean_Division
imports Nat_Transfer
begin

subsection ‹Quotient and remainder in integral domains›

class semidom_modulo = algebraic_semidom + semiring_modulo
begin

lemma mod_0 [simp]: "0 mod a = 0"
using div_mult_mod_eq [of 0 a] by simp

lemma mod_by_0 [simp]: "a mod 0 = a"
using div_mult_mod_eq [of a 0] by simp

lemma mod_by_1 [simp]:
"a mod 1 = 0"
proof -
from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
then have "a + a mod 1 = a + 0" by simp
then show ?thesis by (rule add_left_imp_eq)
qed

lemma mod_self [simp]:
"a mod a = 0"
using div_mult_mod_eq [of a a] by simp

lemma dvd_imp_mod_0 [simp]:
assumes "a dvd b"
shows "b mod a = 0"
using assms minus_div_mult_eq_mod [of b a] by simp

lemma mod_0_imp_dvd:
assumes "a mod b = 0"
shows   "b dvd a"
proof -
have "b dvd ((a div b) * b)" by simp
also have "(a div b) * b = a"
using div_mult_mod_eq [of a b] by (simp add: assms)
finally show ?thesis .
qed

lemma mod_eq_0_iff_dvd:
"a mod b = 0 ⟷ b dvd a"
by (auto intro: mod_0_imp_dvd)

lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
"a dvd b ⟷ b mod a = 0"

lemma dvd_mod_iff:
assumes "c dvd b"
shows "c dvd a mod b ⟷ c dvd a"
proof -
from assms have "(c dvd a mod b) ⟷ (c dvd ((a div b) * b + a mod b))"
also have "(a div b) * b + a mod b = a"
using div_mult_mod_eq [of a b] by simp
finally show ?thesis .
qed

lemma dvd_mod_imp_dvd:
assumes "c dvd a mod b" and "c dvd b"
shows "c dvd a"
using assms dvd_mod_iff [of c b a] by simp

end

class idom_modulo = idom + semidom_modulo
begin

subclass idom_divide ..

lemma div_diff [simp]:
"c dvd a ⟹ c dvd b ⟹ (a - b) div c = a div c - b div c"

end

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

class euclidean_semiring = semidom_modulo + normalization_semidom +
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 size_mult_mono': "b ≠ 0 ⟹ euclidean_size a ≤ euclidean_size (b * a)"
by (subst mult.commute) (rule size_mult_mono)

lemma euclidean_size_normalize [simp]:
"euclidean_size (normalize a) = euclidean_size a"
proof (cases "a = 0")
case True
then show ?thesis
by simp
next
case [simp]: False
have "euclidean_size (normalize a) ≤ euclidean_size (normalize a * unit_factor a)"
by (rule size_mult_mono) simp
moreover have "euclidean_size a ≤ euclidean_size (a * (1 div unit_factor a))"
by (rule size_mult_mono) simp
ultimately show ?thesis
by simp
qed

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]) (insert assms, 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 elim!: dvdE 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

end

class euclidean_ring = idom_modulo + euclidean_semiring

subsection ‹Uniquely determined division›

class unique_euclidean_semiring = euclidean_semiring +
fixes uniqueness_constraint :: "'a ⇒ 'a ⇒ bool"
assumes size_mono_mult:
"b ≠ 0 ⟹ euclidean_size a < euclidean_size c
⟹ euclidean_size (a * b) < euclidean_size (c * b)"
-- ‹FIXME justify›
assumes uniqueness_constraint_mono_mult:
"uniqueness_constraint a b ⟹ uniqueness_constraint (a * c) (b * c)"
assumes uniqueness_constraint_mod:
"b ≠ 0 ⟹ ¬ b dvd a ⟹ uniqueness_constraint (a mod b) b"
assumes div_bounded:
"b ≠ 0 ⟹ uniqueness_constraint r b
⟹ euclidean_size r < euclidean_size b
⟹ (q * b + r) div b = q"
begin

lemma divmod_cases [case_names divides remainder by0]:
obtains
(divides) q where "b ≠ 0"
and "a div b = q"
and "a mod b = 0"
and "a = q * b"
| (remainder) q r where "b ≠ 0" and "r ≠ 0"
and "uniqueness_constraint r b"
and "euclidean_size r < euclidean_size b"
and "a div b = q"
and "a mod b = r"
and "a = q * b + r"
| (by0) "b = 0"
proof (cases "b = 0")
case True
then show thesis
by (rule by0)
next
case False
show thesis
proof (cases "b dvd a")
case True
then obtain q where "a = b * q" ..
with ‹b ≠ 0› divides
show thesis
next
case False
then have "a mod b ≠ 0"
moreover from ‹b ≠ 0› ‹¬ b dvd a› have "uniqueness_constraint (a mod b) b"
by (rule uniqueness_constraint_mod)
moreover have "euclidean_size (a mod b) < euclidean_size b"
using ‹b ≠ 0› by (rule mod_size_less)
moreover have "a = a div b * b + a mod b"
ultimately show thesis
using ‹b ≠ 0› by (blast intro: remainder)
qed
qed

lemma div_eqI:
"a div b = q" if "b ≠ 0" "uniqueness_constraint r b"
"euclidean_size r < euclidean_size b" "q * b + r = a"
proof -
from that have "(q * b + r) div b = q"
by (auto intro: div_bounded)
with that show ?thesis
by simp
qed

lemma mod_eqI:
"a mod b = r" if "b ≠ 0" "uniqueness_constraint r b"
"euclidean_size r < euclidean_size b" "q * b + r = a"
proof -
from that have "a div b = q"
by (rule div_eqI)
moreover have "a div b * b + a mod b = a"
by (fact div_mult_mod_eq)
ultimately have "a div b * b + a mod b = a div b * b + r"
using ‹q * b + r = a› by simp
then show ?thesis
by simp
qed

end

class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring

end
```