Theory MPoly_Type_Univariate

(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
theory MPoly_Type_Univariate
  imports
    More_MPoly_Type
    "HOL-Computational_Algebra.Polynomial"
begin

text ‹This file connects univariate MPolys to the theory of univariate polynomials from
  @{theory "HOL-Computational_Algebra.Polynomial"}.›

definition poly_to_mpoly::"nat  'a::comm_monoid_add poly  'a mpoly"
where "poly_to_mpoly v p = MPoly (Abs_poly_mapping (λm. (coeff p (Poly_Mapping.lookup m v)) when Poly_Mapping.keys m  {v}))"

lemma poly_to_mpoly_finite: "finite {m::nat 0 nat. (coeff p (Poly_Mapping.lookup m v) when Poly_Mapping.keys m  {v})  0}" (is "finite ?M")
proof -
  have "?M  Poly_Mapping.single v ` {x. Polynomial.coeff p x  0}"
  proof
    fix m assume "m  ?M"
    then have "v'. v'v  Poly_Mapping.lookup m v' = 0" by (fastforce simp add: in_keys_iff)
    then have "m = Poly_Mapping.single v (Poly_Mapping.lookup m v)"
      using Poly_Mapping.poly_mapping_eqI by (metis (full_types) lookup_single_eq lookup_single_not_eq)
    then show "m  (Poly_Mapping.single v) ` {x. Polynomial.coeff p x  0}" using m  ?M by auto
  qed
  then show ?thesis using finite_surj[OF MOST_coeff_eq_0[unfolded eventually_cofinite]] by blast
qed

lemma coeff_poly_to_mpoly: "MPoly_Type.coeff (poly_to_mpoly v p) (Poly_Mapping.single v k) = Polynomial.coeff p k"
  unfolding poly_to_mpoly_def coeff_def MPoly_inverse[OF Set.UNIV_I] lookup_Abs_poly_mapping[OF poly_to_mpoly_finite]
  using empty_subsetI keys_single lookup_single order_refl when_simps(1) by simp

definition mpoly_to_poly::"nat  'a::comm_monoid_add mpoly  'a poly"
where "mpoly_to_poly v p = Abs_poly (λk. MPoly_Type.coeff p (Poly_Mapping.single v k))"

lemma coeff_mpoly_to_poly[simp]: "Polynomial.coeff (mpoly_to_poly v p) k = MPoly_Type.coeff p (Poly_Mapping.single v k)"
proof -
  have 0:"Poly_Mapping.single v ` {x. Poly_Mapping.lookup (mapping_of p) (Poly_Mapping.single v x)  0}
           {k. Poly_Mapping.lookup (mapping_of p) k  0}"
    by auto
  have " k. MPoly_Type.coeff p (Poly_Mapping.single v k) = 0" unfolding coeff_def eventually_cofinite
    using  finite_imageD[OF finite_subset[OF 0 Poly_Mapping.finite_lookup]] inj_single by (metis inj_eq inj_onI)
  then show ?thesis
    unfolding mpoly_to_poly_def by (simp add: Abs_poly_inverse)
qed

lemma mpoly_to_poly_inverse:
assumes "vars p  {v}"
shows "poly_to_mpoly v (mpoly_to_poly v p) = p"
proof -
  define f where "f = (λm. Polynomial.coeff (mpoly_to_poly v p) (Poly_Mapping.lookup m v) when Poly_Mapping.keys m  {v})"
  have "finite {m. f m  0}" unfolding f_def using poly_to_mpoly_finite by blast
  have "Abs_poly_mapping f = mapping_of p"
  proof (rule "Poly_Mapping.poly_mapping_eqI")
    fix m
    show "Poly_Mapping.lookup (Abs_poly_mapping f) m = Poly_Mapping.lookup (mapping_of p) m"
    proof (cases "Poly_Mapping.keys m  {v}")
      assume "Poly_Mapping.keys m  {v}"
      then show ?thesis unfolding "Poly_Mapping.lookup_Abs_poly_mapping"[OF finite {m. f m  0}] unfolding f_def
        unfolding coeff_mpoly_to_poly coeff_def using when_simps(1) apply simp
        using keys_single lookup_not_eq_zero_eq_in_keys lookup_single_eq
        lookup_single_not_eq poly_mapping_eqI subset_singletonD
        by (metis (no_types, lifting) aux lookup_eq_zero_in_keys_contradict)
    next
      assume "¬Poly_Mapping.keys m  {v}"
      then show ?thesis unfolding "Poly_Mapping.lookup_Abs_poly_mapping"[OF finite {m. f m  0}] unfolding f_def
        using vars p  {v} unfolding vars_def by (metis (no_types, lifting) UN_I lookup_not_eq_zero_eq_in_keys subsetCE subsetI when_def)
    qed
  qed
  then show ?thesis
    unfolding poly_to_mpoly_def f_def  by (simp add: mapping_of_inverse)
qed

lemma poly_to_mpoly_inverse: "mpoly_to_poly v (poly_to_mpoly v p) = p"
  unfolding mpoly_to_poly_def coeff_poly_to_mpoly by (simp add: coeff_inverse)

lemma poly_to_mpoly0: "poly_to_mpoly v 0 = 0"
proof -
  have "m. (Polynomial.coeff 0 (Poly_Mapping.lookup m v) when Poly_Mapping.keys m  {v}) = 0" by simp
  have "Abs_poly_mapping (λm. Polynomial.coeff 0 (Poly_Mapping.lookup m v) when Poly_Mapping.keys m  {v}) = 0"
    apply (rule Poly_Mapping.poly_mapping_eqI) unfolding lookup_Abs_poly_mapping[OF poly_to_mpoly_finite] by auto
  then show ?thesis using poly_to_mpoly_def zero_mpoly.abs_eq by (metis (no_types))
qed

lemma mpoly_to_poly_add: "mpoly_to_poly v (p1 + p2) = mpoly_to_poly v p1 + mpoly_to_poly v p2"
  unfolding  Polynomial.plus_poly.abs_eq More_MPoly_Type.coeff_add coeff_mpoly_to_poly
  using mpoly_to_poly_def by auto

lemma poly_eq_insertion:
assumes "vars p  {v}"
shows "poly (mpoly_to_poly v p) x = insertion (λv. x) p"
using assms proof (induction p rule:mpoly_induct)
  case (monom m a)
  then show ?case
  proof (cases "a=0")
    case True
    then show ?thesis
      by (metis MPoly_Type.monom.abs_eq insertion_zero monom_zero poly_0 poly_to_mpoly0 poly_to_mpoly_inverse single_zero)
  next
    case False
    then have "Poly_Mapping.keys m  {v}" using monom unfolding vars_def MPoly_Type.mapping_of_monom keys_single by simp
    then have "v'. v'v  Poly_Mapping.lookup m v' = 0" unfolding vars_def by (auto simp: in_keys_iff)
    then have "m = Poly_Mapping.single v (Poly_Mapping.lookup m v)"
      by (metis lookup_single_eq lookup_single_not_eq poly_mapping_eqI)
    then have 0:"insertion (λv. x) (MPoly_Type.monom m a) = a * x ^ (Poly_Mapping.lookup m v)"
      using insertion_single by metis
    have "k. Poly_Mapping.single v k = m  Poly_Mapping.lookup m v = k"
      using m = Poly_Mapping.single v (Poly_Mapping.lookup m v) by auto
    then have "monom a (Poly_Mapping.lookup m v) = (Abs_poly (λk. if Poly_Mapping.single v k = m then a else 0))"
      by (simp add: Polynomial.monom.abs_eq)
    then show ?thesis unfolding mpoly_to_poly_def More_MPoly_Type.coeff_monom 0 when_def by (metis poly_monom)
  qed
next
  case (sum p1 p2 m a)
  then have "poly (mpoly_to_poly v p1) x = insertion (λv. x) p1"
            "poly (mpoly_to_poly v p2) x = insertion (λv. x) p2"
    by (simp_all add: vars_add_monom)
  then show ?case unfolding insertion_add mpoly_to_poly_add by simp
qed

text ‹Using the new connection between MPoly and univariate polynomials, we can transfer:›

lemma univariate_mpoly_roots_finite:
fixes p::"'a::idom mpoly"
assumes "vars p  {v}" "p  0"
shows "finite {x. insertion (λv. x) p = 0}"
using poly_roots_finite[of "mpoly_to_poly v p", unfolded poly_eq_insertion[OF vars p  {v}]]
using assms(1) assms(2) mpoly_to_poly_inverse poly_to_mpoly0 by fastforce

end