Theory Hilbert_Basis

section ‹The Hilbert Basis theorem for Indexed Polynomials Rings›
theory Hilbert_Basis

imports "Weak_Hilbert_Basis" 

begin 

subsection ‹The isomorphism between ‹A[X⇩0..X⇩n] and A[X⇩0..X⇩n⇩-⇩1][X⇩n]››

text ‹This part until $var_factor_iso$ is due to Aaron Crighton›
lemma ring_iso_memI': 
  assumes "f ∈ ring_hom R S"
  assumes "g ∈ ring_hom S R"
  assumes "⋀ x. x ∈ carrier R ⟹ g (f x) = x"
  assumes "⋀ x. x ∈ carrier S ⟹ f (g x) = x"
  shows "f ∈ ring_iso R S"
    "g ∈ ring_iso S R"
proof- 
  show 0: "f ∈ ring_iso R S"
    unfolding ring_iso_def mem_Collect_eq
    apply(rule conjI, rule assms(1), rule bij_betwI[of _ _ _ g])
    using assms ring_hom_memE by auto 
  show "g ∈ ring_iso S R"
    unfolding ring_iso_def mem_Collect_eq
    apply(rule conjI, rule assms(2), rule bij_betwI[of _ _ _ f])
    using assms ring_hom_memE by auto 
qed


lemma(in cring) var_factor_inverse:
  assumes "I = J0 ∪ J1"
  assumes "J1 ⊆ I"
  assumes "J1 ∩ J0 = {}"
  assumes "ψ1 = (var_factor_inv I J0 J1)"
  assumes "ψ0 = (var_factor I J0 J1)"
  assumes "P ∈ carrier (Pring (Pring R J0) J1)"
  shows "ψ0 (ψ1 P) = P"
proof(induct rule: ring.Pring_car_induct''[of "Pring R J0" _ J1])
  case 1
  then show ?case 
    using Pring_is_ring by blast 
next
  case 2
  then show ?case 
    using assms(6) by force
next
  case (3 c)
  interpret pring_cring: cring "Pring R J0"
    using Pring_is_cring is_cring by auto 
  interpret Rcring: cring R
    using is_cring by auto 
  have 0: "ring_hom_ring (Pring (Pring R J0) J1) (Pring R I) ψ1"
    by (simp add: assms(1) assms(3) assms(4) var_factor_inv_morphism(1)) 
  have 1: "ring_hom_ring (Pring R I) (Pring (Pring R J0) J1) ψ0"
    by (simp add: assms(1) assms(3) assms(5) var_factor_morphism'(1))
  have 2: "ψ0 ∘ ψ1 ∈ ring_hom (Pring (Pring R J0) J1) (Pring (Pring R J0) J1) "
    using 0 1 ring_hom_trans[of ψ1 "Pring (Pring R J0) J1" "Pring R I" ψ0 "Pring (Pring R J0) J1"]
      ring_hom_ring.homh[of "Pring R I" "Pring (Pring R J0) J1" ψ0]
      ring_hom_ring.homh[of "Pring (Pring R J0) J1" "Pring R I" ψ1]
    by blast
  then show ?case using assms 
    by (simp add: 3 var_factor_inv_morphism(3) var_factor_morphism'(3))
next
  case (4 p q)
  interpret pring_cring: cring "Pring R J0"
    using Pring_is_cring is_cring by auto 
  interpret Rcring: cring R
    using is_cring by auto 
  have 0: "ring_hom_ring (Pring (Pring R J0) J1) (Pring R I) ψ1"
    by (simp add: assms(1) assms(3) assms(4) var_factor_inv_morphism(1)) 
  have 1: "ring_hom_ring (Pring R I) (Pring (Pring R J0) J1) ψ0"
    by (simp add: assms(1) assms(3) assms(5) var_factor_morphism'(1))
  have 2: "ψ0 ∘ ψ1 ∈ ring_hom (Pring (Pring R J0) J1) (Pring (Pring R J0) J1) "
    using 0 1 ring_hom_trans[of ψ1 "Pring (Pring R J0) J1" "Pring R I" ψ0 "Pring (Pring R J0) J1"]
      ring_hom_ring.homh[of "Pring R I" "Pring (Pring R J0) J1" ψ0]
      ring_hom_ring.homh[of "Pring (Pring R J0) J1" "Pring R I" ψ1]
    by blast
  from 4 show ?case  
  proof- 
    fix p q
    assume A: "p ∈ carrier (Pring (Pring R J0) J1)"
      "q ∈ carrier (Pring (Pring R J0) J1)"
      "ψ0 (ψ1 p) = p"
      "ψ0 (ψ1 q) = q"
    show "ψ0 (ψ1 (p ⊕⇘Pring (Pring R J0) J1⇙ q)) = p ⊕⇘Pring (Pring R J0) J1⇙ q"
      using A 2 ring_hom_add[of "ψ0 ∘ ψ1" "Pring (Pring R J0) J1" "Pring (Pring R J0) J1" p q]
        comp_apply[of ψ0 ψ1]
      by (simp add: pring_cring.Pring_add pring_cring.Pring_car)
  qed
next
  case (5 p i)
  interpret pring_cring: cring "Pring R J0"
    using Pring_is_cring is_cring by auto 
  interpret Rcring: cring R
    using is_cring by auto 
  have 0: "ring_hom_ring (Pring (Pring R J0) J1) (Pring R I) ψ1"
    by (simp add: assms(1) assms(3) assms(4) var_factor_inv_morphism(1)) 
  have 1: "ring_hom_ring (Pring R I) (Pring (Pring R J0) J1) ψ0"
    by (simp add: assms(1) assms(3) assms(5) var_factor_morphism'(1))
  have 2: "ψ0 ∘ ψ1 ∈ ring_hom (Pring (Pring R J0) J1) (Pring (Pring R J0) J1) "
    using 0 1 ring_hom_trans[of ψ1 "Pring (Pring R J0) J1" "Pring R I" ψ0 "Pring (Pring R J0) J1"]
      ring_hom_ring.homh[of "Pring R I" "Pring (Pring R J0) J1" ψ0]
      ring_hom_ring.homh[of "Pring (Pring R J0) J1" "Pring R I" ψ1]
    by blast
  from 5 show ?case 
  proof-
    fix p i assume A: "p ∈ carrier (Pring (Pring R J0) J1)"
      "ψ0 (ψ1 p) = p"
      "i ∈ J1"
    show " ψ0 (ψ1 (p ⊗⇘Pring (Pring R J0) J1⇙ pvar (Pring R J0) i)) =
         p ⊗⇘Pring (Pring R J0) J1⇙ pvar (Pring R J0) i"              
    proof- 
      have A1: "ψ0 (ψ1 (pvar (Pring R J0) i)) = pvar (Pring R J0) i"
        by (metis A(3) assms(1) assms(2) assms(3) assms(4) assms(5) 
            var_factor_inv_morphism(2) var_factor_morphism'(2)) 
      then show ?thesis
        using 2  A ring_hom_mult[of "ψ0 ∘ ψ1" "(Pring (Pring R J0) J1)"] 2
          Pring_car  comp_apply[of ψ0 ψ1] 
        by (metis pring_cring.Pring_car pring_cring.Pring_var_closed)
    qed
  qed
qed


lemma(in cring) var_factor_iso:
  assumes "I = J0 ∪ J1"
  assumes "J1 ⊆ I"
  assumes "J1 ∩ J0 = {}"
  assumes "ψ1 = (var_factor_inv I J0 J1)"
  assumes "ψ0 = (var_factor I J0 J1)"
  shows "ψ0 ∈ ring_iso (Pring R I) (Pring (Pring R J0) J1)"
    "ψ1 ∈ ring_iso (Pring (Pring R J0) J1)(Pring R I)"
proof- 
  have 1: "ψ0 ∈ ring_hom (Pring R I) (Pring (Pring R J0) J1)"
    "ψ1 ∈ ring_hom (Pring (Pring R J0) J1) (Pring R I)"
    "⋀x. x ∈ carrier (Pring R I) ⟹ ψ1 (ψ0 x) = x"
    "⋀x. x ∈ carrier (Pring (Pring R J0) J1) ⟹ ψ0 (ψ1 x) = x"
    using assms var_factor_inv_inverse[of I  J0 J1 ψ1] var_factor_inverse[of I  J0 J1 ψ1]
    by (auto simp add: var_factor_inv_morphism(1) cring.var_factor_morphism'(1) is_cring 
        ring_hom_ring.homh)
  show "ψ0 ∈ ring_iso (Pring R I) (Pring (Pring R J0) J1)"
    "ψ1 ∈ ring_iso (Pring (Pring R J0) J1) (Pring R I) "
    using 1 ring_iso_memI'[of ψ0 "Pring R I" "Pring (Pring R J0) J1"  ψ1  ] 
    by auto 
qed


lemma (in cring) is_iso_Prings:
  assumes h1:"I = J0 ∪ J1"
  assumes h2:"J1 ⊆ I"
  assumes h3:"J1 ∩ J0 = {}"
  shows "(Pring (Pring R J0) J1) ≃ (Pring R I)" and "(Pring R I) ≃ (Pring (Pring R J0) J1)"
proof -
  show ‹(Pring (Pring R J0) J1) ≃ (Pring R I)› 
    unfolding is_ring_iso_def 
    using h2 var_factor_iso[of I J0 J1 ‹var_factor_inv I J0 J1› ‹var_factor I J0 J1›]
    using h1 h3 by auto
  show ‹(Pring R I) ≃ (Pring (Pring R J0) J1)› 
    unfolding is_ring_iso_def 
    using h2 var_factor_iso[of I J0 J1 ‹var_factor_inv I J0 J1› ‹var_factor I J0 J1›]
    using h1 h3 by auto
qed

subsection ‹Preliminaries lemmas›
lemma (in cring) poly_no_var:
  assumes ‹x ∈ ((carrier R) [𝒳⇘{}⇙]) ∧ xa ≠ {#}›
  shows ‹x xa = 𝟬›
  apply(rule ring.Pring_car_induct''[of "R" x ‹{}›])
      apply (simp add: local.ring_axioms)
     apply (simp add: Pring_car assms)
  unfolding indexed_const_def using assms 
  by(auto simp add: Pring_add indexed_padd_def) 


lemma (in cring) R_isom_P_mt:‹R ≃ Pring R {}› 
proof -
  interpret cringP: cring "Pring R {}"
    by (simp add: Pring_is_cring is_cring)
  have f0:‹bij_betw indexed_const (carrier R) (carrier (Pring R {}))›
  proof(unfold bij_betw_def inj_on_def, safe)
    fix x y
    assume h1:‹x ∈ carrier R›‹y ∈ carrier R›‹indexed_const x = indexed_const y›
    show ‹indexed_const x = indexed_const y ⟹ x = y›
      by (metis indexed_const_def)
  next
    fix x xa
    assume h1:‹xa ∈ carrier R›
    show ‹indexed_const xa ∈ carrier (Pring R {})›
      by (simp add: h1 indexed_const_closed)
  next
    fix x::‹'f multiset ⇒ 'a›
    assume h1:‹x ∈ carrier (Pring R {})›
    then show ‹x ∈ indexed_const ` carrier R›
      unfolding image_def apply(safe)
      apply(rule bexI[where x=‹x {#}›])
      unfolding indexed_const_def
      by (auto simp:fun_eq_iff Pring_def poly_no_var)
  qed
  show ?thesis
    unfolding is_ring_iso_def ring_iso_def 
    apply(subst ex_in_conv[symmetric])
    unfolding ring_hom_def
    apply(rule exI[where  x="indexed_const"])
    apply(safe)
        apply (simp add: indexed_const_closed)
       apply (simp add: indexed_const_mult)
    using  cringP.indexed_padd_const 
      apply (simp add: Pring_add indexed_padd_const)
     apply (simp add: Pring_one)
    by(simp add:f0)
qed

subsection ‹Hilbert Basis theorem›
text ‹We show after this Hilbert basis theorem, based on Indexed Polynomials in HOL-Algebra
and its extension in $Padic_Fields$›

theorem (in domain) Hilbert_basis:
  assumes h1:‹noetherian_ring R› and h2:‹finite I›
  shows ‹noetherian_ring (Pring R I)›
proof(induct rule :finite.induct[OF h2])
  case 1
  interpret cringP: cring "Pring R {}"
    by (simp add: Pring_is_cring is_cring)
  show ?case 
    using R_isom_P_mt cringP.ring_axioms h1 noetherian_isom_imp_noetherian by auto
next
  case (2 A a)
  have f0:‹noetherian_ring (Pring R A)› 
    using 2 by blast
  have f1:‹cring (Pring R A)›
    using Pring_is_cring is_cring by auto
  interpret UPcring: UP_cring "Pring R A" "UP (Pring R A)"
    by (simp add: UP_cring.intro f1)+
  have f2:‹Pring (Pring R A) {a} ≃ UP (Pring R A)›
    using cring.Pring_one_index_isom_P UP_cring_def f1 
    by (simp add: UPcring.R.Pring_one_index_isom_P)
  then have f3:‹noetherian_ring (UP (Pring R A))› 
    using Pring_is_domain domain.noetherian_R_imp_noetherian_UP_R f0 by blast
  have f7:‹cring (Pring (Pring R A) {a})›
    by (simp add: UPcring.R.Pring_is_cring f1)
  then have ‹UP (Pring R A) ≃ Pring (Pring R A) {a}›
    by (simp add: cring_def f2 ring_iso_sym)
  have f6:‹noetherian_ring (Pring (Pring R A) {a})›
    using ‹UP (Pring R A) ≃ Pring (Pring R A) {a}› cring.axioms(1) f3 
      f7 noetherian_isom_imp_noetherian by auto
  have f10:‹a∉A ⟹ Pring (Pring R A) {a} ≃ (Pring R (insert a A))›
    apply(rule cring.is_iso_Prings(1))
    by (simp add: is_cring)+
  have f11:‹ring (Pring R (insert a A))›
    by (simp add: Pring_is_ring)
  then show ?case 
    apply(cases ‹a∈A›)
    using f0 
     apply (simp add: insert_absorb)
    using noetherian_isom_imp_noetherian[of ‹Pring (Pring R A) {a}› 
        ‹(Pring R (insert a A))›] f10 f11 f6 by(simp)
qed

lemma (in domain) R_noetherian_implies_IP_noetherian:
  assumes h1:‹noetherian_ring R› 
  shows ‹noetherian_ring (Pring R {0..N::nat})›
  using Hilbert_basis h1 by blast

lemma (in domain) IP_noetherian_implies_R_noetherian:
  assumes h1:‹noetherian_ring (Pring R I)› and h2:‹finite I›
  shows ‹noetherian_ring R›
proof(insert h1, induct rule:finite.induct[OF h2])
  case 1
  interpret cringP: cring "Pring R {}"
    by (simp add: Pring_is_cring is_cring)
  have ‹Pring R {} ≃ R›
    using local.ring_axioms R_isom_P_mt ring_iso_sym by blast
  then show ?case 
    using "1" local.ring_axioms noetherian_isom_imp_noetherian by blast
next
  case (2 A a)
  have f1:‹cring (Pring R A)›
    using Pring_is_cring is_cring by auto
  interpret UPcring: UP_cring "Pring R A" "UP (Pring R A)"
    by (simp add: UP_cring.intro f1)+
  interpret dom: domain "(Pring R (A))"
    using Pring_is_domain by blast
  have f2:‹Pring (Pring R A) {a} ≃ UP (Pring R A)›
    using cring.Pring_one_index_isom_P UP_cring_def f1 
    by (simp add: UPcring.R.Pring_one_index_isom_P)
  {assume h2:‹a∉A›
    then have ‹ (Pring (Pring R (A)) {a}) ≃ (Pring R (insert a A))›
      by (simp add: cring.is_iso_Prings(1) is_cring)
    then have ‹noetherian_ring (Pring (Pring R (A)) {a})› 
      using "2.prems" UPcring.R.Pring_is_ring 
        noetherian_isom_imp_noetherian ring_iso_sym by blast
    then have ‹noetherian_ring (Pring R (A))›
      by (simp add: dom.IP_noeth_imp_R_noeth)
    then have ‹noetherian_ring R› 
      using "2.hyps"(2) by blast}note a_not_in=this
  then show ?case apply(cases ‹a∈A›)
    using 2 
     apply (simp add: insert_absorb)
    using a_not_in by blast
qed



end