Theory Polynomials_Ring_Misc

section ‹Polynomials Ring Miscellaneous›

theory Polynomials_Ring_Misc

imports "HOL-Algebra.Polynomials"

begin

text ‹Some lemmas that may be considered as useful, and that helps for the Hilbert's basis proof›

definition(in ring) deg_poly_set:‹deg_poly_set S k =  {a. a∈S ∧ degree a = k}∪{[]}›

definition (in ring)  lead_coeff_set::‹'a list set⇒ nat ⇒ 'a set›
  where ‹lead_coeff_set S k ≡ {coeff a (degree a) | a. a∈deg_poly_set S k}›



lemma rule_union:‹x∈(⋃n≤k. A l n) ⟷ (∃n≤k. x∈A l n)›
  by(auto)

lemma (in ring) add_0_eq_0_is_0:‹a∈carrier ((carrier R)[X]) ⟹ [] ⊕⇘(carrier R) [X]⇙ a = [] ⟹ a = []›
proof -
  assume h1:‹a∈carrier ((carrier R)[X])› and h2:‹[] ⊕⇘(carrier R) [X]⇙ a = []›
  have ‹poly_add [] a = a›
    apply(rule local.poly_add_zero(2)[of ‹(carrier R)›])
     apply (simp add: carrier_is_subring)
    by (simp add: h1 univ_poly_carrier)
  then show ?thesis 
    using h2 unfolding univ_poly_add by presburger
qed


lemma (in domain) inv_coeff_sum:‹a∈carrier((carrier R)[X]) ⟹ aa∈carrier((carrier R)[X]) 
⟹ a ⊕⇘(carrier R)[X]⇙ aa = [] ⟷ (∀n. coeff a n = inv⇘add_monoid R⇙ (coeff aa n))›
proof(safe, induct a)
  case Nil
  then have ‹aa = []› 
    by (simp add: Nil.prems(2) Nil.prems(3) add_0_eq_0_is_0)
  then show ?case by(auto)
next
  case (Cons a1 a2)
  then show ?case 
    by (metis add.comm_inv_char coeff.simps(1) coeff_in_carrier local.add.m_comm local.ring_axioms 
        poly_add_coeff polynomial_in_carrier ring.carrier_is_subring univ_poly_add univ_poly_carrier)
next 
  interpret kxr: cring "(carrier R)[X]"
    using carrier_is_subring univ_poly_is_cring by blast
  assume h1:‹a ∈ carrier ((carrier R) [X])› and h2:‹aa ∈ carrier ((carrier R) [X])›
    and h3:‹∀n. local.coeff a n = inv⇘add_monoid R⇙ local.coeff aa n›
  then show ‹a ⊕⇘(carrier R) [X]⇙ aa = []› 
    by (metis (no_types, lifting) abelian_group_def abelian_monoid.a_monoid add.Units_eq
        carrier_is_subring coeff_in_carrier kxr.add.m_closed kxr.add.m_comm lead_coeff_simp local.ring_axioms 
        mem_Collect_eq monoid.Units_r_inv monoid.select_convs(1) monoid.select_convs(2) partial_object.select_convs(1) 
        poly_add_coeff polynomial_def polynomial_in_carrier ring_def univ_poly_add univ_poly_def)
qed


lemma (in ring) coeffs_of_add_poly:‹a∈carrier((carrier R)[X]) ⟹ aa∈carrier((carrier R)[X]) 
    ⟹ coeff (a ⊕⇘(carrier R)[X]⇙ aa) n = coeff a n ⊕ coeff aa n›
  by (metis local.ring_axioms poly_add_coeff ring.polynomial_incl univ_poly_add univ_poly_carrier)

lemma (in ring) length_add:‹a∈carrier((carrier R)[X]) ⟹ aa∈carrier((carrier R)[X]) 
⟹ coeff a (degree a) ≠ inv⇘add_monoid R⇙ coeff aa (degree aa)
 ⟹ degree (a ⊕⇘(carrier R)[X]⇙ aa) = max (degree a) (degree aa)›
proof -
  assume h1:‹a∈carrier((carrier R)[X])› 
    and h2:‹aa∈carrier((carrier R)[X])› 
    and h3:‹coeff a (degree a) ≠ inv⇘add_monoid R⇙ coeff aa (degree aa)›
  have f0:‹∀n>(max (degree a) (degree aa)). coeff (a ⊕⇘(carrier R)[X]⇙ aa) n = 𝟬›
    by (simp add: coeff_degree coeffs_of_add_poly h1 h2)
  then have f1:‹degree a = degree aa ⟹ coeff (a ⊕⇘(carrier R)[X]⇙ aa) (degree a)
                 = coeff a (degree a) ⊕ coeff aa (degree aa)›
    using coeffs_of_add_poly h1 h2 by presburger
  also have f2: ‹coeff a (degree a) ⊕ coeff aa (degree aa) ≠ 𝟬› using h3 
    by (meson add.inv_comm add.inv_unique' coeff_in_carrier h1 h2 local.ring_axioms 
        ring.polynomial_incl univ_poly_carrier)
  then show ?thesis 
    apply(cases "degree a = degree aa")
    using f0 f1 
     apply (metis coeff_degree le_neq_implies_less max.idem poly_add_degree univ_poly_add)
    apply(cases ‹degree a > degree aa›)
    by (metis carrier_is_subring h1 h2 local.ring_axioms 
        ring.poly_add_degree_eq univ_poly_add univ_poly_carrier)+
qed


lemma (in domain) inv_imp_zero:‹a∈carrier((carrier R)[X]) ⟹ a ⊕⇘(carrier R) [X]⇙ inv⇘add_monoid ((carrier R) [X])⇙ a = []›
  using local.add.Units_eq local.add.Units_r_inv univ_poly_zero 
  by (metis a_inv_def abelian_group.r_neg carrier_is_subring domain.univ_poly_is_abelian_group domain_axioms)

lemma (in domain) R_subdom:‹subdomain (carrier R) R›
  by (simp add: carrier_is_subring subdomainI')

lemma (in domain) lead_coeff_in_carrier:
  ‹ideal I ((carrier R)[X]) ⟹ a∈ I ⟹ coeff a (degree a) ∈ (carrier R)› for I a
  using poly_coeff_in_carrier[of ‹carrier R› a] 
  by (simp add: carrier_is_subring ideal.Icarr univ_poly_carrier)

lemma (in domain) degree_of_inv:‹p∈carrier((carrier R)[X]) ⟹ degree (inv⇘add_monoid ((carrier R)[X])⇙ p) = degree p› for p
  using univ_poly_a_inv_degree[of ‹carrier R› p] 
  by (simp add: a_inv_def carrier_is_subring)

lemma (in domain) inv_in_deg_poly_set:‹ideal I ((carrier R)[X]) ⟹ a∈ deg_poly_set I k 
⟹ inv⇘add_monoid ((carrier R)[X])⇙ a ∈ deg_poly_set I k› for I k a
proof -
  interpret kxr: cring "(carrier R)[X]"
    using carrier_is_subring univ_poly_is_cring by blast
  assume h1:‹ideal I ((carrier R)[X])› ‹a∈ deg_poly_set I k›
  then show ?thesis
    unfolding deg_poly_set
    apply(safe) 
       apply (meson additive_subgroup_def group.subgroupE(3) ideal_def kxr.add.is_group)
      apply (meson degree_of_inv ideal.Icarr)
    by (metis kxr.add.inv_one univ_poly_zero)+
qed

lemma (in domain) ideal_lead_coeff_set:‹ideal (lead_coeff_set I k) R› 
  if  h':‹ideal I ((carrier R)[X])› for I k 
proof(rule idealI)
  show ‹ring R› 
    by (simp add: local.ring_axioms)
next
  interpret kxr: cring "(carrier R)[X]"
    using carrier_is_subring univ_poly_is_cring by blast
  show ‹subgroup (lead_coeff_set I k) (add_monoid R)›
    unfolding subgroup_def lead_coeff_set_def 
  proof(safe)
    fix a x
    assume h1:‹a ∈ deg_poly_set I k›
    show ‹local.coeff a (degree a) ∈ carrier (add_monoid R)›
      using lead_coeff_in_carrier h' h1  
      by (metis (no_types, lifting) Un_iff deg_poly_set empty_iff insert_iff 
          kxr.oneideal mem_Collect_eq partial_object.select_convs(1) univ_poly_zero_closed)
  next 
    fix x y a aa
    assume h1:‹a ∈ deg_poly_set I k› and h2:‹aa ∈ deg_poly_set I k› 
    then have imp:‹a∈carrier ((carrier R)[X]) ∧ aa ∈ carrier ((carrier R)[X])›
      unfolding deg_poly_set using h' unfolding ideal_def 
      by(auto simp:additive_subgroup.a_Hcarr)
    then show ‹∃ab. local.coeff a (degree a) ⊗⇘add_monoid R⇙ local.coeff aa (degree aa) 
  = local.coeff ab (degree ab) ∧ ab ∈ deg_poly_set I k›
      apply(cases ‹a=[]›)
      using lead_coeff_in_carrier h2 kxr.oneideal apply auto[1]
      apply(cases ‹aa=[]›)
      using lead_coeff_in_carrier h1 kxr.oneideal apply auto[1]
      apply(cases ‹local.coeff aa (length aa - Suc 0) 
  ≠ inv⇘add_monoid R⇙ local.coeff a (length a - Suc 0)›)
       apply(rule exI[where x=‹a ⊕⇘(carrier R)[X]⇙ aa›])
      using imp length_add h1 h2 unfolding deg_poly_set apply(safe) 
         apply (metis One_nat_def coeffs_of_add_poly kxr.add.m_comm max.idem monoid.select_convs(1))
        apply (meson additive_subgroup.a_closed ideal_def that)
       apply (metis One_nat_def kxr.add.m_comm max.idem)
      by (metis (no_types, lifting) One_nat_def Un_iff add.comm_inv_char add.r_inv_ex coeff.simps(1) 
          lead_coeff_in_carrier insert_iff monoid.select_convs(1) that)
  next
    show ‹∃a. 𝟭⇘add_monoid R⇙ = local.coeff a (degree a) ∧ a ∈ deg_poly_set I k›
      by (smt (verit, ccfv_threshold) Un_insert_right coeff.simps(1) deg_poly_set insertI1 monoid.select_convs(2))
  next
    fix a
    assume ‹a ∈ deg_poly_set I k›
    obtain a' where ‹a'= inv⇘add_monoid ((carrier R)[X])⇙ a ∧ a ∈ I›
      using h' 
      by (metis (no_types, lifting) Un_iff ‹a ∈ deg_poly_set I k› deg_poly_set empty_iff insert_iff kxr.add.normal_invE(1)
          kxr.ideal_is_normal mem_Collect_eq monoid.select_convs(2) subgroup_def univ_poly_zero)
    then show ‹∃aa. inv⇘add_monoid R⇙ local.coeff a (degree a) = local.coeff aa (degree aa) ∧ aa ∈ deg_poly_set I k›
      apply(intro exI[where x=‹inv⇘add_monoid ((carrier R)[X])⇙ a›]) 
      apply(safe) 
       apply (metis (no_types, opaque_lifting) degree_of_inv ideal.Icarr kxr.add.Units_eq kxr.add.Units_inv_closed 
          kxr.add.Units_l_inv inv_coeff_sum that univ_poly_zero)
      using ‹a ∈ deg_poly_set I k› inv_in_deg_poly_set that by blast
  qed
next
  interpret kxr: cring "(carrier R)[X]"
    using carrier_is_subring univ_poly_is_cring by blast
  fix a y
  assume h1:‹ a ∈ lead_coeff_set I k› and h2:‹y ∈ (carrier R)›
  then obtain l where h3:‹l∈deg_poly_set I k ∧ a = coeff l (degree l)›
    using lead_coeff_set_def by auto
  then have t0:‹set l ⊆ (carrier R)› 
    by (metis (no_types, lifting) Un_iff additive_subgroup.a_Hcarr deg_poly_set h' ideal.axioms(1) 
        kxr.zeroideal mem_Collect_eq partial_object.select_convs(1) polynomial_incl univ_poly_def 
        univ_poly_zero)
  have t1:‹l∈carrier ((carrier R)[X])› using h3 h' unfolding deg_poly_set ideal_def 
    by(auto simp:additive_subgroup.a_Hcarr)
  have h4:‹y≠𝟬 ⟹ [y] ∈ carrier((carrier R)[X])›  
    using h2 by (simp add: polynomial_def univ_poly_def)
  have f4a:‹subring (carrier R) R› 
    using carrier_is_subring by auto
  have h5:‹y≠𝟬 ⟹ [y] ∈ carrier ((carrier R) [X]) ⟹ l ∈ carrier ((carrier R)[X]) 
  ⟹ l≠[] ⟹ [y] ⊗⇘(carrier R) [X]⇙ l ∈ deg_poly_set I k›
    using h3 h4 unfolding deg_poly_set apply(safe)
     apply (meson h' ideal_axioms_def ideal_def) 
    unfolding univ_poly_mult
    using poly_mult_degree_eq[of "(carrier R)" ‹[y]› l] 
    using f4a univ_poly_carrier by auto 
  have t4:‹y≠𝟬 ⟹ [y] ∈ carrier ((carrier R) [X]) ⟹ l ∈ carrier ((carrier R)[X]) ⟹ l≠[] ⟹y ⊗ a = local.coeff ([y] ⊗⇘(carrier R) [X]⇙ l) (degree ([y] ⊗⇘(carrier R) [X]⇙ l))›
    unfolding univ_poly_mult 
    by (metis f4a h3 lead_coeff_simp list.sel(1) not_Cons_self poly_mult_integral 
        poly_mult_lead_coeff univ_poly_carrier)
  have t6:‹a≠𝟬 ⟹ l≠[]› 
    using h3 by fastforce
  show symet:‹y ⊗ a ∈ lead_coeff_set I k› 
    unfolding lead_coeff_set_def deg_poly_set apply(safe)
    apply(cases ‹a = 𝟬›)
     apply(rule exI[where x=‹[]›])
     apply (simp add: h2)
    apply(cases ‹y=𝟬›)     
     apply(rule exI[where x=‹[]›])
    using coeff.simps(1) coeff_in_carrier h2 h3 integral_iff t0 apply simp
    apply(rule exI[where x=‹ [y] ⊗⇘(carrier R) [X]⇙ l›])
    apply(safe)
      apply (metis One_nat_def coeff.simps(1) h3 h4 t1 t4)
    using h5 h4 t6 by(auto simp add: deg_poly_set t1)  
  show ‹a ⊗ y ∈ lead_coeff_set I k› 
    using h2 h3 m_comm symet t0 by auto
qed

lemma (in ring) deg_poly_set_0:‹deg_poly_set x' 0 = {[a] | a. [a]∈x'}∪{[]}› for x'::‹'c list set›
  unfolding deg_poly_set 
  apply(safe)
   apply (metis One_nat_def Suc_pred length_0_conv length_Suc_conv length_greater_0_conv)
  by(auto)

lemma (in ring) lead_coeff_set_0:‹lead_coeff_set x' 0 = {a. [a]∈x'}∪{𝟬}› for x'
  unfolding lead_coeff_set_def 
proof(subst deg_poly_set_0, safe)
  fix x a aa
  assume h1:‹local.coeff [aa] (degree [aa]) ∉ {}› ‹local.coeff [aa] (degree [aa]) ≠ 𝟬›
    ‹[aa] ∈ x'›
  then show ‹[local.coeff [aa] (degree [aa])] ∈ x'›
    by(simp) 
next
  fix x a
  assume h1:‹local.coeff [] (degree []) ∉ {}› ‹local.coeff [] (degree []) ≠ 𝟬›
  then show ‹[local.coeff [] (degree [])] ∈ x'› by simp
next
  fix x
  assume h1:‹[x] ∈ x'›
  then show ‹∃a. x = local.coeff a (degree a) ∧ a ∈ {[a] |a. [a] ∈ x'} ∪ {[]}›
    apply(intro exI[where x=‹[x]›]) 
    by(simp)
next
  fix x
  show ‹∃a. 𝟬 = local.coeff a (degree a) ∧ a ∈ {[a] |a. [a] ∈ x'} ∪ {[]} ›
    apply(rule exI[where x=‹[]›]) 
    by(simp)
qed

end