Theory Examples_Noetherian_Rings

section ‹Examples›
theory Examples_Noetherian_Rings

imports 
  "Hilbert_Basis" 
  Real_Ring_Definition
begin

subsection ‹Examples of noetherian rings with ‹ℤ› and ‹ℤ[X]››
lemma INTEG_euclidean_domain:‹euclidean_domain INTEG (λx. nat (abs x))›
  apply(rule domain.euclidean_domainI)
  unfolding domain_def domain_axioms_def using INTEG_cring apply(simp add:INTEG_def)
  unfolding INTEG_def 
  using abs_mod_less div_mod_decomp_int mult.commute 
  by (metis Diff_iff INTEG.R.r_null INTEG_def INTEG_mult UNIV_I abs_ge_zero insert_iff 
      mult_zero_left nat_less_eq_zless partial_object.select_convs(1) ring_record_simps(12))


lemma principal_ideal_INTEG:‹ideal I INTEG ⟹ principalideal I INTEG›
proof(rule principalidealI)
  assume h:‹ideal I INTEG›
  then show ‹ideal I INTEG› by(simp)
  {assume h1:‹I ≠ {0}›
    define E where imp:‹E≡{nat (abs x)|x. x∈I ∧ x≠0}›
    then have ‹E≠{}› 
      using h h1 additive_subgroup.zero_closed unfolding ideal_def 
      by fastforce
    then have ‹∃n∈E. ∀x∈E. n≤x ∧ n>0›
      using abs_ge_zero imp zero_less_abs_iff 
      by (smt (verit) all_not_in_conv exists_least_iff gr_zeroI leI mem_Collect_eq nat_0_iff)
    define E' where imp2:‹E'≡{(abs x)|x. x∈I ∧ x≠0}›
    then have ‹bij_betw nat E' E›
      unfolding bij_betw_def
      apply(safe) 
      using inj_on_def apply force
      using imp apply blast
      using imp by blast
    then have ‹∃n∈E'. ∀x∈E'. n≤x ∧ n>0› 
      by (smt (verit, best) ‹∃n∈E. ∀x∈E. n ≤ x ∧ 0 < n› 
          bij_betw_iff_bijections le_nat_iff nat_eq_iff2 nat_le_iff zero_less_nat_eq) 
    then obtain n where f1:‹∀x∈E'. n≤x ∧ n>0 ∧ n∈E'› by blast
    then have ‹∃a∈I. abs a =  n› 
      using ‹∃n∈E'. ∀x∈E'. n ≤ x ∧ 0 < n› imp2 by blast 
    then obtain a where f0:‹a∈I ∧ abs a =  n› by blast
    then have ‹∀x. ∃q r. x = a*q+r ∧ abs r < abs a›
      using INTEG_euclidean_domain unfolding euclidean_domain_def 
      by (metis ‹∃n∈E'. ∀x∈E'. n ≤ x ∧ 0 < n› ‹∀x∈E'. n ≤ x ∧ 0 < n ∧ n ∈ E'› 
          abs_mod_less div_mod_decomp_int mult.commute zero_less_abs_iff)
    then have f2:‹x∈I∧ r =x - a*q ⟹ r∈I› for q r x
      using h unfolding ideal_def INTEG_def additive_subgroup_def subgroup_def ideal_axioms_def
        ring_def apply(safe, simp)
      by (metis ‹a ∈ I ∧ ¦a¦ = n› integer_group_def inv_integer_group uminus_add_conv_diff)
    have f3:‹x∈I∧ r =x - a*q ⟹ abs r < abs a ⟹ r = 0› for r q x 
      apply(frule f2)
      using imp2 f1 f0
      by fastforce
    have ‹x∈I∧ r =x - a*q ⟹ abs r < abs a ⟹ x ∈ Idl⇘INTEG⇙ {a}›
      for x r q 
      apply(frule f3)
       apply blast
      unfolding genideal_def ideal_def INTEG_def additive_subgroup_def 
        subgroup_def ideal_axioms_def by(auto)
    then have ‹x∈I ⟹ x ∈ Idl⇘INTEG⇙ {a}›   for x
      by (metis ‹∀x. ∃q r. x = a * q + r ∧ ¦r¦ < ¦a¦› add_diff_cancel_left')
    then have ‹ideal I INTEG ⟹ ∃i∈carrier INTEG. I = Idl⇘INTEG⇙ {i}›
      using INTEG.R.cgenideal_eq_genideal INTEG.R.cgenideal_minimal f0 by blast
  }note non_trivial_ideal=this
  show ‹∃i∈carrier INTEG. I = Idl⇘INTEG⇙ {i}›
    apply(cases ‹I={0}›) 
     apply (metis INTEG.R.genideal_self 
        INTEG.R.ring_axioms INTEG_closed h ring.Idl_subset_ideal subsetI subset_antisym)
    using non_trivial_ideal h by auto
qed


lemma INTEG_noetherian_ring:‹noetherian_ring INTEG›
  apply(rule ring.noetherian_ringI)
   apply (simp add: INTEG.R.ring_axioms)
  using principal_ideal_INTEG unfolding principalideal_def
  by (meson INTEG_closed finite.emptyI finite_insert principalideal_axioms_def subsetI)

lemma INTEG_noetherian_domain:‹noetherian_domain INTEG›
  unfolding noetherian_domain_def 
  using INTEG_noetherian_ring INTEG_euclidean_domain euclidean_domain.axioms(1) by blast

lemma Polynomials_INTEG_noetherian_ring:‹noetherian_ring (univ_poly INTEG (carrier INTEG))›
  by (simp add: INTEG_noetherian_domain noetherian_domain.weak_Hilbert_basis)

lemma Polynomials_INTEG_noetherian_domain: ‹noetherian_domain (univ_poly INTEG (carrier INTEG))›
  using INTEG.R.ring_axioms INTEG_noetherian_domain Polynomials_INTEG_noetherian_ring 
    domain.univ_poly_is_domain noetherian_domain.axioms(2) noetherian_domain.intro 
    ring.carrier_is_subring by blast



subsection ‹Another example with ‹ℝ› and ‹ℝ[X]››

lemma REAL_noetherian_domain:‹noetherian_domain REAL›
  unfolding noetherian_domain_def 
  by (simp add: REAL_field domain.noetherian_RX_imp_noetherian_R domain.univ_poly_is_principal 
      field.axioms(1) field.carrier_is_subfield principal_imp_noetherian)

lemma PolyREAL_noetherian_domain:‹noetherian_domain (univ_poly REAL (carrier REAL))›
  unfolding noetherian_domain_def 
  by (simp add: REAL_field REAL_noetherian_domain REAL_ring domain.univ_poly_is_domain 
      field.axioms(1) noetherian_domain.weak_Hilbert_basis ring.carrier_is_subring)


end