src/HOL/Algebra/Ring_Divisibility.thy

merged

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

theory Ring_Divisibility
imports Ideal Divisibility QuotRing
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"

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