moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
--- 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 \<open>Definition of basic zero, one, constant, X, and inverse X elements\<close>
+subsubsection \<open>Definition of basic Laurent series\<close>
instantiation fls :: (zero) zero
begin
@@ -2008,14 +2008,13 @@
subsubsection \<open>Inverses\<close>
-\<comment> \<open>See lemma fls_left_inverse\<close>
+
abbreviation fls_left_inverse ::
"'a::{comm_monoid_add,uminus,times} fls \<Rightarrow> 'a \<Rightarrow> 'a fls"
where
"fls_left_inverse f x \<equiv>
fls_shift (fls_subdegree f) (fps_to_fls (fps_left_inverse (fls_base_factor_to_fps f) x))"
-\<comment> \<open>See lemma fls_right_inverse\<close>
abbreviation fls_right_inverse ::
"'a::{comm_monoid_add,uminus,times} fls \<Rightarrow> 'a \<Rightarrow> '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"
- \<comment> \<open>These assumptions imply y equals f $$ fls_subdegree f, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply y equals \<open>f $$ fls_subdegree f\<close>, but no need to assume that.\<close>
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"
- \<comment> \<open>These assumptions imply y equals f $$ fls_subdegree f, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply y equals \<open>f $$ fls_subdegree f\<close>, but no need to assume that.\<close>
shows "fls_right_inverse (fls_right_inverse f x) y = f"
proof-
from assms(1) have
@@ -3645,7 +3644,7 @@
subsection \<open>Formal differentiation and integration\<close>
-subsubsection \<open>Derivative definition and basic properties\<close>
+subsubsection \<open>Derivative\<close>
definition "fls_deriv f = Abs_fls (\<lambda>n. of_int (n+1) * f$$(n+1))"
@@ -3802,7 +3801,7 @@
qed
-subsubsection \<open>Algebra rules of the derivative\<close>
+subsubsection \<open>Algebraic rules of the derivative\<close>
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 \<open>Integral definition and basic properties\<close>
-\<comment> \<open>To incorporate a constant of integration, just add an fps_const.\<close>
definition fls_integral :: "'a::{ring_1,inverse} fls \<Rightarrow> 'a fls"
where "fls_integral a = Abs_fls (\<lambda>n. if n=0 then 0 else inverse (of_int n) * a$$(n - 1))"
@@ -4371,7 +4369,7 @@
qed
-subsubsection \<open>Algebra rules of the integral\<close>
+subsubsection \<open>Algebraic rules of the integral\<close>
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 \<open>Notation bundle\<close>
+subsection \<open>Notation\<close>
no_notation fls_nth (infixl "$$" 75)
--- 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 \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)"
+lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $ n \<noteq> 0)"
by (simp add: expand_fps_eq)
lemma fps_nonzero_nth_minimal: "f \<noteq> 0 \<longleftrightarrow> (\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m < n. f $ m = 0))"
@@ -412,8 +412,7 @@
by (auto simp: fps_mult_nth_conv_inside_subdegrees)
-subsection \<open>Formal power series form a commutative ring with unity, if the range of sequences
- they represent is a commutative ring with unity\<close>
+subsection \<open>Ring structure\<close>
instance fps :: (semigroup_add) semigroup_add
proof
@@ -539,8 +538,6 @@
instance fps :: (semiring_1_cancel) semiring_1_cancel ..
-subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
-
lemma fps_square_nth: "(f^2) $ n = (\<Sum>k\<le>n. f $ k * f $ (n - k))"
by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost)
@@ -554,8 +551,6 @@
qed
-subsection \<open>Injection of the basic ring elements and multiplication by scalars\<close>
-
definition "fps_const c = Abs_fps (\<lambda>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 \<open>Formal power series form an integral domain\<close>
-
instance fps :: (ring) ring ..
instance fps :: (comm_ring) comm_ring ..
@@ -791,8 +784,6 @@
by (cases "f = 0"; induction n) simp_all
-subsection \<open>The efps_Xtractor series fps_X\<close>
-
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 \<open>Formal Power series form a metric space\<close>
+subsection \<open>Metrizability\<close>
instantiation fps :: ("{minus,zero}") dist
begin
@@ -1472,7 +1463,7 @@
qed
-subsection \<open>Inverses and division of formal power series\<close>
+subsection \<open>Division\<close>
declare sum.cong[fundef_cong]
@@ -1483,7 +1474,7 @@
| "fps_left_inverse_constructor f a (Suc n) =
- sum (\<lambda>i. fps_left_inverse_constructor f a i * f$(Suc n - i)) {0..n} * a"
-\<comment> \<open>This will construct a left inverse for f in case that x * f$0 = 1\<close>
+\<comment> \<open>This will construct a left inverse for f in case that \<^prop>\<open>x * f$0 = 1\<close>\<close>
abbreviation "fps_left_inverse \<equiv> (\<lambda>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 (\<lambda>i. f$i * fps_right_inverse_constructor f a (n - i)) {1..n}"
-\<comment> \<open>This will construct a right inverse for f in case that f$0 * y = 1\<close>
+\<comment> \<open>This will construct a right inverse for f in case that \<^prop>\<open>f$0 * y = 1\<close>\<close>
abbreviation "fps_right_inverse \<equiv> (\<lambda>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
-\<comment> \<open>
+text \<open>
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.
\<close>
lemma fps_left_inverse_eq_fps_right_inverse:
fixes f :: "'a::ring_1 fps"
assumes f0: "x * f$0 = 1" "f $ 0 * y = 1"
- \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply that $x$ equals $y$, but no need to assume that.\<close>
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"
- \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply $x$ equals $y$, but no need to assume that.\<close>
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"
- \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply $x$ equals $y$, but no need to assume that.\<close>
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"
- \<comment> \<open>These assumptions imply y equals f$0, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply $y$ equals \<open>f$0\<close>, but no need to assume that.\<close>
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"
- \<comment> \<open>These assumptions imply y equals f$0, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply $y$ equals \<open>f$0\<close>, but no need to assume that.\<close>
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 \<open>Formal power series form a Euclidean ring\<close>
+subsection \<open>Euclidean division\<close>
instantiation fps :: (field) euclidean_ring_cancel
begin
@@ -2994,7 +2985,7 @@
-subsection \<open>Formal Derivatives, and the MacLaurin theorem around 0\<close>
+subsection \<open>Formal Derivatives\<close>
definition "fps_deriv f = Abs_fps (\<lambda>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"
- \<comment> \<open>These assumptions imply x equals y, but no need to assume that.\<close>
+ \<comment> \<open>These assumptions imply $x$ equals $y$, but no need to assume that.\<close>
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 \<open>Composition of FPSs\<close>
+subsection \<open>Composition\<close>
definition fps_compose :: "'a::semiring_1 fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55)
where "a oo b = Abs_fps (\<lambda>n. sum (\<lambda>i. a$i * (b^i$n)) {0..n})"
@@ -3722,10 +3713,10 @@
subsubsection \<open>Rule 3\<close>
-text \<open>Rule 3 is trivial and is given by \<open>fps_times_def\<close>.\<close>
-
-
-subsubsection \<open>Rule 5 --- summation and "division" by (1 - fps_X)\<close>
+text \<open>Rule 3 is trivial and is given by \texttt{fps\_times\_def}.\<close>
+
+
+subsubsection \<open>Rule 5 --- summation and ``division'' by $1 - X$\<close>
lemma fps_divide_fps_X_minus1_sum_lemma:
"a = ((1::'a::ring_1 fps) - fps_X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})"
@@ -3759,8 +3750,10 @@
using fps_divide_fps_X_minus1_sum_ring1[of a] by simp
-subsubsection \<open>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\<close>
+subsubsection \<open>Rule 4 in its more general form\<close>
+
+text \<open>This generalizes Rule 3 for an arbitrary
+ finite product of FPS, also the relevant instance of powers of a FPS.\<close>
definition "natpermute n k = {l :: nat list. length l = k \<and> sum_list l = n}"
@@ -4619,7 +4612,7 @@
by (simp add: divide_inverse fps_divide_def)
-subsection \<open>Derivative of composition\<close>
+subsection \<open>Chain rule\<close>
lemma fps_compose_deriv:
fixes a :: "'a::idom fps"
@@ -4658,9 +4651,6 @@
then show ?thesis by (simp add: fps_eq_iff)
qed
-
-subsection \<open>Finite FPS (i.e. polynomials) and fps_X\<close>
-
lemma fps_poly_sum_fps_X:
assumes "\<forall>i > n. a$i = 0"
shows "a = sum (\<lambda>i. fps_const (a$i) * fps_X^i) {0..n}" (is "a = ?r")
@@ -5742,7 +5732,7 @@
qed
-subsubsection \<open>Formal trigonometric functions\<close>
+subsubsection \<open>Trigonometric functions\<close>
definition "fps_sin (c::'a::field_char_0) =
Abs_fps (\<lambda>n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))"
--- 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\<open>A formalization of the fraction field of any integral domain;
- generalization of theory Rat from int to any integral domain\<close>
+section\<open>The fraction field of any integral domain\<close>
theory Fraction_Field
imports Main
--- 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 \<open>Fundamental theorem of algebra\<close>
-lemma fundamental_theorem_of_algebra:
+theorem fundamental_theorem_of_algebra:
assumes nc: "\<not> constant (poly p)"
shows "\<exists>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) (\<Prod>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 "\<not>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))
+ (\<Prod>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) (\<Prod>z\<in>{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 "(\<Prod>z\<in>{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p)) =
+ (\<Prod>z\<in>{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) (\<Prod>x\<in>#proots p. [:-x, 1:]) = (p :: complex poly)"
+proof (cases "p = 0")
+ case False
+ hence "(\<Prod>x\<in>#proots p. [:-x, 1:]) = (\<Prod>x | poly p x = 0. [:-x, 1:] ^ order x p)"
+ by (subst image_prod_mset_multiplicity) simp_all
+ also have "smult (lead_coeff p) \<dots> = p"
+ by (rule complex_poly_decompose)
+ finally show ?thesis .
+qed auto
+
+lemma complex_poly_decompose':
+ obtains root where "smult (lead_coeff p) (\<Prod>i<degree p. [:-root i, 1:]) = (p :: complex poly)"
+proof -
+ obtain roots where roots: "mset roots = proots p"
+ using ex_mset by blast
+
+ have "p = smult (lead_coeff p) (\<Prod>x\<in>#proots p. [:-x, 1:])"
+ by (rule complex_poly_decompose_multiset [symmetric])
+ also have "(\<Prod>x\<in>#proots p. [:-x, 1:]) = (\<Prod>x\<leftarrow>roots. [:-x, 1:])"
+ by (subst prod_mset_prod_list [symmetric]) (simp add: roots)
+ also have "\<dots> = (\<Prod>i<length roots. [:-roots ! i, 1:])"
+ by (subst prod.list_conv_set_nth) (auto simp: atLeast0LessThan)
+ finally have eq: "p = smult (lead_coeff p) (\<Prod>i<length roots. [:-roots ! i, 1:])" .
+ also have [simp]: "degree p = length roots"
+ using roots by (subst eq) (auto simp: degree_prod_sum_eq)
+ finally show ?thesis by (intro that[of "\<lambda>i. roots ! i"]) auto
+qed
+
+lemma complex_poly_decompose_rsquarefree:
+ assumes "rsquarefree p"
+ shows "smult (lead_coeff p) (\<Prod>z|poly p z = 0. [:-z, 1:]) = (p :: complex poly)"
+proof (cases "p = 0")
+ case False
+ have "(\<Prod>z|poly p z = 0. [:-z, 1:]) = (\<Prod>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) \<dots> = p"
+ by (rule complex_poly_decompose)
+ finally show ?thesis .
+qed auto
+
+
text \<open>Arithmetic operations on multivariate polynomials.\<close>
lemma mpoly_base_conv:
--- 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: "\<forall>\<^sub>\<infinity> n. coeff p n = 0"
using coeff [of p] by simp
+lemma coeff_Abs_poly:
+ assumes "\<And>i. i > n \<Longrightarrow> f i = 0"
+ shows "coeff (Abs_poly f) = f"
+proof (rule Abs_poly_inverse, clarify)
+ have "eventually (\<lambda>i. i > n) cofinite"
+ by (auto simp: MOST_nat)
+ thus "eventually (\<lambda>i. f i = 0) cofinite"
+ by eventually_elim (use assms in auto)
+qed
+
subsection \<open>Degree of a polynomial\<close>
definition degree :: "'a::zero poly \<Rightarrow> nat"
where "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"
+lemma degree_cong:
+ assumes "\<And>i. coeff p i = 0 \<longleftrightarrow> coeff q i = 0"
+ shows "degree p = degree q"
+proof -
+ have "(\<lambda>n. \<forall>i>n. poly.coeff p i = 0) = (\<lambda>n. \<forall>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 (\<lambda>i. if i \<le> n then f i else 0)) = (\<lambda>i. if i \<le> n then f i else 0)"
+proof (rule Abs_poly_inverse, clarify)
+ have "eventually (\<lambda>i. i > n) cofinite"
+ by (auto simp: MOST_nat)
+ thus "eventually (\<lambda>i. (if i \<le> 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 \<longleftrightarrow> p = 0"
by (cases "p = 0") (simp_all add: leading_coeff_neq_0)
+lemma degree_lessI:
+ assumes "p \<noteq> 0 \<or> n > 0" "\<forall>k\<ge>n. coeff p k = 0"
+ shows "degree p < n"
+proof (cases "p = 0")
+ case False
+ show ?thesis
+ proof (rule ccontr)
+ assume *: "\<not>(degree p < n)"
+ define d where "d = degree p"
+ from \<open>p \<noteq> 0\<close> have "coeff p d \<noteq> 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 \<le> n" and "coeff p n = 0"
shows "p = 0 \<or> 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 (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
by (induct A rule: infinite_finite_induct) simp_all
+lemma poly_sum_list: "poly (\<Sum>p\<leftarrow>ps. p) y = (\<Sum>p\<leftarrow>ps. poly p y)"
+ by (induction ps) auto
+
+lemma poly_sum_mset: "poly (\<Sum>x\<in>#A. p x) y = (\<Sum>x\<in>#A. poly (p x) y)"
+ by (induction A) auto
+
lemma degree_sum_le: "finite S \<Longrightarrow> (\<And>p. p \<in> S \<Longrightarrow> degree (f p) \<le> n) \<Longrightarrow> degree (sum f S) \<le> 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 "\<And>x. x \<in> A \<Longrightarrow> 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 \<le> n"
shows "(\<Sum>i\<le>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) \<le> degree p + degree q"
proof (rule degree_le)
show "\<forall>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: "(\<Prod>x\<in>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) \<le> degree p * n"
by (induct n) (auto intro: order_trans degree_mult_le)
@@ -1103,6 +1169,18 @@
lemma poly_prod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
by (induct A rule: infinite_finite_induct) simp_all
+lemma poly_prod_list: "poly (\<Prod>p\<leftarrow>ps. p) y = (\<Prod>p\<leftarrow>ps. poly p y)"
+ by (induction ps) auto
+
+lemma poly_prod_mset: "poly (\<Prod>x\<in>#A. p x) y = (\<Prod>x\<in>#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 \<Longrightarrow> degree (prod f S) \<le> sum (degree \<circ> f) S"
proof (induct S rule: finite_induct)
case empty
@@ -1261,6 +1339,43 @@
lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>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 "\<And>n. poly.coeff p n \<in> \<real>"
+ 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 "\<And>n. poly.coeff p n \<in> \<real>"
+ shows "poly p (cnj z) = 0 \<longleftrightarrow> poly p z = 0"
+proof -
+ have "poly p (cnj z) = cnj (poly p z)"
+ by (simp add: poly_cnj_real assms)
+ also have "\<dots> = 0 \<longleftrightarrow> poly p z = 0" by simp
+ finally show ?thesis .
+qed
+
+lemma sum_to_poly: "(\<Sum>x\<in>A. [:f x:]) = [:\<Sum>x\<in>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: "(\<Prod>x\<in>A. [:f x:]) = [:\<Prod>x\<in>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 \<open>Conversions\<close>
@@ -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 \<le> 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 (\<dots> ^ n) i = (\<Sum>k\<le>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 "\<dots> = (\<Sum>k\<in>{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 \<open>Lemmas about divisibility\<close>
@@ -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:
+ "(\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0) \<Longrightarrow>
+ degree (prod f A :: 'a :: idom poly) = (\<Sum>x\<in>A. degree (f x))"
+ by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)
+
lemma dvd_imp_degree:
\<open>degree x \<le> degree y\<close> if \<open>x dvd y\<close> \<open>x \<noteq> 0\<close> \<open>y \<noteq> 0\<close>
for x y :: \<open>'a::{comm_semiring_1,semiring_no_zero_divisors} poly\<close>
@@ -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 \<noteq> 0"
+ shows "card {x. poly p x = 0} \<le> degree p"
+using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ case (less p)
+ show ?case
+ proof (cases "\<exists>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 \<open>p \<noteq> 0\<close> have [simp]: "q \<noteq> 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} \<le> card (insert x {x. poly q x = 0})"
+ by (intro card_mono) (auto intro: poly_roots_finite simp: q)
+ also have "\<dots> \<le> Suc (card {x. poly q x = 0})"
+ by (rule card_insert_le_m1) auto
+ also from deg have "card {x. poly q x = 0} \<le> degree q"
+ using \<open>p \<noteq> 0\<close> and q by (intro less) auto
+ also have "Suc \<dots> = 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 "\<And>x. x \<in> A \<Longrightarrow> poly p x = poly q x"
+ assumes "card A > degree p" "card A > degree q"
+ shows "p = q"
+proof (rule ccontr)
+ assume neq: "p \<noteq> q"
+ have "degree (p - q) \<le> max (degree p) (degree q)"
+ by (rule degree_diff_le_max)
+ also from assms have "\<dots> < card A" by linarith
+ also have "\<dots> \<le> card {x. poly (p - q) x = 0}"
+ using neq and assms by (intro card_mono poly_roots_finite) auto
+ finally have "degree (p - q) < card {x. poly (p - q) x = 0}" .
+ moreover have "degree (p - q) \<ge> card {x. poly (p - q) x = 0}"
+ using neq by (intro card_poly_roots_bound) auto
+ ultimately show False by linarith
+qed
+
+
subsubsection \<open>Order of polynomial roots\<close>
@@ -1927,6 +2112,134 @@
lemma monom_1_dvd_iff: "p \<noteq> 0 \<Longrightarrow> monom 1 n dvd p \<longleftrightarrow> n \<le> order 0 p"
using order_divides[of 0 n p] by (simp add: monom_altdef)
+lemma poly_root_order_induct [case_names 0 no_roots root]:
+ fixes p :: "'a :: idom poly"
+ assumes "P 0" "\<And>p. (\<And>x. poly p x \<noteq> 0) \<Longrightarrow> P p"
+ "\<And>p x n. n > 0 \<Longrightarrow> poly p x \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P ([:-x, 1:] ^ n * p)"
+ shows "P p"
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ case (less p)
+ consider "p = 0" | "p \<noteq> 0" "\<exists>x. poly p x = 0" | "\<And>x. poly p x \<noteq> 0" by blast
+ thus ?case
+ proof cases
+ case 3
+ with assms(2)[of p] show ?thesis by simp
+ next
+ case 2
+ then obtain x where x: "poly p x = 0" by auto
+ have "[:-x, 1:] ^ order x p dvd p" by (intro order_1)
+ then obtain q where q: "p = [:-x, 1:] ^ order x p * q" by (auto simp: dvd_def)
+ with 2 have [simp]: "q \<noteq> 0" by auto
+ have order_pos: "order x p > 0"
+ using \<open>p \<noteq> 0\<close> and x by (auto simp: order_root)
+ have "order x p = order x p + order x q"
+ by (subst q, subst order_mult) (auto simp: order_power_n_n)
+ hence [simp]: "order x q = 0" by simp
+ have deg: "degree p = order x p + degree q"
+ by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq)
+ with order_pos have "degree q < degree p" by simp
+ hence "P q" by (rule less)
+ with order_pos have "P ([:-x, 1:] ^ order x p * q)"
+ by (intro assms(3)) (auto simp: order_root)
+ with q show ?thesis by simp
+ qed (simp_all add: assms(1))
+qed
+
+
+context
+ includes multiset.lifting
+begin
+
+lift_definition proots :: "('a :: idom) poly \<Rightarrow> 'a multiset" is
+ "\<lambda>(p :: 'a poly) (x :: 'a). if p = 0 then 0 else order x p"
+proof -
+ fix p :: "'a poly"
+ show "finite {x. 0 < (if p = 0 then 0 else order x p)}"
+ by (cases "p = 0")
+ (auto simp: order_gt_0_iff intro: finite_subset[OF _ poly_roots_finite[of p]])
+qed
+
+lemma proots_0 [simp]: "proots (0 :: 'a :: idom poly) = {#}"
+ by transfer' auto
+
+lemma proots_1 [simp]: "proots (1 :: 'a :: idom poly) = {#}"
+ by transfer' auto
+
+lemma proots_const [simp]: "proots [: x :] = 0"
+ by transfer' (auto split: if_splits simp: fun_eq_iff order_eq_0_iff)
+
+lemma proots_numeral [simp]: "proots (numeral n) = 0"
+ by (simp add: numeral_poly)
+
+lemma count_proots [simp]:
+ "p \<noteq> 0 \<Longrightarrow> count (proots p) a = order a p"
+ by transfer' auto
+
+lemma set_count_proots [simp]:
+ "p \<noteq> 0 \<Longrightarrow> set_mset (proots p) = {x. poly p x = 0}"
+ by (auto simp: set_mset_def order_gt_0_iff)
+
+lemma proots_uminus [simp]: "proots (-p) = proots p"
+ by (cases "p = 0"; rule multiset_eqI) auto
+
+lemma proots_smult [simp]: "c \<noteq> 0 \<Longrightarrow> proots (smult c p) = proots p"
+ by (cases "p = 0"; rule multiset_eqI) (auto simp: order_smult)
+
+lemma proots_mult:
+ assumes "p \<noteq> 0" "q \<noteq> 0"
+ shows "proots (p * q) = proots p + proots q"
+ using assms by (intro multiset_eqI) (auto simp: order_mult)
+
+lemma proots_prod:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+ shows "proots (\<Prod>x\<in>A. f x) = (\<Sum>x\<in>A. proots (f x))"
+ using assms by (induction A rule: infinite_finite_induct) (auto simp: proots_mult)
+
+lemma proots_prod_mset:
+ assumes "0 \<notin># A"
+ shows "proots (\<Prod>p\<in>#A. p) = (\<Sum>p\<in>#A. proots p)"
+ using assms by (induction A) (auto simp: proots_mult)
+
+lemma proots_prod_list:
+ assumes "0 \<notin> set ps"
+ shows "proots (\<Prod>p\<leftarrow>ps. p) = (\<Sum>p\<leftarrow>ps. proots p)"
+ using assms by (induction ps) (auto simp: proots_mult prod_list_zero_iff)
+
+lemma proots_power: "proots (p ^ n) = repeat_mset n (proots p)"
+proof (cases "p = 0")
+ case False
+ thus ?thesis
+ by (induction n) (auto simp: proots_mult)
+qed (auto simp: power_0_left)
+
+lemma proots_linear_factor [simp]: "proots [:x, 1:] = {#-x#}"
+proof -
+ have "order (-x) [:x, 1:] > 0"
+ by (subst order_gt_0_iff) auto
+ moreover have "order (-x) [:x, 1:] \<le> degree [:x, 1:]"
+ by (rule order_degree) auto
+ moreover have "order y [:x, 1:] = 0" if "y \<noteq> -x" for y
+ by (rule order_0I) (use that in \<open>auto simp: add_eq_0_iff\<close>)
+ ultimately show ?thesis
+ by (intro multiset_eqI) auto
+qed
+
+lemma size_proots_le: "size (proots p) \<le> degree p"
+proof (induction p rule: poly_root_order_induct)
+ case (no_roots p)
+ hence "proots p = 0"
+ by (simp add: multiset_eqI order_root)
+ thus ?case by simp
+next
+ case (root p x n)
+ have [simp]: "p \<noteq> 0"
+ using root.hyps by auto
+ from root.IH show ?case
+ by (auto simp: proots_mult proots_power degree_mult_eq degree_power_eq)
+qed auto
+
+end
+
subsection \<open>Additional induction rules on polynomials\<close>
@@ -2015,6 +2328,13 @@
lemma pcompose_pCons: "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def)
+lemma pcompose_altdef: "pcompose p q = poly (map_poly (\<lambda>x. [:x:]) p) q"
+ by (induction p) (simp_all add: map_poly_pCons pcompose_pCons)
+
+lemma coeff_pcompose_0 [simp]:
+ "coeff (pcompose p q) 0 = poly p (coeff q 0)"
+ by (induction p) (simp_all add: coeff_mult_0 pcompose_pCons)
+
lemma pcompose_1: "pcompose 1 p = 1"
for p :: "'a::comm_semiring_1 poly"
by (auto simp: one_pCons pcompose_pCons)
@@ -2155,6 +2475,16 @@
by simp
qed
+lemma pcompose_eq_0_iff:
+ fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
+ assumes "degree q > 0"
+ shows "pcompose p q = 0 \<longleftrightarrow> p = 0"
+ using pcompose_eq_0[OF _ assms] by auto
+
+lemma coeff_pcompose_linear:
+ "coeff (pcompose p [:0, a :: 'a :: comm_semiring_1:]) i = a ^ i * coeff p i"
+ by (induction p arbitrary: i) (auto simp: pcompose_pCons coeff_pCons mult_ac split: nat.splits)
+
lemma lead_coeff_comp:
fixes p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
assumes "degree q > 0"
@@ -2439,6 +2769,9 @@
lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)
+lemma reflect_poly_eq_0_iff [simp]: "reflect_poly p = 0 \<longleftrightarrow> p = 0"
+ using coeff_0_reflect_poly_0_iff by fastforce
+
(* TODO: does this work with zero divisors as well? Probably not. *)
lemma reflect_poly_mult: "reflect_poly (p * q) = reflect_poly p * reflect_poly q"
for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
@@ -2672,6 +3005,15 @@
by (simp add: pderiv_mult smult_add_left algebra_simps)
qed auto
+lemma pderiv_power:
+ "pderiv (p ^ n) = smult (of_nat n) (p ^ (n - 1) * pderiv p)"
+ by (cases n) (simp_all add: pderiv_power_Suc del: power_Suc)
+
+lemma pderiv_monom:
+ "pderiv (monom c n) = monom (of_nat n * c) (n - 1)"
+ by (cases n)
+ (simp_all add: monom_altdef pderiv_power_Suc pderiv_smult pderiv_pCons mult_ac del: power_Suc)
+
lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q"
by (induction p rule: pCons_induct)
(auto simp: pcompose_pCons pderiv_add pderiv_mult pderiv_pCons pcompose_add algebra_simps)
@@ -2695,6 +3037,51 @@
by (auto simp add: ac_simps intro!: sum.cong)
qed auto
+lemma coeff_higher_pderiv:
+ "coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * coeff f (n + m)"
+ by (induction m arbitrary: n) (simp_all add: coeff_pderiv pochhammer_rec algebra_simps)
+
+lemma higher_pderiv_0 [simp]: "(pderiv ^^ n) 0 = 0"
+ by (induction n) simp_all
+
+lemma higher_pderiv_add: "(pderiv ^^ n) (p + q) = (pderiv ^^ n) p + (pderiv ^^ n) q"
+ by (induction n arbitrary: p q) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_add)
+
+lemma higher_pderiv_smult: "(pderiv ^^ n) (smult c p) = smult c ((pderiv ^^ n) p)"
+ by (induction n arbitrary: p) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_smult)
+
+lemma higher_pderiv_monom:
+ "m \<le> n + 1 \<Longrightarrow> (pderiv ^^ m) (monom c n) = monom (pochhammer (int n - int m + 1) m * c) (n - m)"
+proof (induction m arbitrary: c n)
+ case (Suc m)
+ thus ?case
+ by (cases n)
+ (simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH)
+qed simp_all
+
+lemma higher_pderiv_monom_eq_zero:
+ "m > n + 1 \<Longrightarrow> (pderiv ^^ m) (monom c n) = 0"
+proof (induction m arbitrary: c n)
+ case (Suc m)
+ thus ?case
+ by (cases n)
+ (simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH)
+qed simp_all
+
+lemma higher_pderiv_sum: "(pderiv ^^ n) (sum f A) = (\<Sum>x\<in>A. (pderiv ^^ n) (f x))"
+ by (induction A rule: infinite_finite_induct) (simp_all add: higher_pderiv_add)
+
+lemma higher_pderiv_sum_mset: "(pderiv ^^ n) (sum_mset A) = (\<Sum>p\<in>#A. (pderiv ^^ n) p)"
+ by (induction A) (simp_all add: higher_pderiv_add)
+
+lemma higher_pderiv_sum_list: "(pderiv ^^ n) (sum_list ps) = (\<Sum>p\<leftarrow>ps. (pderiv ^^ n) p)"
+ by (induction ps) (simp_all add: higher_pderiv_add)
+
+lemma degree_higher_pderiv: "Polynomial.degree ((pderiv ^^ n) p) = Polynomial.degree p - n"
+ for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly"
+ by (induction n) (auto simp: degree_pderiv)
+
+
lemma DERIV_pow2: "DERIV (\<lambda>x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
by (rule DERIV_cong, rule DERIV_pow) simp
declare DERIV_pow2 [simp] DERIV_pow [simp]
@@ -2919,6 +3306,15 @@
qed
qed (simp add: rsquarefree_def)
+lemma rsquarefree_root_order:
+ assumes "rsquarefree p" "poly p z = 0" "p \<noteq> 0"
+ shows "order z p = 1"
+proof -
+ from assms have "order z p \<in> {0, 1}" by (auto simp: rsquarefree_def)
+ moreover from assms have "order z p > 0" by (auto simp: order_root)
+ ultimately show "order z p = 1" by auto
+qed
+
lemma poly_squarefree_decomp:
fixes p :: "'a::field_char_0 poly"
assumes "pderiv p \<noteq> 0"
@@ -2944,6 +3340,37 @@
subsection \<open>Algebraic numbers\<close>
+
+lemma intpolyE:
+ assumes "\<And>i. poly.coeff p i \<in> \<int>"
+ obtains q where "p = map_poly of_int q"
+proof -
+ have "\<forall>i\<in>{..Polynomial.degree p}. \<exists>x. poly.coeff p i = of_int x"
+ using assms by (auto simp: Ints_def)
+ from bchoice[OF this] obtain f
+ where f: "\<And>i. i \<le> Polynomial.degree p \<Longrightarrow> poly.coeff p i = of_int (f i)" by blast
+ define q where "q = Poly (map f [0..<Suc (Polynomial.degree p)])"
+ have "p = map_poly of_int q"
+ by (intro poly_eqI)
+ (auto simp: coeff_map_poly q_def nth_default_def f coeff_eq_0 simp del: upt_Suc)
+ with that show ?thesis by blast
+qed
+
+lemma ratpolyE:
+ assumes "\<And>i. poly.coeff p i \<in> \<rat>"
+ obtains q where "p = map_poly of_rat q"
+proof -
+ have "\<forall>i\<in>{..Polynomial.degree p}. \<exists>x. poly.coeff p i = of_rat x"
+ using assms by (auto simp: Rats_def)
+ from bchoice[OF this] obtain f
+ where f: "\<And>i. i \<le> Polynomial.degree p \<Longrightarrow> poly.coeff p i = of_rat (f i)" by blast
+ define q where "q = Poly (map f [0..<Suc (Polynomial.degree p)])"
+ have "p = map_poly of_rat q"
+ by (intro poly_eqI)
+ (auto simp: coeff_map_poly q_def nth_default_def f coeff_eq_0 simp del: upt_Suc)
+ with that show ?thesis by blast
+qed
+
text \<open>
Algebraic numbers can be defined in two equivalent ways: all real numbers that are
roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry
@@ -3024,6 +3451,200 @@
ultimately show "\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0" by auto
qed
+lemma algebraicI': "(\<And>i. coeff p i \<in> \<rat>) \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> poly p x = 0 \<Longrightarrow> algebraic x"
+ unfolding algebraic_altdef by blast
+
+lemma algebraicE':
+ assumes "algebraic (x :: 'a :: field_char_0)"
+ obtains p where "p \<noteq> 0" "poly (map_poly of_int p) x = 0"
+proof -
+ from assms obtain q where q: "\<And>i. coeff q i \<in> \<int>" "q \<noteq> 0" "poly q x = 0"
+ by (erule algebraicE)
+ moreover from this(1) obtain q' where q': "q = map_poly of_int q'" by (erule intpolyE)
+ moreover have "q' \<noteq> 0"
+ using q' q by auto
+ ultimately show ?thesis by (intro that[of q']) simp_all
+qed
+
+lemma algebraicE'_nonzero:
+ assumes "algebraic (x :: 'a :: field_char_0)" "x \<noteq> 0"
+ obtains p where "p \<noteq> 0" "coeff p 0 \<noteq> 0" "poly (map_poly of_int p) x = 0"
+proof -
+ from assms(1) obtain p where p: "p \<noteq> 0" "poly (map_poly of_int p) x = 0"
+ by (erule algebraicE')
+ define n :: nat where "n = order 0 p"
+ have "monom 1 n dvd p" by (simp add: monom_1_dvd_iff p n_def)
+ then obtain q where q: "p = monom 1 n * q" by (erule dvdE)
+ have [simp]: "map_poly of_int (monom 1 n * q) = monom (1 :: 'a) n * map_poly of_int q"
+ by (induction n) (auto simp: monom_0 monom_Suc map_poly_pCons)
+ from p have "q \<noteq> 0" "poly (map_poly of_int q) x = 0" by (auto simp: q poly_monom assms(2))
+ moreover from this have "order 0 p = n + order 0 q" by (simp add: q order_mult)
+ hence "order 0 q = 0" by (simp add: n_def)
+ with \<open>q \<noteq> 0\<close> have "poly q 0 \<noteq> 0" by (simp add: order_root)
+ ultimately show ?thesis using that[of q] by (auto simp: poly_0_coeff_0)
+qed
+
+lemma rat_imp_algebraic: "x \<in> \<rat> \<Longrightarrow> algebraic x"
+proof (rule algebraicI')
+ show "poly [:-x, 1:] x = 0"
+ by simp
+qed (auto simp: coeff_pCons split: nat.splits)
+
+lemma algebraic_0 [simp, intro]: "algebraic 0"
+ and algebraic_1 [simp, intro]: "algebraic 1"
+ and algebraic_numeral [simp, intro]: "algebraic (numeral n)"
+ and algebraic_of_nat [simp, intro]: "algebraic (of_nat k)"
+ and algebraic_of_int [simp, intro]: "algebraic (of_int m)"
+ by (simp_all add: rat_imp_algebraic)
+
+lemma algebraic_ii [simp, intro]: "algebraic \<i>"
+proof (rule algebraicI)
+ show "poly [:1, 0, 1:] \<i> = 0"
+ by simp
+qed (auto simp: coeff_pCons split: nat.splits)
+
+lemma algebraic_minus [intro]:
+ assumes "algebraic x"
+ shows "algebraic (-x)"
+proof -
+ from assms obtain p where p: "\<forall>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0"
+ by (elim algebraicE) auto
+ define s where "s = (if even (degree p) then 1 else -1 :: 'a)"
+
+ define q where "q = Polynomial.smult s (pcompose p [:0, -1:])"
+ have "poly q (-x) = 0"
+ using p by (auto simp: q_def poly_pcompose s_def)
+ moreover have "q \<noteq> 0"
+ using p by (auto simp: q_def s_def pcompose_eq_0_iff)
+ find_theorems "pcompose _ _ = 0"
+ moreover have "coeff q i \<in> \<int>" for i
+ proof -
+ have "coeff (pcompose p [:0, -1:]) i \<in> \<int>"
+ using p by (intro coeff_pcompose_semiring_closed) (auto simp: coeff_pCons split: nat.splits)
+ thus ?thesis by (simp add: q_def s_def)
+ qed
+ ultimately show ?thesis
+ by (auto simp: algebraic_def)
+qed
+
+lemma algebraic_minus_iff [simp]:
+ "algebraic (-x) \<longleftrightarrow> algebraic (x :: 'a :: field_char_0)"
+ using algebraic_minus[of x] algebraic_minus[of "-x"] by auto
+
+lemma algebraic_inverse [intro]:
+ assumes "algebraic x"
+ shows "algebraic (inverse x)"
+proof (cases "x = 0")
+ case [simp]: False
+ from assms obtain p where p: "\<forall>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0"
+ by (elim algebraicE) auto
+ show ?thesis
+ proof (rule algebraicI)
+ show "poly (reflect_poly p) (inverse x) = 0"
+ using assms p by (simp add: poly_reflect_poly_nz)
+ qed (use assms p in \<open>auto simp: coeff_reflect_poly\<close>)
+qed auto
+
+lemma algebraic_root:
+ assumes "algebraic y"
+ and "poly p x = y" and "\<forall>i. coeff p i \<in> \<int>" and "lead_coeff p = 1" and "degree p > 0"
+ shows "algebraic x"
+proof -
+ from assms obtain q where q: "poly q y = 0" "\<forall>i. coeff q i \<in> \<int>" "q \<noteq> 0"
+ by (elim algebraicE) auto
+ show ?thesis
+ proof (rule algebraicI)
+ from assms q show "pcompose q p \<noteq> 0"
+ by (auto simp: pcompose_eq_0_iff)
+ from assms q show "coeff (pcompose q p) i \<in> \<int>" for i
+ by (intro allI coeff_pcompose_semiring_closed) auto
+ show "poly (pcompose q p) x = 0"
+ using assms q by (simp add: poly_pcompose)
+ qed
+qed
+
+lemma algebraic_abs_real [simp]:
+ "algebraic \<bar>x :: real\<bar> \<longleftrightarrow> algebraic x"
+ by (auto simp: abs_if)
+
+lemma algebraic_nth_root_real [intro]:
+ assumes "algebraic x"
+ shows "algebraic (root n x)"
+proof (cases "n = 0")
+ case False
+ show ?thesis
+ proof (rule algebraic_root)
+ show "poly (monom 1 n) (root n x) = (if even n then \<bar>x\<bar> else x)"
+ using sgn_power_root[of n x] False
+ by (auto simp add: poly_monom sgn_if split: if_splits)
+ qed (use False assms in \<open>auto simp: degree_monom_eq\<close>)
+qed auto
+
+lemma algebraic_sqrt [intro]: "algebraic x \<Longrightarrow> algebraic (sqrt x)"
+ by (auto simp: sqrt_def)
+
+lemma algebraic_csqrt [intro]: "algebraic x \<Longrightarrow> algebraic (csqrt x)"
+ by (rule algebraic_root[where p = "monom 1 2"])
+ (auto simp: poly_monom degree_monom_eq)
+
+lemma algebraic_cnj [intro]:
+ assumes "algebraic x"
+ shows "algebraic (cnj x)"
+proof -
+ from assms obtain p where p: "poly p x = 0" "\<forall>i. coeff p i \<in> \<int>" "p \<noteq> 0"
+ by (elim algebraicE) auto
+ show ?thesis
+ proof (rule algebraicI)
+ show "poly (map_poly cnj p) (cnj x) = 0"
+ using p by simp
+ show "map_poly cnj p \<noteq> 0"
+ using p by (auto simp: map_poly_eq_0_iff)
+ show "coeff (map_poly cnj p) i \<in> \<int>" for i
+ using p by (auto simp: coeff_map_poly)
+ qed
+qed
+
+lemma algebraic_cnj_iff [simp]: "algebraic (cnj x) \<longleftrightarrow> algebraic x"
+ using algebraic_cnj[of x] algebraic_cnj[of "cnj x"] by auto
+
+lemma algebraic_of_real [intro]:
+ assumes "algebraic x"
+ shows "algebraic (of_real x)"
+proof -
+ from assms obtain p where p: "p \<noteq> 0" "poly (map_poly of_int p) x = 0" by (erule algebraicE')
+ have 1: "map_poly of_int p \<noteq> (0 :: 'a poly)"
+ using p by (metis coeff_0 coeff_map_poly leading_coeff_0_iff of_int_eq_0_iff)
+
+ have "poly (map_poly of_int p) (of_real x :: 'a) = of_real (poly (map_poly of_int p) x)"
+ by (simp add: poly_altdef degree_map_poly coeff_map_poly)
+ also note p(2)
+ finally have 2: "poly (map_poly of_int p) (of_real x :: 'a) = 0"
+ by simp
+
+ from 1 2 show "algebraic (of_real x :: 'a)"
+ by (intro algebraicI[of "map_poly of_int p"]) (auto simp: coeff_map_poly)
+qed
+
+lemma algebraic_of_real_iff [simp]:
+ "algebraic (of_real x :: 'a :: {real_algebra_1,field_char_0}) \<longleftrightarrow> algebraic x"
+proof
+ assume "algebraic (of_real x :: 'a)"
+ then obtain p where p: "p \<noteq> 0" "poly (map_poly of_int p) (of_real x :: 'a) = 0"
+ by (erule algebraicE')
+ have 1: "(map_poly of_int p :: real poly) \<noteq> 0"
+ using p by (metis coeff_0 coeff_map_poly leading_coeff_0_iff of_int_0 of_int_eq_iff)
+
+ note p(2)
+ also have "poly (map_poly of_int p) (of_real x :: 'a) = of_real (poly (map_poly of_int p) x)"
+ by (simp add: poly_altdef degree_map_poly coeff_map_poly)
+ also have "\<dots> = 0 \<longleftrightarrow> poly (map_poly of_int p) x = 0"
+ using of_real_eq_0_iff by blast
+ finally have 2: "poly (map_poly real_of_int p) x = 0" .
+
+ from 1 and 2 show "algebraic x"
+ by (intro algebraicI[of "map_poly of_int p"]) (auto simp: coeff_map_poly)
+qed auto
+
subsection \<open>Algebraic integers\<close>
@@ -3227,9 +3848,6 @@
by (rule algebraic_int_root[where p = "monom 1 2"])
(auto simp: poly_monom degree_monom_eq)
-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)
-
lemma algebraic_int_cnj [intro]:
assumes "algebraic_int x"
shows "algebraic_int (cnj x)"
@@ -3564,6 +4182,39 @@
for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
+lemma root_imp_reducible_poly:
+ fixes x :: "'a :: field"
+ assumes "poly p x = 0" and "degree p > 1"
+ shows "\<not>irreducible p"
+proof -
+ from assms have "p \<noteq> 0"
+ by auto
+ define q where "q = [:-x, 1:]"
+ have "q dvd p"
+ using assms by (simp add: poly_eq_0_iff_dvd q_def)
+ then obtain r where p_eq: "p = q * r"
+ by (elim dvdE)
+ have [simp]: "q \<noteq> 0" "r \<noteq> 0"
+ using \<open>p \<noteq> 0\<close> by (auto simp: p_eq)
+ have "degree p = Suc (degree r)"
+ unfolding p_eq by (subst degree_mult_eq) (auto simp: q_def)
+ with assms(2) have "degree r > 0"
+ by auto
+ hence "\<not>r dvd 1"
+ by (auto simp: is_unit_poly_iff)
+ moreover have "\<not>q dvd 1"
+ by (auto simp: is_unit_poly_iff q_def)
+ ultimately show ?thesis using p_eq
+ by (auto simp: irreducible_def)
+qed
+
+lemma reducible_polyI:
+ fixes p :: "'a :: field poly"
+ assumes "p = q * r" "degree q > 0" "degree r > 0"
+ shows "\<not>irreducible p"
+ using assms unfolding irreducible_def
+ by (metis (no_types, opaque_lifting) is_unitE is_unit_iff_degree not_gr0)
+
subsubsection \<open>Pseudo-Division\<close>
@@ -5221,6 +5872,345 @@
by (simp_all add: content_mult mult_ac)
qed (auto simp: content_mult)
+
+subsection \<open>A typeclass for algebraically closed fields\<close>
+
+(* TODO: Move! *)
+
+text \<open>
+ Since the required sort constraints are not available inside the class, we have to resort
+ to a somewhat awkward way of writing the definition of algebraically closed fields:
+\<close>
+class alg_closed_field = field +
+ assumes alg_closed: "n > 0 \<Longrightarrow> f n \<noteq> 0 \<Longrightarrow> \<exists>x. (\<Sum>k\<le>n. f k * x ^ k) = 0"
+
+text \<open>
+ We can then however easily show the equivalence to the proper definition:
+\<close>
+lemma alg_closed_imp_poly_has_root:
+ assumes "degree (p :: 'a :: alg_closed_field poly) > 0"
+ shows "\<exists>x. poly p x = 0"
+proof -
+ have "\<exists>x. (\<Sum>k\<le>degree p. coeff p k * x ^ k) = 0"
+ using assms by (intro alg_closed) auto
+ thus ?thesis
+ by (simp add: poly_altdef)
+qed
+
+lemma alg_closedI [Pure.intro]:
+ assumes "\<And>p :: 'a poly. degree p > 0 \<Longrightarrow> lead_coeff p = 1 \<Longrightarrow> \<exists>x. poly p x = 0"
+ shows "OFCLASS('a :: field, alg_closed_field_class)"
+proof
+ fix n :: nat and f :: "nat \<Rightarrow> 'a"
+ assume n: "n > 0" "f n \<noteq> 0"
+ define p where "p = Abs_poly (\<lambda>k. if k \<le> n then f k else 0)"
+ have coeff_p: "coeff p k = (if k \<le> n then f k else 0)" for k
+ proof -
+ have "eventually (\<lambda>k. k > n) cofinite"
+ by (auto simp: MOST_nat)
+ hence "eventually (\<lambda>k. (if k \<le> n then f k else 0) = 0) cofinite"
+ by eventually_elim auto
+ thus ?thesis
+ unfolding p_def by (subst Abs_poly_inverse) auto
+ qed
+
+ from n have "degree p \<ge> n"
+ by (intro le_degree) (auto simp: coeff_p)
+ moreover have "degree p \<le> n"
+ by (intro degree_le) (auto simp: coeff_p)
+ ultimately have deg_p: "degree p = n"
+ by linarith
+ from deg_p and n have [simp]: "p \<noteq> 0"
+ by auto
+
+ define p' where "p' = smult (inverse (lead_coeff p)) p"
+ have deg_p': "degree p' = degree p"
+ by (auto simp: p'_def)
+ have lead_coeff_p' [simp]: "lead_coeff p' = 1"
+ by (auto simp: p'_def)
+
+ from deg_p and deg_p' and n have "degree p' > 0"
+ by simp
+ from assms[OF this] obtain x where "poly p' x = 0"
+ by auto
+ hence "poly p x = 0"
+ by (simp add: p'_def)
+ also have "poly p x = (\<Sum>k\<le>n. f k * x ^ k)"
+ unfolding poly_altdef by (intro sum.cong) (auto simp: deg_p coeff_p)
+ finally show "\<exists>x. (\<Sum>k\<le>n. f k * x ^ k) = 0" ..
+qed
+
+
+text \<open>
+ We can now prove by induction that every polynomial of degree \<open>n\<close> splits into a product of
+ \<open>n\<close> linear factors:
+\<close>
+lemma alg_closed_imp_factorization:
+ fixes p :: "'a :: alg_closed_field poly"
+ assumes "p \<noteq> 0"
+ shows "\<exists>A. size A = degree p \<and> p = smult (lead_coeff p) (\<Prod>x\<in>#A. [:-x, 1:])"
+ using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+ case (less p)
+ show ?case
+ proof (cases "degree p = 0")
+ case True
+ thus ?thesis
+ by (intro exI[of _ "{#}"]) (auto elim!: degree_eq_zeroE)
+ next
+ case False
+ then obtain x where x: "poly p x = 0"
+ using alg_closed_imp_poly_has_root by blast
+ hence "[:-x, 1:] dvd p"
+ using poly_eq_0_iff_dvd by blast
+ then obtain q where p_eq: "p = [:-x, 1:] * q"
+ by (elim dvdE)
+ have "q \<noteq> 0"
+ using less.prems p_eq by auto
+ moreover from this have deg: "degree p = Suc (degree q)"
+ unfolding p_eq by (subst degree_mult_eq) auto
+ ultimately obtain A where A: "size A = degree q" "q = smult (lead_coeff q) (\<Prod>x\<in>#A. [:-x, 1:])"
+ using less.hyps[of q] by auto
+ have "smult (lead_coeff p) (\<Prod>y\<in>#add_mset x A. [:- y, 1:]) =
+ [:- x, 1:] * smult (lead_coeff q) (\<Prod>y\<in>#A. [:- y, 1:])"
+ unfolding p_eq lead_coeff_mult by simp
+ also note A(2) [symmetric]
+ also note p_eq [symmetric]
+ finally show ?thesis using A(1)
+ by (intro exI[of _ "add_mset x A"]) (auto simp: deg)
+ qed
+qed
+
+text \<open>
+ As an alternative characterisation of algebraic closure, one can also say that any
+ polynomial of degree at least 2 splits into non-constant factors:
+\<close>
+lemma alg_closed_imp_reducible:
+ assumes "degree (p :: 'a :: alg_closed_field poly) > 1"
+ shows "\<not>irreducible p"
+proof -
+ have "degree p > 0"
+ using assms by auto
+ then obtain z where z: "poly p z = 0"
+ using alg_closed_imp_poly_has_root[of p] by blast
+ then have dvd: "[:-z, 1:] dvd p"
+ by (subst dvd_iff_poly_eq_0) auto
+ then obtain q where q: "p = [:-z, 1:] * q"
+ by (erule dvdE)
+ have [simp]: "q \<noteq> 0"
+ using assms q by auto
+
+ show ?thesis
+ proof (rule reducible_polyI)
+ show "p = [:-z, 1:] * q"
+ by fact
+ next
+ have "degree p = degree ([:-z, 1:] * q)"
+ by (simp only: q)
+ also have "\<dots> = degree q + 1"
+ by (subst degree_mult_eq) auto
+ finally show "degree q > 0"
+ using assms by linarith
+ qed auto
+qed
+
+text \<open>
+ When proving algebraic closure through reducibility, we can assume w.l.o.g. that the polynomial
+ is monic and has a non-zero constant coefficient:
+\<close>
+lemma alg_closedI_reducible:
+ assumes "\<And>p :: 'a poly. degree p > 1 \<Longrightarrow> lead_coeff p = 1 \<Longrightarrow> coeff p 0 \<noteq> 0 \<Longrightarrow>
+ \<not>irreducible p"
+ shows "OFCLASS('a :: field, alg_closed_field_class)"
+proof
+ fix p :: "'a poly" assume p: "degree p > 0" "lead_coeff p = 1"
+ show "\<exists>x. poly p x = 0"
+ proof (cases "coeff p 0 = 0")
+ case True
+ hence "poly p 0 = 0"
+ by (simp add: poly_0_coeff_0)
+ thus ?thesis by blast
+ next
+ case False
+ from p and this show ?thesis
+ proof (induction "degree p" arbitrary: p rule: less_induct)
+ case (less p)
+ show ?case
+ proof (cases "degree p = 1")
+ case True
+ then obtain a b where p: "p = [:a, b:]"
+ by (cases p) (auto split: if_splits elim!: degree_eq_zeroE)
+ from True have [simp]: "b \<noteq> 0"
+ by (auto simp: p)
+ have "poly p (-a/b) = 0"
+ by (auto simp: p)
+ thus ?thesis by blast
+ next
+ case False
+ hence "degree p > 1"
+ using less.prems by auto
+ from assms[OF \<open>degree p > 1\<close> \<open>lead_coeff p = 1\<close> \<open>coeff p 0 \<noteq> 0\<close>]
+ have "\<not>irreducible p" by auto
+ then obtain r s where rs: "degree r > 0" "degree s > 0" "p = r * s"
+ using less.prems unfolding irreducible_def
+ by (metis is_unit_iff_degree mult_not_zero zero_less_iff_neq_zero)
+ hence "coeff r 0 \<noteq> 0"
+ using \<open>coeff p 0 \<noteq> 0\<close> by (auto simp: coeff_mult_0)
+
+ define r' where "r' = smult (inverse (lead_coeff r)) r"
+ have [simp]: "degree r' = degree r"
+ by (simp add: r'_def)
+ have lc: "lead_coeff r' = 1"
+ using rs by (auto simp: r'_def)
+ have nz: "coeff r' 0 \<noteq> 0"
+ using \<open>coeff r 0 \<noteq> 0\<close> by (auto simp: r'_def)
+
+ have "degree r < degree r + degree s"
+ using rs by linarith
+ also have "\<dots> = degree (r * s)"
+ using rs(3) less.prems by (subst degree_mult_eq) auto
+ also have "r * s = p"
+ using rs(3) by simp
+ finally have "\<exists>x. poly r' x = 0"
+ by (intro less) (use lc rs nz in auto)
+ thus ?thesis
+ using rs(3) by (auto simp: r'_def)
+ qed
+ qed
+ qed
+qed
+
+text \<open>
+ Using a clever Tschirnhausen transformation mentioned e.g. in the article by
+ Nowak~\<^cite>\<open>"nowak2000"\<close>, we can also assume w.l.o.g. that the coefficient $a_{n-1}$ is zero.
+\<close>
+lemma alg_closedI_reducible_coeff_deg_minus_one_eq_0:
+ assumes "\<And>p :: 'a poly. degree p > 1 \<Longrightarrow> lead_coeff p = 1 \<Longrightarrow> coeff p (degree p - 1) = 0 \<Longrightarrow>
+ coeff p 0 \<noteq> 0 \<Longrightarrow> \<not>irreducible p"
+ shows "OFCLASS('a :: field_char_0, alg_closed_field_class)"
+proof (rule alg_closedI_reducible, goal_cases)
+ case (1 p)
+ define n where [simp]: "n = degree p"
+ define a where "a = coeff p (n - 1)"
+ define r where "r = [: -a / of_nat n, 1 :]"
+ define s where "s = [: a / of_nat n, 1 :]"
+ define q where "q = pcompose p r"
+
+ have "n > 0"
+ using 1 by simp
+ have r_altdef: "r = monom 1 1 + [:-a / of_nat n:]"
+ by (simp add: r_def monom_altdef)
+ have deg_q: "degree q = n"
+ by (simp add: q_def r_def degree_pcompose)
+ have lc_q: "lead_coeff q = 1"
+ unfolding q_def using 1 by (subst lead_coeff_comp) (simp_all add: r_def)
+ have "q \<noteq> 0"
+ using 1 deg_q by auto
+
+ have "coeff q (n - 1) =
+ (\<Sum>i\<le>n. \<Sum>k\<le>i. coeff p i * (of_nat (i choose k) *
+ ((-a / of_nat n) ^ (i - k) * (if k = n - 1 then 1 else 0))))"
+ unfolding q_def pcompose_altdef poly_altdef r_altdef
+ by (simp_all add: degree_map_poly coeff_map_poly coeff_sum binomial_ring sum_distrib_left poly_const_pow
+ sum_distrib_right mult_ac monom_power coeff_monom_mult of_nat_poly cong: if_cong)
+ also have "\<dots> = (\<Sum>i\<le>n. \<Sum>k\<in>(if i \<ge> n - 1 then {n-1} else {}).
+ coeff p i * (of_nat (i choose k) * (-a / of_nat n) ^ (i - k)))"
+ by (rule sum.cong [OF refl], rule sum.mono_neutral_cong_right) (auto split: if_splits)
+ also have "\<dots> = (\<Sum>i\<in>{n-1,n}. \<Sum>k\<in>(if i \<ge> n - 1 then {n-1} else {}).
+ coeff p i * (of_nat (i choose k) * (-a / of_nat n) ^ (i - k)))"
+ by (rule sum.mono_neutral_right) auto
+ also have "\<dots> = a - of_nat (n choose (n - 1)) * a / of_nat n"
+ using 1 by (simp add: a_def)
+ also have "n choose (n - 1) = n"
+ using \<open>n > 0\<close> by (subst binomial_symmetric) auto
+ also have "a - of_nat n * a / of_nat n = 0"
+ using \<open>n > 0\<close> by simp
+ finally have "coeff q (n - 1) = 0" .
+
+ show ?case
+ proof (cases "coeff q 0 = 0")
+ case True
+ hence "poly p (- (a / of_nat (degree p))) = 0"
+ by (auto simp: q_def r_def)
+ thus ?thesis
+ by (rule root_imp_reducible_poly) (use 1 in auto)
+ next
+ case False
+ hence "\<not>irreducible q"
+ using assms[of q] and lc_q and 1 and \<open>coeff q (n - 1) = 0\<close>
+ by (auto simp: deg_q)
+ then obtain u v where uv: "degree u > 0" "degree v > 0" "q = u * v"
+ using \<open>q \<noteq> 0\<close> 1 deg_q unfolding irreducible_def
+ by (metis degree_mult_eq_0 is_unit_iff_degree n_def neq0_conv not_one_less_zero)
+
+ have "p = pcompose q s"
+ by (simp add: q_def r_def s_def pcompose_pCons flip: pcompose_assoc)
+ also have "q = u * v"
+ by fact
+ finally have "p = pcompose u s * pcompose v s"
+ by (simp add: pcompose_mult)
+ moreover have "degree (pcompose u s) > 0" "degree (pcompose v s) > 0"
+ using uv by (simp_all add: s_def degree_pcompose)
+ ultimately show "\<not>irreducible p"
+ using 1 by (intro reducible_polyI)
+ qed
+qed
+
+text \<open>
+ As a consequence of the full factorisation lemma proven above, we can also show that any
+ polynomial with at least two different roots splits into two non-constant coprime factors:
+\<close>
+lemma alg_closed_imp_poly_splits_coprime:
+ assumes "degree (p :: 'a :: {alg_closed_field} poly) > 1"
+ assumes "poly p x = 0" "poly p y = 0" "x \<noteq> y"
+ obtains r s where "degree r > 0" "degree s > 0" "coprime r s" "p = r * s"
+proof -
+ define n where "n = order x p"
+ have "n > 0"
+ using assms by (metis degree_0 gr0I n_def not_one_less_zero order_root)
+ have "[:-x, 1:] ^ n dvd p"
+ unfolding n_def by (simp add: order_1)
+ then obtain q where p_eq: "p = [:-x, 1:] ^ n * q"
+ by (elim dvdE)
+ from assms have [simp]: "q \<noteq> 0"
+ by (auto simp: p_eq)
+ have "order x p = n + Polynomial.order x q"
+ unfolding p_eq by (subst order_mult) (auto simp: order_power_n_n)
+ hence "Polynomial.order x q = 0"
+ by (simp add: n_def)
+ hence "poly q x \<noteq> 0"
+ by (simp add: order_root)
+
+ show ?thesis
+ proof (rule that)
+ show "coprime ([:-x, 1:] ^ n) q"
+ proof (rule coprimeI)
+ fix d
+ assume d: "d dvd [:-x, 1:] ^ n" "d dvd q"
+ have "degree d = 0"
+ proof (rule ccontr)
+ assume "\<not>(degree d = 0)"
+ then obtain z where z: "poly d z = 0"
+ using alg_closed_imp_poly_has_root by blast
+ moreover from this and d(1) have "poly ([:-x, 1:] ^ n) z = 0"
+ using dvd_trans poly_eq_0_iff_dvd by blast
+ ultimately have "poly d x = 0"
+ by auto
+ with d(2) have "poly q x = 0"
+ using dvd_trans poly_eq_0_iff_dvd by blast
+ with \<open>poly q x \<noteq> 0\<close> show False by contradiction
+ qed
+ thus "is_unit d" using d
+ by (metis \<open>q \<noteq> 0\<close> dvd_0_left is_unit_iff_degree)
+ qed
+ next
+ have "poly q y = 0"
+ using \<open>poly p y = 0\<close> \<open>x \<noteq> y\<close> by (auto simp: p_eq)
+ with \<open>q \<noteq> 0\<close> show "degree q > 0"
+ using order_degree order_gt_0_iff order_less_le_trans by blast
+ qed (use \<open>n > 0\<close> in \<open>simp_all add: p_eq degree_power_eq\<close>)
+qed
+
no_notation cCons (infixr "##" 65)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Computational_Algebra/document/root.bib Fri Mar 29 19:28:59 2024 +0100
@@ -0,0 +1,8 @@
+@article{nowak2000,
+ title={Some elementary proofs of {P}uiseux’s theorems},
+ author={Nowak, Krzysztof Jan},
+ journal={Univ. Iagel. Acta Math},
+ volume={38},
+ pages={279--282},
+ year={2000}
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Computational_Algebra/document/root.tex Fri Mar 29 19:28:59 2024 +0100
@@ -0,0 +1,38 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{latexsym}
+\usepackage{textcomp}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{pdfsetup}
+\usepackage{graphicx}
+
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+\title{Computational Algebra}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+ \includegraphics[width=\textwidth]{session_graph}
+\end{center}
+
+\newpage
+
+\renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}}
+
+\parindent 0pt\parskip 0.5ex
+\input{session}
+
+\pagestyle{headings}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
--- a/src/HOL/Groups_List.thy Sat Mar 30 01:12:48 2024 +0100
+++ b/src/HOL/Groups_List.thy Fri Mar 29 19:28:59 2024 +0100
@@ -47,6 +47,16 @@
"set.F g (set xs) = list.F (map g (remdups xs))"
by (simp add: distinct_set_conv_list [symmetric])
+lemma list_conv_set_nth:
+ "list.F xs = set.F (\<lambda>i. xs ! i) {0..<length xs}"
+proof -
+ have "xs = map (\<lambda>i. xs ! i) [0..<length xs]"
+ by (simp add: map_nth)
+ also have "list.F \<dots> = set.F (\<lambda>i. xs ! i) {0..<length xs}"
+ by (subst distinct_set_conv_list [symmetric]) auto
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Library/Multiset.thy Sat Mar 30 01:12:48 2024 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Mar 29 19:28:59 2024 +0100
@@ -1594,6 +1594,11 @@
lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
by (cases M) auto
+lemma set_mset_subset_singletonD:
+ assumes "set_mset A \<subseteq> {x}"
+ shows "A = replicate_mset (size A) x"
+ using assms by (induction A) auto
+
subsubsection \<open>Strong induction and subset induction for multisets\<close>
@@ -2308,6 +2313,15 @@
lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
by (induct n, simp_all)
+lemma size_repeat_mset [simp]: "size (repeat_mset n A) = n * size A"
+ by (induction n) auto
+
+lemma size_multiset_sum [simp]: "size (\<Sum>x\<in>A. f x :: 'a multiset) = (\<Sum>x\<in>A. size (f x))"
+ by (induction A rule: infinite_finite_induct) auto
+
+lemma size_multiset_sum_list [simp]: "size (\<Sum>X\<leftarrow>Xs. X :: 'a multiset) = (\<Sum>X\<leftarrow>Xs. size X)"
+ by (induction Xs) auto
+
lemma count_le_replicate_mset_subset_eq: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
by (auto simp add: mset_subset_eqI) (metis count_replicate_mset subseteq_mset_def)
@@ -2774,7 +2788,10 @@
by (induction M) auto
lemma Union_image_single_mset[simp]: "\<Sum>\<^sub># (image_mset (\<lambda>x. {#x#}) m) = m"
-by(induction m) auto
+ by(induction m) auto
+
+lemma size_multiset_sum_mset [simp]: "size (\<Sum>X\<in>#A. X :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
+ by (induction A) auto
context comm_monoid_mult
begin
@@ -2891,6 +2908,32 @@
then show ?thesis by (simp add: normalize_prod_mset)
qed
+lemma image_prod_mset_multiplicity:
+ "prod_mset (image_mset f M) = prod (\<lambda>x. f x ^ count M x) (set_mset M)"
+proof (induction M)
+ case (add x M)
+ show ?case
+ proof (cases "x \<in> set_mset M")
+ case True
+ have "(\<Prod>y\<in>set_mset (add_mset x M). f y ^ count (add_mset x M) y) =
+ (\<Prod>y\<in>set_mset M. (if y = x then f x else 1) * f y ^ count M y)"
+ using True add by (intro prod.cong) auto
+ also have "\<dots> = f x * (\<Prod>y\<in>set_mset M. f y ^ count M y)"
+ using True by (subst prod.distrib) auto
+ also note add.IH [symmetric]
+ finally show ?thesis using True by simp
+ next
+ case False
+ hence "(\<Prod>y\<in>set_mset (add_mset x M). f y ^ count (add_mset x M) y) =
+ f x * (\<Prod>y\<in>set_mset M. f y ^ count (add_mset x M) y)"
+ by (auto simp: not_in_iff)
+ also have "(\<Prod>y\<in>set_mset M. f y ^ count (add_mset x M) y) =
+ (\<Prod>y\<in>set_mset M. f y ^ count M y)"
+ using False by (intro prod.cong) auto
+ also note add.IH [symmetric]
+ finally show ?thesis by simp
+ qed
+qed auto
subsection \<open>Multiset as order-ignorant lists\<close>
--- a/src/HOL/Library/Real_Mod.thy Sat Mar 30 01:12:48 2024 +0100
+++ b/src/HOL/Library/Real_Mod.thy Fri Mar 29 19:28:59 2024 +0100
@@ -7,6 +7,8 @@
imports Complex_Main
begin
+(* MOVED TO HOL-Library ON 20.03.2024 *)
+
definition rmod :: "real \<Rightarrow> real \<Rightarrow> real" (infixl "rmod" 70) where
"x rmod y = x - \<bar>y\<bar> * of_int \<lfloor>x / \<bar>y\<bar>\<rfloor>"
--- a/src/HOL/ROOT Sat Mar 30 01:12:48 2024 +0100
+++ b/src/HOL/ROOT Fri Mar 29 19:28:59 2024 +0100
@@ -148,6 +148,9 @@
Computational_Algebra
(*conflicting type class instantiations and dependent applications*)
Field_as_Ring
+ document_files
+ "root.tex"
+ "root.bib"
session "HOL-Real_Asymp" in Real_Asymp = HOL +
sessions
--- a/src/HOL/Rat.thy Sat Mar 30 01:12:48 2024 +0100
+++ b/src/HOL/Rat.thy Fri Mar 29 19:28:59 2024 +0100
@@ -877,6 +877,12 @@
for a :: "'a::field_char_0"
by (metis Rats_cases Rats_of_rat of_rat_power)
+lemma Rats_sum [intro]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<rat>) \<Longrightarrow> sum f A \<in> \<rat>"
+ by (induction A rule: infinite_finite_induct) auto
+
+lemma Rats_prod [intro]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<rat>) \<Longrightarrow> prod f A \<in> \<rat>"
+ by (induction A rule: infinite_finite_induct) auto
+
lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
by (rule Rats_cases) auto