Theory Rings2

(*
    Title:      Rings2.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

section‹Rings›

theory Rings2
imports
   "HOL-Analysis.Analysis"
   "HOL-Computational_Algebra.Polynomial_Factorial"
begin

subsection‹Previous lemmas and results›

lemma chain_le:
  fixes I::"nat => 'a set"
  assumes inc: "∀n. I(n) ⊆ I(n+1)"
  shows "∀n≤m. I(n) ⊆ I(m)"
  using assms
proof (induct m)
  case 0
  show ?case by auto
next
  case (Suc m)
  show ?case by (metis Suc_eq_plus1 inc lift_Suc_mono_le)
qed

context Rings.ring
begin

lemma sum_add:
  assumes A: "finite A"
  and B: "finite B"
  shows "sum f A + sum g B = sum f (A - B) + sum g (B - A) + sum (λx. f x + g x) (A ∩ B)"
proof -
  have 1: "sum f A = sum f (A - B) + sum f (A ∩ B)"
    by (metis A Int_Diff_disjoint Un_Diff_Int finite_Diff finite_Int inf_sup_aci(1) local.sum.union_disjoint)
  have 2: "sum g B = sum g (B - A) + sum g (A ∩ B)"
    by (metis B Int_Diff_disjoint Int_commute Un_Diff_Int finite_Diff finite_Int local.sum.union_disjoint)
  have 3: "sum f (A ∩ B) + sum g (A ∩ B) = sum (λx. f x + g x) (A ∩ B)"
    by (simp add: sum.distrib)
  show ?thesis
    by (simp add: "1" "2" "3" add.assoc add.left_commute)
qed

text‹This lemma is presented in the library but for additive abelian groups›

lemma sum_negf:
  "sum (%x. - (f x)::'a) A = - sum f A"
proof (cases "finite A")
  case True thus ?thesis by (induct set: finite) auto
next
  case False thus ?thesis by simp
qed


text‹The following lemmas are presented in the library but for other type classes (semiring\_0)›

lemma sum_distrib_left:
  shows "r * sum f A = sum (%n. r * f n) A"
proof (cases "finite A")
  case True
  thus ?thesis
  proof induct
    case empty thus ?case by simp
  next
    case (insert x A) thus ?case by (simp add: distrib_left)
  qed
next
  case False thus ?thesis by simp
qed

lemma sum_distrib_right:
  "sum f A * r = (∑n∈A. f n * r)"
proof (cases "finite A")
  case True
  then show ?thesis
  proof induct
    case empty thus ?case by simp
  next
    case (insert x A) thus ?case by (simp add: distrib_right)
  qed
next
  case False thus ?thesis by simp
qed

end


context comm_monoid_add
begin

lemma sum_two_elements:
  assumes "a ≠ b"
  shows "sum f {a,b} = f a + f b"
  by (metis Diff_cancel assms empty_Diff finite.emptyI infinite_remove add_0_right
    sum.empty sum.insert sum.insert_remove singletonD)

lemma sum_singleton: "sum f {x} = f x"
  by simp

end

subsection‹Subgroups›

context group_add
begin
definition "subgroup A ≡ (0 ∈ A ∧ (∀a∈A. ∀b ∈ A. a + b ∈ A) ∧ (∀a∈A. -a ∈ A))"

lemma subgroup_0: "subgroup {0}"
  unfolding subgroup_def by auto

lemma subgroup_UNIV: "subgroup (UNIV)"
  unfolding subgroup_def by auto

lemma subgroup_inter:
  assumes "subgroup A" and "subgroup B"
  shows "subgroup (A ∩ B)"
  using assms unfolding subgroup_def by blast

lemma subgroup_Inter:
  assumes "∀I∈S. subgroup I"
  shows "subgroup (⋂S)"
  using assms unfolding subgroup_def by auto

lemma subgroup_Union:
  fixes I::"nat => 'a set"
  defines S: "S≡{I n|n. n∈UNIV}"
  assumes all_subgroup: "∀A∈S. subgroup A"
  and inc: "∀n. I(n) ⊆ I(n+1)"
  shows "subgroup (⋃S)"
unfolding subgroup_def
proof (safe; (unfold Union_iff)?)
  show "∃X∈S. 0 ∈ X"
  proof (rule bexI[of _ "I 0"])
    show "I 0 ∈ S" unfolding S by auto
    thus "0 ∈ I 0" using all_subgroup unfolding subgroup_def by auto
  qed
  fix y a ya b assume y: "y ∈ S" and a: "a ∈ y" and ya: "ya ∈ S" and b: "b ∈ ya"
  obtain n m where In: "y=I n" and Im: "ya = I m" using y ya S by auto
  have In_I_max:"I n ⊆ I (max n m)" using chain_le[OF inc] by auto
  have Im_I_max:"I m ⊆ I (max n m)" using chain_le[OF inc] by auto
  show "∃x∈S. a + b ∈ x"
  proof (rule bexI[of _ "I (max n m)"])
    show "a + b ∈ I (max n m)"
      by (metis Im Im_I_max In In_I_max a all_subgroup b in_mono max_def subgroup_def y ya)
    show "I (max n m) ∈ S" using S by auto
  qed
  show "∃x∈S. - a ∈ x"
  proof (rule bexI[of _ "I (max n m)"])
    show "- a ∈ I (max n m)" by (metis In In_I_max a all_subgroup in_mono subgroup_def y)
    show "I (max n m) ∈ S" using S by auto
  qed
qed



end

subsection‹Ideals›

context Rings.ring
begin

lemma subgroup_left_principal_ideal: "subgroup {r*a|r. r∈UNIV}"
proof (unfold subgroup_def, auto)
  show "∃r. 0 = r * a" by (rule exI[of _ 0], simp)
  fix r ra show "∃rb. r * a + ra * a = rb * a"
    by (metis add_0_right combine_common_factor)
  show "∃ra. - (r * a) = ra * a" by (metis minus_mult_left)
qed


definition "left_ideal I = (subgroup I ∧ (∀x∈I. ∀r. r*x ∈ I))"
definition "right_ideal I = (subgroup I ∧ (∀x∈I. ∀r. x*r ∈ I))"
definition "ideal I= (left_ideal I ∧ right_ideal I)"

definition "left_ideal_generated S = ⋂{I. left_ideal I ∧ S ⊆ I}"
definition "right_ideal_generated S = ⋂{I. right_ideal I ∧ S ⊆ I}"
definition "ideal_generated S = ⋂{I. ideal I ∧ S ⊆ I}"

definition "left_principal_ideal S =  (∃a. left_ideal_generated {a} = S)"
definition "right_principal_ideal S = (right_ideal S ∧ (∃a. right_ideal_generated {a} = S))"
definition "principal_ideal S = (∃a. ideal_generated {a} = S)"

lemma ideal_inter:
  assumes "ideal I" and "ideal J" shows "ideal (I ∩ J)"
  using assms
  unfolding ideal_def left_ideal_def right_ideal_def subgroup_def
  by auto

lemma ideal_Inter:
  assumes "∀I∈S. ideal I"
  shows "ideal (⋂S)"
proof (unfold ideal_def left_ideal_def right_ideal_def, auto)
  show "subgroup (⋂S)" and "subgroup (⋂S)"
    using subgroup_Inter assms
    unfolding ideal_def left_ideal_def by auto
  fix x r xa assume X: "∀X∈S. x ∈ X" and xa: "xa ∈ S"
  show "r * x ∈ xa" by (metis X assms ideal_def left_ideal_def xa)
next
  fix x r xa assume X: "∀X∈S. x ∈ X" and xa: "xa ∈ S"
  show "x * r ∈ xa" by (metis X assms ideal_def right_ideal_def xa)
qed


lemma ideal_Union:
  fixes I::"nat => 'a set"
  defines S: "S≡{I n|n. n∈UNIV}"
  assumes all_ideal: "∀A∈S. ideal A"
  and inc: "∀n. I(n) ⊆ I(n+1)"
  shows "ideal (⋃S)"
unfolding ideal_def left_ideal_def right_ideal_def
proof (safe; (unfold Union_iff)?)
  fix y x r
  assume y: "y ∈ S" and x: "x ∈ y"
  obtain n where n: "y=I n" using y S by auto
  show "∃xa∈S. r * x ∈ xa"
  proof (rule bexI[of _ "I n"])
    show "r * x ∈ I n" by (metis n assms(2) ideal_def left_ideal_def x y)
    show "I n ∈ S" by (metis n y)
  qed
  show "∃xa∈S. x * r ∈ xa"
  proof (rule bexI[of _ "I n"])
    show "x * r ∈ I n" by (metis n assms(2) ideal_def right_ideal_def x y)
    show "I n ∈ S" by (metis n y)
  qed
next
  show "subgroup (⋃S)" and "subgroup (⋃S)"
    using subgroup_Union
    by (metis (mono_tags) S all_ideal ideal_def inc right_ideal_def)+
qed



lemma ideal_not_empty:
  assumes "ideal I"
  shows "I ≠ {}"
  using assms unfolding ideal_def left_ideal_def subgroup_def by auto

lemma ideal_0: "ideal {0}"
  unfolding ideal_def left_ideal_def right_ideal_def using subgroup_0 by auto

lemma ideal_UNIV: "ideal UNIV"
  unfolding ideal_def left_ideal_def right_ideal_def using subgroup_UNIV by auto

lemma ideal_generated_0: "ideal_generated {0} = {0}"
  unfolding ideal_generated_def using ideal_0 by auto

lemma ideal_generated_subset_generator:
  assumes "ideal_generated A = I"
  shows "A ⊆ I"
  using assms unfolding ideal_generated_def by auto

lemma left_ideal_minus:
  assumes "left_ideal I"
  and "a∈I" and "b∈I"
  shows "a - b ∈ I"
  by (metis assms(1) assms(2) assms(3) diff_minus_eq_add left_ideal_def minus_minus subgroup_def)

lemma right_ideal_minus:
  assumes "right_ideal I"
  and "a∈I" and "b∈I"
  shows "a - b ∈ I"
  by (metis assms(1) assms(2) assms(3) diff_minus_eq_add minus_minus right_ideal_def subgroup_def)

lemma ideal_minus:
  assumes "ideal I"
  and "a∈I" and "b∈I"
  shows "a - b ∈ I"
  by (metis assms(1) assms(2) assms(3) ideal_def right_ideal_minus)


lemma ideal_ideal_generated: "ideal (ideal_generated S)"
  unfolding ideal_generated_def
  unfolding ideal_def left_ideal_def subgroup_def right_ideal_def
  by blast

lemma sum_left_ideal:
  assumes li_X: "left_ideal X"
  and U_X: "U ⊆ X" and U: "finite U"
  shows "(∑i∈U. f i * i) ∈ X"
  using U U_X
proof (induct U)
  case empty show ?case using li_X by (simp add:  left_ideal_def subgroup_def)
next
  case (insert x U)
  have x_in_X: "x ∈ X" using insert.prems by simp
  have fx_x_X: "f x * x ∈ X" using li_X x_in_X unfolding left_ideal_def by simp
  have sum_in_X: "(∑i∈U. f i * i) ∈ X" using insert.prems insert.hyps(3) by simp
  have "(∑i∈(insert x U). f i * i) = f x * x + (∑i∈U. f i * i)"
    by (simp add: insert.hyps(1) insert.hyps(2))
  also have "... ∈ X" using li_X fx_x_X sum_in_X unfolding left_ideal_def subgroup_def by auto
  finally show "(∑i∈(insert x U). f i * i) ∈ X" .
qed

lemma sum_right_ideal:
  assumes li_X: "right_ideal X"
  and U_X: "U ⊆ X" and U: "finite U"
  shows "(∑i∈U. i * f i) ∈ X"
  using U U_X
proof (induct U)
  case empty show ?case using li_X by (simp add: right_ideal_def subgroup_def)
next
  case (insert x U)
  have x_in_X: "x ∈ X" using insert.prems by simp
  have fx_x_X: "x * f x ∈ X" using li_X x_in_X unfolding right_ideal_def by simp
  have sum_in_X: "(∑i∈U. i * f i) ∈ X" using insert.prems insert.hyps(3) by simp
  have "(∑i∈(insert x U). i * f i) =  x * f x + (∑i∈U. i * f i)"
    by (simp add: insert.hyps(1) insert.hyps(2))
  also have "... ∈ X" using li_X fx_x_X sum_in_X unfolding right_ideal_def subgroup_def by auto
  finally show "(∑i∈(insert x U). i * f i) ∈ X" .
qed

lemma left_ideal_generated_subset:
  assumes "S ⊆ T"
  shows "left_ideal_generated S ⊆ left_ideal_generated T"
  unfolding left_ideal_generated_def using assms by auto

lemma right_ideal_generated_subset:
  assumes "S ⊆ T"
  shows "right_ideal_generated S ⊆ right_ideal_generated T"
  unfolding right_ideal_generated_def using assms by auto

lemma ideal_generated_subset:
  assumes "S ⊆ T"
  shows "ideal_generated S ⊆ ideal_generated T"
  unfolding ideal_generated_def using assms by auto

lemma ideal_generated_in:
  assumes "a ∈ A"
  shows "a ∈ ideal_generated A"
  unfolding ideal_generated_def using assms by auto

lemma ideal_generated_repeated: "ideal_generated {a,a} = ideal_generated {a}"
  unfolding ideal_generated_def by auto

end

context ring_1
begin

lemma left_ideal_explicit:
  "left_ideal_generated S = {y. ∃f U. finite U ∧ U ⊆ S ∧ sum (λi. f i * i) U = y}" (is "?S = ?B")
proof
  have S_in_B: "S ⊆ ?B"
  proof (auto)
    fix x assume x: "x∈S"
    show "∃f U. finite U ∧ U ⊆ S ∧ (∑i∈U. f i * i) = x"
      by (rule exI[of _ "λi. 1"], rule exI[of _ "{x}"], simp add: x)
  qed
  have left_ideal_B: "left_ideal ?B"
  proof (unfold left_ideal_def, auto)
    show "subgroup ?B"
    proof (unfold subgroup_def, auto)
      show "∃f U. finite U ∧ U ⊆ S ∧ (∑i∈U. f i * i) = 0"
        by (rule exI[of _ "id"], rule exI[of _ "{}"], auto)
      fix f A assume A: "finite A" and AS: "A ⊆ S"
      show"∃fa Ua. finite Ua ∧ Ua ⊆ S ∧ (∑i∈Ua. fa i * i) = - (∑i∈A. f i * i)"
        by (rule exI[of _ "λi. - f i"], rule exI[of _ A],
            auto simp add: A AS sum_negf[of "λi. f i * i" A])
      fix fa B assume B: "finite B" and BS: "B ⊆ S"
      let ?g="λi. if i ∈ A - B then f i else if i ∈ B - A then fa i else f i + fa i"
      show "∃fb Ub. finite Ub ∧ Ub ⊆ S ∧ (∑i∈Ub. fb i * i)
        = (∑i∈A. f i * i) + (∑i∈B. fa i * i)"
      proof (rule exI[of _ ?g], rule exI[of _ "A ∪ B"], simp add: A B AS BS)
        let ?g2 = "(λi. (if i ∈ A ∧ i ∉ B then f i else
          if i ∈ B - A then fa i else f i + fa i) * i)"
        have "(∑i∈A. f i * i) + (∑i∈B. fa i * i)
          = (∑i∈A - B. f i * i) + (∑i∈B - A. fa i * i) + (∑i∈A∩B. (f i * i) + (fa i * i))"
          by (rule sum_add[OF A B])
        also have "... = (∑i∈A - B. f i * i) + (∑i∈B - A. fa i * i)
          + (∑i∈A ∩ B. (f i + fa i) * i)"
          by (simp add: distrib_right)
        also have "... =  sum ?g2 (A - B) + sum ?g2 (B - A) + sum ?g2 (A ∩ B)" by auto
        also have "... = sum ?g2 (A ∪ B)" by (rule sum.union_diff2[OF A B, symmetric])
        finally show "sum ?g2 (A ∪ B) = (∑i∈A. f i * i) + (∑i∈B. fa i * i)" ..
      qed
    qed
    fix f U r assume U: "finite U" and U_in_S: "U ⊆ S"
    show "∃fa Ua. finite Ua ∧ Ua ⊆ S ∧ (∑i∈Ua. fa i * i) = r * (∑i∈U. f i * i)"
      by (rule exI[of _ "λi. r * f i"], rule exI[of _ U])
    (simp add: U U_in_S sum_distrib_left mult_assoc)
  qed
  thus "?S ⊆ ?B" using S_in_B unfolding left_ideal_generated_def by auto
next
  show "?B ⊆ ?S"
  proof (unfold left_ideal_generated_def, auto)
    fix X f U
    assume li_X: "left_ideal X" and S_X: "S ⊆ X" and U: "finite U" and U_in_S: "U ⊆ S"
    have U_in_X: "U ⊆ X" using U_in_S S_X by simp
    show "(∑i∈U. f i * i) ∈ X"
      by (rule sum_left_ideal[OF li_X U_in_X U])
  qed
qed


lemma right_ideal_explicit:
  "right_ideal_generated S = {y. ∃f U. finite U ∧ U ⊆ S ∧ sum (λi. i * f i) U = y}" (is "?S = ?B")
proof
  have S_in_B: "S ⊆ ?B"
  proof (auto)
    fix x assume x: "x∈S"
    show "∃f U. finite U ∧ U ⊆ S ∧ (∑i∈U. i * f i) = x"
      by (rule exI[of _ "λi. 1"], rule exI[of _ "{x}"], simp add: x)
  qed
  have right_ideal_B: "right_ideal ?B"
  proof (unfold right_ideal_def, auto)
    show "subgroup ?B"
    proof (unfold subgroup_def, auto)
      show "∃f U. finite U ∧ U ⊆ S ∧ (∑i∈U. i * f i) = 0"
        by (rule exI[of _ "id"], rule exI[of _ "{}"], auto)
      fix f A assume A: "finite A" and AS: "A ⊆ S"
      show"∃fa Ua. finite Ua ∧ Ua ⊆ S ∧ (∑i∈Ua.  i * fa i) = - (∑i∈A.  i * f i)"
        by (rule exI[of _ "λi. - f i"], rule exI[of _ A],
            auto simp add: A AS sum_negf[of "λi. i * f i" A])
      fix fa B assume B: "finite B" and BS: "B ⊆ S"
      let ?g="λi. if i ∈ A - B then f i else if i ∈ B - A then fa i else f i + fa i"
      show "∃fb Ub. finite Ub ∧ Ub ⊆ S ∧ (∑i∈Ub. i * fb i)
        = (∑i∈A. i * f i) + (∑i∈B. i * fa i)"
      proof (rule exI[of _ ?g], rule exI[of _ "A ∪ B"], simp add: A B AS BS)
        let ?g2 = "(λi. i * (if i ∈ A ∧ i ∉ B then f i else
          if i ∈ B - A then fa i else f i + fa i))"
        have "(∑i∈A.  i * f i) + (∑i∈B.  i * fa i)
          = (∑i∈A - B.  i * f i) + (∑i∈B - A.  i * fa i) + (∑i∈A∩B. (i * f i) + (i * fa i))"
          by (rule sum_add[OF A B])
        also have "... = (∑i∈A - B. i * f i) + (∑i∈B - A.  i * fa i)
          + (∑i∈A ∩ B. i * (f i + fa i))"
          by (simp add: distrib_left)
        also have "... =  sum ?g2 (A - B) + sum ?g2 (B - A) + sum ?g2 (A ∩ B)" by auto
        also have "... = sum ?g2 (A ∪ B)" by (rule sum.union_diff2[OF A B, symmetric])
        finally show "sum ?g2 (A ∪ B) = (∑i∈A. i * f i) + (∑i∈B. i * fa i)" ..
      qed
    qed
    fix f U r assume U: "finite U" and U_in_S: "U ⊆ S"
    show "∃fa Ua. finite Ua ∧ Ua ⊆ S ∧ (∑i∈Ua. i * fa i) = (∑i∈U. i * f i) * r"
      by (rule exI[of _ "λi. f i * r"], rule exI[of _ U])
    (simp add: U U_in_S sum_distrib_right mult_assoc)
  qed
  thus "?S ⊆ ?B" using S_in_B unfolding right_ideal_generated_def by auto
next
  show "?B ⊆ ?S"
  proof (unfold right_ideal_generated_def, auto)
    fix X f U
    assume li_X: "right_ideal X" and S_X: "S ⊆ X" and U: "finite U" and U_in_S: "U ⊆ S"
    have U_in_X: "U ⊆ X" using U_in_S S_X by simp
    show "(∑i∈U. i * f i) ∈ X"
      by (rule sum_right_ideal[OF li_X U_in_X U])
  qed
qed

end

context comm_ring
begin

lemma left_ideal_eq_right_ideal: "left_ideal I = right_ideal I"
  unfolding left_ideal_def right_ideal_def subgroup_def
  by auto (metis mult_commute)+

corollary ideal_eq_left_ideal: "ideal I = left_ideal I"
  by (metis ideal_def left_ideal_eq_right_ideal)

lemma ideal_eq_right_ideal: "ideal I = right_ideal I"
  by (metis ideal_def left_ideal_eq_right_ideal)

lemma principal_ideal_eq_left:
  "principal_ideal S = (∃a. left_ideal_generated {a} = S)"
  unfolding principal_ideal_def ideal_generated_def left_ideal_generated_def
  unfolding ideal_eq_left_ideal ..

end

context comm_ring_1
begin

lemma ideal_generated_eq_left_ideal: "ideal_generated A = left_ideal_generated A"
  unfolding ideal_generated_def ideal_def
  by (metis (no_types, lifting) Collect_cong left_ideal_eq_right_ideal left_ideal_generated_def)

lemma ideal_generated_eq_right_ideal: "ideal_generated A = right_ideal_generated A"
  unfolding ideal_generated_def ideal_def
  by (metis (no_types, lifting) Collect_cong left_ideal_eq_right_ideal right_ideal_generated_def)


lemma obtain_sum_ideal_generated:
  assumes a: "a ∈ ideal_generated A" and A: "finite A"
  obtains f where "sum (λi. f i * i) A = a"
proof -
  obtain g U where g: "sum (λi. g i * i) U = a" and UA: "U ⊆ A" and U: "finite U"
    using a unfolding ideal_generated_eq_left_ideal
    unfolding left_ideal_explicit by blast
  let ?f="λi. if i ∈ A - U then 0 else g i"
  have A_union: "A = (A - U) ∪ U" using UA by auto
  have "sum (λi. ?f i * i) A = sum (λi. ?f i * i) ((A - U) ∪ U)" using A_union by simp
  also have "... = sum (λi. ?f i * i) (A - U) + sum (λi. ?f i * i) U"
    by (rule sum.union_disjoint[OF _ U], auto simp add: A U UA)
  also have "... = sum (λi. ?f i * i) U" by auto
  also have "... = a" using g by auto
  finally have "sum (λi. ?f i * i) A = a" .
  with that show ?thesis .
qed

lemma dvd_ideal_generated_singleton:
  assumes subset: "ideal_generated {a} ⊆ ideal_generated {b}"
  shows "b dvd a"
proof -
 have "a ∈ ideal_generated {a}" by (simp add: ideal_generated_in)
 hence a: "a ∈ ideal_generated {b}" by (metis subset subsetCE)
 obtain f where "sum (λi. f i * i) {b} = a" by (rule obtain_sum_ideal_generated[OF a], simp)
 hence fb_b_a: "f b * b = a" unfolding sum_singleton .
 show ?thesis unfolding dvd_def by (rule exI[of _ "f b"], metis fb_b_a mult_commute)
qed

lemma ideal_generated_singleton: "ideal_generated {a} = {k*a|k. k ∈ UNIV}"
proof (auto simp add: ideal_generated_eq_left_ideal left_ideal_explicit)
  fix f U
  assume U: "finite U" and U_in_a: "U ⊆ {a}"
  show "∃k. (∑i∈U. f i * i) = k * a"
  proof (cases "U={}")
    case True show ?thesis by (rule exI[of _ 0], simp add: True)
  next
    case False
    hence Ua: "U = {a}" using U_in_a by auto
    show ?thesis by (rule exI[of _ "f a"]) (simp add: Ua sum_singleton)
  qed
next
  fix k
  show " ∃f U. finite U ∧ U ⊆ {a} ∧ (∑i∈U. f i * i) = k * a"
    by (rule exI[of _ "λi. k"], rule exI[of _ "{a}"], simp)
qed


lemma dvd_ideal_generated_singleton':
  assumes b_dvd_a: "b dvd a"
  shows "ideal_generated {a} ⊆ ideal_generated {b}"
  apply (simp only: ideal_generated_singleton)
  using assms unfolding dvd_def
  apply auto
  apply (simp_all only: mult_commute)
  unfolding mult_assoc[symmetric]
  apply blast
  done


lemma ideal_generated_subset2:
  assumes ac: "ideal_generated {a} ⊆ ideal_generated {c}"
  and bc: "ideal_generated {b} ⊆ ideal_generated {c}"
  shows "ideal_generated {a,b} ⊆ ideal_generated {c}"
proof
  fix x
  assume x: "x ∈ ideal_generated {a, b}"
  show " x ∈ ideal_generated {c}"
  proof (cases "a=b")
    case True
    show ?thesis using x bc unfolding True ideal_generated_repeated by fast
  next
    case False
    obtain k where k: "a = c * k"
      using dvd_ideal_generated_singleton[OF ac] unfolding dvd_def by auto
    obtain k' where k': "b = c * k'"
      using dvd_ideal_generated_singleton[OF bc] unfolding dvd_def by auto
    obtain f where f: "sum (λi. f i * i) {a,b} = x"
      by (rule obtain_sum_ideal_generated[OF x], simp)
    hence "x = f a * a + f b * b " unfolding sum_two_elements[OF False] by simp
    also have "... = f a * (c * k) + f b * (c * k')" unfolding k k' by simp
    also have "... = (f a * k) * c + (f b * k') * c"
      by (simp only: mult_assoc) (simp only: mult_commute)
    also have "... = (f a * k +  f b * k') * c"
      by (simp only: mult_commute) (simp only: distrib_left)
    finally have "x = (f a * k + f b * k') * c" .
    thus ?thesis unfolding ideal_generated_singleton by auto
  qed
qed

end

lemma ideal_kZ: "ideal {k*x|x. x∈(UNIV::int set)}"
  unfolding ideal_def left_ideal_def right_ideal_def subgroup_def
  apply auto
  apply (metis int_distrib(2))
  apply (metis minus_mult_right)
  apply (metis int_distrib(2))
  apply (metis minus_mult_right)
  done

subsection‹GCD Rings and Bezout Domains›

text‹To define GCD rings and Bezout rings, there are at least two options:
fix the operation gcd or just assume its existence. We have chosen the second one in order to be
able to use subclasses (if we fix a gcd in the bezout ring class, then we couln't prove that
principal ideal rings are a subclass of bezout rings).›

class GCD_ring = comm_ring_1
  + assumes exists_gcd: "∃d. d dvd a ∧ d dvd b ∧ (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd d)"
begin

text‹In this structure, there is always a gcd for each pair of elements, but maybe not unique.
The following definition essentially says if a function satisfies the condition to be a gcd.›

definition is_gcd :: "('a ⇒ 'a ⇒ 'a) ⇒ bool"
  where "is_gcd (gcd') = (∀a b. (gcd' a b dvd a)
                          ∧ (gcd' a b dvd b)
                          ∧ (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd gcd' a b))"

lemma gcd'_dvd1:
  assumes "is_gcd gcd'" shows "gcd' a b dvd a" using assms unfolding is_gcd_def by auto

lemma gcd'_dvd2:
  assumes "is_gcd gcd'" shows "gcd' a b dvd b"
  using assms unfolding is_gcd_def by auto

lemma gcd'_greatest:
  assumes "is_gcd gcd'" and "l dvd a" and "l dvd b"
  shows "l dvd gcd' a b"
  using assms unfolding is_gcd_def by auto

lemma gcd'_zero [simp]:
  assumes "is_gcd gcd'"
  shows "gcd' x y = 0 ⟷ x = 0 ∧ y = 0"
  by (metis dvd_0_left dvd_refl gcd'_dvd1 gcd'_dvd2 gcd'_greatest assms)+

end

class GCD_domain = GCD_ring + idom

class bezout_ring = comm_ring_1 +
        assumes exists_bezout: "∃p q d. (p*a + q*b = d)
                    ∧ (d dvd a)
                    ∧ (d dvd b)
                    ∧ (∀d'. (d' dvd a ∧ d' dvd b) ⟶ d' dvd d)"
begin

subclass GCD_ring
proof
  fix a b
  show "∃d. d dvd a ∧ d dvd b ∧ (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd d)"
    using exists_bezout[of a b] by auto
qed

text‹In this structure, there is always a bezout decomposition for each pair of elements, but it is
not unique. The following definition essentially says if a function satisfies the condition to be a
bezout decomposition.›

definition is_bezout :: "('a ⇒'a ⇒ ('a × 'a × 'a)) ⇒ bool"
  where "is_bezout (bezout) = (∀a b. let (p, q, gcd_a_b) = bezout a b
                                      in
                                        p * a + q * b = gcd_a_b
                                        ∧ (gcd_a_b dvd a)
                                        ∧ (gcd_a_b dvd b)
                                        ∧ (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd gcd_a_b))"

text‹The following definition is similar to the previous one, and checks if the input is a
function that given two parameters ‹a b› returns 5 elements ‹(p,q,u,v,d)›
where ‹d› is a gcd of ‹a› and ‹b›, ‹p› and ‹q› are the
bezout coefficients such that ‹p*a+q*b=d›, ‹d*u = -b› and ‹d*v= a›.
The elements ‹u› and ‹v› are useful for defining the bezout matrix.›

definition is_bezout_ext :: "('a ⇒'a ⇒ ('a × 'a × 'a × 'a × 'a)) ⇒ bool"
  where "is_bezout_ext (bezout) = (∀a b. let (p, q, u, v, gcd_a_b) = bezout a b
                                          in
                                            p * a + q * b = gcd_a_b
                                            ∧ (gcd_a_b dvd a)
                                            ∧ (gcd_a_b dvd b)
                                            ∧ (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd gcd_a_b)
                                            ∧ gcd_a_b * u = -b
                                            ∧ gcd_a_b * v = a)"

lemma is_gcd_is_bezout_ext:
  assumes "is_bezout_ext bezout"
  shows "is_gcd (λa b. case bezout a b of (x, xa,u,v, gcd') ⇒ gcd')"
  unfolding is_gcd_def using assms unfolding is_bezout_ext_def Let_def by (simp add: split_beta)

lemma is_bezout_ext_is_bezout:
  assumes "is_bezout_ext bezout"
  shows "is_bezout (λa b. case bezout a b of (x,xa,u,v, gcd') ⇒ (x,xa,gcd'))"
  unfolding is_bezout_def using assms unfolding is_bezout_ext_def Let_def by (simp add: split_beta)

lemma is_gcd_is_bezout:
  assumes "is_bezout bezout"
  shows "is_gcd (λa b. (case bezout a b of (_, _, gcd') ⇒ (gcd')))"
  unfolding is_gcd_def using assms unfolding is_bezout_def Let_def by (simp add: split_beta)

text‹The assumptions of the Bezout rings say that there exists a bezout operation.
  Now we will show that there also exists an operation satisfying ‹is_bezout_ext››

lemma exists_bezout_ext_aux:
  fixes a and b
  shows "∃p q u v d. (p * a + q * b = d)
                    ∧ (d dvd a)
                    ∧ (d dvd b)
                    ∧ (∀d'. (d' dvd a ∧ d' dvd b) ⟶ d' dvd d) ∧ d * u = -b ∧ d * v = a"
proof -
  obtain p q d where prems01: "(p * a + q * b = d)
                    ∧ (d dvd a)
                    ∧ (d dvd b)
                    ∧ (∀d'. (d' dvd a ∧ d' dvd b) ⟶ d' dvd d)"
                    using exists_bezout [of a b] by fastforce
  hence db: "d dvd b" and da: "d dvd a" by blast+
  obtain u v where prems02: "d * u = -b" and prems03: "d * v = a" using db and da
    by (metis local.dvdE local.minus_mult_right)
  show ?thesis using exI [of _ "(p,q,u,v,d)"] prems01 prems02 prems03
  by metis
qed

lemma exists_bezout_ext: "∃bezout_ext. is_bezout_ext bezout_ext"
proof -
  define bezout_ext where "bezout_ext a b = (SOME (p,q,u,v,d). p * a + q * b = d
    ∧ (d dvd a) ∧ (d dvd b) ∧ (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd d) ∧ d * u = -b ∧ d * v = a)"
    for a b
  show ?thesis
  proof (rule exI [of _ bezout_ext], unfold is_bezout_ext_def, rule+)
    fix a b
    obtain p q u v d where foo: "p * a + q * b = d ∧
              d dvd a ∧
              d dvd b ∧
              (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd d) ∧
              d * u = - b ∧ d * v = a" using exists_bezout_ext_aux [of a b] by fastforce
    show "let (p, q, u, v, gcd_a_b) = bezout_ext a b
           in p * a + q * b = gcd_a_b ∧
              gcd_a_b dvd a ∧
              gcd_a_b dvd b ∧
              (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd gcd_a_b) ∧
              gcd_a_b * u = - b ∧ gcd_a_b * v = a"
      by (unfold bezout_ext_def Let_def, rule someI [of _ "(p,q,u,v,d)"], clarify, rule foo)
   qed
qed

end

class bezout_domain = bezout_ring + idom

subclass (in bezout_domain) GCD_domain
proof
qed

class bezout_ring_div = bezout_ring + euclidean_semiring
class bezout_domain_div = bezout_domain + euclidean_semiring

subclass (in bezout_ring_div) bezout_domain_div
proof qed

subsection‹Principal Ideal Domains›

class pir = comm_ring_1 + assumes all_ideal_is_principal: "ideal I ⟹ principal_ideal I"
class pid = idom + pir

text‹Thanks to the following proof, we will show that there exist bezout and gcd operations
in principal ideal rings for each pair of elements.›

subclass (in pir) bezout_ring
proof
  fix a b
  define S where "S = ideal_generated {a,b}"
  have ideal_S: "ideal S" using ideal_ideal_generated unfolding S_def by simp
  obtain d where d: "ideal_generated {d} = S" using all_ideal_is_principal[OF ideal_S]
    unfolding principal_ideal_def by blast
  have ideal_d: "ideal (ideal_generated {d})" using ideal_ideal_generated by simp
  have a_subset_d: "ideal_generated {a} ⊆ ideal_generated {d}"
    by (metis S_def d insertI1 ideal_generated_subset singletonD subsetI)
  have b_subset_d: "ideal_generated {b} ⊆ ideal_generated {d}"
    by (metis S_def d insert_iff ideal_generated_subset subsetI)
  have d_in_S: "d ∈ S" by (metis d insert_subset ideal_generated_subset_generator)
  obtain f U where U: "U ⊆ {a,b}" and f: "sum (λi. f i * i) U = d"
    using left_ideal_explicit[of "{a,b}"] d_in_S unfolding S_def ideal_generated_eq_left_ideal
    by auto
  define g where "g i = (if i ∈ U then f i else 0)" for i
  show "∃p q d. p * a + q * b = d ∧ d dvd a ∧ d dvd b ∧ (∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd d)"
  proof (cases "a = b")
    case True
    show ?thesis
    proof (rule exI[of _ "g a"], rule exI[of _ "0"], rule exI[of _ d], auto)
      show ga_a_d: "g a * a = d"
        unfolding g_def
      proof auto
        assume "a ∈ U"
        hence Ua: "U = {a}" using U True by auto
        show "f a * a = d" using f unfolding Ua
          unfolding sum_singleton .
      next
        assume "a ∉ U"
        hence U_empty: "U = {}" using U True by auto
        show "0 = d" using f unfolding U_empty by auto
      qed
      show "d dvd a" by (rule dvd_ideal_generated_singleton[OF a_subset_d])
      show "d dvd b" by (rule dvd_ideal_generated_singleton[OF b_subset_d])
      fix d' assume d'_dvd_a: "d' dvd a" and d'_dvd_b: "d' dvd b"
      show "d' dvd d" by (metis ga_a_d d'_dvd_a dvd_mult2 mult_commute)
    qed
  next
    case False
    show ?thesis
    proof (rule exI[of _ "g a"], rule exI[of _ "g b"], rule exI[of _ d], auto)
      show "g a * a + g b * b = d"
      proof (auto simp add: g_def)
        assume a: "a ∈ U" and b: "b ∈ U"
        hence U_ab: "U = {a,b}" using U by auto
        show "f a * a + f b * b = d"  using f unfolding U_ab sum_two_elements[OF False] .
      next
        assume a: "a ∈ U" and b: "b ∉ U"
        hence U_a: "U = {a}" using U by auto
        show "f a * a = d" using f unfolding U_a sum_singleton .
      next
        assume a: "a ∉ U" and b: "b ∈ U"
        hence U_b: "U = {b}" using U by auto
        show "f b * b = d" using f unfolding U_b sum_singleton .
      next
        assume a: "a ∉ U" and b: "b ∉ U"
        hence "U = {}" using U by auto
        thus "0 = d" using f by auto
      qed
      show "d dvd a" by (rule dvd_ideal_generated_singleton[OF a_subset_d])
      show "d dvd b" by (rule dvd_ideal_generated_singleton[OF b_subset_d])
      fix d' assume d'a: "d' dvd a" and d'b: "d' dvd b"
      have ad': "ideal_generated {a} ⊆ ideal_generated {d'}"
        by (rule dvd_ideal_generated_singleton'[OF d'a])
      have bd': "ideal_generated {b} ⊆ ideal_generated {d'}"
        by (rule dvd_ideal_generated_singleton'[OF d'b])
      have abd': "ideal_generated {a,b} ⊆ ideal_generated {d'}"
        by (rule ideal_generated_subset2[OF ad' bd'])
      hence dd': "ideal_generated {d} ⊆ ideal_generated {d'}"
        by (simp add: S_def d)
      show "d' dvd d" by (rule dvd_ideal_generated_singleton[OF dd'])
    qed
  qed
qed

subclass (in pid) bezout_domain
proof
qed

context pir
begin

lemma ascending_chain_condition:
  fixes I::"nat=>'a set"
  assumes all_ideal: "∀n. ideal (I(n))"
  and inc: "∀n. I(n) ⊆ I(n+1)"
  shows "∃n. I(n)=I(n+1)"
proof -
  let ?I = "⋃{I(n)|n. n∈(UNIV::nat set)}"
  have "ideal ?I" using ideal_Union[of I] all_ideal inc by fast
  from this obtain a where a: "ideal_generated {a} = ?I"
    using all_ideal_is_principal
    unfolding principal_ideal_def by fastforce
  have "a ∈ ?I" using a ideal_generated_subset_generator[of "{a}" "?I"] by simp
  from this obtain k where a_Ik: "a ∈ I(k)" using Union_iff[of a "{I n |n. n ∈ UNIV}"] by auto
  show ?thesis
  proof (rule exI[of _ k], rule)
    show "I k ⊆ I (k + 1)" using inc by simp
    show "I (k + 1) ⊆ I k"
    proof (auto)
      fix x assume x: "x ∈ I (Suc k)"
      have "ideal_generated {a} = I k"
      proof
        have ideal_Ik: "ideal (I (k))" using all_ideal by simp
        show "I k ⊆ ideal_generated {a}" using a by auto
        show "ideal_generated {a} ⊆ I k"
          by (metis (lifting) a_Ik all_ideal ideal_generated_def
            le_Inf_iff mem_Collect_eq singleton_iff subsetI)
      qed
      thus "x ∈ I k" using x unfolding a by auto
    qed
  qed
qed


lemma ascending_chain_condition2:
  "∄I::(nat ⇒ 'a set). (∀n. ideal (I n) ∧ I n ⊂ I (n + 1))"
proof (rule ccontr, auto)
  fix I assume a: "∀n. ideal (I n) ∧ I n ⊂ I (Suc n)"
  hence "∀n. ideal (I n)" "∀n. I n ⊆ I (Suc n)" by auto
  hence "∃n. I(n)=I(n+1)" using ascending_chain_condition by auto
  thus False using a by auto
qed

end

class pir_div = pir + euclidean_semiring
class pid_div = pid + euclidean_semiring

subclass (in pir_div) pid_div
proof qed

subclass (in pir_div) bezout_ring_div
proof qed

subclass (in pid_div) bezout_domain_div
proof qed

subsection‹Euclidean Domains›

text‹We make use of the euclidean ring (domain) class developed by Manuel Eberl.›

subclass (in euclidean_ring) pid
proof
  fix I assume I: "ideal I"
  show "principal_ideal I"
  proof (cases "I={0}")
    case True show ?thesis unfolding principal_ideal_def True
      using ideal_generated_0 ideal_0 by auto
  next
    case False
    have fI_not_empty: "(euclidean_size` (I-{0}))≠{}" using False ideal_not_empty[OF I] by auto
    from this obtain d where fd: "euclidean_size d
      = Least (λi. i ∈ (euclidean_size`(I-{0})))" and d: "d∈(I-{0})"
      by (metis (lifting, mono_tags) LeastI_ex imageE ex_in_conv)
    have d_not_0: "d≠0" using d by simp
    have fd_le: "∀x∈I-{0}. euclidean_size d ≤ euclidean_size x"
      by (metis (mono_tags) Least_le fd image_eqI)
    show "principal_ideal I"
    proof (unfold principal_ideal_def, rule exI[of _ d], auto)
      fix x assume x:"x ∈ ideal_generated {d}" show "x ∈ I"
        using x unfolding ideal_generated_def
        by (auto, metis Diff_iff I d)
    next
      fix a assume a: "a ∈ I"
      obtain q r where "a = q * d + r"
        and fr_fd: "euclidean_size r < euclidean_size d"
        using div_mult_mod_eq [of a d, symmetric] d_not_0 mod_size_less
        by blast
      show "a ∈ ideal_generated {d}"
      proof (cases "r=0")
        case True hence "a = q * d" using ‹a = q * d + r›
          by auto
        then show ?thesis unfolding ideal_generated_def
          unfolding ideal_def right_ideal_def
          by (simp add: ac_simps)
      next
        case False
        hence r_noteq_0: "r ≠ 0" by simp
        have "r = a - d * q" using ‹a = q * d + r›
          by (simp add: algebra_simps)
        also have "... ∈ I"
        proof (rule left_ideal_minus)
          show "left_ideal I" using I unfolding ideal_def by simp
          show "a ∈ I" using a .
          show "d * q ∈ I" using d I unfolding ideal_def right_ideal_def by simp
        qed
        finally have "r ∈ I-{0}" using r_noteq_0 by auto
        hence "euclidean_size d ≤ euclidean_size r" using fd_le by auto
        thus ?thesis using fr_fd by auto
      qed
    qed
  qed
qed

context euclidean_ring_gcd
begin

text‹This is similar to the ‹euclid_ext› operation, but involving two more parameters
to satisfy that ‹is_bezout_ext euclid_ext2››

definition euclid_ext2 :: "'a ⇒ 'a ⇒ 'a × 'a × 'a × 'a × 'a"
  where "euclid_ext2 a b =
   (fst (bezout_coefficients a b), snd (bezout_coefficients a b), - b div gcd a b, a div gcd a b, gcd a b)"

lemma is_bezout_ext_euclid_ext2: "is_bezout_ext (euclid_ext2)"
proof (unfold is_bezout_ext_def Let_def, clarify, intro conjI)
  fix a b p q u v d
  assume e: "euclid_ext2 a b = (p, q, u, v, d)"
  then have "bezout_coefficients a b = (p, q)" and "gcd a b = d"
    by (auto simp add: euclid_ext2_def)
  then show "p * a + q * b = d"
    by (simp add: bezout_coefficients)
  from ‹gcd a b = d› show "d dvd a" and "d dvd b"
    by auto
  from ‹gcd a b = d› show "∀d'. d' dvd a ∧ d' dvd b ⟶ d' dvd d"
    by auto
  have "a div d = v" and "-b div d = u"
    using e by (auto simp add: euclid_ext2_def)
  then show "d * v = a" and "d * u = - b"
    using ‹d dvd a› and ‹d dvd b› by auto
qed

lemma is_bezout_euclid_ext: "is_bezout (λa b. (fst (bezout_coefficients a b), snd (bezout_coefficients a b), gcd a b))"
  by (auto simp add: is_bezout_def bezout_coefficients)

end

subclass (in euclidean_ring) pid_div ..


subsection‹More gcd structures›

text‹The following classes represent structures where there exists a gcd
  for each pair of elements and the operation is fixed.›

class pir_gcd = pir + semiring_gcd
class pid_gcd = pid + pir_gcd

subclass (in euclidean_ring_gcd) pid_gcd ..



subsection‹Field›

text‹Proving that any field is a euclidean domain. There are alternatives to do this,
see @{url "https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-October/msg00034.html"}›

(* TODO Remove *)
class field_euclidean = field + euclidean_ring +
  assumes "euclidean_size = (λi. if i = 0 then 0 else 1::nat)"
  and "normalisation_factor = id"

end


(*********** Possible future work: ***********)
(*
  - Prime elements, irreducible elements...
  - Prufer Domain, Noetherian...
*)