Theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW

  File:     More_Multivariate_Polynomial_HLW.thy
  Author:   Manuel Eberl, TU München
section ‹Additional facts about multivariate polynomials›
theory More_Multivariate_Polynomial_HLW
  imports "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"

subsection ‹Miscellaneous›

lemma Var_altdef: "Var i = monom (Poly_Mapping.single i 1) 1"
  by transfer' (simp add: Var0_def)

lemma Const_conv_monom: "Const c = monom 0 c"
  by transfer' (auto simp: Const0_def)

lemma smult_conv_mult_Const: "smult c p = Const c * p"
  by (simp add: smult_conv_mult Const_conv_monom)

lemma mpoly_map_vars_Var [simp]: "bij f  mpoly_map_vars f (Var i) = Var (f i)"
  unfolding Var_altdef
  by (subst mpoly_map_vars_monom) (auto simp: permutep_single bij_imp_bij_inv inv_inv_eq)

lemma symmetric_mpoly_symmetric_prod':
  assumes "π. π permutes A  g π permutes X"
  assumes "x π. x  X  π permutes A  mpoly_map_vars π (f x) = f (g π x)"
  shows "symmetric_mpoly A (xX. f x)"
  unfolding symmetric_mpoly_def
proof safe
  fix π assume π: "π permutes A"
  have "mpoly_map_vars π (prod f X) = (xX. mpoly_map_vars π (f x))"
    by simp
  also have " = (xX. f (g π x))"
    by (intro prod.cong assms π refl)
  also have " = (xg π`X. f x)"
    using assms(1)[OF π] by (subst prod.reindex) (auto simp: permutes_inj_on)
  also have "g π ` X = X"
    using assms(1)[OF π] by (simp add: permutes_image)
  finally show "mpoly_map_vars π (prod f X) = prod f X" .

subsection ‹Converting a univariate polynomial into a multivariate one›

lift_definition mpoly_of_poly_aux :: "nat  'a :: zero poly  (nat 0 nat) 0 'a" is
  "λi c m. if Poly_Mapping.keys m  {i} then c (Poly_Mapping.lookup m i) else 0"
proof goal_cases
  case (1 i c)
  hence fin: "finite {n. c n  0}"
    by (metis eventually_cofinite)
  show "finite {x. (if keys x  {i} then c (lookup x i) else 0)  0}"
  proof (rule finite_subset)
    show "finite (Poly_Mapping.single i ` {n. c n  0})"
      by (intro finite_imageI fin)
    show "{x. (if keys x  {i} then c (lookup x i) else 0)  0} 
            Poly_Mapping.single i ` {n. c n  0}"
    proof (safe, split if_splits)
      fix x :: "(nat 0 nat)"
      assume x: "keys x  {i}" "c (lookup x i)  0"
      hence "x = Poly_Mapping.single i (lookup x i)"
        by (metis Diff_eq_empty_iff keys_empty_iff lookup_single_eq
                  remove_key_keys remove_key_single remove_key_sum)
      thus "x  Poly_Mapping.single i ` {n. c n  0}"
        using x by blast
    qed auto

lift_definition mpoly_of_poly :: "nat  'a :: zero poly  'a mpoly" is
  "mpoly_of_poly_aux" .

lemma mpoly_of_poly_0 [simp]: "mpoly_of_poly i 0 = 0"
  by (transfer', transfer) auto

lemma coeff_mpoly_of_poly1 [simp]:
  "coeff (mpoly_of_poly i p) (Poly_Mapping.single i n) = poly.coeff p n"
  by (transfer', transfer') auto

lemma coeff_mpoly_of_poly2 [simp]:
  assumes "¬keys x  {i}"
  shows "coeff (mpoly_of_poly i p) x = 0"
  using assms by (transfer', transfer') auto

lemma coeff_mpoly_of_poly:
  "coeff (mpoly_of_poly i p) m =
     (poly.coeff p (Poly_Mapping.lookup m i) when keys m  {i})"
  by (transfer', transfer') auto

lemma poly_mapping_single_eq_0_iff [simp]: "Poly_Mapping.single i n = 0  n = 0"
  by (metis lookup_single_eq single_zero)

lemma mpoly_of_poly_pCons [simp]:
  fixes p :: "'a :: semiring_1 poly"
  shows "mpoly_of_poly i (pCons c p) = Const c + Var i * mpoly_of_poly i p"
proof (rule mpoly_eqI)
  fix mon :: "nat 0 nat"
  define moni :: "nat 0 nat" where "moni = Poly_Mapping.single i 1"
  have "coeff (Var i * mpoly_of_poly i p) mon =
          (l. (1 when l = moni) * (q. coeff (mpoly_of_poly i p) q when mon = moni + q))"
    unfolding coeff_mpoly_times prod_fun_def coeff_Var moni_def
    by (rule Sum_any.cong) (auto simp: when_def)
  also have " = (a. coeff (mpoly_of_poly i p) a when mon = moni + a)"
    by (subst Sum_any_left_distrib [symmetric]) simp_all
  finally have eq: "coeff (Var i * mpoly_of_poly i p) mon = " .

  show "coeff (mpoly_of_poly i (pCons c p)) mon = coeff (Const c + Var i * mpoly_of_poly i p) mon"
  proof (cases "keys mon  {i}")
    case False
    hence [simp]: "mon  0"
      by auto
    obtain j where j: "j  keys mon" "j  i"
      using False by auto
    have "coeff (mpoly_of_poly i p) mon' = 0" if mon_eq: "mon = moni + mon'" for mon'
    proof -
      have "Poly_Mapping.lookup mon j  0"
        using j by (meson lookup_eq_zero_in_keys_contradict)
      also have "Poly_Mapping.lookup mon j = Poly_Mapping.lookup mon' j"
        unfolding mon_eq moni_def using j by (simp add: lookup_add lookup_single)
      finally have "j  keys mon'"
        by (meson lookup_not_eq_zero_eq_in_keys)
      with j have "¬keys mon'  {i}"
        by blast
      thus ?thesis by simp
    hence "coeff (Var i * mpoly_of_poly i p) mon = 0"
      unfolding eq by (intro Sum_any_zeroI) (auto simp: when_def)
    thus ?thesis using False
      by (simp add: mpoly_coeff_Const)
    case True
    define n where "n = Poly_Mapping.lookup mon i"
    have mon_eq: "mon = Poly_Mapping.single i n"
      using True unfolding n_def
      by (metis Diff_eq_empty_iff add_cancel_right_left keys_empty_iff remove_key_keys remove_key_sum)
    have eq': "mon = moni + mon'  n > 0  mon' = Poly_Mapping.single i (n - 1)" for mon'
    proof safe
      assume eq: "mon = moni + mon'"
      thus "n > 0" "mon' = Poly_Mapping.single i (n - 1)"
        unfolding moni_def mon_eq using gr0I by (force simp: single_diff)+
      assume "n > 0" "mon' = Poly_Mapping.single i (n - 1)"
      thus "mon = moni + Poly_Mapping.single i (n - 1)"
        unfolding mon_eq moni_def by (subst single_add [symmetric]) auto
    have "coeff (Var i * mpoly_of_poly i p) mon = (poly.coeff p (n - 1) when (n > 0))"
      unfolding eq eq' by (auto simp: when_def)
    thus ?thesis
      by (auto simp: mon_eq when_def mpoly_coeff_Const coeff_pCons split: nat.splits)

lemma mpoly_of_poly_1 [simp]: "mpoly_of_poly i 1 = 1"
  unfolding one_pCons mpoly_of_poly_pCons mpoly_of_poly_0 by simp

lemma mpoly_of_poly_uminus [simp]: "mpoly_of_poly i (-p) = -mpoly_of_poly i p"
  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)

lemma mpoly_of_poly_add [simp]: "mpoly_of_poly i (p + q) = mpoly_of_poly i p + mpoly_of_poly i q"
  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)

lemma mpoly_of_poly_diff [simp]: "mpoly_of_poly i (p - q) = mpoly_of_poly i p - mpoly_of_poly i q"
  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)

lemma mpoly_of_poly_smult [simp]:
  "mpoly_of_poly i (Polynomial.smult c p) = smult c (mpoly_of_poly i p)"
  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)

lemma mpoly_of_poly_mult [simp]:
  fixes p q :: "'a :: comm_semiring_1 poly"
  shows "mpoly_of_poly i (p * q) = mpoly_of_poly i p * mpoly_of_poly i q"
  by (induction p) (auto simp: algebra_simps smult_conv_mult_Const)

lemma insertion_mpoly_of_poly [simp]: "insertion f (mpoly_of_poly i p) = poly p (f i)"
  by (induction p) (auto simp: insertion_add insertion_mult)

lemma mapping_of_mpoly_of_poly [simp]: "mapping_of (mpoly_of_poly i p) = mpoly_of_poly_aux i p"
  by transfer' simp

lemma vars_mpoly_of_poly: "vars (mpoly_of_poly i p)  {i}"
proof -
  have "x = i" if "xa  keys (mpoly_of_poly_aux i p)" "x  keys xa" for x xa
    using that
    by (meson in_mono lookup_eq_zero_in_keys_contradict mpoly_of_poly_aux.rep_eq singletonD)
  thus ?thesis
    by (auto simp: vars_def)

lemma mpoly_map_vars_mpoly_of_poly [simp]:
  assumes "bij f"
  shows   "mpoly_map_vars f (mpoly_of_poly i p) = mpoly_of_poly (f i) p"
proof (rule mpoly_eqI, goal_cases)
  case (1 mon)
  have "f -` keys mon  {i}  keys mon  {f i}"
    using assms by (simp add: vimage_subset_eq)
  thus ?case using assms
    by (simp add: coeff_mpoly_map_vars coeff_mpoly_of_poly lookup_permutep keys_permutep when_def)