Theory Hilbert_Basis_Introduction

(*<*)
theory Hilbert_Basis_Introduction
  imports Main

begin
(*>*)


section‹A Proof of Hilbert Basis Theorems and 
          an Extension to Formal Power Series›

text‹
The Hilbert Basis Theorem is enlisted in the extension of Wiedijk's 
catalogue "Formalizing 100 Theorems" \cite{source3} , a well-known collection 
of challenge problems for the formalisation of mathematics.

In this paper, we present a formal proof of several versions
of this theorem in Isabelle/HOL. Hilbert's basis theorem asserts that 
every ideal of a polynomial ring over a commutative ring has a finite generating 
family (a finite basis in Hilbert's terminology). 
A prominent alternative formulation is:
every polynomial ring over a Noetherian ring is also Noetherian.

In more detail, the statement and our generalization can be presented as follows:

  ▪ ❙‹Hilbert's Basis Theorem.› Let ‹ℜ[X]› denote the ring of polynomials in the indeterminate ‹X› 
  over the commutative ring ‹ℜ›. Then ‹ℜ[X]› is Noetherian iff ‹ℜ› is.
  ▪ ❙‹Corrollary›. ‹ℜ[X⇩1,...,X⇩n]› is Noetherian iff ‹ℜ› is. 
  ▪ ❙‹Extension›. If ‹ℜ› is a Noetherian ring, then ‹ℜ[[X]]› is a Noetherian ring,
  where ‹ℜ[[X]]› denotes the formal power series over the ring ‹ℜ›.\\

We also provide isomorphisms between the three types of polynomial rings defined in HOL-Algebra.
Together with the fact that the noetherian property is preserved by isomorphism, we get 
Hilbert's Basis theorem for all three models. We believe that this technique has a wider
potential of applications in the AFP library.

\newpage›
(*<*)
end
(*>*)