Theory Divisibility_Theory
section ‹Divisibility in commutative rings: units, associates, irreducibles, primes›
theory Divisibility_Theory
imports Ideal_Theory
begin
text ‹Elementary multiplicative divisibility theory for a commutative ring, in the locale idiom of
‹Ring_Theory›. We work directly with ring elements rather than lifting the
multiplicative monoid, which keeps the statements close to textbook divisibility.›
context commutative_ring
begin
subsection ‹Divisibility and units›
text ‹@{term "divides a b"}: ‹a› divides ‹b›, i.e.\ ‹b = a ⋅ c› for some ring element ‹c›.›
definition divides :: "'a ⇒ 'a ⇒ bool"
where "divides a b ≡ (∃c∈R. b = a ⋅ c)"
lemma dividesI [intro]: "⟦ c ∈ R; b = a ⋅ c ⟧ ⟹ divides a b"
unfolding divides_def by blast
lemma dividesE [elim]:
assumes "divides a b" obtains c where "c ∈ R" "b = a ⋅ c"
using assms unfolding divides_def by blast
lemma divides_refl [simp]: "a ∈ R ⟹ divides a a"
using Monoid.unit_closed multiplicative.Monoid_axioms by fastforce
lemma divides_trans [trans]:
assumes "divides a b" "divides b c" and a: "a ∈ R"
shows "divides a c"
using a assms divides_def by auto
lemma divides_zero [simp]: "a ∈ R ⟹ divides a 𝟬"
by (rule dividesI[of 𝟬]) simp_all
lemma one_divides [simp]: "a ∈ R ⟹ divides 𝟭 a"
by (simp add: divides_def)
lemma divides_mult_right:
assumes "b ∈ R" shows "divides a (a ⋅ b)"
using assms by blast
text ‹A unit is an invertible element of the multiplicative monoid.›
abbreviation is_unit :: "'a ⇒ bool"
where "is_unit u ≡ multiplicative.invertible u"
lemma is_unitI [intro]: "⟦ u ⋅ v = 𝟭; v ⋅ u = 𝟭; v ∈ R ⟧ ⟹ is_unit u"
by (rule multiplicative.invertibleI)
lemma unit_divides_one:
assumes "is_unit u" shows "divides u 𝟭"
using assms by auto
lemma one_divides_unit_iff:
assumes u: "u ∈ R" shows "divides u 𝟭 ⟷ is_unit u"
using is_unitI multiplicative.commutative u by blast
lemma unit_divides_all:
assumes "is_unit u" "u ∈ R" "a ∈ R" shows "divides u a"
using assms divides_trans one_divides one_divides_unit_iff by meson
subsection ‹Associated elements›
text ‹Two elements are associated if each divides the other.›
definition associated :: "'a ⇒ 'a ⇒ bool"
where "associated a b ⟷ divides a b ∧ divides b a"
lemma associatedI [intro]: "⟦ divides a b; divides b a ⟧ ⟹ associated a b"
unfolding associated_def by blast
lemma associatedD1: "associated a b ⟹ divides a b"
unfolding associated_def by blast
lemma associatedD2: "associated a b ⟹ divides b a"
unfolding associated_def by blast
lemma associated_refl [simp]: "a ∈ R ⟹ associated a a"
by (simp add: associated_def)
lemma associated_sym: "associated a b ⟹ associated b a"
unfolding associated_def by blast
lemma associated_trans [trans]:
assumes "associated a b" "associated b c" "a ∈ R" "b ∈ R" "c ∈ R"
shows "associated a c"
using assms unfolding associated_def by (meson divides_trans)
subsection ‹Greatest common divisors and least common multiples›
text ‹@{term "is_gcd d a b"}: ‹d› is a common divisor of ‹a› and ‹b› that every common divisor
divides. Gcds need not exist in a general ring, but when they do they are unique up to
association; existence is established in a principal ideal domain (Bezout) below.›
definition is_gcd :: "'a ⇒ 'a ⇒ 'a ⇒ bool"
where "is_gcd d a b ⟷
d ∈ R ∧ divides d a ∧ divides d b ∧ (∀c∈R. divides c a ∧ divides c b ⟶ divides c d)"
text ‹@{term "is_lcm m a b"}: ‹m› is a common multiple of ‹a› and ‹b› dividing every common
multiple.›
definition is_lcm :: "'a ⇒ 'a ⇒ 'a ⇒ bool"
where "is_lcm m a b ⟷
m ∈ R ∧ divides a m ∧ divides b m ∧ (∀c∈R. divides a c ∧ divides b c ⟶ divides m c)"
lemma is_gcdI:
"⟦ d ∈ R; divides d a; divides d b;
⋀c. ⟦ c ∈ R; divides c a; divides c b ⟧ ⟹ divides c d ⟧ ⟹ is_gcd d a b"
unfolding is_gcd_def by blast
lemma is_gcdD:
assumes "is_gcd d a b"
shows "d ∈ R" "divides d a" "divides d b"
and "⋀c. ⟦ c ∈ R; divides c a; divides c b ⟧ ⟹ divides c d"
using assms unfolding is_gcd_def by blast+
lemma is_gcd_sym: "is_gcd d a b ⟹ is_gcd d b a"
unfolding is_gcd_def by blast
lemma is_lcm_sym: "is_lcm m a b ⟹ is_lcm m b a"
unfolding is_lcm_def by blast
text ‹Any two gcds of the same pair are associated.›
lemma is_gcd_unique:
assumes "is_gcd d a b" and "is_gcd d' a b"
shows "associated d d'"
using assms associated_def is_gcd_def by force
text ‹Dually, any two lcms are associated.›
lemma is_lcm_unique:
assumes "is_lcm m a b" and "is_lcm m' a b"
shows "associated m m'"
using assms associated_def is_lcm_def by force
end
subsection ‹Irreducible and prime elements›
context commutative_ring
begin
text ‹An irreducible element is a nonzero non-unit whose only factorisations are trivial.›
definition irreducible_elem :: "'a ⇒ bool"
where "irreducible_elem p ⟷
p ∈ R ∧ p ≠ 𝟬 ∧ ¬ is_unit p ∧
(∀a∈R. ∀b∈R. p = a ⋅ b ⟶ is_unit a ∨ is_unit b)"
lemma irreducible_elemI:
assumes "p ∈ R" "p ≠ 𝟬" "¬ is_unit p"
and "⋀a b. ⟦ a ∈ R; b ∈ R; p = a ⋅ b ⟧ ⟹ is_unit a ∨ is_unit b"
shows "irreducible_elem p"
using assms unfolding irreducible_elem_def by blast
lemma irreducible_elemD:
assumes "irreducible_elem p"
shows "p ∈ R" "p ≠ 𝟬" "¬ is_unit p"
and "⋀a b. ⟦ a ∈ R; b ∈ R; p = a ⋅ b ⟧ ⟹ is_unit a ∨ is_unit b"
using assms unfolding irreducible_elem_def by blast+
text ‹A prime element is a nonzero non-unit that, when dividing a product, divides a factor.›
definition prime_elem :: "'a ⇒ bool"
where "prime_elem p ⟷
p ∈ R ∧ p ≠ 𝟬 ∧ ¬ is_unit p ∧
(∀a∈R. ∀b∈R. divides p (a ⋅ b) ⟶ divides p a ∨ divides p b)"
lemma prime_elemI:
assumes "p ∈ R" "p ≠ 𝟬" "¬ is_unit p"
and "⋀a b. ⟦ a ∈ R; b ∈ R; divides p (a ⋅ b) ⟧ ⟹ divides p a ∨ divides p b"
shows "prime_elem p"
using assms unfolding prime_elem_def by blast
lemma prime_elemD:
assumes "prime_elem p"
shows "p ∈ R" "p ≠ 𝟬" "¬ is_unit p"
and "⋀a b. ⟦ a ∈ R; b ∈ R; divides p (a ⋅ b) ⟧ ⟹ divides p a ∨ divides p b"
using assms unfolding prime_elem_def by blast+
end
subsection ‹In an integral domain, prime elements are irreducible›
context integral_domain
begin
text ‹Cancellation of a nonzero factor: the defining property that separates domains from general
commutative rings. From ‹c ⋅ a = c ⋅ b› with ‹c ≠ 𝟬› we get ‹c ⋅ (a - b) = 𝟬›, and absence of
zero divisors forces ‹a - b = 𝟬›.›
lemma mult_cancel_left:
assumes c: "c ∈ R" and a: "a ∈ R" and b: "b ∈ R" and cnz: "c ≠ 𝟬" and eq: "c ⋅ a = c ⋅ b"
shows "a = b"
proof -
have "c ⋅ (a - b) = c ⋅ a + c ⋅ (- b)" using c a b by (simp add: distributive)
then have "c ⋅ (a - b) = 𝟬"
by (simp add: b c eq local.right_minus)
then have "c = 𝟬 ∨ a - b = 𝟬"
using c no_zero_divisors by (simp add: a b)
then have z: "a - b = 𝟬" using cnz by blast
then show ?thesis
using a additive.commutative additive.inverse_equality b by fastforce
qed
text ‹The classical characterization of association in a domain: ‹a› and ‹b› are associated iff
they differ by a unit factor, ‹b = u ⋅ a›. (The right-to-left direction holds in any commutative
ring; the forward direction is where cancellation --- hence the domain hypothesis --- is used.)›
lemma associated_iff_unit_multiple:
assumes a: "a ∈ R" and b: "b ∈ R"
shows "associated a b ⟷ (∃u. is_unit u ∧ u ∈ R ∧ b = u ⋅ a)"
proof
assume "associated a b"
then have ab: "divides a b" and ba: "divides b a"
by (auto dest: associatedD1 associatedD2)
obtain s where s: "s ∈ R" "b = a ⋅ s" using ab by blast
obtain t where t: "t ∈ R" "a = b ⋅ t" using ba by blast
show "∃u. is_unit u ∧ u ∈ R ∧ b = u ⋅ a"
proof (cases "a = 𝟬")
case True
then show ?thesis using s a by force
next
case False
have eq1: "a ⋅ 𝟭 = a ⋅ (s ⋅ t)"
using multiplicative.associative a s t by force
have stR: "s ⋅ t ∈ R" using s t by simp
have one_st: "𝟭 = s ⋅ t"
by (rule mult_cancel_left[OF a multiplicative.unit_closed stR False eq1])
then show ?thesis using s(1)
using a is_unitI multiplicative.commutative s(2) t(1) by blast
qed
next
assume "∃u. is_unit u ∧ u ∈ R ∧ b = u ⋅ a"
then obtain u where u: "is_unit u" "u ∈ R" and beq: "b = u ⋅ a" and iuR: "multiplicative.inverse u ∈ R"
by blast
show "associated a b"
proof (rule associatedI)
show "divides a b"
using a beq multiplicative.commutative u(2) by blast
show "divides b a"
unfolding divides_def
using a b beq iuR multiplicative.commutative multiplicative.invertible_left_inverse2 u
by metis
qed
qed
lemma prime_imp_irreducible:
assumes p: "prime_elem p"
shows "irreducible_elem p"
proof (rule irreducible_elemI)
show pR: "p ∈ R" and pnz: "p ≠ 𝟬" and pnu: "¬ is_unit p"
using p by (auto dest: prime_elemD)
fix a b assume a: "a ∈ R" and b: "b ∈ R" and eq: "p = a ⋅ b"
then have "divides p a ∨ divides p b" using a b p by (auto simp: prime_elem_def)
then show "is_unit a ∨ is_unit b"
proof
assume "divides p a"
then obtain d where d: "d ∈ R" "a = p ⋅ d" by blast
have "p ⋅ 𝟭 = p ⋅ (d ⋅ b)"
using eq d a b pR by (simp add: multiplicative.associative)
then have db: "d ⋅ b = 𝟭" using mult_cancel_left[OF pR _ _ pnz] d b pR by simp
then show ?thesis
using b d(1) is_unitI multiplicative.commutative by blast
next
assume "divides p b"
then obtain d where d: "d ∈ R" "b = p ⋅ d" by blast
then have "p ⋅ 𝟭 = p ⋅ (d ⋅ a)"
using a eq multiplicative.commutative multiplicative.left_commutative pR by force
then have da: "d ⋅ a = 𝟭" using mult_cancel_left[OF pR _ _ pnz] d a pR by simp
then show ?thesis
using a d(1) is_unitI multiplicative.commutative by blast
qed
qed
end
subsection ‹Divisibility via principal ideals›
text ‹Divisibility is containment of principal ideals the other way round: ‹a› divides ‹b› iff
‹(b) ⊆ (a)› iff ‹b ∈ (a)›. This is the bridge that turns the ideal-theoretic PID argument into
statements about ring elements.›
context commutative_ring
begin
lemma divides_iff_mem_principal:
assumes a: "a ∈ R" and b: "b ∈ R"
shows "divides a b ⟷ b ∈ principal_ideal a"
using a divides_def multiplicative.commutative principal_ideal_def by auto
lemma divides_iff_principal_subset:
assumes a: "a ∈ R" and b: "b ∈ R"
shows "divides a b ⟷ principal_ideal b ⊆ principal_ideal a"
proof
assume dvd: "divides a b"
show "principal_ideal b ⊆ principal_ideal a"
proof
fix x assume "x ∈ principal_ideal b"
then obtain r c where "r ∈ R" "x = r ⋅ b" and "c ∈ R" "b = a ⋅ c"
unfolding principal_ideal_def using dvd by blast
then show "x ∈ principal_ideal a" using principal_ideal_memI[of "r ⋅ c" a]
using a multiplicative.associative multiplicative.commutative by auto
qed
next
assume "principal_ideal b ⊆ principal_ideal a"
moreover have "b ∈ principal_ideal b" using b by (simp add: principal_ideal_contains)
ultimately have "b ∈ principal_ideal a" by blast
then show "divides a b" using divides_iff_mem_principal[OF a b] by simp
qed
text ‹Associated elements generate the same principal ideal.›
lemma associated_iff_same_principal:
assumes a: "a ∈ R" and b: "b ∈ R"
shows "associated a b ⟷ principal_ideal a = principal_ideal b"
unfolding associated_def
using divides_iff_principal_subset[OF a b] divides_iff_principal_subset[OF b a] by blast
text ‹An ideal containing @{term 𝟭} is the whole ring.›
lemma ideal_contains_one_eq_whole:
assumes I: "Ideal I R (+) (⋅) 𝟬 𝟭" and one: "𝟭 ∈ I"
shows "I = R"
proof -
interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
show ?thesis using one I.additive.subset
by (metis I.Ideal(1) multiplicative.right_unit subsetI subset_antisym)
qed
text ‹A principal ideal is the whole ring exactly when its generator is a unit.›
lemma principal_ideal_eq_whole_iff_unit:
assumes a: "a ∈ R"
shows "principal_ideal a = R ⟷ is_unit a"
proof
assume "principal_ideal a = R"
then have "𝟭 ∈ principal_ideal a" by simp
then obtain r where r: "r ∈ R" "r ⋅ a = 𝟭" "a ⋅ r = 𝟭"
unfolding principal_ideal_def
using assms multiplicative.commutative by auto
then show "is_unit a"
using is_unitI by blast
next
assume u: "is_unit a"
have "𝟭 ∈ principal_ideal a"
using multiplicative.invertibleE principal_ideal_memI u by metis
then show "principal_ideal a = R"
using assms ideal_proper_iff_one_notin principal_ideal_is_ideal by blast
qed
end
subsection ‹Noetherian rings›
text ‹A (two-sided) noetherian ring is one in which every ascending chain of ideals
eventually stabilises. This is the ascending-chain formulation of noetherianity, and is the
form used by the factorisation arguments below.›
locale Noetherian_Ring = Ring +
assumes ideal_chain_stabilises:
"⟦ ⋀n. Ideal (A n) R (+) (⋅) 𝟬 𝟭; ⋀n. A n ⊆ A (Suc n) ⟧ ⟹
∃N. ∀n. N ≤ n ⟶ A n = A N"
text ‹A noetherian domain is both noetherian and an integral domain.›
locale Noetherian_Domain = Noetherian_Ring + integral_domain
subsection ‹Principal ideal domains›
text ‹A principal ideal domain (PID) is an integral domain in which every ideal is principal.›
locale principal_ideal_domain = integral_domain +
assumes principal: "Ideal I R (+) (⋅) 𝟬 𝟭 ⟹ ∃a∈R. I = principal_ideal a"
context principal_ideal_domain
begin
text ‹In a PID an irreducible element generates a maximal ideal. We use the maximality criterion of
@{locale Ideal}: any ideal ‹J› containing ‹(p)› is principal, ‹J = (q)›, so ‹q› divides ‹p›; by
irreducibility one factor is a unit, giving ‹J = (p)› or ‹J = R›.›
theorem irreducible_imp_maximal_ideal:
assumes p: "irreducible_elem p"
shows "Ideal.maximal_ideal (principal_ideal p) R (+) (⋅) 𝟬 𝟭"
proof -
have pR: "p ∈ R" and pnu: "¬ is_unit p" using p by (auto dest: irreducible_elemD)
interpret P: Ideal "principal_ideal p" R "(+)" "(⋅)" 𝟬 𝟭
by (rule principal_ideal_is_ideal[OF pR])
show ?thesis
unfolding P.maximal_ideal_def
proof (intro conjI allI impI)
show "principal_ideal p ≠ R" using principal_ideal_eq_whole_iff_unit[OF pR] pnu by blast
next
fix J assume J: "Ideal J R (+) (⋅) 𝟬 𝟭" and sub: "principal_ideal p ⊆ J"
obtain q where q: "q ∈ R" "J = principal_ideal q" using principal[OF J] by blast
have "principal_ideal p ⊆ principal_ideal q" using sub q by simp
then have "divides q p" using divides_iff_principal_subset[OF q(1) pR] by simp
then obtain r where r: "r ∈ R" "p = q ⋅ r" by blast
have "is_unit q ∨ is_unit r" using p q(1) r by (auto dest: irreducible_elemD)
then show "J = principal_ideal p ∨ J = R"
proof
assume "is_unit q"
then show ?thesis using principal_ideal_eq_whole_iff_unit q by blast
next
assume ur: "is_unit r"
have "p ⋅ multiplicative.inverse r = q"
by (simp add: multiplicative.associative q(1) r ur)
then have "divides p q"
using r(1) ur by auto
then show ?thesis using q(2)
using divides_iff_principal_subset pR q(1) sub by blast
qed
qed
qed
text ‹Hence in a PID every irreducible element is prime (the converse of
@{thm integral_domain.prime_imp_irreducible}).›
theorem irreducible_imp_prime:
assumes p: "irreducible_elem p"
shows "prime_elem p"
proof -
have pR: "p ∈ R" and pnz: "p ≠ 𝟬" and pnu: "¬ is_unit p"
using p by (auto dest: irreducible_elemD)
interpret P: ideal_in_comm_ring "principal_ideal p" R "(+)" "(⋅)" 𝟬 𝟭
by (intro ideal_in_comm_ring.intro principal_ideal_is_ideal[OF pR] commutative_ring_axioms)
have prime: "P.prime_ideal"
using P.maximal_imp_prime_ideal irreducible_imp_maximal_ideal p by blast
show ?thesis
using P.prime_ideal_def divides_iff_mem_principal pR pnu pnz prime prime_elemI by auto
qed
subsubsection ‹The ascending chain condition on principal ideals›
text ‹The union of a countable ascending chain of ideals is an ideal.›
lemma Union_chain_ideal:
assumes I: "⋀n. Ideal (A n) R (+) (⋅) 𝟬 𝟭"
and mono: "⋀n. A n ⊆ A (Suc n)"
shows "Ideal (⋃n. A n) R (+) (⋅) 𝟬 𝟭"
proof -
have mono_le: "A m ⊆ A n" if "m ≤ n" for m n
using that by (induct n) (simp_all add: lift_Suc_mono_le mono)
have dir: "⋀x y. x ∈ (⋃n. A n) ⟹ y ∈ (⋃n. A n) ⟹ ∃k. x ∈ A k ∧ y ∈ A k"
using mono mono_le by (metis UN_E not_less_eq_eq subset_eq)
interpret A0: Ideal "A 0" R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
have sub: "Subgroup (⋃n. A n) R (+) 𝟬"
proof (rule additive.subgroupI)
show "(⋃n. A n) ⊆ R"
proof
fix x assume "x ∈ (⋃n. A n)"
then obtain n where "x ∈ A n" by blast
interpret An: Ideal "A n" R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
show "x ∈ R" using ‹x ∈ A n› An.additive.subset by blast
qed
next
show "𝟬 ∈ (⋃n. A n)" using A0.additive.sub_unit_closed by blast
next
fix g h assume "g ∈ (⋃n. A n)" "h ∈ (⋃n. A n)"
then obtain k where gh: "g ∈ A k" "h ∈ A k" using dir by blast
interpret Ak: Ideal "A k" R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
show "g + h ∈ (⋃n. A n)" using gh Ak.additive.sub_composition_closed by blast
next
fix g assume "g ∈ (⋃n. A n)"
then obtain n where "g ∈ A n" by blast
interpret An: Ideal "A n" R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
show "additive.invertible g" using ‹g ∈ A n› An.additive.subset by auto
show "additive.inverse g ∈ (⋃n. A n)"
using ‹g ∈ A n› An.additive.submonoid_inverse_closed An.additive.sub.invertible by blast
qed
interpret U: Subgroup "⋃n. A n" R "(+)" 𝟬 by (rule sub)
show ?thesis
proof
fix a x assume a: "a ∈ R" and x: "x ∈ (⋃n. A n)"
obtain n where "x ∈ A n" using x by blast
interpret An: Ideal "A n" R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
show "a ⋅ x ∈ (⋃n. A n)" "x ⋅ a ∈ (⋃n. A n)"
using a ‹x ∈ A n› An.Ideal by blast+
qed
qed
text ‹∗‹Ascending chain condition›: every ascending chain of (principal) ideals in a PID
stabilises. Proof: the union is an ideal, hence principal ‹= (c)›; the generator ‹c› lies in
some ‹A N›, and from there on the chain cannot grow beyond ‹A N›.›
theorem ascending_chain_stabilises:
assumes I: "⋀n. Ideal (A n) R (+) (⋅) 𝟬 𝟭"
and mono: "⋀n. A n ⊆ A (Suc n)"
obtains N where "⋀n. N ≤ n ⟹ A n = A N"
proof -
have mono_le: "A m ⊆ A n" if "m ≤ n" for m n
using that
by (induct n) (simp_all add: lift_Suc_mono_le mono)
have Uideal: "Ideal (⋃n. A n) R (+) (⋅) 𝟬 𝟭"
using I mono by (rule Union_chain_ideal)
obtain c where c: "c ∈ R" and Uc: "(⋃n. A n) = principal_ideal c"
using principal[OF Union_chain_ideal] I mono by metis
with principal_ideal_contains obtain N where cN: "c ∈ A N"
by fastforce
have "A n = A N" if "N ≤ n" for n
proof
show "A N ⊆ A n" using mono_le that .
show "A n ⊆ A N"
proof
fix x assume "x ∈ A n"
then have "x ∈ principal_ideal c" using Uc by blast
then obtain r where r: "r ∈ R" "x = r ⋅ c" unfolding principal_ideal_def by blast
interpret AN: Ideal "A N" R "(+)" "(⋅)" 𝟬 𝟭
by (rule I)
show "x ∈ A N" using r cN AN.Ideal(1) by blast
qed
qed
then show ?thesis using that by blast
qed
subsubsection ‹Bezout: existence of greatest common divisors›
text ‹The ideal generated by two elements, ‹(a, b) = {x ⋅ a + y ⋅ b}›.›
definition bezout_ideal :: "'a ⇒ 'a ⇒ 'a set"
where "bezout_ideal a b ≡ {x ⋅ a + y ⋅ b | x y. x ∈ R ∧ y ∈ R}"
lemma bezout_ideal_memI:
"⟦ x ∈ R; y ∈ R ⟧ ⟹ x ⋅ a + y ⋅ b ∈ bezout_ideal a b"
unfolding bezout_ideal_def by blast
lemma bezout_ideal_is_ideal:
assumes a: "a ∈ R" and b: "b ∈ R"
shows "Ideal (bezout_ideal a b) R (+) (⋅) 𝟬 𝟭"
proof -
have sg: "Subgroup (bezout_ideal a b) R (+) 𝟬"
proof (rule additive.subgroupI)
show "bezout_ideal a b ⊆ R"
using a b principal_ideal_domain.bezout_ideal_def principal_ideal_domain_axioms by fastforce
show "𝟬 ∈ bezout_ideal a b" using a b
using additive.left_unit additive.unit_closed bezout_ideal_memI left_zero by metis
next
fix g h assume "g ∈ bezout_ideal a b" "h ∈ bezout_ideal a b"
then obtain x1 y1 x2 y2 where
g: "x1 ∈ R" "y1 ∈ R" "g = x1 ⋅ a + y1 ⋅ b" and h: "x2 ∈ R" "y2 ∈ R" "h = x2 ⋅ a + y2 ⋅ b"
unfolding bezout_ideal_def by blast
have "g + h = (x1 + x2) ⋅ a + (y1 + y2) ⋅ b"
by (simp add: a additive.commutative additive.left_commutative b distributive(2) g h)
then show "g + h ∈ bezout_ideal a b"
using g h bezout_ideal_memI[of "x1+x2" "y1+y2" a b] by simp
next
fix g assume "g ∈ bezout_ideal a b"
then obtain x y where xy: "x ∈ R" "y ∈ R" "g = x ⋅ a + y ⋅ b"
unfolding bezout_ideal_def by blast
show "additive.invertible g"
using xy a b by simp
show "additive.inverse g ∈ bezout_ideal a b"
using xy a b bezout_ideal_memI[of "- x" "- y" a b]
by (simp add: left_minus additive.inverse_composition_commute additive.commutative)
qed
interpret S: Subgroup "bezout_ideal a b" R "(+)" 𝟬 by (rule sg)
show ?thesis
proof
fix r z assume r: "r ∈ R" and "z ∈ bezout_ideal a b"
then obtain x y where z: "x ∈ R" "y ∈ R" "z = x ⋅ a + y ⋅ b"
unfolding bezout_ideal_def by blast
have "r ⋅ z = (r ⋅ x) ⋅ a + (r ⋅ y) ⋅ b"
using r z a b by (simp add: distributive multiplicative.associative)
then show "r ⋅ z ∈ bezout_ideal a b"
using r z bezout_ideal_memI[of "r ⋅ x" "r ⋅ y" a b] by simp
then show "z ⋅ r ∈ bezout_ideal a b"
using r z a b by (simp add: multiplicative.commutative)
qed
qed
text ‹@{term a} and @{term b} both lie in ‹(a, b)›.›
lemma a_in_bezout_ideal: "⟦ a ∈ R; b ∈ R ⟧ ⟹ a ∈ bezout_ideal a b"
using bezout_ideal_memI[of 𝟭 𝟬 a b] by simp
lemma b_in_bezout_ideal: "⟦ a ∈ R; b ∈ R ⟧ ⟹ b ∈ bezout_ideal a b"
using bezout_ideal_memI[of 𝟬 𝟭 a b] by simp
text ‹∗‹Bezout's theorem.› The gcd generates the ideal ‹(a, b)›: divisibility of ‹a› and ‹b›
is membership, and any common divisor divides every element of ‹(a, b)›, in particular ‹d›.›
theorem bezout:
assumes a: "a ∈ R" and b: "b ∈ R"
obtains d x y where "is_gcd d a b" "x ∈ R" "y ∈ R" "d = x ⋅ a + y ⋅ b"
proof -
have I: "Ideal (bezout_ideal a b) R (+) (⋅) 𝟬 𝟭" by (rule bezout_ideal_is_ideal[OF a b])
obtain d where d: "d ∈ R" and gen: "bezout_ideal a b = principal_ideal d"
using principal[OF I] by blast
have "d ∈ bezout_ideal a b" using gen d by (simp add: principal_ideal_contains)
then obtain x y where xy: "x ∈ R" "y ∈ R" "d = x ⋅ a + y ⋅ b"
unfolding bezout_ideal_def by blast
obtain dda: "divides d a" and ddb: "divides d b"
using a_in_bezout_ideal b_in_bezout_ideal gen divides_iff_mem_principal[OF d] a b by metis
have "is_gcd d a b"
proof (rule is_gcdI[OF d dda ddb])
fix c assume c: "c ∈ R" and ca: "divides c a" and cb: "divides c b"
obtain s t where s: "s ∈ R" "a = c ⋅ s" and t: "t ∈ R" "b = c ⋅ t" using ca cb by blast
then have "d = c ⋅ (x ⋅ s + y ⋅ t)"
by (simp add: c distributive(1) multiplicative.left_commutative xy)
moreover have "x ⋅ s + y ⋅ t ∈ R" using xy s t by simp
ultimately show "divides c d" by (blast intro: dividesI)
qed
then show ?thesis using xy that by blast
qed
text ‹Consequently a greatest common divisor exists for every pair.›
corollary gcd_exists:
assumes "a ∈ R" "b ∈ R" shows "∃d. is_gcd d a b"
using bezout[OF assms] by blast
end
text ‹Principal ideal domains satisfy the noetherian ascending-chain condition.›
sublocale principal_ideal_domain ⊆ Noetherian_Domain
proof unfold_locales
fix A
assume I: "⋀n. Ideal (A n) R (+) (⋅) 𝟬 𝟭"
and mono: "⋀n. A n ⊆ A (Suc n)"
show "∃N. ∀n. N ≤ n ⟶ A n = A N"
using I ascending_chain_stabilises mono by meson
qed
subsection ‹Euclidean domains›
text ‹A Euclidean domain is an integral domain equipped with a degree function ‹φ› into the naturals
admitting division with remainder: for ‹a, b› nonzero there are ‹q, r› with ‹a = b ⋅ q + r› and
either ‹r = 𝟬› or ‹φ r < φ b›.›
locale Euclidean_Domain = integral_domain +
fixes φ :: "'a ⇒ nat"
assumes euclidean_division:
"⟦ a ∈ R; b ∈ R; a ≠ 𝟬; b ≠ 𝟬 ⟧ ⟹
∃q∈R. ∃r∈R. a = b ⋅ q + r ∧ (r = 𝟬 ∨ φ r < φ b)"
begin
text ‹Every Euclidean domain is a principal ideal domain: an ideal is generated by any nonzero
element of least ‹φ›-value, since division with remainder against it lands back in the ideal and
minimality forces a zero remainder.›
sublocale principal_ideal_domain
proof unfold_locales
fix I assume I: "Ideal I R (+) (⋅) 𝟬 𝟭"
interpret I: Ideal I R "(+)" "(⋅)" 𝟬 𝟭 by (rule I)
show "∃a∈R. I = principal_ideal a"
proof (cases "I = {𝟬}")
case True
have "principal_ideal 𝟬 = {𝟬}"
using principal_ideal_memI[of 𝟬 𝟬] by (force simp: principal_ideal_def)
then show ?thesis using True by auto
next
case False
define Inz where "Inz ≡ {x ∈ I. x ≠ 𝟬}"
have ne: "Inz ≠ {}" using False I.additive.sub_unit_closed Inz_def by blast
define φimg where "φimg ≡ φ ` Inz"
have "φimg ≠ {}" using ne φimg_def by simp
then obtain a where a: "a ∈ Inz" and amin: "⋀b. b ∈ Inz ⟹ φ a ≤ φ b"
using exists_least_iff[of "λn. n ∈ φimg"] unfolding φimg_def image_def mem_Collect_eq
by (metis ne all_not_in_conv linorder_not_le)
have aI: "a ∈ I" using a Inz_def by blast
have aR: "a ∈ R" using aI I.additive.subset by blast
have anz: "a ≠ 𝟬" using a Inz_def by blast
have "I = principal_ideal a"
proof
show "principal_ideal a ⊆ I"
using I.Ideal(1) aI principal_ideal_def by auto
next
show "I ⊆ principal_ideal a"
proof
fix b assume bI: "b ∈ I"
have bR: "b ∈ R" using bI I.additive.subset by blast
show "b ∈ principal_ideal a"
proof (cases "b = 𝟬")
case True then show ?thesis using principal_ideal_memI[of 𝟬 a] aR by simp
next
case bnz: False
obtain q r where q: "q ∈ R" and rR: "r ∈ R" and beq: "b = a ⋅ q + r"
and rem: "r = 𝟬 ∨ φ r < φ a"
using euclidean_division[OF bR aR bnz anz] by blast
have aqI: "a ⋅ q ∈ I" using I.Ideal(2)[OF q aI] .
then have req: "r = b - a ⋅ q"
using I.additive.sub additive.commutative additive.commute_iff_inverse beq rR by metis
have "- (a ⋅ q) ∈ I" using aqI by simp
then have "b + (- (a ⋅ q)) ∈ I"
using bI I.additive.sub_composition_closed by blast
then have rI: "r ∈ I" using req by simp
have "r = 𝟬"
using rI rem Inz_def amin linorder_not_less by blast
then show ?thesis using q principal_ideal_memI[of q a]
using aR beq multiplicative.commutative by auto
qed
qed
qed
then show ?thesis using aR by blast
qed
qed
end
text ‹A field is a Euclidean domain with the constant degree function (division with remainder is
exact: ‹a = b ⋅ (b¯ ⋅ a) + 𝟬›).›
sublocale Field ⊆ Euclidean_Domain R "(+)" "(⋅)" 𝟬 𝟭 "λ_. 0"
proof
fix a b assume a: "a ∈ R" and b: "b ∈ R" and bnz: "b ≠ 𝟬"
have "a = b ⋅ (multiplicative.inverse b ⋅ a) + 𝟬"
by (simp add: a b bnz field_inverse multiplicative.invertible_right_inverse2)
then show "∃q∈R. ∃r∈R. a = b ⋅ q + r ∧ (r = 𝟬 ∨ (0::nat) < 0)"
using a b bnz field_inverse by auto
qed
subsection ‹Factorizations into irreducibles›
text ‹The product of a list of ring elements.›
context commutative_ring
begin
definition list_prod :: "'a list ⇒ 'a"
where "list_prod xs = foldr (⋅) xs 𝟭"
lemma list_prod_Nil [simp]: "list_prod [] = 𝟭"
by (simp add: list_prod_def)
lemma list_prod_Cons [simp]: "list_prod (x # xs) = x ⋅ list_prod xs"
by (simp add: list_prod_def)
lemma list_prod_closed [intro, simp]:
"set xs ⊆ R ⟹ list_prod xs ∈ R"
by (induct xs) auto
text ‹A factorization of ‹a› is a list of irreducible ring elements whose product is ‹a›.›
definition factorization :: "'a list ⇒ 'a ⇒ bool"
where "factorization fs a ≡ (∀p∈set fs. irreducible_elem p) ∧ list_prod fs = a"
lemma factorizationI:
"⟦ ⋀p. p ∈ set fs ⟹ irreducible_elem p; list_prod fs = a ⟧ ⟹ factorization fs a"
unfolding factorization_def by blast
lemma factorization_irreducible: "⟦ factorization fs a; p ∈ set fs ⟧ ⟹ irreducible_elem p"
unfolding factorization_def by blast
lemma factorization_prod: "factorization fs a ⟹ list_prod fs = a"
unfolding factorization_def by blast
lemma factorization_set_R: "factorization fs a ⟹ set fs ⊆ R"
unfolding factorization_def using irreducible_elemD(1) by blast
lemma list_prod_append [simp]:
assumes "set xs ⊆ R" "set ys ⊆ R"
shows "list_prod (xs @ ys) = list_prod xs ⋅ list_prod ys"
using assms
by (induct xs) (simp_all add: multiplicative.associative)
text ‹An irreducible element has the one-item factorization ‹[p]›.›
lemma factorization_single: "irreducible_elem p ⟹ factorization [p] p"
by (simp add: factorization_def irreducible_elemD)
text ‹Concatenating factorizations multiplies the factored elements.›
lemma factorization_append:
assumes "factorization fs a" "factorization gs b"
shows "factorization (fs @ gs) (a ⋅ b)"
using assms factorization_def factorization_set_R by auto
end
subsection ‹Uniqueness of factorization›
context integral_domain
begin
text ‹A prime element dividing a list-product divides one of the factors.›
lemma prime_divides_list_prod:
assumes p: "prime_elem p" and fs: "set fs ⊆ R" and dvd: "divides p (list_prod fs)"
shows "∃f∈set fs. divides p f"
using fs dvd
proof (induct fs)
case Nil with one_divides_unit_iff p prime_elem_def show ?case
by force
next
case (Cons f fs)
then have "divides p f ∨ divides p (list_prod fs)"
using p prime_elem_def by auto
then show ?case
using Cons by force
qed
text ‹If an irreducible ‹q› divides an irreducible ‹p› then they are associated.›
lemma irreducible_dvd_irreducible_assoc:
assumes q: "irreducible_elem q" and p: "irreducible_elem p" and dvd: "divides q p"
shows "associated q p"
proof -
have qR: "q ∈ R" and pR: "p ∈ R" using q p by (auto dest: irreducible_elemD)
obtain c where c: "c ∈ R" "p = q ⋅ c" using dvd by blast
have "is_unit q ∨ is_unit c" using irreducible_elemD(4)[OF p qR c(1) c(2)] .
then have cu: "is_unit c" using irreducible_elemD(3)[OF q] by blast
have "divides p q"
using associated_iff_unit_multiple c cu local.associatedD2 multiplicative.commutative pR qR
by metis
then show ?thesis using dvd
by blast
qed
text ‹Cancellation for association: a common nonzero factor may be dropped.›
lemma associated_cancel:
assumes c: "c ∈ R" and x: "x ∈ R" and y: "y ∈ R" and cnz: "c ≠ 𝟬"
and as: "associated (c ⋅ x) (c ⋅ y)"
shows "associated x y"
proof (rule associatedI)
have d1: "divides (c ⋅ x) (c ⋅ y)" and d2: "divides (c ⋅ y) (c ⋅ x)"
using as by (auto dest: associatedD1 associatedD2)
show "divides x y"
proof -
obtain d where d: "d ∈ R" "c ⋅ y = (c ⋅ x) ⋅ d" using d1 by blast
then have "y = x ⋅ d"
using mult_cancel_left[OF c y _ cnz] x d c by auto
then show ?thesis using d by blast
qed
show "divides y x"
proof -
obtain d where d: "d ∈ R" "c ⋅ x = (c ⋅ y) ⋅ d" using d2 by blast
then show ?thesis using d
using ‹divides x y› c cnz divides_def local.mult_cancel_left multiplicative.associative
multiplicative.composition_closed x by metis
qed
qed
text ‹Multiplying by a unit yields an associate.›
lemma associated_unit_mult:
assumes u: "is_unit u" "u ∈ R" and b: "b ∈ R"
shows "associated (u ⋅ b) b"
proof (rule associatedI)
show "divides (u ⋅ b) b"
using associated_iff_unit_multiple b local.associatedD2 u by blast
show "divides b (u ⋅ b)" using u b by (metis dividesI multiplicative.commutative)
qed
text ‹Product of a list is unchanged by removing then re-multiplying a member (commutativity).›
lemma list_prod_remove1:
assumes "set gs ⊆ R" and "g ∈ set gs"
shows "list_prod gs = g ⋅ list_prod (remove1 g gs)"
using assms
proof (induct gs)
case (Cons h hs)
have hR: "h ∈ R" and hsR: "set hs ⊆ R" using Cons.prems(1) by auto
show ?case
proof (cases "g = h")
case False
have tR: "list_prod (remove1 g hs) ∈ R"
using hsR set_remove1_subset by fastforce
have "list_prod (h # hs) = h ⋅ (g ⋅ list_prod (remove1 g hs))"
using Cons.hyps Cons.prems(2) False hsR by force
also have "… = g ⋅ list_prod (h # remove1 g hs)"
using Cons.prems tR by (auto simp: mult_ac)
also have "h # remove1 g hs = remove1 g (h # hs)" using False by simp
finally show ?thesis .
qed auto
qed auto
text ‹∗‹Uniqueness of factorization› (length form): any two prime factorizations of associated
products have the same number of factors. This is the well-definedness of the number of
irreducible factors --- the core uniqueness statement of unique factorization.›
theorem prime_factorization_length_unique:
assumes "⋀f. f ∈ set fs ⟹ prime_elem f" and "⋀g. g ∈ set gs ⟹ prime_elem g"
and "associated (list_prod fs) (list_prod gs)"
shows "length fs = length gs"
using assms
proof (induct fs arbitrary: gs)
case Nil
have "associated 𝟭 (list_prod gs)" using Nil.prems(3) by simp
then have 1: "divides (list_prod gs) 𝟭" by (auto dest: associatedD2)
have "gs = []"
proof (rule ccontr)
assume "gs ≠ []"
then obtain g gs' where gs: "gs = g # gs'" using list.exhaust by blast
have gp: "prime_elem g" using Nil.prems(2) gs by simp
have gR: "g ∈ R" and gsR: "set gs' ⊆ R"
using gp gs Nil.prems(2) by (auto dest: prime_elemD(1))
have "divides g (list_prod gs)" using gs gR gsR by (auto intro: dividesI)
then show False using prime_elemD(3)[OF gp]
using 1 divides_trans gR one_divides_unit_iff by blast
qed
then show ?case by simp
next
case (Cons f fs')
have fp: "prime_elem f" using Cons.prems(1) by simp
then have fR: "f ∈ R" and fnz: "f ≠ 𝟬" by (auto dest: prime_elemD)
have fs'p: "⋀x. x ∈ set fs' ⟹ prime_elem x" using Cons.prems(1) by simp
have fsR: "set fs' ⊆ R" using fs'p prime_elemD(1) by blast
have gsR: "set gs ⊆ R" using Cons.prems(2) prime_elemD(1) by blast
have "divides f (list_prod (f # fs'))" using fR fsR by (auto intro: dividesI)
then have "divides f (list_prod gs)"
using Cons.prems(3) fR list_prod_closed[OF gsR] by (meson associatedD1 divides_trans)
then obtain g where g: "g ∈ set gs" and fg: "divides f g"
using Cons.prems(1) prime_divides_list_prod[OF _ gsR] by auto
have gp: "prime_elem g" using Cons.prems(2) g by simp
have gR: "g ∈ R" and gnz: "g ≠ 𝟬" using gp by (auto dest: prime_elemD)
have assoc_fg: "associated f g"
by (simp add: Cons.prems(1) fg gp irreducible_dvd_irreducible_assoc prime_imp_irreducible)
define rest where "rest ≡ remove1 g gs"
have restR: "set rest ⊆ R"
using gsR rest_def by force
have restp: "⋀x. x ∈ set rest ⟹ prime_elem x"
unfolding rest_def using Cons.prems(2) set_remove1_subset by (meson subset_iff)
have gs_split: "list_prod gs = g ⋅ list_prod rest"
using list_prod_remove1[OF gsR g] rest_def by simp
obtain u where u: "u ∈ R" "g = f ⋅ u"
using assoc_fg by (auto dest: associatedD1)
then have uu: "is_unit u"
using fp gp irreducible_elem_def prime_imp_irreducible by metis
have "associated (f ⋅ list_prod fs') (g ⋅ list_prod rest)"
using Cons.prems(3) gs_split by simp
then have "associated (f ⋅ list_prod fs') (f ⋅ (u ⋅ list_prod rest))"
using u by (simp add: multiplicative.associative fR u(1) restR)
then have "associated (list_prod fs') (u ⋅ list_prod rest)"
using associated_cancel[OF fR list_prod_closed[OF fsR]] fnz u(1) restR by simp
moreover have "associated (u ⋅ list_prod rest) (list_prod rest)"
using associated_unit_mult[OF uu u(1) list_prod_closed[OF restR]] .
ultimately have "associated (list_prod fs') (list_prod rest)"
using fsR restR u(1) associated_trans by (meson associated_def divides_trans list_prod_closed)
then have eqlen: "length fs' = length rest" using Cons.hyps[OF fs'p restp] by simp
have "0 < length gs" using g by (cases gs) auto
then show ?case using eqlen
using g rest_def by (simp add: length_remove1)
qed
end
subsection ‹Factorial domains (unique factorization domains)›
context principal_ideal_domain
begin
subsubsection ‹Existence of factorizations›
text ‹Every nonzero non-unit of a PID admits a factorization into irreducibles. If not, the
set of ``bad'' elements (nonzero non-units without a factorization) is nonempty; a bad element
is not irreducible, so it factors into two non-units, at least one of which is bad and is a
∗‹proper› divisor. Iterating (dependent choice) yields a strictly ascending chain of principal
ideals, contradicting the ascending chain condition.›
theorem factorization_exists:
assumes a: "a ∈ R" and anz: "a ≠ 𝟬" and anu: "¬ is_unit a"
shows "∃fs. factorization fs a"
proof (rule ccontr)
define bad where "bad x ≡ x ∈ R ∧ x ≠ 𝟬 ∧ ¬ is_unit x ∧ ¬ (∃fs. factorization fs x)" for x
assume non: "¬ (∃fs. factorization fs a)"
then have bad_a: "bad a" using assms bad_def by simp
have step: "∃y. bad y ∧ divides y x ∧ ¬ divides x y" if bx: "bad x" for x
proof -
have xR: "x ∈ R" and xnz: "x ≠ 𝟬" and xnu: "¬ is_unit x"
and xnf: "¬ (∃fs. factorization fs x)" using bx bad_def by auto
have "¬ irreducible_elem x" using xnf factorization_single by blast
then obtain p q where pq: "p ∈ R" "q ∈ R" "x = p ⋅ q" "¬ is_unit p" "¬ is_unit q"
using irreducible_elemI[OF xR xnz xnu] by blast
have pnz: "p ≠ 𝟬" and qnz: "q ≠ 𝟬" using pq(3) xnz pq(1,2) by auto
have "¬ (∃fs. factorization fs p) ∨ ¬ (∃fs. factorization fs q)"
using factorization_append pq(3) xnf by blast
then show ?thesis
proof
assume npf: "¬ (∃fs. factorization fs p)"
have "bad p" using pq(1) pnz pq(4) npf bad_def by simp
moreover have "¬ divides x p"
proof
assume "divides x p"
then obtain d where d: "d ∈ R" "p = x ⋅ d" by blast
then have "x ⋅ 𝟭 = x ⋅ (q ⋅ d)"
using d multiplicative.associative multiplicative.commutative pq(2,3) xR by force
then have qd: "q ⋅ d = 𝟭" using mult_cancel_left[OF xR _ _ xnz] pq(2) d by simp
have "d ⋅ q = 𝟭" using qd pq(2) d(1) by (simp add: multiplicative.commutative)
then show False
using d is_unitI pq(5) qd by blast
qed
ultimately show ?thesis using pq by blast
next
assume nqf: "¬ (∃fs. factorization fs q)"
have "bad q" using pq(2) qnz pq(5) nqf bad_def by simp
moreover have "divides q x"
using multiplicative.commutative pq by blast
moreover have "¬ divides x q"
proof
assume "divides x q"
then obtain d where d: "d ∈ R" "q = x ⋅ d" by blast
then have "x ⋅ 𝟭 = x ⋅ (p ⋅ d)"
using multiplicative.left_commutative pq xR by auto
then have pd: "p ⋅ d = 𝟭" using mult_cancel_left[OF xR _ _ xnz] pq(1) d by simp
have "d ⋅ p = 𝟭" using pd pq(1) d(1) by (simp add: multiplicative.commutative)
then show False
using d(1) is_unitI pd pq(4) by presburger
qed
ultimately show ?thesis by blast
qed
qed
have "∃f. ∀n. bad (f n) ∧ (divides (f (Suc n)) (f n) ∧ ¬ divides (f n) (f (Suc n)))"
by (rule dependent_nat_choice) (use bad_a step in blast)+
then obtain f where fbad: "⋀n. bad (f n)"
and fdvd: "⋀n. divides (f (Suc n)) (f n)" and fndvd: "⋀n. ¬ divides (f n) (f (Suc n))"
by blast
have fR: "⋀n. f n ∈ R" using fbad bad_def by simp
define A where "A n ≡ principal_ideal (f n)" for n
have "⋀n. A n ⊆ A (Suc n)"
using A_def fdvd divides_iff_principal_subset[OF fR fR] by simp
then obtain N where stab: "⋀n. N ≤ n ⟹ A n = A N"
using A_def principal_ideal_is_ideal[OF fR] ideal_chain_stabilises by force
have "A (Suc N) = A N" using stab[of "Suc N"] by simp
then show False using fndvd
unfolding A_def using divides_iff_mem_principal fR principal_ideal_contains by metis
qed
end
text ‹A factorial domain (UFD) is an integral domain in which every nonzero non-unit factors into
irreducibles, uniquely up to the number of factors (and, via
@{thm integral_domain.prime_factorization_length_unique}, up to associates and order once the
factors are prime).›
locale Factorial_Domain = integral_domain +
assumes factors_exist: "⟦ a ∈ R; a ≠ 𝟬; ¬ is_unit a ⟧ ⟹ ∃fs. factorization fs a"
text ‹Every principal ideal domain is a factorial domain: existence of factorizations is
@{thm principal_ideal_domain.factorization_exists}, established via the ascending chain condition.›
sublocale principal_ideal_domain ⊆ Factorial_Domain
by unfold_locales (rule factorization_exists)
subsection ‹Euclidean type classes as locale Euclidean domains; the integers›
text ‹Isabelle's type class @{class euclidean_ring} (an @{class idom} with a @{const euclidean_size}
and division with remainder) is exactly the type-class analogue of our locale
@{locale Euclidean_Domain}. The ring of integers ‹ℤ› is the primary instance.›
text ‹Restore HOL arithmetic notation locally (‹Ring_Theory› suppresses it).›
notation plus (infixl ‹+› 65)
notation minus (infixl ‹-› 65)
unbundle uminus_syntax
subsection ‹The general type-class bridge›
text ‹The division-with-remainder axiom of @{locale Euclidean_Domain} is witnessed by ‹q = a div b›,
‹r = a mod b›: the identity @{thm mult_div_mod_eq} gives ‹a = b ⋅ q + r›, and @{thm mod_size_less}
bounds the remainder's size. (The class's extra axioms --- @{thm size_0}, @{thm size_mult_mono}
--- exceed what the locale requires, so this is a one-directional bridge, which is all we need.)›
lemma euclidean_domain_TC:
"Euclidean_Domain (UNIV :: 'a :: euclidean_ring set) (+) (*) 0 1 euclidean_size"
proof (rule Euclidean_Domain.intro)
show "integral_domain (UNIV :: 'a set) (+) (*) 0 1" by (rule idom_TC)
next
show "Euclidean_Domain_axioms (UNIV :: 'a set) (+) (*) 0 euclidean_size"
proof
fix a b :: 'a assume "a ∈ UNIV" "b ∈ UNIV" "a ≠ 0" and bnz: "b ≠ 0"
have "a = b * (a div b) + a mod b" by (simp add: mult_div_mod_eq)
moreover have "a mod b = 0 ∨ euclidean_size (a mod b) < euclidean_size b"
using mod_size_less[OF bnz] by blast
ultimately show "∃q∈UNIV. ∃r∈UNIV.
a = b * q + r ∧ (r = 0 ∨ euclidean_size r < euclidean_size b)"
by (intro bexI[of _ "a div b"] bexI[of _ "a mod b"]) auto
qed
qed
subsection ‹The integers›
text ‹‹ℤ› is a Euclidean ring with Euclidean size the absolute value, so the bridge specialises to
it directly. Through the interpretation ‹ℤ› inherits the whole tower: it is a principal ideal
domain and a factorial (unique factorization) domain --- the fundamental theorem of arithmetic.›