Theory HOL-Algebra.Ring_Divisibility

(*  Title:      HOL/Algebra/Ring_Divisibility.thy
    Author:     Paulo EmΓ­lio de Vilhena
*)

theory Ring_Divisibility
imports Ideal Divisibility QuotRing Multiplicative_Group

begin

(* TEMPORARY ====================================================================== *)
definition mult_of :: "('a, 'b) ring_scheme β‡’ 'a monoid" where
  "mult_of R ≑ ⦇ carrier = carrier R - {πŸ¬β‡˜R⇙}, mult = mult R, one = πŸ­β‡˜Rβ‡™β¦ˆ"

lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {πŸ¬β‡˜R⇙}"
  by (simp add: mult_of_def)

lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
 by (simp add: mult_of_def)

lemma nat_pow_mult_of: "([^]β‡˜mult_of R⇙) = (([^]β‡˜R⇙) :: _ β‡’ nat β‡’ _)"
  by (simp add: mult_of_def fun_eq_iff nat_pow_def)

lemma one_mult_of [simp]: "πŸ­β‡˜mult_of R⇙ = πŸ­β‡˜R⇙"
  by (simp add: mult_of_def)
(* ================================================================================ *)

section β€ΉThe Arithmetic of Ringsβ€Ί

text β€ΉIn this section we study the links between the divisibility theory and that of ringsβ€Ί


subsection β€ΉDefinitionsβ€Ί

locale factorial_domain = domain + factorial_monoid "mult_of R"

locale noetherian_ring = ring +
  assumes finetely_gen: "ideal I R ⟹ βˆƒA βŠ† carrier R. finite A ∧ I = Idl A"

locale noetherian_domain = noetherian_ring + domain

locale principal_domain = domain +
  assumes exists_gen: "ideal I R ⟹ βˆƒa ∈ carrier R. I = PIdl a"

locale euclidean_domain =
  domain R for R (structure) + fixes Ο† :: "'a β‡’ nat"
  assumes euclidean_function:
  " ⟦ a ∈ carrier R - { 𝟬 }; b ∈ carrier R - { 𝟬 } ⟧ ⟹
   βˆƒq r. q ∈ carrier R ∧ r ∈ carrier R ∧ a = (b βŠ— q) βŠ• r ∧ ((r = 𝟬) ∨ (Ο† r < Ο† b))"

definition ring_irreducible :: "('a, 'b) ring_scheme β‡’ 'a β‡’ bool" (β€Ήring'_irreducibleΔ±β€Ί)
  where "ring_irreducibleβ‡˜R⇙ a ⟷ (a β‰  πŸ¬β‡˜R⇙) ∧ (irreducible R a)"

definition ring_prime :: "('a, 'b) ring_scheme β‡’ 'a β‡’ bool" (β€Ήring'_primeΔ±β€Ί)
  where "ring_primeβ‡˜R⇙ a ⟷ (a β‰  πŸ¬β‡˜R⇙) ∧ (prime R a)"


subsection β€ΉThe cancellative monoid of a domain. β€Ί

sublocale domain < mult_of: comm_monoid_cancel "mult_of R"
  rewrites "mult (mult_of R) = mult R"
       and "one  (mult_of R) =  one R"
  using m_comm m_assoc
  by (auto intro!: comm_monoid_cancelI comm_monoidI
         simp add: m_rcancel integral_iff)

sublocale factorial_domain < mult_of: factorial_monoid "mult_of R"
  rewrites "mult (mult_of R) = mult R"
       and "one  (mult_of R) =  one R"
  using factorial_monoid_axioms by auto

lemma (in ring) noetherian_ringI:
  assumes "β‹€I. ideal I R ⟹ βˆƒA βŠ† carrier R. finite A ∧ I = Idl A"
  shows "noetherian_ring R"
  using assms by unfold_locales auto

lemma (in domain) euclidean_domainI:
  assumes "β‹€a b. ⟦ a ∈ carrier R - { 𝟬 }; b ∈ carrier R - { 𝟬 } ⟧ ⟹
           βˆƒq r. q ∈ carrier R ∧ r ∈ carrier R ∧ a = (b βŠ— q) βŠ• r ∧ ((r = 𝟬) ∨ (Ο† r < Ο† b))"
  shows "euclidean_domain R Ο†"
  using assms by unfold_locales auto


subsection β€ΉPassing from termβ€ΉRβ€Ί to termβ€Ήmult_of Rβ€Ί and vice-versa. β€Ί

lemma divides_mult_imp_divides [simp]: "a dividesβ‡˜(mult_of R)⇙ b ⟹ a dividesβ‡˜R⇙ b"
  unfolding factor_def by auto

lemma (in domain) divides_imp_divides_mult [simp]:
  "⟦ a ∈ carrier R; b ∈ carrier R - { 𝟬 } ⟧ ⟹ a dividesβ‡˜R⇙ b ⟹ a dividesβ‡˜(mult_of R)⇙ b"
  unfolding factor_def using integral_iff by auto

lemma (in cring) divides_one:
  assumes "a ∈ carrier R"
  shows "a divides 𝟭 ⟷ a ∈ Units R"
  using assms m_comm unfolding factor_def Units_def by force

lemma (in ring) one_divides:
  assumes "a ∈ carrier R" shows "𝟭 divides a"
  using assms unfolding factor_def by simp

lemma (in ring) divides_zero:
  assumes "a ∈ carrier R" shows "a divides 𝟬"
  using r_null[OF assms] unfolding factor_def by force

lemma (in ring) zero_divides:
  shows "𝟬 divides a ⟷ a = 𝟬"
  unfolding factor_def by auto

lemma (in domain) divides_mult_zero:
  assumes "a ∈ carrier R" shows "a dividesβ‡˜(mult_of R)⇙ 𝟬 ⟹ a = 𝟬"
  using integral[OF _ assms] unfolding factor_def by auto

lemma (in ring) divides_mult:
  assumes "a ∈ carrier R" "c ∈ carrier R"
  shows "a divides b ⟹ (c βŠ— a) divides (c βŠ— b)"
  using m_assoc[OF assms(2,1)] unfolding factor_def by auto

lemma (in domain) mult_divides:
  assumes "a ∈ carrier R" "b ∈ carrier R" "c ∈ carrier R - { 𝟬 }"
  shows "(c βŠ— a) divides (c βŠ— b) ⟹ a divides b"
  using assms m_assoc[of c] unfolding factor_def by (simp add: m_lcancel)

lemma (in domain) assoc_iff_assoc_mult:
  assumes "a ∈ carrier R" and "b ∈ carrier R"
  shows "a ∼ b ⟷ a βˆΌβ‡˜(mult_of R)⇙ b"
proof
  assume "a βˆΌβ‡˜(mult_of R)⇙ b" thus "a ∼ b"
    unfolding associated_def factor_def by auto
next
  assume A: "a ∼ b"
  then obtain c1 c2
    where c1: "c1 ∈ carrier R" "a = b βŠ— c1" and c2: "c2 ∈ carrier R" "b = a βŠ— c2"
    unfolding associated_def factor_def by auto
  show "a βˆΌβ‡˜(mult_of R)⇙ b"
  proof (cases "a = 𝟬")
    assume a: "a = 𝟬" then have b: "b = 𝟬"
      using c2 by auto
    show ?thesis
      unfolding associated_def factor_def a b by auto
  next
    assume a: "a β‰  𝟬"
    hence b: "b β‰  𝟬" and c1_not_zero: "c1 β‰  𝟬"
      using c1 assms by auto
    hence c2_not_zero: "c2 β‰  𝟬"
      using c2 assms by auto
    show ?thesis
      unfolding associated_def factor_def using c1 c2 c1_not_zero c2_not_zero a b by auto
  qed
qed

lemma (in domain) Units_mult_eq_Units [simp]: "Units (mult_of R) = Units R"
  unfolding Units_def using insert_Diff integral_iff by auto

lemma (in domain) ring_associated_iff:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a ∼ b ⟷ (βˆƒu ∈ Units R. a = u βŠ— b)"
proof (cases "a = 𝟬")
  assume [simp]: "a = 𝟬" show ?thesis
  proof
    assume "a ∼ b" thus "βˆƒu ∈ Units R. a = u βŠ— b"
      using zero_divides unfolding associated_def by force
  next
    assume "βˆƒu ∈ Units R. a = u βŠ— b" then have "b = 𝟬"
      by (metis Units_closed Units_l_cancel β€Ήa = πŸ¬β€Ί assms r_null)
    thus "a ∼ b"
      using zero_divides[of 𝟬] by auto
  qed
next
  assume a: "a β‰  𝟬" show ?thesis
  proof (cases "b = 𝟬")
    assume "b = 𝟬" thus ?thesis
      using assms a zero_divides[of a] r_null unfolding associated_def by blast
  next
    assume b: "b β‰  𝟬"
    have "(βˆƒu ∈ Units R. a = u βŠ— b) ⟷ (βˆƒu ∈ Units R. a = b βŠ— u)"
      using m_comm[OF assms(2)] Units_closed by auto
    thus ?thesis
      using mult_of.associated_iff[of a b] a b assms
      unfolding assoc_iff_assoc_mult[OF assms] Units_mult_eq_Units
      by auto
  qed
qed

lemma (in domain) properfactor_mult_imp_properfactor:
  "⟦ a ∈ carrier R; b ∈ carrier R ⟧ ⟹ properfactor (mult_of R) b a ⟹ properfactor R b a"
proof -
  assume A: "a ∈ carrier R" "b ∈ carrier R" "properfactor (mult_of R) b a"
  then obtain c where c: "c ∈ carrier (mult_of R)" "a = b βŠ— c"
    unfolding properfactor_def factor_def by auto
  have "a β‰  𝟬"
  proof (rule ccontr)
    assume a: "Β¬ a β‰  𝟬"
    hence "b = 𝟬" using c A integral[of b c] by auto
    hence "b = a βŠ— 𝟭" using a A by simp
    hence "a dividesβ‡˜(mult_of R)⇙ b"
      unfolding factor_def by auto
    thus False using A unfolding properfactor_def by simp
  qed
  hence "b β‰  𝟬"
    using c A integral_iff by auto
  thus "properfactor R b a"
    using A divides_imp_divides_mult[of a b] unfolding properfactor_def
    by (meson DiffI divides_mult_imp_divides empty_iff insert_iff)
qed

lemma (in domain) properfactor_imp_properfactor_mult:
  "⟦ a ∈ carrier R - { 𝟬 }; b ∈ carrier R ⟧ ⟹ properfactor R b a ⟹ properfactor (mult_of R) b a"
  unfolding properfactor_def factor_def by auto

lemma (in domain) properfactor_of_zero:
  assumes "b ∈ carrier R"
  shows "Β¬ properfactor (mult_of R) b 𝟬" and "properfactor R b 𝟬 ⟷ b β‰  𝟬"
  using divides_mult_zero[OF assms] divides_zero[OF assms] unfolding properfactor_def by auto


subsection β€ΉIrreducibleβ€Ί

text β€ΉThe following lemmas justify the need for a definition of irreducible specific to rings:
      for termβ€Ήirreducible Rβ€Ί, we need to suppose we are not in a field (which is plausible,
      but termβ€ΉΒ¬ field Rβ€Ί is an assumption we want to avoid; for termβ€Ήirreducible (mult_of R)β€Ί, zero
      is allowed. β€Ί

lemma (in domain) zero_is_irreducible_mult:
  shows "irreducible (mult_of R) 𝟬"
  unfolding irreducible_def Units_def properfactor_def factor_def
  using integral_iff by fastforce

lemma (in domain) zero_is_irreducible_iff_field:
  shows "irreducible R 𝟬 ⟷ field R"
proof
  assume irr: "irreducible R 𝟬"
  have "β‹€a. ⟦ a ∈ carrier R; a β‰  𝟬 ⟧ ⟹ properfactor R a 𝟬"
    unfolding properfactor_def factor_def by (auto, metis r_null zero_closed)
  hence "carrier R - { 𝟬 } = Units R"
    using irr unfolding irreducible_def by auto
  thus "field R"
    using field.intro[OF domain_axioms] unfolding field_axioms_def by simp
next
  assume field: "field R" show "irreducible R 𝟬"
    using field.field_Units[OF field]
    unfolding irreducible_def properfactor_def factor_def by blast
qed

lemma (in domain) irreducible_imp_irreducible_mult:
  "⟦ a ∈ carrier R; irreducible R a ⟧ ⟹ irreducible (mult_of R) a"
  using zero_is_irreducible_mult Units_mult_eq_Units properfactor_mult_imp_properfactor
  by (cases "a = 𝟬") (auto simp add: irreducible_def)

lemma (in domain) irreducible_mult_imp_irreducible:
  "⟦ a ∈ carrier R - { 𝟬 }; irreducible (mult_of R) a ⟧ ⟹ irreducible R a"
    unfolding irreducible_def using properfactor_imp_properfactor_mult properfactor_divides by fastforce

lemma (in domain) ring_irreducibleE:
  assumes "r ∈ carrier R" and "ring_irreducible r"
  shows "r β‰  𝟬" "irreducible R r" "irreducible (mult_of R) r" "r βˆ‰ Units R"
    and "β‹€a b. ⟦ a ∈ carrier R; b ∈ carrier R ⟧ ⟹ r = a βŠ— b ⟹ a ∈ Units R ∨ b ∈ Units R"
proof -
  show "irreducible (mult_of R) r" "irreducible R r"
    using assms irreducible_imp_irreducible_mult unfolding ring_irreducible_def by auto
  show "r β‰  𝟬" "r βˆ‰ Units R"
    using assms unfolding ring_irreducible_def irreducible_def by auto
next
  fix a b assume a: "a ∈ carrier R" and b: "b ∈ carrier R" and r: "r = a βŠ— b"
  show "a ∈ Units R ∨ b ∈ Units R"
  proof (cases "properfactor R a r")
    assume "properfactor R a r" thus ?thesis
      using a assms(2) unfolding ring_irreducible_def irreducible_def by auto
  next
    assume not_proper: "Β¬ properfactor R a r"
    hence "r divides a"
      using r b unfolding properfactor_def by auto
    then obtain c where c: "c ∈ carrier R" "a = r βŠ— c"
      unfolding factor_def by auto
    have "𝟭 = c βŠ— b"
      using r c(1) b assms m_assoc m_lcancel[OF _ assms(1) one_closed m_closed[OF c(1) b]]
      unfolding c(2) ring_irreducible_def by auto
    thus ?thesis
      using c(1) b m_comm unfolding Units_def by auto
  qed
qed

lemma (in domain) ring_irreducibleI:
  assumes "r ∈ carrier R - { 𝟬 }" "r βˆ‰ Units R"
    and "β‹€a b. ⟦ a ∈ carrier R; b ∈ carrier R ⟧ ⟹ r = a βŠ— b ⟹ a ∈ Units R ∨ b ∈ Units R"
  shows "ring_irreducible r"
  unfolding ring_irreducible_def
proof
  show "r β‰  𝟬" using assms(1) by blast
next
  show "irreducible R r"
  proof (rule irreducibleI[OF assms(2)])
    fix a assume a: "a ∈ carrier R" "properfactor R a r"
    then obtain b where b: "b ∈ carrier R" "r = a βŠ— b"
      unfolding properfactor_def factor_def by blast
    hence "a ∈ Units R ∨ b ∈ Units R"
      using assms(3)[OF a(1) b(1)] by simp
    thus "a ∈ Units R"
    proof (auto)
      assume "b ∈ Units R"
      hence "r βŠ— inv b = a" and "inv b ∈ carrier R"
        using b a by (simp add: m_assoc)+
      thus ?thesis
        using a(2) unfolding properfactor_def factor_def by blast
    qed
  qed
qed

lemma (in domain) ring_irreducibleI':
  assumes "r ∈ carrier R - { 𝟬 }" "irreducible (mult_of R) r"
  shows "ring_irreducible r"
  unfolding ring_irreducible_def
  using irreducible_mult_imp_irreducible[OF assms] assms(1) by auto


subsection β€ΉPrimesβ€Ί

lemma (in domain) zero_is_prime: "prime R 𝟬" "prime (mult_of R) 𝟬"
  using integral unfolding prime_def factor_def Units_def by auto

lemma (in domain) prime_eq_prime_mult:
  assumes "p ∈ carrier R"
  shows "prime R p ⟷ prime (mult_of R) p"
proof (cases "p = 𝟬", auto simp add: zero_is_prime)
  assume "p β‰  𝟬" "prime R p" thus "prime (mult_of R) p"
    unfolding prime_def
    using divides_mult_imp_divides Units_mult_eq_Units mult_mult_of
    by (metis DiffD1 assms carrier_mult_of divides_imp_divides_mult)
next
  assume p: "p β‰  𝟬" "prime (mult_of R) p" show "prime R p"
  proof (rule primeI)
    show "p βˆ‰ Units R"
      using p(2) Units_mult_eq_Units unfolding prime_def by simp
  next
    fix a b assume a: "a ∈ carrier R" and b: "b ∈ carrier R" and dvd: "p divides a βŠ— b"
    then obtain c where c: "c ∈ carrier R" "a βŠ— b = p βŠ— c"
      unfolding factor_def by auto
    show "p divides a ∨ p divides b"
    proof (cases "a βŠ— b = 𝟬")
      case True thus ?thesis
        using integral[OF _ a b] c unfolding factor_def by force
    next
      case False
      hence "p dividesβ‡˜(mult_of R)⇙ (a βŠ— b)"
        using divides_imp_divides_mult[OF assms _ dvd] m_closed[OF a b] by simp
      moreover have "a β‰  𝟬" "b β‰  𝟬" "c β‰  𝟬"
        using False a b c p l_null integral_iff by (auto, simp add: assms)
      ultimately show ?thesis
        using a b p unfolding prime_def
        by (auto, metis Diff_iff divides_mult_imp_divides singletonD)
    qed
  qed
qed

lemma (in domain) ring_primeE:
  assumes "p ∈ carrier R" "ring_prime p"
  shows "p β‰  𝟬" "prime (mult_of R) p" "prime R p"
  using assms prime_eq_prime_mult unfolding ring_prime_def by auto

lemma (in ring) ring_primeI: (* in ring only to avoid instantiating R *)
  assumes "p β‰  𝟬" "prime R p" shows "ring_prime p"
  using assms unfolding ring_prime_def by auto

lemma (in domain) ring_primeI':
  assumes "p ∈ carrier R - { 𝟬 }" "prime (mult_of R) p"
  shows "ring_prime p"
  using assms prime_eq_prime_mult unfolding ring_prime_def by auto


subsection β€ΉBasic Propertiesβ€Ί

lemma (in cring) to_contain_is_to_divide:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "PIdl b βŠ† PIdl a ⟷ a divides b"
proof
  show "PIdl b βŠ† PIdl a ⟹ a divides b"
  proof -
    assume "PIdl b βŠ† PIdl a"
    hence "b ∈ PIdl a"
      by (meson assms(2) local.ring_axioms ring.cgenideal_self subsetCE)
    thus ?thesis
      unfolding factor_def cgenideal_def using m_comm assms(1) by blast
  qed
  show "a divides b ⟹ PIdl b βŠ† PIdl a"
  proof -
    assume "a divides b" then obtain c where c: "c ∈ carrier R" "b = c βŠ— a"
      unfolding factor_def using m_comm[OF assms(1)] by blast
    show "PIdl b βŠ† PIdl a"
    proof
      fix x assume "x ∈ PIdl b"
      then obtain d where d: "d ∈ carrier R" "x = d βŠ— b"
        unfolding cgenideal_def by blast
      hence "x = (d βŠ— c) βŠ— a"
        using c d m_assoc assms by simp
      thus "x ∈ PIdl a"
        unfolding cgenideal_def using m_assoc assms c d by blast
    qed
  qed
qed

lemma (in cring) associated_iff_same_ideal:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a ∼ b ⟷ PIdl a = PIdl b"
  unfolding associated_def
  using to_contain_is_to_divide[OF assms]
        to_contain_is_to_divide[OF assms(2,1)] by auto

lemma (in cring) ideal_eq_carrier_iff:
  assumes "a ∈ carrier R"
  shows "carrier R = PIdl a ⟷ a ∈ Units R"
proof
  assume "carrier R = PIdl a"
  hence "𝟭 ∈ PIdl a"
    by auto
  then obtain b where "b ∈ carrier R" "𝟭 = a βŠ— b" "𝟭 = b βŠ— a"
    unfolding cgenideal_def using m_comm[OF assms] by auto
  thus "a ∈ Units R"
    using assms unfolding Units_def by auto
next
  assume "a ∈ Units R"
  then have inv_a: "inv a ∈ carrier R" "inv a βŠ— a = 𝟭"
    by auto
  have "carrier R βŠ† PIdl a"
  proof
    fix b assume "b ∈ carrier R"
    hence "(b βŠ— inv a) βŠ— a = b" and "b βŠ— inv a ∈ carrier R"
      using m_assoc[OF _ inv_a(1) assms] inv_a by auto
    thus "b ∈ PIdl a"
      unfolding cgenideal_def by force
  qed
  thus "carrier R = PIdl a"
    using assms by (simp add: cgenideal_eq_rcos r_coset_subset_G subset_antisym)
qed

lemma (in domain) primeideal_iff_prime:
  assumes "p ∈ carrier R - { 𝟬 }"
  shows "primeideal (PIdl p) R ⟷ ring_prime p"
proof
  assume PIdl: "primeideal (PIdl p) R" show "ring_prime p"
  proof (rule ring_primeI)
    show "p β‰  𝟬" using assms by simp
  next
    show "prime R p"
    proof (rule primeI)
      show "p βˆ‰ Units R"
        using ideal_eq_carrier_iff[of p] assms primeideal.I_notcarr[OF PIdl] by auto
    next
      fix a b assume a: "a ∈ carrier R" and b: "b ∈ carrier R" and dvd: "p divides a βŠ— b"
      hence "a βŠ— b ∈ PIdl p"
        by (meson assms DiffD1 cgenideal_self contra_subsetD m_closed to_contain_is_to_divide)
      hence "a ∈ PIdl p ∨ b ∈ PIdl p"
        using primeideal.I_prime[OF PIdl a b] by simp
      thus "p divides a ∨ p divides b"
        using assms a b Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
    qed
  qed
next
  assume prime: "ring_prime p" show "primeideal (PIdl p) R"
  proof (rule primeidealI[OF cgenideal_ideal cring_axioms])
    show "p ∈ carrier R" and "carrier R β‰  PIdl p"
      using ideal_eq_carrier_iff[of p] assms prime
      unfolding ring_prime_def prime_def by auto
  next
    fix a b assume a: "a ∈ carrier R" and b: "b ∈ carrier R" "a βŠ— b ∈ PIdl p"
    hence "p divides a βŠ— b"
      using assms Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
    hence "p divides a ∨ p divides b"
      using a b assms primeE[OF ring_primeE(3)[OF _ prime]] by auto
    thus "a ∈ PIdl p ∨ b ∈ PIdl p"
      using a b assms Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
  qed
qed


subsection β€ΉNoetherian Ringsβ€Ί

lemma (in ring) chain_Union_is_ideal:
  assumes "subset.chain { I. ideal I R } C"
  shows "ideal (if C = {} then { 𝟬 } else (⋃C)) R"
proof (cases "C = {}")
  case True thus ?thesis by (simp add: zeroideal)
next
  case False have "ideal (⋃C) R"
  proof (rule idealI[OF ring_axioms])
    show "subgroup (⋃C) (add_monoid R)"
    proof
      show "⋃C βŠ† carrier (add_monoid R)"
        using assms subgroup.subset[OF additive_subgroup.a_subgroup]
        unfolding pred_on.chain_def ideal_def by auto

      obtain I where I: "I ∈ C" "ideal I R"
        using False assms unfolding pred_on.chain_def by auto
      thus "πŸ­β‡˜add_monoid R⇙ ∈ ⋃C"
        using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF I(2)]] by auto
    next
      fix x y assume "x ∈ ⋃C" "y ∈ ⋃C"
      then obtain I where I: "I ∈ C" "x ∈ I" "y ∈ I"
        using assms unfolding pred_on.chain_def by blast
      hence ideal: "ideal I R"
        using assms unfolding pred_on.chain_def by auto
      thus "x βŠ—β‡˜add_monoid R⇙ y ∈ ⋃C"
        using UnionI I additive_subgroup.a_closed unfolding ideal_def by fastforce

      show "invβ‡˜add_monoid R⇙ x ∈ ⋃C"
        using UnionI I additive_subgroup.a_inv_closed ideal unfolding ideal_def a_inv_def by metis
    qed
  next
    fix a x assume a: "a ∈ ⋃C" and x: "x ∈ carrier R"
    then obtain I where I: "ideal I R" "a ∈ I" and "I ∈ C"
      using assms unfolding pred_on.chain_def by auto
    thus "x βŠ— a ∈ ⋃C" and "a βŠ— x ∈ ⋃C"
      using ideal.I_l_closed[OF I x] ideal.I_r_closed[OF I x] by auto
  qed
  thus ?thesis
    using False by simp
qed

lemma (in noetherian_ring) ideal_chain_is_trivial:
  assumes "C β‰  {}" "subset.chain { I. ideal I R } C"
  shows "⋃C ∈ C"
proof -
  { fix S assume "finite S" "S βŠ† ⋃C"
    hence "βˆƒI. I ∈ C ∧ S βŠ† I"
    proof (induct S)
      case empty thus ?case
        using assms(1) by blast
    next
      case (insert s S)
      then obtain I where I: "I ∈ C" "S βŠ† I"
        by blast
      moreover obtain I' where I': "I' ∈ C" "s ∈ I'"
        using insert(4) by blast
      ultimately have "I βŠ† I' ∨ I' βŠ† I"
        using assms unfolding pred_on.chain_def by blast
      thus ?case
        using I I' by blast
    qed } note aux_lemma = this

  obtain S where S: "finite S" "S βŠ† carrier R" "⋃C = Idl S"
    using finetely_gen[OF chain_Union_is_ideal[OF assms(2)]] assms(1) by auto
  then obtain I where I: "I ∈ C" and "S βŠ† I"
    using aux_lemma[OF S(1)] genideal_self[OF S(2)] by blast
  hence "Idl S βŠ† I"
    using assms unfolding pred_on.chain_def
    by (metis genideal_minimal mem_Collect_eq rev_subsetD)
  hence "⋃C = I"
    using S(3) I by auto
  thus ?thesis
    using I by simp
qed

lemma (in ring) trivial_ideal_chain_imp_noetherian:
  assumes "β‹€C. ⟦ C β‰  {}; subset.chain { I. ideal I R } C ⟧ ⟹ ⋃C ∈ C"
  shows "noetherian_ring R"
proof (rule noetherian_ringI)
  fix I assume I: "ideal I R"
  have in_carrier: "I βŠ† carrier R" and add_subgroup: "additive_subgroup I R"
    using ideal.axioms(1)[OF I] additive_subgroup.a_subset by auto

  define S where "S = { Idl S' | S'. S' βŠ† I ∧ finite S' }"
  have "βˆƒM ∈ S. βˆ€S' ∈ S. M βŠ† S' ⟢ S' = M"
  proof (rule subset_Zorn)
    fix C assume C: "subset.chain S C"
    show "βˆƒU ∈ S. βˆ€S' ∈ C. S' βŠ† U"
    proof (cases "C = {}")
      case True
      have "{ 𝟬 } ∈ S"
        using additive_subgroup.zero_closed[OF add_subgroup] genideal_zero
        by (auto simp add: S_def)
      thus ?thesis
        using True by auto
    next
      case False
      have "S βŠ† { I. ideal I R }"
        using additive_subgroup.a_subset[OF add_subgroup] genideal_ideal
        by (auto simp add: S_def)
      hence "subset.chain { I. ideal I R } C"
        using C unfolding pred_on.chain_def by auto
      then have "⋃C ∈ C"
        using assms False by simp
      thus ?thesis
        by (meson C Union_upper pred_on.chain_def subsetCE)
    qed
  qed
  then obtain M where M: "M ∈ S" "β‹€S'. ⟦S' ∈ S; M βŠ† S' ⟧ ⟹ S' = M"
    by auto
  then obtain S' where S': "S' βŠ† I" "finite S'" "M = Idl S'"
    by (auto simp add: S_def)
  hence "M βŠ† I"
    using I genideal_minimal by (auto simp add: S_def)
  moreover have "I βŠ† M"
  proof (rule ccontr)
    assume "Β¬ I βŠ† M"
    then obtain a where a: "a ∈ I" "a βˆ‰ M"
      by auto
    have "M βŠ† Idl (insert a S')"
      using S' a(1) genideal_minimal[of "Idl (insert a S')" S']
            in_carrier genideal_ideal genideal_self
      by (meson insert_subset subset_trans)
    moreover have "Idl (insert a S') ∈ S"
      using a(1) S' by (auto simp add: S_def)
    ultimately have "M = Idl (insert a S')"
      using M(2) by auto
    hence "a ∈ M"
      using genideal_self S'(1) a (1) in_carrier by (meson insert_subset subset_trans)
    from β€Ήa ∈ Mβ€Ί and β€Ήa βˆ‰ Mβ€Ί show False by simp
  qed
  ultimately have "M = I" by simp
  thus "βˆƒA βŠ† carrier R. finite A ∧ I = Idl A"
    using S' in_carrier by blast
qed

lemma (in noetherian_domain) factorization_property:
  assumes "a ∈ carrier R - { 𝟬 }" "a βˆ‰ Units R"
  shows "βˆƒfs. set fs βŠ† carrier (mult_of R) ∧ wfactors (mult_of R) fs a" (is "?factorizable a")
proof (rule ccontr)
  assume a: "Β¬ ?factorizable a"
  define S where "S = { PIdl r | r. r ∈ carrier R - { 𝟬 } ∧ r βˆ‰ Units R ∧ Β¬ ?factorizable r }"
  then obtain C where C: "subset.maxchain S C"
    using subset.Hausdorff by blast
  hence chain: "subset.chain S C"
    using pred_on.maxchain_def by blast
  moreover have "S βŠ† { I. ideal I R }"
    using cgenideal_ideal by (auto simp add: S_def)
  ultimately have "subset.chain { I. ideal I R } C"
    by (meson dual_order.trans pred_on.chain_def)
  moreover have "PIdl a ∈ S"
    using assms a by (auto simp add: S_def)
  hence "subset.chain S { PIdl a }"
    unfolding pred_on.chain_def by auto
  hence "C β‰  {}"
    using C unfolding pred_on.maxchain_def by auto
  ultimately have "⋃C ∈ C"
    using ideal_chain_is_trivial by simp
  hence "⋃C ∈ S"
    using chain unfolding pred_on.chain_def by auto
  then obtain r where r: "⋃C = PIdl r" "r ∈ carrier R - { 𝟬 }" "r βˆ‰ Units R" "Β¬ ?factorizable r"
    by (auto simp add: S_def)
  have "βˆƒp. p ∈ carrier R - { 𝟬 } ∧ p βˆ‰ Units R ∧ Β¬ ?factorizable p ∧ p divides r ∧ Β¬ r divides p"
  proof -
    have "wfactors (mult_of R) [ r ] r" if "irreducible (mult_of R) r"
      using r(2) that unfolding wfactors_def by auto
    hence "Β¬ irreducible (mult_of R) r"
      using r(2,4) by auto
    hence "Β¬ ring_irreducible r"
      using ring_irreducibleE(3) r(2) by auto
    then obtain p1 p2
      where p1_p2: "p1 ∈ carrier R" "p2 ∈ carrier R" "r = p1 βŠ— p2" "p1 βˆ‰ Units R" "p2 βˆ‰ Units R"
      using ring_irreducibleI[OF r(2-3)] by auto
    hence in_carrier: "p1 ∈ carrier (mult_of R)" "p2 ∈ carrier (mult_of R)"
      using r(2) by auto

    have "⟦ ?factorizable p1; ?factorizable p2 ⟧ ⟹ ?factorizable r"
      using mult_of.wfactors_mult[OF _ _ in_carrier] p1_p2(3) by (metis le_sup_iff set_append)
    hence "¬ ?factorizable p1 ∨ ¬ ?factorizable p2"
      using r(4) by auto

    moreover
    have "β‹€p1 p2. ⟦ p1 ∈ carrier R; p2 ∈ carrier R; r = p1 βŠ— p2; r divides p1 ⟧ ⟹ p2 ∈ Units R"
    proof -
      fix p1 p2 assume A: "p1 ∈ carrier R" "p2 ∈ carrier R" "r = p1 βŠ— p2" "r divides p1"
      then obtain c where c: "c ∈ carrier R" "p1 = r βŠ— c"
        unfolding factor_def by blast
      hence "𝟭 = c βŠ— p2"
        using A m_lcancel[OF _ _ one_closed, of r "c βŠ— p2"] r(2) by (auto, metis m_assoc m_closed)
      thus "p2 ∈ Units R"
        unfolding Units_def using c A(2) m_comm[OF c(1) A(2)] by auto
    qed
    hence "Β¬ r divides p1" and "Β¬ r divides p2"
      using p1_p2 m_comm[OF p1_p2(1-2)] by blast+

    ultimately show ?thesis
      using p1_p2 in_carrier by (metis carrier_mult_of dividesI' m_comm)
  qed
  then obtain p
    where p: "p ∈ carrier R - { 𝟬 }" "p βˆ‰ Units R" "Β¬ ?factorizable p" "p divides r" "Β¬ r divides p"
    by blast
  hence "PIdl p ∈ S"
    unfolding S_def by auto
  moreover have "⋃C βŠ‚ PIdl p"
    using p r to_contain_is_to_divide unfolding r(1) by (metis Diff_iff psubsetI)
  ultimately have "subset.chain S (insert (PIdl p) C)" and "C βŠ‚ (insert (PIdl p) C)"
    unfolding pred_on.chain_def by (metis C psubsetE subset_maxchain_max, blast)
  thus False
    using C unfolding pred_on.maxchain_def by blast
qed

lemma (in noetherian_domain) exists_irreducible_divisor:
  assumes "a ∈ carrier R - { 𝟬 }" and "a βˆ‰ Units R"
  obtains b where "b ∈ carrier R" and "ring_irreducible b" and "b divides a"
proof -
  obtain fs where set_fs: "set fs βŠ† carrier (mult_of R)" and "wfactors (mult_of R) fs a"
    using factorization_property[OF assms] by blast
  hence "a ∈ Units R" if "fs = []"
    using that assms(1) Units_cong assoc_iff_assoc_mult unfolding wfactors_def by (simp, blast)
  hence "fs β‰  []"
    using assms(2) by auto
  then obtain f' fs' where fs: "fs = f' # fs'"
    using list.exhaust by blast
  from β€Ήwfactors (mult_of R) fs aβ€Ί have "f' divides a"
    using mult_of.wfactors_dividesI[OF _ set_fs] assms(1) unfolding fs by auto
  moreover from β€Ήwfactors (mult_of R) fs aβ€Ί have "ring_irreducible f'" and "f' ∈ carrier R"
    using set_fs ring_irreducibleI'[of f'] unfolding wfactors_def fs by auto
  ultimately show thesis
    using that by blast
qed


subsection β€ΉPrincipal Domainsβ€Ί

sublocale principal_domain βŠ† noetherian_domain
proof
  fix I assume "ideal I R"
  then obtain i where "i ∈ carrier R" "I = Idl { i }"
    using exists_gen cgenideal_eq_genideal by auto
  thus "βˆƒA βŠ† carrier R. finite A ∧ I = Idl A"
    by blast
qed

lemma (in principal_domain) irreducible_imp_maximalideal:
  assumes "p ∈ carrier R"
    and "ring_irreducible p"
  shows "maximalideal (PIdl p) R"
proof (rule maximalidealI)
  show "ideal (PIdl p) R"
    using assms(1) by (simp add: cgenideal_ideal)
next
  show "carrier R β‰  PIdl p"
    using ideal_eq_carrier_iff[OF assms(1)] ring_irreducibleE(4)[OF assms] by auto
next
  fix J assume J: "ideal J R" "PIdl p βŠ† J" "J βŠ† carrier R"
  then obtain q where q: "q ∈ carrier R" "J = PIdl q"
    using exists_gen[OF J(1)] cgenideal_eq_rcos by metis
  hence "q divides p"
    using to_contain_is_to_divide[of q p] using assms(1) J(1-2) by simp
  then obtain r where r: "r ∈ carrier R" "p = q βŠ— r"
    unfolding factor_def by auto
  hence "q ∈ Units R ∨ r ∈ Units R"
    using ring_irreducibleE(5)[OF assms q(1)] by auto
  thus "J = PIdl p ∨ J = carrier R"
  proof
    assume "q ∈ Units R" thus ?thesis
      using ideal_eq_carrier_iff[OF q(1)] q(2) by auto
  next
    assume "r ∈ Units R" hence "p ∼ q"
      using assms(1) r q(1) associatedI2' by blast
    thus ?thesis
      unfolding associated_iff_same_ideal[OF assms(1) q(1)] q(2) by auto
  qed
qed

corollary (in principal_domain) primeness_condition:
  assumes "p ∈ carrier R"
  shows "ring_irreducible p ⟷ ring_prime p"
proof
  show "ring_irreducible p ⟹ ring_prime p"
    using maximalideal_prime[OF irreducible_imp_maximalideal] ring_irreducibleE(1)
          primeideal_iff_prime assms by auto
next
  show "ring_prime p ⟹ ring_irreducible p"
    using mult_of.prime_irreducible ring_primeI[of p] ring_irreducibleI' assms
    unfolding ring_prime_def prime_eq_prime_mult[OF assms] by auto
qed

lemma (in principal_domain) domain_iff_prime:
  assumes "a ∈ carrier R - { 𝟬 }"
  shows "domain (R Quot (PIdl a)) ⟷ ring_prime a"
  using quot_domain_iff_primeideal[of "PIdl a"] primeideal_iff_prime[of a]
        cgenideal_ideal[of a] assms by auto

lemma (in principal_domain) field_iff_prime:
  assumes "a ∈ carrier R - { 𝟬 }"
  shows "field (R Quot (PIdl a)) ⟷ ring_prime a"
proof
  show "ring_prime a ⟹ field  (R Quot (PIdl a))"
    using  primeness_condition[of a] irreducible_imp_maximalideal[of a]
           maximalideal.quotient_is_field[of "PIdl a" R] is_cring assms by auto
next
  show "field  (R Quot (PIdl a)) ⟹ ring_prime a"
    unfolding field_def using domain_iff_prime[of a] assms by auto
qed


sublocale principal_domain < mult_of: primeness_condition_monoid "mult_of R"
  rewrites "mult (mult_of R) = mult R"
       and "one  (mult_of R) = one R"
    unfolding primeness_condition_monoid_def
              primeness_condition_monoid_axioms_def
proof (auto simp add: mult_of.is_comm_monoid_cancel)
  fix a assume a: "a ∈ carrier R" "a β‰  𝟬" "irreducible (mult_of R) a"
  show "prime (mult_of R) a"
    using primeness_condition[OF a(1)] irreducible_mult_imp_irreducible[OF _ a(3)] a(1-2)
    unfolding ring_prime_def ring_irreducible_def prime_eq_prime_mult[OF a(1)] by auto
qed

sublocale principal_domain < mult_of: factorial_monoid "mult_of R"
  rewrites "mult (mult_of R) = mult R"
       and "one  (mult_of R) = one R"
  using mult_of.wfactors_unique factorization_property mult_of.is_comm_monoid_cancel
  by (auto intro!: mult_of.factorial_monoidI)

sublocale principal_domain βŠ† factorial_domain
  unfolding factorial_domain_def using domain_axioms mult_of.factorial_monoid_axioms by simp

lemma (in principal_domain) ideal_sum_iff_gcd:
  assumes "a ∈ carrier R" "b ∈ carrier R" "d ∈ carrier R"
  shows "PIdl d = PIdl a <+>β‡˜R⇙ PIdl b ⟷ d gcdof a b"
proof -
  { fix a b d
    assume in_carrier: "a ∈ carrier R" "b ∈ carrier R" "d ∈ carrier R"
       and ideal_eq: "PIdl d = PIdl a <+>β‡˜R⇙ PIdl b"
    have "d gcdof a b"
    proof (auto simp add: isgcd_def)
      have "a ∈ PIdl d" and "b ∈ PIdl d"
        using in_carrier(1-2)[THEN cgenideal_ideal] additive_subgroup.zero_closed[OF ideal.axioms(1)]
              in_carrier(1-2)[THEN cgenideal_self] in_carrier(1-2)
        unfolding ideal_eq set_add_def' by force+
      thus "d divides a" and "d divides b"
        using in_carrier(1,2)[THEN to_contain_is_to_divide[OF in_carrier(3)]]
              cgenideal_minimal[OF cgenideal_ideal[OF in_carrier(3)]] by simp+
    next
      fix c assume c: "c ∈ carrier R" "c divides a" "c divides b"
      hence "PIdl a βŠ† PIdl c" and "PIdl b βŠ† PIdl c"
        using to_contain_is_to_divide in_carrier by auto
      hence "PIdl a <+>β‡˜R⇙ PIdl b βŠ† PIdl c"
        by (metis Un_subset_iff c(1) in_carrier(1-2) cgenideal_ideal genideal_minimal union_genideal)
      thus "c divides d"
        using ideal_eq to_contain_is_to_divide[OF c(1) in_carrier(3)] by simp
    qed } note aux_lemma = this

  have "PIdl d = PIdl a <+>β‡˜R⇙ PIdl b ⟹ d gcdof a b"
    using aux_lemma assms by simp

  moreover
  have "d gcdof a b ⟹ PIdl d = PIdl a <+>β‡˜R⇙ PIdl b"
  proof -
    assume d: "d gcdof a b"
    obtain c where c: "c ∈ carrier R" "PIdl c = PIdl a <+>β‡˜R⇙ PIdl b"
      using exists_gen[OF add_ideals[OF assms(1-2)[THEN cgenideal_ideal]]] by blast
    hence "c gcdof a b"
      using aux_lemma assms by simp
    from β€Ήd gcdof a bβ€Ί and β€Ήc gcdof a bβ€Ί have "d ∼ c"
      using assms c(1) by (simp add: associated_def isgcd_def)
    thus ?thesis
      using c(2) associated_iff_same_ideal[OF assms(3) c(1)] by simp
  qed

  ultimately show ?thesis by auto
qed

lemma (in principal_domain) bezout_identity:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "PIdl a <+>β‡˜R⇙ PIdl b = PIdl (somegcd R a b)"
proof -
  have "βˆƒd ∈ carrier R. d gcdof a b"
    using exists_gen[OF add_ideals[OF assms(1-2)[THEN cgenideal_ideal]]]
          ideal_sum_iff_gcd[OF assms(1-2)] by auto
  thus ?thesis
    using ideal_sum_iff_gcd[OF assms(1-2)] somegcd_def
    by (metis (no_types, lifting) tfl_some)
qed

subsection β€ΉEuclidean Domainsβ€Ί

sublocale euclidean_domain βŠ† principal_domain
  unfolding principal_domain_def principal_domain_axioms_def
proof (auto)
  show "domain R" by (simp add: domain_axioms)
next
  fix I assume I: "ideal I R" have "principalideal I R"
  proof (cases "I = { 𝟬 }")
    case True thus ?thesis by (simp add: zeropideal)
  next
    case False hence A: "I - { 𝟬 } β‰  {}"
      using I additive_subgroup.zero_closed ideal.axioms(1) by auto
    define phi_img :: "nat set" where "phi_img = (Ο† ` (I - { 𝟬 }))"
    hence "phi_img β‰  {}" using A by simp
    then obtain m where "m ∈ phi_img" "β‹€k. k ∈ phi_img ⟹ m ≀ k"
      using exists_least_iff[of "λn. n ∈ phi_img"] not_less by force
    then obtain a where a: "a ∈ I - { 𝟬 }" "β‹€b. b ∈ I - { 𝟬 } ⟹ Ο† a ≀ Ο† b"
      using phi_img_def by blast
    have "I = PIdl a"
    proof (rule ccontr)
      assume "I β‰  PIdl a"
      then obtain b where b: "b ∈ I" "b βˆ‰ PIdl a"
        using I β€Ήa ∈ I - {𝟬}β€Ί cgenideal_minimal by auto
      hence "b β‰  𝟬"
        by (metis DiffD1 I a(1) additive_subgroup.zero_closed cgenideal_ideal ideal.Icarr ideal.axioms(1))
      then obtain q r
        where eucl_div: "q ∈ carrier R" "r ∈ carrier R" "b = (a βŠ— q) βŠ• r" "r = 𝟬 ∨ Ο† r < Ο† a"
        using euclidean_function[of b a] a(1) b(1) ideal.Icarr[OF I] by auto
      hence "r = 𝟬 ⟹ b ∈ PIdl a"
        unfolding cgenideal_def using m_comm[of a] ideal.Icarr[OF I] a(1) by auto
      hence 1: "Ο† r < Ο† a ∧ r β‰  𝟬"
        using eucl_div(4) b(2) by auto

      have "r = (βŠ– (a βŠ— q)) βŠ• b"
        using eucl_div(1-3) a(1) b(1) ideal.Icarr[OF I] r_neg1 by auto
      moreover have "βŠ– (a βŠ— q) ∈ I"
        using eucl_div(1) a(1) I
        by (meson DiffD1 additive_subgroup.a_inv_closed ideal.I_r_closed ideal.axioms(1))
      ultimately have 2: "r ∈ I"
        using b(1) additive_subgroup.a_closed[OF ideal.axioms(1)[OF I]] by auto

      from 1 and 2 show False
        using a(2) by fastforce
    qed
    thus ?thesis
      by (meson DiffD1 I cgenideal_is_principalideal ideal.Icarr local.a(1))
  qed
  thus "βˆƒa ∈ carrier R. I = PIdl a"
    by (simp add: cgenideal_eq_genideal principalideal.generate)
qed


sublocale field βŠ† euclidean_domain R "Ξ»_. 0"
proof (rule euclidean_domainI)
  fix a b
  let ?eucl_div = "Ξ»q r. q ∈ carrier R ∧ r ∈ carrier R ∧ a = b βŠ— q βŠ• r ∧ (r = 𝟬 ∨ 0 < 0)"

  assume a: "a ∈ carrier R - { 𝟬 }" and b: "b ∈ carrier R - { 𝟬 }"
  hence "a = b βŠ— ((inv b) βŠ— a) βŠ• 𝟬"
    by (metis DiffD1 Units_inv_closed Units_r_inv field_Units l_one m_assoc r_zero)
  hence "?eucl_div _ ((inv b) βŠ— a) 𝟬"
    using a b field_Units by auto
  thus "βˆƒq r. ?eucl_div _ q r"
    by blast
qed

end