Theory RRI_Misc
section ‹Misc results about polynomials›
theory RRI_Misc imports
"HOL-Computational_Algebra.Computational_Algebra"
"Budan_Fourier.BF_Misc"
"Polynomial_Interpolation.Ring_Hom_Poly"
begin
subsection ‹Misc›
declare pcompose_pCons[simp del]
lemma Setcompr_subset: "⋀f P S. {f x | x. P x} ⊆ S = (∀ x. P x ⟶ f x ∈ S)"
by blast
lemma map_cong':
assumes "xs = map h ys" and "⋀y. y ∈ set ys ⟹ f (h y) = g y"
shows "map f xs = map g ys"
using assms map_replicate_trivial by simp
lemma nth_default_replicate_eq:
"nth_default dflt (replicate n x) i = (if i < n then x else dflt)"
by (auto simp: nth_default_def)
lemma square_bounded_less:
fixes a b::"'a :: linordered_ring_strict"
shows "-a < b ∧ b < a ⟹ b*b < a*a"
by (metis (no_types, lifting) leD leI minus_less_iff minus_mult_minus mult_strict_mono'
neg_less_eq_nonneg neg_less_pos verit_minus_simplify(4) zero_le_mult_iff zero_le_square)
lemma square_bounded_le:
fixes a b::"'a :: linordered_ring_strict"
shows "-a ≤ b ∧ b ≤ a ⟹ b*b ≤ a*a"
by (metis le_less minus_mult_minus square_bounded_less)
context vector_space
begin
lemma card_le_dim_spanning:
assumes BV: "B ⊆ V"
and VB: "V ⊆ span B"
and fB: "finite B"
and dVB: "dim V ≥ card B"
shows "independent B"
proof -
{
fix a
assume a: "a ∈ B" "a ∈ span (B - {a})"
from a fB have c0: "card B ≠ 0"
by auto
from a fB have cb: "card (B - {a}) = card B - 1"
by auto
{
fix x
assume x: "x ∈ V"
from a have eq: "insert a (B - {a}) = B"
by blast
from x VB have x': "x ∈ span B"
by blast
from span_trans[OF a(2), unfolded eq, OF x']
have "x ∈ span (B - {a})" .
}
then have th1: "V ⊆ span (B - {a})"
by blast
have th2: "finite (B - {a})"
using fB by auto
from dim_le_card[OF th1 th2]
have c: "dim V ≤ card (B - {a})" .
from c c0 dVB cb have False by simp
}
then show ?thesis
unfolding dependent_def by blast
qed
end
subsection ‹Misc results about polynomials›
lemma smult_power: "smult (x^n) (p^n) = smult x p ^ n"
apply (induction n)
subgoal by fastforce
by (metis smult_power)
lemma reflect_poly_monom: "reflect_poly (monom n i) = monom n 0"
apply (induction i)
by (auto simp: coeffs_eq_iff coeffs_monom coeffs_reflect_poly)
lemma poly_eq_by_eval:
fixes P Q :: "'a::{comm_ring_1,ring_no_zero_divisors,ring_char_0} poly"
assumes h: "⋀x. poly P x = poly Q x" shows "P = Q"
proof -
have "poly P = poly Q" using h by fast
thus ?thesis by (auto simp: poly_eq_poly_eq_iff)
qed
lemma poly_binomial:
"[:(1::'a::comm_ring_1), 1:]^n = (∑k≤n. monom (of_nat (n choose k)) k)"
proof -
have "[:(1::'a::comm_ring_1), 1:]^n = (monom 1 1 + 1)^n"
by (metis (no_types, lifting) add.left_neutral add.right_neutral add_pCons
monom_altdef pCons_one power_one_right smult_1_left)
also have "... = (∑k≤n. of_nat (n choose k) * monom 1 1 ^ k)"
apply (subst binomial_ring)
by force
also have "... = (∑k≤n. monom (of_nat (n choose k)) k)"
by (auto simp: monom_altdef of_nat_poly)
finally show ?thesis .
qed
lemma degree_0_iff: "degree P = 0 ⟷ (∃a. P = [:a:])"
by (meson degree_eq_zeroE degree_pCons_0)