src/HOL/Algebra/Ring_Divisibility.thy

 (*  Title:      HOL/Algebra/Ring_Divisibility.thy
     Author:     Paulo Emílio de Vilhena
 *)
 
 theory Ring_Divisibility
-imports Ideal Divisibility QuotRing
+imports Ideal Divisibility QuotRing Multiplicative_Group HOL.Zorn
+
 begin
 
-section \<open>Definitions ported from @{text "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"
+  assumes finetely_gen: "ideal I R \<Longrightarrow> \<exists>A \<subseteq> carrier R. 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 exists_gen: "ideal I R \<Longrightarrow> \<exists>a \<in> carrier R. I = PIdl a"
+
+locale euclidean_domain = 
+  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)"
+definition ring_irreducible :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> bool" ("ring'_irreducible\<index>")
+  where "ring_irreducible\<^bsub>R\<^esub> a \<longleftrightarrow> (a \<noteq> \<zero>\<^bsub>R\<^esub>) \<and> (irreducible R a)"
+
+definition ring_prime :: "('a, 'b) ring_scheme \<Rightarrow> 'a \<Rightarrow> bool" ("ring'_prime\<index>")
+  where "ring_prime\<^bsub>R\<^esub> a \<longleftrightarrow> (a \<noteq> \<zero>\<^bsub>R\<^esub>) \<and> (prime R a)"
+
+
+subsection \<open>The cancellative monoid of a domain. \<close>
+
+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" ..
+       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"
+       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>Passing from R to mult_of R and vice-versa. \<close>
+
+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 (in cring) divides_one:
+  assumes "a \<in> carrier R"
+  shows "a divides \<one> \<longleftrightarrow> a \<in> Units R"
+  using assms m_comm unfolding factor_def Units_def by force 
+
+lemma (in ring) one_divides:
+  assumes "a \<in> carrier R" shows "\<one> divides a"
+  using assms unfolding factor_def by simp
+
+lemma (in ring) divides_zero:
+  assumes "a \<in> carrier R" shows "a divides \<zero>"
+  using r_null[OF assms] unfolding factor_def by force
+
+lemma (in ring) zero_divides:
+  shows "\<zero> divides a \<longleftrightarrow> a = \<zero>"
+  unfolding factor_def by auto
+
+lemma (in domain) divides_mult_zero:
+  assumes "a \<in> carrier R" shows "a divides\<^bsub>(mult_of R)\<^esub> \<zero> \<Longrightarrow> a = \<zero>"
+  using integral[OF _ assms] unfolding factor_def by auto
+
+lemma (in ring) divides_mult:
+  assumes "a \<in> carrier R" "c \<in> carrier R"
+  shows "a divides b \<Longrightarrow> (c \<otimes> a) divides (c \<otimes> b)"
+  using m_assoc[OF assms(2,1)] unfolding factor_def by auto 
+
+lemma (in domain) mult_divides:
+  assumes "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R - { \<zero> }"
+  shows "(c \<otimes> a) divides (c \<otimes> b) \<Longrightarrow> 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 \<in> carrier R" and "b \<in> carrier R"
+  shows "a \<sim> b \<longleftrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+proof
+  assume "a \<sim>\<^bsub>(mult_of R)\<^esub> b" thus "a \<sim> b"
+    unfolding associated_def factor_def by auto
+next
+  assume A: "a \<sim> b"
+  then obtain c1 c2
+    where c1: "c1 \<in> carrier R" "a = b \<otimes> c1" and c2: "c2 \<in> carrier R" "b = a \<otimes> c2"
+    unfolding associated_def factor_def by auto
+  show "a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+  proof (cases "a = \<zero>")
+    assume a: "a = \<zero>" then have b: "b = \<zero>"
+      using c2 by auto
+    show ?thesis
+      unfolding associated_def factor_def a b by auto
+  next
+    assume a: "a \<noteq> \<zero>"
+    hence b: "b \<noteq> \<zero>" and c1_not_zero: "c1 \<noteq> \<zero>"
+      using c1 assms by auto
+    hence c2_not_zero: "c2 \<noteq> \<zero>"
+      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 \<in> carrier R" "b \<in> carrier R"
+  shows "a \<sim> b \<longleftrightarrow> (\<exists>u \<in> Units R. a = u \<otimes> b)"
+proof (cases "a = \<zero>")
+  assume [simp]: "a = \<zero>" show ?thesis
+  proof
+    assume "a \<sim> b" thus "\<exists>u \<in> Units R. a = u \<otimes> b"
+      using zero_divides unfolding associated_def by force
+  next
+    assume "\<exists>u \<in> Units R. a = u \<otimes> b" then have "b = \<zero>"
+      by (metis Units_closed Units_l_cancel \<open>a = \<zero>\<close> assms r_null)
+    thus "a \<sim> b"
+      using zero_divides[of \<zero>] by auto
+  qed
+next
+  assume a: "a \<noteq> \<zero>" show ?thesis
+  proof (cases "b = \<zero>")
+    assume "b = \<zero>" thus ?thesis
+      using assms a zero_divides[of a] r_null unfolding associated_def by blast
+  next
+    assume b: "b \<noteq> \<zero>"
+    have "(\<exists>u \<in> Units R. a = u \<otimes> b) \<longleftrightarrow> (\<exists>u \<in> Units R. a = b \<otimes> 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:
+  "\<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) properfactor_of_zero:
+  assumes "b \<in> carrier R"
+  shows "\<not> properfactor (mult_of R) b \<zero>" and "properfactor R b \<zero> \<longleftrightarrow> b \<noteq> \<zero>"
+  using divides_mult_zero[OF assms] divides_zero[OF assms] unfolding properfactor_def by auto
+
+
+subsection \<open>Irreducible\<close>
+
+text \<open>The following lemmas justify the need for a definition of irreducible specific to rings:
+      for "irreducible R", we need to suppose we are not in a field (which is plausible,
+      but "\<not> field R" is an assumption we want to avoid; for "irreducible (mult_of R)", zero
+      is allowed. \<close>
+
+lemma (in domain) zero_is_irreducible_mult:
+  shows "irreducible (mult_of R) \<zero>"
+  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 \<zero> \<longleftrightarrow> field R"
+proof
+  assume irr: "irreducible R \<zero>"
+  have "\<And>a. \<lbrakk> a \<in> carrier R; a \<noteq> \<zero> \<rbrakk> \<Longrightarrow> properfactor R a \<zero>"
+    unfolding properfactor_def factor_def by (auto, metis r_null zero_closed)
+  hence "carrier R - { \<zero> } = 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 \<zero>"
+    using field.field_Units[OF field]
+    unfolding irreducible_def properfactor_def factor_def by blast
+qed
+
+lemma (in domain) irreducible_imp_irreducible_mult:
+  "\<lbrakk> a \<in> carrier R; irreducible R a \<rbrakk> \<Longrightarrow> irreducible (mult_of R) a"
+  using zero_is_irreducible_mult Units_mult_eq_Units properfactor_mult_imp_properfactor
+  by (cases "a = \<zero>") (auto simp add: irreducible_def)
+
+lemma (in domain) irreducible_mult_imp_irreducible:
+  "\<lbrakk> a \<in> carrier R - { \<zero> }; irreducible (mult_of R) a \<rbrakk> \<Longrightarrow> irreducible R a"
+    unfolding irreducible_def using properfactor_imp_properfactor_mult properfactor_divides by fastforce
+
+lemma (in domain) ring_irreducibleE:
+  assumes "r \<in> carrier R" and "ring_irreducible r"
+  shows "r \<noteq> \<zero>" "irreducible R r" "irreducible (mult_of R) r" "r \<notin> Units R"
+    and "\<And>a b. \<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> r = a \<otimes> b \<Longrightarrow> a \<in> Units R \<or> b \<in> 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 \<noteq> \<zero>" "r \<notin> Units R"
+    using assms unfolding ring_irreducible_def irreducible_def by auto
+next
+  fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and r: "r = a \<otimes> b"
+  show "a \<in> Units R \<or> b \<in> 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: "\<not> properfactor R a r"
+    hence "r divides a"
+      using r b unfolding properfactor_def by auto
+    then obtain c where c: "c \<in> carrier R" "a = r \<otimes> c"
+      unfolding factor_def by auto
+    have "\<one> = c \<otimes> 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 \<in> carrier R - { \<zero> }" "r \<notin> Units R"
+    and "\<And>a b. \<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> r = a \<otimes> b \<Longrightarrow> a \<in> Units R \<or> b \<in> Units R"
+  shows "ring_irreducible r"
+  unfolding ring_irreducible_def
+proof
+  show "r \<noteq> \<zero>" using assms(1) by blast
+next
+  show "irreducible R r"
+  proof (rule irreducibleI[OF assms(2)])
+    fix a assume a: "a \<in> carrier R" "properfactor R a r"
+    then obtain b where b: "b \<in> carrier R" "r = a \<otimes> b"
+      unfolding properfactor_def factor_def by blast
+    hence "a \<in> Units R \<or> b \<in> Units R"
+      using assms(3)[OF a(1) b(1)] by simp
+    thus "a \<in> Units R"
+    proof (auto)
+      assume "b \<in> Units R"
+      hence "r \<otimes> inv b = a" and "inv b \<in> 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 \<in> carrier R - { \<zero> }" "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 \<open>Primes\<close>
+
+lemma (in domain) zero_is_prime: "prime R \<zero>" "prime (mult_of R) \<zero>"
+  using integral unfolding prime_def factor_def Units_def by auto
+
+lemma (in domain) prime_eq_prime_mult:
+  assumes "p \<in> carrier R"
+  shows "prime R p \<longleftrightarrow> prime (mult_of R) p"
+proof (cases "p = \<zero>", auto simp add: zero_is_prime)
+  assume "p \<noteq> \<zero>" "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 \<noteq> \<zero>" "prime (mult_of R) p" show "prime R p"
+  proof (rule primeI)
+    show "p \<notin> Units R"
+      using p(2) Units_mult_eq_Units unfolding prime_def by simp
+  next
+    fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and dvd: "p divides a \<otimes> b"
+    then obtain c where c: "c \<in> carrier R" "a \<otimes> b = p \<otimes> c"
+      unfolding factor_def by auto
+    show "p divides a \<or> p divides b"
+    proof (cases "a \<otimes> b = \<zero>")
+      case True thus ?thesis
+        using integral[OF _ a b] c unfolding factor_def by force
+    next
+      case False
+      hence "p divides\<^bsub>(mult_of R)\<^esub> (a \<otimes> b)"
+        using divides_imp_divides_mult[OF assms _ dvd] m_closed[OF a b] by simp
+      moreover have "a \<noteq> \<zero>" "b \<noteq> \<zero>" "c \<noteq> \<zero>"
+        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 \<in> carrier R" "ring_prime p"
+  shows "p \<noteq> \<zero>" "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 \<noteq> \<zero>" "prime R p" shows "ring_prime p"
+  using assms unfolding ring_prime_def by auto
+
+lemma (in domain) ring_primeI':
+  assumes "p \<in> carrier R - { \<zero> }" "prime (mult_of R) p"
+  shows "ring_prime p"
+  using assms prime_eq_prime_mult unfolding ring_prime_def by 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)"
+  shows "PIdl b \<subseteq> PIdl a \<longleftrightarrow> 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"

   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)"
+  shows "a \<sim> b \<longleftrightarrow> 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"
+        to_contain_is_to_divide[OF assms(2,1)] by auto
+
+lemma (in cring) ideal_eq_carrier_iff:
+  assumes "a \<in> carrier R"
+  shows "carrier R = PIdl a \<longleftrightarrow> a \<in> Units R"
+proof
+  assume "carrier R = PIdl a"
+  hence "\<one> \<in> PIdl a"
+    by auto
+  then obtain b where "b \<in> carrier R" "\<one> = a \<otimes> b" "\<one> = b \<otimes> a"
+    unfolding cgenideal_def using m_comm[OF assms] by auto
+  thus "a \<in> Units R"
+    using assms unfolding Units_def by auto
+next
+  assume "a \<in> Units R"
+  then have inv_a: "inv a \<in> carrier R" "inv a \<otimes> a = \<one>"
+    by auto
+  have "carrier R \<subseteq> PIdl a"
+  proof
+    fix b assume "b \<in> carrier R"
+    hence "(b \<otimes> inv a) \<otimes> a = b" and "b \<otimes> inv a \<in> carrier R"
+      using m_assoc[OF _ inv_a(1) assms] inv_a by auto
+    thus "b \<in> 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 \<in> carrier R - { \<zero> }"
+  shows "primeideal (PIdl p) R \<longleftrightarrow> ring_prime p"
+proof 
+  assume PIdl: "primeideal (PIdl p) R" show "ring_prime p"
+  proof (rule ring_primeI)
+    show "p \<noteq> \<zero>" using assms by simp
+  next
+    show "prime R p"
+    proof (rule primeI)
+      show "p \<notin> Units R"
+        using ideal_eq_carrier_iff[of p] assms primeideal.I_notcarr[OF PIdl] by auto
+    next
+      fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and dvd: "p divides a \<otimes> b"
+      hence "a \<otimes> b \<in> PIdl p"
+        by (meson assms DiffD1 cgenideal_self contra_subsetD m_closed to_contain_is_to_divide)
+      hence "a \<in> PIdl p \<or> b \<in> PIdl p"
+        using primeideal.I_prime[OF PIdl a b] by simp
+      thus "p divides a \<or> 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 \<in> carrier R" and "carrier R \<noteq> 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 \<in> carrier R" and b: "b \<in> carrier R" "a \<otimes> b \<in> PIdl p"
+    hence "p divides a \<otimes> b"
+      using assms Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
+    hence "p divides a \<or> p divides b"
+      using a b assms primeE[OF ring_primeE(3)[OF _ prime]] by auto
+    thus "a \<in> PIdl p \<or> b \<in> PIdl p"
+      using a b assms Idl_subset_ideal' cgenideal_eq_genideal to_contain_is_to_divide by auto
+  qed
+qed
+
+
+subsection \<open>Noetherian Rings\<close>
+
+lemma (in ring) chain_Union_is_ideal:
+  assumes "subset.chain { I. ideal I R } C"
+  shows "ideal (if C = {} then { \<zero> } else (\<Union>C)) R"
+proof (cases "C = {}")
+  case True thus ?thesis by (simp add: zeroideal) 
+next
+  case False have "ideal (\<Union>C) R"
+  proof (rule idealI[OF ring_axioms])
+    show "subgroup (\<Union>C) (add_monoid R)"
+    proof
+      show "\<Union>C \<subseteq> 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 \<in> C" "ideal I R"
+        using False assms unfolding pred_on.chain_def by auto
+      thus "\<one>\<^bsub>add_monoid R\<^esub> \<in> \<Union>C"
+        using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF I(2)]] by auto
+    next
+      fix x y assume "x \<in> \<Union>C" "y \<in> \<Union>C"
+      then obtain I where I: "I \<in> C" "x \<in> I" "y \<in> 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 \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> \<Union>C"
+        using UnionI I additive_subgroup.a_closed unfolding ideal_def by fastforce 
+
+      show "inv\<^bsub>add_monoid R\<^esub> x \<in> \<Union>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 \<in> \<Union>C" and x: "x \<in> carrier R"
+    then obtain I where I: "ideal I R" "a \<in> I" and "I \<in> C"
+      using assms unfolding pred_on.chain_def by auto
+    thus "x \<otimes> a \<in> \<Union>C" and "a \<otimes> x \<in> \<Union>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 \<noteq> {}" "subset.chain { I. ideal I R } C"
+  shows "\<Union>C \<in> C"
 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>"
+  { fix S assume "finite S" "S \<subseteq> \<Union>C"
+    hence "\<exists>I. I \<in> C \<and> S \<subseteq> I"
+    proof (induct S)
+      case empty thus ?case
+        using assms(1) by blast
+    next
+      case (insert s S)
+      then obtain I where I: "I \<in> C" "S \<subseteq> I"
+        by blast
+      moreover obtain I' where I': "I' \<in> C" "s \<in> I'"
+        using insert(4) by blast
+      ultimately have "I \<subseteq> I' \<or> I' \<subseteq> 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 \<subseteq> carrier R" "\<Union>C = Idl S"
+    using finetely_gen[OF chain_Union_is_ideal[OF assms(2)]] assms(1) by auto
+  then obtain I where I: "I \<in> C" and "S \<subseteq> I"
+    using aux_lemma[OF S(1)] genideal_self[OF S(2)] by blast
+  hence "Idl S \<subseteq> I"
+    using assms unfolding pred_on.chain_def
+    by (metis genideal_minimal mem_Collect_eq rev_subsetD)
+  hence "\<Union>C = I"
+    using S(3) I by auto
+  thus ?thesis
+    using I by simp
+qed
+
+lemma (in ring) trivial_ideal_chain_imp_noetherian:
+  assumes "\<And>C. \<lbrakk> C \<noteq> {}; subset.chain { I. ideal I R } C \<rbrakk> \<Longrightarrow> \<Union>C \<in> C"
+  shows "noetherian_ring R"
+proof (auto simp add: noetherian_ring_def noetherian_ring_axioms_def ring_axioms)
+  fix I assume I: "ideal I R"
+  have in_carrier: "I \<subseteq> 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' \<subseteq> I \<and> finite S' }"
+  have "\<exists>M \<in> S. \<forall>S' \<in> S. M \<subseteq> S' \<longrightarrow> S' = M"
+  proof (rule subset_Zorn)
+    fix C assume C: "subset.chain S C"
+    show "\<exists>U \<in> S. \<forall>S' \<in> C. S' \<subseteq> U"
+    proof (cases "C = {}")
+      case True
+      have "{ \<zero> } \<in> 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 \<subseteq> { 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 "\<Union>C \<in> 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 \<in> S" "\<And>S'. \<lbrakk>S' \<in> S; M \<subseteq> S' \<rbrakk> \<Longrightarrow> S' = M"
+    by auto
+  then obtain S' where S': "S' \<subseteq> I" "finite S'" "M = Idl S'"
+    by (auto simp add: S_def)
+  hence "M \<subseteq> I"
+    using I genideal_minimal by (auto simp add: S_def)
+  moreover have "I \<subseteq> M"
   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 cginideal_def' by (metis (no_types, lifting) image_iff one_closed)
-      hence "p \<in> Units R" unfolding Units_def using m_comm assms by auto
-      thus False using A unfolding prime_def by simp
+    assume "\<not> I \<subseteq> M"
+    then obtain a where a: "a \<in> I" "a \<notin> M"
+      by auto
+    have "M \<subseteq> 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') \<in> 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 \<in> M"
+      using genideal_self S'(1) a (1) in_carrier by (meson insert_subset subset_trans)
+    from \<open>a \<in> M\<close> and \<open>a \<notin> M\<close> show False by simp
+  qed
+  ultimately have "M = I" by simp
+  thus "\<exists>A \<subseteq> carrier R. finite A \<and> I = Idl A"
+    using S' in_carrier by blast
+qed
+
+lemma (in noetherian_domain) factorization_property:
+  assumes "a \<in> carrier R - { \<zero> }" "a \<notin> Units R"
+  shows "\<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs a" (is "?factorizable a")
+proof (rule ccontr)
+  assume a: "\<not> ?factorizable a"
+  define S where "S = { PIdl r | r. r \<in> carrier R - { \<zero> } \<and> r \<notin> Units R \<and> \<not> ?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 \<subseteq> { 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 \<in> 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 \<noteq> {}"
+    using C unfolding pred_on.maxchain_def by auto
+  ultimately have "\<Union>C \<in> C"
+    using ideal_chain_is_trivial by simp
+  hence "\<Union>C \<in> S"
+    using chain unfolding pred_on.chain_def by auto 
+  then obtain r where r: "\<Union>C = PIdl r" "r \<in> carrier R - { \<zero> }" "r \<notin> Units R" "\<not> ?factorizable r"
+    by (auto simp add: S_def)
+  have "\<exists>p. p \<in> carrier R - { \<zero> } \<and> p \<notin> Units R \<and> \<not> ?factorizable p \<and> p divides r \<and> \<not> 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 "\<not> irreducible (mult_of R) r"
+      using r(2,4) by auto
+    hence "\<not> ring_irreducible r"
+      using ring_irreducibleE(3) r(2) by auto
+    then obtain p1 p2
+      where p1_p2: "p1 \<in> carrier R" "p2 \<in> carrier R" "r = p1 \<otimes> p2" "p1 \<notin> Units R" "p2 \<notin> Units R"
+      using ring_irreducibleI[OF r(2-3)] by auto
+    hence in_carrier: "p1 \<in> carrier (mult_of R)" "p2 \<in> carrier (mult_of R)"
+      using r(2) by auto
+
+    have "\<lbrakk> ?factorizable p1; ?factorizable p2 \<rbrakk> \<Longrightarrow> ?factorizable r"
+      using mult_of.wfactors_mult[OF _ _ in_carrier] p1_p2(3) by (metis le_sup_iff set_append)
+    hence "\<not> ?factorizable p1 \<or> \<not> ?factorizable p2"
+      using r(4) by auto
+
+    moreover
+    have "\<And>p1 p2. \<lbrakk> p1 \<in> carrier R; p2 \<in> carrier R; r = p1 \<otimes> p2; r divides p1 \<rbrakk> \<Longrightarrow> p2 \<in> Units R"
+    proof -
+      fix p1 p2 assume A: "p1 \<in> carrier R" "p2 \<in> carrier R" "r = p1 \<otimes> p2" "r divides p1"
+      then obtain c where c: "c \<in> carrier R" "p1 = r \<otimes> c"
+        unfolding factor_def by blast
+      hence "\<one> = c \<otimes> p2"
+        using A m_lcancel[OF _ _ one_closed, of r "c \<otimes> p2"] r(2) by (auto, metis m_assoc m_closed)
+      thus "p2 \<in> Units R"
+        unfolding Units_def using c A(2) m_comm[OF c(1) A(2)] by auto
     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 proofs below\<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
+    hence "\<not> r divides p1" and "\<not> 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 \<in> carrier R - { \<zero> }" "p \<notin> Units R" "\<not> ?factorizable p" "p divides r" "\<not> r divides p"
+    by blast
+  hence "PIdl p \<in> S"
+    unfolding S_def by auto
+  moreover have "\<Union>C \<subset> 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 \<subset> (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
 
 
 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
+    using exists_gen cgenideal_eq_genideal by auto
+  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"
+  assumes "p \<in> 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 \<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
+    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 \<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)
+    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
-  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
+  then obtain r where r: "r \<in> carrier R" "p = q \<otimes> r"
+    unfolding factor_def by auto
+  hence "q \<in> Units R \<or> r \<in> Units R"
+    using ring_irreducibleE(5)[OF assms q(1)] by auto
+  thus "J = PIdl p \<or> J = carrier R"
+  proof
+    assume "q \<in> Units R" thus ?thesis
+      using ideal_eq_carrier_iff[OF q(1)] q(2) by auto
+  next
+    assume "r \<in> Units R" hence "p \<sim> 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 \<in> carrier (mult_of R)"
-  shows "(irreducible (mult_of R) p) \<longleftrightarrow> (prime (mult_of R) p)"
+  assumes "p \<in> carrier R"
+  shows "ring_irreducible p \<longleftrightarrow> ring_prime 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
+  show "ring_irreducible p \<Longrightarrow> ring_prime p"
+    using maximalideal_prime[OF irreducible_imp_maximalideal] ring_irreducibleE(1)
+          primeideal_iff_prime assms by auto 
+next
+  show "ring_prime p \<Longrightarrow> 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 \<in> carrier R - { \<zero> }"
-  shows "domain (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) a"
+  shows "domain (R Quot (PIdl a)) \<longleftrightarrow> 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 \<in> carrier R - { \<zero> }"
-  shows "field (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) a"
+  shows "field (R Quot (PIdl a)) \<longleftrightarrow> ring_prime a"
 proof
-  show "prime (mult_of R) a \<Longrightarrow> field  (R Quot (PIdl a))"
+  show "ring_prime 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"
+  show "field  (R Quot (PIdl a)) \<Longrightarrow> 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)"
+
+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)"
+    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 \<in> carrier R" "a \<noteq> \<zero>" "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"
-  apply (rule mult_of.factorial_monoidI)
-  using mult_of.wfactors_unique wfactors_exists mult_of.is_comm_monoid_cancel by auto
+  using mult_of.wfactors_unique factorization_property mult_of.is_comm_monoid_cancel
+  by (auto intro!: mult_of.factorial_monoidI)
 
 sublocale principal_domain \<subseteq> factorial_domain
-  unfolding factorial_domain_def using is_domain mult_of.is_factorial_monoid by simp
+  unfolding factorial_domain_def using domain_axioms mult_of.factorial_monoid_axioms 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"
+  assumes "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
+  shows "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b \<longleftrightarrow> d gcdof a b"
+proof -
+  { fix a b d
+    assume in_carrier: "a \<in> carrier R" "b \<in> carrier R" "d \<in> carrier R"
+       and ideal_eq: "PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl b"
+    have "d gcdof a b"
+    proof (auto simp add: isgcd_def)
+      have "a \<in> PIdl d" and "b \<in> 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 \<in> carrier R" "c divides a" "c divides b"
+      hence "PIdl a \<subseteq> PIdl c" and "PIdl b \<subseteq> PIdl c"
+        using to_contain_is_to_divide in_carrier by auto
+      hence "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> 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 <+>\<^bsub>R\<^esub> PIdl b \<Longrightarrow> d gcdof a b"
+    using aux_lemma assms by simp
+
+  moreover
+  have "d gcdof a b \<Longrightarrow> PIdl d = PIdl a <+>\<^bsub>R\<^esub> PIdl 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
+    assume d: "d gcdof a b"
+    obtain c where c: "c \<in> carrier R" "PIdl c = PIdl a <+>\<^bsub>R\<^esub> 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 \<open>d gcdof a b\<close> and \<open>c gcdof a b\<close> have "d \<sim> 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 \<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))"
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "PIdl a <+>\<^bsub>R\<^esub> PIdl b = PIdl (somegcd 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
+  have "\<exists>d \<in> 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 mult_of.gcd_exists[OF assms] by blast
-qed
-
+    using ideal_sum_iff_gcd[OF assms(1-2)] somegcd_def
+    by (metis (no_types, lifting) tfl_some)
+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"
+  fix I assume I: "ideal I R" have "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 

         using a(2) by fastforce
     qed
     thus ?thesis
       by (meson DiffD1 I cgenideal_is_principalideal ideal.Icarr local.a(1))
   qed
-qed
+  thus "\<exists>a \<in> carrier R. I = PIdl a"
+    by (simp add: cgenideal_eq_genideal principalideal.generate)
+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