Theory Polynomials.Quasi_PM_Power_Products

(* Author: Alexander Maletzky *)

section ‹Quasi-Poly-Mapping Power-Products›

theory Quasi_PM_Power_Products
  imports MPoly_Type_Class_Ordered
begin

text ‹In this theory we introduce a subclass of @{class graded_dickson_powerprod} that approximates
  polynomial mappings even closer. We need this class for signature-based Gr\"obner basis algorithms.›

definition (in monoid_add) hom_grading_fun :: "('a  nat)  (nat  'a  'a)  bool"
  where "hom_grading_fun d f  (n. (s t. f n (s + t) = f n s + f n t) 
          (t. d (f n t)  n  (d t  n  f n t = t)))"

definition (in monoid_add) hom_grading :: "('a  nat)  bool"
  where "hom_grading d  (f. hom_grading_fun d f)"

definition (in monoid_add) decr_grading :: "('a  nat)  nat  'a  'a"
  where "decr_grading d = (SOME f. hom_grading_fun d f)"

lemma decr_grading:
  assumes "hom_grading d"
  shows "hom_grading_fun d (decr_grading d)"
proof -
  from assms obtain f where "hom_grading_fun d f" unfolding hom_grading_def ..
  thus ?thesis unfolding decr_grading_def by (metis someI)
qed

lemma decr_grading_plus:
  "hom_grading d  decr_grading d n (s + t) = decr_grading d n s + decr_grading d n t"
  using decr_grading unfolding hom_grading_fun_def by blast

lemma decr_grading_zero:
  assumes "hom_grading d"
  shows "decr_grading d n 0 = (0::'a::cancel_comm_monoid_add)"
proof -
  have "decr_grading d n 0 = decr_grading d n (0 + 0)" by simp
  also from assms have "... = decr_grading d n 0 + decr_grading d n 0" by (rule decr_grading_plus)
  finally show ?thesis by simp
qed

lemma decr_grading_le: "hom_grading d  d (decr_grading d n t)  n"
  using decr_grading unfolding hom_grading_fun_def by blast

lemma decr_grading_idI: "hom_grading d  d t  n  decr_grading d n t = t"
  using decr_grading unfolding hom_grading_fun_def by blast

class quasi_pm_powerprod = ulcs_powerprod +
  assumes ex_hgrad: "d::'a  nat. dickson_grading d  hom_grading d"
begin

subclass graded_dickson_powerprod
proof
  from ex_hgrad show "d. dickson_grading d" by blast
qed

end (* quasi_pm_powerprod *)

lemma hom_grading_varnum:
  "hom_grading ((varnum X)::('x::countable 0 'b::add_wellorder)  nat)"
proof -
  define f where "f = (λn t. (except t (- (X  {x. elem_index x < n})))::'x 0 'b)"
  show ?thesis unfolding hom_grading_def hom_grading_fun_def
  proof (intro exI allI conjI impI)
    fix n s t
    show "f n (s + t) = f n s + f n t" by (simp only: f_def except_plus)
  next
    fix n t
    show "varnum X (f n t)  n" by (auto simp: varnum_le_iff keys_except f_def)
  next
    fix n t
    show "varnum X t  n  f n t = t" by (auto simp: f_def except_id_iff varnum_le_iff)
  qed
qed

instance poly_mapping :: (countable, add_wellorder) quasi_pm_powerprod
  by (standard, intro exI conjI, fact dickson_grading_varnum_empty, fact hom_grading_varnum)

context term_powerprod
begin

definition decr_grading_term :: "('a  nat)  nat  't  't"
  where "decr_grading_term d n v = term_of_pair (decr_grading d n (pp_of_term v), component_of_term v)"

definition decr_grading_p :: "('a  nat)  nat  ('t 0 'b)  ('t 0 'b::comm_monoid_add)"
  where "decr_grading_p d n p = (vkeys p. monomial (lookup p v) (decr_grading_term d n v))"

lemma decr_grading_term_splus:
  "hom_grading d  decr_grading_term d n (t  v) = decr_grading d n t  decr_grading_term d n v"
  by (simp add: decr_grading_term_def term_simps decr_grading_plus splus_def)

lemma decr_grading_term_le: "hom_grading d  d (pp_of_term (decr_grading_term d n v))  n"
  by (simp add: decr_grading_term_def term_simps decr_grading_le)

lemma decr_grading_term_idI: "hom_grading d  d (pp_of_term v)  n  decr_grading_term d n v = v"
  by (simp add: decr_grading_term_def term_simps decr_grading_idI)

lemma punit_decr_grading_term: "punit.decr_grading_term = decr_grading"
  by (intro ext, simp add: punit.decr_grading_term_def)

lemma decr_grading_p_zero: "decr_grading_p d n 0 = 0"
  by (simp add: decr_grading_p_def)

lemma decr_grading_p_monomial: "decr_grading_p d n (monomial c v) = monomial c (decr_grading_term d n v)"
  by (simp add: decr_grading_p_def)

lemma decr_grading_p_plus:
  "decr_grading_p d n (p + q) = (decr_grading_p d n p) + (decr_grading_p d n q)"
proof -
  from finite_keys finite_keys have fin: "finite (keys p  keys q)" by (rule finite_UnI)
  hence eq1: "(vkeys p  keys q. monomial (lookup p v) (decr_grading_term d n v)) =
              (vkeys p. monomial (lookup p v) (decr_grading_term d n v))"
  proof (rule sum.mono_neutral_right)
    show "vkeys p  keys q - keys p. monomial (lookup p v) (decr_grading_term d n v) = 0"
      by (simp add: in_keys_iff)
  qed simp
  from fin have eq2: "(vkeys p  keys q. monomial (lookup q v) (decr_grading_term d n v)) =
              (vkeys q. monomial (lookup q v) (decr_grading_term d n v))"
  proof (rule sum.mono_neutral_right)
    show "vkeys p  keys q - keys q. monomial (lookup q v) (decr_grading_term d n v) = 0"
      by (simp add: in_keys_iff)
  qed simp
  from fin Poly_Mapping.keys_add
  have "decr_grading_p d n (p + q) =
                (vkeys p  keys q. monomial (lookup (p + q) v) (decr_grading_term d n v))"
    unfolding decr_grading_p_def
  proof (rule sum.mono_neutral_left)
    show "vkeys p  keys q - keys (p + q). monomial (lookup (p + q) v) (decr_grading_term d n v) = 0"
      by (simp add: in_keys_iff)
  qed
  also have "... = (vkeys p  keys q. monomial (lookup p v) (decr_grading_term d n v)) +
                   (vkeys p  keys q. monomial (lookup q v) (decr_grading_term d n v))"
    by (simp only: lookup_add single_add sum.distrib)
  also have "... = (decr_grading_p d n p) + (decr_grading_p d n q)"
    by (simp only: eq1 eq2 decr_grading_p_def)
  finally show ?thesis .
qed

corollary decr_grading_p_sum: "decr_grading_p d n (sum f A) = (aA. decr_grading_p d n (f a))"
  using decr_grading_p_zero decr_grading_p_plus by (rule fun_sum_commute)

lemma decr_grading_p_monom_mult:
  assumes "hom_grading d"
  shows "decr_grading_p d n (monom_mult c t p) = monom_mult c (decr_grading d n t) (decr_grading_p d n p)"
proof (induct p rule: poly_mapping_plus_induct)
  case 1
  show ?case by (simp add: decr_grading_p_zero)
next
  case (2 p a s)
  from assms show ?case
    by (simp add: monom_mult_dist_right decr_grading_p_plus 2(3) monom_mult_monomial
        decr_grading_p_monomial decr_grading_term_splus)
qed

lemma decr_grading_p_mult_scalar:
  assumes "hom_grading d"
  shows "decr_grading_p d n (p  q) = punit.decr_grading_p d n p  decr_grading_p d n q"
proof (induct p rule: poly_mapping_plus_induct)
  case 1
  show ?case by (simp add: punit.decr_grading_p_zero decr_grading_p_zero)
next
  case (2 p a s)
  from assms show ?case
    by (simp add: mult_scalar_distrib_right decr_grading_p_plus punit.decr_grading_p_plus 2(3)
        punit.decr_grading_p_monomial mult_scalar_monomial decr_grading_p_monom_mult punit_decr_grading_term)
qed

lemma decr_grading_p_keys_subset: "keys (decr_grading_p d n p)  decr_grading_term d n ` keys p"
proof
  fix v
  assume "v  keys (decr_grading_p d n p)"
  also have "...  (ukeys p. keys (monomial (lookup p u) (decr_grading_term d n u)))"
    unfolding decr_grading_p_def by (fact keys_sum_subset)
  finally obtain u where "u  keys p" and "v  keys (monomial (lookup p u) (decr_grading_term d n u))" ..
  from this(2) have eq: "v = decr_grading_term d n u" by (simp split: if_split_asm)
  show "v  decr_grading_term d n ` keys p" unfolding eq using u  keys p by (rule imageI)
qed

lemma decr_grading_p_idI':
  assumes "hom_grading d" and "v. v  keys p  d (pp_of_term v)  n"
  shows "decr_grading_p d n p = p"
proof -
  have "decr_grading_p d n p = (v  keys p. monomial (lookup p v) v)" unfolding decr_grading_p_def
    using refl
  proof (rule sum.cong)
    fix v
    assume "v  keys p"
    hence "d (pp_of_term v)  n" by (rule assms(2))
    with assms(1) have "decr_grading_term d n v = v" by (rule decr_grading_term_idI)
    thus "monomial (lookup p v) (decr_grading_term d n v) = monomial (lookup p v) v" by simp
  qed
  also have "... = p" by (fact poly_mapping_sum_monomials)
  finally show ?thesis .
qed

end (* term_powerprod *)

context gd_term
begin

lemma decr_grading_p_idI:
  assumes "hom_grading d" and "p  dgrad_p_set d m"
  shows "decr_grading_p d m p = p"
proof -
  from assms(2) have "v. v  keys p  d (pp_of_term v)  m"
    by (auto simp: dgrad_p_set_def dgrad_set_def)
  with assms(1) show ?thesis by (rule decr_grading_p_idI')
qed

lemma decr_grading_p_dgrad_p_setI:
  assumes "hom_grading d"
  shows "decr_grading_p d m p  dgrad_p_set d m"
proof (rule dgrad_p_setI)
  fix v
  assume "v  keys (decr_grading_p d m p)"
  hence "v  decr_grading_term d m ` keys p" using decr_grading_p_keys_subset ..
  then obtain u where "v = decr_grading_term d m u" ..
  with assms show "d (pp_of_term v)  m" by (simp add: decr_grading_term_le)
qed

lemma (in gd_term) in_pmdlE_dgrad_p_set:
  assumes "hom_grading d" and "B  dgrad_p_set d m" and "p  dgrad_p_set d m" and "p  pmdl B"
  obtains A q where "finite A" and "A  B" and "b. q b  punit.dgrad_p_set d m"
    and "p = (bA. q b  b)"
proof -
  from assms(4) obtain A q0 where "finite A" and "A  B" and p: "p = (bA. q0 b  b)"
    by (rule pmdl.spanE)
  define q where "q = (λb. punit.decr_grading_p d m (q0 b))"
  from finite A A  B show ?thesis
  proof
    fix b
    show "q b  punit.dgrad_p_set d m" unfolding q_def using assms(1) by (rule punit.decr_grading_p_dgrad_p_setI)
  next
    from assms(1, 3) have "p = decr_grading_p d m p" by (simp only: decr_grading_p_idI)
    also from assms(1) have "... = (bA. q b  (decr_grading_p d m b))"
      by (simp add: p q_def decr_grading_p_sum decr_grading_p_mult_scalar)
    also from refl have "... = (bA. q b  b)"
    proof (rule sum.cong)
      fix b
      assume "b  A"
      hence "b  B" using A  B ..
      hence "b  dgrad_p_set d m" using assms(2) ..
      with assms(1) have "decr_grading_p d m b = b" by (rule decr_grading_p_idI)
      thus "q b  decr_grading_p d m b = q b  b" by simp
    qed
    finally show "p = (bA. q b  b)" .
  qed
qed

end (* gd_term *)

end (* theory *)