Theory Substitutions
theory Substitutions
imports Poly_Expansions
begin
subsection ‹Substitution›
text ‹The following definitions allow substituting polynomials into the variables of the given
polynomial p. They correspond to ‹{@const subst_pp}› and ‹{@const poly_subst› in the
AFP entry ‹{@afp Polynomials.Poly_PM}››
definition poly_subst_monom :: "(nat ⇒ 'a::comm_semiring_1 mpoly) ⇒ (nat ⇒⇩0 nat) ⇒ 'a mpoly"
where "poly_subst_monom f t = (∏x. (f x) ^ (lookup t x))"
definition poly_subst :: "(nat ⇒ 'a::comm_semiring_1 mpoly) ⇒ 'a mpoly ⇒ 'a mpoly"
where "poly_subst f p = Sum_any (λt. (Const (coeff p t)) * (poly_subst_monom f t))"
definition poly_subst_list where "poly_subst_list ≡ poly_subst ∘ (!⇩0)"
abbreviation insertion_list where "insertion_list ≡ insertion ∘ (!⇩0)"
lemma poly_subst_monom_alt: "poly_subst_monom f t = (∏x ∈ keys t. (f x) ^ (lookup t x))"
unfolding poly_subst_monom_def
apply (rule Prod_any.expand_superset)
subgoal by simp
subgoal using in_keys_iff by fastforce
done
lemma poly_subst_alt: "poly_subst f p = (∑t ∈ keys (mapping_of p). (Const (coeff p t)) * (poly_subst_monom f t))"
unfolding poly_subst_def
apply (rule Sum_any.expand_superset)
subgoal by simp
subgoal using Const_zero coeff_keys mult_not_zero by fastforce
done
lemma poly_subst_list_id:
fixes p :: "'a::{comm_semiring_1,ring_no_zero_divisors} mpoly"
assumes "k ≥ max_vars p"
shows "poly_subst_list (map Var [0..<Suc k]) p = p"
proof -
have h0: "⋀x t. x∈keys t ∧ t ∈ keys (mapping_of p) ⟹ x < Suc (max_vars p)"
unfolding max_vars_def vars_def
apply (subst less_Suc_eq_le)
by (subst Max.coboundedI, auto)
hence "⋀x t. x∈keys t ∧ t ∈ keys (mapping_of p) ⟹ x < Suc k"
using assms by fastforce
hence h1: "⋀x t. x∈keys t ∧ t ∈ keys (mapping_of p) ⟹
map Var [0..<Suc k] !⇩0 x = (Var x)"
unfolding nth0_def
apply (subst nth_map, simp)
by (subst nth_upt, simp_all)
show ?thesis
unfolding poly_subst_list_def comp_def
unfolding poly_subst_alt poly_subst_monom_alt
apply (subst (9) mpoly_multivariate_expansion')
apply (rule sum.cong, simp)
apply (subst mult_left_cancel, metis Const_zero coeff_Const_zero coeff_keys)
apply (rule prod.mono_neutral_cong_left, simp)
using h0 less_Suc_eq_le apply force
apply (simp add: in_keys_iff)
by (subst h1, simp_all add: assms)
qed
lemma insertion_poly_subst_monom:
"insertion g (poly_subst_monom f t) = (∏x. (insertion g (f x)) ^ (lookup t x))"
unfolding poly_subst_monom_alt
apply (subst insertion_prod)
subgoal by simp
subgoal
unfolding insertion_pow
apply (rule Prod_any.expand_superset[symmetric])
subgoal by simp
subgoal using in_keys_iff by fastforce
done
done
lemma insertion_poly_subst:
"insertion g (poly_subst f p) = insertion ((insertion g) ∘ f) p"
unfolding poly_subst_alt
apply (subst (7) poly_eq_sum_monom_alt)
apply (subst (1 2) insertion_sum)
subgoal by simp
subgoal
unfolding insertion_mult insertion_Const
unfolding insertion_poly_subst_monom
unfolding insertion_monom
by simp
done
lemma insertion_nth0: "insertion f (l !⇩0 x) = (map (insertion f) l) !⇩0 x"
unfolding nth0_def
apply (induction l)
by simp (metis insertion_zero length_map nth_map when_def)
lemma poly_subst_monom_zero [simp]:
"poly_subst_monom f 0 = 1"
unfolding poly_subst_monom_alt keys_zero
by simp
lemma poly_subst_monom_single [simp]:
"poly_subst_monom f (Poly_Mapping.single v 1) = f v"
unfolding poly_subst_monom_alt
by simp
lemma poly_subst_monom_add: "poly_subst_monom f (m⇩1 + m⇩2) = poly_subst_monom f m⇩1 * poly_subst_monom f m⇩2"
unfolding poly_subst_monom_def lookup_add power_add
apply (rule Prod_any.distrib)
apply (metis (mono_tags, lifting) finite_keys finite_nat_set_iff_bounded in_keys_iff mem_Collect_eq power_0)+
done
lemma poly_subst_zero [simp]:
"poly_subst f 0 = 0"
unfolding poly_subst_def poly_subst_monom_def coeff_def zero_mpoly.rep_eq zero_poly_mapping.rep_eq Const_when when_mult Sum_any_when_equal Const_zero
by simp
lemma poly_subst_one [simp]:
"poly_subst f 1 = 1"
unfolding poly_subst_def poly_subst_monom_def coeff_def one_mpoly.rep_eq one_poly_mapping.rep_eq Const_when when_mult Sum_any_when_equal Const_one
by simp
lemma poly_subst_Var [simp]:
"poly_subst f (Var v) = f v"
unfolding poly_subst_alt Var.rep_eq keys.rep_eq Var⇩0_def lookup_single when_neq_zero
apply simp
apply (subst (2) power_one_right[symmetric])
unfolding One_nat_def[symmetric]
apply (subst coeff_var_power_eq)
unfolding poly_subst_monom_single Const_one
by simp
lemma poly_subst_Const [simp]:
"poly_subst f (Const c) = (Const c)"
unfolding poly_subst_alt Const.rep_eq keys.rep_eq Const⇩0_def lookup_single when_neq_zero
apply (cases "c = 0")
by (auto simp add: Const_zero coeff_Const_zero)
lemma poly_subst_numeral[simp]:
"poly_subst f (numeral n) = (numeral n)"
unfolding Const_numeral[symmetric]
by simp
lemma poly_subst_add [simp]:
"poly_subst f (P + Q) = poly_subst f P + poly_subst f Q"
proof -
have 0: "⋀P. {a. Const (lookup (mapping_of P) a) * poly_subst_monom f a ≠ 0}
⊆ {a. lookup (mapping_of P) a ≠ 0}"
by (auto simp: Const_zero)
have H: "finite {a. Const (lookup (mapping_of P) a) * poly_subst_monom f a ≠ 0}" for P
using 0[of P] finite_lookup
by (rule finite_subset)
thus ?thesis
unfolding poly_subst_def coeff_add[symmetric] Const_add[symmetric]
unfolding coeff_def
unfolding Sum_any.distrib[OF H H, symmetric]
unfolding coeff_def[symmetric]
by (auto simp: algebra_simps)
qed
lemma poly_subst_uminus [simp]:
"poly_subst f (- P) = - poly_subst f P "
by (metis add_cancel_right_right add_eq_0_iff poly_subst_add)
lemma poly_subst_diff [simp]:
"poly_subst f ((P::('a::{ab_group_add,comm_semiring_1}) mpoly) - Q) = poly_subst f P - poly_subst f Q"
by (metis diff_eq_eq poly_subst_add)
lemma poly_subst_sum:
"poly_subst f (sum P A) = sum (poly_subst f ∘ P) A"
by (induct A rule: infinite_finite_induct; auto)
lemma poly_subst_mult [simp]:
"poly_subst f (P * Q) = poly_subst f P * poly_subst f Q"
unfolding poly_subst_def
unfolding coeff_def times_mpoly.rep_eq times_poly_mapping.rep_eq prod_fun_def
unfolding coeff_def[symmetric]
proof -
have 0: "finite {m. coeff P m ≠ 0}" by (simp add: coeff_def)
have 1: "finite {m. coeff Q m ≠ 0}" by (simp add: coeff_def)
have "finite ({m⇩1. coeff P m⇩1 ≠ 0} × {m⇩2. coeff Q m⇩2 ≠ 0})"
using 0 1 by simp
hence "finite {(m⇩1, m⇩2). coeff P m⇩1 ≠ 0 ∧ coeff Q m⇩2 ≠ 0}"
apply (rule back_subst)
apply (rule arg_cong[of _ _ finite])
apply auto
done
hence 2: "finite {(m⇩1, m⇩2). Const (coeff P m⇩1) * Const (coeff Q m⇩2) * poly_subst_monom f (m⇩1 + m⇩2) ≠ 0}"
apply (rule rev_finite_subset)
apply (auto simp add: Const_zero)
done
have "Sum_any (λm. Const (Sum_any (λm⇩1. coeff P m⇩1 * Sum_any (λm⇩2. coeff Q m⇩2 when m = m⇩1 + m⇩2))) * poly_subst_monom f m) =
Sum_any (λm. Sum_any (λm⇩1. (Const (coeff P m⇩1)) * Sum_any (λm⇩2. Const ((coeff Q m⇩2) when m = m⇩1 + m⇩2))) * poly_subst_monom f m)"
unfolding Const_sum_Any comp_def Const_mult[symmetric] ..
also have "... = Sum_any (λm. Sum_any (λm⇩1. Sum_any (λm⇩2. (Const (coeff P m⇩1)) * Const ((coeff Q m⇩2) when m = m⇩1 + m⇩2))) * poly_subst_monom f m)"
apply (subst Sum_any_right_distrib)
subgoal by (rule rev_finite_subset[OF 1]; auto simp add: Const_zero)
subgoal ..
done
also have "... = Sum_any (λm. Sum_any (λm⇩1. Sum_any (λm⇩2. (Const (coeff P m⇩1)) * Const (coeff Q m⇩2) when m = m⇩1 + m⇩2)) * poly_subst_monom f m)"
unfolding Const_when mult_when ..
also have "... = Sum_any (λm. Sum_any (λm⇩1. Sum_any (λm⇩2. (Const (coeff P m⇩1)) * Const (coeff Q m⇩2) * poly_subst_monom f (m⇩1 + m⇩2) when m = m⇩1 + m⇩2)))"
apply (subst Sum_any_left_distrib)
subgoal by (rule finite_subset[OF _ 0]; auto simp add: Const_zero)
subgoal
apply (subst Sum_any_left_distrib)
subgoal by (rule finite_subset[OF _ 1]; auto simp add: Const_zero)
subgoal
apply (rule Sum_any.cong)
apply (rule Sum_any.cong)
apply (rule Sum_any.cong)
unfolding when_mult
apply (rule when_cong[OF refl])
apply simp
done
done
done
also have "... = Sum_any (λm⇩1. Sum_any (λm⇩2. (Const (coeff P m⇩1)) * (Const (coeff Q m⇩2)) * poly_subst_monom f (m⇩1 + m⇩2)))"
by (rule Sum_any_rev_image_add[OF 2])
also have "... = Sum_any (λm⇩1. Sum_any (λm⇩2. (Const (coeff P m⇩1) * poly_subst_monom f m⇩1) * (Const (coeff Q m⇩2) * poly_subst_monom f m⇩2)))"
unfolding poly_subst_monom_add by (simp add: algebra_simps)
also have "... = Sum_any (λm⇩1. Const (coeff P m⇩1) * poly_subst_monom f m⇩1) * Sum_any (λm⇩2. Const (coeff Q m⇩2) * poly_subst_monom f m⇩2)"
apply (rule Sum_any_product[symmetric])
subgoal by (rule finite_subset[OF _ 0]; auto simp add: Const_zero)
subgoal by (rule finite_subset[OF _ 1]; auto simp add: Const_zero)
done
finally show "Sum_any (λm. Const (Sum_any (λm⇩1. coeff P m⇩1 * Sum_any (λm⇩2. coeff Q m⇩2 when m = m⇩1 + m⇩2))) * poly_subst_monom f m) =
Sum_any (λm⇩1. Const (coeff P m⇩1) * poly_subst_monom f m⇩1) * Sum_any (λm⇩2. Const (coeff Q m⇩2) * poly_subst_monom f m⇩2)"
.
qed
lemma poly_subst_prod:
"poly_subst f (prod P A) = prod (poly_subst f ∘ P) A"
by (induct A rule: infinite_finite_induct; auto)
lemma poly_subst_monom_id: "poly_subst_monom (Var) t = monom t 1"
proof -
have "mapping_of (poly_subst_monom (Var) t) = Poly_Mapping.single t 1"
unfolding poly_subst_monom_alt
apply (subst monom.rep_eq[symmetric])
apply (subst monom_expansion)
by (subst mapping_of_inject, simp add: Const_one)
thus ?thesis
unfolding monom.abs_eq by (smt (verit) mapping_of_inverse)
qed
lemma poly_subst_id: "poly_subst (Var) p = p"
apply (induct p rule: mpoly_induct, simp_all)
apply (simp add: poly_subst_def poly_subst_monom_id)
by (smt (verit, ccfv_SIG) Const.abs_eq Const⇩0_def Sum_any.cong monom.abs_eq mult.right_neutral
poly_eq_sum_monom smult_conv_mult smult_monom)
text ‹Vars of substitutions›
lemma vars_poly_subst_monom: "vars (poly_subst_monom f t) ⊆ ⋃ (vars ` (f ` keys t))"
unfolding poly_subst_monom_alt
apply (rule subset_trans[OF vars_prod])
using vars_pow by auto
lemma vars_poly_subst_monom': "vars (poly_subst_monom ((!⇩0) ls) t) ⊆ ⋃ (vars ` set ls)"
apply (rule subset_trans[OF vars_poly_subst_monom])
unfolding nth0_def when_def keys.rep_eq
using nth_mem Const_zero MPoly_Type.degree_zero vars_non_zero_degree by force
lemma vars_poly_subst_list: "vars (poly_subst_list ls p) ⊆ ⋃ (vars ` set ls)"
unfolding poly_subst_alt comp_def poly_subst_list_def
apply (rule subset_trans[OF vars_setsum], simp_all)
using vars_poly_subst_monom' vars_mult by fastforce
lemma vars_poly_subst_monom_bounded:
"∀v∈(keys t). v ≤ bound ⟹ vars (poly_subst_monom ((!⇩0) ls) t) ⊆ ⋃ (vars ` set (take (Suc bound) ls))"
unfolding poly_subst_monom_alt
apply (rule subset_trans[OF vars_prod], auto)
apply (drule set_mp[OF vars_pow])
subgoal for m v
proof (rule bexI[of _ "ls !⇩0 v"], assumption)
assume "∀v∈(keys t). v ≤ bound"
moreover assume "v ∈ keys t"
ultimately have "v ≤ bound" by auto
moreover assume "m ∈ vars (ls !⇩0 v)"
ultimately show "ls !⇩0 v ∈ set (take (Suc bound) ls)"
apply (cases "v < length ls", simp_all add: nth0_def)
unfolding in_set_conv_nth by (intro exI[of _ v], auto)
qed done
lemma aux0: "max_vars p ≤ bound ⟹ m ∈ keys (mapping_of p) ⟹ ∀v∈(keys m). v ≤ bound"
unfolding max_vars_def vars_def by auto
lemma vars_poly_subst_list_bounded:
assumes "max_vars p ≤ bound"
shows "vars (poly_subst_list ls p) ⊆ ⋃ (vars ` set (take (Suc bound) ls))"
proof -
from assms have a: "t∈keys (mapping_of p) ⟹ ∀v∈(keys t). v ≤ bound" for t
by (simp add: aux0)
hence b: "t∈keys (mapping_of p) ⟹ vars (poly_subst_monom ((!⇩0) ls) t)
⊆ ⋃ (vars ` set (take (Suc bound) ls))" for t
by (rule vars_poly_subst_monom_bounded, simp)
show ?thesis
apply (simp add: poly_subst_list_def poly_subst_alt)
apply (rule subset_trans[OF vars_setsum], auto simp: vars_mult)
subgoal for x t
using vars_mult b[of t] apply simp
by (smt (verit, del_insts) UN_iff subset_iff sup_bot_left vars_Const vars_mult)
done
qed
lemma vars_poly_subst:
"vars (poly_subst f p) ⊆ (⋃t ∈ vars p. vars (f t))"
proof -
{
fix x y
assume "x ∈ keys (mapping_of p)"
and "y ∈ (λxa. f xa ^ lookup x xa) ` keys x"
from this obtain z where "z ∈ keys x" and y_def: "y = f z ^ lookup x z"
by auto
from this have z_in: "z ∈ vars p"
unfolding vars_def image_def
apply (intro UnionI[of "keys x" "{y. ∃x∈keys (mapping_of p). y = keys x}" z])
unfolding mem_Collect_eq
apply (rule bexI[of _ x])
using `x ∈ keys (mapping_of p)`
by auto
have 0: "vars (f z) ∈ {y. ∃x∈⋃ {y. ∃x∈keys (mapping_of p). y = keys x}.
y = ⋃ {y. ∃x∈keys (mapping_of (f x)). y = keys x}}"
unfolding mem_Collect_eq
unfolding image_def[symmetric] vars_def[symmetric] y_def
by (rule bexI[of _ z, OF _ z_in]; simp)
{
fix w
assume "w ∈ {ya. ∃x∈keys (mapping_of y). ya = keys x}"
from this obtain v where "v ∈ keys (mapping_of y)" and w_def: "w = keys v"
by auto
hence "keys v ⊆ vars y"
unfolding vars_def
by auto
have "w ⊆ vars (f z)"
unfolding w_def
apply (rule subset_trans[OF `keys v ⊆ vars y`])
unfolding y_def
by (simp add: vars_pow)
from this and 0
have "∃y. y ∈ {y. ∃x∈⋃ {y. ∃x∈keys (mapping_of p). y = keys x}.
y = ⋃ {y. ∃x∈keys (mapping_of (f x)). y = keys x}} ∧
w ⊆ y"
by auto
}
note 0 = this
hence "vars y ⊆ (⋃t∈vars p. vars (f t))"
unfolding vars_def UN_simps image_def
apply (intro Union_subsetI)
by assumption
}
note 0 = this
{
fix x
assume Hx: "x ∈ keys (mapping_of p)"
have "vars (Const (coeff p x) * poly_subst_monom f x) ⊆ vars (poly_subst_monom f x)"
apply (rule subset_trans[OF vars_mult Un_least])
by simp_all
also have "... ⊆ (⋃t∈vars p. vars (f t))"
unfolding poly_subst_monom_alt
apply (rule subset_trans[OF vars_prod])
apply (rule UN_least)
using 0[OF Hx] by assumption
finally have "vars (Const (coeff p x) * poly_subst_monom f x) ⊆ (⋃t∈vars p. vars (f t))" .
}
note 0 = this
show ?thesis
unfolding poly_subst_alt
apply (rule subset_trans[OF vars_setsum[OF finite_keys]])
apply (rule UN_least)
using 0 by assumption
qed
lemma max_vars_poly_subst_list_general:
shows "max_vars (poly_subst_list ls p) ≤ Max (max_vars ` set ls)"
unfolding max_vars_def
apply (rule Max.boundedI, auto simp add: vars_finite)
subgoal for a
proof -
assume "a ∈ vars (poly_subst_list ls p)"
hence "a ∈ ⋃ (vars ` set ls)" using vars_poly_subst_list by force
thus "a ≤ (MAX P∈set ls. Max (insert 0 (vars P)))"
apply simp
by (smt (verit, best) List.finite_set Max_ge dual_order.trans finite_imageI finite_insert
imageI insert_absorb insert_subset subset_insertI vars_finite)
qed done
lemma max_vars_poly_subst_list_bounded:
"max_vars p ≤ bound ⟹ max_vars (poly_subst_list ls p) ≤ Max (max_vars ` set (take (Suc bound) ls))"
proof -
assume a: "max_vars p ≤ bound"
{
fix a
assume "a ∈ vars (poly_subst_list ls p)"
hence "a ∈ ⋃ (vars ` set (take (Suc bound) ls))"
using vars_poly_subst_list_bounded[OF a] by auto
hence "a ≤ (MAX P∈set (take (Suc bound) ls). Max (insert 0 (vars P)))"
apply simp
by (smt (verit, best) List.finite_set Max_ge dual_order.trans finite_imageI finite_insert
imageI insert_absorb insert_subset subset_insertI vars_finite)
} note b = this
show ?thesis
unfolding max_vars_def
by (rule Max.boundedI, auto simp add: vars_finite b)
qed
lemma max_vars_id:
fixes p :: "'a::{comm_semiring_1,ring_no_zero_divisors} mpoly"
shows "max_vars (poly_subst_list (map Var [0..<Suc k]) p) ≤ k"
by (rule le_trans[OF max_vars_poly_subst_list_general], auto simp: max_vars_def)
text ‹Degrees of substitutions›
lemma degree_poly_subst_monom:
fixes f
assumes "finite {k. f k ≠ 0}"
defines "degree_monom ≡ (λm t. (lookup m) t)"
shows "degree (poly_subst_monom f m) v
≤ (∑t | v∈vars (f t). degree_monom m t * degree (f t) v)"
proof -
have a0: "v ∉ vars (f k) ⟹ degree (f k ^ lookup m k) v = 0" for k
unfolding le_0_eq[of "degree _ v", symmetric]
apply (rule le_trans[OF degree_pow])
by (simp add: in_vars_non_zero_degree)
have a1: "(∑t | v ∈ vars (f t). lookup m t * degree (f t) v)
= (∑t | t ∈ keys m ∧ v ∈ vars (f t). lookup m t * degree (f t) v)"
unfolding keys.rep_eq apply (rule sum.mono_neutral_right, auto)
using assms
by (smt (verit, del_insts) MPoly_Type.degree_zero finite_nat_set_iff_bounded
in_vars_non_zero_degree mem_Collect_eq)
show ?thesis
unfolding poly_subst_monom_alt degree_monom_def
apply (subst a1)
apply (rule le_trans[OF degree_prod[OF finite_keys]])
apply (subst sum.setdiff_irrelevant[OF finite_keys,
of "λk. degree (f k ^ lookup m k) v", symmetric])
apply (rule le_trans[OF sum_mono[OF degree_pow]])
apply (rule sum_mono2, auto)
by (rule ccontr, auto simp: a0)
qed
lemma degree_poly_subst:
fixes p :: "'a::comm_ring_1 mpoly"
fixes f :: "nat ⇒ 'a mpoly"
assumes "finite {k. f k ≠ 0}"
shows "degree (poly_subst f p) v ≤ (∑t | v ∈ vars (f t). degree p t * degree (f t) v)"
proof -
have "a ∈ keys (mapping_of p) ⟹ degree (poly_subst_monom f a) v
≤ (∑t | v ∈ vars (f t). degree p t * degree (f t) v)" for a
apply (rule le_trans[OF degree_poly_subst_monom[of f, OF assms]])
apply (rule sum_mono, simp)
unfolding degree.rep_eq by auto
hence a0: "Max (insert 0 ((λi. degree (poly_subst_monom f i) v) ` keys (mapping_of p)))
≤ (∑t | v ∈ vars (f t). degree p t * degree (f t) v)"
by auto
show ?thesis
unfolding poly_subst_alt
apply (rule le_trans[OF _ a0])
apply (rule le_trans[OF degree_sum[OF finite_keys, of "λt. Const (coeff p t) * poly_subst_monom f t"
"mapping_of p" v]])
using degree_mult degree_Const
by simp (smt (verit, best) Max.coboundedI add_cancel_right_right degree_Const degree_mult
finite_imageI finite_insert finite_keys imageI insert_iff le_trans mult.commute)
qed
lemma degree_poly_subst':
fixes p :: "'a::comm_ring_1 mpoly"
fixes f :: "nat ⇒ 'a mpoly"
assumes "finite {k. f k ≠ 0}"
shows "degree (poly_subst f p) v ≤ (∑t∈vars p. degree p t * degree (f t) v)"
apply (rule le_trans[OF degree_poly_subst], simp add: assms)
apply (subst sum.mono_neutral_right[of "{t. v ∈ vars (f t)}" "vars p ∩ {t. v ∈ vars (f t)}"])
using in_vars_non_zero_degree assms
subgoal by (smt (verit) Collect_mono emptyE rev_finite_subset vars_zero vars_finite)
subgoal by auto
subgoal using in_vars_non_zero_degree by auto
subgoal by (simp add: sum_mono2 vars_finite)
done
lemma degree_poly_subst_list:
fixes p :: "'a::comm_ring_1 mpoly"
shows "degree (poly_subst_list ls p) v ≤ (∑t | v ∈ vars (ls !⇩0 t). degree p t * degree (ls !⇩0 t) v)"
unfolding poly_subst_list_def
using degree_poly_subst[OF nth0_finite] by auto
lemma degree_poly_subst_list':
fixes p :: "'a::comm_ring_1 mpoly"
shows "degree (poly_subst_list ls p) v ≤ (∑t ≤ length ls. degree p t * degree (ls !⇩0 t) v)"
apply (rule le_trans[OF degree_poly_subst_list])
by (rule sum_mono2, auto simp: nth0_def when_def in_vars_non_zero_degree)
text ‹Total degree of substitions›
lemma deg_imp_tot_deg_zero: "(∀v ∈ vars P. degree P v = 0) ⟹ total_degree P = 0"
by (metis bot_nat_0.extremum_uniqueI sum.neutral total_degree_bound)
lemma total_degree_poly_subst_monom:
fixes f
defines "degree_monom ≡ (λm t. (lookup m) t)"
shows "total_degree (poly_subst_monom f m)
≤ (∑t∈keys m. degree_monom m t * total_degree (f t))"
unfolding poly_subst_monom_alt degree_monom_def
apply (rule le_trans[OF total_degree_prod[OF finite_keys]])
apply (rule le_trans[OF sum_mono[OF total_degree_pow]])
by (rule sum_mono2) auto
lemma total_degree_poly_subst:
shows "total_degree (poly_subst f p) ≤ (∑t∈vars p. degree p t * total_degree (f t))"
proof -
have "a ∈ keys (mapping_of p) ⟹ total_degree (poly_subst_monom f a)
≤ (∑t∈vars p. degree p t * total_degree (f t))" for a
apply (rule le_trans[OF total_degree_poly_subst_monom[of f]])
apply (rule sum_le_included[of _ _ _ "λx. x"], auto simp add: vars_finite vars_def)
unfolding degree.rep_eq by auto
hence a0: "Max (insert 0 ((λi. total_degree (poly_subst_monom f i)) ` keys (mapping_of p)))
≤ (∑t∈vars p. degree p t * total_degree (f t))"
by auto
show ?thesis
unfolding poly_subst_alt
apply (rule le_trans[OF _ a0])
apply (rule le_trans[OF total_degree_sum[OF finite_keys]])
using total_degree_mult total_degree_Const
apply simp
by (smt (verit, del_insts) Max_ge add_0 dual_order.trans finite_imageI finite_insert
finite_keys image_eqI insert_iff total_degree_Const total_degree_mult)
qed
lemma total_degree_poly_subst_list:
fixes p :: "'a::comm_ring_1 mpoly"
shows "total_degree (poly_subst_list ls p) ≤ (∑t∈vars p. degree p t * total_degree (ls !⇩0 t))"
unfolding poly_subst_list_def
using total_degree_poly_subst by auto
lemma total_degree_poly_subst_list':
fixes p :: "'a::comm_ring_1 mpoly"
assumes "max_vars p ≤ length ls"
shows "total_degree (poly_subst_list ls p) ≤ (∑t≤length ls. degree p t * total_degree (ls !⇩0 t))"
apply (rule le_trans[OF total_degree_poly_subst_list])
apply (cases "vars p = {}", simp_all)
apply (rule sum_mono2, simp_all)
using assms[unfolded max_vars_def]
by (simp add: subset_iff vars_finite)
lemma total_degree_poly_subst_list'':
fixes p :: "'a::comm_ring_1 mpoly"
assumes "∀i ≤ length ls. card (vars (ls ! i)) ≤ 1"
shows "total_degree (poly_subst_list ls p) ≤
length ls * (∑t ≤ length ls. degree p t * total_degree (ls !⇩0 t))"
proof -
from assms have asm: "⋀i. i ∈ set ls ⟹ card (vars i) ≤ 1"
by (metis in_set_conv_nth less_or_eq_imp_le)
have card0: "card (vars (poly_subst_list ls p)) ≤ length ls"
apply (rule le_trans[OF card_mono[OF _ vars_poly_subst_list]], simp add: vars_finite)
apply (rule le_trans[OF card_UN_le], simp)
apply (rule le_trans[OF sum_bounded_above[OF asm]])
by (auto simp add: card_length)
have "sum (degree (poly_subst_list ls p)) (vars (poly_subst_list ls p))
≤ sum (λv. ∑t ≤ length ls. degree p t * degree (ls !⇩0 t) v) (vars (poly_subst_list ls p))"
apply (rule sum_mono)
using degree_poly_subst_list' by auto
also have "... = (∑t ≤ length ls. degree p t * sum (degree (ls !⇩0 t)) (vars (poly_subst_list ls p)))"
apply (subst sum.swap)
by (subst sum_distrib_left, simp)
also have "... ≤ (∑t ≤ length ls. degree p t * length ls * total_degree (ls !⇩0 t))"
apply (rule sum_mono, auto)
apply (rule le_trans[OF sum_bounded_above, of _ _ "total_degree (ls !⇩0 _)"])
using degree_total_degree_bound vars_poly_subst_list card0 by auto
finally show ?thesis
apply simp
apply (rule le_trans[OF total_degree_bound])
apply (subst sum_distrib_left)
by (smt (verit) ab_semigroup_mult_class.mult_ac(1) mult.commute sum.cong)
qed
end