Theory Rings2_Extended

(*
    Author:      Jose Divasón
    Email:       jose.divason@unirioja.es
*)

section ‹Some theorems about rings and ideals›

theory Rings2_Extended
  imports
    Echelon_Form.Rings2
    "HOL-Types_To_Sets.Types_To_Sets"
begin

subsection ‹Missing properties on ideals›

lemma ideal_generated_subset2:
  assumes  "bB. b  ideal_generated A"
  shows "ideal_generated B  ideal_generated A"
  by (metis (mono_tags, lifting) InterE assms ideal_generated_def
ideal_ideal_generated mem_Collect_eq subsetI)

context comm_ring_1
begin

lemma ideal_explicit: "ideal_generated S
      = {y. f U. finite U  U  S  (iU. f i * i) = y}"
  by (simp add: ideal_generated_eq_left_ideal left_ideal_explicit)
end

lemma ideal_generated_minus:
  assumes a: "a  ideal_generated (S-{a})"
  shows "ideal_generated S = ideal_generated (S-{a})"
proof (cases "a  S")
  case True note a_in_S = True
  show ?thesis
  proof
    show "ideal_generated S  ideal_generated (S - {a})"
    proof (rule ideal_generated_subset2, auto)
      fix b assume b: "b  S" show "b  ideal_generated (S - {a})"
      proof (cases "b = a")
        case True
        then show ?thesis using a by auto
      next
        case False
        then show ?thesis using b
          by (simp add: ideal_generated_in)
      qed
    qed
    show "ideal_generated (S - {a})  ideal_generated S"
      by (rule ideal_generated_subset, auto)
  qed
next
  case False
  then show ?thesis by simp
qed

lemma ideal_generated_dvd_eq:
  assumes a_dvd_b: "a dvd b"
  and a: "a  S"
  and a_not_b: "a  b"
  shows "ideal_generated S = ideal_generated (S - {b})"
proof
  show "ideal_generated S  ideal_generated (S - {b})"
  proof (rule ideal_generated_subset2, auto)
    fix x assume x: "x  S"
    show "x  ideal_generated (S - {b})"
    proof (cases "x = b")
      case True
      obtain k where b_ak: "b = a * k" using a_dvd_b unfolding dvd_def by blast
      let ?f = "λc. k"
      have "(i{a}. i * ?f i) = x" using True b_ak by auto
      moreover have "{a}  S - {b}" using a_not_b a by auto
      moreover have "finite {a}" by auto
      ultimately show ?thesis
        unfolding ideal_def
        by (metis True b_ak ideal_def ideal_generated_in ideal_ideal_generated insert_subset right_ideal_def)
    next
      case False
      then show ?thesis by (simp add: ideal_generated_in x)
    qed
  qed
  show "ideal_generated (S - {b})  ideal_generated S" by (rule ideal_generated_subset, auto)
qed

lemma ideal_generated_dvd_eq_diff_set:
  assumes i_in_I: "iI" and i_in_J: "i  J" and i_dvd_j: "jJ. i dvd j"
  and f: "finite J"
  shows "ideal_generated I = ideal_generated (I - J)"
  using f i_in_J i_dvd_j i_in_I
  proof (induct J arbitrary: I)
  case empty
    then show ?case by auto
  next
    case (insert x J)
    have "ideal_generated I = ideal_generated (I-{x})"
      by (rule ideal_generated_dvd_eq[of i], insert insert.prems , auto)
    also have "... = ideal_generated ((I-{x}) - J)"
      by (rule insert.hyps, insert insert.prems insert.hyps, auto)
    also have "... = ideal_generated (I - insert x J)"
      using Diff_insert2[of I x J] by auto
    finally show ?case .
  qed


context comm_ring_1
begin

lemma ideal_generated_singleton_subset:
  assumes d: "d  ideal_generated S" and fin_S: "finite S"
  shows "ideal_generated {d}  ideal_generated S"
proof
  fix x assume x: "x  ideal_generated {d}"
  obtain k where x_kd: "x = k*d " using x using obtain_sum_ideal_generated[OF x]
    by (metis finite.emptyI finite.insertI sum_singleton)
  show "x  ideal_generated S"
    using d ideal_eq_right_ideal ideal_ideal_generated right_ideal_def mult_commute x_kd by auto
qed

lemma ideal_generated_singleton_dvd:
  assumes i: "ideal_generated S = ideal_generated {d}" and x: "x  S"
  shows "d dvd x"
  by (metis i x finite.intros dvd_ideal_generated_singleton
      ideal_generated_in ideal_generated_singleton_subset)

lemma ideal_generated_UNIV_insert:
  assumes "ideal_generated S = UNIV"
  shows "ideal_generated (insert a S) = UNIV" using assms
  using local.ideal_generated_subset by blast

lemma ideal_generated_UNIV_union:
  assumes "ideal_generated S = UNIV"
  shows "ideal_generated (A  S) = UNIV"
  using assms local.ideal_generated_subset
  by (metis UNIV_I Un_subset_iff equalityI subsetI)

lemma ideal_explicit2:
  assumes "finite S"
  shows "ideal_generated S = {y. f. (iS. f i * i) = y}"
  by (smt (verit) Collect_cong assms ideal_explicit obtain_sum_ideal_generated mem_Collect_eq subsetI)

lemma ideal_generated_unit:
  assumes u: "u dvd 1"
  shows "ideal_generated {u} = UNIV"
proof -
  have "x  ideal_generated {u}" for x
  proof -
    obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def
      using local.mult_ac(2) by blast
    have "x = x * inv_u * u" using inv_u by (simp add: local.mult_ac(1))
    also have "...  {k * u |k. k  UNIV}" by auto
    also have "... = ideal_generated {u}" unfolding ideal_generated_singleton by simp
    finally show ?thesis .
  qed
  thus ?thesis by auto
qed


lemma ideal_generated_dvd_subset:
  assumes x: "x  S. d dvd x" and S: "finite S"
  shows "ideal_generated S  ideal_generated {d}"
proof
  fix x assume "x ideal_generated S"
  from this obtain f where f: "(iS. f i * i) = x" using ideal_explicit2[OF S] by auto
  have "d dvd (iS. f i * i)" by (rule dvd_sum, insert x, auto)
  thus "x  ideal_generated {d}"
    using f dvd_ideal_generated_singleton' ideal_generated_in singletonI by blast
qed


lemma ideal_generated_mult_unit:
  assumes f: "finite S" and u: "u dvd 1"
  shows "ideal_generated ((λx. u*x)` S) = ideal_generated S"
  using f
proof (induct S)
  case empty
  then show ?case by auto
next
  case (insert x S)
  obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def
    using mult_ac by blast
  have f: "finite (insert (u*x) ((λx. u*x)` S))" using insert.hyps by auto
  have f2: "finite (insert x S)" by (simp add: insert(1))
  have f3: "finite S" by (simp add: insert)
  have f4: "finite ((*) u ` S)" by (simp add: insert)
  have inj_ux: "inj_on (λx. u*x) S" unfolding inj_on_def
    by (auto, metis inv_u local.mult_1_left local.semiring_normalization_rules(18))
  have "ideal_generated ((λx. u*x)` (insert x S)) = ideal_generated (insert (u*x) ((λx. u*x)` S))"
    by auto
  also have "... = {y. f. (iinsert (u*x) ((λx. u*x)` S). f i * i) = y}"
    using ideal_explicit2[OF f] by auto
  also have "... = {y. f. (i(insert x S). f i * i) = y}" (is "?L = ?R")
  proof -
    have "a  ?L"  if a: "a  ?R" for a
    proof -
      obtain f where sum_rw: "(i(insert x S). f i * i) = a" using a by auto
      define b where "b=(iS. f i * i)"
      have "b  ideal_generated S" unfolding b_def ideal_explicit2[OF f3] by auto
      hence "b  ideal_generated ((*) u ` S)" using insert.hyps(3) by auto
      from this obtain g where "(i((*) u ` S). g i * i) = b"
        unfolding ideal_explicit2[OF f4] by auto
      hence sum_rw2: "(iS. f i * i) = (i((*) u ` S). g i * i)" unfolding b_def by auto
      let ?g = "λi. if i = u*x then f x * inv_u else g i"
       have sum_rw3: "sum ((λi. g i * i)  (λx. u*x)) S = sum ((λi. ?g i * i)  (λx. u*x)) S"
        by (rule sum.cong, auto, metis inv_u local.insert(2) local.mult_1_right
              local.mult_ac(2) local.semiring_normalization_rules(18))
      have sum_rw4: "(i(λx. u*x)` S. g i * i) = sum ((λi. g i * i)  (λx. u*x)) S"
        by (rule sum.reindex[OF inj_ux])
      have "a = f x * x + (iS. f i * i)"
        using sum_rw local.insert(1) local.insert(2) by auto
      also have "... = f x * x + (i(λx. u*x)` S. g i * i)" using sum_rw2 by auto
      also have "... = ?g (u * x) * (u * x) + (i(λx. u*x)` S. g i * i)"
        using inv_u by (smt (verit) local.mult_1_right local.mult_ac(1))
      also have "... =  ?g (u * x) * (u * x) + sum ((λi. g i * i)  (λx. u*x)) S"
        using sum_rw4 by auto
      also have "... = ((λi. ?g i * i)  (λx. u*x)) x + sum ((λi. g i * i)  (λx. u*x)) S" by auto
      also have "... = ((λi. ?g i * i)  (λx. u*x)) x + sum ((λi. ?g i * i)  (λx. u*x)) S"
        using sum_rw3 by auto
      also have "... = sum ((λi. ?g i * i)  (λx. u*x)) (insert x S)"
        by (rule sum.insert[symmetric], auto simp add: insert)
      also have "... = (iinsert (u * x) ((λx. u*x)` S). ?g i * i)"
        by (smt (verit) abel_semigroup.commute f2 image_insert inv_u mult.abel_semigroup_axioms mult_1_right
            semiring_normalization_rules(18) sum.reindex_nontrivial)
      also have "... = (i(λx. u*x)` (insert x S). ?g i * i)" by auto
      finally show ?thesis by auto
    qed
    moreover have "a  ?R" if a: "a  ?L" for a
    proof -
      obtain f where sum_rw: "(i(insert (u * x) ((*) u ` S)). f i * i) = a" using a by auto
      have ux_notin: "u*x  ((*) u ` S)"
        by (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI inv_u local.insert(2) local.mult_1_left
            local.semiring_normalization_rules(18) subsetI)
      let ?f = "(λx. f x * x)"
      have "sum ?f ((*) u ` S)  ideal_generated ((*) u ` S)"
        unfolding ideal_explicit2[OF f4] by auto
      from this obtain g where sum_rw1: "sum (λi. g i * i) S = sum ?f (((*) u ` S))"
        using insert.hyps(3) unfolding ideal_explicit2[OF f3] by blast
      let ?g = "(λi. if i = x  then (f (u*x) *u) * x else g i * i)"
      let ?g' = "λi. if i = x  then f (u*x) * u else g i"
      have sum_rw2: "sum (λi. g i * i) S = sum ?g S" by (rule sum.cong, insert inj_ux ux_notin, auto)
      have "a = (i(insert (u * x) ((*) u ` S)). f i * i)" using sum_rw by simp
      also have "... = ?f (u*x) +  sum ?f (((*) u ` S))"
        by (rule sum.insert[OF f4], insert inj_ux) (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI
            inv_u local.insert(2) local.mult_1_left local.semiring_normalization_rules(18) subsetI)
      also have "... = ?f (u*x) + sum (λi. g i * i) S" unfolding sum_rw1 by auto
      also have "... = ?g x + sum ?g S" unfolding sum_rw2 using mult.assoc by auto
      also have "... = sum ?g (insert x S)" by (rule sum.insert[symmetric, OF f3 insert.hyps(2)])
      also have "... = sum (λi. ?g' i * i) (insert x S)" by (rule sum.cong, auto)
      finally show ?thesis by fast
    qed
    ultimately show ?thesis by blast
  qed
  also have "... = ideal_generated (insert x S)" using ideal_explicit2[OF f2] by auto
  finally show ?case by auto
qed

corollary ideal_generated_mult_unit2:
  assumes u: "u dvd 1"
  shows "ideal_generated {u*a,u*b} = ideal_generated {a,b}"
proof -
  let ?S = "{a,b}"
  have "ideal_generated {u*a,u*b} = ideal_generated ((λx. u*x)` {a,b})" by auto
  also have "... = ideal_generated {a,b}" by (rule ideal_generated_mult_unit[OF _ u], simp)
  finally show ?thesis .
qed

lemma ideal_generated_1[simp]: "ideal_generated {1} = UNIV"
  by (metis ideal_generated_unit dvd_ideal_generated_singleton order_refl)

lemma ideal_generated_pair: "ideal_generated {a,b} = {p*a+q*b | p q. True}"
proof -
  have i: "ideal_generated {a,b} = {y. f. (i{a,b}. f i * i) = y}" using ideal_explicit2 by auto
  show ?thesis
  proof (cases "a=b")
    case True
    show ?thesis using True i
      by (auto, metis mult_ac(2) semiring_normalization_rules)
      (metis (no_types, opaque_lifting) add_minus_cancel mult_ac ring_distribs semiring_normalization_rules)
  next
    case False
    have 1: "p q. (i{a, b}. f i * i) = p * a + q * b" for f
      by (rule exI[of _ "f a"], rule exI[of _ "f b"], rule sum_two_elements[OF False])
    moreover have "f. (i{a, b}. f i * i) = p * a + q * b" for p q
      by (rule exI[of _ "λi. if i=a then p else q"],
          unfold sum_two_elements[OF False], insert False, auto)
    ultimately show ?thesis using i by auto
  qed
qed

lemma ideal_generated_pair_exists_pq1:
  assumes i: "ideal_generated {a,b} = (UNIV::'a set)"
  shows "p q. p*a + q*b = 1"
  using i unfolding ideal_generated_pair
  by (smt (verit) iso_tuple_UNIV_I mem_Collect_eq)

lemma ideal_generated_pair_UNIV:
  assumes sa_tb_u: "s*a+t*b = u" and u: "u dvd 1"
  shows "ideal_generated {a,b} = UNIV"
proof -
  have f: "finite {a,b}" by simp
  obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def
    by (metis mult.commute)
  have "x  ideal_generated {a,b}" for x
  proof (cases "a = b")
    case True
    then show ?thesis
      by (metis UNIV_I dvd_def dvd_ideal_generated_singleton' ideal_generated_unit insert_absorb2
          mult.commute sa_tb_u semiring_normalization_rules(34) subsetI subset_antisym u)
  next
    case False note a_not_b = False
    let ?f = "λy. if y = a then inv_u * x * s else inv_u * x * t"
    have "(i{a,b}. ?f i * i) = ?f a * a + ?f b * b" by (rule sum_two_elements[OF a_not_b])
    also have "... = x" using a_not_b sa_tb_u inv_u
      by (auto, metis mult_ac(1) mult_ac(2) ring_distribs(1) semiring_normalization_rules(12))
    finally show ?thesis unfolding ideal_explicit2[OF f] by auto
  qed
  thus ?thesis by auto
qed


lemma ideal_generated_pair_exists:
  assumes l: "(ideal_generated {a,b} = ideal_generated {d})"
  shows "( p q. p*a+q*b = d)"
proof -
  have d: "d  ideal_generated {d}" by (simp add: ideal_generated_in)
  hence "d  ideal_generated {a,b}" using l by auto
  from this obtain p q where "d = p*a+q*b" using ideal_generated_pair[of a b] by auto
  thus ?thesis by auto
qed


lemma obtain_ideal_generated_pair:
  assumes "c  ideal_generated {a,b}"
  obtains p q where "p*a+q*b=c"
proof -
  have "c  {p * a + q * b |p q. True}" using assms ideal_generated_pair by auto
  thus ?thesis using that by auto
qed

lemma ideal_generated_pair_exists_UNIV:
  shows "(ideal_generated {a,b} = ideal_generated {1}) = (p q. p*a+q*b = 1)" (is "?lhs = ?rhs")
proof
  assume r: ?rhs
  have "x  ideal_generated {a,b}" for x
  proof (cases "a=b")
    case True
    then show ?thesis
      by (metis UNIV_I r dvd_ideal_generated_singleton finite.intros ideal_generated_1
          ideal_generated_pair_UNIV ideal_generated_singleton_subset)
  next
    case False
    have f: "finite {a,b}" by simp
    have 1: "1  ideal_generated {a,b}"
      using ideal_generated_pair_UNIV local.one_dvd r by blast
    hence i: "ideal_generated {a,b} = {y. f. (i{a,b}. f i * i) = y}"
      using ideal_explicit2[of "{a,b}"] by auto
    from this obtain f where f: "f a * a + f b * b = 1" using sum_two_elements 1 False by auto
    let ?f = "λy. if y = a then x * f a else x * f b"
    have "(i{a,b}. ?f i * i) = x" unfolding sum_two_elements[OF False] using f False
      using mult_ac(1) ring_distribs(1) semiring_normalization_rules(12) by force
    thus ?thesis unfolding i by auto
  qed
  thus ?lhs by auto
next
  assume ?lhs thus ?rhs using ideal_generated_pair_exists[of a b 1] by auto
qed

corollary ideal_generated_UNIV_obtain_pair:
  assumes "ideal_generated {a,b} = ideal_generated {1}"
  shows " (p q. p*a+q*b = d)"
proof -
  obtain x y where "x*a+y*b = 1" using ideal_generated_pair_exists_UNIV assms by auto
  hence "d*x*a+d*y*b=d"
    using local.mult_ac(1) local.ring_distribs(1) local.semiring_normalization_rules(12) by force
  thus ?thesis by auto
qed



lemma sum_three_elements:
  shows "x y z::'a. (i{a,b,c}. f i * i) = x * a + y * b + z * c"
proof (cases "a  b  b  c  a  c")
  case True
  then show ?thesis by (auto, metis add.assoc)
next
  case False
  have 1: "x y z. f c * c = x * c + y * c + z * c"
    by (rule exI[of _ 0],rule exI[of _ 0], rule exI[of _ "f c"], auto)
  have 2: "x y z. f b * b + f c * c = x * b + y * b + z * c"
    by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], auto)
  have 3: "x y z. f a * a + f c * c = x * a + y * c + z * c"
    by (rule exI[of _ "f a"],rule exI[of _ 0], rule exI[of _ "f c"], auto)
  have 4: "x y z. (i{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b  c"
    by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], insert a b,
        auto simp add: insert_commute)
  show ?thesis using False
    by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4)
qed

lemma sum_three_elements':
  shows "f::'a'a. (i{a,b,c}. f i * i) = x * a + y * b + z * c"
proof (cases "a  b  b  c  a  c")
  case True
  let ?f = "λi. if i = a then x else if i = b then y else if i = c then z else 0"
  show ?thesis by (rule exI[of _ "?f"], insert True mult.assoc, auto simp add: local.add_ac)
next
  case False
  have 1: "f. f c * c = x * c + y * c + z * c"
    by (rule exI[of _ "λi. if i = c then x+y+z else 0"], auto simp add: local.ring_distribs)
  have 2: "f. f a * a + f c * c = x * a + y * c + z * c" if bc: " b = c" and ac: "a  c"
    by (rule exI[of _ "λi. if i = a then x else y+z"], insert ac bc add_ac ring_distribs, auto)
  have 3: "f. f b * b + f c * c = x * b + y * b + z * c" if bc: " b  c" and ac: "a = b"
    by (rule exI[of _ "λi. if i = a then x+y else z"], insert ac bc add_ac ring_distribs, auto)
  have 4: "f. (i{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b  c"
    by (rule exI[of _ "λi. if i = c then x+z else y"], insert a b add_ac ring_distribs,
        auto simp add: insert_commute)
  show ?thesis using False
    by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4)
qed


(*This is generalizable to arbitrary sets.*)
lemma ideal_generated_triple_pair_rewrite:
  assumes i1: "ideal_generated {a, b, c} = ideal_generated {d}"
    and i2: "ideal_generated {a, b} = ideal_generated {d'}"
  shows "ideal_generated{d',c} = ideal_generated {d}"
proof
  have d': "d'  ideal_generated {a,b}" using i2 by (simp add: ideal_generated_in)
  show "ideal_generated {d', c}  ideal_generated {d}"
  proof
    fix x assume x: "x  ideal_generated {d', c}"
    obtain f1 f2 where f: "f1*d' + f2*c = x" using obtain_ideal_generated_pair[OF x] by auto
    obtain g1 g2 where g: "g1*a + g2*b = d'" using obtain_ideal_generated_pair[OF d'] by blast
    have 1: "f1*g1*a + f1*g2*b + f2*c = x"
      using f g local.ring_distribs(1) local.semiring_normalization_rules(18) by auto
    have "x  ideal_generated {a, b, c}"
    proof -
      obtain f where "(i{a,b,c}. f i * i) = f1*g1*a + f1*g2*b + f2*c"
        using sum_three_elements' 1 by blast
      moreover have "ideal_generated {a,b,c} = {y. f. (i{a,b,c}. f i * i) = y}"
        using ideal_explicit2[of "{a,b,c}"] by simp
      ultimately show ?thesis using 1 by auto
    qed
    thus "x  ideal_generated {d}" using i1 by auto
  qed
  show "ideal_generated {d}  ideal_generated {d', c}"
  proof (rule ideal_generated_singleton_subset)
    obtain f1 f2 f3 where f: "f1*a + f2*b + f3*c = d"
    proof -
      have "d  ideal_generated {a,b,c}" using i1  by (simp add: ideal_generated_in)
      from this obtain f where d: "(i{a,b,c}. f i * i) = d"
        using ideal_explicit2[of "{a,b,c}"] by auto
      obtain x y z where "(i{a,b,c}. f i * i) = x * a + y * b + z * c"
        using sum_three_elements by blast
      thus ?thesis using d that by auto
    qed
    obtain k where k: "f1*a + f2*b = k*d'"
    proof -
      have "f1*a + f2*b  ideal_generated{a,b}" using ideal_generated_pair by blast
      also have "... = ideal_generated {d'}" using i2 by simp
      also have "... = {k*d' |k. kUNIV}" using ideal_generated_singleton by auto
      finally show ?thesis using that by auto
    qed
    have "k*d'+f3*c=d" using f k by auto
    thus "d  ideal_generated {d', c}"
      using ideal_generated_pair by blast
  qed (simp)
qed

lemma ideal_generated_dvd:
  assumes i: "ideal_generated {a,b::'a} = ideal_generated{d} "
  and a: "d' dvd a" and b: "d' dvd b"
shows "d' dvd d"
proof -
  obtain p q where "p*a+q*b = d"
    using i ideal_generated_pair_exists by blast
  thus ?thesis using a b by auto
qed

lemma ideal_generated_dvd2:
  assumes i: "ideal_generated S = ideal_generated{d::'a} "
  and "finite S"
  and x: "xS. d' dvd x"
shows "d' dvd d"
  by (metis assms dvd_ideal_generated_singleton ideal_generated_dvd_subset)

end


subsection ‹An equivalent characterization of B\'ezout rings›

text ‹The goal of this subsection is to prove that a ring is B\'ezout ring if and only if every
  finitely generated ideal is principal.›

definition "finitely_generated_ideal I = (ideal I  (S. finite S  ideal_generated S = I))"

context
  assumes "SORT_CONSTRAINT('a::comm_ring_1)"
begin


lemma sum_two_elements':
  fixes d::'a
  assumes s: "(i{a,b}. f i * i) = d"
  obtains p and q where "d = p * a + q * b"
proof (cases "a=b")
  case True
  then show ?thesis
    by (metis (no_types, lifting) add_diff_cancel_left' emptyE finite.emptyI insert_absorb2
        left_diff_distrib' s sum.insert sum_singleton that)
next
  case False
  show ?thesis using s unfolding sum_two_elements[OF False]
    using that by auto
qed

text ‹This proof follows Theorem 6-3 in "First Course in Rings and Ideals" by Burton›

lemma all_fin_gen_ideals_are_principal_imp_bezout:
  assumes all: "I::'a set. finitely_generated_ideal I  principal_ideal I"
  shows "OFCLASS ('a, bezout_ring_class)"
proof (intro_classes)
  fix a b::'a
  obtain d where ideal_d: "ideal_generated {a,b} = ideal_generated {d}"
    using all unfolding finitely_generated_ideal_def
    by (metis finite.emptyI finite_insert ideal_ideal_generated principal_ideal_def)
  have a_in_d: "a  ideal_generated {d}"
    using ideal_d ideal_generated_subset_generator by blast
  have b_in_d: "b  ideal_generated {d}"
    using ideal_d ideal_generated_subset_generator by blast
  have d_in_ab: "d  ideal_generated {a,b}"
    using ideal_d ideal_generated_subset_generator by auto
  obtain f where "(i{a,b}. f i * i) = d" using obtain_sum_ideal_generated[OF d_in_ab] by auto
  from this obtain p q where d_eq: "d = p*a + q*b" using sum_two_elements' by blast
  moreover have d_dvd_a: "d dvd a"
    by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset insert_commute
        subset_insertI)
  moreover have "d dvd b"
    by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset subset_insertI)
  moreover have "d' dvd d" if d'_dvd: "d' dvd a  d' dvd b" for d'
  proof -
    obtain s1 s2 where s1_dvd: "a = s1*d'" and s2_dvd: "b = s2*d'"
      using mult.commute d'_dvd unfolding dvd_def by auto
    have "d = p*a + q*b" using d_eq .
    also have "...= p * s1 * d' + q * s2 *d'" unfolding s1_dvd s2_dvd by auto
    also have "... = (p * s1 + q * s2) * d'" by (simp add: ring_class.ring_distribs(2))
    finally show "d' dvd d" using mult.commute unfolding dvd_def by auto
  qed
  ultimately 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)" by auto
qed
end


context bezout_ring
begin

lemma exists_bezout_extended:
  assumes S: "finite S" and ne: "S  {}"
  shows "f d. (aS. f a * a) = d  (aS. d dvd a)  (d'. (aS. d' dvd a)  d' dvd d)"
  using S ne
proof (induct S)
  case empty
  then show ?case by auto
next
  case (insert x S)
  show ?case
  proof (cases  "S={}")
    case True
    let ?f = "λx. 1"
    show ?thesis by (rule exI[of _ ?f], insert True, auto)
  next
    case False note ne = False
    note x_notin_S = insert.hyps(2)
    obtain f d where sum_eq_d: "(aS. f a * a) = d"
      and d_dvd_each_a: "(aS. d dvd a)"
      and d_is_gcd: "(d'. (aS. d' dvd a)  d' dvd d)"
      using insert.hyps(3)[OF ne] by auto
    have "p q d'. p * d + q * x = d'  d' dvd d  d' dvd x  (c. c dvd d  c dvd x  c dvd d')"
      using exists_bezout by auto
    from this obtain p q d' where pd_qx_d': "p*d + q*x = d'"
      and d'_dvd_d: "d' dvd d" and d'_dvd_x: "d' dvd x"
      and d'_dvd: "c. (c dvd d  c dvd x)  c dvd d'" by blast
    let ?f = "λa. if a = x then q else p * f a"
    have "(ainsert x S. ?f a * a) = d'"
    proof -
      have "(ainsert x S. ?f a * a) = (aS. ?f a * a) + ?f x * x"
        by (simp add: add_commute insert.hyps(1) insert.hyps(2))
      also have "... = p * (aS. f a * a) + q * x"
        unfolding sum_distrib_left
        by (auto, rule sum.cong, insert x_notin_S,
            auto simp add: mult.semigroup_axioms semigroup.assoc)
      finally show ?thesis using pd_qx_d' sum_eq_d by auto
    qed
    moreover have "(ainsert x S. d' dvd a)"
      by (metis d'_dvd_d d'_dvd_x d_dvd_each_a insert_iff local.dvdE local.dvd_mult_left)
    moreover have " (c. (ainsert x S. c dvd a)  c dvd d')"
      by (simp add: d'_dvd d_is_gcd)
    ultimately show ?thesis by auto
  qed
qed

end

lemma ideal_generated_empty: "ideal_generated {} = {0}"
  unfolding ideal_generated_def using ideal_generated_0
  by (metis empty_subsetI ideal_generated_def ideal_generated_subset ideal_ideal_generated
      ideal_not_empty subset_singletonD)


lemma bezout_imp_all_fin_gen_ideals_are_principal:
  fixes I::"'a :: bezout_ring set"
  assumes fin: "finitely_generated_ideal I"
  shows "principal_ideal I"
proof -
  obtain S where fin_S: "finite S" and ideal_gen_S: "ideal_generated S = I"
    using fin unfolding finitely_generated_ideal_def by auto
  show ?thesis
  proof (cases "S = {}")
    case True
    then show ?thesis
      using ideal_gen_S unfolding True
      using ideal_generated_empty ideal_generated_0 principal_ideal_def by fastforce
  next
    case False note ne = False
    obtain d f where sum_S_d: "(iS. f i * i) = d"
    and d_dvd_a: "(aS. d dvd a)" and d_is_gcd: "(d'. (aS. d' dvd a)  d' dvd d)"
      using exists_bezout_extended[OF fin_S ne] by auto
    have d_in_S: "d  ideal_generated S"
      by (metis fin_S ideal_def ideal_generated_subset_generator
          ideal_ideal_generated sum_S_d sum_left_ideal)
    have "ideal_generated {d}  ideal_generated S"
      by (rule ideal_generated_singleton_subset[OF d_in_S fin_S])
    moreover have "ideal_generated S  ideal_generated {d}"
    proof
      fix x assume x_in_S: "x  ideal_generated S"
      obtain f where sum_S_x: "(aS. f a * a) = x"
        using fin_S obtain_sum_ideal_generated x_in_S by blast
      have d_dvd_each_a: "k. a = k * d" if "a  S" for a
        by (metis d_dvd_a dvdE mult.commute that)
      let ?g = "λa. SOME k. a = k*d"
      have "x = (aS. f a * a)" using sum_S_x by simp
      also have "... = (aS. f a * (?g a * d))"
      proof (rule sum.cong)
        fix a assume a_in_S: "a  S"
        obtain k where a_kd: "a = k * d" using d_dvd_each_a a_in_S by auto
        have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd)
        thus "f a * a = f a * ((SOME k. a = k * d) * d)" by auto
      qed (simp)
      also have "... = (aS. f a * ?g a * d)" by (rule sum.cong, auto)
      also have "... = (aS. f a * ?g a)*d" using sum_distrib_right[of _ S d] by auto
      finally show "x  ideal_generated {d}"
        by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right
            ideal_generated_in singletonI)
    qed
    ultimately show ?thesis unfolding principal_ideal_def using ideal_gen_S by auto
  qed
qed

text ‹Now we have the required lemmas to prove the theorem that states that
  a ring is B\'ezout ring if and only if every
  finitely generated ideal is principal. They are the following ones.

\begin{itemize}
\item @{text "all_fin_gen_ideals_are_principal_imp_bezout"}
\item @{text "bezout_imp_all_fin_gen_ideals_are_principal"}
\end{itemize}

However, in order to prove the final lemma, we need the lemmas with no type restrictions.
For instance, we need a version of theorem @{text "bezout_imp_all_fin_gen_ideals_are_principal"}
as

@{text "OFCLASS('a,bezout_ring) ⟹"} the theorem with generic types
  (i.e., @{text "'a"} with no type restrictions)


or as

@{text "class.bezout_ring _ _ _ _ ⟹"} the theorem with generic
  types (i.e., @{text "'a"} with no type restrictions)
›

(*A possible workaround is to adapt the proof*)
(*
lemma bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory:
  assumes a1: "class.bezout_ring ( * ) (1::'a::comm_ring_1) (+) 0 (-) uminus" (*Me da igual esto que OFCLASS*)
  shows "∀I::'a set. finitely_generated_ideal I ⟶ principal_ideal I"
proof (rule allI, rule impI)
  fix I::"'a set" assume fin: "finitely_generated_ideal I"
  interpret a: bezout_ring "( * )" "(1::'a)" "(+)" 0 "(-)" uminus using a1 .
  interpret dvd "( * )::'a⇒'a⇒'a" .
  interpret b: comm_monoid_add "(+)" "(0::'a)" using a1 by intro_locales
  have c: " class.comm_monoid_add (+) (0::'a)"  using a1 by intro_locales
  have [simp]: "(dvd.dvd ( * ) d a) = (d dvd a)" for d a::'a
    by (auto simp add: dvd.dvd_def dvd_def)
  have [simp]: "comm_monoid_add.sum (+) 0 (λa. f a * a) S = sum (λa. f a * a) S"
    for f and S::"'a set"
    unfolding sum_def unfolding comm_monoid_add.sum_def[OF c] ..
  obtain S where fin_S: "finite S" and ideal_gen_S: "ideal_generated S = I"
    using fin unfolding finitely_generated_ideal_def by auto
  show "principal_ideal I"
  proof (cases "S = {}")
    case True
    then show ?thesis
      using ideal_gen_S unfolding True
      using ideal_generated_empty ideal_generated_0 principal_ideal_def by fastforce
  next
    case False note ne = False
    obtain d f where sum_S_d: "(∑i∈S. f i * i) = d"
    and d_dvd_a: "(∀a∈S. d dvd a)" and d_is_gcd: "(∀d'. (∀a∈S. d' dvd a) ⟶ d' dvd d)"
      using a.exists_bezout_extended[OF fin_S ne] by auto
    have d_in_S: "d ∈ ideal_generated S"
      by (metis fin_S ideal_def ideal_generated_subset_generator
          ideal_ideal_generated sum_S_d sum_left_ideal)
    have "ideal_generated {d} ⊆ ideal_generated S"
      by (rule ideal_generated_singleton_subset[OF d_in_S fin_S])
    moreover have "ideal_generated S ⊆ ideal_generated {d}"
    proof
      fix x assume x_in_S: "x ∈ ideal_generated S"
      obtain f where sum_S_x: "(∑a∈S. f a * a) = x"
        using fin_S obtain_sum_ideal_generated x_in_S by blast
      have d_dvd_each_a: "∃k. a = k * d" if "a ∈ S" for a
        by (metis d_dvd_a dvdE mult.commute that)
      let ?g = "λa. SOME k. a = k*d"
      have "x = (∑a∈S. f a * a)" using sum_S_x by simp
      also have "... = (∑a∈S. f a * (?g a * d))"
      proof (rule sum.cong)
        fix a assume a_in_S: "a ∈ S"
        obtain k where a_kd: "a = k * d" using d_dvd_each_a a_in_S by auto
        have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd)
        thus "f a * a = f a * ((SOME k. a = k * d) * d)" by auto
      qed (simp)
      also have "... = (∑a∈S. f a * ?g a * d)" by (rule sum.cong, auto)
      also have "... = (∑a∈S. f a * ?g a)*d" using sum_distrib_right[of _ S d] by auto
      finally show "x ∈ ideal_generated {d}"
        by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right
            ideal_generated_in singletonI)
    qed
    ultimately show ?thesis unfolding principal_ideal_def using ideal_gen_S by auto
  qed
qed
*)

text ‹Thanks to local type definitions, we can obtain it automatically by means
  of @{text "internalize-sort"}.›

lemma bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory:
  assumes a1: "class.bezout_ring (*) (1::'b::comm_ring_1) (+) 0 (-) uminus" (*It is algo possible to prove it using OFCLASS*)
  shows "I::'b set. finitely_generated_ideal I  principal_ideal I"
  using bezout_imp_all_fin_gen_ideals_are_principal[internalize_sort "'a::bezout_ring"]
  using a1 by auto


text ‹The standard library does not connect @{text "OFCLASS"} and @{text "class.bezout_ring"}
in both directions. Here we show that @{text "OFCLASS ⟹ class.bezout_ring"}. ›

lemma OFCLASS_bezout_ring_imp_class_bezout_ring:
  assumes "OFCLASS('a::comm_ring_1,bezout_ring_class)"
  shows "class.bezout_ring ((*)::'a'a'a) 1 (+) 0 (-) uminus"
  using assms
  unfolding bezout_ring_class_def class.bezout_ring_def
  using conjunctionD2[of "OFCLASS('a, comm_ring_1_class)"
                         "class.bezout_ring_axioms ((*)::'a'a'a) (+)"]
  by (auto, intro_locales)

text ‹The other implication can be obtained
  by thm @{text bezout_ring.intro_of_class}
thm bezout_ring.intro_of_class


(*OFCLASS is a proposition (Prop), and then the following statement is not valid.*)

(*
lemma
  shows "(∀I::'a::comm_ring_1 set. finitely_generated_ideal I ⟶ principal_ideal I)
    = OFCLASS('a, bezout_ring_class)"
*)

(*Thus, we use the meta-equality and the meta universal quantifier.*)
text ‹Final theorem (with OFCLASS)›
lemma bezout_ring_iff_fin_gen_principal_ideal:
    "(I::'a::comm_ring_1 set. finitely_generated_ideal I  principal_ideal I)
     OFCLASS('a, bezout_ring_class)"
proof
  show "(I::'a::comm_ring_1 set. finitely_generated_ideal I  principal_ideal I)
     OFCLASS('a, bezout_ring_class)"
    using all_fin_gen_ideals_are_principal_imp_bezout [where ?'a='a] by auto
  show "I::'a::comm_ring_1 set. OFCLASS('a, bezout_ring_class)
     finitely_generated_ideal I  principal_ideal I"
    using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory[where ?'b='a]
    using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a] by auto
qed

text ‹Final theorem (with @{text "class.bezout_ring"})›

lemma bezout_ring_iff_fin_gen_principal_ideal2:
    "(I::'a::comm_ring_1 set. finitely_generated_ideal I  principal_ideal I)
    = (class.bezout_ring ((*)::'a'a'a) 1 (+) 0 (-) uminus)"
proof
  show "I::'a::comm_ring_1 set. finitely_generated_ideal I  principal_ideal I
       class.bezout_ring (*) 1 (+) (0::'a) (-) uminus"
    using all_fin_gen_ideals_are_principal_imp_bezout[where ?'a='a]
    using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a]
    by auto
  show "class.bezout_ring (*) 1 (+) (0::'a) (-) uminus  I::'a set.
    finitely_generated_ideal I  principal_ideal I"
    using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory by auto
qed

end