(* Author: Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> *) section "Misc results for polynomials and sign variations" theory BF_Misc imports "HOL-Computational_Algebra.Polynomial_Factorial" "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" Sturm_Tarski.Sturm_Tarski begin subsection ‹Induction on polynomial roots› (*adapted from the poly_root_induct in Polynomial.thy.*) lemma poly_root_induct_alt [case_names 0 no_proots root]: fixes p :: "'a :: idom poly" assumes "Q 0" assumes "⋀p. (⋀a. poly p a ≠ 0) ⟹ Q p" assumes "⋀a p. Q p ⟹ Q ([:-a, 1:] * p)" shows "Q p" proof (induction "degree p" arbitrary: p rule: less_induct) case (less p) have ?case when "p=0" using ‹Q 0› that by auto moreover have ?case when "∄a. poly p a = 0" using assms(2) that by blast moreover have ?case when "∃a. poly p a = 0" "p≠0" proof - obtain a where "poly p a =0" using ‹∃a. poly p a = 0› by auto then obtain q where pq:"p= [:-a,1:] * q" by (meson dvdE poly_eq_0_iff_dvd) then have "q≠0" using ‹p≠0› by auto then have "degree q<degree p" unfolding pq by (subst degree_mult_eq,auto) then have "Q q" using less by auto then show ?case using assms(3) unfolding pq by auto qed ultimately show ?case by auto qed subsection ‹Misc› lemma lead_coeff_pderiv: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" shows "lead_coeff (pderiv p) = of_nat (degree p) * lead_coeff p" apply (auto simp:degree_pderiv coeff_pderiv) apply (cases "degree p") by (auto simp add: coeff_eq_0) lemma gcd_degree_le_min: assumes "p≠0" "q≠0" shows "degree (gcd p q) ≤ min (degree p) (degree q)" by (simp add: assms(1) assms(2) dvd_imp_degree_le) lemma lead_coeff_normalize_field: fixes p::"'a::{field,semidom_divide_unit_factor} poly" assumes "p≠0" shows "lead_coeff (normalize p) = 1" by (metis (no_types, lifting) assms coeff_normalize divide_self_if dvd_field_iff is_unit_unit_factor leading_coeff_0_iff normalize_eq_0_iff normalize_idem) lemma smult_normalize_field_eq: fixes p::"'a::{field,semidom_divide_unit_factor} poly" shows "p = smult (lead_coeff p) (normalize p)" proof (rule poly_eqI) fix n have "unit_factor (lead_coeff p) = lead_coeff p" by (metis dvd_field_iff is_unit_unit_factor unit_factor_0) then show "coeff p n = coeff (smult (lead_coeff p) (normalize p)) n" by simp qed lemma lead_coeff_gcd_field: fixes p q::"'a::field_gcd poly" assumes "p≠0 ∨ q≠0" shows "lead_coeff (gcd p q) = 1" using assms by (metis gcd.normalize_idem gcd_eq_0_iff lead_coeff_normalize_field) lemma poly_gcd_0_iff: "poly (gcd p q) x = 0 ⟷ poly p x=0 ∧ poly q x=0" by (simp add:poly_eq_0_iff_dvd) lemma degree_eq_oneE: fixes p :: "'a::zero poly" assumes "degree p = 1" obtains a b where "p = [:a,b:]" "b≠0" proof - obtain a b q where p:"p=pCons a (pCons b q)" by (metis pCons_cases) with assms have "q=0" by (cases "q = 0") simp_all with p have "p=[:a,b:]" by auto moreover then have "b≠0" using assms by auto ultimately show ?thesis .. qed subsection ‹More results about sign variations (i.e. @{term changes}› lemma changes_0[simp]:"changes (0#xs) = changes xs" by (cases xs) auto lemma changes_Cons:"changes (x#xs) = (if filter (λx. x≠0) xs = [] then 0 else if x* hd (filter (λx. x≠0) xs) < 0 then 1 + changes xs else changes xs)" apply (induct xs) by auto lemma changes_filter_eq: "changes (filter (λx. x≠0) xs) = changes xs" apply (induct xs) by (auto simp add:changes_Cons) lemma changes_filter_empty: assumes "filter (λx. x≠0) xs = []" shows "changes xs = 0" "changes (a#xs) = 0" using assms apply (induct xs) apply auto by (metis changes_0 neq_Nil_conv) lemma changes_append: assumes "xs≠ [] ∧ ys≠ [] ⟶ (last xs = hd ys ∧ last xs≠0)" shows "changes (xs@ys) = changes xs + changes ys" using assms proof (induct xs) case Nil then show ?case by simp next case (Cons a xs) have ?case when "xs=[]" using that Cons apply (cases ys) by auto moreover have ?case when "ys=[]" using that Cons by auto moreover have ?case when "xs≠[]" "ys≠[]" proof - have "filter (λx. x ≠ 0) xs ≠[]" using that Cons apply auto by (metis (mono_tags, lifting) filter.simps(1) filter.simps(2) filter_append snoc_eq_iff_butlast) then have "changes (a # xs @ ys) = changes (a # xs) + changes ys" apply (subst (1 2) changes_Cons) using that Cons by auto then show ?thesis by auto qed ultimately show ?case by blast qed lemma changes_drop_dup: assumes "xs≠ []" "ys≠ [] ⟶ last xs=hd ys" shows "changes (xs@ys) = changes (xs@ tl ys)" using assms proof (induct xs) case Nil then show ?case by simp next case (Cons a xs) have ?case when "ys=[]" using that by simp moreover have ?case when "ys≠[]" "xs=[]" using that Cons apply auto by (metis changes.simps(3) list.exhaust_sel not_square_less_zero) moreover have ?case when "ys≠[]" "xs≠[]" proof - define ts ts' where "ts = filter (λx. x ≠ 0) (xs @ ys)" and "ts' = filter (λx. x ≠ 0) (xs @ tl ys)" have "(ts = [] ⟷ ts' = []) ∧ hd ts = hd ts'" proof (cases "filter (λx. x ≠ 0) xs = []") case True then have "last xs = 0" using ‹xs≠[]› by (metis (mono_tags, lifting) append_butlast_last_id append_is_Nil_conv filter.simps(2) filter_append list.simps(3)) then have "hd ys=0" using Cons(3)[rule_format, OF ‹ys≠[]›] ‹xs≠[]› by auto then have "filter (λx. x ≠ 0) ys = filter (λx. x ≠ 0) (tl ys)" by (metis (mono_tags, lifting) filter.simps(2) list.exhaust_sel that(1)) then show ?thesis unfolding ts_def ts'_def by auto next case False then show ?thesis unfolding ts_def ts'_def by auto qed moreover have "changes (xs @ ys) = changes (xs @ tl ys)" apply (rule Cons(1)) using that Cons(3) by auto moreover have "changes (a # xs @ ys) = (if ts = [] then 0 else if a * hd ts < 0 then 1 + changes (xs @ ys) else changes (xs @ ys))" using changes_Cons[of a "xs @ ys",folded ts_def] . moreover have "changes (a # xs @ tl ys) = (if ts' = [] then 0 else if a * hd ts' < 0 then 1 + changes (xs @ tl ys) else changes (xs @ tl ys))" using changes_Cons[of a "xs @ tl ys",folded ts'_def] . ultimately show ?thesis by auto qed ultimately show ?case by blast qed (* TODO: the following lemmas contain duplicates of some lemmas in Winding_Number_Eval/Missing_Algebraic.thy Will resolve later. *) lemma Im_poly_of_real: "Im (poly p (of_real x)) = poly (map_poly Im p) x" apply (induct p) by (auto simp add:map_poly_pCons) lemma Re_poly_of_real: "Re (poly p (of_real x)) = poly (map_poly Re p) x" apply (induct p) by (auto simp add:map_poly_pCons) subsection ‹More about @{term map_poly} and @{term of_real}› lemma of_real_poly_map_pCons[simp]:"map_poly of_real (pCons a p) = pCons (of_real a) (map_poly of_real p)" by (simp add: map_poly_pCons) lemma of_real_poly_map_plus[simp]: "map_poly of_real (p + q) = map_poly of_real p + map_poly of_real q" apply (rule poly_eqI) by (auto simp add: coeff_map_poly) lemma of_real_poly_map_smult[simp]:"map_poly of_real (smult s p) = smult (of_real s) (map_poly of_real p)" apply (rule poly_eqI) by (auto simp add: coeff_map_poly) lemma of_real_poly_map_mult[simp]:"map_poly of_real (p*q) = map_poly of_real p * map_poly of_real q" by (induct p,intro poly_eqI,auto) lemma of_real_poly_map_poly: "of_real (poly p x) = poly (map_poly of_real p) (of_real x)" by (induct p,auto) lemma of_real_poly_map_power:"map_poly of_real (p^n) = (map_poly of_real p) ^ n" by (induct n,auto) (*FIXME: not duplicate*) lemma of_real_poly_eq_iff [simp]: "map_poly of_real p = map_poly of_real q ⟷ p = q" by (auto simp: poly_eq_iff coeff_map_poly) (*FIXME: not duplicate*) lemma of_real_poly_eq_0_iff [simp]: "map_poly of_real p = 0 ⟷ p = 0" by (auto simp: poly_eq_iff coeff_map_poly) subsection ‹More about @{term order}› lemma order_multiplicity_eq: assumes "p≠0" shows "order a p = multiplicity [:-a,1:] p" by (metis assms multiplicity_eqI order_1 order_2) lemma order_gcd: assumes "p≠0" "q≠0" shows "order x (gcd p q) = min (order x p) (order x q)" proof - have "prime [:- x, 1:]" apply (auto simp add: prime_elem_linear_poly normalize_poly_def intro!:primeI) by (simp add: pCons_one) then show ?thesis using assms by (auto simp add:order_multiplicity_eq intro:multiplicity_gcd) qed lemma order_linear[simp]: "order x [:-a,1:] = (if x=a then 1 else 0)" by (auto simp add:order_power_n_n[where n=1,simplified] order_0I) lemma map_poly_order_of_real: assumes "p≠0" shows "order (of_real t) (map_poly of_real p) = order t p" using assms proof (induct p rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) then have "order t p = 0" using order_root by blast moreover have "poly (map_poly of_real p) (of_real x) ≠0" for x apply (subst of_real_poly_map_poly[symmetric]) using no_proots order_root by simp then have "order (of_real t) (map_poly of_real p) = 0" using order_root by blast ultimately show ?case by auto next case (root a p) define a1 where "a1=[:-a,1:]" have [simp]:"a1≠0" "p≠0" unfolding a1_def using root(2) by auto have "order (of_real t) (map_poly of_real a1) = order t a1" unfolding a1_def by simp then show ?case apply (fold a1_def) by (simp add:order_mult root) qed lemma order_pcompose: assumes "pcompose p q≠0" shows "order x (pcompose p q) = order x (q-[:poly q x:]) * order (poly q x) p" using ‹pcompose p q≠0› proof (induct p rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) have "order x (p ∘⇩_{p}q) = 0" apply (rule order_0I) using no_proots by (auto simp:poly_pcompose) moreover have "order (poly q x) p = 0" apply (rule order_0I) using no_proots by (auto simp:poly_pcompose) ultimately show ?case by auto next case (root a p) define a1 where "a1=[:-a,1:]" have [simp]: "a1≠0" "p≠0" "a1 ∘⇩_{p}q ≠0" "p ∘⇩_{p}q ≠ 0" subgoal using root(2) unfolding a1_def by simp subgoal using root(2) by auto using root(2) by (fold a1_def,auto simp:pcompose_mult) have "order x ((a1 * p) ∘⇩_{p}q) = order x (a1 ∘⇩_{p}q) + order x (p ∘⇩_{p}q)" unfolding pcompose_mult by (auto simp: order_mult) also have "... = order x (q-[:poly q x:]) * (order (poly q x) a1 + order (poly q x) p)" proof - have "order x (a1 ∘⇩_{p}q) = order x (q-[:poly q x:]) * order (poly q x) a1" unfolding a1_def apply (auto simp: pcompose_pCons algebra_simps diff_conv_add_uminus ) by (simp add: order_0I) moreover have "order x (p ∘⇩_{p}q) = order x (q - [:poly q x:]) * order (poly q x) p" apply (rule root.hyps) by auto ultimately show ?thesis by (auto simp:algebra_simps) qed also have "... = order x (q - [:poly q x:]) * order (poly q x) (a1 * p)" by (auto simp:order_mult) finally show ?case unfolding a1_def . qed subsection ‹Polynomial roots / zeros› definition proots_within::"'a::comm_semiring_0 poly ⇒ 'a set ⇒ 'a set" where "proots_within p s = {x∈s. poly p x=0}" abbreviation proots::"'a::comm_semiring_0 poly ⇒ 'a set" where "proots p ≡ proots_within p UNIV" lemma proots_def: "proots p = {x. poly p x=0}" unfolding proots_within_def by auto lemma proots_within_empty[simp]: "proots_within p {} = {}" unfolding proots_within_def by auto lemma proots_within_0[simp]: "proots_within 0 s = s" unfolding proots_within_def by auto lemma proots_withinI[intro,simp]: "poly p x=0 ⟹ x∈s ⟹ x∈proots_within p s" unfolding proots_within_def by auto lemma proots_within_iff[simp]: "x∈proots_within p s ⟷ poly p x=0 ∧ x∈s" unfolding proots_within_def by auto lemma proots_within_union: "proots_within p A ∪ proots_within p B = proots_within p (A ∪ B)" unfolding proots_within_def by auto lemma proots_within_times: fixes s::"'a::{semiring_no_zero_divisors,comm_semiring_0} set" shows "proots_within (p*q) s = proots_within p s ∪ proots_within q s" unfolding proots_within_def by auto lemma proots_within_gcd: fixes s::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize} set" shows "proots_within (gcd p q) s= proots_within p s ∩ proots_within q s" unfolding proots_within_def by (auto simp add: poly_eq_0_iff_dvd) lemma proots_within_inter: "NO_MATCH UNIV s ⟹ proots_within p s = proots p ∩ s" unfolding proots_within_def by auto lemma proots_within_proots[simp]: "proots_within p s ⊆ proots p" unfolding proots_within_def by auto lemma finite_proots[simp]: fixes p :: "'a::idom poly" shows "p≠0 ⟹ finite (proots_within p s)" unfolding proots_within_def using poly_roots_finite by fast lemma proots_within_pCons_1_iff: fixes a::"'a::idom" shows "proots_within [:-a,1:] s = (if a∈s then {a} else {})" "proots_within [:a,-1:] s = (if a∈s then {a} else {})" by (cases "a∈s",auto) lemma proots_within_uminus[simp]: fixes p :: "'a::comm_ring poly" shows "proots_within (- p) s = proots_within p s" by auto lemma proots_within_smult: fixes a::"'a::{semiring_no_zero_divisors,comm_semiring_0}" assumes "a≠0" shows "proots_within (smult a p) s = proots_within p s" unfolding proots_within_def using assms by auto subsection ‹Polynomial roots counting multiplicities.› (*counting the number of proots WITH MULTIPLICITIES within a set*) definition proots_count::"'a::idom poly ⇒ 'a set ⇒ nat" where "proots_count p s = (∑r∈proots_within p s. order r p)" lemma proots_count_emtpy[simp]:"proots_count p {} = 0" unfolding proots_count_def by auto lemma proots_count_times: fixes s :: "'a::idom set" assumes "p*q≠0" shows "proots_count (p*q) s = proots_count p s + proots_count q s" proof - define pts where "pts=proots_within p s" define qts where "qts=proots_within q s" have [simp]: "finite pts" "finite qts" using ‹p*q≠0› unfolding pts_def qts_def by auto have "(∑r∈pts ∪ qts. order r p) = (∑r∈pts. order r p)" proof (rule comm_monoid_add_class.sum.mono_neutral_cong_right,simp_all) show "∀i∈pts ∪ qts - pts. order i p = 0" unfolding pts_def qts_def proots_within_def using order_root by fastforce qed moreover have "(∑r∈pts ∪ qts. order r q) = (∑r∈qts. order r q)" proof (rule comm_monoid_add_class.sum.mono_neutral_cong_right,simp_all) show "∀i∈pts ∪ qts - qts. order i q = 0" unfolding pts_def qts_def proots_within_def using order_root by fastforce qed ultimately show ?thesis unfolding proots_count_def apply (simp add:proots_within_times order_mult[OF ‹p*q≠0›] sum.distrib) apply (fold pts_def qts_def) by auto qed lemma proots_count_power_n_n: shows "proots_count ([:- a, 1:]^n) s = (if a∈s ∧ n>0 then n else 0)" proof - have "proots_within ([:- a, 1:] ^ n) s= (if a∈s ∧ n>0 then {a} else {})" unfolding proots_within_def by auto thus ?thesis unfolding proots_count_def using order_power_n_n by auto qed lemma degree_proots_count: fixes p::"complex poly" shows "degree p = proots_count p UNIV" proof (induct "degree p" arbitrary:p ) case 0 then obtain c where c_def:"p=[:c:]" using degree_eq_zeroE by auto then show ?case unfolding proots_count_def apply (cases "c=0") by (auto intro!:sum.infinite simp add:infinite_UNIV_char_0 order_0I) next case (Suc n) then have "degree p≠0" and "p≠0" by auto obtain z where "poly p z = 0" using Fundamental_Theorem_Algebra.fundamental_theorem_of_algebra ‹degree p≠0› constant_degree[of p] by auto define onez where "onez=[:-z,1:]" have [simp]: "onez≠0" "degree onez = 1" unfolding onez_def by auto obtain q where q_def:"p= onez * q" using poly_eq_0_iff_dvd ‹poly p z = 0› dvdE unfolding onez_def by blast hence "q≠0" using ‹p≠0› by auto hence "n=degree q" using degree_mult_eq[of onez q] ‹Suc n = degree p› apply (fold q_def) by auto hence "degree q = proots_count q UNIV" using Suc.hyps(1) by simp moreover have " Suc 0 = proots_count onez UNIV" unfolding onez_def using proots_count_power_n_n[of z 1 UNIV] by auto ultimately show ?case unfolding q_def using degree_mult_eq[of onez q] proots_count_times[of onez q UNIV] ‹q≠0› by auto qed lemma proots_count_smult: fixes a::"'a::{semiring_no_zero_divisors,idom}" assumes "a≠0" shows "proots_count (smult a p) s= proots_count p s" proof (cases "p=0") case True then show ?thesis by auto next case False then show ?thesis unfolding proots_count_def using order_smult[OF assms] proots_within_smult[OF assms] by auto qed lemma proots_count_pCons_1_iff: fixes a::"'a::idom" shows "proots_count [:-a,1:] s = (if a∈s then 1 else 0)" unfolding proots_count_def by (cases "a∈s",auto simp add:proots_within_pCons_1_iff order_power_n_n[of _ 1,simplified]) lemma proots_count_uminus[simp]: "proots_count (- p) s = proots_count p s" unfolding proots_count_def by simp lemma card_proots_within_leq: assumes "p≠0" shows "proots_count p s ≥ card (proots_within p s)" using assms proof (induct rule:poly_root_induct[of _ "λx. x∈s"]) case 0 then show ?case unfolding proots_within_def proots_count_def by auto next case (no_roots p) then have "proots_within p s = {}" by auto then show ?case unfolding proots_count_def by auto next case (root a p) have "card (proots_within ([:- a, 1:] * p) s) ≤ card (proots_within [:- a, 1:] s)+card (proots_within p s)" unfolding proots_within_times by (auto simp add:card_Un_le) also have "... ≤ 1+ proots_count p s" proof - have "card (proots_within [:- a, 1:] s) ≤ 1" proof (cases "a∈s") case True then have "proots_within [:- a, 1:] s = {a}" by auto then show ?thesis by auto next case False then have "proots_within [:- a, 1:] s = {}" by auto then show ?thesis by auto qed moreover have "card (proots_within p s) ≤ proots_count p s" apply (rule root.hyps) using root by auto ultimately show ?thesis by auto qed also have "... = proots_count ([:- a,1:] * p) s" apply (subst proots_count_times) subgoal by (metis mult_eq_0_iff pCons_eq_0_iff root.prems zero_neq_one) using root by (auto simp add:proots_count_pCons_1_iff) finally have "card (proots_within ([:- a, 1:] * p) s) ≤ proots_count ([:- a, 1:] * p) s" . then show ?case by (metis (no_types, opaque_lifting) add.inverse_inverse add.inverse_neutral minus_pCons mult_minus_left proots_count_uminus proots_within_uminus) qed (*FIXME: not duplicate*) lemma proots_count_0_imp_empty: assumes "proots_count p s=0" "p≠0" shows "proots_within p s = {}" proof - have "card (proots_within p s) = 0" using card_proots_within_leq[OF ‹p≠0›,of s] ‹proots_count p s=0› by auto moreover have "finite (proots_within p s)" using ‹p≠0› by auto ultimately show ?thesis by auto qed lemma proots_count_leq_degree: assumes "p≠0" shows "proots_count p s≤ degree p" using assms proof (induct rule:poly_root_induct[of _ "λx. x∈s"]) case 0 then show ?case by auto next case (no_roots p) then have "proots_within p s = {}" by auto then show ?case unfolding proots_count_def by auto next case (root a p) have "proots_count ([:a, - 1:] * p) s = proots_count [:a, - 1:] s + proots_count p s" apply (subst proots_count_times) using root by auto also have "... = 1 + proots_count p s" proof - have "proots_count [:a, - 1:] s =1" by (metis (no_types, lifting) add.inverse_inverse add.inverse_neutral minus_pCons proots_count_pCons_1_iff proots_count_uminus root.hyps(1)) then show ?thesis by auto qed also have "... ≤ degree ([:a,-1:] * p)" apply (subst degree_mult_eq) subgoal by auto subgoal using root by auto subgoal using root by (simp add: ‹p ≠ 0›) done finally show ?case . qed (*TODO: not a duplicate*) lemma proots_count_union_disjoint: assumes "A ∩ B = {}" "p≠0" shows "proots_count p (A ∪ B) = proots_count p A + proots_count p B" unfolding proots_count_def apply (subst proots_within_union[symmetric]) apply (subst sum.union_disjoint) using assms by auto lemma proots_count_cong: assumes order_eq:"∀x∈s. order x p = order x q" and "p≠0" and "q≠0" shows "proots_count p s = proots_count q s" unfolding proots_count_def proof (rule sum.cong) have "poly p x = 0 ⟷ poly q x = 0" when "x∈s" for x using order_eq that by (simp add: assms(2) assms(3) order_root) then show "proots_within p s = proots_within q s" by auto show "⋀x. x ∈ proots_within q s ⟹ order x p = order x q" using order_eq by auto qed lemma proots_count_of_real: assumes "p≠0" shows "proots_count (map_poly of_real p) ((of_real::_⇒'a::{real_algebra_1,idom}) ` s) = proots_count p s" proof - define k where "k=(of_real::_⇒'a)" have "proots_within (map_poly of_real p) (k ` s) =k ` (proots_within p s)" unfolding proots_within_def k_def by (auto simp add:of_real_poly_map_poly[symmetric]) then have "proots_count (map_poly of_real p) (k ` s) = (∑r∈k ` (proots_within p s). order r (map_poly of_real p))" unfolding proots_count_def by simp also have "... = sum ((λr. order r (map_poly of_real p)) ∘ k) (proots_within p s)" apply (subst sum.reindex) unfolding k_def by (auto simp add: inj_on_def) also have "... = proots_count p s" unfolding proots_count_def apply (rule sum.cong) unfolding k_def comp_def using ‹p≠0› by (auto simp add:map_poly_order_of_real) finally show ?thesis unfolding k_def . qed (*Is field really necessary here?*) lemma proots_pcompose: fixes p q::"'a::field poly" assumes "p≠0" "degree q=1" shows "proots_count (pcompose p q) s = proots_count p (poly q ` s)" proof - obtain a b where ab:"q=[:a,b:]" "b≠0" using ‹degree q=1› degree_eq_oneE by metis define f where "f=(λy. (y-a)/b)" have f_eq:"f (poly q x) = x" "poly q (f x) = x" for x unfolding f_def using ab by auto have "proots_count (p ∘⇩_{p}q) s = (∑r∈ f ` proots_within p (poly q ` s). order r (p ∘⇩_{p}q))" unfolding proots_count_def apply (rule arg_cong2[where f =sum]) apply (auto simp:poly_pcompose proots_within_def f_eq) by (metis (mono_tags, lifting) f_eq(1) image_eqI mem_Collect_eq) also have "... = (∑x∈proots_within p (poly q ` s). order (f x) (p ∘⇩_{p}q))" apply (subst sum.reindex) subgoal unfolding f_def inj_on_def using ‹b≠0› by auto by simp also have "... = (∑x∈proots_within p (poly q ` s). order x p)" proof - have "p ∘⇩_{p}q ≠ 0" using assms(1) assms(2) pcompose_eq_0 by force moreover have "order (f x) (q - [:x:]) = 1" for x proof - have "order (f x) (q - [:x:]) = order (f x) (smult b [:-((x - a) / b),1:])" unfolding f_def using ab by auto also have "... = 1" apply (subst order_smult) using ‹b≠0› unfolding f_def by auto finally show ?thesis . qed ultimately have "order (f x) (p ∘⇩_{p}q) = order x p" for x apply (subst order_pcompose) using f_eq by auto then show ?thesis by auto qed also have "... = proots_count p (poly q ` s)" unfolding proots_count_def by auto finally show ?thesis . qed subsection ‹Composition of a polynomial and a rational function› (*composition of a polynomial and a rational function. Maybe a more general version in the future?*) definition fcompose::"'a ::field poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a poly" where "fcompose p q r = fst (fold_coeffs (λa (c,d). (d*[:a:] + q * c,r*d)) p (0,1))" lemma fcompose_0 [simp]: "fcompose 0 q r = 0" by (simp add: fcompose_def) lemma fcompose_const[simp]:"fcompose [:a:] q r = [:a:]" unfolding fcompose_def by (cases "a=0") auto lemma fcompose_pCons: "fcompose (pCons a p) q1 q2 = smult a (q2^(degree (pCons a p))) + q1 * fcompose p q1 q2" proof (cases "p=0") case False define ff where "ff=(λa (c, d). (d * [:a:] + q1 * c, q2 * d))" define fc where "fc=fold_coeffs ff p (0, 1)" have snd_ff:"snd fc = (if p=0 then 1 else q2^(degree p + 1))" unfolding fc_def apply (induct p) subgoal by simp subgoal for a p by (auto simp add:ff_def split:if_splits prod.splits) done have "fcompose (pCons a p) q1 q2 = fst (fold_coeffs ff (pCons a p) (0, 1))" unfolding fcompose_def ff_def by simp also have "... = fst (ff a fc)" using False unfolding fc_def by auto also have "... = snd fc * [:a:] + q1 * fst fc" unfolding ff_def by (auto split:prod.splits) also have "... = smult a (q2^(degree (pCons a p))) + q1 * fst fc" using snd_ff False by auto also have "... = smult a (q2^(degree (pCons a p))) + q1 * fcompose p q1 q2" unfolding fc_def ff_def fcompose_def by simp finally show ?thesis . qed simp lemma fcompose_uminus: "fcompose (-p) q r = - fcompose p q r" by (induct p) (auto simp:fcompose_pCons) lemma fcompose_add_less: assumes "degree p1 > degree p2" shows "fcompose (p1+p2) q1 q2 = fcompose p1 q1 q2 + q2^(degree p1-degree p2) * fcompose p2 q1 q2" using assms proof (induction p1 p2 rule: poly_induct2) case (pCons a1 p1 a2 p2) have ?case when "p2=0" using that by (simp add:fcompose_pCons smult_add_left) moreover have ?case when "p2≠0" "¬ degree p2 < degree p1" using that pCons(2) by auto moreover have ?case when "p2≠0" "degree p2< degree p1" proof - define d1 d2 where "d1=degree (pCons a1 p1)" and "d2=degree (pCons a2 p2) " define fp1 fp2 where "fp1= fcompose p1 q1 q2" and "fp2=fcompose p2 q1 q2" have "fcompose (pCons a1 p1 + pCons a2 p2) q1 q2 = fcompose (pCons (a1+a2) (p1+p2)) q1 q2" by simp also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * fcompose (p1 + p2) q1 q2" proof - have "degree (pCons (a1 + a2) (p1 + p2)) = d1" unfolding d1_def using that degree_add_eq_left by fastforce then show ?thesis unfolding fcompose_pCons by simp qed also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * (fp1 + q2 ^ (d1 - d2) * fp2)" proof - have "degree p1 - degree p2 = d1 - d2" unfolding d1_def d2_def using that by simp then show ?thesis unfolding pCons(1)[OF that(2),folded fp1_def fp2_def] by simp qed also have "... = fcompose (pCons a1 p1) q1 q2 + q2 ^ (d1 - d2) * fcompose (pCons a2 p2) q1 q2" proof - have "d1 > d2" unfolding d1_def d2_def using that by auto then show ?thesis unfolding fcompose_pCons apply (fold d1_def d2_def fp1_def fp2_def) by (simp add:algebra_simps smult_add_left power_add[symmetric]) qed finally show ?thesis unfolding d1_def d2_def . qed ultimately show ?case by blast qed simp lemma fcompose_add_eq: assumes "degree p1 = degree p2" shows "q2^(degree p1 - degree (p1+p2)) * fcompose (p1+p2) q1 q2 = fcompose p1 q1 q2 + fcompose p2 q1 q2" using assms proof (induction p1 p2 rule: poly_induct2) case (pCons a1 p1 a2 p2) have ?case when "p1+p2=0" proof - have "p2=-p1" using that by algebra then show ?thesis by (simp add:fcompose_pCons fcompose_uminus smult_add_left) qed moreover have ?case when "p1=0" proof - have "p2=0" using pCons(2) that by (auto split:if_splits) then show ?thesis using that by simp qed moreover have ?case when "p1≠0" "p1+p2≠0" proof - define d1 d2 dp where "d1=degree (pCons a1 p1)" and "d2=degree (pCons a2 p2)" and "dp = degree p1 - degree (p1+p2)" define fp1 fp2 where "fp1= fcompose p1 q1 q2" and "fp2=fcompose p2 q1 q2" have "q2 ^ (degree (pCons a1 p1) - degree (pCons a1 p1 + pCons a2 p2)) * fcompose (pCons a1 p1 + pCons a2 p2) q1 q2 = q2 ^ dp * fcompose (pCons (a1+a2) (p1 +p2)) q1 q2" unfolding dp_def using that by auto also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * (q2 ^ dp * fcompose (p1 + p2) q1 q2)" proof - have "degree p1 ≥ degree (p1 + p2)" by (metis degree_add_le degree_pCons_eq_if not_less_eq_eq order_refl pCons.prems zero_le) then show ?thesis unfolding fcompose_pCons dp_def d1_def using that by (simp add:algebra_simps power_add[symmetric]) qed also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * (fp1 + fp2)" apply (subst pCons(1)[folded dp_def fp1_def fp2_def]) subgoal by (metis degree_pCons_eq_if diff_Suc_Suc diff_zero not_less_eq_eq pCons.prems zero_le) subgoal by simp done also have "... = fcompose (pCons a1 p1) q1 q2 + fcompose (pCons a2 p2) q1 q2" proof - have *:"d1 = degree (pCons a2 p2)" unfolding d1_def using pCons(2) by simp show ?thesis unfolding fcompose_pCons apply (fold d1_def fp1_def fp2_def *) by (simp add:smult_add_left algebra_simps) qed finally show ?thesis . qed ultimately show ?case by blast qed simp lemma fcompose_add_const: "fcompose ([:a:] + p) q1 q2 = smult a (q2 ^ degree p) + fcompose p q1 q2" apply (cases p) by (auto simp add:fcompose_pCons smult_add_left) lemma fcompose_smult: "fcompose (smult a p) q1 q2 = smult a (fcompose p q1 q2)" by (induct p) (simp_all add:fcompose_pCons smult_add_right) lemma fcompose_mult: "fcompose (p1*p2) q1 q2 = fcompose p1 q1 q2 * fcompose p2 q1 q2" proof (induct p1) case 0 then show ?case by simp next case (pCons a p1) have ?case when "p1=0 ∨ p2=0" using that by (auto simp add:fcompose_smult) moreover have ?case when "p1≠0" "p2≠0" "a=0" using that by (simp add:fcompose_pCons pCons) moreover have ?case when "p1≠0" "p2≠0" "a≠0" proof - have "fcompose (pCons a p1 * p2) q1 q2 = fcompose (pCons 0 (p1 * p2) + smult a p2) q1 q2" by (simp add:algebra_simps) also have "... = fcompose (pCons 0 (p1 * p2)) q1 q2 + q2 ^ (degree p1 +1) * fcompose (smult a p2) q1 q2" proof - have "degree (pCons 0 (p1 * p2)) > degree (smult a p2)" using that by (simp add: degree_mult_eq) from fcompose_add_less[OF this,of q1 q2] that show ?thesis by (simp add:degree_mult_eq) qed also have "... = fcompose (pCons a p1) q1 q2 * fcompose p2 q1 q2" using that by (simp add:fcompose_pCons fcompose_smult pCons algebra_simps) finally show ?thesis . qed ultimately show ?case by blast qed lemma fcompose_poly: assumes "poly q2 x≠0" shows "poly p (poly q1 x/poly q2 x) = poly (fcompose p q1 q2) x / poly (q2^(degree p)) x" apply (induct p) using assms by (simp_all add:fcompose_pCons field_simps) lemma poly_fcompose: assumes "poly q2 x≠0" shows "poly (fcompose p q1 q2) x = poly p (poly q1 x/poly q2 x) * (poly q2 x)^(degree p)" using fcompose_poly[OF assms] assms by (auto simp add:field_simps) lemma poly_fcompose_0_denominator: assumes "poly q2 x=0" shows "poly (fcompose p q1 q2) x = poly q1 x ^ degree p * lead_coeff p" apply (induct p) using assms by (auto simp add:fcompose_pCons) lemma fcompose_0_denominator:"fcompose p q1 0 = smult (lead_coeff p) (q1^degree p)" apply (induct p) by (auto simp:fcompose_pCons) lemma fcompose_nzero: fixes p::"'a::field poly" assumes "p≠0" and "q2≠0" and nconst:"∀c. q1 ≠ smult c q2" and infi:"infinite (UNIV::'a set)" shows "fcompose p q1 q2 ≠ 0" using ‹p≠0› proof (induct p rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) have False when "fcompose p q1 q2 = 0" proof - obtain x where "poly q2 x≠0" proof - have "finite (proots q2)" using ‹q2≠0› by auto then have "∃x. poly q2 x≠0" by (meson UNIV_I ex_new_if_finite infi proots_withinI) then show ?thesis using that by auto qed define y where "y = poly q1 x / poly q2 x" have "poly p y = 0" using ‹fcompose p q1 q2 = 0› fcompose_poly[OF ‹poly q2 x≠0›,of p q1,folded y_def] by simp then show False using no_proots(1) by auto qed then show ?case by auto next case (root a p) have "fcompose [:- a, 1:] q1 q2 ≠ 0" unfolding fcompose_def using nconst[rule_format,of a] by simp moreover have "fcompose p q1 q2 ≠ 0" using root by fastforce ultimately show ?case unfolding fcompose_mult by auto qed subsection ‹Bijection (@{term bij_betw}) and the number of polynomial roots› lemma proots_fcompose_bij_eq: fixes p::"'a::field poly" assumes bij:"bij_betw (λx. poly q1 x/poly q2 x) A B" and "p≠0" and nzero:"∀x∈A. poly q2 x≠0" and max_deg: "max (degree q1) (degree q2) ≤ 1" and nconst:"∀c. q1 ≠ smult c q2" and infi:"infinite (UNIV::'a set)" shows "proots_count p B = proots_count (fcompose p q1 q2) A" using ‹p≠0› proof (induct p rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) have "proots_count p B = 0" proof - have "proots_within p B = {}" using no_proots by auto then show ?thesis unfolding proots_count_def by auto qed moreover have "proots_count (fcompose p q1 q2) A = 0" proof - have "proots_within (fcompose p q1 q2) A = {}" using no_proots unfolding proots_within_def by (smt div_0 empty_Collect_eq fcompose_poly nzero) then show ?thesis unfolding proots_count_def by auto qed ultimately show ?case by auto next case (root b p) have "proots_count ([:- b, 1:] * p) B = proots_count [:- b, 1:] B + proots_count p B" using proots_count_times[OF ‹[:- b, 1:] * p ≠ 0›] by simp also have "... = proots_count (fcompose [:- b, 1:] q1 q2) A + proots_count (fcompose p q1 q2) A" proof - define g where "g=(λx. poly q1 x/poly q2 x)" have "proots_count [:- b, 1:] B = proots_count (fcompose [:- b, 1:] q1 q2) A" proof (cases "b∈B") case True then have "proots_count [:- b, 1:] B = 1" unfolding proots_count_pCons_1_iff by simp moreover have "proots_count (fcompose [:- b, 1:] q1 q2) A = 1" proof - obtain a where "b=g a" "a∈A" using bij[folded g_def] True by (metis bij_betwE bij_betw_the_inv_into f_the_inv_into_f_bij_betw) define qq where "qq=q1 - smult b q2" have qq_0:"poly qq a=0" and qq_deg: "degree qq≤1" and ‹qq≠0› unfolding qq_def subgoal using ‹b=g a› nzero[rule_format,OF ‹a∈A›] unfolding g_def by auto subgoal using max_deg by (simp add: degree_diff_le) subgoal using nconst[rule_format,of b] by auto done have "proots_within qq A = {a}" proof - have "a∈proots_within qq A" using qq_0 ‹a∈A› by auto moreover have "card (proots_within qq A) = 1" proof - have "finite (proots_within qq A)" using ‹qq≠0› by simp moreover have "proots_within qq A ≠ {}" using ‹a∈proots_within qq A› by auto ultimately have "card (proots_within qq A) ≠0" by auto moreover have "card (proots_within qq A) ≤ 1" by (meson ‹qq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree qq_deg) ultimately show ?thesis by auto qed ultimately show ?thesis by (metis card_1_singletonE singletonD) qed moreover have "order a qq=1" by (metis One_nat_def ‹qq ≠ 0› le_antisym le_zero_eq not_less_eq_eq order_degree order_root qq_0 qq_deg) ultimately show ?thesis unfolding fcompose_def proots_count_def qq_def by auto qed ultimately show ?thesis by auto next case False then have "proots_count [:- b, 1:] B = 0" unfolding proots_count_pCons_1_iff by simp moreover have "proots_count (fcompose [:- b, 1:] q1 q2) A = 0" proof - have "proots_within (fcompose [:- b, 1:] q1 q2) A = {}" proof (rule ccontr) assume "proots_within (fcompose [:- b, 1:] q1 q2) A ≠ {}" then obtain a where "a∈A" "poly q1 a = b * poly q2 a" unfolding fcompose_def proots_within_def by auto then have "b = g a" unfolding g_def using nzero[rule_format,OF ‹a∈A›] by auto then have "b∈B" using ‹a∈A› bij[folded g_def] using bij_betwE by blast then show False using False by auto qed then show ?thesis unfolding proots_count_def by auto qed ultimately show ?thesis by simp qed moreover have "proots_count p B = proots_count (fcompose p q1 q2) A" apply (rule root.hyps) using mult_eq_0_iff root.prems by blast ultimately show ?thesis by auto qed also have "... = proots_count (fcompose ([:- b, 1:] * p) q1 q2) A" proof (cases "A={}") case False have "fcompose [:- b, 1:] q1 q2 ≠0" using nconst[rule_format,of b] unfolding fcompose_def by auto moreover have "fcompose p q1 q2 ≠ 0" apply (rule fcompose_nzero[OF _ _ nconst infi]) subgoal using ‹[:- b, 1:] * p ≠ 0› by auto subgoal using nzero False by auto done ultimately show ?thesis unfolding fcompose_mult apply (subst proots_count_times) by auto qed auto finally show ?case . qed lemma proots_card_fcompose_bij_eq: fixes p::"'a::field poly" assumes bij:"bij_betw (λx. poly q1 x/poly q2 x) A B" and "p≠0" and nzero:"∀x∈A. poly q2 x≠0" and max_deg: "max (degree q1) (degree q2) ≤ 1" and nconst:"∀c. q1 ≠ smult c q2" and infi:"infinite (UNIV::'a set)" shows "card (proots_within p B) = card (proots_within (fcompose p q1 q2) A)" using ‹p≠0› proof (induct p rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) have "proots_within p B = {}" using no_proots by auto moreover have "proots_within (fcompose p q1 q2) A = {}" using no_proots fcompose_poly by (smt Collect_empty_eq divide_eq_0_iff nzero proots_within_def) ultimately show ?case by auto next case (root b p) then have [simp]:"p≠0" by auto have ?case when "b∉B ∨ poly p b=0" proof - have "proots_within ([:- b, 1:] * p) B = proots_within p B" using that by auto moreover have "proots_within (fcompose ([:- b, 1:] * p) q1 q2) A = proots_within (fcompose p q1 q2) A" using that nzero unfolding fcompose_mult proots_within_times apply (auto simp add: poly_fcompose) using bij bij_betwE by blast ultimately show ?thesis using root by auto qed moreover have ?case when "b∈B" "poly p b≠0" proof - define bb where "bb=[:- b, 1:]" have "card (proots_within (bb * p) B) = card {b} + card (proots_within p B)" proof - have "proots_within bb B = {b}" using that unfolding bb_def by auto then show ?thesis unfolding proots_within_times apply (subst card_Un_disjoint) by (use that in auto) qed also have "... = 1 + card (proots_within (fcompose p q1 q2) A)" using root.hyps by simp also have "... = card (proots_within (fcompose (bb * p) q1 q2) A)" unfolding proots_within_times fcompose_mult proof (subst card_Un_disjoint) obtain a where b_poly:"b=poly q1 a / poly q2 a" and "a∈A" by (metis (no_types, lifting) ‹b ∈ B› bij bij_betwE bij_betw_the_inv_into f_the_inv_into_f_bij_betw) define bbq pq where "bbq=fcompose bb q1 q2" and "pq=fcompose p q1 q2" have bbq_0:"poly bbq a=0" and bbq_deg: "degree bbq≤1" and "bbq≠0" unfolding bbq_def bb_def subgoal using ‹a ∈ A› b_poly nzero poly_fcompose by fastforce subgoal by (metis (no_types, lifting) degree_add_le degree_pCons_eq_if degree_smult_le dual_order.trans fcompose_const fcompose_pCons max.boundedE max_deg mult_cancel_left2 one_neq_zero one_poly_eq_simps(1) power.simps) subgoal by (metis ‹a ∈ A› ‹poly (fcompose [:- b, 1:] q1 q2) a = 0› fcompose_nzero infi nconst nzero one_neq_zero pCons_eq_0_iff) done show "finite (proots_within bbq A)" using ‹bbq≠0› by simp show "finite (proots_within pq A)" unfolding pq_def by (metis ‹a ∈ A› ‹p ≠ 0› fcompose_nzero finite_proots infi nconst nzero poly_0 pq_def) have bbq_a:"proots_within bbq A = {a}" proof - have "a∈proots_within bbq A" by (simp add: ‹a ∈ A› bbq_0) moreover have "card (proots_within bbq A) = 1" proof - have "card (proots_within bbq A) ≠0" using ‹a∈proots_within bbq A› ‹finite (proots_within bbq A)› by auto moreover have "card (proots_within bbq A) ≤ 1" by (meson ‹bbq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree bbq_deg) ultimately show ?thesis by auto qed ultimately show ?thesis by (metis card_1_singletonE singletonD) qed show "proots_within (bbq) A ∩ proots_within (pq) A = {}" using b_poly bbq_a fcompose_poly nzero pq_def that(2) by fastforce show "1 + card (proots_within pq A) = card (proots_within bbq A) + card (proots_within pq A)" using bbq_a by simp qed finally show ?thesis unfolding bb_def . qed ultimately show ?case by auto qed lemma proots_pcompose_bij_eq: fixes p::"'a::idom poly" assumes bij:"bij_betw (λx. poly q x) A B" and "p≠0" and q_deg: "degree q = 1" shows "proots_count p B = proots_count (p ∘⇩_{p}q) A" using ‹p≠0› proof (induct p rule:poly_root_induct_alt) case 0 then show ?case by simp next case (no_proots p) have "proots_count p B = 0" proof - have "proots_within p B = {}" using no_proots by auto then show ?thesis unfolding proots_count_def by auto qed moreover have "proots_count (p ∘⇩_{p}q) A = 0" proof - have "proots_within (p ∘⇩_{p}q) A = {}" using no_proots unfolding proots_within_def by (auto simp:poly_pcompose) then show ?thesis unfolding proots_count_def by auto qed ultimately show ?case by auto next case (root b p) have "proots_count ([:- b, 1:] * p) B = proots_count [:- b, 1:] B + proots_count p B" using proots_count_times[OF ‹[:- b, 1:] * p ≠ 0›] by simp also have "... = proots_count ([:- b, 1:] ∘⇩_{p}q) A + proots_count (p ∘⇩_{p}q) A" proof - have "proots_count [:- b, 1:] B = proots_count ([:- b, 1:] ∘⇩_{p}q) A" proof (cases "b∈B") case True then have "proots_count [:- b, 1:] B = 1" unfolding proots_count_pCons_1_iff by simp moreover have "proots_count ([:- b, 1:] ∘⇩_{p}q) A = 1" proof - obtain a where "b=poly q a" "a∈A" using True bij by (metis bij_betwE bij_betw_the_inv_into f_the_inv_into_f_bij_betw) define qq where "qq=[:- b:] + q" have qq_0:"poly qq a=0" and qq_deg: "degree qq≤1" and ‹qq≠0› unfolding qq_def subgoal using ‹b=poly q a› by auto subgoal using q_deg by (simp add: degree_add_le) subgoal using q_deg add.inverse_unique by force done have "proots_within qq A = {a}" proof - have "a∈proots_within qq A" using qq_0 ‹a∈A› by auto moreover have "card (proots_within qq A) = 1" proof - have "finite (proots_within qq A)" using ‹qq≠0› by simp moreover have "proots_within qq A ≠ {}" using ‹a∈proots_within qq A› by auto ultimately have "card (proots_within qq A) ≠0" by auto moreover have "card (proots_within qq A) ≤ 1" by (meson ‹qq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree qq_deg) ultimately show ?thesis by auto qed ultimately show ?thesis by (metis card_1_singletonE singletonD) qed moreover have "order a qq=1" by (metis One_nat_def ‹qq ≠ 0› le_antisym le_zero_eq not_less_eq_eq order_degree order_root qq_0 qq_deg) ultimately show ?thesis unfolding pcompose_def proots_count_def qq_def by auto qed ultimately show ?thesis by auto next case False then have "proots_count [:- b, 1:] B = 0" unfolding proots_count_pCons_1_iff by simp moreover have "proots_count ([:- b, 1:] ∘⇩_{p}q) A = 0" proof - have "proots_within ([:- b, 1:] ∘⇩_{p}q) A = {}" unfolding pcompose_def apply auto using False bij bij_betwE by blast then show ?thesis unfolding proots_count_def by auto qed ultimately show ?thesis by simp qed moreover have "proots_count p B = proots_count (p ∘⇩_{p}q) A" apply (rule root.hyps) using ‹[:- b, 1:] * p ≠ 0› by auto ultimately show ?thesis by auto qed also have "... = proots_count (([:- b, 1:] * p) ∘⇩_{p}q) A" unfolding pcompose_mult apply (subst proots_count_times) subgoal by (metis (no_types, lifting) One_nat_def add.right_neutral degree_0 degree_mult_eq degree_pCons_eq_if degree_pcompose mult_eq_0_iff one_neq_zero one_pCons pcompose_mult q_deg root.prems) by simp finally show ?case . qed lemma proots_card_pcompose_bij_eq: fixes p::"'a::idom poly" assumes bij:"bij_betw (λx. poly q x) A B" and "p≠0" and q_deg: "degree q = 1" shows "card (proots_within p B) = card (proots_within (p ∘⇩_{p}q) A)" using ‹p≠0› proof (induct p rule:poly_root_induct_alt) case 0 then show ?case by auto next case (no_proots p) have "proots_within p B = {}" using no_proots by auto moreover have "proots_within (p ∘⇩_{p}q) A = {}" using no_proots by (simp add: poly_pcompose proots_within_def) ultimately show ?case by auto next case (root b p) then have [simp]:"p≠0" by auto have ?case when "b∉B ∨ poly p b=0" proof - have "proots_within ([:- b, 1:] * p) B = proots_within p B" using that by auto moreover have "proots_within (([:- b, 1:] * p) ∘⇩_{p}q) A = proots_within (p ∘⇩_{p}q) A" using that unfolding pcompose_mult proots_within_times apply (auto simp add: poly_pcompose) using bij bij_betwE by blast ultimately show ?thesis using root.hyps[OF ‹p≠0›] by auto qed moreover have ?case when "b∈B" "poly p b≠0" proof - define bb where "bb=[:- b, 1:]" have "card (proots_within (bb * p) B) = card {b} + card (proots_within p B)" proof - have "proots_within bb B = {b}" using that unfolding bb_def by auto then show ?thesis unfolding proots_within_times apply (subst card_Un_disjoint) by (use that in auto) qed also have "... = 1 + card (proots_within (p ∘⇩_{p}q) A)" using root.hyps by simp also have "... = card (proots_within ((bb * p) ∘⇩_{p}q) A)" unfolding proots_within_times pcompose_mult proof (subst card_Un_disjoint) obtain a where "b=poly q a" "a∈A" by (metis ‹b ∈ B› bij bij_betwE bij_betw_the_inv_into f_the_inv_into_f_bij_betw) define bbq pq where "bbq=bb ∘⇩_{p}q" and "pq=p ∘⇩_{p}q" have bbq_0:"poly bbq a=0" and bbq_deg: "degree bbq≤1" and "bbq≠0" unfolding bbq_def bb_def poly_pcompose subgoal using ‹b=poly q a› by auto subgoal using q_deg by (simp add: degree_add_le degree_pcompose) subgoal using pcompose_eq_0 q_deg by fastforce done show "finite (proots_within bbq A)" using ‹bbq≠0› by simp show "finite (proots_within pq A)" unfolding pq_def by (metis ‹p ≠ 0› finite_proots pcompose_eq_0 q_deg zero_less_one) have bbq_a:"proots_within bbq A = {a}" proof - have "a∈proots_within bbq A" unfolding bb_def proots_within_def poly_pcompose bbq_def using ‹b=poly q a› ‹a∈A› by simp moreover have "card (proots_within bbq A) = 1" proof - have "card (proots_within bbq A) ≠0" using ‹a∈proots_within bbq A› ‹finite (proots_within bbq A)› by auto moreover have "card (proots_within bbq A) ≤ 1" by (meson ‹bbq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree bbq_deg) ultimately show ?thesis by auto qed ultimately show ?thesis by (metis card_1_singletonE singletonD) qed show "proots_within (bbq) A ∩ proots_within (pq) A = {}" using bbq_a ‹b = poly q a› that(2) unfolding pq_def by (simp add:poly_pcompose) show "1 + card (proots_within pq A) = card (proots_within bbq A) + card (proots_within pq A)" using bbq_a by simp qed finally show ?thesis unfolding bb_def . qed ultimately show ?case by auto qed end