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