diff --git a/thys/Factor_Algebraic_Polynomial/Multivariate_Resultant.thy b/thys/Factor_Algebraic_Polynomial/Multivariate_Resultant.thy --- a/thys/Factor_Algebraic_Polynomial/Multivariate_Resultant.thy +++ b/thys/Factor_Algebraic_Polynomial/Multivariate_Resultant.thy @@ -1,139 +1,130 @@ subsection \Resultants of Multivariate Polynomials\ text \We utilize the conversion of multivariate polynomials into univariate polynomials for the definition of the resultant of multivariate polynomials via the resultant for univariate polynomials. In this way, we can use the algorithm to efficiently compute resultants for the multivariate case.\ theory Multivariate_Resultant imports Poly_Connection Algebraic_Numbers.Resultant Subresultants.Subresultant MPoly_Divide_Code MPoly_Container begin hide_const (open) MPoly_Type.degree MPoly_Type.coeff Symmetric_Polynomials.lead_coeff lemma det_sylvester_matrix_higher_degree: "det (sylvester_mat_sub (degree f + n) (degree g) f g) = det (sylvester_mat_sub (degree f) (degree g) f g) * (lead_coeff g * (-1)^(degree g))^n" proof (induct n) case (Suc n) let ?A = "sylvester_mat_sub (degree f + Suc n) (degree g) f g" let ?d = "degree f + Suc n + degree g" define h where "h i = ?A $$ (i,0) * cofactor ?A i 0" for i have mult_left_zero: "x = 0 \ x * y = 0" for x y :: 'a by auto have "det ?A = (\i = sum h ({degree g} \ ({.. = sum h {degree g} + sum h ({.. = lead_coeff g * cofactor ?A (degree g) 0" unfolding h_def by (rule arg_cong[of _ _ "\ x. x * _"], simp add: sylvester_mat_sub_def) also have "cofactor ?A (degree g) 0 = (-1)^(degree g) * det (sylvester_mat_sub (degree f + n) (degree g) f g)" unfolding cofactor_def proof (intro arg_cong2[of _ _ _ _ "\ x y. (-1)^x * det y"], force) show "mat_delete ?A (degree g) 0 = sylvester_mat_sub (degree f + n) (degree g) f g" unfolding sylvester_mat_sub_def by (intro eq_matI, auto simp: mat_delete_def coeff_eq_0) qed finally show ?case unfolding Suc by simp qed simp text \The conversion of multivariate into univariate polynomials permits us to define resultants in the multivariate setting. Since in our application one of the polynomials is already univariate, we use a non-symmetric definition where only one of the input polynomials is multivariate.\ definition resultant_mpoly_poly :: "nat \ 'a :: comm_ring_1 mpoly \ 'a poly \ 'a mpoly" where "resultant_mpoly_poly x p q = resultant (mpoly_to_mpoly_poly x p) (map_poly Const q)" text \This lemma tells us that there is only a minor difference between computing the multivariate resultant and then plugging in values, or first inserting values and then evaluate the univariate resultant.\ lemma insertion_resultant_mpoly_poly: "insertion \ (resultant_mpoly_poly x p q) = resultant (partial_insertion \ x p) q * (lead_coeff q * (-1)^ degree q)^(degree (mpoly_to_mpoly_poly x p) - degree (partial_insertion \ x p))" proof - let ?pa = "partial_insertion \ x" let ?a = "insertion \" let ?q = "map_poly Const q" let ?m = "mpoly_to_mpoly_poly x" interpret a: comm_ring_hom ?a by (rule comm_ring_hom_insertion) define m where "m = degree (?m p) - degree (?pa p)" from degree_partial_insertion_le_mpoly[of \ x p] have deg: "degree (?m p) = degree (?pa p) + m" unfolding m_def by simp define k where "k = degree (?pa p) + m" define l where "l = degree q" have "resultant (?pa p) q = det (sylvester_mat_sub (degree (?pa p)) (degree q) (?pa p) q)" unfolding resultant_def sylvester_mat_def by simp have "?a (resultant_mpoly_poly x p q) = ?a (det (sylvester_mat_sub (degree (?pa p) + m) (degree q) (?m p) ?q))" unfolding resultant_mpoly_poly_def resultant_def sylvester_mat_def degree_map_poly_Const deg .. also have "\ = det (a.mat_hom (sylvester_mat_sub (degree (?pa p) + m) (degree q) (?m p) ?q))" unfolding a.hom_det .. also have "a.mat_hom (sylvester_mat_sub (degree (?pa p) + m) (degree q) (?m p) ?q) = sylvester_mat_sub (degree (?pa p) + m) (degree q) (?pa p) q" unfolding k_def[symmetric] l_def[symmetric] by (intro eq_matI, auto simp: sylvester_mat_sub_def coeff_map_poly) also have "det \ = det (sylvester_mat_sub (degree (?pa p)) (degree q) (?pa p) q) * (lead_coeff q * (- 1) ^ degree q) ^ m" by (subst det_sylvester_matrix_higher_degree, simp) also have "det (sylvester_mat_sub (degree (?pa p)) (degree q) (?pa p) q) = resultant (?pa p) q" unfolding resultant_def sylvester_mat_def by simp finally show ?thesis unfolding m_def by auto qed lemma insertion_resultant_mpoly_poly_zero: fixes q :: "'a :: idom poly" assumes q: "q \ 0" shows "insertion \ (resultant_mpoly_poly x p q) = 0 \ resultant (partial_insertion \ x p) q = 0" unfolding insertion_resultant_mpoly_poly using q by auto lemma vars_resultant: "vars (resultant p q) \ \ (vars ` (range (coeff p) \ range (coeff q)))" unfolding resultant_def det_def sylvester_mat_def sylvester_mat_sub_def apply simp apply (rule order.trans[OF vars_setsum]) subgoal using finite_permutations by blast apply (rule UN_least) apply (rule order.trans[OF vars_mult]) apply simp apply (rule order.trans[OF vars_prod]) apply (rule UN_least) by auto text \By taking the resultant, one variable is deleted.\ lemma vars_resultant_mpoly_poly: "vars (resultant_mpoly_poly x p q) \ vars p - {x}" proof fix y assume "y \ vars (resultant_mpoly_poly x p q)" from set_mp[OF vars_resultant this[unfolded resultant_mpoly_poly_def]] obtain i where "y \ vars (coeff (mpoly_to_mpoly_poly x p) i) \ y \ vars (coeff (map_poly Const q) i)" by auto moreover have "vars (coeff (map_poly Const q) i) = {}" by (subst coeff_map_poly, auto) ultimately have "y \ vars (coeff (mpoly_to_mpoly_poly x p) i)" by auto thus "y \ More_MPoly_Type.vars p - {x}" using vars_coeff_mpoly_to_mpoly_poly by blast qed text \For resultants, we manually have to select the implementation that works on integral domains, because there is no factorial ring instance for @{typ "int mpoly"}.\ lemma resultant_mpoly_poly_code[code]: - "resultant_mpoly_poly x p q = resultant_impl_idom_divide (mpoly_to_mpoly_poly x p) (map_poly Const q)" - unfolding resultant_mpoly_poly_def by simp - -text \Make the idom-divide-resultant algorithm executable. The following - three lines have to be removed when switching to the development version of AFP, - where the code-setup for @{const resultant_impl_idom_divide} is already integrated.\ -declare resultant_impl_main_def[code] -declare subresultant_prs_def[code] -declare subresultant_prs_main.simps[code] - - + "resultant_mpoly_poly x p q = resultant_impl_basic (mpoly_to_mpoly_poly x p) (map_poly Const q)" + unfolding resultant_mpoly_poly_def div_exp_basic.resultant_impl by simp end \ No newline at end of file diff --git a/thys/Factor_Algebraic_Polynomial/Poly_Connection.thy b/thys/Factor_Algebraic_Polynomial/Poly_Connection.thy --- a/thys/Factor_Algebraic_Polynomial/Poly_Connection.thy +++ b/thys/Factor_Algebraic_Polynomial/Poly_Connection.thy @@ -1,695 +1,695 @@ section \Resultants and Multivariate Polynomials\ subsection \Connecting Univariate and Multivariate Polynomials\ text \We define a conversion of multivariate polynomials into univariate polynomials w.r.t.\ a fixed variable $x$ and multivariate polynomials as coefficients.\ theory Poly_Connection imports Polynomials.MPoly_Type_Univariate - Jordan_Normal_Form.Missing_Permutations + Jordan_Normal_Form.Missing_Misc Polynomial_Interpolation.Ring_Hom_Poly Hermite_Lindemann.More_Multivariate_Polynomial_HLW Polynomials.MPoly_Type_Class begin lemma mpoly_is_unitE: fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} mpoly" assumes "p dvd 1" obtains c where "p = Const c" "c dvd 1" proof - obtain r where r: "p * r = 1" using assms by auto from r have [simp]: "p \ 0" "r \ 0" by auto have "0 = lead_monom (1 :: 'a mpoly)" by simp also have "1 = p * r" using r by simp also have "lead_monom (p * r) = lead_monom p + lead_monom r" by (intro lead_monom_mult) auto finally have "lead_monom p = 0" by simp hence "vars p = {}" by (simp add: lead_monom_eq_0_iff) hence *: "p = Const (lead_coeff p)" by (auto simp: vars_empty_iff) have "1 = lead_coeff (1 :: 'a mpoly)" by simp also have "1 = p * r" using r by simp also have "lead_coeff (p * r) = lead_coeff p * lead_coeff r" by (intro lead_coeff_mult) auto finally have "lead_coeff p dvd 1" using dvdI by blast with * show ?thesis using that by blast qed lemma Const_eq_Const_iff [simp]: "Const c = Const c' \ c = c'" by (metis lead_coeff_Const) lemma is_unit_ConstI [intro]: "c dvd 1 \ Const c dvd 1" by (metis dvd_def mpoly_Const_1 mpoly_Const_mult) lemma is_unit_Const_iff: fixes c :: "'a :: {comm_semiring_1, semiring_no_zero_divisors}" shows "Const c dvd 1 \ c dvd 1" proof assume "Const c dvd 1" thus "c dvd 1" by (auto elim!: mpoly_is_unitE) qed auto lemma vars_emptyE: "vars p = {} \ (\c. p = Const c \ P) \ P" by (auto simp: vars_empty_iff) lemma degree_geI: assumes "MPoly_Type.coeff p m \ 0" shows "MPoly_Type.degree p i \ Poly_Mapping.lookup m i" proof - have "lookup m i \ Max (insert 0 ((\m. lookup m i) ` keys (mapping_of p)))" proof (rule Max.coboundedI) show "lookup m i \ insert 0 ((\m. lookup m i) ` keys (mapping_of p))" using assms by (auto simp: coeff_keys) qed auto thus ?thesis unfolding MPoly_Type.degree_def by auto qed lemma monom_of_degree_exists: assumes "p \ 0" obtains m where "MPoly_Type.coeff p m \ 0" "Poly_Mapping.lookup m i = MPoly_Type.degree p i" proof (cases "MPoly_Type.degree p i = 0") case False have "MPoly_Type.degree p i = Max (insert 0 ((\m. lookup m i) ` keys (mapping_of p)))" by (simp add: MPoly_Type.degree_def) also have "\ \ insert 0 ((\m. lookup m i) ` keys (mapping_of p))" by (rule Max_in) auto finally show ?thesis using False that by (auto simp: coeff_keys) next case [simp]: True from assms obtain m where m: "MPoly_Type.coeff p m \ 0" using coeff_all_0 by blast show ?thesis using degree_geI[of p m i] m by (intro that[of m]) auto qed lemma degree_leI: assumes "\m. Poly_Mapping.lookup m i > n \ MPoly_Type.coeff p m = 0" shows "MPoly_Type.degree p i \ n" proof (cases "p = 0") case False obtain m where m: "MPoly_Type.coeff p m \ 0" "Poly_Mapping.lookup m i = MPoly_Type.degree p i" using monom_of_degree_exists False by blast with assms show ?thesis by force qed auto lemma coeff_gt_degree_eq_0: assumes "Poly_Mapping.lookup m i > MPoly_Type.degree p i" shows "MPoly_Type.coeff p m = 0" using assms degree_geI leD by blast lemma vars_altdef: "vars p = (\m\{m. MPoly_Type.coeff p m \ 0}. keys m)" unfolding vars_def by (intro arg_cong[where f = "\"] image_cong refl) (simp flip: coeff_keys) lemma degree_pos_iff: "MPoly_Type.degree p x > 0 \ x \ vars p" proof assume "MPoly_Type.degree p x > 0" hence "p \ 0" by auto then obtain m where m: "lookup m x = MPoly_Type.degree p x" "MPoly_Type.coeff p m \ 0" using monom_of_degree_exists[of p x] by metis from m and \MPoly_Type.degree p x > 0\ have "x \ keys m" by (simp add: in_keys_iff) with m show "x \ vars p" by (auto simp: vars_altdef) next assume "x \ vars p" then obtain m where m: "x \ keys m" "MPoly_Type.coeff p m \ 0" by (auto simp: vars_altdef) have "0 < lookup m x" using m by (auto simp: in_keys_iff) also from m have "\ \ MPoly_Type.degree p x" by (intro degree_geI) auto finally show "MPoly_Type.degree p x > 0" . qed lemma degree_eq_0_iff: "MPoly_Type.degree p x = 0 \ x \ vars p" using degree_pos_iff[of p x] by auto lemma MPoly_Type_monom_zero[simp]: "MPoly_Type.monom m 0 = 0" by (simp add: More_MPoly_Type.coeff_monom coeff_all_0) lemma vars_monom_keys': "vars (MPoly_Type.monom m c) = (if c = 0 then {} else keys m)" by (cases "c = 0") (auto simp: vars_monom_keys) lemma Const_eq_0_iff [simp]: "Const c = 0 \ c = 0" by (metis lead_coeff_Const mpoly_Const_0) lemma monom_remove_key: "MPoly_Type.monom m (a :: 'a :: semiring_1) = MPoly_Type.monom (remove_key x m) a * MPoly_Type.monom (Poly_Mapping.single x (lookup m x)) 1" unfolding MPoly_Type.mult_monom by (rule arg_cong2[of _ _ _ _ MPoly_Type.monom], auto simp: remove_key_sum) lemma MPoly_Type_monom_0_iff[simp]: "MPoly_Type.monom m x = 0 \ x = 0" by (metis (full_types) MPoly_Type_monom_zero More_MPoly_Type.coeff_monom when_def) lemma vars_signof[simp]: "vars (signof x) = {}" - by (simp add: signof_def) + by (simp add: sign_def) lemma prod_mset_Const: "prod_mset (image_mset Const A) = Const (prod_mset A)" by (induction A) (auto simp: mpoly_Const_mult) lemma Const_eq_product_iff: fixes c :: "'a :: idom" assumes "c \ 0" shows "Const c = a * b \ (\a' b'. a = Const a' \ b = Const b' \ c = a' * b')" proof assume *: "Const c = a * b" have "lead_monom (a * b) = 0" by (auto simp flip: *) hence "lead_monom a = 0 \ lead_monom b = 0" by (subst (asm) lead_monom_mult) (use assms * in auto) hence "vars a = {}" "vars b = {}" by (auto simp: lead_monom_eq_0_iff) then obtain a' b' where "a = Const a'" "b = Const b'" by (auto simp: vars_empty_iff) with * show "(\a' b'. a = Const a' \ b = Const b' \ c = a' * b')" by (auto simp flip: mpoly_Const_mult) qed (auto simp: mpoly_Const_mult) lemma irreducible_Const_iff [simp]: "irreducible (Const (c :: 'a :: idom)) \ irreducible c" proof assume *: "irreducible (Const c)" show "irreducible c" proof (rule irreducibleI) fix a b assume "c = a * b" hence "Const c = Const a * Const b" by (simp add: mpoly_Const_mult) with * have "Const a dvd 1 \ Const b dvd 1" by blast thus "a dvd 1 \ b dvd 1" by (meson is_unit_Const_iff) qed (use * in \auto simp: irreducible_def\) next assume *: "irreducible c" have [simp]: "c \ 0" using * by auto show "irreducible (Const c)" proof (rule irreducibleI) fix a b assume "Const c = a * b" then obtain a' b' where [simp]: "a = Const a'" "b = Const b'" and "c = a' * b'" by (auto simp: Const_eq_product_iff) hence "a' dvd 1 \ b' dvd 1" using * by blast thus "a dvd 1 \ b dvd 1" by auto qed (use * in \auto simp: irreducible_def is_unit_Const_iff\) qed lemma Const_dvd_Const_iff [simp]: "Const a dvd Const b \ a dvd b" proof assume "a dvd b" then obtain c where "b = a * c" by auto hence "Const b = Const a * Const c" by (auto simp: mpoly_Const_mult) thus "Const a dvd Const b" by simp next assume "Const a dvd Const b" then obtain p where p: "Const b = Const a * p" by auto have "MPoly_Type.coeff (Const b) 0 = MPoly_Type.coeff (Const a * p) 0" using p by simp also have "\ = MPoly_Type.coeff (Const a) 0 * MPoly_Type.coeff p 0" using mpoly_coeff_times_0 by blast finally show "a dvd b" by (simp add: mpoly_coeff_Const) qed text \The lemmas above should be moved into the right theories. The part below is on the new connection between multivariate polynomials and univariate polynomials.\ text \The imported theories only allow a conversion from one-variable mpoly's to poly and vice-versa. However, we require a conversion from arbitrary mpoly's into poly's with mpolys as coefficients.\ (* converts a multi-variate polynomial into a univariate polynomial with multivariate coefficients *) definition mpoly_to_mpoly_poly :: "nat \ 'a :: comm_ring_1 mpoly \ 'a mpoly poly" where "mpoly_to_mpoly_poly x p = (\m . Polynomial.monom (MPoly_Type.monom (remove_key x m) (MPoly_Type.coeff p m)) (lookup m x))" lemma mpoly_to_mpoly_poly_add [simp]: "mpoly_to_mpoly_poly x (p + q) = mpoly_to_mpoly_poly x p + mpoly_to_mpoly_poly x q" unfolding mpoly_to_mpoly_poly_def More_MPoly_Type.coeff_add[symmetric] MPoly_Type.monom_add add_monom[symmetric] by (rule Sum_any.distrib) auto lemma mpoly_to_mpoly_poly_monom: "mpoly_to_mpoly_poly x (MPoly_Type.monom m a) = Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x)" proof - have "mpoly_to_mpoly_poly x (MPoly_Type.monom m a) = (\ m'. Polynomial.monom (MPoly_Type.monom (remove_key x m') a) (lookup m' x) when m' = m)" unfolding mpoly_to_mpoly_poly_def by (intro Sum_any.cong, auto simp: when_def More_MPoly_Type.coeff_monom) also have "\ = Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x)" unfolding Sum_any_when_equal .. finally show ?thesis . qed lemma remove_key_transfer [transfer_rule]: "rel_fun (=) (rel_fun (pcr_poly_mapping (=) (=)) (pcr_poly_mapping (=) (=))) (\k0 f k. f k when k \ k0) remove_key" unfolding pcr_poly_mapping_def cr_poly_mapping_def OO_def by (auto simp: rel_fun_def remove_key_lookup) lemma remove_key_0 [simp]: "remove_key x 0 = 0" by transfer auto lemma remove_key_single' [simp]: "x \ y \ remove_key x (Poly_Mapping.single y n) = Poly_Mapping.single y n" by transfer (auto simp: when_def fun_eq_iff) lemma poly_coeff_Sum_any: assumes "finite {x. f x \ 0}" shows "poly.coeff (Sum_any f) n = Sum_any (\x. poly.coeff (f x) n)" proof - have "Sum_any f = (\x | f x \ 0. f x)" by (rule Sum_any.expand_set) also have "poly.coeff \ n = (\x | f x \ 0. poly.coeff (f x) n)" by (simp add: Polynomial.coeff_sum) also have "\ = Sum_any (\x. poly.coeff (f x) n)" by (rule Sum_any.expand_superset [symmetric]) (use assms in auto) finally show ?thesis . qed lemma coeff_coeff_mpoly_to_mpoly_poly: "MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) n) m = (MPoly_Type.coeff p (m + Poly_Mapping.single x n) when lookup m x = 0)" proof - have "MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) n) m = MPoly_Type.coeff (\a. MPoly_Type.monom (remove_key x a) (MPoly_Type.coeff p a) when lookup a x = n) m" unfolding mpoly_to_mpoly_poly_def by (subst poly_coeff_Sum_any) (auto simp: when_def) also have "\ = (\xa. MPoly_Type.coeff (MPoly_Type.monom (remove_key x xa) (MPoly_Type.coeff p xa)) m when lookup xa x = n)" by (subst coeff_Sum_any, force) (auto simp: when_def intro!: Sum_any.cong) also have "\ = (\a. MPoly_Type.coeff p a when lookup a x = n \ m = remove_key x a)" by (intro Sum_any.cong) (simp add: More_MPoly_Type.coeff_monom when_def) also have "(\a. lookup a x = n \ m = remove_key x a) = (\a. lookup m x = 0 \ a = m + Poly_Mapping.single x n)" by (rule ext, transfer) (auto simp: fun_eq_iff when_def) also have "(\a. MPoly_Type.coeff p a when \ a) = (\a. MPoly_Type.coeff p a when lookup m x = 0 when a = m + Poly_Mapping.single x n)" by (intro Sum_any.cong) (auto simp: when_def) also have "\ = (MPoly_Type.coeff p (m + Poly_Mapping.single x n) when lookup m x = 0)" by (rule Sum_any_when_equal) finally show ?thesis . qed lemma mpoly_to_mpoly_poly_Const [simp]: "mpoly_to_mpoly_poly x (Const c) = [:Const c:]" proof - have "mpoly_to_mpoly_poly x (Const c) = (\m. Polynomial.monom (MPoly_Type.monom (remove_key x m) (MPoly_Type.coeff (Const c) m)) (lookup m x) when m = 0)" unfolding mpoly_to_mpoly_poly_def by (intro Sum_any.cong) (auto simp: when_def mpoly_coeff_Const) also have "\ = [:Const c:]" by (subst Sum_any_when_equal) (auto simp: mpoly_coeff_Const monom_altdef simp flip: Const_conv_monom) finally show ?thesis . qed lemma mpoly_to_mpoly_poly_Var: "mpoly_to_mpoly_poly x (Var y) = (if x = y then [:0, 1:] else [:Var y:])" proof - have "mpoly_to_mpoly_poly x (Var y) = (\a. Polynomial.monom (MPoly_Type.monom (remove_key x a) 1) (lookup a x) when a = Poly_Mapping.single y 1)" unfolding mpoly_to_mpoly_poly_def by (intro Sum_any.cong) (auto simp: when_def coeff_Var) also have "\ = (if x = y then [:0, 1:] else [:Var y:])" by (auto simp: Polynomial.monom_altdef lookup_single Var_altdef) finally show ?thesis . qed lemma mpoly_to_mpoly_poly_Var_this [simp]: "mpoly_to_mpoly_poly x (Var x) = [:0, 1:]" "x \ y \ mpoly_to_mpoly_poly x (Var y) = [:Var y:]" by (simp_all add: mpoly_to_mpoly_poly_Var) lemma mpoly_to_mpoly_poly_uminus [simp]: "mpoly_to_mpoly_poly x (-p) = -mpoly_to_mpoly_poly x p" unfolding mpoly_to_mpoly_poly_def by (auto simp: monom_uminus Sum_any_uminus simp flip: minus_monom) lemma mpoly_to_mpoly_poly_diff [simp]: "mpoly_to_mpoly_poly x (p - q) = mpoly_to_mpoly_poly x p - mpoly_to_mpoly_poly x q" by (subst diff_conv_add_uminus, subst mpoly_to_mpoly_poly_add) auto lemma mpoly_to_mpoly_poly_0 [simp]: "mpoly_to_mpoly_poly x 0 = 0" unfolding mpoly_Const_0 [symmetric] mpoly_to_mpoly_poly_Const by simp lemma mpoly_to_mpoly_poly_1 [simp]: "mpoly_to_mpoly_poly x 1 = 1" unfolding mpoly_Const_1 [symmetric] mpoly_to_mpoly_poly_Const by simp lemma mpoly_to_mpoly_poly_of_nat [simp]: "mpoly_to_mpoly_poly x (of_nat n) = of_nat n" unfolding of_nat_mpoly_eq mpoly_to_mpoly_poly_Const of_nat_poly .. lemma mpoly_to_mpoly_poly_of_int [simp]: "mpoly_to_mpoly_poly x (of_int n) = of_int n" unfolding of_nat_mpoly_eq mpoly_to_mpoly_poly_Const of_nat_poly by (cases n) auto lemma mpoly_to_mpoly_poly_numeral [simp]: "mpoly_to_mpoly_poly x (numeral n) = numeral n" using mpoly_to_mpoly_poly_of_nat[of x "numeral n"] by (simp del: mpoly_to_mpoly_poly_of_nat) lemma coeff_monom_mult': "MPoly_Type.coeff (MPoly_Type.monom m a * q) m' = (a * MPoly_Type.coeff q (m' - m) when lookup m' \ lookup m)" proof (cases "lookup m' \ lookup m") case True have "a * MPoly_Type.coeff q (m' - m) = MPoly_Type.coeff (MPoly_Type.monom m a * q) (m + (m' - m))" by (rule More_MPoly_Type.coeff_monom_mult [symmetric]) also have "m + (m' - m) = m'" using True by transfer (auto simp: le_fun_def) finally show ?thesis using True by (simp add: when_def) next case False have "MPoly_Type.coeff (MPoly_Type.monom m a * q) m' = (\m1. a * (\m2. MPoly_Type.coeff q m2 when m' = m1 + m2) when m1 = m)" unfolding coeff_mpoly_times prod_fun_def by (intro Sum_any.cong) (auto simp: More_MPoly_Type.coeff_monom when_def) also have "\ = a * (\m2. MPoly_Type.coeff q m2 when m' = m + m2)" by (subst Sum_any_when_equal) auto also have "(\m2. m' = m + m2) = (\m2. False)" by (rule ext) (use False in \transfer, auto simp: le_fun_def\) finally show ?thesis using False by simp qed lemma mpoly_to_mpoly_poly_mult_monom: "mpoly_to_mpoly_poly x (MPoly_Type.monom m a * q) = Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x) * mpoly_to_mpoly_poly x q" (is "?lhs = ?rhs") proof (rule poly_eqI, rule mpoly_eqI) fix n :: nat and mon :: "nat \\<^sub>0 nat" have "MPoly_Type.coeff (poly.coeff ?lhs n) mon = (a * MPoly_Type.coeff q (mon + Poly_Mapping.single x n - m) when lookup m \ lookup (mon + Poly_Mapping.single x n) \ lookup mon x = 0)" by (simp add: coeff_coeff_mpoly_to_mpoly_poly coeff_monom_mult' when_def) have "MPoly_Type.coeff (poly.coeff ?rhs n) mon = (a * MPoly_Type.coeff q (mon - remove_key x m + Poly_Mapping.single x (n - lookup m x)) when lookup (remove_key x m) \ lookup mon \ lookup m x \ n \ lookup mon x = 0)" by (simp add: coeff_coeff_mpoly_to_mpoly_poly coeff_monom_mult' lookup_minus_fun remove_key_lookup Missing_Polynomial.coeff_monom_mult when_def) also have "lookup (remove_key x m) \ lookup mon \ lookup m x \ n \ lookup mon x = 0 \ lookup m \ lookup (mon + Poly_Mapping.single x n) \ lookup mon x = 0" (is "_ = ?P") by transfer (auto simp: when_def le_fun_def) also have "mon - remove_key x m + Poly_Mapping.single x (n - lookup m x) = mon + Poly_Mapping.single x n - m" if ?P using that by transfer (auto simp: fun_eq_iff when_def) hence "(a * MPoly_Type.coeff q (mon - remove_key x m + Poly_Mapping.single x (n - lookup m x)) when ?P) = (a * MPoly_Type.coeff q \ when ?P)" by (intro when_cong) auto also have "\ = MPoly_Type.coeff (poly.coeff ?lhs n) mon" by (simp add: coeff_coeff_mpoly_to_mpoly_poly coeff_monom_mult' when_def) finally show "MPoly_Type.coeff (poly.coeff ?lhs n) mon = MPoly_Type.coeff (poly.coeff ?rhs n) mon" .. qed lemma mpoly_to_mpoly_poly_mult [simp]: "mpoly_to_mpoly_poly x (p * q) = mpoly_to_mpoly_poly x p * mpoly_to_mpoly_poly x q" by (induction p arbitrary: q rule: mpoly_induct) (simp_all add: mpoly_to_mpoly_poly_monom mpoly_to_mpoly_poly_mult_monom ring_distribs) lemma coeff_mpoly_to_mpoly_poly: "Polynomial.coeff (mpoly_to_mpoly_poly x p) n = Sum_any (\m. MPoly_Type.monom (remove_key x m) (MPoly_Type.coeff p m) when Poly_Mapping.lookup m x = n)" unfolding mpoly_to_mpoly_poly_def by (subst poly_coeff_Sum_any) (auto simp: when_def) lemma mpoly_coeff_to_mpoly_poly_coeff: "MPoly_Type.coeff p m = MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) (lookup m x)) (remove_key x m)" proof - have "MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) (lookup m x)) (remove_key x m) = (\xa. MPoly_Type.coeff (MPoly_Type.monom (remove_key x xa) (MPoly_Type.coeff p xa) when lookup xa x = lookup m x) (remove_key x m))" by (subst coeff_mpoly_to_mpoly_poly, subst coeff_Sum_any) auto also have "\ = (\xa. MPoly_Type.coeff (MPoly_Type.monom (remove_key x xa) (MPoly_Type.coeff p xa)) (remove_key x m) when lookup xa x = lookup m x)" by (intro Sum_any.cong) (auto simp: when_def) also have "\ = (\xa. MPoly_Type.coeff p xa when remove_key x m = remove_key x xa \ lookup xa x = lookup m x)" by (intro Sum_any.cong) (auto simp: More_MPoly_Type.coeff_monom when_def) also have "(\xa. remove_key x m = remove_key x xa \ lookup xa x = lookup m x) = (\xa. xa = m)" using remove_key_sum by metis also have "(\xa. MPoly_Type.coeff p xa when xa = m) = MPoly_Type.coeff p m" by simp finally show ?thesis .. qed lemma degree_mpoly_to_mpoly_poly [simp]: "Polynomial.degree (mpoly_to_mpoly_poly x p) = MPoly_Type.degree p x" proof (rule antisym) show "Polynomial.degree (mpoly_to_mpoly_poly x p) \ MPoly_Type.degree p x" proof (intro Polynomial.degree_le allI impI) fix i assume i: "i > MPoly_Type.degree p x" have "poly.coeff (mpoly_to_mpoly_poly x p) i = (\m. 0 when lookup m x = i)" unfolding coeff_mpoly_to_mpoly_poly using i by (intro Sum_any.cong when_cong refl) (auto simp: coeff_gt_degree_eq_0) also have "\ = 0" by simp finally show "poly.coeff (mpoly_to_mpoly_poly x p) i = 0" . qed next show "Polynomial.degree (mpoly_to_mpoly_poly x p) \ MPoly_Type.degree p x" proof (cases "p = 0") case False then obtain m where m: "MPoly_Type.coeff p m \ 0" "lookup m x = MPoly_Type.degree p x" using monom_of_degree_exists by blast show "Polynomial.degree (mpoly_to_mpoly_poly x p) \ MPoly_Type.degree p x" proof (rule Polynomial.le_degree) have "0 \ MPoly_Type.coeff p m" using m by auto also have "MPoly_Type.coeff p m = MPoly_Type.coeff (poly.coeff (mpoly_to_mpoly_poly x p) (lookup m x)) (remove_key x m)" by (rule mpoly_coeff_to_mpoly_poly_coeff) finally show "poly.coeff (mpoly_to_mpoly_poly x p) (MPoly_Type.degree p x) \ 0" using m by auto qed qed auto qed text \The upcoming lemma is similar to @{thm reduce_nested_mpoly_extract_var}.\ lemma poly_mpoly_to_mpoly_poly: "poly (mpoly_to_mpoly_poly x p) (Var x) = p" proof (induct p rule: mpoly_induct) case (monom m a) show ?case unfolding mpoly_to_mpoly_poly_monom poly_monom by (transfer, simp add: Var\<^sub>0_power mult_single remove_key_sum) next case (sum p1 p2 m a) then show ?case by (simp add: mpoly_to_mpoly_poly_add) qed lemma mpoly_to_mpoly_poly_eq_iff [simp]: "mpoly_to_mpoly_poly x p = mpoly_to_mpoly_poly x q \ p = q" proof assume "mpoly_to_mpoly_poly x p = mpoly_to_mpoly_poly x q" hence "poly (mpoly_to_mpoly_poly x p) (Var x) = poly (mpoly_to_mpoly_poly x q) (Var x)" by simp thus "p = q" by (auto simp: poly_mpoly_to_mpoly_poly) qed auto text \Evaluation, i.e., insertion of concrete values is identical\ lemma insertion_mpoly_to_mpoly_poly: assumes "\ y. y \ x \ \ y = \ y" shows "poly (map_poly (insertion \) (mpoly_to_mpoly_poly x p)) (\ x) = insertion \ p" proof (induct p rule: mpoly_induct) case (monom m a) let ?rkm = "remove_key x m" have to_alpha: "insertion \ (MPoly_Type.monom ?rkm a) = insertion \ (MPoly_Type.monom ?rkm a)" by (rule insertion_irrelevant_vars, rule assms, insert vars_monom_subset[of ?rkm a], auto simp: remove_key_keys[symmetric]) have main: "insertion \ (MPoly_Type.monom ?rkm a) * \ x ^ lookup m x = insertion \ (MPoly_Type.monom m a)" unfolding monom_remove_key[of m a x] insertion_mult by (metis insertion_single mult.left_neutral) show ?case using main to_alpha by (simp add: mpoly_to_mpoly_poly_monom map_poly_monom poly_monom) next case (sum p1 p2 m a) then show ?case by (simp add: mpoly_to_mpoly_poly_add insertion_add map_poly_add) qed lemma mpoly_to_mpoly_poly_dvd_iff [simp]: "mpoly_to_mpoly_poly x p dvd mpoly_to_mpoly_poly x q \ p dvd q" proof assume "mpoly_to_mpoly_poly x p dvd mpoly_to_mpoly_poly x q" hence "poly (mpoly_to_mpoly_poly x p) (Var x) dvd poly (mpoly_to_mpoly_poly x q) (Var x)" by (intro poly_hom.hom_dvd) thus "p dvd q" by (simp add: poly_mpoly_to_mpoly_poly) qed auto lemma vars_coeff_mpoly_to_mpoly_poly: "vars (poly.coeff (mpoly_to_mpoly_poly x p) i) \ vars p - {x}" unfolding mpoly_to_mpoly_poly_def Sum_any.expand_set Polynomial.coeff_sum More_MPoly_Type.coeff_monom apply (rule order.trans[OF vars_setsum], force) apply (rule UN_least, simp) apply (intro impI order.trans[OF vars_monom_subset]) by (simp add: remove_key_keys[symmetric] Diff_mono SUP_upper2 coeff_keys vars_def) locale transfer_mpoly_to_mpoly_poly = fixes x :: nat begin definition R :: "'a :: comm_ring_1 mpoly poly \ 'a mpoly \ bool" where "R p p' \ p = mpoly_to_mpoly_poly x p'" context includes lifting_syntax begin lemma transfer_0 [transfer_rule]: "R 0 0" and transfer_1 [transfer_rule]: "R 1 1" and transfer_Const [transfer_rule]: "R [:Const c:] (Const c)" and transfer_uminus [transfer_rule]: "(R ===> R) uminus uminus" and transfer_of_nat [transfer_rule]: "((=) ===> R) of_nat of_nat" and transfer_of_int [transfer_rule]: "((=) ===> R) of_nat of_nat" and transfer_numeral [transfer_rule]: "((=) ===> R) of_nat of_nat" and transfer_add [transfer_rule]: "(R ===> R ===> R) (+) (+)" and transfer_diff [transfer_rule]: "(R ===> R ===> R) (+) (+)" and transfer_mult [transfer_rule]: "(R ===> R ===> R) (*) (*)" and transfer_dvd [transfer_rule]: "(R ===> R ===> (=)) (dvd) (dvd)" and transfer_monom [transfer_rule]: "((=) ===> (=) ===> R) (\m a. Polynomial.monom (MPoly_Type.monom (remove_key x m) a) (lookup m x)) MPoly_Type.monom" and transfer_coeff [transfer_rule]: "(R ===> (=) ===> (=)) (\p m. MPoly_Type.coeff (poly.coeff p (lookup m x)) (remove_key x m)) MPoly_Type.coeff" and transfer_degree [transfer_rule]: "(R ===> (=)) Polynomial.degree (\p. MPoly_Type.degree p x)" unfolding R_def by (auto simp: rel_fun_def mpoly_to_mpoly_poly_monom simp flip: mpoly_coeff_to_mpoly_poly_coeff) lemma transfer_vars [transfer_rule]: assumes [transfer_rule]: "R p p'" shows "(\i. vars (poly.coeff p i)) \ (if Polynomial.degree p = 0 then {} else {x}) = vars p'" (is "?A \ ?B = _") proof (intro equalityI) have "vars p' = vars (poly p (Var x))" using assms by (simp add: R_def poly_mpoly_to_mpoly_poly) also have "poly p (Var x) = (\i\Polynomial.degree p. poly.coeff p i * Var x ^ i)" unfolding poly_altdef .. also have "vars \ \ (\i. vars (poly.coeff p i) \ (if Polynomial.degree p = 0 then {} else {x}))" proof (intro order.trans[OF vars_sum] UN_mono order.trans[OF vars_mult] Un_mono) fix i :: nat assume i: "i \ {..Polynomial.degree p}" show "vars (Var x ^ i) \ (if Polynomial.degree p = 0 then {} else {x})" proof (cases "Polynomial.degree p = 0") case False thus ?thesis by (intro order.trans[OF vars_power]) (auto simp: vars_Var) qed (use i in auto) qed auto finally show "vars p' \ ?A \ ?B" by blast next have "?A \ vars p'" using assms vars_coeff_mpoly_to_mpoly_poly by (auto simp: R_def) moreover have "?B \ vars p'" using assms by (auto simp: R_def degree_pos_iff) ultimately show "?A \ ?B \ vars p'" by blast qed lemma right_total [transfer_rule]: "right_total R" unfolding right_total_def proof safe fix p' :: "'a mpoly" show "\p. R p p'" by (rule exI[of _ "mpoly_to_mpoly_poly x p'"]) (auto simp: R_def) qed lemma bi_unique [transfer_rule]: "bi_unique R" unfolding bi_unique_def by (auto simp: R_def) end end lemma mpoly_degree_mult_eq: fixes p q :: "'a :: idom mpoly" assumes "p \ 0" "q \ 0" shows "MPoly_Type.degree (p * q) x = MPoly_Type.degree p x + MPoly_Type.degree q x" proof - interpret transfer_mpoly_to_mpoly_poly x . define deg :: "'a mpoly \ nat" where "deg = (\p. MPoly_Type.degree p x)" have [transfer_rule]: "rel_fun R (=) Polynomial.degree deg" using transfer_degree unfolding deg_def . have "deg (p * q) = deg p + deg q" using assms unfolding deg_def [symmetric] by transfer (simp add: degree_mult_eq) thus ?thesis by (simp add: deg_def) qed text \Converts a multi-variate polynomial into a univariate polynomial via inserting values for all but one variable\ definition partial_insertion :: "(nat \ 'a) \ nat \ 'a :: comm_ring_1 mpoly \ 'a poly" where "partial_insertion \ x p = map_poly (insertion \) (mpoly_to_mpoly_poly x p)" lemma comm_ring_hom_insertion: "comm_ring_hom (insertion \)" by (unfold_locales, auto simp: insertion_add insertion_mult) lemma partial_insertion_add: "partial_insertion \ x (p + q) = partial_insertion \ x p + partial_insertion \ x q" proof - interpret i: comm_ring_hom "insertion \" by (rule comm_ring_hom_insertion) show ?thesis unfolding partial_insertion_def mpoly_to_mpoly_poly_add hom_distribs .. qed lemma partial_insertion_monom: "partial_insertion \ x (MPoly_Type.monom m a) = Polynomial.monom (insertion \ (MPoly_Type.monom (remove_key x m) a)) (lookup m x)" unfolding partial_insertion_def mpoly_to_mpoly_poly_monom by (subst map_poly_monom, auto) text \Partial insertion + insertion of last value is identical to (full) insertion\ lemma insertion_partial_insertion: assumes "\ y. y \ x \ \ y = \ y" shows "poly (partial_insertion \ x p) (\ x) = insertion \ p" proof (induct p rule: mpoly_induct) case (monom m a) let ?rkm = "remove_key x m" have to_alpha: "insertion \ (MPoly_Type.monom ?rkm a) = insertion \ (MPoly_Type.monom ?rkm a)" by (rule insertion_irrelevant_vars, rule assms, insert vars_monom_subset[of ?rkm a], auto simp: remove_key_keys[symmetric]) have main: "insertion \ (MPoly_Type.monom ?rkm a) * \ x ^ lookup m x = insertion \ (MPoly_Type.monom m a)" unfolding monom_remove_key[of m a x] insertion_mult by (metis insertion_single mult.left_neutral) show ?case using main to_alpha by (simp add: partial_insertion_monom poly_monom) next case (sum p1 p2 m a) then show ?case by (simp add: partial_insertion_add insertion_add map_poly_add) qed lemma insertion_coeff_mpoly_to_mpoly_poly[simp]: "insertion \ (coeff (mpoly_to_mpoly_poly x p) k) = coeff (partial_insertion \ x p) k" unfolding partial_insertion_def by (subst coeff_map_poly, auto) lemma degree_map_poly_Const: "degree (map_poly (Const :: 'a :: semiring_0 \ _) f) = degree f" by (rule degree_map_poly, auto) lemma degree_partial_insertion_le_mpoly: "degree (partial_insertion \ x p) \ degree (mpoly_to_mpoly_poly x p)" unfolding partial_insertion_def by (rule degree_map_poly_le) end \ No newline at end of file diff --git a/thys/Factor_Algebraic_Polynomial/ROOT b/thys/Factor_Algebraic_Polynomial/ROOT --- a/thys/Factor_Algebraic_Polynomial/ROOT +++ b/thys/Factor_Algebraic_Polynomial/ROOT @@ -1,12 +1,15 @@ chapter AFP session Factor_Algebraic_Polynomial(AFP) = Cubic_Quartic_Equations + options [timeout = 600] + sessions + Polynomials + Hermite_Lindemann theories Complex_Roots_IA_Code Poly_Connection Multivariate_Resultant Factor_Real_Poly document_files "root.tex" "root.bib" diff --git a/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly.thy b/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly.thy --- a/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly.thy +++ b/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly.thy @@ -1,931 +1,931 @@ section \Representing Roots of Polynomials with Algebraic Coefficients\ text \We provide an algorithm to compute a non-zero integer polynomial $q$ from a polynomial $p$ with algebraic coefficients such that all roots of $p$ are also roots of $q$. In this way, we have a constructive proof that the set of complex algebraic numbers is algebraically closed.\ theory Roots_of_Algebraic_Poly imports - Cubic_Quartic_Equations.Min_Int_Poly_Impl + Cubic_Quartic_Equations.Min_Int_Poly_Complex_Impl Multivariate_Resultant Is_Int_To_Int begin subsection \Preliminaries\ hide_const (open) up_ring.monom hide_const (open) MPoly_Type.monom lemma map_mpoly_Const: "f 0 = 0 \ map_mpoly f (Const i) = Const (f i)" by (intro mpoly_eqI, auto simp: coeff_map_mpoly mpoly_coeff_Const) lemma map_mpoly_Var: "f 1 = 1 \ map_mpoly (f :: 'b :: zero_neq_one \ _) (Var i) = Var i" by (intro mpoly_eqI, auto simp: coeff_map_mpoly coeff_Var when_def) lemma map_mpoly_monom: "f 0 = 0 \ map_mpoly f (MPoly_Type.monom m a) = (MPoly_Type.monom m (f a))" by (intro mpoly_eqI, unfold coeff_map_mpoly if_distrib coeff_monom, simp add: when_def) lemma remove_key_single': "remove_key v (Poly_Mapping.single w n) = (if v = w then 0 else Poly_Mapping.single w n)" by (metis add.right_neutral lookup_single_not_eq remove_key_single remove_key_sum single_zero) context comm_monoid_add_hom begin lemma hom_Sum_any: assumes fin: "finite {x. f x \ 0}" shows "hom (Sum_any f) = Sum_any (\ x. hom (f x))" unfolding Sum_any.expand_set hom_sum by (rule sum.mono_neutral_right[OF fin], auto) lemma comm_monoid_add_hom_mpoly_map: "comm_monoid_add_hom (map_mpoly hom)" by (unfold_locales; intro mpoly_eqI, auto simp: hom_add) lemma map_mpoly_hom_Const: "map_mpoly hom (Const i) = Const (hom i)" by (rule map_mpoly_Const, simp) lemma map_mpoly_hom_monom: "map_mpoly hom (MPoly_Type.monom m a) = MPoly_Type.monom m (hom a)" by (rule map_mpoly_monom, simp) end context comm_ring_hom begin lemma mpoly_to_poly_map_mpoly_hom: "mpoly_to_poly x (map_mpoly hom p) = map_poly hom (mpoly_to_poly x p)" by (rule poly_eqI, unfold coeff_mpoly_to_poly coeff_map_poly_hom, subst coeff_map_mpoly', auto) lemma comm_ring_hom_mpoly_map: "comm_ring_hom (map_mpoly hom)" proof - interpret mp: comm_monoid_add_hom "map_mpoly hom" by (rule comm_monoid_add_hom_mpoly_map) show ?thesis proof (unfold_locales) show "map_mpoly hom 1 = 1" by (intro mpoly_eqI, simp add: MPoly_Type.coeff_def, transfer fixing: hom, transfer fixing: hom, auto simp: when_def) fix x y show "map_mpoly hom (x * y) = map_mpoly hom x * map_mpoly hom y" apply (intro mpoly_eqI) apply (subst coeff_map_mpoly', force) apply (unfold coeff_mpoly_times) apply (subst prod_fun_unfold_prod, blast, blast) apply (subst prod_fun_unfold_prod, blast, blast) apply (subst coeff_map_mpoly', force) apply (subst coeff_map_mpoly', force) apply (subst hom_Sum_any) subgoal proof - let ?X = "{a. MPoly_Type.coeff x a \ 0}" let ?Y = "{a. MPoly_Type.coeff y a \ 0}" have fin: "finite (?X \ ?Y)" by auto show ?thesis by (rule finite_subset[OF _ fin], auto) qed apply (rule Sum_any.cong) subgoal for mon pair by (cases pair, auto simp: hom_mult when_def) done qed qed lemma mpoly_to_mpoly_poly_map_mpoly_hom: "mpoly_to_mpoly_poly x (map_mpoly hom p) = map_poly (map_mpoly hom) (mpoly_to_mpoly_poly x p)" proof - interpret mp: comm_ring_hom "map_mpoly hom" by (rule comm_ring_hom_mpoly_map) interpret mmp: map_poly_comm_monoid_add_hom "map_mpoly hom" .. show ?thesis unfolding mpoly_to_mpoly_poly_def apply (subst mmp.hom_Sum_any, force) apply (rule Sum_any.cong) apply (unfold mp.map_poly_hom_monom map_mpoly_hom_monom) by auto qed end context inj_comm_ring_hom begin lemma inj_comm_ring_hom_mpoly_map: "inj_comm_ring_hom (map_mpoly hom)" proof - interpret mp: comm_ring_hom "map_mpoly hom" by (rule comm_ring_hom_mpoly_map) show ?thesis proof (unfold_locales) fix x assume 0: "map_mpoly hom x = 0" show "x = 0" proof (intro mpoly_eqI) fix m show "MPoly_Type.coeff x m = MPoly_Type.coeff 0 m" using arg_cong[OF 0, of "\ p. MPoly_Type.coeff p m"] by simp qed qed qed lemma resultant_mpoly_poly_hom: "resultant_mpoly_poly x (map_mpoly hom p) (map_poly hom q) = map_mpoly hom (resultant_mpoly_poly x p q)" proof - interpret mp: inj_comm_ring_hom "map_mpoly hom" by (rule inj_comm_ring_hom_mpoly_map) show ?thesis unfolding resultant_mpoly_poly_def unfolding mpoly_to_mpoly_poly_map_mpoly_hom apply (subst mp.resultant_map_poly[symmetric]) subgoal by (subst mp.degree_map_poly_hom, unfold_locales, auto) subgoal by (subst mp.degree_map_poly_hom, unfold_locales, auto) subgoal apply (rule arg_cong[of _ _ "resultant _"], intro poly_eqI) apply (subst coeff_map_poly, force)+ by (simp add: map_mpoly_hom_Const) done qed end lemma map_insort_key: assumes [simp]: "\ x y. g1 x \ g1 y \ g2 (f x) \ g2 (f y)" shows "map f (insort_key g1 a xs) = insort_key g2 (f a) (map f xs)" by (induct xs, auto) lemma map_sort_key: assumes [simp]: "\ x y. g1 x \ g1 y \ g2 (f x) \ g2 (f y)" shows "map f (sort_key g1 xs) = sort_key g2 (map f xs)" by (induct xs, auto simp: map_insort_key) hide_const (open) MPoly_Type.degree hide_const (open) MPoly_Type.coeffs hide_const (open) MPoly_Type.coeff hide_const (open) Symmetric_Polynomials.lead_coeff subsection \More Facts about Resultants\ lemma resultant_iff_coprime_main: fixes f g :: "'a :: field poly" assumes deg: "degree f > 0 \ degree g > 0" shows "resultant f g = 0 \ \ coprime f g" proof (cases "resultant f g = 0") case True from resultant_zero_imp_common_factor[OF deg True] True show ?thesis by simp next case False from deg have fg: "f \ 0 \ g \ 0" by auto from resultant_non_zero_imp_coprime[OF False fg] deg False show ?thesis by auto qed lemma resultant_zero_iff_coprime: fixes f g :: "'a :: field poly" assumes "f \ 0 \ g \ 0" shows "resultant f g = 0 \ \ coprime f g" proof (cases "degree f > 0 \ degree g > 0") case True thus ?thesis using resultant_iff_coprime_main[OF True] by simp next case False hence "degree f = 0" "degree g = 0" by auto then obtain c d where f: "f = [:c:]" and g: "g = [:d:]" using degree0_coeffs by metis+ from assms have cd: "c \ 0 \ d \ 0" unfolding f g by auto have res: "resultant f g = 1" unfolding f g resultant_const by auto have "coprime f g" by (metis assms one_neq_zero res resultant_non_zero_imp_coprime) with res show ?thesis by auto qed text \The problem with the upcoming lemma is that "root" and "irreducibility" refer to the same type. In the actual application we interested in "irreducibility" over the integers, but the roots we are interested in are either real or complex.\ lemma resultant_zero_iff_common_root_irreducible: fixes f g :: "'a :: field poly" assumes irr: "irreducible g" and root: "poly g a = 0" (* g has at least some root *) shows "resultant f g = 0 \ (\ x. poly f x = 0 \ poly g x = 0)" proof - from irr root have deg: "degree g \ 0" using degree0_coeffs[of g] by fastforce show ?thesis proof assume "\ x. poly f x = 0 \ poly g x = 0" then obtain x where "poly f x = 0" "poly g x = 0" by auto from resultant_zero[OF _ this] deg show "resultant f g = 0" by auto next assume "resultant f g = 0" from resultant_zero_imp_common_factor[OF _ this] deg have "\ coprime f g" by auto from this[unfolded not_coprime_iff_common_factor] obtain r where rf: "r dvd f" and rg: "r dvd g" and r: "\ is_unit r" by auto from rg r irr have "g dvd r" by (meson algebraic_semidom_class.irreducible_altdef) with rf have "g dvd f" by auto with root show "\ x. poly f x = 0 \ poly g x = 0" by (intro exI[of _ a], auto simp: dvd_def) qed qed lemma resultant_zero_iff_common_root_complex: fixes f g :: "complex poly" assumes g: "g \ 0" shows "resultant f g = 0 \ (\ x. poly f x = 0 \ poly g x = 0)" proof (cases "degree g = 0") case deg: False show ?thesis proof assume "\ x. poly f x = 0 \ poly g x = 0" then obtain x where "poly f x = 0" "poly g x = 0" by auto from resultant_zero[OF _ this] deg show "resultant f g = 0" by auto next assume "resultant f g = 0" from resultant_zero_imp_common_factor[OF _ this] deg have "\ coprime f g" by auto from this[unfolded not_coprime_iff_common_factor] obtain r where rf: "r dvd f" and rg: "r dvd g" and r: "\ is_unit r" by auto from rg g have r0: "r \ 0" by auto with r have degr: "degree r \ 0" by simp hence "\ constant (poly r)" by (simp add: constant_degree) from fundamental_theorem_of_algebra[OF this] obtain a where root: "poly r a = 0" by auto from rf rg root show "\ x. poly f x = 0 \ poly g x = 0" by (intro exI[of _ a], auto simp: dvd_def) qed next case deg: True from degree0_coeffs[OF deg] obtain c where gc: "g = [:c:]" by auto from gc g have c: "c \ 0" by auto hence "resultant f g \ 0" unfolding gc resultant_const by simp with gc c show ?thesis by auto qed subsection \Systems of Polynomials\ text \Definition of solving a system of polynomials, one being multivariate\ definition mpoly_polys_solution :: "'a :: field mpoly \ (nat \ 'a poly) \ nat set \ (nat \ 'a) \ bool" where "mpoly_polys_solution p qs N \ = ( insertion \ p = 0 \ (\ i \ N. poly (qs i) (\ (Suc i)) = 0))" text \The upcoming lemma shows how to eliminate single variables in multi-variate root-problems. Because of the problem mentioned in @{thm [source] resultant_zero_iff_common_root_irreducible}, we here restrict to polynomials over the complex numbers. Since the result computations are homomorphisms, we are able to lift it to integer polynomials where we are interested in real or complex roots.\ lemma resultant_mpoly_polys_solution: fixes p :: "complex mpoly" assumes nz: "0 \ qs ` N" and i: "i \ N" shows "mpoly_polys_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) \ \ (\ v. mpoly_polys_solution p qs N (\((Suc i) := v)))" proof - let ?x = "Suc i" let ?q = "qs i" let ?mres = "resultant_mpoly_poly ?x p ?q" from i obtain M where N: "N = insert i M" and MN: "M = N - {i}" and iM: "i \ M" by auto from nz i have nzq: "?q \ 0" by auto hence lc0: "lead_coeff (qs i) \ 0" by auto have "mpoly_polys_solution ?mres qs (N - {i}) \ \ insertion \ ?mres = 0 \ (\ i \ M. poly (qs i) (\ (Suc i)) = 0)" unfolding mpoly_polys_solution_def MN .. also have "insertion \ ?mres = 0 \ resultant (partial_insertion \ ?x p) ?q = 0" by (rule insertion_resultant_mpoly_poly_zero[OF nzq]) also have "\ \ (\v. poly (partial_insertion \ ?x p) v = 0 \ poly ?q v = 0)" by (rule resultant_zero_iff_common_root_complex[OF nzq]) also have "\ \ (\v. insertion (\(?x := v)) p = 0 \ poly ?q v = 0)" (is "?lhs = ?rhs") proof (intro iff_exI conj_cong refl arg_cong[of _ _ "\ x. x = 0"]) fix v have "poly (partial_insertion \ ?x p) v = poly (partial_insertion \ ?x p) ((\(?x := v)) ?x)" by simp also have "\ = insertion (\(?x := v)) p" by (rule insertion_partial_insertion, auto) finally show "poly (partial_insertion \ ?x p) v = insertion (\(?x := v)) p" . qed also have "\ \ (\i\M. poly (qs i) (\ (Suc i)) = 0) \ (\v. insertion (\(?x := v)) p = 0 \ poly (qs i) v = 0 \ (\i\M. poly (qs i) ((\(?x := v)) (Suc i)) = 0))" using iM by auto also have "\ \ (\ v. mpoly_polys_solution p qs N (\((Suc i) := v)))" unfolding mpoly_polys_solution_def N by (intro iff_exI, auto) finally show ?thesis . qed text \We now restrict solutions to be evaluated to zero outside the variable range. Then there are only finitely many solutions for our applications.\ definition mpoly_polys_zero_solution :: "'a :: field mpoly \ (nat \ 'a poly) \ nat set \ (nat \ 'a) \ bool" where "mpoly_polys_zero_solution p qs N \ = (mpoly_polys_solution p qs N \ \ (\ i. i \ insert 0 (Suc ` N) \ \ i = 0))" lemma resultant_mpoly_polys_zero_solution: fixes p :: "complex mpoly" assumes nz: "0 \ qs ` N" and i: "i \ N" shows "mpoly_polys_zero_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) \ \ \ v. mpoly_polys_zero_solution p qs N (\(Suc i := v))" "mpoly_polys_zero_solution p qs N \ \ mpoly_polys_zero_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) (\(Suc i := 0))" proof - assume "mpoly_polys_zero_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) \" hence 1: "mpoly_polys_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) \" and 2: "(\ i. i \ insert 0 (Suc ` (N - {i})) \ \ i = 0)" unfolding mpoly_polys_zero_solution_def by auto from resultant_mpoly_polys_solution[of qs N _ p \, OF nz i] 1 obtain v where "mpoly_polys_solution p qs N (\(Suc i := v))" by auto with 2 have "mpoly_polys_zero_solution p qs N (\(Suc i := v))" using i unfolding mpoly_polys_zero_solution_def by auto thus "\ v. mpoly_polys_zero_solution p qs N (\(Suc i := v))" .. next assume "mpoly_polys_zero_solution p qs N \" from this[unfolded mpoly_polys_zero_solution_def] have 1: "mpoly_polys_solution p qs N \" and 2: "\i. i \ insert 0 (Suc ` N) \ \ i = 0" by auto from 1 have "mpoly_polys_solution p qs N (\(Suc i := \ (Suc i)))" by auto hence "\ v. mpoly_polys_solution p qs N (\(Suc i := v))" by blast with resultant_mpoly_polys_solution[of qs N _ p \, OF nz i] have "mpoly_polys_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) \" by auto hence "mpoly_polys_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) (\ (Suc i := 0))" unfolding mpoly_polys_solution_def apply simp apply (subst insertion_irrelevant_vars[of _ _ \]) by (insert vars_resultant_mpoly_poly, auto) thus "mpoly_polys_zero_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) (\(Suc i := 0))" unfolding mpoly_polys_zero_solution_def using 2 by auto qed text \The following two lemmas show that if we start with a system of polynomials with finitely many solutions, then the resulting polynomial cannot be the zero-polynomial.\ lemma finite_resultant_mpoly_polys_non_empty: fixes p :: "complex mpoly" assumes nz: "0 \ qs ` N" and i: "i \ N" and fin: "finite {\. mpoly_polys_zero_solution p qs N \}" shows "finite {\. mpoly_polys_zero_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i}) \}" proof - let ?solN = "mpoly_polys_zero_solution p qs N" let ?solN1 = "mpoly_polys_zero_solution (resultant_mpoly_poly (Suc i) p (qs i)) qs (N - {i})" let ?x = "Suc i" note defs = mpoly_polys_zero_solution_def define zero where "zero \ = \(?x := 0)" for \ :: "nat \ complex" { fix \ assume sol: "?solN1 \" from sol[unfolded defs] have 0: "\ ?x = 0" by auto from resultant_mpoly_polys_zero_solution(1)[of qs N i p, OF nz i sol] obtain v where "?solN (\(?x := v))" by auto hence sol: "\(?x := v) \ {\. ?solN \}" by auto hence "zero (\(?x := v)) \ zero ` {\. ?solN \}" by auto also have "zero (\(?x := v)) = \" using 0 by (auto simp: zero_def) finally have "\ \ zero ` {\. ?solN \}" . } hence "{\. ?solN1 \} \ zero ` {\. ?solN \}" by blast from finite_subset[OF this finite_imageI[OF fin]] show ?thesis . qed lemma finite_resultant_mpoly_polys_empty: fixes p :: "complex mpoly" assumes "finite {\. mpoly_polys_zero_solution p qs {} \}" shows "p \ 0" proof define g where "g x = (\ i :: nat. if i = 0 then x else 0)" for x :: complex assume "p = 0" hence "\ x. mpoly_polys_zero_solution p qs {} (g x)" unfolding mpoly_polys_zero_solution_def mpoly_polys_solution_def g_def by auto hence "range g \ {\. mpoly_polys_zero_solution p qs {} \}" by auto from finite_subset[OF this assms] have "finite (range g)" . moreover have "inj g" unfolding g_def inj_on_def by metis ultimately have "finite (UNIV :: complex set)" by simp thus False using infinite_UNIV_char_0 by auto qed subsection \Elimination of Auxiliary Variables\ fun eliminate_aux_vars :: "'a :: comm_ring_1 mpoly \ (nat \ 'a poly) \ nat list \ 'a poly" where "eliminate_aux_vars p qs [] = mpoly_to_poly 0 p" | "eliminate_aux_vars p qs (i # is) = eliminate_aux_vars (resultant_mpoly_poly (Suc i) p (qs i)) qs is" lemma eliminate_aux_vars_of_int_poly: "eliminate_aux_vars (map_mpoly (of_int :: _ \ 'a :: {comm_ring_1,ring_char_0}) mp) (of_int_poly \ qs) is = of_int_poly (eliminate_aux_vars mp qs is)" proof - let ?h = "of_int :: _ \ 'a" interpret mp: comm_ring_hom "(map_mpoly ?h)" by (rule of_int_hom.comm_ring_hom_mpoly_map) show ?thesis proof (induct "is" arbitrary: mp) case Nil show ?case by (simp add: of_int_hom.mpoly_to_poly_map_mpoly_hom) next case (Cons i "is" mp) show ?case unfolding eliminate_aux_vars.simps Cons[symmetric] apply (rule arg_cong[of _ _ "\ x. eliminate_aux_vars x _ _"], unfold o_def) by (rule of_int_hom.resultant_mpoly_poly_hom) qed qed text \The polynomial of the elimination process will represent the first value @{term "\ 0 :: complex"} of any solution to the multi-polynomial problem.\ lemma eliminate_aux_vars: fixes p :: "complex mpoly" assumes "distinct is" and "vars p \ insert 0 (Suc ` set is)" and "finite {\. mpoly_polys_zero_solution p qs (set is) \}" and "0 \ qs ` set is" and "mpoly_polys_solution p qs (set is) \" shows "poly (eliminate_aux_vars p qs is) (\ 0) = 0 \ eliminate_aux_vars p qs is \ 0" using assms proof (induct "is" arbitrary: p) case (Nil p) from Nil(3) finite_resultant_mpoly_polys_empty[of p] have p0: "p \ 0" by auto from Nil(2) have vars: "vars p \ {0}" by auto note [simp] = poly_eq_insertion[OF this] from Nil(5)[unfolded mpoly_polys_solution_def] have "insertion \ p = 0" by auto also have "insertion \ p = insertion (\v. \ 0) p" by (rule insertion_irrelevant_vars, insert vars, auto) finally show ?case using p0 mpoly_to_poly_inverse[OF vars] by (auto simp: poly_to_mpoly0) next case (Cons i "is" p) let ?x = "Suc i" let ?p = "resultant_mpoly_poly ?x p (qs i)" have dist: "distinct is" using Cons(2) by auto have vars: "vars ?p \ insert 0 (Suc ` set is)" using Cons(3) vars_resultant_mpoly_poly[of ?x p "qs i"] by auto have fin: "finite {\. mpoly_polys_zero_solution ?p qs (set is) \}" using finite_resultant_mpoly_polys_non_empty[of qs "set (i # is)" i p, OF Cons(5)] Cons(2,4) by auto have 0: "0 \ qs ` set is" using Cons(5) by auto have "(\v. mpoly_polys_solution p qs (set (i # is)) (\(?x := v)))" using Cons(6) by (intro exI[of _ "\ ?x"], auto) from this resultant_mpoly_polys_solution[OF Cons(5), of i p \] have "mpoly_polys_solution ?p qs (set (i # is) - {i}) \" by auto also have "set (i # is) - {i} = set is" using Cons(2) by auto finally have "mpoly_polys_solution ?p qs (set is) \" by auto note IH = Cons(1)[OF dist vars fin 0 this] show ?case unfolding eliminate_aux_vars.simps using IH by simp qed subsection \A Representing Polynomial for the Roots of a Polynomial with Algebraic Coefficients\ text \First convert an algebraic polynomial into a system of integer polynomials.\ definition initial_root_problem :: "'a :: {is_rat,field_gcd} poly \ int mpoly \ (nat \ 'a \ int poly) list" where "initial_root_problem p = (let n = degree p; cs = coeffs p; rcs = remdups (filter (\ c. c \ \) cs); pairs = map (\ c. (c, min_int_poly c)) rcs; spairs = sort_key (\ (c,f). degree f) pairs; \ \sort by degree so that easy computations will be done first\ triples = zip [0 ..< length spairs] spairs; mpoly = (sum (\ i. let c = coeff p i in MPoly_Type.monom (Poly_Mapping.single 0 i) 1 * \ \$x_0 ^ i * ...$\ (case find (\ (j,d,f). d = c) triples of None \ Const (to_int c) | Some (j,pair) \ Var (Suc j))) {..n}) in (mpoly, triples))" text \And then eliminate all auxiliary variables\ definition representative_poly :: "'a :: {is_rat,field_char_0,field_gcd} poly \ int poly" where "representative_poly p = (case initial_root_problem p of (mp, triples) \ let is = map fst triples; qs = (\ j. snd (snd (triples ! j))) in eliminate_aux_vars mp qs is)" subsection \Soundness Proof for Complex Algebraic Polynomials\ lemma get_representative_complex: fixes p :: "complex poly" assumes p: "p \ 0" and algebraic: "Ball (set (coeffs p)) algebraic" and res: "initial_root_problem p = (mp, triples)" and "is": "is = map fst triples" and qs: "\ j. j < length is \ qs j = snd (snd (triples ! j))" and root: "poly p x = 0" shows "eliminate_aux_vars mp qs is represents x" proof - define rcs where "rcs = remdups (filter (\c. c \ \) (coeffs p))" define spairs where "spairs = sort_key (\(c, f). degree f) (map (\c. (c, min_int_poly c)) rcs)" let ?find = "\ i. find (\(j, d, f). d = coeff p i) triples" define trans where "trans i = (case ?find i of None \ Const (to_int (coeff p i)) | Some (j, pair) \ Var (Suc j))" for i note res = res[unfolded initial_root_problem_def Let_def, folded rcs_def, folded spairs_def] have triples: "triples = zip [0..i\degree p. MPoly_Type.monom (Poly_Mapping.single 0 i) 1 * trans i)" using res by auto have dist_rcs: "distinct rcs" unfolding rcs_def by auto hence "distinct (map fst (map (\c. (c, min_int_poly c)) rcs))" by (simp add: o_def) hence dist_spairs: "distinct (map fst spairs)" unfolding spairs_def by (metis (no_types, lifting) distinct_map distinct_sort set_sort) { fix c assume "c \ set rcs" hence "c \ set (coeffs p)" unfolding rcs_def by auto with algebraic have "algebraic c" by auto } note rcs_alg = this { fix c assume c: "c \ range (coeff p)" "c \ \" hence "c \ set (coeffs p)" unfolding range_coeff by auto with c have crcs: "c \ set rcs" unfolding rcs_def by auto from rcs_alg[OF crcs] have "algebraic c" . from min_int_poly_represents[OF this] have "min_int_poly c represents c" . hence "\ f. (c,f) \ set spairs \ f represents c" using crcs unfolding spairs_def by auto } have dist_is: "distinct is" unfolding "is" triples by simp note eliminate = eliminate_aux_vars[OF dist_is] let ?mp = "map_mpoly of_int mp :: complex mpoly" have vars_mp: "vars mp \ insert 0 (Suc ` set is)" unfolding mp apply (rule order.trans[OF vars_setsum], force) apply (rule UN_least, rule order.trans[OF vars_mult], rule Un_least) apply (intro order.trans[OF vars_monom_single], force) subgoal for i proof - show ?thesis proof (cases "?find i") case None show ?thesis unfolding trans_def None by auto next case (Some j_pair) then obtain j c f where find: "?find i = Some (j,c,f)" by (cases j_pair, auto) from find_Some_D[OF find] have "Suc j \ Suc ` (fst ` set triples)" by force thus ?thesis unfolding trans_def find by (simp add: vars_Var "is") qed qed done hence varsMp: "vars ?mp \ insert 0 (Suc ` set is)" using vars_map_mpoly_subset by auto note eliminate = eliminate[OF this] let ?f = "\ j. snd (snd (triples ! j))" let ?c = "\ j. fst (snd (triples ! j))" { fix j assume "j \ set is" hence "(?c j, ?f j) \ set spairs" unfolding "is" triples by simp hence "?f j represents ?c j" "?f j = min_int_poly (?c j)" unfolding spairs_def by (auto intro: min_int_poly_represents[OF rcs_alg]) } note is_repr = this let ?qs = "(of_int_poly o qs) :: nat \ complex poly" { fix j assume "j \ set is" hence "j < length is" unfolding "is" triples by simp } note j_len = this have qs_0: "0 \ qs ` set is" proof assume "0 \ qs ` set is" then obtain j where j: "j \ set is" and 0: "qs j = 0" by auto from is_repr[OF j] have "?f j \ 0" by auto with 0 show False unfolding qs[OF j_len[OF j]] by auto qed hence qs0: "0 \ ?qs ` set is" by auto note eliminate = eliminate[OF _ this] define roots where "roots p = (SOME xs. set xs = {x . poly p x = 0})" for p :: "complex poly" { fix p :: "complex poly" assume "p \ 0" from someI_ex[OF finite_list[OF poly_roots_finite[OF this]], folded roots_def] have "set (roots p) = {x. poly p x = 0}" . } note roots = this define qs_roots where "qs_roots = concat_lists (map (\ i. roots (?qs i)) [0 ..< length triples])" define evals where "evals = concat (map (\ part. let q = partial_insertion (\ i. part ! (i - 1)) 0 ?mp; new_roots = roots q in map (\ r. r # part) new_roots) qs_roots)" define conv where "conv roots i = (if i \ length triples then roots ! i else 0 :: complex)" for roots i define alphas where "alphas = map conv evals" { fix n assume n: "n \ {..degree p}" let ?cn = "coeff p n" from n have mem: "?cn \ set (coeffs p)" using p unfolding Polynomial.coeffs_def by force { assume "?cn \ \" with mem have "?cn \ set rcs" unfolding rcs_def by auto hence "(?cn, min_int_poly ?cn) \ set spairs" unfolding spairs_def by auto hence "\ i. (i, ?cn, min_int_poly ?cn) \ set triples" unfolding triples set_zip set_conv_nth by force hence "?find n \ None" unfolding find_None_iff by auto } } note non_int_find = this have fin: "finite {\. mpoly_polys_zero_solution ?mp ?qs (set is) \}" proof (rule finite_subset[OF _ finite_set[of alphas]], standard, clarify) fix \ assume sol: "mpoly_polys_zero_solution ?mp ?qs (set is) \" define part where "part = map (\ i. \ (Suc i)) [0 ..< length triples]" { fix i assume "i > length triples" hence "i \ insert 0 (Suc ` set is)" unfolding triples "is" by auto hence "\ i = 0" using sol[unfolded mpoly_polys_zero_solution_def] by auto } note alpha0 = this { fix i assume "i < length triples" hence i: "i \ set is" unfolding triples "is" by auto from qs0 i have 0: "?qs i \ 0" by auto from i sol[unfolded mpoly_polys_zero_solution_def mpoly_polys_solution_def] have "poly (?qs i) (\ (Suc i)) = 0" by auto hence "\ (Suc i) \ set (roots (?qs i))" "poly (?qs i) (\ (Suc i)) = 0" using roots[OF 0] by auto } note roots2 = this hence part: "part \ set qs_roots" unfolding part_def qs_roots_def concat_lists_listset listset by auto let ?gamma = "(\i. part ! (i - 1))" let ?f = "partial_insertion ?gamma 0 ?mp" have "\ 0 \ set (roots ?f)" proof - from sol[unfolded mpoly_polys_zero_solution_def mpoly_polys_solution_def] have "0 = insertion \ ?mp" by simp also have "\ = insertion (\ i. if i \ length triples then \ i else part ! (i - 1)) ?mp" (is "_ = insertion ?beta _") proof (rule insertion_irrelevant_vars) fix i assume "i \ vars ?mp" from set_mp[OF varsMp this] have "i \ length triples" unfolding triples "is" by auto thus "\ i = ?beta i" by auto qed also have "\ = poly (partial_insertion (?beta(0 := part ! 0)) 0 ?mp) (?beta 0)" by (subst insertion_partial_insertion, auto) also have "?beta(0 := part ! 0) = ?gamma" unfolding part_def by (intro ext, auto) finally have root: "poly ?f (\ 0) = 0" by auto have "?f \ 0" proof interpret mp: inj_comm_ring_hom "map_mpoly complex_of_int" by (rule of_int_hom.inj_comm_ring_hom_mpoly_map) assume "?f = 0" hence "0 = coeff ?f (degree p)" by simp also have "\ = insertion ?gamma (coeff (mpoly_to_mpoly_poly 0 ?mp) (degree p))" unfolding insertion_coeff_mpoly_to_mpoly_poly[symmetric] .. also have "coeff (mpoly_to_mpoly_poly 0 ?mp) (degree p) = map_mpoly of_int (coeff (mpoly_to_mpoly_poly 0 mp) (degree p))" unfolding of_int_hom.mpoly_to_mpoly_poly_map_mpoly_hom by (subst coeff_map_poly, auto) also have "coeff (mpoly_to_mpoly_poly 0 mp) (degree p) = (\x. MPoly_Type.monom (remove_key 0 x) (MPoly_Type.coeff mp x) when lookup x 0 = degree p)" unfolding mpoly_to_mpoly_poly_def when_def by (subst coeff_hom.hom_Sum_any, force, unfold Polynomial.coeff_monom, auto) also have "\ = (\x. MPoly_Type.monom (remove_key 0 x) (\xa\degree p. let xx = Poly_Mapping.single 0 xa in \(a, b). MPoly_Type.coeff (trans xa) b when x = xx + b when a = xx) when lookup x 0 = degree p)" unfolding mp coeff_sum More_MPoly_Type.coeff_monom coeff_mpoly_times Let_def apply (subst prod_fun_unfold_prod, force, force) apply (unfold when_mult, subst when_commute) by (auto simp: when_def intro!: Sum_any.cong sum.cong if_cong arg_cong[of _ _ "MPoly_Type.monom _"]) also have "\ = (\x. MPoly_Type.monom (remove_key 0 x) (\i\degree p. \m. MPoly_Type.coeff (trans i) m when x = Poly_Mapping.single 0 i + m) when lookup x 0 = degree p)" unfolding Sum_any_when_dependent_prod_left Let_def by simp also have "\ = (\x. MPoly_Type.monom (remove_key 0 x) (\i \ {degree p}. \m. MPoly_Type.coeff (trans i) m when x = Poly_Mapping.single 0 i + m) when lookup x 0 = degree p)" apply (intro Sum_any.cong when_cong refl arg_cong[of _ _ "MPoly_Type.monom _"] sum.mono_neutral_right, force+) apply (intro ballI Sum_any_zeroI, auto simp: when_def) subgoal for i x proof (goal_cases) case 1 hence "lookup x 0 > 0" by (auto simp: lookup_add) moreover have "0 \ vars (trans i)" unfolding trans_def by (auto split: option.splits simp: vars_Var) ultimately show ?thesis by (metis set_mp coeff_notin_vars in_keys_iff neq0_conv) qed done also have "\ = (\x. MPoly_Type.monom (remove_key 0 x) (\m. MPoly_Type.coeff (trans (degree p)) m when x = Poly_Mapping.single 0 (degree p) + m) when lookup x 0 = degree p)" (is "_ = ?mid") by simp also have "insertion ?gamma (map_mpoly of_int \) \ 0" proof (cases "?find (degree p)") case None from non_int_find[of "degree p"] None have lcZ: "lead_coeff p \ \" by auto have "?mid = (\x. MPoly_Type.monom (remove_key 0 x) (\m. (to_int (lead_coeff p) when x = Poly_Mapping.single 0 (degree p) + m when m = 0)) when lookup x 0 = degree p)" using None unfolding trans_def None option.simps mpoly_coeff_Const when_def by (intro Sum_any.cong if_cong refl, intro arg_cong[of _ _ "MPoly_Type.monom _"] Sum_any.cong, auto) also have "\ = (\x. MPoly_Type.monom (remove_key 0 x) (to_int (lead_coeff p) when x = Poly_Mapping.single 0 (degree p)) when lookup x 0 = degree p when x = Poly_Mapping.single 0 (degree p))" unfolding Sum_any_when_equal[of _ 0] by (intro Sum_any.cong, auto simp: when_def) also have "\ = MPoly_Type.monom (remove_key 0 (Poly_Mapping.single 0 (degree p))) (to_int (lead_coeff p)) " unfolding Sum_any_when_equal by simp also have "\ = Const (to_int (lead_coeff p))" by (simp add: mpoly_monom_0_eq_Const) also have "map_mpoly of_int \ = Const (lead_coeff p)" unfolding of_int_hom.map_mpoly_hom_Const of_int_to_int[OF lcZ] by simp also have "insertion ?gamma \ = lead_coeff p" by simp also have "\ \ 0" using p by auto finally show ?thesis . next case Some from find_Some_D[OF this] Some obtain j f where mem: "(j,lead_coeff p,f) \ set triples" and Some: "?find (degree p) = Some (j, lead_coeff p, f)" by auto from mem have j: "j < length triples" unfolding triples set_zip by auto have "?mid = (\x. if lookup x 0 = degree p then MPoly_Type.monom (remove_key 0 x) (\m. 1 when m = Poly_Mapping.single (Suc j) 1 when x = Poly_Mapping.single 0 (degree p) + m) else 0)" unfolding trans_def Some option.simps split when_def coeff_Var by auto also have "\ = (\x. if lookup x 0 = degree p then MPoly_Type.monom (remove_key 0 x) 1 when x = Poly_Mapping.single 0 (degree p) + Poly_Mapping.single (Suc j) 1 else 0 when x = Poly_Mapping.single 0 (degree p) + Poly_Mapping.single (Suc j) 1)" apply (subst when_commute) apply (unfold Sum_any_when_equal) by (rule Sum_any.cong, auto simp: when_def) also have "\ = (\x. (MPoly_Type.monom (remove_key 0 x) 1 when lookup x 0 = degree p) when x = Poly_Mapping.single 0 (degree p) + Poly_Mapping.single (Suc j) 1)" by (rule Sum_any.cong, auto simp: when_def) also have "\ = MPoly_Type.monom (Poly_Mapping.single (Suc j) 1) 1" unfolding Sum_any_when_equal unfolding when_def by (simp add: lookup_add remove_key_add[symmetric] remove_key_single' lookup_single) also have "\ = Var (Suc j)" by (intro mpoly_eqI, simp add: coeff_Var coeff_monom) also have "map_mpoly complex_of_int \ = Var (Suc j)" by (simp add: map_mpoly_Var) also have "insertion ?gamma \ = part ! j" by simp also have "\ = \ (Suc j)" unfolding part_def using j by auto also have "\ \ 0" proof assume "\ (Suc j) = 0" with roots2(2)[OF j] have root0: "poly (?qs j) 0 = 0" by auto from j "is" have ji: "j < length is" by auto hence jis: "j \ set is" unfolding "is" triples set_zip by auto from mem have tj: "triples ! j = (j, lead_coeff p, f)" unfolding triples set_zip by auto from root0[unfolded qs[OF ji] o_def tj] have rootf: "poly f 0 = 0" by auto from is_repr[OF jis, unfolded tj] have rootlc: "ipoly f (lead_coeff p) = 0" and f: "f = min_int_poly (lead_coeff p)" by auto from f have irr: "irreducible f" by auto from rootf have "[:0,1:] dvd f" using dvd_iff_poly_eq_0 by fastforce from this[unfolded dvd_def] obtain g where f: "f = [:0, 1:] * g" by auto from irreducibleD[OF irr f] have "is_unit g" by (metis is_unit_poly_iff one_neq_zero one_pCons pCons_eq_iff) then obtain c where g: "g = [:c:]" and c: "c dvd 1" unfolding is_unit_poly_iff by auto from rootlc[unfolded f g] c have "lead_coeff p = 0" by auto with p show False by auto qed finally show ?thesis . qed finally show False by auto qed from roots[OF this] root show ?thesis by auto qed hence "\ 0 # part \ set evals" unfolding evals_def set_concat Let_def set_map by (auto intro!: bexI[OF _ part]) hence "map \ [0 ..< Suc (length triples)] \ set evals" unfolding part_def by (metis Utility.map_upt_Suc) hence "conv (map \ [0 ..< Suc (length triples)]) \ set alphas" unfolding alphas_def by auto also have "conv (map \ [0 ..< Suc (length triples)]) = \" proof fix i show "conv (map \ [0.. i" unfolding conv_def using alpha0 by (cases "i < length triples"; cases "i = length triples"; auto simp: nth_append) qed finally show "\ \ set alphas" . qed note eliminate = eliminate[OF this] define \ where "\ x j = (if j = 0 then x else ?c (j - 1))" for x j have \: "\ x (Suc j) = ?c j" "\ x 0 = x" for j x unfolding \_def by auto interpret mp: inj_comm_ring_hom "map_mpoly complex_of_int" by (rule of_int_hom.inj_comm_ring_hom_mpoly_map) have ins: "insertion (\ x) ?mp = poly p x" for x unfolding poly_altdef mp mp.hom_sum insertion_sum insertion_mult mp.hom_mult proof (rule sum.cong[OF refl], subst mult.commute, rule arg_cong2[of _ _ _ _ "(*)"]) fix n assume n: "n \ {..degree p}" let ?cn = "coeff p n" from n have mem: "?cn \ set (coeffs p)" using p unfolding Polynomial.coeffs_def by force have "insertion (\ x) (map_mpoly complex_of_int (MPoly_Type.monom (Poly_Mapping.single 0 n) 1)) = (\a. \ x a ^ (n when a = 0))" unfolding of_int_hom.map_mpoly_hom_monom by (simp add: lookup_single) also have "\ = (\a. if a = 0 then \ x a ^ n else 1)" by (rule Prod_any.cong, auto simp: when_def) also have "\ = \ x 0 ^ n" by simp also have "\ = x ^ n" unfolding \ .. finally show "insertion (\ x) (map_mpoly complex_of_int (MPoly_Type.monom (Poly_Mapping.single 0 n) 1)) = x ^ n" . show "insertion (\ x) (map_mpoly complex_of_int (trans n)) = ?cn" proof (cases "?find n") case None with non_int_find[OF n] have ints: "?cn \ \" by auto from None show ?thesis unfolding trans_def using ints by (simp add: of_int_hom.map_mpoly_hom_Const of_int_to_int) next case (Some triple) from find_Some_D[OF this] this obtain j f where mem: "(j,?cn,f) \ set triples" and Some: "?find n = Some (j,?cn,f)" by (cases triple, auto) from mem have "triples ! j = (j,?cn,f)" unfolding triples set_zip by auto thus ?thesis unfolding trans_def Some by (simp add: map_mpoly_Var \_def) qed qed from root have "insertion (\ x) ?mp = 0" unfolding ins by auto hence "mpoly_polys_solution ?mp ?qs (set is) (\ x)" unfolding mpoly_polys_solution_def proof (standard, intro ballI) fix j assume j: "j \ set is" from is_repr[OF this] show "poly (?qs j) (\ x (Suc j)) = 0" unfolding \ qs[OF j_len[OF j]] o_def by auto qed note eliminate = eliminate[OF this, unfolded \ eliminate_aux_vars_of_int_poly] thus "eliminate_aux_vars mp qs is represents x" by auto qed lemma representative_poly_complex: fixes x :: complex assumes p: "p \ 0" and algebraic: "Ball (set (coeffs p)) algebraic" and root: "poly p x = 0" shows "representative_poly p represents x" proof - obtain mp triples where init: "initial_root_problem p = (mp, triples)" by force from get_representative_complex[OF p algebraic init refl _ root] show ?thesis unfolding representative_poly_def init Let_def by auto qed subsection \Soundness Proof for Real Algebraic Polynomials\ text \We basically use the result for complex algebraic polynomials which are a superset of real algebraic polynomials.\ lemma initial_root_problem_complex_of_real_poly: "initial_root_problem (map_poly complex_of_real p) = map_prod id (map (map_prod id (map_prod complex_of_real id))) (initial_root_problem p)" proof - let ?c = "of_real :: real \ complex" let ?cp = "map_poly ?c" let ?p = "?cp p :: complex poly" define cn where "cn = degree ?p" define n where "n = degree p" have n: "cn = n" unfolding n_def cn_def by simp note def = initial_root_problem_def[of ?p] note def = def[folded cn_def, unfolded n] define ccs where "ccs = coeffs ?p" define cs where "cs = coeffs p" have cs: "ccs = map ?c cs" unfolding ccs_def cs_def by auto note def = def[folded ccs_def] define crcs where "crcs = remdups (filter (\c. c \ \) ccs)" define rcs where "rcs = remdups (filter (\c. c \ \) cs)" have rcs: "crcs = map ?c rcs" unfolding crcs_def rcs_def cs by (induct cs, auto) define cpairs where "cpairs = map (\c. (c, min_int_poly c)) crcs" define pairs where "pairs = map (\c. (c, min_int_poly c)) rcs" have pairs: "cpairs = map (map_prod ?c id) pairs" unfolding pairs_def cpairs_def rcs by auto define cspairs where "cspairs = sort_key (\(c, y). degree y) cpairs" define spairs where "spairs = sort_key (\(c, y). degree y) pairs" have spairs: "cspairs = map (map_prod ?c id) spairs" unfolding spairs_def cspairs_def pairs by (rule sym, rule map_sort_key, auto) define ctriples where "ctriples = zip [0.. x. _ * x"], induct triples, auto) qed lemma representative_poly_real: fixes x :: real assumes p: "p \ 0" and algebraic: "Ball (set (coeffs p)) algebraic" and root: "poly p x = 0" shows "representative_poly p represents x" proof - obtain mp triples where init: "initial_root_problem p = (mp, triples)" by force define "is" where "is = map fst triples" define qs where "qs = (\ j. snd (snd (triples ! j)))" let ?c = "of_real :: real \ complex" let ?cp = "map_poly ?c" let ?ct = "map (map_prod id (map_prod ?c id))" let ?p = "?cp p :: complex poly" have p: "?p \ 0" using p by auto have "initial_root_problem ?p = map_prod id ?ct (initial_root_problem p)" by (rule initial_root_problem_complex_of_real_poly) from this[unfolded init] have res: "initial_root_problem ?p = (mp, ?ct triples)" by auto from root have "0 = ?c (poly p x)" by simp also have "\ = poly ?p (?c x)" by simp finally have root: "poly ?p (?c x) = 0" by simp have qs: "j < length is \ qs j = snd (snd (?ct triples ! j))" for j unfolding is_def qs_def by (auto simp: set_conv_nth) have "is": "is = map fst (?ct triples)" unfolding is_def by auto { fix cc assume "cc \ set (coeffs ?p)" then obtain c where "c \ set (coeffs p)" and cc: "cc = ?c c" by auto from algebraic this(1) have "algebraic cc" unfolding cc algebraic_complex_iff by auto } hence algebraic: "Ball (set (coeffs ?p)) algebraic" .. from get_representative_complex[OF p this res "is" qs root] have "eliminate_aux_vars mp qs is represents ?c x" . hence "eliminate_aux_vars mp qs is represents x" by simp thus ?thesis unfolding representative_poly_def res init split Let_def qs_def is_def . qed subsection \Algebraic Closedness of Complex Algebraic Numbers\ (* TODO: could be generalised to arbitrary algebraically closed fields? *) lemma complex_algebraic_numbers_are_algebraically_closed: assumes nc: "\ constant (poly p)" and alg: "Ball (set (coeffs p)) algebraic" shows "\ z :: complex. algebraic z \ poly p z = 0" proof - from fundamental_theorem_of_algebra[OF nc] obtain z where root: "poly p z = 0" by auto from algebraic_representsI[OF representative_poly_complex[OF _ alg root]] nc root have "algebraic z \ poly p z = 0" using constant_degree degree_0 by blast thus ?thesis .. qed end \ No newline at end of file diff --git a/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly_Impl.thy b/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly_Impl.thy --- a/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly_Impl.thy +++ b/thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly_Impl.thy @@ -1,52 +1,52 @@ subsection \Executable Version to Compute Representative Polynomials\ theory Roots_of_Algebraic_Poly_Impl imports Roots_of_Algebraic_Poly Polynomials.MPoly_Type_Class_FMap begin text \We need to specialize our code to real and complex polynomials, since @{const algebraic} and @{const min_int_poly} are not executable in their parametric versions.\ definition initial_root_problem_real :: "real poly \ _" where [simp]: "initial_root_problem_real p = initial_root_problem p" definition initial_root_problem_complex :: "complex poly \ _" where [simp]: "initial_root_problem_complex p = initial_root_problem p" lemmas initial_root_problem_code = initial_root_problem_real_def[unfolded initial_root_problem_def] initial_root_problem_complex_def[unfolded initial_root_problem_def] declare initial_root_problem_code[code] lemma initial_root_problem_code_unfold[code_unfold]: "initial_root_problem = initial_root_problem_complex" "initial_root_problem = initial_root_problem_real" by (intro ext, simp)+ definition representative_poly_real :: "real poly \ _" where [simp]: "representative_poly_real p = representative_poly p" definition representative_poly_complex :: "complex poly \ _" where [simp]: "representative_poly_complex p = representative_poly p" lemmas representative_poly_code = representative_poly_real_def[unfolded representative_poly_def] representative_poly_complex_def[unfolded representative_poly_def] declare representative_poly_code[code] lemma representative_poly_code_unfold[code_unfold]: "representative_poly = representative_poly_complex" "representative_poly = representative_poly_real" by (intro ext, simp)+ text \TODO: after merging with AFP devel, this code equation can be removed as it is already present there.\ -lemma algebraic_complex_fun[code_unfold]: "algebraic = (\ x. algebraic (Re x) \ algebraic (Im x))" +lemma algebraic_complex_fun[code_unfold]: "algebraic = (\ y. let x = y in algebraic (Re x) \ algebraic (Im x))" by (intro ext, rule algebraic_complex_iff) end \ No newline at end of file