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)