# HG changeset patch # User Manuel Eberl # Date 1711736939 -3600 # Node ID 4c1347e172b1c6f0d3c1d40adb4c2ec33f944f1b # Parent f82639fe786e5a811af6d5e94e54bc6556f774fb moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields diff -r f82639fe786e -r 4c1347e172b1 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Sat Mar 30 01:12:48 2024 +0100 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Fri Mar 29 19:28:59 2024 +0100 @@ -79,7 +79,7 @@ qed -subsubsection \Definition of basic zero, one, constant, X, and inverse X elements\ +subsubsection \Definition of basic Laurent series\ instantiation fls :: (zero) zero begin @@ -2008,14 +2008,13 @@ subsubsection \Inverses\ -\ \See lemma fls_left_inverse\ + abbreviation fls_left_inverse :: "'a::{comm_monoid_add,uminus,times} fls \ 'a \ 'a fls" where "fls_left_inverse f x \ fls_shift (fls_subdegree f) (fps_to_fls (fps_left_inverse (fls_base_factor_to_fps f) x))" -\ \See lemma fls_right_inverse\ abbreviation fls_right_inverse :: "'a::{comm_monoid_add,uminus,times} fls \ 'a \ 'a fls" where @@ -2605,7 +2604,7 @@ lemma fls_left_inverse_idempotent_ring1: fixes f :: "'a::ring_1 fls" assumes "x * f $$ fls_subdegree f = 1" "y * x = 1" - \ \These assumptions imply y equals f $$ fls_subdegree f, but no need to assume that.\ + \ \These assumptions imply y equals \f $$ fls_subdegree f\, but no need to assume that.\ shows "fls_left_inverse (fls_left_inverse f x) y = f" proof- from assms(1) have @@ -2630,7 +2629,7 @@ lemma fls_right_inverse_idempotent_ring1: fixes f :: "'a::ring_1 fls" assumes "f $$ fls_subdegree f * x = 1" "x * y = 1" - \ \These assumptions imply y equals f $$ fls_subdegree f, but no need to assume that.\ + \ \These assumptions imply y equals \f $$ fls_subdegree f\, but no need to assume that.\ shows "fls_right_inverse (fls_right_inverse f x) y = f" proof- from assms(1) have @@ -3645,7 +3644,7 @@ subsection \Formal differentiation and integration\ -subsubsection \Derivative definition and basic properties\ +subsubsection \Derivative\ definition "fls_deriv f = Abs_fls (\n. of_int (n+1) * f$$(n+1))" @@ -3802,7 +3801,7 @@ qed -subsubsection \Algebra rules of the derivative\ +subsubsection \Algebraic rules of the derivative\ lemma fls_deriv_add [simp]: "fls_deriv (f+g) = fls_deriv f + fls_deriv g" by (auto intro: fls_eqI simp: algebra_simps) @@ -4155,7 +4154,6 @@ subsubsection \Integral definition and basic properties\ -\ \To incorporate a constant of integration, just add an fps_const.\ definition fls_integral :: "'a::{ring_1,inverse} fls \ 'a fls" where "fls_integral a = Abs_fls (\n. if n=0 then 0 else inverse (of_int n) * a$$(n - 1))" @@ -4371,7 +4369,7 @@ qed -subsubsection \Algebra rules of the integral\ +subsubsection \Algebraic rules of the integral\ lemma fls_integral_add [simp]: "fls_integral (f+g) = fls_integral f + fls_integral g" by (intro fls_eqI) (simp add: algebra_simps) @@ -4580,7 +4578,7 @@ unfolding open_dist subset_eq by simp -subsection \Notation bundle\ +subsection \Notation\ no_notation fls_nth (infixl "$$" 75) diff -r f82639fe786e -r 4c1347e172b1 src/HOL/Computational_Algebra/Formal_Power_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sat Mar 30 01:12:48 2024 +0100 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Fri Mar 29 19:28:59 2024 +0100 @@ -44,7 +44,7 @@ lemma fps_zero_nth [simp]: "0 $ n = 0" unfolding fps_zero_def by simp -lemma fps_nonzero_nth: "f \ 0 \ (\ n. f $n \ 0)" +lemma fps_nonzero_nth: "f \ 0 \ (\ n. f $ n \ 0)" by (simp add: expand_fps_eq) lemma fps_nonzero_nth_minimal: "f \ 0 \ (\n. f $ n \ 0 \ (\m < n. f $ m = 0))" @@ -412,8 +412,7 @@ by (auto simp: fps_mult_nth_conv_inside_subdegrees) -subsection \Formal power series form a commutative ring with unity, if the range of sequences - they represent is a commutative ring with unity\ +subsection \Ring structure\ instance fps :: (semigroup_add) semigroup_add proof @@ -539,8 +538,6 @@ instance fps :: (semiring_1_cancel) semiring_1_cancel .. -subsection \Selection of the nth power of the implicit variable in the infinite sum\ - lemma fps_square_nth: "(f^2) $ n = (\k\n. f $ k * f $ (n - k))" by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost) @@ -554,8 +551,6 @@ qed -subsection \Injection of the basic ring elements and multiplication by scalars\ - definition "fps_const c = Abs_fps (\n. if n = 0 then c else 0)" lemma fps_nth_fps_const [simp]: "fps_const c $ n = (if n = 0 then c else 0)" @@ -619,8 +614,6 @@ by (induct n) auto -subsection \Formal power series form an integral domain\ - instance fps :: (ring) ring .. instance fps :: (comm_ring) comm_ring .. @@ -791,8 +784,6 @@ by (cases "f = 0"; induction n) simp_all -subsection \The efps_Xtractor series fps_X\ - lemma minus_one_power_iff: "(- (1::'a::ring_1)) ^ n = (if even n then 1 else - 1)" by (induct n) auto @@ -1324,7 +1315,7 @@ thus ?thesis by (simp add: fps_mult_nth) qed -subsection \Formal Power series form a metric space\ +subsection \Metrizability\ instantiation fps :: ("{minus,zero}") dist begin @@ -1472,7 +1463,7 @@ qed -subsection \Inverses and division of formal power series\ +subsection \Division\ declare sum.cong[fundef_cong] @@ -1483,7 +1474,7 @@ | "fps_left_inverse_constructor f a (Suc n) = - sum (\i. fps_left_inverse_constructor f a i * f$(Suc n - i)) {0..n} * a" -\ \This will construct a left inverse for f in case that x * f$0 = 1\ +\ \This will construct a left inverse for f in case that \<^prop>\x * f$0 = 1\\ abbreviation "fps_left_inverse \ (\f x. Abs_fps (fps_left_inverse_constructor f x))" fun fps_right_inverse_constructor :: @@ -1493,7 +1484,7 @@ | "fps_right_inverse_constructor f a n = - a * sum (\i. f$i * fps_right_inverse_constructor f a (n - i)) {1..n}" -\ \This will construct a right inverse for f in case that f$0 * y = 1\ +\ \This will construct a right inverse for f in case that \<^prop>\f$0 * y = 1\\ abbreviation "fps_right_inverse \ (\f y. Abs_fps (fps_right_inverse_constructor f y))" instantiation fps :: ("{comm_monoid_add,inverse,times,uminus}") inverse @@ -1721,14 +1712,14 @@ qed (simp add: f0 fps_inverse_def) qed -\ \ +text \ It is possible in a ring for an element to have a left inverse but not a right inverse, or vice versa. But when an element has both, they must be the same. \ lemma fps_left_inverse_eq_fps_right_inverse: fixes f :: "'a::ring_1 fps" assumes f0: "x * f$0 = 1" "f $ 0 * y = 1" - \ \These assumptions imply x equals y, but no need to assume that.\ + \ \These assumptions imply that $x$ equals $y$, but no need to assume that.\ shows "fps_left_inverse f x = fps_right_inverse f y" proof- from f0(2) have "f * fps_right_inverse f y = 1" @@ -1751,7 +1742,7 @@ lemma fps_left_inverse': fixes f :: "'a::ring_1 fps" assumes "x * f$0 = 1" "f$0 * y = 1" - \ \These assumptions imply x equals y, but no need to assume that.\ + \ \These assumptions imply $x$ equals $y$, but no need to assume that.\ shows "fps_right_inverse f y * f = 1" using assms fps_left_inverse_eq_fps_right_inverse[of x f y] fps_left_inverse[of x f] by simp @@ -1759,7 +1750,7 @@ lemma fps_right_inverse': fixes f :: "'a::ring_1 fps" assumes "x * f$0 = 1" "f$0 * y = 1" - \ \These assumptions imply x equals y, but no need to assume that.\ + \ \These assumptions imply $x$ equals $y$, but no need to assume that.\ shows "f * fps_left_inverse f x = 1" using assms fps_left_inverse_eq_fps_right_inverse[of x f y] fps_right_inverse[of f y] by simp @@ -1808,7 +1799,7 @@ lemma fps_left_inverse_idempotent_ring1: fixes f :: "'a::ring_1 fps" assumes "x * f$0 = 1" "y * x = 1" - \ \These assumptions imply y equals f$0, but no need to assume that.\ + \ \These assumptions imply $y$ equals \f$0\, but no need to assume that.\ shows "fps_left_inverse (fps_left_inverse f x) y = f" proof- from assms(1) have @@ -1831,7 +1822,7 @@ lemma fps_right_inverse_idempotent_ring1: fixes f :: "'a::ring_1 fps" assumes "f$0 * x = 1" "x * y = 1" - \ \These assumptions imply y equals f$0, but no need to assume that.\ + \ \These assumptions imply $y$ equals \f$0\, but no need to assume that.\ shows "fps_right_inverse (fps_right_inverse f x) y = f" proof- from assms(1) have "f * (fps_right_inverse f x * fps_right_inverse (fps_right_inverse f x) y) = @@ -2854,7 +2845,7 @@ end -subsection \Formal power series form a Euclidean ring\ +subsection \Euclidean division\ instantiation fps :: (field) euclidean_ring_cancel begin @@ -2994,7 +2985,7 @@ -subsection \Formal Derivatives, and the MacLaurin theorem around 0\ +subsection \Formal Derivatives\ definition "fps_deriv f = Abs_fps (\n. of_nat (n + 1) * f $ (n + 1))" @@ -3196,7 +3187,7 @@ lemma fps_deriv_lr_inverse: fixes x y :: "'a::ring_1" assumes "x * f$0 = 1" "f$0 * y = 1" - \ \These assumptions imply x equals y, but no need to assume that.\ + \ \These assumptions imply $x$ equals $y$, but no need to assume that.\ shows "fps_deriv (fps_left_inverse f x) = - fps_left_inverse f x * fps_deriv f * fps_left_inverse f x" and "fps_deriv (fps_right_inverse f y) = @@ -3622,7 +3613,7 @@ qed -subsection \Composition of FPSs\ +subsection \Composition\ definition fps_compose :: "'a::semiring_1 fps \ 'a fps \ 'a fps" (infixl "oo" 55) where "a oo b = Abs_fps (\n. sum (\i. a$i * (b^i$n)) {0..n})" @@ -3722,10 +3713,10 @@ subsubsection \Rule 3\ -text \Rule 3 is trivial and is given by \fps_times_def\.\ - - -subsubsection \Rule 5 --- summation and "division" by (1 - fps_X)\ +text \Rule 3 is trivial and is given by \texttt{fps\_times\_def}.\ + + +subsubsection \Rule 5 --- summation and ``division'' by $1 - X$\ lemma fps_divide_fps_X_minus1_sum_lemma: "a = ((1::'a::ring_1 fps) - fps_X) * Abs_fps (\n. sum (\i. a $ i) {0..n})" @@ -3759,8 +3750,10 @@ using fps_divide_fps_X_minus1_sum_ring1[of a] by simp -subsubsection \Rule 4 in its more general form: generalizes Rule 3 for an arbitrary - finite product of FPS, also the relvant instance of powers of a FPS\ +subsubsection \Rule 4 in its more general form\ + +text \This generalizes Rule 3 for an arbitrary + finite product of FPS, also the relevant instance of powers of a FPS.\ definition "natpermute n k = {l :: nat list. length l = k \ sum_list l = n}" @@ -4619,7 +4612,7 @@ by (simp add: divide_inverse fps_divide_def) -subsection \Derivative of composition\ +subsection \Chain rule\ lemma fps_compose_deriv: fixes a :: "'a::idom fps" @@ -4658,9 +4651,6 @@ then show ?thesis by (simp add: fps_eq_iff) qed - -subsection \Finite FPS (i.e. polynomials) and fps_X\ - lemma fps_poly_sum_fps_X: assumes "\i > n. a$i = 0" shows "a = sum (\i. fps_const (a$i) * fps_X^i) {0..n}" (is "a = ?r") @@ -5742,7 +5732,7 @@ qed -subsubsection \Formal trigonometric functions\ +subsubsection \Trigonometric functions\ definition "fps_sin (c::'a::field_char_0) = Abs_fps (\n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))" diff -r f82639fe786e -r 4c1347e172b1 src/HOL/Computational_Algebra/Fraction_Field.thy --- a/src/HOL/Computational_Algebra/Fraction_Field.thy Sat Mar 30 01:12:48 2024 +0100 +++ b/src/HOL/Computational_Algebra/Fraction_Field.thy Fri Mar 29 19:28:59 2024 +0100 @@ -2,8 +2,7 @@ Author: Amine Chaieb, University of Cambridge *) -section\A formalization of the fraction field of any integral domain; - generalization of theory Rat from int to any integral domain\ +section\The fraction field of any integral domain\ theory Fraction_Field imports Main diff -r f82639fe786e -r 4c1347e172b1 src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Sat Mar 30 01:12:48 2024 +0100 +++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Fri Mar 29 19:28:59 2024 +0100 @@ -518,7 +518,7 @@ text \Fundamental theorem of algebra\ -lemma fundamental_theorem_of_algebra: +theorem fundamental_theorem_of_algebra: assumes nc: "\ constant (poly p)" shows "\z::complex. poly p z = 0" using nc @@ -779,6 +779,92 @@ by (metis degree_eq_zeroE pcompose_const poly_0 poly_pcompose that) qed +lemma complex_poly_decompose: + "smult (lead_coeff p) (\z|poly p z = 0. [:-z, 1:] ^ order z p) = (p :: complex poly)" +proof (induction p rule: poly_root_order_induct) + case (no_roots p) + show ?case + proof (cases "degree p = 0") + case False + hence "\constant (poly p)" by (subst constant_degree) + with fundamental_theorem_of_algebra and no_roots show ?thesis by blast + qed (auto elim!: degree_eq_zeroE) +next + case (root p x n) + from root have *: "{z. poly ([:- x, 1:] ^ n * p) z = 0} = insert x {z. poly p z = 0}" + by auto + have "smult (lead_coeff ([:-x, 1:] ^ n * p)) + (\z|poly ([:-x,1:] ^ n * p) z = 0. [:-z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = + [:- x, 1:] ^ order x ([:- x, 1:] ^ n * p) * + smult (lead_coeff p) (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p))" + by (subst *, subst prod.insert) + (insert root, auto intro: poly_roots_finite simp: mult_ac lead_coeff_mult lead_coeff_power) + also have "order x ([:- x, 1:] ^ n * p) = n" + using root by (subst order_mult) (auto simp: order_power_n_n order_0I) + also have "(\z\{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = + (\z\{z. poly p z = 0}. [:- z, 1:] ^ order z p)" + proof (intro prod.cong refl, goal_cases) + case (1 y) + with root have "order y ([:-x,1:] ^ n) = 0" by (intro order_0I) auto + thus ?case using root by (subst order_mult) auto + qed + also note root.IH + finally show ?case . +qed simp_all + +instance complex :: alg_closed_field + by standard (use fundamental_theorem_of_algebra constant_degree neq0_conv in blast) + +lemma size_proots_complex: "size (proots (p :: complex poly)) = degree p" +proof (cases "p = 0") + case [simp]: False + show "size (proots p) = degree p" + by (subst (1 2) complex_poly_decompose [symmetric]) + (simp add: proots_prod proots_power degree_prod_sum_eq degree_power_eq) +qed auto + +lemma complex_poly_decompose_multiset: + "smult (lead_coeff p) (\x\#proots p. [:-x, 1:]) = (p :: complex poly)" +proof (cases "p = 0") + case False + hence "(\x\#proots p. [:-x, 1:]) = (\x | poly p x = 0. [:-x, 1:] ^ order x p)" + by (subst image_prod_mset_multiplicity) simp_all + also have "smult (lead_coeff p) \ = p" + by (rule complex_poly_decompose) + finally show ?thesis . +qed auto + +lemma complex_poly_decompose': + obtains root where "smult (lead_coeff p) (\ix\#proots p. [:-x, 1:])" + by (rule complex_poly_decompose_multiset [symmetric]) + also have "(\x\#proots p. [:-x, 1:]) = (\x\roots. [:-x, 1:])" + by (subst prod_mset_prod_list [symmetric]) (simp add: roots) + also have "\ = (\iii. roots ! i"]) auto +qed + +lemma complex_poly_decompose_rsquarefree: + assumes "rsquarefree p" + shows "smult (lead_coeff p) (\z|poly p z = 0. [:-z, 1:]) = (p :: complex poly)" +proof (cases "p = 0") + case False + have "(\z|poly p z = 0. [:-z, 1:]) = (\z|poly p z = 0. [:-z, 1:] ^ order z p)" + using assms False by (intro prod.cong) (auto simp: rsquarefree_root_order) + also have "smult (lead_coeff p) \ = p" + by (rule complex_poly_decompose) + finally show ?thesis . +qed auto + + text \Arithmetic operations on multivariate polynomials.\ lemma mpoly_base_conv: diff -r f82639fe786e -r 4c1347e172b1 src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Sat Mar 30 01:12:48 2024 +0100 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Fri Mar 29 19:28:59 2024 +0100 @@ -80,12 +80,41 @@ lemma MOST_coeff_eq_0: "\\<^sub>\ n. coeff p n = 0" using coeff [of p] by simp +lemma coeff_Abs_poly: + assumes "\i. i > n \ f i = 0" + shows "coeff (Abs_poly f) = f" +proof (rule Abs_poly_inverse, clarify) + have "eventually (\i. i > n) cofinite" + by (auto simp: MOST_nat) + thus "eventually (\i. f i = 0) cofinite" + by eventually_elim (use assms in auto) +qed + subsection \Degree of a polynomial\ definition degree :: "'a::zero poly \ nat" where "degree p = (LEAST n. \i>n. coeff p i = 0)" +lemma degree_cong: + assumes "\i. coeff p i = 0 \ coeff q i = 0" + shows "degree p = degree q" +proof - + have "(\n. \i>n. poly.coeff p i = 0) = (\n. \i>n. poly.coeff q i = 0)" + using assms by (auto simp: fun_eq_iff) + thus ?thesis + by (simp only: degree_def) +qed + +lemma coeff_Abs_poly_If_le: + "coeff (Abs_poly (\i. if i \ n then f i else 0)) = (\i. if i \ n then f i else 0)" +proof (rule Abs_poly_inverse, clarify) + have "eventually (\i. i > n) cofinite" + by (auto simp: MOST_nat) + thus "eventually (\i. (if i \ n then f i else 0) = 0) cofinite" + by eventually_elim auto +qed + lemma coeff_eq_0: assumes "degree p < n" shows "coeff p n = 0" @@ -156,6 +185,23 @@ lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \ p = 0" by (cases "p = 0") (simp_all add: leading_coeff_neq_0) +lemma degree_lessI: + assumes "p \ 0 \ n > 0" "\k\n. coeff p k = 0" + shows "degree p < n" +proof (cases "p = 0") + case False + show ?thesis + proof (rule ccontr) + assume *: "\(degree p < n)" + define d where "d = degree p" + from \p \ 0\ have "coeff p d \ 0" + by (auto simp: d_def) + moreover have "coeff p d = 0" + using assms(2) * by (auto simp: not_less) + ultimately show False by contradiction + qed +qed (use assms in auto) + lemma eq_zero_or_degree_less: assumes "degree p \ n" and "coeff p n = 0" shows "p = 0 \ degree p < n" @@ -192,6 +238,9 @@ lemmas coeff_pCons = pCons.rep_eq +lemma coeff_pCons': "poly.coeff (pCons c p) n = (if n = 0 then c else poly.coeff p (n - 1))" + by transfer'(auto split: nat.splits) + lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a" by transfer simp @@ -811,6 +860,12 @@ lemma poly_sum: "poly (\k\A. p k) x = (\k\A. poly (p k) x)" by (induct A rule: infinite_finite_induct) simp_all +lemma poly_sum_list: "poly (\p\ps. p) y = (\p\ps. poly p y)" + by (induction ps) auto + +lemma poly_sum_mset: "poly (\x\#A. p x) y = (\x\#A. poly (p x) y)" + by (induction A) auto + lemma degree_sum_le: "finite S \ (\p. p \ S \ degree (f p) \ n) \ degree (sum f S) \ n" proof (induct S rule: finite_induct) case empty @@ -823,6 +878,11 @@ unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le) qed +lemma degree_sum_less: + assumes "\x. x \ A \ degree (f x) < n" "n > 0" + shows "degree (sum f A) < n" + using assms by (induction rule: infinite_finite_induct) (auto intro!: degree_add_less) + lemma poly_as_sum_of_monoms': assumes "degree p \ n" shows "(\i\n. monom (coeff p i) i) = p" @@ -1013,6 +1073,9 @@ by (cases n) (simp_all add: sum.atMost_Suc_shift del: sum.atMost_Suc) qed +lemma coeff_mult_0: "coeff (p * q) 0 = coeff p 0 * coeff q 0" + by (simp add: coeff_mult) + lemma degree_mult_le: "degree (p * q) \ degree p + degree q" proof (rule degree_le) show "\i>degree p + degree q. coeff (p * q) i = 0" @@ -1084,6 +1147,9 @@ instance poly :: (comm_ring_1) comm_ring_1 .. instance poly :: (comm_ring_1) comm_semiring_1_cancel .. +lemma prod_smult: "(\x\A. smult (c x) (p x)) = smult (prod c A) (prod p A)" + by (induction A rule: infinite_finite_induct) (auto simp: mult_ac) + lemma degree_power_le: "degree (p ^ n) \ degree p * n" by (induct n) (auto intro: order_trans degree_mult_le) @@ -1103,6 +1169,18 @@ lemma poly_prod: "poly (\k\A. p k) x = (\k\A. poly (p k) x)" by (induct A rule: infinite_finite_induct) simp_all +lemma poly_prod_list: "poly (\p\ps. p) y = (\p\ps. poly p y)" + by (induction ps) auto + +lemma poly_prod_mset: "poly (\x\#A. p x) y = (\x\#A. poly (p x) y)" + by (induction A) auto + +lemma poly_const_pow: "[: c :] ^ n = [: c ^ n :]" + by (induction n) (auto simp: algebra_simps) + +lemma monom_power: "monom c n ^ k = monom (c ^ k) (n * k)" + by (induction k) (auto simp: mult_monom) + lemma degree_prod_sum_le: "finite S \ degree (prod f S) \ sum (degree \ f) S" proof (induct S rule: finite_induct) case empty @@ -1261,6 +1339,43 @@ lemma smult_conv_map_poly: "smult c p = map_poly (\x. c * x) p" by (intro poly_eqI) (simp_all add: coeff_map_poly) +lemma poly_cnj: "cnj (poly p z) = poly (map_poly cnj p) (cnj z)" + by (simp add: poly_altdef degree_map_poly coeff_map_poly) + +lemma poly_cnj_real: + assumes "\n. poly.coeff p n \ \" + shows "cnj (poly p z) = poly p (cnj z)" +proof - + from assms have "map_poly cnj p = p" + by (intro poly_eqI) (auto simp: coeff_map_poly Reals_cnj_iff) + with poly_cnj[of p z] show ?thesis by simp +qed + +lemma real_poly_cnj_root_iff: + assumes "\n. poly.coeff p n \ \" + shows "poly p (cnj z) = 0 \ poly p z = 0" +proof - + have "poly p (cnj z) = cnj (poly p z)" + by (simp add: poly_cnj_real assms) + also have "\ = 0 \ poly p z = 0" by simp + finally show ?thesis . +qed + +lemma sum_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]" + by (induction A rule: infinite_finite_induct) auto + +lemma diff_to_poly: "[:c:] - [:d:] = [:c - d:]" + by (simp add: poly_eq_iff mult_ac) + +lemma mult_to_poly: "[:c:] * [:d:] = [:c * d:]" + by (simp add: poly_eq_iff mult_ac) + +lemma prod_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]" + by (induction A rule: infinite_finite_induct) (auto simp: mult_to_poly mult_ac) + +lemma poly_map_poly_cnj [simp]: "poly (map_poly cnj p) x = cnj (poly p (cnj x))" + by (induction p) (auto simp: map_poly_pCons) + subsection \Conversions\ @@ -1327,6 +1442,21 @@ "lead_coeff (numeral n) = numeral n" by (simp add: numeral_poly) +lemma coeff_linear_poly_power: + fixes c :: "'a :: semiring_1" + assumes "i \ n" + shows "coeff ([:a, b:] ^ n) i = of_nat (n choose i) * b ^ i * a ^ (n - i)" +proof - + have "[:a, b:] = monom b 1 + [:a:]" + by (simp add: monom_altdef) + also have "coeff (\ ^ n) i = (\k\n. a^(n-k) * of_nat (n choose k) * (if k = i then b ^ k else 0))" + by (subst binomial_ring) (simp add: coeff_sum of_nat_poly monom_power poly_const_pow mult_ac) + also have "\ = (\k\{i}. a ^ (n - i) * b ^ i * of_nat (n choose k))" + using assms by (intro sum.mono_neutral_cong_right) (auto simp: mult_ac) + finally show *: ?thesis by (simp add: mult_ac) +qed + + subsection \Lemmas about divisibility\ @@ -1407,6 +1537,11 @@ for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum) +lemma degree_prod_sum_eq: + "(\x. x \ A \ f x \ 0) \ + degree (prod f A :: 'a :: idom poly) = (\x\A. degree (f x))" + by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq) + lemma dvd_imp_degree: \degree x \ degree y\ if \x dvd y\ \x \ 0\ \y \ 0\ for x y :: \'a::{comm_semiring_1,semiring_no_zero_divisors} poly\ @@ -1733,6 +1868,56 @@ for p :: "'a::{ring_char_0,comm_ring_1,ring_no_zero_divisors} poly" by (auto simp add: poly_eq_poly_eq_iff [symmetric]) +lemma card_poly_roots_bound: + fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" + assumes "p \ 0" + shows "card {x. poly p x = 0} \ degree p" +using assms +proof (induction "degree p" arbitrary: p rule: less_induct) + case (less p) + show ?case + proof (cases "\x. poly p x = 0") + case False + hence "{x. poly p x = 0} = {}" by blast + thus ?thesis by simp + next + case True + then obtain x where x: "poly p x = 0" by blast + hence "[:-x, 1:] dvd p" by (subst (asm) poly_eq_0_iff_dvd) + then obtain q where q: "p = [:-x, 1:] * q" by (auto simp: dvd_def) + with \p \ 0\ have [simp]: "q \ 0" by auto + have deg: "degree p = Suc (degree q)" + by (subst q, subst degree_mult_eq) auto + have "card {x. poly p x = 0} \ card (insert x {x. poly q x = 0})" + by (intro card_mono) (auto intro: poly_roots_finite simp: q) + also have "\ \ Suc (card {x. poly q x = 0})" + by (rule card_insert_le_m1) auto + also from deg have "card {x. poly q x = 0} \ degree q" + using \p \ 0\ and q by (intro less) auto + also have "Suc \ = degree p" by (simp add: deg) + finally show ?thesis by - simp_all + qed +qed + +lemma poly_eqI_degree: + fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly" + assumes "\x. x \ A \