--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Ring_Divisibility.thy Mon Jul 02 22:40:25 2018 +0100
@@ -0,0 +1,806 @@
+(* ************************************************************************** *)
+(* Title: Ring_Divisibility.thy *)
+(* Author: Paulo EmÃlio de Vilhena *)
+(* ************************************************************************** *)
+
+theory Ring_Divisibility
+imports Ideal Divisibility QuotRing
+
+begin
+
+section \<open>Definitions ported from Multiplicative_Group.thy\<close>
+
+definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
+ "mult_of R \<equiv> \<lparr> carrier = carrier R - { \<zero>\<^bsub>R\<^esub> }, mult = mult R, one = \<one>\<^bsub>R\<^esub> \<rparr>"
+
+lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - { \<zero>\<^bsub>R\<^esub> }"
+ 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: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
+ by (simp add: mult_of_def fun_eq_iff nat_pow_def)
+
+lemma one_mult_of [simp]: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
+ by (simp add: mult_of_def)
+
+lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
+
+
+section \<open>The Arithmetic of Rings\<close>
+
+text \<open>In this section we study the links between the divisibility theory and that of rings\<close>
+
+
+subsection \<open>Definitions\<close>
+
+locale factorial_domain = domain + factorial_monoid "mult_of R"
+
+locale noetherian_ring = ring +
+ assumes finetely_gen: "ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
+
+locale noetherian_domain = noetherian_ring + domain
+
+locale principal_domain = domain +
+ assumes principal_I: "ideal I R \<Longrightarrow> principalideal I R"
+
+locale euclidean_domain = R?: domain R for R (structure) + fixes \<phi> :: "'a \<Rightarrow> nat"
+ assumes euclidean_function:
+ " \<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+ \<exists>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = (b \<otimes> q) \<oplus> r \<and> ((r = \<zero>) \<or> (\<phi> r < \<phi> b))"
+
+lemma (in domain) mult_of_is_comm_monoid: "comm_monoid (mult_of R)"
+ apply (rule comm_monoidI)
+ apply (auto simp add: integral_iff m_assoc)
+ apply (simp add: m_comm)
+ done
+
+lemma (in domain) cancel_property: "comm_monoid_cancel (mult_of R)"
+ by (rule comm_monoid_cancelI) (auto simp add: mult_of_is_comm_monoid m_rcancel)
+
+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 cancel_property by auto
+
+sublocale noetherian_domain \<subseteq> domain ..
+
+sublocale principal_domain \<subseteq> domain ..
+
+sublocale euclidean_domain \<subseteq> domain ..
+
+lemma (in factorial_monoid) is_factorial_monoid: "factorial_monoid G" ..
+
+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 domain) factorial_domainI:
+ assumes "\<And>a. a \<in> carrier (mult_of R) \<Longrightarrow>
+ \<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs a"
+ and "\<And>a fs fs'. \<lbrakk> a \<in> carrier (mult_of R);
+ set fs \<subseteq> carrier (mult_of R);
+ set fs' \<subseteq> carrier (mult_of R);
+ wfactors (mult_of R) fs a;
+ wfactors (mult_of R) fs' a \<rbrakk> \<Longrightarrow>
+ essentially_equal (mult_of R) fs fs'"
+ shows "factorial_domain R"
+ unfolding factorial_domain_def using mult_of.factorial_monoidI assms domain_axioms by auto
+
+lemma (in domain) is_domain: "domain R" ..
+
+lemma (in ring) noetherian_ringI:
+ assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
+ shows "noetherian_ring R"
+ unfolding noetherian_ring_def noetherian_ring_axioms_def using assms is_ring by simp
+
+lemma (in domain) noetherian_domainI:
+ assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
+ shows "noetherian_domain R"
+ unfolding noetherian_domain_def noetherian_ring_def noetherian_ring_axioms_def
+ using assms is_ring is_domain by simp
+
+lemma (in domain) principal_domainI:
+ assumes "\<And>I. ideal I R \<Longrightarrow> principalideal I R"
+ shows "principal_domain R"
+ unfolding principal_domain_def principal_domain_axioms_def using is_domain assms by auto
+
+lemma (in domain) principal_domainI2:
+ assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>a \<in> carrier R. I = PIdl a"
+ shows "principal_domain R"
+ unfolding principal_domain_def principal_domain_axioms_def
+ using is_domain assms principalidealI cgenideal_eq_genideal by auto
+
+lemma (in domain) euclidean_domainI:
+ assumes "\<And>a b. \<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+ \<exists>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = (b \<otimes> q) \<oplus> r \<and> ((r = \<zero>) \<or> (\<phi> r < \<phi> b))"
+ shows "euclidean_domain R \<phi>"
+ using assms by unfold_locales auto
+
+
+subsection \<open>Basic Properties\<close>
+
+text \<open>Links between domains and commutative cancellative monoids\<close>
+
+lemma (in cring) to_contain_is_to_divide:
+ assumes "a \<in> carrier R" "b \<in> carrier R"
+ shows "(PIdl b \<subseteq> PIdl a) = (a divides b)"
+proof
+ show "PIdl b \<subseteq> PIdl a \<Longrightarrow> a divides b"
+ proof -
+ assume "PIdl b \<subseteq> PIdl a"
+ hence "b \<in> 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 \<Longrightarrow> PIdl b \<subseteq> PIdl a"
+ proof -
+ assume "a divides b" then obtain c where c: "c \<in> carrier R" "b = c \<otimes> a"
+ unfolding factor_def using m_comm[OF assms(1)] by blast
+ show "PIdl b \<subseteq> PIdl a"
+ proof
+ fix x assume "x \<in> PIdl b"
+ then obtain d where d: "d \<in> carrier R" "x = d \<otimes> b"
+ unfolding cgenideal_def by blast
+ hence "x = (d \<otimes> c) \<otimes> a"
+ using c d m_assoc assms by simp
+ thus "x \<in> 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 \<in> carrier R" "b \<in> carrier R"
+ shows "(a \<sim> b) = (PIdl a = PIdl b)"
+ unfolding associated_def
+ using to_contain_is_to_divide[OF assms]
+ to_contain_is_to_divide[OF assms(2) assms(1)] by auto
+
+lemma divides_mult_imp_divides [simp]: "a divides\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a divides\<^bsub>R\<^esub> b"
+ unfolding factor_def by auto
+
+lemma (in domain) divides_imp_divides_mult [simp]:
+ "\<lbrakk> a \<in> carrier R; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+ a divides\<^bsub>R\<^esub> b \<Longrightarrow> a divides\<^bsub>(mult_of R)\<^esub> b"
+ unfolding factor_def using integral_iff by auto
+
+lemma assoc_mult_imp_assoc [simp]: "a \<sim>\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>R\<^esub> b"
+ unfolding associated_def by simp
+
+lemma (in domain) assoc_imp_assoc_mult [simp]:
+ "\<lbrakk> a \<in> carrier R - { \<zero> } ; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+ a \<sim>\<^bsub>R\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+ unfolding associated_def by simp
+
+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) properfactor_mult_imp_properfactor:
+ "\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor (mult_of R) b a \<Longrightarrow> properfactor R b a"
+proof -
+ assume A: "a \<in> carrier R" "b \<in> carrier R" "properfactor (mult_of R) b a"
+ then obtain c where c: "c \<in> carrier (mult_of R)" "a = b \<otimes> c"
+ unfolding properfactor_def factor_def by auto
+ have "a \<noteq> \<zero>"
+ proof (rule ccontr)
+ assume a: "\<not> a \<noteq> \<zero>"
+ hence "b = \<zero>" using c A integral[of b c] by auto
+ hence "b = a \<otimes> \<one>" using a A by simp
+ hence "a divides\<^bsub>(mult_of R)\<^esub> b"
+ unfolding factor_def by auto
+ thus False using A unfolding properfactor_def by simp
+ qed
+ hence "b \<noteq> \<zero>"
+ 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:
+ "\<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor R b a \<Longrightarrow> properfactor (mult_of R) b a"
+ unfolding properfactor_def factor_def by auto
+
+lemma (in domain) primeideal_iff_prime:
+ assumes "p \<in> carrier (mult_of R)"
+ shows "(primeideal (PIdl p) R) = (prime (mult_of R) p)"
+proof
+ show "prime (mult_of R) p \<Longrightarrow> primeideal (PIdl p) R"
+ proof (rule primeidealI)
+ assume A: "prime (mult_of R) p"
+ show "ideal (PIdl p) R" and "cring R"
+ using assms is_cring by (auto simp add: cgenideal_ideal)
+ show "carrier R \<noteq> PIdl p"
+ proof (rule ccontr)
+ assume "\<not> carrier R \<noteq> PIdl p" hence "carrier R = PIdl p" by simp
+ then obtain c where "c \<in> carrier R" "c \<otimes> p = \<one>"
+ unfolding cgenideal_def using one_closed by (smt mem_Collect_eq)
+ hence "p \<in> Units R" unfolding Units_def using m_comm assms by auto
+ thus False using A unfolding prime_def by simp
+ qed
+ fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> PIdl p"
+ thus "a \<in> PIdl p \<or> b \<in> PIdl p"
+ proof (cases "a = \<zero> \<or> b = \<zero>")
+ case True thus "a \<in> PIdl p \<or> b \<in> PIdl p" using ab a b by auto
+ next
+ { fix a assume "a \<in> carrier R" "p divides\<^bsub>mult_of R\<^esub> a"
+ then obtain c where "c \<in> carrier R" "a = p \<otimes> c"
+ unfolding factor_def by auto
+ hence "a \<in> PIdl p" unfolding cgenideal_def using assms m_comm by auto }
+ note aux_lemma = this
+
+ case False hence "a \<noteq> \<zero> \<and> b \<noteq> \<zero>" by simp
+ hence diff_zero: "a \<otimes> b \<noteq> \<zero>" using a b integral by blast
+ then obtain c where c: "c \<in> carrier R" "a \<otimes> b = p \<otimes> c"
+ using assms ab m_comm unfolding cgenideal_def by auto
+ hence "c \<noteq> \<zero>" using c assms diff_zero by auto
+ hence "p divides\<^bsub>(mult_of R)\<^esub> (a \<otimes> b)"
+ unfolding factor_def using ab c by auto
+ hence "p divides\<^bsub>(mult_of R)\<^esub> a \<or> p divides\<^bsub>(mult_of R)\<^esub> b"
+ using A a b False unfolding prime_def by auto
+ thus "a \<in> PIdl p \<or> b \<in> PIdl p" using a b aux_lemma by blast
+ qed
+ qed
+next
+ show "primeideal (PIdl p) R \<Longrightarrow> prime (mult_of R) p"
+ proof -
+ assume A: "primeideal (PIdl p) R" show "prime (mult_of R) p"
+ proof (rule primeI)
+ show "p \<notin> Units (mult_of R)"
+ proof (rule ccontr)
+ assume "\<not> p \<notin> Units (mult_of R)"
+ hence p: "p \<in> Units (mult_of R)" by simp
+ then obtain q where q: "q \<in> carrier R - { \<zero> }" "p \<otimes> q = \<one>" "q \<otimes> p = \<one>"
+ unfolding Units_def apply simp by blast
+ have "PIdl p = carrier R"
+ proof
+ show "PIdl p \<subseteq> carrier R"
+ by (simp add: assms A additive_subgroup.a_subset ideal.axioms(1) primeideal.axioms(1))
+ next
+ show "carrier R \<subseteq> PIdl p"
+ proof
+ fix r assume r: "r \<in> carrier R" hence "r = (r \<otimes> q) \<otimes> p"
+ using p q m_assoc unfolding Units_def by simp
+ thus "r \<in> PIdl p" unfolding cgenideal_def using q r m_closed by blast
+ qed
+ qed
+ moreover have "PIdl p \<noteq> carrier R" using A primeideal.I_notcarr by auto
+ ultimately show False by simp
+ qed
+ next
+ { fix a assume "a \<in> PIdl p" and a: "a \<noteq> \<zero>"
+ then obtain c where c: "c \<in> carrier R" "a = p \<otimes> c"
+ unfolding cgenideal_def using m_comm assms by auto
+ hence "c \<noteq> \<zero>" using assms a by auto
+ hence "p divides\<^bsub>mult_of R\<^esub> a" unfolding factor_def using c by auto }
+ note aux_lemma = this
+
+ fix a b
+ assume a: "a \<in> carrier (mult_of R)" and b: "b \<in> carrier (mult_of R)"
+ and p: "p divides\<^bsub>mult_of R\<^esub> a \<otimes>\<^bsub>mult_of R\<^esub> b"
+ then obtain c where "c \<in> carrier R" "a \<otimes> b = c \<otimes> p"
+ unfolding factor_def using m_comm assms by auto
+ hence "a \<otimes> b \<in> PIdl p" unfolding cgenideal_def by blast
+ hence "a \<in> PIdl p \<or> b \<in> PIdl p" using A primeideal.I_prime[OF A] a b by auto
+ thus "p divides\<^bsub>mult_of R\<^esub> a \<or> p divides\<^bsub>mult_of R\<^esub> b"
+ using a b aux_lemma by auto
+ qed
+ qed
+qed
+
+
+subsection \<open>Noetherian Rings\<close>
+
+lemma (in noetherian_ring) trivial_ideal_seq:
+ assumes "\<And>i :: nat. ideal (I i) R"
+ and "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
+ shows "\<exists>n. \<forall>k. k \<ge> n \<longrightarrow> I k = I n"
+proof -
+ have "ideal (\<Union>i. I i) R"
+ proof
+ show "(\<Union>i. I i) \<subseteq> carrier (add_monoid R)"
+ using additive_subgroup.a_subset assms(1) ideal.axioms(1) by fastforce
+ have "\<one>\<^bsub>add_monoid R\<^esub> \<in> I 0"
+ by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1))
+ thus "\<one>\<^bsub>add_monoid R\<^esub> \<in> (\<Union>i. I i)" by blast
+ next
+ fix x y assume x: "x \<in> (\<Union>i. I i)" and y: "y \<in> (\<Union>i. I i)"
+ then obtain i j where i: "x \<in> I i" and j: "y \<in> I j" by blast
+ hence "inv\<^bsub>add_monoid R\<^esub> x \<in> I i"
+ by (simp add: additive_subgroup.a_subgroup assms(1) ideal.axioms(1) subgroup.m_inv_closed)
+ thus "inv\<^bsub>add_monoid R\<^esub> x \<in> (\<Union>i. I i)" by blast
+ have "x \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> I (max i j)"
+ by (metis add.subgroupE(4) additive_subgroup.a_subgroup assms(1-2) i j ideal.axioms(1)
+ max.cobounded1 max.cobounded2 monoid.select_convs(1) rev_subsetD)
+ thus "x \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> (\<Union>i. I i)" by blast
+ next
+ fix x a assume x: "x \<in> carrier R" and a: "a \<in> (\<Union>i. I i)"
+ then obtain i where i: "a \<in> I i" by blast
+ hence "x \<otimes> a \<in> I i" and "a \<otimes> x \<in> I i"
+ by (simp_all add: assms(1) ideal.I_l_closed ideal.I_r_closed x)
+ thus "x \<otimes> a \<in> (\<Union>i. I i)"
+ and "a \<otimes> x \<in> (\<Union>i. I i)" by blast+
+ qed
+
+ then obtain S where S: "S \<subseteq> carrier R" "finite S" "(\<Union>i. I i) = Idl S"
+ by (meson finetely_gen)
+ hence "S \<subseteq> (\<Union>i. I i)"
+ by (simp add: genideal_self)
+
+ from \<open>finite S\<close> and \<open>S \<subseteq> (\<Union>i. I i)\<close> have "\<exists>n. S \<subseteq> I n"
+ proof (induct S set: "finite")
+ case empty thus ?case by simp
+ next
+ case (insert x S')
+ then obtain n m where m: "S' \<subseteq> I m" and n: "x \<in> I n" by blast
+ hence "insert x S' \<subseteq> I (max m n)"
+ by (meson assms(2) insert_subsetI max.cobounded1 max.cobounded2 rev_subsetD subset_trans)
+ thus ?case by blast
+ qed
+ then obtain n where "S \<subseteq> I n" by blast
+ hence "I n = (\<Union>i. I i)"
+ by (metis S(3) Sup_upper assms(1) genideal_minimal range_eqI subset_antisym)
+ thus ?thesis
+ by (metis (full_types) Sup_upper assms(2) range_eqI subset_antisym)
+qed
+
+lemma increasing_set_seq_iff:
+ "(\<And>i. I i \<subseteq> I (Suc i)) == (\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j)"
+proof
+ fix i j :: "nat"
+ assume A: "\<And>i. I i \<subseteq> I (Suc i)" and "i \<le> j"
+ then obtain k where k: "j = i + k"
+ using le_Suc_ex by blast
+ have "I i \<subseteq> I (i + k)"
+ by (induction k) (simp_all add: A lift_Suc_mono_le)
+ thus "I i \<subseteq> I j" using k by simp
+next
+ fix i assume "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
+ thus "I i \<subseteq> I (Suc i)" by simp
+qed
+
+
+text \<open>Helper definition for the lemma: trivial_ideal_seq_imp_noetherian\<close>
+fun S_builder :: "_ \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set" where
+ "S_builder R J 0 = {}" |
+ "S_builder R J (Suc n) =
+ (let diff = (J - Idl\<^bsub>R\<^esub> (S_builder R J n)) in
+ (if diff \<noteq> {} then insert (SOME x. x \<in> diff) (S_builder R J n) else (S_builder R J n)))"
+
+lemma S_builder_incl: "S_builder R J n \<subseteq> J"
+ by (induction n) (simp_all, (metis (no_types, lifting) some_eq_ex subsetI))
+
+lemma (in ring) S_builder_const1:
+ assumes "ideal J R" "S_builder R J (Suc n) = S_builder R J n"
+ shows "J = Idl (S_builder R J n)"
+proof -
+ have "J - Idl (S_builder R J n) = {}"
+ proof (rule ccontr)
+ assume "J - Idl (S_builder R J n) \<noteq> {}"
+ hence "S_builder R J (Suc n) = insert (SOME x. x \<in> (J - Idl (S_builder R J n))) (S_builder R J n)"
+ by simp
+ moreover have "(S_builder R J n) \<subseteq> Idl (S_builder R J n)"
+ using S_builder_incl assms(1)
+ by (metis additive_subgroup.a_subset dual_order.trans genideal_self ideal.axioms(1))
+ ultimately have "S_builder R J (Suc n) \<noteq> S_builder R J n"
+ by (metis Diff_iff \<open>J - Idl S_builder R J n \<noteq> {}\<close> insert_subset some_in_eq)
+ thus False using assms(2) by simp
+ qed
+ thus "J = Idl (S_builder R J n)"
+ by (meson S_builder_incl[of R J n] Diff_eq_empty_iff assms(1) genideal_minimal subset_antisym)
+qed
+
+lemma (in ring) S_builder_const2:
+ assumes "ideal J R" "Idl (S_builder R J (Suc n)) = Idl (S_builder R J n)"
+ shows "S_builder R J (Suc n) = S_builder R J n"
+proof (rule ccontr)
+ assume "S_builder R J (Suc n) \<noteq> S_builder R J n"
+ hence A: "J - Idl (S_builder R J n) \<noteq> {}" by auto
+ hence "S_builder R J (Suc n) = insert (SOME x. x \<in> (J - Idl (S_builder R J n))) (S_builder R J n)" by simp
+ then obtain x where x: "x \<in> (J - Idl (S_builder R J n))"
+ and S: "S_builder R J (Suc n) = insert x (S_builder R J n)"
+ using A some_in_eq by blast
+ have "x \<notin> Idl (S_builder R J n)" using x by blast
+ moreover have "x \<in> Idl (S_builder R J (Suc n))"
+ by (metis (full_types) S S_builder_incl additive_subgroup.a_subset
+ assms(1) dual_order.trans genideal_self ideal.axioms(1) insert_subset)
+ ultimately show False using assms(2) by blast
+qed
+
+lemma (in ring) trivial_ideal_seq_imp_noetherian:
+ assumes "\<And>I. \<lbrakk> \<And>i :: nat. ideal (I i) R; \<And>i j. i \<le> j \<Longrightarrow> (I i) \<subseteq> (I j) \<rbrakk> \<Longrightarrow>
+ (\<exists>n. \<forall>k. k \<ge> n \<longrightarrow> I k = I n)"
+ shows "noetherian_ring R"
+proof -
+ have "\<And>J. ideal J R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> J = Idl A"
+ proof -
+ fix J assume J: "ideal J R"
+ define S and I where "S = (\<lambda>i. S_builder R J i)" and "I = (\<lambda>i. Idl (S i))"
+ hence "\<And>i. ideal (I i) R"
+ by (meson J S_builder_incl additive_subgroup.a_subset genideal_ideal ideal.axioms(1) subset_trans)
+ moreover have "\<And>n. S n \<subseteq> S (Suc n)" using S_def by auto
+ hence "\<And>n. I n \<subseteq> I (Suc n)"
+ using S_builder_incl[of R J] J S_def I_def
+ by (meson additive_subgroup.a_subset dual_order.trans ideal.axioms(1) subset_Idl_subset)
+ ultimately obtain n where "\<And>k. k \<ge> n \<Longrightarrow> I k = I n"
+ using assms increasing_set_seq_iff[of I] by (metis lift_Suc_mono_le)
+ hence "J = Idl (S_builder R J n)"
+ using S_builder_const1[OF J, of n] S_builder_const2[OF J, of n] I_def S_def
+ by (meson Suc_n_not_le_n le_cases)
+ moreover have "finite (S_builder R J n)" by (induction n) (simp_all)
+ ultimately show "\<exists>A. A \<subseteq> carrier R \<and> finite A \<and> J = Idl A"
+ by (meson J S_builder_incl ideal.Icarr set_rev_mp subsetI)
+ qed
+ thus ?thesis
+ by (simp add: local.ring_axioms noetherian_ring_axioms_def noetherian_ring_def)
+qed
+
+lemma (in noetherian_domain) wfactors_exists:
+ assumes "x \<in> carrier (mult_of R)"
+ shows "\<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs x" (is "?P x")
+proof (rule ccontr)
+ { fix x
+ assume A: "x \<in> carrier (mult_of R)" "\<not> ?P x"
+ have "\<exists>a. a \<in> carrier (mult_of R) \<and> properfactor (mult_of R) a x \<and> \<not> ?P a"
+ proof -
+ have "\<not> irreducible (mult_of R) x"
+ proof (rule ccontr)
+ assume "\<not> (\<not> irreducible (mult_of R) x)" hence "irreducible (mult_of R) x" by simp
+ hence "wfactors (mult_of R) [ x ] x" unfolding wfactors_def using A by auto
+ thus False using A by auto
+ qed
+ moreover have "\<not> x \<in> Units (mult_of R)"
+ using A monoid.unit_wfactors[OF mult_of.monoid_axioms, of x] by auto
+ ultimately
+ obtain a where a: "a \<in> carrier (mult_of R)" "properfactor (mult_of R) a x" "a \<notin> Units (mult_of R)"
+ unfolding irreducible_def by blast
+ then obtain b where b: "b \<in> carrier (mult_of R)" "x = a \<otimes> b"
+ unfolding properfactor_def by auto
+ hence b_properfactor: "properfactor (mult_of R) b x"
+ using A a mult_of.m_comm mult_of.properfactorI3 by blast
+ have "\<not> ?P a \<or> \<not> ?P b"
+ proof (rule ccontr)
+ assume "\<not> (\<not> ?P a \<or> \<not> ?P b)"
+ then obtain fs_a fs_b
+ where fs_a: "wfactors (mult_of R) fs_a a" "set fs_a \<subseteq> carrier (mult_of R)"
+ and fs_b: "wfactors (mult_of R) fs_b b" "set fs_b \<subseteq> carrier (mult_of R)" by blast
+ hence "wfactors (mult_of R) (fs_a @ fs_b) x"
+ using fs_a fs_b a b mult_of.wfactors_mult by simp
+ moreover have "set (fs_a @ fs_b) \<subseteq> carrier (mult_of R)"
+ using fs_a fs_b by auto
+ ultimately show False using A by blast
+ qed
+ thus ?thesis using a b b_properfactor mult_of.m_comm by blast
+ qed } note aux_lemma = this
+
+ assume A: "\<not> ?P x"
+
+ define f :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "f = (\<lambda>a x. (a \<in> carrier (mult_of R) \<and> properfactor (mult_of R) a x \<and> \<not> ?P a))"
+ define factor_seq :: "nat \<Rightarrow> 'a"
+ where "factor_seq = rec_nat x (\<lambda>n y. (SOME a. f a y))"
+ define I where "I = (\<lambda>i. PIdl (factor_seq i))"
+ have factor_seq_props:
+ "\<And>n. properfactor (mult_of R) (factor_seq (Suc n)) (factor_seq n) \<and>
+ (factor_seq n) \<in> carrier (mult_of R) \<and> \<not> ?P (factor_seq n)" (is "\<And>n. ?Q n")
+ proof -
+ fix n show "?Q n"
+ proof (induct n)
+ case 0
+ have x: "factor_seq 0 = x"
+ using factor_seq_def by simp
+ hence "factor_seq (Suc 0) = (SOME a. f a x)"
+ by (simp add: factor_seq_def)
+ moreover have "\<exists>a. f a x"
+ using aux_lemma[OF assms] A f_def by blast
+ ultimately have "f (factor_seq (Suc 0)) x"
+ using tfl_some by metis
+ thus ?case using f_def A assms x by simp
+ next
+ case (Suc n)
+ have "factor_seq (Suc n) = (SOME a. f a (factor_seq n))"
+ by (simp add: factor_seq_def)
+ moreover have "\<exists>a. f a (factor_seq n)"
+ using aux_lemma f_def Suc.hyps by blast
+ ultimately have Step0: "f (factor_seq (Suc n)) (factor_seq n)"
+ using tfl_some by metis
+ hence "\<exists>a. f a (factor_seq (Suc n))"
+ using aux_lemma f_def by blast
+ moreover have "factor_seq (Suc (Suc n)) = (SOME a. f a (factor_seq (Suc n)))"
+ by (simp add: factor_seq_def)
+ ultimately have Step1: "f (factor_seq (Suc (Suc n))) (factor_seq (Suc n))"
+ using tfl_some by metis
+ show ?case using Step0 Step1 f_def by simp
+ qed
+ qed
+
+ have in_carrier: "\<And>i. factor_seq i \<in> carrier R"
+ using factor_seq_props by simp
+ hence "\<And>i. ideal (I i) R"
+ using I_def by (simp add: cgenideal_ideal)
+
+ moreover
+ have "\<And>i. factor_seq (Suc i) divides factor_seq i"
+ using factor_seq_props unfolding properfactor_def by auto
+ hence "\<And>i. PIdl (factor_seq i) \<subseteq> PIdl (factor_seq (Suc i))"
+ using in_carrier to_contain_is_to_divide by simp
+ hence "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
+ using increasing_set_seq_iff[of I] unfolding I_def by auto
+
+ ultimately obtain n where "\<And>k. n \<le> k \<Longrightarrow> I n = I k"
+ by (metis trivial_ideal_seq)
+ hence "I (Suc n) \<subseteq> I n" by (simp add: equalityD2)
+ hence "factor_seq n divides factor_seq (Suc n)"
+ using in_carrier I_def to_contain_is_to_divide by simp
+ moreover have "\<not> factor_seq n divides\<^bsub>(mult_of R)\<^esub> factor_seq (Suc n)"
+ using factor_seq_props[of n] unfolding properfactor_def by simp
+ hence "\<not> factor_seq n divides factor_seq (Suc n)"
+ using divides_imp_divides_mult[of "factor_seq n" "factor_seq (Suc n)"]
+ in_carrier[of n] factor_seq_props[of "Suc n"] by auto
+ ultimately show False by simp
+qed
+
+
+subsection \<open>Principal Domains\<close>
+
+sublocale principal_domain \<subseteq> noetherian_domain
+proof
+ fix I assume "ideal I R"
+ then obtain i where "i \<in> carrier R" "I = Idl { i }"
+ using principal_I principalideal.generate by blast
+ thus "\<exists>A \<subseteq> carrier R. finite A \<and> I = Idl A" by blast
+qed
+
+lemma (in principal_domain) irreducible_imp_maximalideal:
+ assumes "p \<in> carrier (mult_of R)"
+ and "irreducible (mult_of R) 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 \<noteq> PIdl p"
+ proof (rule ccontr)
+ assume "\<not> carrier R \<noteq> PIdl p"
+ hence "carrier R = PIdl p" by simp
+ then obtain c where "c \<in> carrier R" "\<one> = c \<otimes> p"
+ unfolding cgenideal_def using one_closed by auto
+ hence "p \<in> Units R"
+ unfolding Units_def using assms(1) m_comm by auto
+ thus False
+ using assms unfolding irreducible_def by auto
+ qed
+next
+ fix J assume J: "ideal J R" "PIdl p \<subseteq> J" "J \<subseteq> carrier R"
+ then obtain q where q: "q \<in> carrier R" "J = PIdl q"
+ using principal_I[OF J(1)] cgenideal_eq_rcos is_cring
+ principalideal.rcos_generate by (metis contra_subsetD)
+ hence "q divides p"
+ using to_contain_is_to_divide[of q p] using assms(1) J(1-2) by simp
+ hence q_div_p: "q divides\<^bsub>(mult_of R)\<^esub> p"
+ using assms(1) divides_imp_divides_mult[OF q(1), of p] by (simp add: \<open>q divides p\<close>)
+ show "J = PIdl p \<or> J = carrier R"
+ proof (cases "q \<in> Units R")
+ case True thus ?thesis
+ by (metis J(1) Units_r_inv_ex cgenideal_self ideal.I_r_closed ideal.one_imp_carrier q(1) q(2))
+ next
+ case False
+ have q_in_carr: "q \<in> carrier (mult_of R)"
+ using q_div_p unfolding factor_def using assms(1) q(1) by auto
+ hence "p divides\<^bsub>(mult_of R)\<^esub> q"
+ using q_div_p False assms(2) unfolding irreducible_def properfactor_def by auto
+ hence "p \<sim> q" using q_div_p
+ unfolding associated_def by simp
+ thus ?thesis using associated_iff_same_ideal[of p q] assms(1) q_in_carr q by simp
+ qed
+qed
+
+corollary (in principal_domain) primeness_condition:
+ assumes "p \<in> carrier (mult_of R)"
+ shows "(irreducible (mult_of R) p) \<longleftrightarrow> (prime (mult_of R) p)"
+proof
+ show "irreducible (mult_of R) p \<Longrightarrow> prime (mult_of R) p"
+ using irreducible_imp_maximalideal maximalideal_prime primeideal_iff_prime assms by auto
+next
+ show "prime (mult_of R) p \<Longrightarrow> irreducible (mult_of R) p"
+ using mult_of.prime_irreducible by simp
+qed
+
+lemma (in principal_domain) domain_iff_prime:
+ assumes "a \<in> carrier R - { \<zero> }"
+ shows "domain (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) 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 \<in> carrier R - { \<zero> }"
+ shows "field (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) a"
+proof
+ show "prime (mult_of R) a \<Longrightarrow> 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)) \<Longrightarrow> prime (mult_of R) 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
+ using mult_of.is_comm_monoid_cancel primeness_condition by auto
+
+sublocale principal_domain < mult_of: factorial_monoid "(mult_of R)"
+ rewrites "mult (mult_of R) = mult R"
+ and "one (mult_of R) = one R"
+ apply (rule mult_of.factorial_monoidI)
+ using mult_of.wfactors_unique wfactors_exists mult_of.is_comm_monoid_cancel by auto
+
+sublocale principal_domain \<subseteq> factorial_domain
+ unfolding factorial_domain_def using is_domain mult_of.is_factorial_monoid by simp
+
+lemma (in principal_domain) ideal_sum_iff_gcd:
+ assumes "a \<in> carrier (mult_of R)" "b \<in> carrier (mult_of R)" "d \<in> carrier (mult_of R)"
+ shows "((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl d)) \<longleftrightarrow> (d gcdof\<^bsub>(mult_of R)\<^esub> a b)"
+proof
+ assume A: "(PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl d)" show "d gcdof\<^bsub>(mult_of R)\<^esub> a b"
+ proof -
+ have "(PIdl a) \<subseteq> (PIdl d) \<and> (PIdl b) \<subseteq> (PIdl d)"
+ using assms
+ by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal local.ring_axioms
+ ring.genideal_self ring.oneideal ring.union_genideal A)
+ hence "d divides a \<and> d divides b"
+ using assms apply simp
+ using to_contain_is_to_divide[of d a] to_contain_is_to_divide[of d b] by auto
+ hence "d divides\<^bsub>(mult_of R)\<^esub> a \<and> d divides\<^bsub>(mult_of R)\<^esub> b"
+ using assms by simp
+
+ moreover
+ have "\<And>c. \<lbrakk> c \<in> carrier (mult_of R); c divides\<^bsub>(mult_of R)\<^esub> a; c divides\<^bsub>(mult_of R)\<^esub> b \<rbrakk> \<Longrightarrow>
+ c divides\<^bsub>(mult_of R)\<^esub> d"
+ proof -
+ fix c assume c: "c \<in> carrier (mult_of R)"
+ and "c divides\<^bsub>(mult_of R)\<^esub> a" "c divides\<^bsub>(mult_of R)\<^esub> b"
+ hence "c divides a" "c divides b" by auto
+ hence "(PIdl a) \<subseteq> (PIdl c) \<and> (PIdl b) \<subseteq> (PIdl c)"
+ using to_contain_is_to_divide[of c a] to_contain_is_to_divide[of c b] c assms by simp
+ hence "((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)) \<subseteq> (PIdl c)"
+ using assms c
+ by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
+ Idl_subset_ideal oneideal union_genideal)
+ hence incl: "(PIdl d) \<subseteq> (PIdl c)" using A by simp
+ hence "c divides d"
+ using c assms(3) apply simp
+ using to_contain_is_to_divide[of c d] by blast
+ thus "c divides\<^bsub>(mult_of R)\<^esub> d" using c assms(3) by simp
+ qed
+
+ ultimately show ?thesis unfolding isgcd_def by simp
+ qed
+next
+ assume A:"d gcdof\<^bsub>mult_of R\<^esub> a b" show "PIdl a <+>\<^bsub>R\<^esub> PIdl b = PIdl d"
+ proof
+ have "d divides a" "d divides b"
+ using A unfolding isgcd_def by auto
+ hence "(PIdl a) \<subseteq> (PIdl d) \<and> (PIdl b) \<subseteq> (PIdl d)"
+ using to_contain_is_to_divide[of d a] to_contain_is_to_divide[of d b] assms by simp
+ thus "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl d" using assms
+ by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
+ Idl_subset_ideal oneideal union_genideal)
+ next
+ have "ideal ((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)) R"
+ using assms by (simp add: cgenideal_ideal local.ring_axioms ring.add_ideals)
+ then obtain c where c: "c \<in> carrier R" "(PIdl c) = (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)"
+ using cgenideal_eq_genideal principal_I principalideal.generate by force
+ hence "(PIdl a) \<subseteq> (PIdl c) \<and> (PIdl b) \<subseteq> (PIdl c)" using assms
+ by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
+ genideal_self oneideal union_genideal)
+ hence "c divides a \<and> c divides b" using c(1) assms apply simp
+ using to_contain_is_to_divide[of c a] to_contain_is_to_divide[of c b] by blast
+ hence "c divides\<^bsub>(mult_of R)\<^esub> a \<and> c divides\<^bsub>(mult_of R)\<^esub> b"
+ using assms(1-2) c(1) by simp
+
+ moreover have neq_zero: "c \<noteq> \<zero>"
+ proof (rule ccontr)
+ assume "\<not> c \<noteq> \<zero>" hence "PIdl c = { \<zero> }"
+ using cgenideal_eq_genideal genideal_zero by auto
+ moreover have "\<one> \<otimes> a \<in> PIdl a \<and> \<zero> \<otimes> b \<in> PIdl b"
+ unfolding cgenideal_def using assms one_closed zero_closed by blast
+ hence "(\<one> \<otimes> a) \<oplus> (\<zero> \<otimes> b) \<in> (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)"
+ unfolding set_add_def' by auto
+ hence "a \<in> PIdl c"
+ using c assms by simp
+ ultimately show False
+ using assms(1) by simp
+ qed
+
+ ultimately have "c divides\<^bsub>(mult_of R)\<^esub> d"
+ using A c(1) unfolding isgcd_def by simp
+ hence "(PIdl d) \<subseteq> (PIdl c)"
+ using to_contain_is_to_divide[of c d] c(1) assms(3) by simp
+ thus "PIdl d \<subseteq> PIdl a <+>\<^bsub>R\<^esub> PIdl b" using c by simp
+ qed
+qed
+
+lemma (in principal_domain) bezout_identity:
+ assumes "a \<in> carrier (mult_of R)" "b \<in> carrier (mult_of R)"
+ shows "(PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl (somegcd (mult_of R) a b))"
+proof -
+ have "(somegcd (mult_of R) a b) \<in> carrier (mult_of R)"
+ using mult_of.gcd_exists[OF assms] by simp
+ hence "\<And>x. x = somegcd (mult_of R) a b \<Longrightarrow> (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl x)"
+ using mult_of.gcd_isgcd[OF assms] ideal_sum_iff_gcd[OF assms] by simp
+ thus ?thesis
+ using mult_of.gcd_exists[OF assms] by blast
+qed
+
+
+subsection \<open>Euclidean Domains\<close>
+
+sublocale euclidean_domain \<subseteq> 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" show "principalideal I R"
+ proof (cases "I = { \<zero> }")
+ case True thus ?thesis by (simp add: zeropideal)
+ next
+ case False hence A: "I - { \<zero> } \<noteq> {}"
+ using I additive_subgroup.zero_closed ideal.axioms(1) by auto
+ define phi_img :: "nat set" where "phi_img = (\<phi> ` (I - { \<zero> }))"
+ hence "phi_img \<noteq> {}" using A by simp
+ then obtain m where "m \<in> phi_img" "\<And>k. k \<in> phi_img \<Longrightarrow> m \<le> k"
+ using exists_least_iff[of "\<lambda>n. n \<in> phi_img"] not_less by force
+ then obtain a where a: "a \<in> I - { \<zero> }" "\<And>b. b \<in> I - { \<zero> } \<Longrightarrow> \<phi> a \<le> \<phi> b"
+ using phi_img_def by blast
+ have "I = PIdl a"
+ proof (rule ccontr)
+ assume "I \<noteq> PIdl a"
+ then obtain b where b: "b \<in> I" "b \<notin> PIdl a"
+ using I \<open>a \<in> I - {\<zero>}\<close> cgenideal_minimal by auto
+ hence "b \<noteq> \<zero>"
+ 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 \<in> carrier R" "r \<in> carrier R" "b = (a \<otimes> q) \<oplus> r" "r = \<zero> \<or> \<phi> r < \<phi> a"
+ using euclidean_function[of b a] a(1) b(1) ideal.Icarr[OF I] by auto
+ hence "r = \<zero> \<Longrightarrow> b \<in> PIdl a"
+ unfolding cgenideal_def using m_comm[of a] ideal.Icarr[OF I] a(1) by auto
+ hence 1: "\<phi> r < \<phi> a \<and> r \<noteq> \<zero>"
+ using eucl_div(4) b(2) by auto
+
+ have "r = (\<ominus> (a \<otimes> q)) \<oplus> b"
+ using eucl_div(1-3) a(1) b(1) ideal.Icarr[OF I] r_neg1 by auto
+ moreover have "\<ominus> (a \<otimes> q) \<in> 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 \<in> 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
+qed
+
+sublocale field \<subseteq> euclidean_domain R "\<lambda>_. 0"
+proof (rule euclidean_domainI)
+ fix a b
+ let ?eucl_div = "\<lambda>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = b \<otimes> q \<oplus> r \<and> (r = \<zero> \<or> 0 < 0)"
+ assume a: "a \<in> carrier R - { \<zero> }" and b: "b \<in> carrier R - { \<zero> }"
+ hence "a = b \<otimes> ((inv b) \<otimes> a) \<oplus> \<zero>"
+ by (metis DiffD1 Units_inv_closed Units_r_inv field_Units l_one m_assoc r_zero)
+ hence "?eucl_div _ ((inv b) \<otimes> a) \<zero>"
+ using a b field_Units by auto
+ thus "\<exists>q r. ?eucl_div _ q r"
+ by blast
+qed
+
+end
\ No newline at end of file