diff --git a/thys/Count_Complex_Roots/Extended_Sturm.thy b/thys/Count_Complex_Roots/Extended_Sturm.thy --- a/thys/Count_Complex_Roots/Extended_Sturm.thy +++ b/thys/Count_Complex_Roots/Extended_Sturm.thy @@ -1,3576 +1,3581 @@ (* Author: Wenda Li *) section \An alternative Sturm sequences\ theory Extended_Sturm imports "Sturm_Tarski.Sturm_Tarski" "Winding_Number_Eval.Cauchy_Index_Theorem" CC_Polynomials_Extra begin text \The main purpose of this theory is to provide an effective way to compute @{term "cindexE a b f"} when @{term f} is a rational function. The idea is similar to and based on the evaluation of @{term cindex_poly} through @{thm cindex_poly_changes_itv_mods}.\ text \ This alternative version of remainder sequences is inspired by the paper "The Fundamental Theorem of Algebra made effective: an elementary real-algebraic proof via Sturm chains" by Michael Eisermann. \ hide_const Permutations.sign subsection \Misc\ lemma path_of_real[simp]:"path (of_real :: real \ 'a::real_normed_algebra_1)" unfolding path_def by (rule continuous_on_of_real_id) lemma pathfinish_of_real[simp]:"pathfinish of_real = 1" unfolding pathfinish_def by simp lemma pathstart_of_real[simp]:"pathstart of_real = 0" unfolding pathstart_def by simp lemma is_unit_pCons_ex_iff: fixes p::"'a::field poly" shows "is_unit p \ (\a. a\0 \ p=[:a:])" using is_unit_poly_iff is_unit_triv by (metis is_unit_pCons_iff) lemma eventually_poly_nz_at_within: fixes x :: "'a::{idom,euclidean_space} " assumes "p\0" shows "eventually (\x. poly p x\0) (at x within S)" proof - have "eventually (\x. poly p x\0) (at x within S) = (\\<^sub>F x in (at x within S). \y\proots p. x \ y)" apply (rule eventually_subst,rule eventuallyI) by (auto simp add:proots_def) also have "... = (\y\proots p. \\<^sub>F x in (at x within S). x \ y)" apply (subst eventually_ball_finite_distrib) using \p\0\ by auto also have "..." unfolding eventually_at by (metis gt_ex not_less_iff_gr_or_eq zero_less_dist_iff) finally show ?thesis . qed lemma sgn_power: fixes x::"'a::linordered_idom" shows "sgn (x^n) = (if n=0 then 1 else if even n then \sgn x\ else sgn x)" apply (induct n) by (auto simp add:sgn_mult) lemma poly_divide_filterlim_at_top: fixes p q::"real poly" defines "ll\( if degree q 0 then at_top else at_bot)" assumes "p\0" "q\0" shows "filterlim (\x. poly q x / poly p x) ll at_top" proof - define pp where "pp=(\x. poly p x / x^(degree p))" define qq where "qq=(\x. poly q x / x^(degree q))" define dd where "dd=(\x::real. if degree p>degree q then 1/x^(degree p - degree q) else x^(degree q - degree p))" have divide_cong:"\\<^sub>Fx in at_top. poly q x / poly p x = qq x / pp x * dd x" proof (rule eventually_at_top_linorderI[of 1]) fix x assume "(x::real)\1" then have "x\0" by auto then show "poly q x / poly p x = qq x / pp x * dd x" unfolding qq_def pp_def dd_def using assms by (auto simp add:field_simps power_diff) qed have qqpp_tendsto:"((\x. qq x / pp x) \ lead_coeff q / lead_coeff p) at_top" proof - have "(qq \ lead_coeff q) at_top" unfolding qq_def using poly_divide_tendsto_aux[of q] by (auto elim!:filterlim_mono simp:at_top_le_at_infinity) moreover have "(pp \ lead_coeff p) at_top" unfolding pp_def using poly_divide_tendsto_aux[of p] by (auto elim!:filterlim_mono simp:at_top_le_at_infinity) ultimately show ?thesis using \p\0\ by (auto intro!:tendsto_eq_intros) qed have ?thesis when "degree qx. poly q x / poly p x) (at 0) at_top" proof (rule filterlim_atI) show "((\x. poly q x / poly p x) \ 0) at_top" using poly_divide_tendsto_0_at_infinity[OF that] by (auto elim:filterlim_mono simp:at_top_le_at_infinity) have "\\<^sub>F x in at_top. poly q x \0" "\\<^sub>F x in at_top. poly p x \0" using poly_eventually_not_zero[OF \q\0\] poly_eventually_not_zero[OF \p\0\] filter_leD[OF at_top_le_at_infinity] by auto then show "\\<^sub>F x in at_top. poly q x / poly p x \ 0" apply eventually_elim by auto qed then show ?thesis unfolding ll_def using that by auto qed moreover have ?thesis when "degree q=degree p" proof - have "((\x. poly q x / poly p x) \ lead_coeff q / lead_coeff p) at_top" using divide_cong qqpp_tendsto that unfolding dd_def by (auto dest:tendsto_cong) then show ?thesis unfolding ll_def using that by auto qed moreover have ?thesis when "degree q>degree p" "sgn_pos_inf q * sgn_pos_inf p > 0" proof - have "filterlim (\x. (qq x / pp x) * dd x) at_top at_top" proof (subst filterlim_tendsto_pos_mult_at_top_iff[OF qqpp_tendsto]) show "0 < lead_coeff q / lead_coeff p" using that(2) unfolding sgn_pos_inf_def by (simp add: zero_less_divide_iff zero_less_mult_iff) show "filterlim dd at_top at_top" unfolding dd_def using that(1) by (auto intro!:filterlim_pow_at_top simp:filterlim_ident) qed then have "LIM x at_top. poly q x / poly p x :> at_top" using filterlim_cong[OF _ _ divide_cong] by blast then show ?thesis unfolding ll_def using that by auto qed moreover have ?thesis when "degree q>degree p" "\ sgn_pos_inf q * sgn_pos_inf p > 0" proof - have "filterlim (\x. (qq x / pp x) * dd x) at_bot at_top" proof (subst filterlim_tendsto_neg_mult_at_bot_iff[OF qqpp_tendsto]) show "lead_coeff q / lead_coeff p < 0" using that(2) \p\0\ \q\0\ unfolding sgn_pos_inf_def by (metis divide_eq_0_iff divide_sgn leading_coeff_0_iff linorder_neqE_linordered_idom sgn_divide sgn_greater) show "filterlim dd at_top at_top" unfolding dd_def using that(1) by (auto intro!:filterlim_pow_at_top simp:filterlim_ident) qed then have "LIM x at_top. poly q x / poly p x :> at_bot" using filterlim_cong[OF _ _ divide_cong] by blast then show ?thesis unfolding ll_def using that by auto qed ultimately show ?thesis by linarith qed lemma poly_divide_filterlim_at_bot: fixes p q::"real poly" defines "ll\( if degree q 0 then at_top else at_bot)" assumes "p\0" "q\0" shows "filterlim (\x. poly q x / poly p x) ll at_bot" proof - define pp where "pp=(\x. poly p x / x^(degree p))" define qq where "qq=(\x. poly q x / x^(degree q))" define dd where "dd=(\x::real. if degree p>degree q then 1/x^(degree p - degree q) else x^(degree q - degree p))" have divide_cong:"\\<^sub>Fx in at_bot. poly q x / poly p x = qq x / pp x * dd x" proof (rule eventually_at_bot_linorderI[of "-1"]) fix x assume "(x::real)\-1" then have "x\0" by auto then show "poly q x / poly p x = qq x / pp x * dd x" unfolding qq_def pp_def dd_def using assms by (auto simp add:field_simps power_diff) qed have qqpp_tendsto:"((\x. qq x / pp x) \ lead_coeff q / lead_coeff p) at_bot" proof - have "(qq \ lead_coeff q) at_bot" unfolding qq_def using poly_divide_tendsto_aux[of q] by (auto elim!:filterlim_mono simp:at_bot_le_at_infinity) moreover have "(pp \ lead_coeff p) at_bot" unfolding pp_def using poly_divide_tendsto_aux[of p] by (auto elim!:filterlim_mono simp:at_bot_le_at_infinity) ultimately show ?thesis using \p\0\ by (auto intro!:tendsto_eq_intros) qed have ?thesis when "degree qx. poly q x / poly p x) (at 0) at_bot" proof (rule filterlim_atI) show "((\x. poly q x / poly p x) \ 0) at_bot" using poly_divide_tendsto_0_at_infinity[OF that] by (auto elim:filterlim_mono simp:at_bot_le_at_infinity) have "\\<^sub>F x in at_bot. poly q x \0" "\\<^sub>F x in at_bot. poly p x \0" using poly_eventually_not_zero[OF \q\0\] poly_eventually_not_zero[OF \p\0\] filter_leD[OF at_bot_le_at_infinity] by auto then show "\\<^sub>F x in at_bot. poly q x / poly p x \ 0" by eventually_elim auto qed then show ?thesis unfolding ll_def using that by auto qed moreover have ?thesis when "degree q=degree p" proof - have "((\x. poly q x / poly p x) \ lead_coeff q / lead_coeff p) at_bot" using divide_cong qqpp_tendsto that unfolding dd_def by (auto dest:tendsto_cong) then show ?thesis unfolding ll_def using that by auto qed moreover have ?thesis when "degree q>degree p" "sgn_neg_inf q * sgn_neg_inf p > 0" proof - define cc where "cc=lead_coeff q / lead_coeff p" have "(cc > 0 \ even (degree q - degree p)) \ (cc<0 \ odd (degree q - degree p))" proof - have "even (degree q - degree p) \ (even (degree q) \ even (degree p)) \ (odd (degree q) \ odd (degree p))" using \degree q>degree p\ by auto then show ?thesis using that \p\0\ \q\0\ unfolding sgn_neg_inf_def cc_def zero_less_mult_iff divide_less_0_iff zero_less_divide_iff apply (simp add:if_split[of "(<) 0"] if_split[of "(>) 0"]) by argo qed moreover have "filterlim (\x. (qq x / pp x) * dd x) at_top at_bot" when "cc>0" "even (degree q - degree p)" proof (subst filterlim_tendsto_pos_mult_at_top_iff[OF qqpp_tendsto]) show "0 < lead_coeff q / lead_coeff p" using \cc>0\ unfolding cc_def by auto show "filterlim dd at_top at_bot" unfolding dd_def using \degree q>degree p\ that(2) by (auto intro!:filterlim_pow_at_bot_even simp:filterlim_ident) qed moreover have "filterlim (\x. (qq x / pp x) * dd x) at_top at_bot" when "cc<0" "odd (degree q - degree p)" proof (subst filterlim_tendsto_neg_mult_at_top_iff[OF qqpp_tendsto]) show "0 > lead_coeff q / lead_coeff p" using \cc<0\ unfolding cc_def by auto show "filterlim dd at_bot at_bot" unfolding dd_def using \degree q>degree p\ that(2) by (auto intro!:filterlim_pow_at_bot_odd simp:filterlim_ident) qed ultimately have "filterlim (\x. (qq x / pp x) * dd x) at_top at_bot" by blast then have "LIM x at_bot. poly q x / poly p x :> at_top" using filterlim_cong[OF _ _ divide_cong] by blast then show ?thesis unfolding ll_def using that by auto qed moreover have ?thesis when "degree q>degree p" "\ sgn_neg_inf q * sgn_neg_inf p > 0" proof - define cc where "cc=lead_coeff q / lead_coeff p" have "(cc < 0 \ even (degree q - degree p)) \ (cc > 0 \ odd (degree q - degree p))" proof - have "even (degree q - degree p) \ (even (degree q) \ even (degree p)) \ (odd (degree q) \ odd (degree p))" using \degree q>degree p\ by auto then show ?thesis using that \p\0\ \q\0\ unfolding sgn_neg_inf_def cc_def zero_less_mult_iff divide_less_0_iff zero_less_divide_iff apply (simp add:if_split[of "(<) 0"] if_split[of "(>) 0"]) by (metis leading_coeff_0_iff linorder_neqE_linordered_idom) qed moreover have "filterlim (\x. (qq x / pp x) * dd x) at_bot at_bot" when "cc<0" "even (degree q - degree p)" proof (subst filterlim_tendsto_neg_mult_at_bot_iff[OF qqpp_tendsto]) show "0 > lead_coeff q / lead_coeff p" using \cc<0\ unfolding cc_def by auto show "filterlim dd at_top at_bot" unfolding dd_def using \degree q>degree p\ that(2) by (auto intro!:filterlim_pow_at_bot_even simp:filterlim_ident) qed moreover have "filterlim (\x. (qq x / pp x) * dd x) at_bot at_bot" when "cc>0" "odd (degree q - degree p)" proof (subst filterlim_tendsto_pos_mult_at_bot_iff[OF qqpp_tendsto]) show "0 < lead_coeff q / lead_coeff p" using \cc>0\ unfolding cc_def by auto show "filterlim dd at_bot at_bot" unfolding dd_def using \degree q>degree p\ that(2) by (auto intro!:filterlim_pow_at_bot_odd simp:filterlim_ident) qed ultimately have "filterlim (\x. (qq x / pp x) * dd x) at_bot at_bot" by blast then have "LIM x at_bot. poly q x / poly p x :> at_bot" using filterlim_cong[OF _ _ divide_cong] by blast then show ?thesis unfolding ll_def using that by auto qed ultimately show ?thesis by linarith qed (*TODO: move*) lemma sgnx_poly_times: assumes "F=at_bot \ F=at_top \ F=at_right x \ F=at_left x" shows "sgnx (poly (p*q)) F = sgnx (poly p) F * sgnx (poly q) F" (is "?PQ = ?P * ?Q") proof - have "(poly p has_sgnx ?P) F" "(poly q has_sgnx ?Q) F" by (rule sgnx_able_sgnx;use assms sgnx_able_poly in blast)+ from has_sgnx_times[OF this] have "(poly (p*q) has_sgnx ?P*?Q) F" by (simp flip:poly_mult) moreover have "(poly (p*q) has_sgnx ?PQ) F" by (rule sgnx_able_sgnx;use assms sgnx_able_poly in blast)+ ultimately show ?thesis using has_sgnx_unique assms by auto qed (*TODO: move*) lemma sgnx_poly_plus: assumes "poly p x=0" "poly q x\0" and F:"F=at_right x \ F=at_left x" shows "sgnx (poly (p+q)) F = sgnx (poly q) F" (is "?L=?R") proof - have "((poly (p+q)) has_sgnx ?R) F" proof - have "sgnx (poly q) F = sgn (poly q x)" using F assms(2) sgnx_poly_nz(1) sgnx_poly_nz(2) by presburger moreover have "((\x. poly (p+q) x) has_sgnx sgn (poly q x)) F" proof (rule tendsto_nonzero_has_sgnx) have "((poly p) \ 0) F" by (metis F assms(1) poly_tendsto(2) poly_tendsto(3)) then have "((\x. poly p x + poly q x) \ poly q x) F" apply (elim tendsto_add[where a=0,simplified]) using F poly_tendsto(2) poly_tendsto(3) by blast then show "((\x. poly (p + q) x) \ poly q x) F" by auto qed fact ultimately show ?thesis by metis qed from has_sgnx_imp_sgnx[OF this] F show ?thesis by auto qed (*TODO: move*) lemma sign_r_pos_plus_imp: assumes "sign_r_pos p x" "sign_r_pos q x" shows "sign_r_pos (p+q) x" using assms unfolding sign_r_pos_def by eventually_elim auto (*TODO: move*) lemma cindex_poly_combine: assumes "a0") case True define A B C D where "A = {x. poly p x = 0 \ a < x \ x < c}" and "B = {x. poly p x = 0 \ a < x \ x < b}" and "C = (if poly p b = 0 then {b} else {})" and "D = {x. poly p x = 0 \ b < x \ x < c}" let ?sum="sum (\x. jump_poly q p x)" have "cindex_poly a c q p = ?sum A" unfolding cindex_poly_def A_def by simp also have "... = ?sum (B \ C \ D)" apply (rule arg_cong2[where f=sum]) unfolding A_def B_def C_def D_def using less_linear assms by auto also have "... = ?sum B + ?sum C + ?sum D" proof - have "finite B" "finite C" "finite D" unfolding B_def C_def D_def using True by (auto simp add: poly_roots_finite) moreover have "B \ C = {}" "C \ D = {}" "B \ D = {}" unfolding B_def C_def D_def using assms by auto ultimately show ?thesis by (subst sum.union_disjoint;auto)+ qed also have "... = cindex_poly a b q p + jump_poly q p b + cindex_poly b c q p" proof - have "?sum C = jump_poly q p b" unfolding C_def using jump_poly_not_root by auto then show ?thesis unfolding cindex_poly_def B_def D_def by auto qed finally show ?thesis by simp qed auto lemma coprime_linear_comp: \\TODO: need to be generalised\ fixes b c::real defines "r0 \ [:b,c:]" assumes "coprime p q" "c\0" shows "coprime (p \\<^sub>p r0) (q \\<^sub>p r0)" proof - define g where "g = gcd (p \\<^sub>p r0) (q \\<^sub>p r0)" define p' where "p' = (p \\<^sub>p r0) div g" define q' where "q' = (q \\<^sub>p r0) div g" define r1 where "r1 = [:-b/c,1/c:]" have r_id: "r0 \\<^sub>p r1 = [:0,1:]" "r1 \\<^sub>p r0 = [:0,1:]" unfolding r0_def r1_def using \c\0\ by (simp add: pcompose_pCons)+ have "p = (g \\<^sub>p r1) * (p' \\<^sub>p r1)" proof - from r_id have "p = p \\<^sub>p (r0 \\<^sub>p r1)" by (metis pcompose_idR) also have "... = (g * p') \\<^sub>p r1" unfolding g_def p'_def by (auto simp:pcompose_assoc) also have "... = (g \\<^sub>p r1) * (p' \\<^sub>p r1)" unfolding pcompose_mult by simp finally show ?thesis . qed moreover have "q = (g \\<^sub>p r1) * (q' \\<^sub>p r1)" proof - from r_id have "q = q \\<^sub>p (r0 \\<^sub>p r1)" by (metis pcompose_idR) also have "... = (g * q') \\<^sub>p r1" unfolding g_def q'_def by (auto simp:pcompose_assoc) also have "... = (g \\<^sub>p r1) * (q' \\<^sub>p r1)" unfolding pcompose_mult by simp finally show ?thesis . qed ultimately have "(g \\<^sub>p r1) dvd gcd p q" by simp then have "g \\<^sub>p r1 dvd 1" using \coprime p q\ by auto from pcompose_hom.hom_dvd_1[OF this] have "is_unit (g \\<^sub>p (r1 \\<^sub>p r0))" by (auto simp:pcompose_assoc) then have "is_unit g" using r_id pcompose_idR by auto then show "coprime (p \\<^sub>p r0) (q \\<^sub>p r0)" unfolding g_def using is_unit_gcd by blast qed lemma finite_ReZ_segments_poly_rectpath: "finite_ReZ_segments (poly p \ rectpath a b) z" unfolding rectpath_def Let_def path_compose_join by ((subst finite_ReZ_segments_joinpaths |intro path_poly_comp conjI); (simp add:poly_linepath_comp finite_ReZ_segments_poly_of_real path_compose_join pathfinish_compose pathstart_compose poly_pcompose)?)+ lemma valid_path_poly_linepath: fixes a b::"'a::real_normed_field" shows "valid_path (poly p o linepath a b)" proof (rule valid_path_compose) show "valid_path (linepath a b)" by simp show "\x. x \ path_image (linepath a b) \ poly p field_differentiable at x" by simp show "continuous_on (path_image (linepath a b)) (deriv (poly p))" unfolding deriv_pderiv by (auto intro:continuous_intros) qed lemma valid_path_poly_rectpath: "valid_path (poly p o rectpath a b)" unfolding rectpath_def Let_def path_compose_join by (simp add: pathfinish_compose pathstart_compose valid_path_poly_linepath) subsection \Sign difference\ definition psign_diff :: "real poly \real poly \ real \ int" where "psign_diff p q x = (if poly p x = 0 \ poly q x = 0 then 1 else \sign (poly p x) - sign (poly q x)\)" lemma psign_diff_alt: assumes "coprime p q" shows "psign_diff p q x = \sign (poly p x) - sign (poly q x)\" unfolding psign_diff_def by (meson assms coprime_poly_0) lemma psign_diff_0[simp]: "psign_diff 0 q x = 1" "psign_diff p 0 x = 1" unfolding psign_diff_def by (auto simp add:sign_def) lemma psign_diff_poly_commute: "psign_diff p q x = psign_diff q p x" unfolding psign_diff_def by (metis abs_minus_commute gcd.commute) lemma normalize_real_poly: "normalize p = smult (1/lead_coeff p) (p::real poly)" unfolding normalize_poly_def by (smt (z3) div_unit_factor normalize_eq_0_iff normalize_poly_def normalize_unit_factor smult_eq_0_iff smult_eq_iff smult_normalize_field_eq unit_factor_1) lemma psign_diff_cancel: assumes "poly r x\0" shows "psign_diff (r*p) (r*q) x = psign_diff p q x" proof - have "poly (r * p) x = 0 \ poly p x=0" by (simp add: assms) moreover have "poly (r * q) x = 0 \ poly q x=0" by (simp add: assms) moreover have "\sign (poly (r * p) x) - sign (poly (r * q) x)\ = \sign (poly p x) - sign (poly q x)\" proof - have "\sign (poly (r * p) x) - sign (poly (r * q) x)\ = \sign (poly r x) * (sign (poly p x) - sign (poly q x))\" by (simp add:algebra_simps sign_times) also have "... = \sign (poly r x) \ * \sign (poly p x) - sign (poly q x)\" unfolding abs_mult by simp also have "... = \sign (poly p x) - sign (poly q x)\" by (simp add: Sturm_Tarski.sign_def assms) finally show ?thesis . qed ultimately show ?thesis - unfolding psign_diff_def by argo + unfolding psign_diff_def by auto qed lemma psign_diff_clear: "psign_diff p q x = psign_diff 1 (p * q) x" unfolding psign_diff_def apply (simp add:sign_times ) by (simp add: sign_def) lemma psign_diff_linear_comp: fixes b c::real defines "h \ (\p. pcompose p [:b,c:])" shows "psign_diff (h p) (h q) x = psign_diff p q (c * x + b)" unfolding psign_diff_def h_def poly_pcompose by (smt (verit, del_insts) mult.commute mult_eq_0_iff poly_0 poly_pCons) subsection \Alternative definition of cross\ definition cross_alt :: "real poly \real poly \ real \ real \ int" where "cross_alt p q a b= psign_diff p q a - psign_diff p q b" lemma cross_alt_0[simp]: "cross_alt 0 q a b = 0" "cross_alt p 0 a b = 0" unfolding cross_alt_def by simp_all lemma cross_alt_poly_commute: "cross_alt p q a b = cross_alt q p a b" unfolding cross_alt_def using psign_diff_poly_commute by auto lemma cross_alt_clear: "cross_alt p q a b = cross_alt 1 (p*q) a b" unfolding cross_alt_def using psign_diff_clear by metis lemma cross_alt_alt: "cross_alt p q a b = sign (poly (p*q) b) - sign (poly (p*q) a)" apply (subst cross_alt_clear) unfolding cross_alt_def psign_diff_def by (auto simp add:sign_def) lemma cross_alt_coprime_0: assumes "coprime p q" "p=0\q=0" shows "cross_alt p q a b=0" proof - have ?thesis when "p=0" proof - have "is_unit q" using that \coprime p q\ by simp then obtain a where "a\0" "q=[:a:]" using is_unit_pCons_ex_iff by blast then show ?thesis using that unfolding cross_alt_def by auto qed moreover have ?thesis when "q=0" proof - have "is_unit p" using that \coprime p q\ by simp then obtain a where "a\0" "p=[:a:]" using is_unit_pCons_ex_iff by blast then show ?thesis using that unfolding cross_alt_def by auto qed ultimately show ?thesis using \p=0\q=0\ by auto qed lemma cross_alt_cancel: assumes "poly q a\0" "poly q b\0" shows "cross_alt (q * r) (q * s) a b = cross_alt r s a b" unfolding cross_alt_def using psign_diff_cancel assms by auto lemma cross_alt_noroot: assumes "ax. a\x \ x\b \ poly (p*q) x\0" shows "cross_alt p q a b = 0" proof - define pq where "pq = p*q" have "cross_alt p q a b = psign_diff 1 pq a - psign_diff 1 pq b " apply (subst cross_alt_clear) unfolding cross_alt_def pq_def by simp also have "... = \1 - sign (poly pq a)\ - \1 - sign (poly pq b)\" unfolding psign_diff_def by simp also have "... = sign (poly pq b) - sign (poly pq a)" unfolding sign_def by auto also have "... = 0" proof (rule ccontr) assume "sign (poly pq b) - sign (poly pq a) \ 0" then have "poly pq a * poly pq b < 0" - by (smt (z3) sign_def assms(1) assms(2) no_zero_divisors pq_def - zero_less_mult_pos zero_less_mult_pos2) + by (smt (verit, best) Sturm_Tarski.sign_def assms(1) assms(2) + divisors_zero eq_iff_diff_eq_0 pq_def zero_less_mult_pos zero_less_mult_pos2) from poly_IVT[OF \a this] have "\x>a. x < b \ poly pq x = 0" . then show False using \\x. a\x \ x\b \ poly (p*q) x\0\ \a apply (fold pq_def) by auto qed finally show ?thesis . qed (* lemma cross_alt_clear_n: assumes "coprime p q" shows "cross_alt p q a b = cross_alt 1 (p*q) a b" proof - have "\sign (poly p a) - sign (poly q a)\ = \1 - sign (poly p a) * sign (poly q a)\" proof (cases "poly p a=0 \ poly q a=0") case True then have False using assms using coprime_poly_0 by blast then show ?thesis by auto next case False then show ?thesis unfolding Sturm_Tarski.sign_def by force qed moreover have "\sign (poly p b) - sign (poly q b)\ = \1 - sign (poly p b) * sign (poly q b)\" proof (cases "poly p b=0 \ poly q b=0") case True then have False using assms using coprime_poly_0 by blast then show ?thesis by auto next case False then show ?thesis unfolding Sturm_Tarski.sign_def by force qed ultimately show ?thesis by (simp add: cross_alt_def sign_times) qed *) lemma cross_alt_linear_comp: fixes b c::real defines "h \ (\p. pcompose p [:b,c:])" shows "cross_alt (h p) (h q) lb ub = cross_alt p q (c * lb + b) (c * ub + b)" unfolding cross_alt_def h_def by (subst (1 2) psign_diff_linear_comp;simp) subsection \Alternative sign variation sequencse\ fun changes_alt:: "('a ::linordered_idom) list \ int" where "changes_alt [] = 0"| "changes_alt [_] = 0" | "changes_alt (x1#x2#xs) = abs(sign x1 - sign x2) + changes_alt (x2#xs)" definition changes_alt_poly_at::"('a ::linordered_idom) poly list \ 'a \ int" where "changes_alt_poly_at ps a= changes_alt (map (\p. poly p a) ps)" definition changes_alt_itv_smods:: "real \ real \real poly \ real poly \ int" where "changes_alt_itv_smods a b p q= (let ps= smods p q in changes_alt_poly_at ps a - changes_alt_poly_at ps b)" lemma changes_alt_itv_smods_rec: assumes "a q = 0 \ q dvd p") case True moreover have "p=0 \ q=0 \ ?thesis" using cross_alt_coprime_0 unfolding changes_alt_itv_smods_def changes_alt_poly_at_def by fastforce moreover have "\p\0;q\0;p mod q = 0\ \ ?thesis" unfolding changes_alt_itv_smods_def changes_alt_poly_at_def cross_alt_def psign_diff_alt[OF \coprime p q\] by (simp add:sign_times) ultimately show ?thesis by auto (auto elim: dvdE) next case False hence "p\0" "q\0" "p mod q\0" by auto then obtain ps where ps:"smods p q=p#q#-(p mod q)#ps" "smods q (-(p mod q)) = q#-(p mod q)#ps" by auto define changes_diff where "changes_diff\\x. changes_alt_poly_at (p#q#-(p mod q)#ps) x - changes_alt_poly_at (q#-(p mod q)#ps) x" have "changes_diff a - changes_diff b=cross_alt p q a b" unfolding changes_diff_def changes_alt_poly_at_def cross_alt_def psign_diff_alt[OF \coprime p q\] by simp thus ?thesis unfolding changes_alt_itv_smods_def changes_diff_def changes_alt_poly_at_def ps by force qed subsection \jumpF on polynomials\ definition jumpF_polyR:: "real poly \ real poly \ real \ real" where "jumpF_polyR q p a = jumpF (\x. poly q x / poly p x) (at_right a)" definition jumpF_polyL:: "real poly \ real poly \ real \ real" where "jumpF_polyL q p a = jumpF (\x. poly q x / poly p x) (at_left a)" definition jumpF_poly_top:: "real poly \ real poly \ real" where "jumpF_poly_top q p = jumpF (\x. poly q x / poly p x) at_top" definition jumpF_poly_bot:: "real poly \ real poly \ real" where "jumpF_poly_bot q p = jumpF (\x. poly q x / poly p x) at_bot" lemma jumpF_polyR_0[simp]: "jumpF_polyR 0 p a = 0" "jumpF_polyR q 0 a = 0" unfolding jumpF_polyR_def by auto lemma jumpF_polyL_0[simp]: "jumpF_polyL 0 p a = 0" "jumpF_polyL q 0 a = 0" unfolding jumpF_polyL_def by auto lemma jumpF_polyR_mult_cancel: assumes "p'\0" shows "jumpF_polyR (p' * q) (p' * p) a = jumpF_polyR q p a" unfolding jumpF_polyR_def proof (rule jumpF_cong) obtain ub where "a < ub" "\z. a < z \ z \ ub \ poly p' z \ 0" using next_non_root_interval[OF \p'\0\,of a] by auto then show "\\<^sub>F x in at_right a. poly (p' * q) x / poly (p' * p) x = poly q x / poly p x" apply (unfold eventually_at_right) apply (intro exI[where x=ub]) by auto qed simp lemma jumpF_polyL_mult_cancel: assumes "p'\0" shows "jumpF_polyL (p' * q) (p' * p) a = jumpF_polyL q p a" unfolding jumpF_polyL_def proof (rule jumpF_cong) obtain lb where "lb < a" "\z. lb \ z \ z < a \ poly p' z \ 0 " using last_non_root_interval[OF \p'\0\,of a] by auto then show "\\<^sub>F x in at_left a. poly (p' * q) x / poly (p' * p) x = poly q x / poly p x" apply (unfold eventually_at_left) apply (intro exI[where x=lb]) by auto qed simp lemma jumpF_poly_noroot: assumes "poly p a\0" shows "jumpF_polyL q p a = 0" "jumpF_polyR q p a = 0" subgoal unfolding jumpF_polyL_def using assms apply (intro jumpF_not_infinity) by (auto intro!:continuous_intros) subgoal unfolding jumpF_polyR_def using assms apply (intro jumpF_not_infinity) by (auto intro!:continuous_intros) done lemma jumpF_polyR_coprime': assumes "poly p x\0 \ poly q x\0" shows "jumpF_polyR q p x = (if p \ 0 \ q \ 0 \ poly p x=0 then if sign_r_pos p x \ poly q x>0 then 1/2 else - 1/2 else 0)" proof (cases "p=0 \ q=0 \ poly p x\0") case True then show ?thesis using jumpF_poly_noroot by fastforce next case False then have asm:"p\0" "q\0" "poly p x=0" by auto then have "poly q x\0" using assms using coprime_poly_0 by blast have ?thesis when "sign_r_pos p x \ poly q x>0" proof - have "(poly p has_sgnx sgn (poly q x)) (at_right x)" by (smt (z3) False \poly q x \ 0\ has_sgnx_imp_sgnx poly_has_sgnx_values(2) sgn_real_def sign_r_pos_sgnx_iff that trivial_limit_at_right_real) then have "LIM x at_right x. poly q x / poly p x :> at_top" apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"]) apply (auto simp add:\poly q x\0\) by (metis asm(3) poly_tendsto(3)) then have "jumpF_polyR q p x = 1/2" unfolding jumpF_polyR_def jumpF_def by auto then show ?thesis using that False by auto qed moreover have ?thesis when "\ (sign_r_pos p x \ poly q x>0)" proof - have "(poly p has_sgnx - sgn (poly q x)) (at_right x)" proof - have "(0::real) < 1 \ \ (1::real) < 0 \ sign_r_pos p x \ (poly p has_sgnx - sgn (poly q x)) (at_right x)" by simp then show ?thesis by (metis (no_types) False \poly q x \ 0\ add.inverse_inverse has_sgnx_imp_sgnx neg_less_0_iff_less poly_has_sgnx_values(2) sgn_if sgn_less sign_r_pos_sgnx_iff that trivial_limit_at_right_real) qed then have "LIM x at_right x. poly q x / poly p x :> at_bot" apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"]) apply (auto simp add:\poly q x\0\) by (metis asm(3) poly_tendsto(3)) then have "jumpF_polyR q p x = - 1/2" unfolding jumpF_polyR_def jumpF_def by auto then show ?thesis using that False by auto qed ultimately show ?thesis by auto qed lemma jumpF_polyR_coprime: assumes "coprime p q" shows "jumpF_polyR q p x = (if p \ 0 \ q \ 0 \ poly p x=0 then if sign_r_pos p x \ poly q x>0 then 1/2 else - 1/2 else 0)" apply (rule jumpF_polyR_coprime') using assms coprime_poly_0 by blast lemma jumpF_polyL_coprime': assumes "poly p x\0 \ poly q x\0" shows "jumpF_polyL q p x = (if p \ 0 \ q \ 0 \ poly p x=0 then if even (order x p) \ sign_r_pos p x \ poly q x>0 then 1/2 else - 1/2 else 0)" proof (cases "p=0 \ q=0 \ poly p x\0") case True then show ?thesis using jumpF_poly_noroot by fastforce next case False then have asm:"p\0" "q\0" "poly p x=0" by auto then have "poly q x\0" using assms using coprime_poly_0 by blast have ?thesis when "even (order x p) \ sign_r_pos p x \ poly q x>0" proof - consider (lt) "poly q x>0" | (gt) " poly q x<0" using \poly q x\0\ by linarith then have "sgnx (poly p) (at_left x) = sgn (poly q x)" apply cases subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF \p\0\,of x] apply (subst poly_sgnx_left_right[OF \p\0\]) by auto subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF \p\0\,of x] apply (subst poly_sgnx_left_right[OF \p\0\]) by auto done then have "(poly p has_sgnx sgn (poly q x)) (at_left x)" by (metis sgnx_able_poly(2) sgnx_able_sgnx) then have "LIM x at_left x. poly q x / poly p x :> at_top" apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"]) apply (auto simp add:\poly q x\0\) by (metis asm(3) poly_tendsto(2)) then have "jumpF_polyL q p x = 1/2" unfolding jumpF_polyL_def jumpF_def by auto then show ?thesis using that False by auto qed moreover have ?thesis when "\ (even (order x p) \ sign_r_pos p x \ poly q x>0)" proof - consider (lt) "poly q x>0" | (gt) " poly q x<0" using \poly q x\0\ by linarith then have "sgnx (poly p) (at_left x) = - sgn (poly q x)" apply cases subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF \p\0\,of x] apply (subst poly_sgnx_left_right[OF \p\0\]) by auto subgoal using that sign_r_pos_sgnx_iff poly_sgnx_values[OF \p\0\,of x] apply (subst poly_sgnx_left_right[OF \p\0\]) by auto done then have "(poly p has_sgnx - sgn (poly q x)) (at_left x)" by (metis sgnx_able_poly(2) sgnx_able_sgnx) then have "LIM x at_left x. poly q x / poly p x :> at_bot" apply (subst filterlim_divide_at_bot_at_top_iff[of _ "poly q x"]) apply (auto simp add:\poly q x\0\) by (metis asm(3) poly_tendsto(2)) then have "jumpF_polyL q p x = - 1/2" unfolding jumpF_polyL_def jumpF_def by auto then show ?thesis using that False by auto qed ultimately show ?thesis by auto qed lemma jumpF_polyL_coprime: assumes "coprime p q" shows "jumpF_polyL q p x = (if p \ 0 \ q \ 0 \ poly p x=0 then if even (order x p) \ sign_r_pos p x \ poly q x>0 then 1/2 else - 1/2 else 0)" apply (rule jumpF_polyL_coprime') using assms coprime_poly_0 by blast lemma jumpF_times: assumes tendsto:"(f \ c) F" and "c\0" "F\bot" shows "jumpF (\x. f x * g x) F = sgn c * jumpF g F" proof - have "c>0 \ c<0" using \c\0\ by auto moreover have ?thesis when "c>0" proof - note filterlim_tendsto_pos_mult_at_top_iff[OF tendsto \c>0\,of g] moreover note filterlim_tendsto_pos_mult_at_bot_iff[OF tendsto \c>0\,of g] moreover have "sgn c = 1" using \c>0\ by auto ultimately show ?thesis unfolding jumpF_def by auto qed moreover have ?thesis when "c<0" proof - define atbot where "atbot = filterlim g at_bot F" define attop where "attop = filterlim g at_top F" have "jumpF (\x. f x * g x) F = (if atbot then 1 / 2 else if attop then - 1 / 2 else 0)" proof - note filterlim_tendsto_neg_mult_at_top_iff[OF tendsto \c<0\,of g] moreover note filterlim_tendsto_neg_mult_at_bot_iff[OF tendsto \c<0\,of g] ultimately show ?thesis unfolding jumpF_def atbot_def attop_def by auto qed also have "... = - (if attop then 1 / 2 else if atbot then - 1 / 2 else 0)" proof - have False when atbot attop using filterlim_at_top_at_bot[OF _ _ \F\bot\] that unfolding atbot_def attop_def by auto then show ?thesis by fastforce qed also have "... = sgn c * jumpF g F" using \c<0\ unfolding jumpF_def attop_def atbot_def by auto finally show ?thesis . qed ultimately show ?thesis by auto qed lemma jumpF_polyR_inverse_add: assumes "coprime p q" shows "jumpF_polyR q p x + jumpF_polyR p q x = jumpF_polyR 1 (q*p) x" proof (cases "p=0 \ q=0") case True then show ?thesis by auto next case False have jumpF_add: "jumpF_polyR q p x= jumpF_polyR 1 (q*p) x" when "poly p x=0" "coprime p q" for p q proof (cases "p=0") case True then show ?thesis by auto next case False have "poly q x\0" using that coprime_poly_0 by blast then have "q\0" by auto moreover have "sign_r_pos p x = (0 < poly q x) \ sign_r_pos (q * p) x" using sign_r_pos_mult[OF \q\0\ \p\0\] sign_r_pos_rec[OF \q\0\] \poly q x\0\ by auto ultimately show ?thesis using \poly p x=0\ unfolding jumpF_polyR_coprime[OF \coprime p q\,of x] jumpF_polyR_coprime[of "q*p" 1 x,simplified] by auto qed have False when "poly p x=0" "poly q x=0" using \coprime p q\ that coprime_poly_0 by blast moreover have ?thesis when "poly p x=0" "poly q x\0" proof - have "jumpF_polyR p q x = 0" using jumpF_poly_noroot[OF \poly q x\0\] by auto then show ?thesis using jumpF_add[OF \poly p x=0\ \coprime p q\] by auto qed moreover have ?thesis when "poly p x\0" "poly q x=0" proof - have "jumpF_polyR q p x = 0" using jumpF_poly_noroot[OF \poly p x\0\] by auto then show ?thesis using jumpF_add[OF \poly q x=0\,of p] \coprime p q\ by (simp add: ac_simps) qed moreover have ?thesis when "poly p x\0" "poly q x\0" by (simp add: jumpF_poly_noroot(2) that(1) that(2)) ultimately show ?thesis by auto qed lemma jumpF_polyL_inverse_add: assumes "coprime p q" shows "jumpF_polyL q p x + jumpF_polyL p q x = jumpF_polyL 1 (q*p) x" proof (cases "p=0 \ q=0") case True then show ?thesis by auto next case False have jumpF_add: "jumpF_polyL q p x= jumpF_polyL 1 (q*p) x" when "poly p x=0" "coprime p q" for p q proof (cases "p=0") case True then show ?thesis by auto next case False have "poly q x\0" using that coprime_poly_0 by blast then have "q\0" by auto moreover have "sign_r_pos p x = (0 < poly q x) \ sign_r_pos (q * p) x" using sign_r_pos_mult[OF \q\0\ \p\0\] sign_r_pos_rec[OF \q\0\] \poly q x\0\ by auto moreover have "order x p = order x (q * p)" by (metis \poly q x \ 0\ add_cancel_right_left divisors_zero order_mult order_root) ultimately show ?thesis using \poly p x=0\ unfolding jumpF_polyL_coprime[OF \coprime p q\,of x] jumpF_polyL_coprime[of "q*p" 1 x,simplified] by auto qed have False when "poly p x=0" "poly q x=0" using \coprime p q\ that coprime_poly_0 by blast moreover have ?thesis when "poly p x=0" "poly q x\0" proof - have "jumpF_polyL p q x = 0" using jumpF_poly_noroot[OF \poly q x\0\] by auto then show ?thesis using jumpF_add[OF \poly p x=0\ \coprime p q\] by auto qed moreover have ?thesis when "poly p x\0" "poly q x=0" proof - have "jumpF_polyL q p x = 0" using jumpF_poly_noroot[OF \poly p x\0\] by auto then show ?thesis using jumpF_add[OF \poly q x=0\,of p] \coprime p q\ by (simp add: ac_simps) qed moreover have ?thesis when "poly p x\0" "poly q x\0" by (simp add: jumpF_poly_noroot that(1) that(2)) ultimately show ?thesis by auto qed lemma jumpF_polyL_smult_1: "jumpF_polyL (smult c q) p x = sgn c * jumpF_polyL q p x" proof (cases "c=0") case True then show ?thesis by auto next case False then show ?thesis unfolding jumpF_polyL_def apply (subst jumpF_times[of "\_. c",symmetric]) by auto qed lemma jumpF_polyR_smult_1: "jumpF_polyR (smult c q) p x = sgn c * jumpF_polyR q p x" proof (cases "c=0") case True then show ?thesis by auto next case False then show ?thesis unfolding jumpF_polyR_def using False apply (subst jumpF_times[of "\_. c",symmetric]) by auto qed lemma shows jumpF_polyR_mod:"jumpF_polyR q p x = jumpF_polyR (q mod p) p x" and jumpF_polyL_mod:"jumpF_polyL q p x = jumpF_polyL (q mod p) p x" proof - define f where "f=(\x. poly (q div p) x)" define g where "g=(\x. poly (q mod p) x / poly p x)" have jumpF_eq:"jumpF (\x. poly q x / poly p x) (at y within S) = jumpF g (at y within S)" when "p\0" for y S proof - let ?F = "at y within S" have "\\<^sub>F x in at y within S. poly p x \ 0" using eventually_poly_nz_at_within[OF \p\0\,of y S] . then have "eventually (\x. (poly q x / poly p x) = (f x+ g x)) ?F" proof (rule eventually_mono) fix x assume P: "poly p x \ 0" have "poly q x = poly (q div p * p + q mod p) x" by simp also have "\ = f x * poly p x + poly (q mod p) x" by (simp only: poly_add poly_mult f_def g_def) moreover have "poly (q mod p) x = g x * poly p x" using P by (simp add: g_def) ultimately show "poly q x / poly p x = f x + g x" using P by simp qed then have "jumpF (\x. poly q x / poly p x) ?F = jumpF (\x. f x+ g x) ?F" by (intro jumpF_cong,auto) also have "... = jumpF g ?F" proof - have "(f \ f y) (at y within S)" unfolding f_def by (intro tendsto_intros) from filterlim_tendsto_add_at_bot_iff[OF this,of g] filterlim_tendsto_add_at_top_iff[OF this,of g] show ?thesis unfolding jumpF_def by auto qed finally show ?thesis . qed show "jumpF_polyR q p x = jumpF_polyR (q mod p) p x" apply (cases "p=0") subgoal by auto subgoal using jumpF_eq unfolding g_def jumpF_polyR_def by auto done show "jumpF_polyL q p x = jumpF_polyL (q mod p) p x" apply (cases "p=0") subgoal by auto subgoal using jumpF_eq unfolding g_def jumpF_polyL_def by auto done qed lemma assumes "order x p \ order x r" shows jumpF_polyR_order_leq: "jumpF_polyR (r+q) p x = jumpF_polyR q p x" and jumpF_polyL_order_leq: "jumpF_polyL (r+q) p x = jumpF_polyL q p x" proof - define f g h where "f=(\x. poly (q + r) x / poly p x)" and "g=(\x. poly q x / poly p x)" and "h=(\x. poly r x / poly p x)" have "\c. h \x\ c" if "p\0" "r\0" proof - define xo where "xo=[:- x, 1:] ^ order x p" obtain p' where "p = xo * p'" "\ [:- x, 1:] dvd p'" using order_decomp[OF \p\0\,of x] unfolding xo_def by auto define r' where "r'= r div xo" define h' where "h' = (\x. poly r' x/ poly p' x)" have "\\<^sub>F x in at x. h x = h' x" proof - obtain S where "open S" "x\S" by blast moreover have " h w = h' w" if "w\S" "w\x" for w proof - have "r=xo * r'" proof - have "xo dvd r" unfolding xo_def using \r\0\ assms by (subst order_divides) simp then show ?thesis unfolding r'_def by simp qed moreover have "poly xo w\0" unfolding xo_def using \w\x\ by simp moreover note \p = xo * p'\ ultimately show ?thesis unfolding h_def h'_def by auto qed ultimately show ?thesis unfolding eventually_at_topological by auto qed moreover have "h'\x\ h' x" proof - have "poly p' x\0" using \\ [:- x, 1:] dvd p'\ poly_eq_0_iff_dvd by blast then show ?thesis unfolding h'_def by (auto intro!:tendsto_eq_intros) qed ultimately have "h \x\ h' x" using tendsto_cong by auto then show ?thesis by auto qed then obtain c where left:"(h \ c) (at_left x)" and right:"(h \ c) (at_right x)" if "p\0" "r\0" unfolding filterlim_at_split by auto show "jumpF_polyR (r+q) p x = jumpF_polyR q p x" proof (cases "p=0 \ r=0") case False have "jumpF_polyR (r+q) p x = (if filterlim (\x. h x + g x) at_top (at_right x) then 1 / 2 else if filterlim (\x. h x + g x) at_bot (at_right x) then - 1 / 2 else 0)" unfolding jumpF_polyR_def jumpF_def g_def h_def by (simp add:poly_add add_divide_distrib) also have "... = (if filterlim g at_top (at_right x) then 1 / 2 else if filterlim g at_bot (at_right x) then - 1 / 2 else 0)" using filterlim_tendsto_add_at_top_iff[OF right] filterlim_tendsto_add_at_bot_iff[OF right] False by simp also have "... = jumpF_polyR q p x" unfolding jumpF_polyR_def jumpF_def g_def by simp finally show "jumpF_polyR (r + q) p x = jumpF_polyR q p x" . qed auto show "jumpF_polyL (r+q) p x = jumpF_polyL q p x" proof (cases "p=0 \ r=0") case False have "jumpF_polyL (r+q) p x = (if filterlim (\x. h x + g x) at_top (at_left x) then 1 / 2 else if filterlim (\x. h x + g x) at_bot (at_left x) then - 1 / 2 else 0)" unfolding jumpF_polyL_def jumpF_def g_def h_def by (simp add:poly_add add_divide_distrib) also have "... = (if filterlim g at_top (at_left x) then 1 / 2 else if filterlim g at_bot (at_left x) then - 1 / 2 else 0)" using filterlim_tendsto_add_at_top_iff[OF left] filterlim_tendsto_add_at_bot_iff[OF left] False by simp also have "... = jumpF_polyL q p x" unfolding jumpF_polyL_def jumpF_def g_def by simp finally show "jumpF_polyL (r + q) p x = jumpF_polyL q p x" . qed auto qed lemma assumes "order x q < order x r" "q\0" shows jumpF_polyR_order_le:"jumpF_polyR (r+q) p x = jumpF_polyR q p x" and jumpF_polyL_order_le:"jumpF_polyL (r+q) p x = jumpF_polyL q p x" proof - have "jumpF_polyR (r+q) p x = jumpF_polyR q p x" "jumpF_polyL (r+q) p x = jumpF_polyL q p x" if "p=0 \ r=0 \ order x p \ order x r" using jumpF_polyR_order_leq jumpF_polyL_order_leq that by auto moreover have "jumpF_polyR (r+q) p x = jumpF_polyR q p x" "jumpF_polyL (r+q) p x = jumpF_polyL q p x" if "p\0" "r\0" "order x p > order x r" proof - define xo where "xo=[:- x, 1:] ^ order x q" have [simp]:"xo\0" unfolding xo_def by simp have xo_q:"order x xo = order x q" unfolding xo_def by (meson order_power_n_n) obtain q' where q:"q = xo * q'" and "\ [:- x, 1:] dvd q'" using order_decomp[OF \q\0\,of x] unfolding xo_def by auto from this(2) have "poly q' x\0" using poly_eq_0_iff_dvd by blast define p' r' where "p'= p div xo" and "r' = r div xo" have p:"p = xo * p'" proof - have "order x q < order x p" using assms(1) less_trans that(3) by blast then have "xo dvd p" unfolding xo_def by (metis less_or_eq_imp_le order_divides) then show ?thesis by (simp add: p'_def) qed have r:"r = xo * r'" proof - have "xo dvd r" unfolding xo_def by (meson assms(1) less_or_eq_imp_le order_divides) then show ?thesis by (simp add: r'_def) qed have "poly r' x=0" proof - have "order x r = order x xo + order x r'" unfolding r using \r \ 0\ r order_mult by blast with xo_q have "order x r' = order x r - order x q" by auto then have "order x r' >0" using \order x r < order x p\ assms(1) by linarith then show "poly r' x=0" using order_root by blast qed have "poly p' x=0" proof - have "order x p = order x xo + order x p'" unfolding p using \p \ 0\ p order_mult by blast with xo_q have "order x p' = order x p - order x q" by auto then have "order x p' >0" using \order x r < order x p\ assms(1) by linarith then show "poly p' x=0" using order_root by blast qed have "jumpF_polyL (r+q) p x = jumpF_polyL (xo * (r'+q')) (xo*p') x" unfolding p q r by (simp add:algebra_simps) also have "... = jumpF_polyL (r'+q') p' x" by (rule jumpF_polyL_mult_cancel) simp also have "... = (if even (order x p') = (sign_r_pos p' x = (0 < poly (r' + q') x)) then 1 / 2 else - 1 / 2)" proof - have "poly (r' + q') x \ 0" using \poly q' x\0\ \poly r' x = 0\ by auto then show ?thesis apply (subst jumpF_polyL_coprime') subgoal by simp subgoal by (smt (z3) \p \ 0\ \poly p' x = 0\ mult.commute mult_zero_left p poly_0) done qed also have "... = (if even (order x p') = (sign_r_pos p' x = (0 < poly q' x)) then 1 / 2 else - 1 / 2)" using \poly r' x=0\ by auto also have "... = jumpF_polyL q' p' x" apply (subst jumpF_polyL_coprime') subgoal using \poly q' x \ 0\ by blast subgoal using \p \ 0\ \poly p' x = 0\ assms(2) p q by simp done also have "... = jumpF_polyL q p x" unfolding p q by (subst jumpF_polyL_mult_cancel) simp_all finally show "jumpF_polyL (r+q) p x = jumpF_polyL q p x" . have "jumpF_polyR (r+q) p x = jumpF_polyR (xo * (r'+q')) (xo*p') x" unfolding p q r by (simp add:algebra_simps) also have "... = jumpF_polyR (r'+q') p' x" by (rule jumpF_polyR_mult_cancel) simp also have "... = (if sign_r_pos p' x = (0 < poly (r' + q') x) then 1 / 2 else - 1 / 2)" proof - have "poly (r' + q') x \ 0" using \poly q' x\0\ \poly r' x = 0\ by auto then show ?thesis apply (subst jumpF_polyR_coprime') subgoal by simp subgoal by (smt (z3) \p \ 0\ \poly p' x = 0\ mult.commute mult_zero_left p poly_0) done qed also have "... = (if sign_r_pos p' x = (0 < poly q' x) then 1 / 2 else - 1 / 2)" using \poly r' x=0\ by auto also have "... = jumpF_polyR q' p' x" apply (subst jumpF_polyR_coprime') subgoal using \poly q' x \ 0\ by blast subgoal using \p \ 0\ \poly p' x = 0\ assms(2) p q by force done also have "... = jumpF_polyR q p x" unfolding p q by (subst jumpF_polyR_mult_cancel) simp_all finally show "jumpF_polyR (r+q) p x = jumpF_polyR q p x" . qed ultimately show "jumpF_polyR (r+q) p x = jumpF_polyR q p x" "jumpF_polyL (r+q) p x = jumpF_polyL q p x" by force + qed lemma jumpF_poly_top_0[simp]: "jumpF_poly_top 0 p = 0" "jumpF_poly_top q 0 = 0" unfolding jumpF_poly_top_def by auto lemma jumpF_poly_bot_0[simp]: "jumpF_poly_bot 0 p = 0" "jumpF_poly_bot q 0 = 0" unfolding jumpF_poly_bot_def by auto lemma jumpF_poly_top_code: "jumpF_poly_top q p = (if p\0 \ q\0 \ degree q>degree p then if sgn_pos_inf q * sgn_pos_inf p > 0 then 1/2 else -1/2 else 0)" proof (cases "p\0 \ q\0 \ degree q>degree p") case True have ?thesis when "sgn_pos_inf q * sgn_pos_inf p > 0" proof - have "LIM x at_top. poly q x / poly p x :> at_top" using poly_divide_filterlim_at_top[of p q] True that by auto then have "jumpF (\x. poly q x / poly p x) at_top = 1/2" unfolding jumpF_def by auto then show ?thesis unfolding jumpF_poly_top_def using that True by auto qed moreover have ?thesis when "\ sgn_pos_inf q * sgn_pos_inf p > 0" proof - have "LIM x at_top. poly q x / poly p x :> at_bot" using poly_divide_filterlim_at_top[of p q] True that by auto then have "jumpF (\x. poly q x / poly p x) at_top = - 1/2" unfolding jumpF_def by auto then show ?thesis unfolding jumpF_poly_top_def using that True by auto qed ultimately show ?thesis by auto next case False define P where "P= (\ (LIM x at_top. poly q x / poly p x :> at_bot) \ \ (LIM x at_top. poly q x / poly p x :> at_top))" have P when "p=0 \ q=0" unfolding P_def using that by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds) moreover have P when "p\0" "q\0" "degree p> degree q" proof - have "LIM x at_top. poly q x / poly p x :> at 0" using poly_divide_filterlim_at_top[OF that(1,2)] that(3) by auto then show ?thesis unfolding P_def by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds simp:filterlim_at) qed moreover have P when "p\0" "q\0" "degree p = degree q" proof - have "((\x. poly q x / poly p x) \ lead_coeff q / lead_coeff p) at_top" using poly_divide_filterlim_at_top[OF that(1,2)] using that by auto then show ?thesis unfolding P_def by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds) qed ultimately have P using False by fastforce then have "jumpF (\x. poly q x / poly p x) at_top = 0" unfolding jumpF_def P_def by auto then show ?thesis unfolding jumpF_poly_top_def using False by presburger qed lemma jumpF_poly_bot_code: "jumpF_poly_bot q p = (if p\0 \ q\0 \ degree q>degree p then if sgn_neg_inf q * sgn_neg_inf p > 0 then 1/2 else -1/2 else 0)" proof (cases "p\0 \ q\0 \ degree q>degree p") case True have ?thesis when "sgn_neg_inf q * sgn_neg_inf p > 0" proof - have "LIM x at_bot. poly q x / poly p x :> at_top" using poly_divide_filterlim_at_bot[of p q] True that by auto then have "jumpF (\x. poly q x / poly p x) at_bot = 1/2" unfolding jumpF_def by auto then show ?thesis unfolding jumpF_poly_bot_def using that True by auto qed moreover have ?thesis when "\ sgn_neg_inf q * sgn_neg_inf p > 0" proof - have "LIM x at_bot. poly q x / poly p x :> at_bot" using poly_divide_filterlim_at_bot[of p q] True that by auto then have "jumpF (\x. poly q x / poly p x) at_bot = - 1/2" unfolding jumpF_def by auto then show ?thesis unfolding jumpF_poly_bot_def using that True by auto qed ultimately show ?thesis by auto next case False define P where "P= (\ (LIM x at_bot. poly q x / poly p x :> at_bot) \ \ (LIM x at_bot. poly q x / poly p x :> at_top))" have P when "p=0 \ q=0" unfolding P_def using that by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds) moreover have P when "p\0" "q\0" "degree p> degree q" proof - have "LIM x at_bot. poly q x / poly p x :> at 0" using poly_divide_filterlim_at_bot[OF that(1,2)] that(3) by auto then show ?thesis unfolding P_def by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds simp:filterlim_at) qed moreover have P when "p\0" "q\0" "degree p = degree q" proof - have "((\x. poly q x / poly p x) \ lead_coeff q / lead_coeff p) at_bot" using poly_divide_filterlim_at_bot[OF that(1,2)] using that by auto then show ?thesis unfolding P_def by (auto elim!:filterlim_at_bot_nhds filterlim_at_top_nhds) qed ultimately have P using False by fastforce then have "jumpF (\x. poly q x / poly p x) at_bot = 0" unfolding jumpF_def P_def by auto then show ?thesis unfolding jumpF_poly_bot_def using False by presburger qed lemma jump_poly_jumpF_poly: shows "jump_poly q p x = jumpF_polyR q p x - jumpF_polyL q p x" proof (cases "p=0 \ q=0") case True then show ?thesis by auto next case False have *:"jump_poly q p x = jumpF_polyR q p x - jumpF_polyL q p x" if "coprime q p" for q p proof (cases "p=0 \ q=0 \ poly p x\0") case True moreover have ?thesis if "p=0 \ q=0" using that by auto moreover have ?thesis if "poly p x\0" by (simp add: jumpF_poly_noroot(1) jumpF_poly_noroot(2) jump_poly_not_root that) ultimately show ?thesis by blast next case False then have " p \ 0" "q \ 0" "poly p x = 0" by auto have "jump_poly q p x = jump (\x. poly q x / poly p x) x" using jump_jump_poly by simp also have "real_of_int ... = jumpF (\x. poly q x / poly p x) (at_right x) - jumpF (\x. poly q x / poly p x) (at_left x)" proof (rule jump_jumpF) have "poly q x\0" by (meson False coprime_poly_0 that) then show "isCont (inverse \ (\x. poly q x / poly p x)) x" unfolding comp_def by simp define l where "l = sgnx (\x. poly q x / poly p x) (at_left x)" define r where "r = sgnx (\x. poly q x / poly p x) (at_right x)" show "((\x. poly q x / poly p x) has_sgnx l) (at_left x)" unfolding l_def by (auto intro!:sgnx_intros sgnx_able_sgnx) show "((\x. poly q x / poly p x) has_sgnx r) (at_right x)" unfolding r_def by (auto intro!:sgnx_intros sgnx_able_sgnx) show "l\0" unfolding l_def apply (subst sgnx_divide) using poly_sgnx_values[OF \p\0\, of x] poly_sgnx_values[OF \q\0\, of x] by auto show "r\0" unfolding r_def apply (subst sgnx_divide) using poly_sgnx_values[OF \p\0\, of x] poly_sgnx_values[OF \q\0\, of x] by auto qed also have "... = jumpF_polyR q p x - jumpF_polyL q p x" unfolding jumpF_polyR_def jumpF_polyL_def by simp finally show ?thesis . qed obtain p' q' g where pq:"p=g*p'" "q=g*q'" and "coprime q' p'" "g=gcd p q" using gcd_coprime_exists[of p q] by (metis False coprime_commute gcd_coprime_exists gcd_eq_0_iff mult.commute) then have "g\0" using False mult_zero_left by blast then have "jump_poly q p x = jump_poly q' p' x" unfolding pq using jump_poly_mult by auto also have "... = jumpF_polyR q' p' x - jumpF_polyL q' p' x" using *[OF \coprime q' p'\] . also have "... = jumpF_polyR q p x - jumpF_polyL q p x" unfolding pq using \g\0\ jumpF_polyL_mult_cancel jumpF_polyR_mult_cancel by auto finally show ?thesis . qed subsection \The extended Cauchy index on polynomials\ definition cindex_polyE:: "real \ real \ real poly \ real poly \ real" where "cindex_polyE a b q p = jumpF_polyR q p a + cindex_poly a b q p - jumpF_polyL q p b" definition cindex_poly_ubd::"real poly \ real poly \ int" where "cindex_poly_ubd q p = (THE l. (\\<^sub>F r in at_top. cindexE (-r) r (\x. poly q x/poly p x) = of_int l))" lemma cindex_polyE_0[simp]: "cindex_polyE a b 0 p = 0" "cindex_polyE a b q 0 = 0" unfolding cindex_polyE_def by auto lemma cindex_polyE_mult_cancel: fixes p q p'::"real poly" assumes "p'\ 0" shows "cindex_polyE a b (p' * q ) (p' * p) = cindex_polyE a b q p" unfolding cindex_polyE_def using cindex_poly_mult[OF \p'\0\] jumpF_polyL_mult_cancel[OF \p'\0\] jumpF_polyR_mult_cancel[OF \p'\0\] by simp lemma cindexE_eq_cindex_polyE: assumes "ax. poly q x/poly p x) = cindex_polyE a b q p" proof (cases "p=0 \ q=0") case True then show ?thesis by (auto simp add: cindexE_constI) next case False then have "p\0" "q\0" by auto define g where "g=gcd p q" define p' q' where "p'=p div g" and "q' = q div g" define f' where "f'=(\x. poly q' x / poly p' x)" have "g\0" using False g_def by auto have pq_f:"p=g*p'" "q=g*q'" and "coprime p' q'" unfolding g_def p'_def q'_def apply simp_all using False div_gcd_coprime by blast have "cindexE a b (\x. poly q x/poly p x) = cindexE a b (\x. poly q' x/poly p' x)" proof - define f where "f=(\x. poly q x / poly p x)" define f' where "f'=(\x. poly q' x / poly p' x)" have "jumpF f (at_right x) = jumpF f' (at_right x)" for x proof (rule jumpF_cong) obtain ub where "x < ub" "\z. x < z \ z \ ub \ poly g z \ 0" using next_non_root_interval[OF \g\0\,of x] by auto then show "\\<^sub>F x in at_right x. f x = f' x" unfolding eventually_at_right f_def f'_def pq_f apply (intro exI[where x=ub]) by auto qed simp moreover have "jumpF f (at_left x) = jumpF f' (at_left x)" for x proof (rule jumpF_cong) obtain lb where "lb < x" "\z. lb \ z \ z < x \ poly g z \ 0 " using last_non_root_interval[OF \g\0\,of x] by auto then show "\\<^sub>F x in at_left x. f x = f' x" unfolding eventually_at_left f_def f'_def pq_f apply (intro exI[where x=lb]) by auto qed simp ultimately show ?thesis unfolding cindexE_def apply (fold f_def f'_def) by auto qed also have "... = jumpF f' (at_right a) + real_of_int (cindex a b f') - jumpF f' (at_left b)" unfolding f'_def apply (rule cindex_eq_cindexE_divide) subgoal using \a . subgoal proof - have "finite (proots (q'*p'))" using False poly_roots_finite pq_f(1) pq_f(2) by auto then show "finite {x. (poly q' x = 0 \ poly p' x = 0) \ a \ x \ x \ b}" by (elim rev_finite_subset) auto qed subgoal using \coprime p' q'\ poly_gcd_0_iff by force subgoal by (auto intro:continuous_intros) subgoal by (auto intro:continuous_intros) done also have "... = cindex_polyE a b q' p'" using cindex_eq_cindex_poly unfolding cindex_polyE_def jumpF_polyR_def jumpF_polyL_def f'_def by auto also have "... = cindex_polyE a b q p" using cindex_polyE_mult_cancel[OF \g\0\] unfolding pq_f by auto finally show ?thesis . qed lemma cindex_polyE_cross: fixes p::"real poly" and a b::real assumes "a0" and noroot:"{x. a< x\ x< b \ poly p x=0 } = {}" proof - have "cindex_polyE a b 1 p = jumpF_polyR 1 p a - jumpF_polyL 1 p b" proof - have "cindex_poly a b 1 p = 0" unfolding cindex_poly_def apply (rule sum.neutral) using that by auto then show ?thesis unfolding cindex_polyE_def by auto qed also have "... = cross_alt 1 p a b / 2" proof - define f where "f = (\x. 1 / poly p x)" define ja where "ja = jumpF f (at_right a)" define jb where "jb = jumpF f (at_left b)" define right where "right = (\R. R ja (0::real) \ (continuous (at_right a) f \ R (poly p a) 0))" define left where "left = (\R. R jb (0::real) \ (continuous (at_left b) f \ R (poly p b) 0))" note ja_alt=jumpF_polyR_coprime[of p 1 a,unfolded jumpF_polyR_def,simplified,folded f_def ja_def] note jb_alt=jumpF_polyL_coprime[of p 1 b,unfolded jumpF_polyL_def,simplified,folded f_def jb_def] have [simp]:"0 < ja \ jumpF_polyR 1 p a = 1/2" "0 > ja \ jumpF_polyR 1 p a = -1/2" "0 < jb \ jumpF_polyL 1 p b = 1/2" "0 > jb \ jumpF_polyL 1 p b = -1/2" unfolding ja_def jb_def jumpF_polyR_def jumpF_polyL_def f_def jumpF_def by auto have [simp]: "poly p a \0 \ continuous (at_right a) f" "poly p b \0 \ continuous (at_left b) f" unfolding f_def by (auto intro!: continuous_intros ) have not_right_left: False when "(right greater \ left less \ right less \ left greater)" proof - have [simp]: "f a > 0 \ poly p a > 0" "f a < 0 \ poly p a < 0" "f b > 0 \ poly p b > 0" "f b < 0 \ poly p b < 0" unfolding f_def by auto have "continuous_on {a<..x>a. x < b \ f x = 0" apply (elim jumpF_IVT[OF \a,of f]) using that unfolding right_def left_def by (fold ja_def jb_def,auto) then show False using noroot using f_def by auto qed have ?thesis when "poly p a>0 \ poly p b>0 \ poly p a<0 \ poly p b<0" using that jumpF_poly_noroot unfolding cross_alt_def psign_diff_def by auto moreover have False when "poly p a>0 \ poly p b<0 \ poly p a<0 \ poly p b>0" apply (rule not_right_left) unfolding right_def left_def using that by auto moreover have ?thesis when "poly p a=0" "poly p b>0 \ poly p b <0" proof - have "ja>0 \ ja < 0" using ja_alt \p\0\ \poly p a=0\ by argo moreover have False when "ja > 0 \ poly p b<0 \ ja < 0 \ poly p b>0" apply (rule not_right_left) unfolding right_def left_def using that by fastforce moreover have ?thesis when "ja >0 \ poly p b>0 \ ja < 0 \ poly p b<0" using that jumpF_poly_noroot \poly p a=0\ unfolding cross_alt_def psign_diff_def by auto ultimately show ?thesis using that jumpF_poly_noroot unfolding cross_alt_def by auto qed moreover have ?thesis when "poly p b=0" "poly p a>0 \ poly p a <0" proof - have "jb>0 \ jb < 0" using jb_alt \p\0\ \poly p b=0\ by argo moreover have False when "jb > 0 \ poly p a<0 \ jb < 0 \ poly p a>0" apply (rule not_right_left) unfolding right_def left_def using that by fastforce moreover have ?thesis when "jb >0 \ poly p a>0 \ jb < 0 \ poly p a<0" using that jumpF_poly_noroot \poly p b=0\ unfolding cross_alt_def psign_diff_def by auto ultimately show ?thesis using that jumpF_poly_noroot unfolding cross_alt_def by auto qed moreover have ?thesis when "poly p a=0" "poly p b=0" proof - have "jb>0 \ jb < 0" using jb_alt \p\0\ \poly p b=0\ by argo moreover have "ja>0 \ ja < 0" using ja_alt \p\0\ \poly p a=0\ by argo moreover have False when "ja>0 \ jb<0 \ ja<0 \ jb>0" apply (rule not_right_left) unfolding right_def left_def using that by fastforce moreover have ?thesis when "ja>0 \ jb>0 \ ja<0 \ jb<0" using that jumpF_poly_noroot \poly p b=0\ \poly p a=0\ unfolding cross_alt_def psign_diff_def by auto ultimately show ?thesis by blast qed ultimately show ?thesis by argo qed finally show ?thesis . qed moreover have ?case when "p\0" and no_empty:"{x. a< x\ x< b \ poly p x=0 } \ {}" proof - define roots where "roots\{x. a< x\ x< b \ poly p x=0 }" have "finite roots" unfolding roots_def using poly_roots_finite[OF \p\0\] by auto define max_r where "max_r\Max roots" hence "poly p max_r=0" and "afinite roots\] no_empty unfolding roots_def by auto define max_rp where "max_rp\[:-max_r,1:]^order max_r p" then obtain p' where p'_def:"p=p'*max_rp" and "\ [:-max_r,1:] dvd p'" by (metis \p\0\ mult.commute order_decomp) hence "p'\0" and "max_rp\0" and max_r_nz:"poly p' max_r\0"(*and "poly p' a\0" and "poly p' b\0" *) (*and "poly max_rp a\0" and "poly max_rp b\0"*) using \p\0\ by (auto simp add: dvd_iff_poly_eq_0) define max_r_sign where "max_r_sign\if odd(order max_r p) then -1 else 1::int" define roots' where "roots'\{x. a< x\ x< b \ poly p' x=0}" have "cindex_polyE a b 1 p = jumpF_polyR 1 p a + (\x\roots. jump_poly 1 p x) - jumpF_polyL 1 p b" unfolding cindex_polyE_def cindex_poly_def roots_def by (simp,meson) also have "... = max_r_sign * cindex_poly a b 1 p' + jump_poly 1 p max_r + max_r_sign * jumpF_polyR 1 p' a - jumpF_polyL 1 p' b" proof - have "(\x\roots. jump_poly 1 p x) = max_r_sign * cindex_poly a b 1 p' + jump_poly 1 p max_r" proof - have "(\x\roots. jump_poly 1 p x)= (\x\roots'. jump_poly 1 p x)+ jump_poly 1 p max_r" proof - have "roots = insert max_r roots'" unfolding roots_def roots'_def p'_def using \poly p max_r=0\ \a \max_r \p\0\ order_root apply (subst max_rp_def) by auto moreover have "finite roots'" unfolding roots'_def using poly_roots_finite[OF \p'\0\] by auto moreover have "max_r \ roots'" unfolding roots'_def using max_r_nz by auto ultimately show ?thesis using sum.insert[of roots' max_r] by auto qed moreover have "(\x\roots'. jump_poly 1 p x) = max_r_sign * cindex_poly a b 1 p'" proof - have "(\x\roots'. jump_poly 1 p x) = (\x\roots'. max_r_sign * jump_poly 1 p' x)" proof (rule sum.cong,rule refl) fix x assume "x \ roots'" hence "x\max_r" using max_r_nz unfolding roots'_def by auto hence "poly max_rp x\0" using poly_power_n_eq unfolding max_rp_def by auto hence "order x max_rp=0" by (metis order_root) moreover have "jump_poly 1 max_rp x=0" using \poly max_rp x\0\ by (metis jump_poly_not_root) moreover have "x\roots" using \x \ roots'\ unfolding roots_def roots'_def p'_def by auto hence "xfinite roots\,of x] \x\max_r\ by (fold max_r_def,auto) hence "sign (poly max_rp x) = max_r_sign" using \poly max_rp x \ 0\ unfolding max_r_sign_def max_rp_def sign_def by (subst poly_power,simp add:linorder_class.not_less zero_less_power_eq) ultimately show "jump_poly 1 p x = max_r_sign * jump_poly 1 p' x" using jump_poly_1_mult[of p' x max_rp] unfolding p'_def by (simp add: \poly max_rp x \ 0\) qed also have "... = max_r_sign * (\x\roots'. jump_poly 1 p' x)" by (simp add: sum_distrib_left) also have "... = max_r_sign * cindex_poly a b 1 p'" unfolding cindex_poly_def roots'_def by meson finally show ?thesis . qed ultimately show ?thesis by simp qed moreover have "jumpF_polyR 1 p a = max_r_sign * jumpF_polyR 1 p' a" proof - define f where "f = (\x. 1 / poly max_rp x)" define g where "g = (\x. 1 / poly p' x)" have "jumpF_polyR 1 p a = jumpF (\x. f x * g x) (at_right a)" unfolding jumpF_polyR_def f_def g_def p'_def by (auto simp add:field_simps) also have "... = sgn (f a) * jumpF g (at_right a)" proof (rule jumpF_times) have [simp]: "poly max_rp a \0" unfolding max_rp_def using \max_r>a\ by auto show "(f \ f a) (at_right a)" "f a \ 0" unfolding f_def by (auto intro:tendsto_intros) qed auto also have "... = max_r_sign * jumpF_polyR 1 p' a" proof - have "sgn (f a) = max_r_sign" unfolding max_r_sign_def f_def max_rp_def using \a by (auto simp add:sgn_power) then show ?thesis unfolding jumpF_polyR_def g_def by auto qed finally show ?thesis . qed moreover have "jumpF_polyL 1 p b = jumpF_polyL 1 p' b" proof - define f where "f = (\x. 1 / poly max_rp x)" define g where "g = (\x. 1 / poly p' x)" have "jumpF_polyL 1 p b = jumpF (\x. f x * g x) (at_left b)" unfolding jumpF_polyL_def f_def g_def p'_def by (auto simp add:field_simps) also have "... = sgn (f b) * jumpF g (at_left b)" proof (rule jumpF_times) have [simp]: "poly max_rp b \0" unfolding max_rp_def using \max_r by auto show "(f \ f b) (at_left b)" "f b \ 0" unfolding f_def by (auto intro:tendsto_intros) qed auto also have "... = jumpF_polyL 1 p' b" proof - have "sgn (f b) = 1" unfolding max_r_sign_def f_def max_rp_def using \b>max_r\ by (auto simp add:sgn_power) then show ?thesis unfolding jumpF_polyL_def g_def by auto qed finally show ?thesis . qed ultimately show ?thesis by auto qed also have "... = max_r_sign * cindex_polyE a b 1 p' + jump_poly 1 p max_r + (max_r_sign - 1) * jumpF_polyL 1 p' b" unfolding cindex_polyE_def roots'_def by (auto simp add:algebra_simps) also have "... = max_r_sign * cross_alt 1 p' a b / 2 + jump_poly 1 p max_r + (max_r_sign - 1) * jumpF_polyL 1 p' b" proof - have "degree max_rp>0" unfolding max_rp_def degree_linear_power using \poly p max_r=0\ order_root \p\0\ by blast then have "degree p'p'\0\ \max_rp\0\] by auto from induct[rule_format, OF this] have "cindex_polyE a b 1 p' = real_of_int (cross_alt 1 p' a b) / 2" by auto then show ?thesis by auto qed also have "... = real_of_int (cross_alt 1 p a b) / 2" proof - have sjump_p:"jump_poly 1 p max_r = (if odd (order max_r p) then sign (poly p' max_r) else 0)" proof - note max_r_nz moreover then have "poly max_rp max_r=0" using \poly p max_r = 0\ p'_def by auto ultimately have "jump_poly 1 p max_r = sign (poly p' max_r) * jump_poly 1 max_rp max_r" unfolding p'_def using jump_poly_1_mult[of p' max_r max_rp] by auto also have "... = (if odd (order max_r max_rp) then sign (poly p' max_r) else 0)" proof - have "sign_r_pos max_rp max_r" unfolding max_rp_def using sign_r_pos_power by auto then show ?thesis using \max_rp\0\ unfolding jump_poly_def by auto qed also have "... = (if odd (order max_r p) then sign (poly p' max_r) else 0)" proof - have "order max_r p'=0" by (simp add: \poly p' max_r \ 0\ order_0I) then have "order max_r max_rp = order max_r p" unfolding p'_def using \p'\0\ \max_rp\0\ apply (subst order_mult) by auto then show ?thesis by auto qed finally show ?thesis . qed have ?thesis when "even (order max_r p)" proof - - have "sign (poly p x) = sign (poly p' x)" when "x\max_r" for x + have "sign (poly p x) = (sign (poly p' x)::int)" when "x\max_r" for x proof - - have "sign (poly max_rp x) = 1" + have "sign (poly max_rp x) = (1::int)" unfolding max_rp_def using \even (order max_r p)\ that apply (simp add:sign_power ) by (simp add: Sturm_Tarski.sign_def) then show ?thesis unfolding p'_def by (simp add:sign_times) qed from this[of a] this[of b] \a \max_r have "cross_alt 1 p' a b = cross_alt 1 p a b" unfolding cross_alt_def psign_diff_def by auto then show ?thesis using that unfolding max_r_sign_def sjump_p by auto qed moreover have ?thesis when "odd (order max_r p)" proof - let ?thesis2 = "sign (poly p' max_r) * 2 - cross_alt 1 p' a b - 4 * jumpF_polyL 1 p' b = cross_alt 1 p a b" have ?thesis2 when "poly p' b=0" proof - have "jumpF_polyL 1 p' b = 1/2 \ jumpF_polyL 1 p' b=-1/2" using jumpF_polyL_coprime[of p' 1 b,simplified] \p'\0\ \poly p' b=0\ by auto moreover have "poly p' max_r>0 \ poly p' max_r<0" using max_r_nz by auto moreover have False when "poly p' max_r>0 \ jumpF_polyL 1 p' b=-1/2 \ poly p' max_r<0 \ jumpF_polyL 1 p' b=1/2" proof - define f where "f= (\x. 1/ poly p' x)" have noroots:"poly p' x\0" when "x\{max_r<.. poly p' x \ 0" then have "poly p x =0" unfolding p'_def by auto then have "x\roots" unfolding roots_def using that \a by auto then have "x\max_r" using Max_ge[OF \finite roots\] unfolding max_r_def by auto moreover have "x>max_r" using that by auto ultimately show False by auto qed have "continuous_on {max_r<..0 \ jumpF f (at_left b)<0 \ f max_r<0 \ jumpF f (at_left b)>0" using that unfolding f_def jumpF_polyL_def by auto ultimately have "\x>max_r. x < b \ f x = 0" apply (intro jumpF_IVT[OF \max_r]) by auto then show False using noroots unfolding f_def by auto qed moreover have ?thesis when "poly p' max_r>0 \ jumpF_polyL 1 p' b=1/2 \ poly p' max_r<0 \ jumpF_polyL 1 p' b=-1/2" proof - have "poly max_rp a < 0" "poly max_rp b>0" unfolding max_rp_def using \odd (order max_r p)\ \a \max_r by (simp_all add:zero_less_power_eq) then have "cross_alt 1 p a b = - cross_alt 1 p' a b" unfolding cross_alt_def p'_def using \poly p' b=0\ apply (simp add:sign_times) by (auto simp add: Sturm_Tarski.sign_def psign_diff_def zero_less_mult_iff) with that show ?thesis by auto qed ultimately show ?thesis by blast qed moreover have ?thesis2 when "poly p' b\0" proof - have [simp]:"jumpF_polyL 1 p' b = 0" using jumpF_polyL_coprime[of p' 1 b,simplified] \poly p' b\0\ by auto have [simp]:"poly max_rp a < 0" "poly max_rp b>0" unfolding max_rp_def using \odd (order max_r p)\ \a \max_r by (simp_all add:zero_less_power_eq) have "poly p' b>0 \ poly p' b<0" using \poly p' b\0\ by auto moreover have "poly p' max_r>0 \ poly p' max_r<0" using max_r_nz by auto moreover have ?thesis when "poly p' b>0 \ poly p' max_r>0 " using that unfolding cross_alt_def p'_def psign_diff_def apply (simp add:sign_times) by (simp add: Sturm_Tarski.sign_def) moreover have ?thesis when "poly p' b<0 \ poly p' max_r<0" using that unfolding cross_alt_def p'_def psign_diff_def apply (simp add:sign_times) by (simp add: Sturm_Tarski.sign_def) moreover have False when "poly p' b>0 \ poly p' max_r<0 \ poly p' b<0 \ poly p' max_r>0" proof - have "\x>max_r. x < b \ poly p' x = 0" apply (rule poly_IVT[OF \max_r,of p']) using that mult_less_0_iff by blast then obtain x where "max_rroots" using \a unfolding roots_def by auto then have "x\max_r" unfolding max_r_def using Max_ge[OF \finite roots\] by auto then show False using \max_r by auto qed ultimately show ?thesis by blast qed ultimately have ?thesis2 by auto then show ?thesis unfolding max_r_sign_def sjump_p using that by simp qed ultimately show ?thesis by auto qed finally show ?thesis . qed ultimately show ?case by fast qed lemma cindex_polyE_inverse_add: fixes p q::"real poly" assumes cp:"coprime p q" shows "cindex_polyE a b q p + cindex_polyE a b p q=cindex_polyE a b 1 (q*p)" unfolding cindex_polyE_def using cindex_poly_inverse_add[OF cp,symmetric] jumpF_polyR_inverse_add[OF cp,symmetric] jumpF_polyL_inverse_add[OF cp,symmetric] by auto lemma cindex_polyE_inverse_add_cross: fixes p q::"real poly" assumes "a < b" "coprime p q" shows "cindex_polyE a b q p + cindex_polyE a b p q = cross_alt p q a b / 2" apply (subst cindex_polyE_inverse_add[OF \coprime p q\]) apply (subst cindex_polyE_cross[OF \a]) apply (subst mult.commute) apply (subst (2) cross_alt_clear) by simp lemma cindex_polyE_inverse_add_cross': fixes p q::"real poly" assumes "a < b" "poly p a\0 \ poly q a\0" "poly p b\0 \ poly q b\0" shows "cindex_polyE a b q p + cindex_polyE a b p q = cross_alt p q a b / 2" proof - define g1 where "g1 = gcd p q" obtain p' q' where pq:"p=g1*p'" "q=g1*q'" and "coprime p' q'" unfolding g1_def by (metis assms(2) coprime_commute div_gcd_coprime dvd_mult_div_cancel gcd_dvd1 gcd_dvd2 order_root) have [simp]:"g1\0" unfolding g1_def using assms(2) by force have "cindex_polyE a b q' p' + cindex_polyE a b p' q' = (cross_alt p' q' a b) / 2" using cindex_polyE_inverse_add_cross[OF \a \coprime p' q'\] . moreover have "cindex_polyE a b p' q' = cindex_polyE a b p q " unfolding pq apply (subst cindex_polyE_mult_cancel) by simp_all moreover have "cindex_polyE a b q' p' = cindex_polyE a b q p" unfolding pq apply (subst cindex_polyE_mult_cancel) by simp_all moreover have "cross_alt p' q' a b = cross_alt p q a b" unfolding pq apply (subst cross_alt_cancel) subgoal using assms(2) g1_def poly_gcd_0_iff by blast subgoal using assms(3) g1_def poly_gcd_0_iff by blast by simp ultimately show ?thesis by auto qed lemma cindex_polyE_smult_1: fixes p q::"real poly" and c::real shows "cindex_polyE a b (smult c q) p = (sgn c) * cindex_polyE a b q p" - unfolding cindex_polyE_def jumpF_polyL_smult_1 jumpF_polyR_smult_1 cindex_poly_smult_1 - by (auto simp add:sgn_sign_eq[symmetric] algebra_simps) +proof - + have "real_of_int (sign c) = sgn c" + by (simp add: sgn_if) + then show ?thesis + unfolding cindex_polyE_def jumpF_polyL_smult_1 jumpF_polyR_smult_1 cindex_poly_smult_1 + by (auto simp add: algebra_simps) +qed lemma cindex_polyE_smult_2: fixes p q::"real poly" and c::real shows "cindex_polyE a b q (smult c p) = (sgn c) * cindex_polyE a b q p" proof (cases "c=0") case True then show ?thesis by simp next case False then have "cindex_polyE a b q (smult c p) = cindex_polyE a b ([:1/c:]*q) ([:1/c:]*(smult c p))" apply (subst cindex_polyE_mult_cancel) by simp_all also have "... = cindex_polyE a b (smult (1/c) q) p" by simp also have "... = (sgn (1/c)) * cindex_polyE a b q p" using cindex_polyE_smult_1 by simp also have "... = (sgn c) * cindex_polyE a b q p" by simp finally show ?thesis . qed lemma cindex_polyE_mod: fixes p q::"real poly" shows "cindex_polyE a b q p = cindex_polyE a b (q mod p) p" unfolding cindex_polyE_def apply (subst cindex_poly_mod) apply (subst jumpF_polyR_mod) apply (subst jumpF_polyL_mod) by simp lemma cindex_polyE_rec: fixes p q::"real poly" assumes "a < b" "coprime p q" shows "cindex_polyE a b q p = cross_alt q p a b/2 + cindex_polyE a b (- (p mod q)) q" proof - note cindex_polyE_inverse_add_cross[OF assms] moreover have "cindex_polyE a b (- (p mod q)) q = - cindex_polyE a b p q" using cindex_polyE_mod cindex_polyE_smult_1[of a b "-1"] by auto ultimately show ?thesis by (auto simp add:field_simps cross_alt_poly_commute) qed lemma cindex_polyE_changes_alt_itv_mods: assumes "acoprime p q\ proof (induct "smods p q" arbitrary:p q) case Nil then have "p=0" by (metis smods_nil_eq) then show ?case by (simp add:changes_alt_itv_smods_def changes_alt_poly_at_def) next case (Cons x xs) then have "p\0" by auto have ?case when "q=0" using that by (simp add:changes_alt_itv_smods_def changes_alt_poly_at_def) moreover have ?case when "q\0" proof - define r where "r\- (p mod q)" obtain ps where ps:"smods p q=p#q#ps" "smods q r=q#ps" and "xs=q#ps" unfolding r_def using \q\0\ \p\0\ \x # xs = smods p q\ by (metis list.inject smods.simps) from Cons.prems \q \ 0\ have "coprime q r" by (simp add: r_def ac_simps) then have "cindex_polyE a b r q = real_of_int (changes_alt_itv_smods a b q r) / 2" apply (rule_tac Cons.hyps(1)) using ps \xs=q#ps\ by simp_all moreover have "changes_alt_itv_smods a b p q = cross_alt p q a b + changes_alt_itv_smods a b q r" using changes_alt_itv_smods_rec[OF \a \coprime p q\,folded r_def] . moreover have "cindex_polyE a b q p = real_of_int (cross_alt q p a b) / 2 + cindex_polyE a b r q" using cindex_polyE_rec[OF \a \coprime p q\,folded r_def] . ultimately show ?case by (auto simp add:field_simps cross_alt_poly_commute) qed ultimately show ?case by blast qed lemma cindex_poly_ubd_eventually: shows "\\<^sub>F r in at_top. cindexE (-r) r (\x. poly q x/poly p x) = of_int (cindex_poly_ubd q p)" proof - define f where "f=(\x. poly q x/poly p x)" obtain R where R_def: "R>0" "proots p \ {-R<..0" proof (cases "p=0") case True then show ?thesis using that[of 1] by auto next case False then have "finite (proots p)" by auto from finite_ball_include[OF this,of 0] obtain r where "r>0" and r_ball:"proots p \ ball 0 r" by auto have "proots p \ {-r<.. proots p" then have "x\ball 0 r" using r_ball by auto then have "abs x {- r<..r>0\ by auto qed then show ?thesis using that[of r] False \r>0\ by auto qed define l where "l=(if p=0 then 0 else cindex_poly (-R) R q p)" define P where "P=(\l. (\\<^sub>F r in at_top. cindexE (-r) r f = of_int l))" have "P l " proof (cases "p=0 ") case True then show ?thesis unfolding P_def f_def l_def using True by (auto intro!: eventuallyI cindexE_constI) next case False have "P l" unfolding P_def proof (rule eventually_at_top_linorderI[of R]) fix r assume "R \ r" then have "cindexE (- r) r f = cindex_polyE (-r) r q p" unfolding f_def using R_def[OF \p\0\] by (auto intro: cindexE_eq_cindex_polyE) also have "... = of_int (cindex_poly (- r) r q p)" proof - have "jumpF_polyR q p (- r) = 0" apply (rule jumpF_poly_noroot) using \R\r\ R_def[OF \p\0\] by auto moreover have "jumpF_polyL q p r = 0" apply (rule jumpF_poly_noroot) using \R\r\ R_def[OF \p\0\] by auto ultimately show ?thesis unfolding cindex_polyE_def by auto qed also have "... = of_int (cindex_poly (- R) R q p)" proof - define rs where "rs={x. poly p x = 0 \ - r < x \ x < r}" define Rs where "Rs={x. poly p x = 0 \ - R < x \ x < R}" have "rs=Rs" using R_def[OF \p\0\] \R\r\ unfolding rs_def Rs_def by force then show ?thesis unfolding cindex_poly_def by (fold rs_def Rs_def,auto) qed also have "... = of_int l" unfolding l_def using False by auto finally show "cindexE (- r) r f = real_of_int l" . qed then show ?thesis unfolding P_def by auto qed moreover have "x=l" when "P x" for x proof - have "\\<^sub>F r in at_top. cindexE (- r) r f = real_of_int x" "\\<^sub>F r in at_top. cindexE (- r) r f = real_of_int l" using \P x\ \P l\ unfolding P_def by auto from eventually_conj[OF this] have "\\<^sub>F r::real in at_top. real_of_int x = real_of_int l" by (elim eventually_mono,auto) then have "real_of_int x = real_of_int l" by auto then show ?thesis by simp qed ultimately have "P (THE x. P x)" using theI[of P l] by blast then show ?thesis unfolding P_def f_def cindex_poly_ubd_def by auto qed lemma cindex_poly_ubd_0: assumes "p=0 \ q=0" shows "cindex_poly_ubd q p = 0" proof - have "\\<^sub>F r in at_top. cindexE (-r) r (\x. poly q x/poly p x) = 0" apply (rule eventuallyI) using assms by (auto intro:cindexE_constI) from eventually_conj[OF this cindex_poly_ubd_eventually[of q p]] have "\\<^sub>F r::real in at_top. (cindex_poly_ubd q p) = (0::int)" apply (elim eventually_mono) by auto then show ?thesis by auto qed lemma cindex_poly_ubd_code: shows "cindex_poly_ubd q p = changes_R_smods p q" proof (cases "p=0") case True then show ?thesis using cindex_poly_ubd_0 by auto next case False define ps where "ps\smods p q" have "p\set ps" using ps_def \p\0\ by auto obtain lb where lb:"\p\set ps. \x. poly p x=0 \ x>lb" and lb_sgn:"\x\lb. \p\set ps. sgn (poly p x) = sgn_neg_inf p" and "lb<0" using root_list_lb[OF no_0_in_smods,of p q,folded ps_def] by auto obtain ub where ub:"\p\set ps. \x. poly p x=0 \ xx\ub. \p\set ps. sgn (poly p x) = sgn_pos_inf p" and "ub>0" using root_list_ub[OF no_0_in_smods,of p q,folded ps_def] by auto define f where "f=(\t. poly q t/ poly p t)" define P where "P=(\l. (\\<^sub>F r in at_top. cindexE (-r) r f = of_int l))" have "P (changes_R_smods p q)" unfolding P_def proof (rule eventually_at_top_linorderI[of "max \lb\ \ub\ + 1"]) fix r assume r_asm:"r\max \lb\ \ub\ + 1" have "cindexE (- r) r f = cindex_polyE (-r) r q p" unfolding f_def using r_asm by (auto intro: cindexE_eq_cindex_polyE) also have "... = of_int (cindex_poly (- r) r q p)" proof - have "jumpF_polyR q p (- r) = 0" apply (rule jumpF_poly_noroot) using r_asm lb[rule_format,OF \p\set ps\,of "-r"] by linarith moreover have "jumpF_polyL q p r = 0" apply (rule jumpF_poly_noroot) using r_asm ub[rule_format,OF \p\set ps\,of "r"] by linarith ultimately show ?thesis unfolding cindex_polyE_def by auto qed also have "... = of_int (changes_itv_smods (- r) r p q)" apply (rule cindex_poly_changes_itv_mods[THEN arg_cong]) using r_asm lb[rule_format,OF \p\set ps\,of "-r"] ub[rule_format,OF \p\set ps\,of "r"] by linarith+ also have "... = of_int (changes_R_smods p q)" proof - have "map (sgn \ (\p. poly p (-r))) ps = map sgn_neg_inf ps" and "map (sgn \ (\p. poly p r)) ps = map sgn_pos_inf ps" using lb_sgn[THEN spec,of "-r",simplified] ub_sgn[THEN spec,of r,simplified] r_asm by auto hence "changes_poly_at ps (-r)=changes_poly_neg_inf ps \ changes_poly_at ps r=changes_poly_pos_inf ps" unfolding changes_poly_neg_inf_def changes_poly_at_def changes_poly_pos_inf_def by (subst (1 3) changes_map_sgn_eq,metis map_map) thus ?thesis unfolding changes_R_smods_def changes_itv_smods_def ps_def by metis qed finally show "cindexE (- r) r f = of_int (changes_R_smods p q)" . qed moreover have "x = changes_R_smods p q" when "P x" for x proof - have "\\<^sub>F r in at_top. cindexE (- r) r f = real_of_int (changes_R_smods p q)" "\\<^sub>F r in at_top. cindexE (- r) r f = real_of_int x" using \P (changes_R_smods p q)\ \P x\ unfolding P_def by auto from eventually_conj[OF this] have "\\<^sub>F (r::real) in at_top. of_int x = of_int (changes_R_smods p q)" by (elim eventually_mono,auto) then have "of_int x = of_int (changes_R_smods p q)" using eventually_const_iff by auto then show ?thesis using of_int_eq_iff by blast qed ultimately have "(THE x. P x) = changes_R_smods p q" using the_equality[of P "changes_R_smods p q"] by blast then show ?thesis unfolding cindex_poly_ubd_def P_def f_def by auto qed lemma cindexE_ubd_poly: "cindexE_ubd (\x. poly q x/poly p x) = cindex_poly_ubd q p" proof (cases "p=0") case True then show ?thesis using cindex_poly_ubd_0 unfolding cindexE_ubd_def by auto next case False define mx mn where "mx = Max {x. poly p x = 0}" and "mn = Min {x. poly p x=0}" define rr where "rr= 1+ (max \mx\ \mn\)" have rr:"-rr < x \ x< rr" when "poly p x = 0 " for x proof - have "finite {x. poly p x = 0}" using \p\0\ poly_roots_finite by blast then have "mn \ x" "x\mx" using Max_ge Min_le that unfolding mn_def mx_def by simp_all then show ?thesis unfolding rr_def by auto qed define f where "f=(\x. poly q x / poly p x)" have "\\<^sub>F r in at_top. cindexE (- r) r f = cindexE_ubd f" proof (rule eventually_at_top_linorderI[of rr]) fix r assume "r\rr" define R1 R2 where "R1={x. jumpF f (at_right x) \ 0 \ - r \ x \ x < r}" and "R2 = {x. jumpF f (at_right x) \ 0}" define L1 L2 where "L1={x. jumpF f (at_left x) \ 0 \ - r < x \ x \ r}" and "L2={x. jumpF f (at_left x) \ 0}" have "R1=R2" proof - have "jumpF f (at_right x) = 0" when "\ (- r \ x \ x < r)" for x proof - have "jumpF f (at_right x) = jumpF_polyR q p x" unfolding f_def jumpF_polyR_def by simp also have "... = 0" apply (rule jumpF_poly_noroot) using that \r\rr\ by (auto dest:rr) finally show ?thesis . qed then show ?thesis unfolding R1_def R2_def by blast qed moreover have "L1=L2" proof - have "jumpF f (at_left x) = 0" when "\ (- r < x \ x \ r)" for x proof - have "jumpF f (at_left x) = jumpF_polyL q p x" unfolding f_def jumpF_polyL_def by simp also have "... = 0" apply (rule jumpF_poly_noroot) using that \r\rr\ by (auto dest:rr) finally show ?thesis . qed then show ?thesis unfolding L1_def L2_def by blast qed ultimately show "cindexE (- r) r f = cindexE_ubd f" unfolding cindexE_def cindexE_ubd_def apply (fold R1_def R2_def L1_def L2_def) by auto qed moreover have "\\<^sub>F r in at_top. cindexE (- r) r f = cindex_poly_ubd q p" using cindex_poly_ubd_eventually unfolding f_def by auto ultimately have "\\<^sub>F r in at_top. cindexE (- r) r f = cindexE_ubd f \ cindexE (- r) r f = cindex_poly_ubd q p" using eventually_conj by auto then have "\\<^sub>F (r::real) in at_top. cindexE_ubd f = cindex_poly_ubd q p" by (elim eventually_mono) auto then show ?thesis unfolding f_def by auto qed lemma cindex_polyE_noroot: assumes "ax. a\x \ x\b \ poly p x\0" shows "cindex_polyE a b q p = 0" proof - have "jumpF_polyR q p a = 0" apply (rule jumpF_poly_noroot) using assms by auto moreover have "jumpF_polyL q p b = 0" apply (rule jumpF_poly_noroot) using assms by auto moreover have "cindex_poly a b q p =0" apply (rule cindex_poly_noroot) using assms by auto ultimately show ?thesis unfolding cindex_polyE_def by auto qed lemma cindex_polyE_combine: assumes "a (\p. pcompose p [:b,c:])" assumes "lb0" shows "cindex_polyE lb ub (h q) (h p) = (if 0 < c then cindex_polyE (c * lb + b) (c * ub + b) q p else - cindex_polyE (c * ub + b) (c * lb + b) q p)" proof - have "cindex_polyE lb ub (h q) (h p) = cindexE lb ub (\x. poly (h q) x / poly (h p) x)" apply (subst cindexE_eq_cindex_polyE[symmetric,OF \lb]) by simp also have "... = cindexE lb ub ((\x. poly q x / poly p x) \ (\x. c * x + b))" unfolding comp_def h_def poly_pcompose by (simp add:algebra_simps) also have "... = (if 0 < c then cindexE (c * lb + b) (c * ub + b) (\x. poly q x / poly p x) else - cindexE (c * ub + b) (c * lb + b) (\x. poly q x / poly p x))" apply (subst cindexE_linear_comp[OF \c\0\]) by simp also have "... = (if 0 < c then cindex_polyE (c * lb + b) (c * ub + b) q p else - cindex_polyE (c * ub + b) (c * lb + b) q p)" proof - have "cindexE (c * lb + b) (c * ub + b) (\x. poly q x / poly p x) = cindex_polyE (c * lb + b) (c * ub + b) q p" if "c>0" apply (subst cindexE_eq_cindex_polyE) using that \lb by auto moreover have "cindexE (c * ub + b) (c * lb + b) (\x. poly q x / poly p x) = cindex_polyE (c * ub + b) (c * lb + b) q p" if "\ c>0" apply (subst cindexE_eq_cindex_polyE) using that assms by auto ultimately show ?thesis by auto qed finally show ?thesis . qed lemma cindex_polyE_product': fixes p r q s::"real poly" and a b ::real assumes "a s=0 \ p=0 \ r=0 \ p * s + q * r = 0") case True moreover have ?thesis if "q=0" proof - have "p\0" using assms(2) coprime_poly_0 poly_0 that by blast then show ?thesis using that cindex_polyE_mult_cancel by simp qed moreover have ?thesis if "s=0" proof - have "r\0" using assms(3) coprime_poly_0 poly_0 that by blast then have "?L = cindex_polyE a b (r * p) (r * q)" using that by (simp add:algebra_simps) also have "... = ?R" using that cindex_polyE_mult_cancel \r\0\ by simp finally show ?thesis . qed moreover have ?thesis if "p * s + q * r = 0" "s\0" "q\0" proof - have "cindex_polyE a b p q = cindex_polyE a b (s*p) (s*q)" using cindex_polyE_mult_cancel[OF \s\0\] by simp also have "... = cindex_polyE a b (-(q * r)) (q* s)" using that(1) by (metis add.inverse_inverse add.inverse_unique mult.commute) also have "... = - cindex_polyE a b (q * r) (q* s)" using cindex_polyE_smult_1[where c="-1",simplified] by simp also have "... = - cindex_polyE a b r s" using cindex_polyE_mult_cancel[OF \q\0\] by simp finally have "cindex_polyE a b p q = - cindex_polyE a b r s" . then show ?thesis using that(1) by simp qed moreover have ?thesis if "p=0" proof - have "poly q a\0" using assms(2) coprime_poly_0 order_root that(1) by blast have "poly q b\0" by (metis assms(2) coprime_poly_0 mpoly_base_conv(1) that) then have "q\0" using poly_0 by blast have "?L= - cindex_polyE a b s r" using that cindex_polyE_smult_1[where c="-1",simplified] cindex_polyE_mult_cancel[OF \q\0\] by simp also have "... = cindex_polyE a b r s - (cross_alt r s a b) / 2" apply (subst cindex_polyE_inverse_add_cross[symmetric]) using \a \coprime s r\ by (auto simp:coprime_commute) also have "... = ?R" using \p=0\ \poly q a\0\ \poly q b\0\ cross_alt_cancel by simp finally show ?thesis . qed moreover have ?thesis if "r=0" proof - have "poly s a\0" using assms(3) coprime_poly_0 order_root that by blast have "poly s b\0" using assms(3) coprime_poly_0 order_root that by blast then have "s\0" using poly_0 by blast have "cindex_polyE a b (- (q * s)) (p * s) = - cindex_polyE a b (q * s) (p * s)" using cindex_polyE_smult_1[where c="-1",simplified] by auto also have "... = - cindex_polyE a b (s * q) (s * p)" by (simp add:algebra_simps) also have "... = - cindex_polyE a b q p" using cindex_polyE_mult_cancel[OF \s\0\] by simp finally have "cindex_polyE a b (- (q * s)) (p * s) = - cindex_polyE a b q p" . moreover have "cross_alt (p * s) (q * s) a b / 2 = cindex_polyE a b q p + cindex_polyE a b p q" proof - have "cross_alt (p * s) (q * s) a b = cross_alt (s * p) (s * q) a b" by (simp add:algebra_simps) also have "... = cross_alt p q a b" using cross_alt_cancel by (simp add: \poly s a \ 0\ \poly s b \ 0\) also have "... / 2 = cindex_polyE a b q p + cindex_polyE a b p q" apply (subst cindex_polyE_inverse_add_cross[symmetric]) using \a \coprime q p\ coprime_commute by auto finally show ?thesis . qed ultimately show ?thesis using that by simp qed ultimately show ?thesis by argo next case False define P where "P=(p * s + q * r)" define Q where "Q = q * s * P" from False have "q\0" "s\0" "p\0" "r\0" "P \ 0" "Q\0" unfolding P_def Q_def by auto then have finite:"finite (proots_within Q {x. a\x \ x\b})" unfolding P_def Q_def by (auto intro: finite_proots) have sign_pos_eq: "sign_r_pos Q a = (poly Q b>0)" "poly Q a \0 \ poly Q a >0 = (poly Q b>0)" if "ax. a x\b \ poly Q x\0" for a b Q proof - have "sign_r_pos Q a = (sgnx (poly Q) (at_right a) >0)" unfolding sign_r_pos_sgnx_iff by simp also have "... = (sgnx (poly Q) (at_left b) >0)" proof (rule ccontr) assume "(0 < sgnx (poly Q) (at_right a)) \ (0 < sgnx (poly Q) (at_left b))" then have "\x>a. x < b \ poly Q x = 0" using sgnx_at_left_at_right_IVT[OF _ \a] by auto then show False using that(2) by auto qed also have "... = (poly Q b>0)" apply (subst sgnx_poly_nz) using that by auto finally show "sign_r_pos Q a = (poly Q b>0)" . show "(poly Q a >0) = (poly Q b>0)" if "poly Q a\0" proof (rule ccontr) assume "(0 < poly Q a) \ (0 < poly Q b)" then have "poly Q a * poly Q b < 0" by (metis \sign_r_pos Q a = (0 < poly Q b)\ poly_0 sign_r_pos_rec that) from poly_IVT[OF \a this] have "\x>a. x < b \ poly Q x = 0" . then show False using noroot by auto qed qed define Case where "Case=(\a b. cindex_polyE a b (p * r - q * s) P = cindex_polyE a b p q + cindex_polyE a b r s - (cross_alt P (q * s) a b) / 2)" have basic_case:"Case a b" if noroot0:"proots_within Q {x. a x0 \ poly Q b\0" and "a x \ b} = {}" and "coprime q p" "coprime s r" "q\0" "s\0" "p\0" "r\0" "p * s + q * r \ 0" "a x \ b} = {}" using that(1) unfolding P_def . have "P\0" using \p * s + q * r \ 0\ unfolding P_def by simp have cind1:"cindex_polyE a b (p * r - q * s) P = (if poly P a = 0 then jumpF_polyR (p * r - q * s) P a else 0)" proof - have "cindex_poly a b (p * r - q * s) P = 0" apply (rule cindex_poly_noroot[OF \a]) using noroot1 by fastforce moreover have "jumpF_polyL (p * r - q * s) P b = 0" apply (rule jumpF_poly_noroot) using noroot1 \a by auto ultimately show ?thesis unfolding cindex_polyE_def by (simp add: jumpF_poly_noroot(2)) qed have cind2:"cindex_polyE a b p q = (if poly q a = 0 then jumpF_polyR p q a else 0)" proof - have "cindex_poly a b p q = 0" apply (rule cindex_poly_noroot) using noroot1 \a by auto fastforce moreover have "jumpF_polyL p q b = 0" apply (rule jumpF_poly_noroot) using noroot1 \a by auto ultimately show ?thesis unfolding cindex_polyE_def by (simp add: jumpF_poly_noroot(2)) qed have cind3:"cindex_polyE a b r s = (if poly s a = 0 then jumpF_polyR r s a else 0)" proof - have "cindex_poly a b r s = 0" apply (rule cindex_poly_noroot) using noroot1 \a by auto fastforce moreover have "jumpF_polyL r s b = 0" apply (rule jumpF_poly_noroot) using noroot1 \a by auto ultimately show ?thesis unfolding cindex_polyE_def by (simp add: jumpF_poly_noroot(2)) qed have ?thesis if "poly (q * s * P) a\0" proof - have noroot2:"proots_within (q * s * P) {x. a\x \ x\b} = {}" using that noroot1 by force have "cindex_polyE a b (p * r - q * s) P = 0" apply (rule cindex_polyE_noroot) using noroot2 \a < b\ by auto moreover have "cindex_polyE a b p q = 0" apply (rule cindex_polyE_noroot) using noroot2 \a < b\ by auto moreover have "cindex_polyE a b r s = 0" apply (rule cindex_polyE_noroot) using noroot2 \a < b\ by auto moreover have "cross_alt P (q * s) a b = 0" apply (rule cross_alt_noroot[OF \a]) using noroot2 by auto ultimately show ?thesis unfolding P_def by auto qed moreover have ?thesis if "poly (q * s * P) a=0" proof - have ?thesis if "poly q a =0" "poly s a\0" proof - have "poly P a\0" using that coprime_poly_0[OF \coprime q p\] unfolding P_def by simp then have "cindex_polyE a b (p * r - q * s) P = 0" using cind1 by auto moreover have "cindex_polyE a b p q = (cross_alt P (q * s) a b) / 2" proof - have "cindex_polyE a b p q = jumpF_polyR p q a" using cind2 that(1) by auto also have "... = (cross_alt 1 (q * s * P) a b) / 2" proof - have sign_eq:"(sign_r_pos q a \ poly p a>0) = (poly (q * s * P) b > 0)" proof - have "(sign_r_pos q a \ poly p a>0) = (sgnx (poly (q*p)) (at_right a) >0)" proof - have "(poly p a>0) = (sgnx (poly p) (at_right a) > 0)" apply (subst sgnx_poly_nz) using \coprime q p\ coprime_poly_0 that(1) by auto then show ?thesis unfolding sign_r_pos_sgnx_iff apply (subst sgnx_poly_times[of _ a]) subgoal by simp using poly_sgnx_values \p\0\ \q\0\ by (metis (no_types, opaque_lifting) add.inverse_inverse mult.right_neutral mult_minus_right zero_less_one) qed also have "... = (sgnx (poly ((q*p) * s^2)) (at_right a) > 0)" proof (subst (2) sgnx_poly_times) have "sgnx (poly (s\<^sup>2)) (at_right a) > 0" using sgn_zero_iff sgnx_poly_nz(2) that(2) by auto then show "(0 < sgnx (poly (q * p)) (at_right a)) = (0 < sgnx (poly (q * p)) (at_right a) * sgnx (poly (s\<^sup>2)) (at_right a))" by (simp add: zero_less_mult_iff) qed auto also have "... = (sgnx (poly (q * s)) (at_right a) * sgnx (poly (p * s)) (at_right a)> 0)" unfolding power2_eq_square apply (subst sgnx_poly_times[where x=a],simp)+ by (simp add:algebra_simps) also have "... = (sgnx (poly (q * s)) (at_right a) * sgnx (poly P) (at_right a)> 0)" proof - have "sgnx (poly P) (at_right a) = sgnx (poly (q * r + p * s)) (at_right a)" unfolding P_def by (simp add:algebra_simps) also have "... = sgnx (poly (p * s)) (at_right a)" apply (rule sgnx_poly_plus[where x=a]) subgoal using \poly q a=0\ by simp subgoal using \coprime q p\ coprime_poly_0 poly_mult_zero_iff that(1) that(2) by blast by simp finally show ?thesis by auto qed also have "... = (0 < sgnx (poly (q * s * P)) (at_right a))" apply (subst sgnx_poly_times[where x=a],simp)+ by (simp add:algebra_simps) also have "... = (0 < sgnx (poly (q * s * P)) (at_left b))" proof - have "sgnx (poly (q * s * P)) (at_right a) = sgnx (poly (q * s * P)) (at_left b)" proof (rule ccontr) assume "sgnx (poly (q * s * P)) (at_right a) \ sgnx (poly (q * s * P)) (at_left b)" from sgnx_at_left_at_right_IVT[OF this \a] have "\x>a. x < b \ poly (q * s * P) x = 0" . then show False using noroot1 by fastforce qed then show ?thesis by auto qed also have "... = (poly (q * s * P) b > 0)" apply (subst sgnx_poly_nz) using noroot1 \a by auto finally show ?thesis . qed have psign_a:"psign_diff 1 (q * s * P) a = 1" unfolding psign_diff_def using \poly (q * s * P) a=0\ by simp have "poly (q * s * P) b \0" using noroot1 \a by blast moreover have ?thesis if "poly (q * s * P) b >0" proof - have "psign_diff 1 (q * s * P) b = 0" using that unfolding psign_diff_def by auto moreover have "jumpF_polyR p q a = 1/2" unfolding jumpF_polyR_coprime[OF \coprime q p\] using \p \ 0\ \poly q a = 0\ \q \ 0\ sign_eq that by presburger ultimately show ?thesis unfolding cross_alt_def using psign_a by auto qed moreover have ?thesis if "poly (q * s * P) b <0" proof - have "psign_diff 1 (q * s * P) b = 2" using that unfolding psign_diff_def by auto moreover have "jumpF_polyR p q a = - 1/2" unfolding jumpF_polyR_coprime[OF \coprime q p\] using \p \ 0\ \poly q a = 0\ \q \ 0\ sign_eq that by auto ultimately show ?thesis unfolding cross_alt_def using psign_a by auto qed ultimately show ?thesis by argo qed also have "... = (cross_alt P (q * s) a b) / 2" apply (subst cross_alt_clear[symmetric]) using \poly P a \ 0\ noroot1 \a cross_alt_poly_commute by auto finally show ?thesis . qed moreover have "cindex_polyE a b r s = 0" using cind3 that by auto ultimately show ?thesis using that apply (fold P_def) by auto qed moreover have ?thesis if "poly q a \0" "poly s a=0" proof - have "poly P a\0" using that coprime_poly_0[OF \coprime s r\] unfolding P_def by simp then have "cindex_polyE a b (p * r - q * s) P = 0" using cind1 by auto moreover have "cindex_polyE a b r s = (cross_alt P (q * s) a b) / 2" proof - have "cindex_polyE a b r s = jumpF_polyR r s a" using cind3 that by auto also have "... = (cross_alt 1 (s * q * P) a b) / 2" proof - have sign_eq:"(sign_r_pos s a \ poly r a>0) = (poly (s * q * P) b > 0)" proof - have "(sign_r_pos s a \ poly r a>0) = (sgnx (poly (s*r)) (at_right a) >0)" proof - have "(poly r a>0) = (sgnx (poly r) (at_right a) > 0)" apply (subst sgnx_poly_nz) using \coprime s r\ coprime_poly_0 that(2) by auto then show ?thesis unfolding sign_r_pos_sgnx_iff apply (subst sgnx_poly_times[of _ a]) subgoal by simp subgoal using \r \ 0\ \s \ 0\ by (metis (no_types, opaque_lifting) add.inverse_inverse mult.right_neutral mult_minus_right poly_sgnx_values(2) zero_less_one) done qed also have "... = (sgnx (poly ((s*r) * q^2)) (at_right a) > 0)" proof (subst (2) sgnx_poly_times) have "sgnx (poly (q\<^sup>2)) (at_right a) > 0" by (metis \q \ 0\ power2_eq_square sign_r_pos_mult sign_r_pos_sgnx_iff) then show "(0 < sgnx (poly (s * r)) (at_right a)) = (0 < sgnx (poly (s * r)) (at_right a) * sgnx (poly (q\<^sup>2)) (at_right a))" by (simp add: zero_less_mult_iff) qed auto also have "... = (sgnx (poly (s * q)) (at_right a) * sgnx (poly (r * q)) (at_right a)> 0)" unfolding power2_eq_square apply (subst sgnx_poly_times[where x=a],simp)+ by (simp add:algebra_simps) also have "... = (sgnx (poly (s * q)) (at_right a) * sgnx (poly P) (at_right a)> 0)" proof - have "sgnx (poly P) (at_right a) = sgnx (poly (p * s + q * r )) (at_right a)" unfolding P_def by (simp add:algebra_simps) also have "... = sgnx (poly (q * r)) (at_right a)" apply (rule sgnx_poly_plus[where x=a]) subgoal using \poly s a=0\ by simp subgoal using \coprime s r\ coprime_poly_0 poly_mult_zero_iff that(1) that(2) by blast by simp finally show ?thesis by (auto simp:algebra_simps) qed also have "... = (0 < sgnx (poly (s * q * P)) (at_right a))" apply (subst sgnx_poly_times[where x=a],simp)+ by (simp add:algebra_simps) also have "... = (0 < sgnx (poly (s * q * P)) (at_left b))" proof - have "sgnx (poly (s * q * P)) (at_right a) = sgnx (poly (s * q * P)) (at_left b)" proof (rule ccontr) assume "sgnx (poly (s * q * P)) (at_right a) \ sgnx (poly (s * q * P)) (at_left b)" from sgnx_at_left_at_right_IVT[OF this \a] have "\x>a. x < b \ poly (s * q * P) x = 0" . then show False using noroot1 by fastforce qed then show ?thesis by auto qed also have "... = (poly (s * q * P) b > 0)" apply (subst sgnx_poly_nz) using noroot1 \a by auto finally show ?thesis . qed have psign_a:"psign_diff 1 (s * q * P) a = 1" unfolding psign_diff_def using \poly (q * s * P) a=0\ by (simp add:algebra_simps) have "poly (s * q * P) b \0" using noroot1 \a by (auto simp:algebra_simps) moreover have ?thesis if "poly (s * q * P) b >0" proof - have "psign_diff 1 (s * q * P) b = 0" using that unfolding psign_diff_def by auto moreover have "jumpF_polyR r s a = 1/2" unfolding jumpF_polyR_coprime[OF \coprime s r\] using \poly s a = 0\ \r \ 0\ \s \ 0\ sign_eq that by presburger ultimately show ?thesis unfolding cross_alt_def using psign_a by auto qed moreover have ?thesis if "poly (s * q * P) b <0" proof - have "psign_diff 1 (s * q * P) b = 2" using that unfolding psign_diff_def by auto moreover have "jumpF_polyR r s a = - 1/2" unfolding jumpF_polyR_coprime[OF \coprime s r\] using \poly s a = 0\ \r \ 0\ sign_eq that by auto ultimately show ?thesis unfolding cross_alt_def using psign_a by auto qed ultimately show ?thesis by argo qed also have "... = (cross_alt P (q * s) a b) / 2" apply (subst cross_alt_clear[symmetric]) using \poly P a \ 0\ noroot1 \a cross_alt_poly_commute by (auto simp:algebra_simps) finally show ?thesis . qed moreover have "cindex_polyE a b p q = 0" using cind2 that by auto ultimately show ?thesis using that apply (fold P_def) by auto qed moreover have ?thesis if "poly P a =0" "poly q a\0" "poly s a\0" proof - have "cindex_polyE a b (p * r - q * s) P = jumpF_polyR (p * r - q * s) P a" using cind1 that by auto also have "... = (if sign_r_pos P a = (0 < poly (p * r - q * s) a) then 1 / 2 else - 1 / 2)" (is "_ = ?R") proof (subst jumpF_polyR_coprime') let ?C="(P \ 0 \ p * r - q * s \ 0 \ poly P a = 0)" have "?C" by (smt (z3) P_def \P \ 0\ add.left_neutral diff_add_cancel poly_add poly_mult_zero_iff sign_r_pos_mult sign_r_pos_rec that(1) that(2) that(3)) then show "(if ?C then ?R else 0) = ?R" by auto show "poly P a \ 0 \ poly (p * r - q * s) a \ 0" by (smt (z3) P_def mult_less_0_iff poly_add poly_diff poly_mult poly_mult_zero_iff that(2) that(3)) qed also have "... = - cross_alt P (q * s) a b / 2" proof - have "(sign_r_pos P a = (0 < poly (p * r - q * s) a)) =(\ (poly (q * s * P) b > 0))" proof - have "(poly (q * s * P) b > 0) = (sgnx (poly (q * s * P)) (at_left b) >0)" apply (subst sgnx_poly_nz) using noroot1 \a by auto also have "... = (sgnx (poly (q * s * P)) (at_right a) >0)" proof (rule ccontr) define F where "F=(q * s * P)" assume "(0 < sgnx (poly F) (at_left b)) \ (0 < sgnx (poly F) (at_right a))" then have "sgnx (poly F) (at_right a) \ sgnx (poly F) (at_left b)" by auto then have "\x>a. x < b \ poly F x = 0" using sgnx_at_left_at_right_IVT[OF _ \a] by auto then show False using noroot1[folded F_def] \a by fastforce qed also have "... = sign_r_pos (q * s * P) a" using sign_r_pos_sgnx_iff by simp also have "... = (sign_r_pos P a = sign_r_pos (q * s) a)" apply (subst sign_r_pos_mult[symmetric]) using \P\0\ \q\0\ \s\0\ by (auto simp add:algebra_simps) also have "... = (sign_r_pos P a = (0 \ poly (p * r - q * s) a))" proof - have "sign_r_pos (q * s) a=(poly (q * s) a > 0)" by (metis poly_0 poly_mult_zero_iff sign_r_pos_rec that(2) that(3)) also have "... = (0 \ poly (p * r - q * s) a)" using \poly P a =0\ unfolding P_def by (smt (verit, ccfv_threshold) \p \ 0\ \q \ 0\ \r \ 0\ \s \ 0\ divisors_zero poly_add poly_diff poly_mult_zero_iff sign_r_pos_mult sign_r_pos_rec that(2) that(3)) finally show ?thesis by simp qed finally have "(0 < poly (q * s * P) b) = (sign_r_pos P a = (poly (p * r - q * s) a \ 0))" . then show ?thesis by argo qed moreover have "cross_alt P (q * s) a b = (if poly (q * s * P) b > 0 then 1 else -1)" proof - have "psign_diff P (q * s) a = 1" by (smt (verit, ccfv_threshold) Sturm_Tarski.sign_def dvd_div_mult_self gcd_dvd1 gcd_dvd2 poly_mult_zero_iff psign_diff_def that(1) that(2) that(3)) moreover have "psign_diff P (q * s) b = (if poly (q * s * P) b > 0 then 0 else 2)" proof - define F where "F = q * s * P" have "psign_diff P (q * s) b = psign_diff 1 F b" apply (subst psign_diff_clear) using noroot1 \a unfolding F_def by (auto simp:algebra_simps) also have "... = (if 0 < poly F b then 0 else 2)" proof - have "poly F b\0" unfolding F_def using \a noroot1 by auto then show ?thesis unfolding psign_diff_def by auto qed finally show ?thesis unfolding F_def . qed ultimately show ?thesis unfolding cross_alt_def by auto qed ultimately show ?thesis by auto qed finally have "cindex_polyE a b (p * r - q * s) P = - cross_alt P (q * s) a b / 2 " . moreover have "cindex_polyE a b p q = 0" using cind2 that by auto moreover have "cindex_polyE a b r s = 0" using cind3 that by auto ultimately show ?thesis by (fold P_def) auto qed moreover have ?thesis if "poly q a=0" "poly s a=0" proof - have "poly p a\0" using \coprime q p\ coprime_poly_0 that(1) by blast have "poly r a\0" using \coprime s r\ coprime_poly_0 that(2) by blast have "poly P a=0" unfolding P_def using that by simp define ff where "ff=(\x. if x then 1/(2::real) else -1/2)" define C1 C2 C3 C4 C5 where "C1 = (sign_r_pos P a)" and "C2 =(0 < poly p a)" and "C3= (0 < poly r a)" and "C4=(sign_r_pos q a)" and "C5=(sign_r_pos s a)" note CC_def = C1_def C2_def C3_def C4_def C5_def have "cindex_polyE a b (p * r - q * s) P = ff ((C1 = C2) = C3)" proof - have "cindex_polyE a b (p * r - q * s) P = jumpF_polyR (p * r - q * s) P a" using cind1 \poly P a=0\ by auto also have "... = (ff (sign_r_pos P a = (0 < poly (p * r - q * s) a)) )" unfolding ff_def apply (subst jumpF_polyR_coprime') subgoal by (simp add: \poly p a \ 0\ \poly r a \ 0\ that(1)) subgoal by (smt (z3) \P \ 0\ \poly P a = 0\ \poly P a \ 0 \ poly (p * r - q * s) a \ 0\ poly_0) done also have "... = (ff (sign_r_pos P a = (0 < poly (p * r) a)))" proof - have "(0 < poly (p * r - q * s) a) = (0 < poly (p * r) a)" by (simp add: that(1)) then show ?thesis by simp qed also have "... = ff ((C1 = C2) = C3)" unfolding CC_def by (smt (z3) \p \ 0\ \poly p a \ 0\ \poly r a \ 0\ \r \ 0\ no_zero_divisors poly_mult_zero_iff sign_r_pos_mult sign_r_pos_rec) finally show ?thesis . qed moreover have "cindex_polyE a b p q = ff (C4 = C2)" proof - have "cindex_polyE a b p q = jumpF_polyR p q a" using cind2 \poly q a=0\ by auto also have "... = ff (sign_r_pos q a = (0 < poly p a))" apply (subst jumpF_polyR_coprime') subgoal using \poly p a \ 0\ by auto subgoal using \p \ 0\ \q \ 0\ ff_def that(1) by presburger done also have "... = ff (C4 = C2)" using \a noroot1 unfolding CC_def by auto finally show ?thesis . qed moreover have " cindex_polyE a b r s = ff (C5 = C3)" proof - have "cindex_polyE a b r s = jumpF_polyR r s a" using cind3 \poly s a=0\ by auto also have "... = ff (sign_r_pos s a = (0 < poly r a))" apply (subst jumpF_polyR_coprime') subgoal using \poly r a \ 0\ by auto subgoal using \r \ 0\ \s \ 0\ ff_def that(2) by presburger done also have "... = ff (C5 = C3)" using \a noroot1 unfolding CC_def by auto finally show ?thesis . qed moreover have "cross_alt P (q * s) a b = 2 * ff ((C1 = C4) = C5)" proof - have "cross_alt P (q * s) a b = sign (poly P b * (poly q b * poly s b))" apply (subst cross_alt_clear) apply (subst cross_alt_alt) using that by auto also have "... = 2 * ff ((C1 = C4) = C5)" proof - have "sign_r_pos P a = (poly P b>0)" apply (rule sign_pos_eq) using \a noroot1 by auto moreover have "sign_r_pos q a = (poly q b>0)" apply (rule sign_pos_eq) using \a noroot1 by auto moreover have "sign_r_pos s a = (poly s b>0)" apply (rule sign_pos_eq) using \a noroot1 by auto ultimately show ?thesis unfolding CC_def ff_def apply (simp add:sign_times) using noroot1 \a by (auto simp:sign_def) qed finally show ?thesis . qed ultimately have "?thesis = (ff ((C1 = C2) = C3) = ff (C4 = C2) + ff (C5 = C3) - ff ((C1 = C4) = C5))" by (fold P_def) auto moreover have "ff ((C1 = C2) = C3) = ff (C4 = C2) + ff (C5 = C3) - ff ((C1 = C4) = C5)" proof - have pp:"(0 < poly p a) = sign_r_pos p a" apply (subst sign_r_pos_rec) using \poly p a\0\ by auto have rr:"(0 < poly r a) = sign_r_pos r a" apply (subst sign_r_pos_rec) using \poly r a\0\ by auto have "C1" if "C2=C5" "C3=C4" proof - have "sign_r_pos (p * s) a" apply (subst sign_r_pos_mult) using pp \C2=C5\ \p\0\ \s\0\ unfolding CC_def by auto moreover have "sign_r_pos (q * r) a" apply (subst sign_r_pos_mult) using rr \C3=C4\ \q\0\ \r\0\ unfolding CC_def by auto ultimately show ?thesis unfolding CC_def P_def using sign_r_pos_plus_imp by auto qed moreover have foo2:"\C1" if "C2\C5" "C3\C4" proof - have "(0 < poly p a) = sign_r_pos (-s) a" apply (subst sign_r_pos_minus) using \s\0\ \C2\C5\ unfolding CC_def by auto then have "sign_r_pos (p * (-s)) a" apply (subst sign_r_pos_mult) unfolding pp using \p\0\ \s\0\ by auto moreover have "(0 < poly r a) = sign_r_pos (-q) a" apply (subst sign_r_pos_minus) using \q\0\ \C3\C4\ unfolding CC_def by auto then have "sign_r_pos (r * (-q)) a" apply (subst sign_r_pos_mult) unfolding rr using \r\0\ \q\0\ by auto ultimately have "sign_r_pos (p * (-s) + r * (-q)) a" using sign_r_pos_plus_imp by blast then have "sign_r_pos (- (p * s + q * r)) a" by (simp add:algebra_simps) then have "\ sign_r_pos P a" apply (subst sign_r_pos_minus) using \P\0\ unfolding P_def by auto then show ?thesis unfolding CC_def . qed ultimately show ?thesis unfolding ff_def by auto qed ultimately show ?thesis by simp qed ultimately show ?thesis using that by auto qed ultimately show ?thesis by auto qed have "?thesis' p r q s a" if "poly Q b \ 0" apply (rule base_case[OF _ \coprime q p\ \coprime s r\]) subgoal using noroot0 that unfolding Q_def P_def by fastforce using False \a by auto moreover have "?thesis' p r q s a" if "poly Q b = 0" proof - have "poly Q a\0" using noroot_disj that by auto define h where "h=(\p. p \\<^sub>p [:a + b, - 1:])" have h_rw: "h p - h q = h (p - q)" "h p * h q = h (p * q)" "h p + h q = h (p + q)" "cindex_polyE a b (h q) (h p) = - cindex_polyE a b q p" "cross_alt (h p) (h q) a b = cross_alt p q b a" for p q unfolding h_def pcompose_diff pcompose_mult pcompose_add cindex_polyE_linear_comp[OF \a, of "-1" _ "a+b",simplified] cross_alt_linear_comp[of p "a+b" "-1" q a b,simplified] by simp_all have "?thesis' (h p) (h r) (h q) (h s) a" proof (rule base_case) have "proots_within (h q * h s * (h p * h s + h q * h r)) {x. a < x \ x \ b} = proots_within (h Q) {x. a < x \ x \ b}" unfolding Q_def P_def h_def by (simp add:pcompose_diff pcompose_mult pcompose_add) also have "... = {}" unfolding proots_within_def h_def poly_pcompose using \a that[folded Q_def] noroot0[unfolded P_def, folded Q_def] \poly Q a\0\ by (auto simp:order.order_iff_strict proots_within_def) finally show "proots_within (h q * h s * (h p * h s + h q * h r)) {x. a < x \ x \ b} = {}" . show "coprime (h q) (h p)" unfolding h_def apply (rule coprime_linear_comp) using \coprime q p\ by auto show "coprime (h s) (h r)" unfolding h_def apply (rule coprime_linear_comp) using \coprime s r\ by auto show "h q \ 0" "h s \ 0" " h p \ 0" " h r \ 0" using False unfolding h_def by (subst pcompose_eq_0;auto)+ have "h (p * s + q * r) \ 0" using False unfolding h_def by (subst pcompose_eq_0;auto) then show "h p * h s + h q * h r \ 0" unfolding h_def pcompose_mult pcompose_add by simp show "a < b" by fact qed moreover have "cross_alt (p * s + q * r) (q * s) b a = - cross_alt (p * s + q * r) (q * s) a b" unfolding cross_alt_def by auto ultimately show ?thesis unfolding h_rw by auto qed ultimately show ?thesis unfolding Case_def P_def by blast qed show ?thesis using \a proof (induct "card (proots_within (q * s * P) {x. a x\b})" arbitrary:a) case 0 have "Case a b" proof (rule basic_case) have *:"proots_within Q {x. a < x \ x \ b} = {}" using 0 \Q\0\ unfolding Q_def by auto then show "proots_within Q {x. a < x \ x < b} = {}" by force show "poly Q a \ 0 \ poly Q b \ 0" using * \a by blast show "a < b" by fact qed then show ?case unfolding Case_def P_def by simp next case (Suc n) define S where "S=(\a. proots_within Q {x. a < x \ x \ b})" have Sa_Suc:"Suc n = card (S a)" using Suc(2) unfolding S_def Q_def by auto define mroot where "mroot = Min (S a)" have fin_S:"finite (S a)" for a using Suc(2) unfolding S_def Q_def by (simp add: \P \ 0\ \q \ 0\ \s \ 0\) have mroot_in:"mroot \ S a" and mroot_min:"\x\S a. mroot\x" proof - have "S a\{}" unfolding S_def Q_def using Suc.hyps(2) by force then show "mroot \ S a" unfolding mroot_def using Min_in fin_S by auto show "\x\S a. mroot\x" using \finite (S a)\ Min_le unfolding mroot_def by auto qed have mroot_nzero:"poly Q x\0" if "aa b. cindex_polyE a b (p * r - q * s) P)" define C2 where "C2=(\a b. cindex_polyE a b p q)" define C3 where "C3=(\a b. cindex_polyE a b r s)" define C4 where "C4=(\a b. cross_alt P (q * s) a b)" note CC_def = C1_def C2_def C3_def C4_def have hyps:"C1 mroot b = C2 mroot b + C3 mroot b - C4 mroot b / 2" if "mroot < b" unfolding C1_def C2_def C3_def C4_def P_def proof (rule Suc.hyps(1)[OF _ that]) have "Suc n = card (S a)" using Sa_Suc by auto also have "... = card (insert mroot (S mroot))" proof - have "S a = proots_within Q {x. a < x \ x \ b}" unfolding S_def Q_def by simp also have "... = proots_within Q ({x. a < x \ x \ mroot} \ {x. mroot < x \ x \ b})" apply (rule arg_cong2[where f=proots_within]) using mroot_in unfolding S_def by auto also have "... = proots_within Q {x. a < x \ x \ mroot} \ S mroot" unfolding S_def Q_def apply (subst proots_within_union) by auto also have "... = {mroot} \ S mroot" proof - have "proots_within Q {x. a < x \ x \ mroot} = {mroot}" using mroot_in mroot_min unfolding S_def by auto force then show ?thesis by auto qed finally have "S a = insert mroot (S mroot)" by auto then show ?thesis by auto qed also have "... = Suc (card (S mroot))" apply (rule card_insert_disjoint) using fin_S unfolding S_def by auto finally have "Suc n = Suc (card (S mroot))" . then have "n = card (S mroot)" by simp then show "n = card (proots_within (q * s * P) {x. mroot < x \ x \ b})" unfolding S_def Q_def by simp qed have ?case if "mroot = b" proof - have nzero:"poly Q x \0" if "amroot = b\ that by auto define m where "m=(a+b)/2" have [simp]:"aa unfolding m_def by auto have "Case a m" proof (rule basic_case) show "proots_within Q {x. a < x \ x < m} = {}" using nzero \a unfolding m_def by auto have "poly Q m \ 0" using nzero \a \m by auto then show "poly Q a \ 0 \ poly Q m \ 0" by auto qed simp moreover have "Case m b" proof (rule basic_case) show "proots_within Q {x. m < x \ x < b} = {}" using nzero \a unfolding m_def by auto have "poly Q m \ 0" using nzero \a \m by auto then show "poly Q m \ 0 \ poly Q b \ 0" by auto qed simp ultimately have "C1 a m + C1 m b = (C2 a m + C2 m b) + (C3 a m + C3 m b) - (C4 a m + C4 m b)/2" unfolding Case_def C1_def apply simp unfolding C2_def C3_def C4_def by (auto simp:algebra_simps) moreover have "C1 a m + C1 m b = C1 a b" "C2 a m + C2 m b = C2 a b" "C3 a m + C3 m b = C3 a b" unfolding CC_def by (rule cindex_polyE_combine;auto)+ moreover have "C4 a m + C4 m b = C4 a b" unfolding C4_def cross_alt_def by simp ultimately have "C1 a b = C2 a b + C3 a b - C4 a b/2" by auto then show ?thesis unfolding CC_def P_def by auto qed moreover have ?case if "mroot \b" proof - have [simp]:"a 0" by (rule mroot_nzero) auto have "C1 mroot b = C2 mroot b + C3 mroot b - C4 mroot b / 2" using hyps \mroot by simp moreover have "Case a m" apply (rule basic_case) subgoal by (smt (verit) Collect_empty_eq \m < mroot\ mem_Collect_eq mroot_nzero proots_within_def) subgoal using \poly Q m \ 0\ by auto by fact then have "C1 a m = C2 a m + C3 a m - C4 a m / 2" unfolding Case_def CC_def by auto moreover have "Case m mroot" apply (rule basic_case) subgoal by (smt (verit) Collect_empty_eq \a < m\ mem_Collect_eq mroot_nzero proots_within_def) subgoal using \poly Q m \ 0\ by auto by fact then have "C1 m mroot = C2 m mroot + C3 m mroot - C4 m mroot / 2" unfolding Case_def CC_def by auto ultimately have "C1 a m + C1 m mroot + C1 mroot b = (C2 a m + C2 m mroot + C2 mroot b) + (C3 a m + C3 m mroot + C3 mroot b) - (C4 a m + C4 m mroot + C4 mroot b) / 2" by simp (simp add:algebra_simps) moreover have "C1 a m + C1 m mroot + C1 mroot b = C1 a b" "C2 a m + C2 m mroot + C2 mroot b = C2 a b" "C3 a m + C3 m mroot + C3 mroot b = C3 a b" unfolding CC_def by (subst cindex_polyE_combine;simp?)+ moreover have "C4 a m + C4 m mroot + C4 mroot b = C4 a b" unfolding C4_def cross_alt_def by simp ultimately have "C1 a b = C2 a b + C3 a b - C4 a b/2" by auto then show ?thesis unfolding CC_def P_def by auto qed ultimately show ?case by auto qed qed lemma cindex_polyE_product: fixes p r q s::"real poly" and a b ::real assumes "a0 \ q\0" "r\0 \ s\0"*) and "poly p a\0 \ poly q a\0" "poly p b\0 \ poly q b\0" and "poly r a\0 \ poly s a\0" "poly r b\0 \ poly s b\0" shows "cindex_polyE a b (p * r - q * s) (p * s + q * r) = cindex_polyE a b p q + cindex_polyE a b r s - cross_alt (p * s + q * r) (q * s) a b / 2" proof - define g1 where "g1 = gcd p q" obtain p' q' where pq:"p=g1*p'" "q=g1*q'" and "coprime q' p'" unfolding g1_def by (metis assms(2) coprime_commute div_gcd_coprime dvd_mult_div_cancel gcd_dvd1 gcd_dvd2 order_root) define g2 where "g2 = gcd r s" obtain r' s' where rs:"r=g2*r'" "s = g2 * s'" "coprime s' r'" unfolding g2_def using assms(4) by (metis coprime_commute div_gcd_coprime dvd_mult_div_cancel gcd_dvd1 gcd_dvd2 order_root) define g where "g=g1 * g2" have [simp]:"g\0" "g1\0" "g2\0" unfolding g_def g1_def g2_def using assms by auto have [simp]:"poly g a \ 0" "poly g b \ 0" unfolding g_def g1_def g2_def subgoal by (metis assms(2) assms(4) poly_gcd_0_iff poly_mult_zero_iff) subgoal by (metis assms(3) assms(5) poly_gcd_0_iff poly_mult_zero_iff) done have "cindex_polyE a b (p' * r' - q' * s') (p' * s' + q' * r') = cindex_polyE a b p' q' + cindex_polyE a b r' s' - (cross_alt (p' * s' + q' * r') (q' * s') a b) / 2" using cindex_polyE_product'[OF \a \coprime q' p'\ \coprime s' r'\] . moreover have "cindex_polyE a b (p * r - q * s) (p * s + q * r) = cindex_polyE a b (g*(p' * r' - q' * s')) (g*(p' * s' + q' * r'))" unfolding pq rs g_def by (auto simp:algebra_simps) then have "cindex_polyE a b (p * r - q * s) (p * s + q * r) = cindex_polyE a b (p' * r' - q' * s') (p' * s' + q' * r')" apply (subst (asm) cindex_polyE_mult_cancel) by simp moreover have "cindex_polyE a b p q = cindex_polyE a b p' q'" unfolding pq using cindex_polyE_mult_cancel by simp moreover have "cindex_polyE a b r s =cindex_polyE a b r' s'" unfolding rs using cindex_polyE_mult_cancel by simp moreover have "cross_alt (p * s + q * r) (q * s) a b = cross_alt (g*(p' * s' + q' * r')) (g*(q' * s')) a b " unfolding pq rs g_def by (auto simp:algebra_simps) then have "cross_alt (p * s + q * r) (q * s) a b = cross_alt (p' * s' + q' * r') (q' * s') a b " apply (subst (asm) cross_alt_cancel) by simp_all ultimately show ?thesis by auto qed (*TODO: move to Winding_Number_Eval*) lemma cindex_pathE_linepath_on: assumes "z \ closed_segment a b" shows "cindex_pathE (linepath a b) z = 0" proof - obtain u where "0\u" "u\1" and z_eq:"z = complex_of_real (1 - u) * a + complex_of_real u * b" using assms unfolding in_segment scaleR_conv_of_real by auto define U where "U = [:-u, 1:]" have "U\0" unfolding U_def by auto have "cindex_pathE (linepath a b) z = cindexE 0 1 (\t. (Im a + t * Im b - (Im z + t * Im a)) / (Re a + t * Re b - (Re z + t * Re a)))" unfolding cindex_pathE_def by (simp add:linepath_def algebra_simps) also have "... = cindexE 0 1 (\t. ( (Im b - Im a) * (t-u)) / ( (Re b - Re a) * (t-u)))" unfolding z_eq by (simp add:algebra_simps) also have "... = cindex_polyE 0 1 (U*[:Im b - Im a:]) (U*[:Re b - Re a:])" proof (subst cindexE_eq_cindex_polyE[symmetric]) have " (Im b - Im a) * (t - u) / ((Re b - Re a) * (t - u)) = poly (U * [:Im b - Im a:]) t / poly (U * [:Re b - Re a:]) t" for t unfolding U_def by (simp add:algebra_simps) then show "cindexE 0 1 (\t. (Im b - Im a) * (t - u) / ((Re b - Re a) * (t - u))) = cindexE 0 1 (\x. poly (U * [:Im b - Im a:]) x / poly (U * [:Re b - Re a:]) x)" by auto qed simp also have "... = cindex_polyE 0 1 [:Im b - Im a:] [:Re b - Re a:]" apply (rule cindex_polyE_mult_cancel) by fact also have "... = cindexE 0 1 (\x. (Im b - Im a) / (Re b - Re a))" apply (subst cindexE_eq_cindex_polyE[symmetric]) by auto also have "... = 0" apply (rule cindexE_constI) by auto finally show ?thesis . qed subsection \More Cauchy indices on polynomials\ definition cindexP_pathE::"complex poly \ (real \ complex) \ real" where "cindexP_pathE p g = cindex_pathE (poly p o g) 0" definition cindexP_lineE :: "complex poly \ complex \ complex \ real" where "cindexP_lineE p a b = cindexP_pathE p (linepath a b)" lemma cindexP_pathE_const:"cindexP_pathE [:c:] g = 0" unfolding cindexP_pathE_def by (auto intro:cindex_pathE_constI) lemma cindex_poly_pathE_joinpaths: assumes "finite_ReZ_segments (poly p o g1) 0" and "finite_ReZ_segments (poly p o g2) 0" and "path g1" and "path g2" and "pathfinish g1 = pathstart g2" shows "cindexP_pathE p (g1 +++ g2) = cindexP_pathE p g1 + cindexP_pathE p g2" proof - have "path (poly p o g1)" "path (poly p o g2)" using \path g1\ \path g2\ by auto moreover have "pathfinish (poly p o g1) = pathstart (poly p o g2)" using \pathfinish g1 = pathstart g2\ by (simp add: pathfinish_compose pathstart_def) ultimately have "cindex_pathE ((poly p \ g1) +++ (poly p \ g2)) 0 = cindex_pathE (poly p \ g1) 0 + cindex_pathE (poly p \ g2) 0" using cindex_pathE_joinpaths[OF assms(1,2)] by auto then show ?thesis unfolding cindexP_pathE_def by (simp add:path_compose_join) qed lemma cindexP_lineE_polyE: fixes p::"complex poly" and a b::complex defines "pp \ pcompose p [:a, b-a:]" defines "pR \ map_poly Re pp" and "pI \ map_poly Im pp" shows "cindexP_lineE p a b = cindex_polyE 0 1 pI pR" proof - have "cindexP_lineE p a b = cindexE 0 1 (\t. Im (poly (p \\<^sub>p [:a, b - a:]) (complex_of_real t)) / Re (poly (p \\<^sub>p [:a, b - a:]) (complex_of_real t)))" unfolding cindexP_lineE_def cindexP_pathE_def cindex_pathE_def by (simp add:poly_linepath_comp') also have "... = cindexE 0 1 (\t. poly pI t/poly pR t)" unfolding pI_def pR_def pp_def by (simp add:Im_poly_of_real Re_poly_of_real) also have "... = cindex_polyE 0 1 pI pR" apply (subst cindexE_eq_cindex_polyE) by simp_all finally show ?thesis . qed definition psign_aux :: "complex poly \ complex poly \ complex \ int" where "psign_aux p q b = sign (Im (poly p b * poly q b) * (Im (poly p b) * Im (poly q b))) + sign (Re (poly p b * poly q b) * Im (poly p b * poly q b)) - sign (Re (poly p b) * Im (poly p b)) - sign (Re (poly q b) * Im (poly q b))" definition cdiff_aux :: "complex poly \ complex poly \ complex \ complex \ int" where "cdiff_aux p q a b = psign_aux p q b - psign_aux p q a" lemma cindexP_lineE_times: fixes p q::"complex poly" and a b::complex assumes "poly p a\0" "poly p b\0" "poly q a\0" "poly q b\0" shows "cindexP_lineE (p*q) a b = cindexP_lineE p a b + cindexP_lineE q a b+cdiff_aux p q a b/2" proof - define pR pI where "pR = map_poly Re (p \\<^sub>p [:a, b - a:])" and "pI = map_poly Im (p \\<^sub>p [:a, b - a:])" define qR qI where "qR = map_poly Re (q \\<^sub>p [:a, b - a:])" and "qI = map_poly Im (q \\<^sub>p [:a, b - a:])" define P1 P2 where "P1 = pR * qI + pI * qR" and "P2=pR * qR - pI * qI" have p_poly: "poly pR 0 = Re (poly p a)" "poly pI 0 = Im (poly p a)" "poly pR 1 = Re (poly p b)" "poly pI 1 = Im (poly p b)" unfolding pR_def pI_def by (simp flip:Re_poly_of_real Im_poly_of_real add:poly_pcompose)+ have q_poly: "poly qR 0 = Re (poly q a)" "poly qI 0 = Im (poly q a)" "poly qR 1 = Re (poly q b)" "poly qI 1 = Im (poly q b)" unfolding qR_def qI_def by (simp flip:Re_poly_of_real Im_poly_of_real add:poly_pcompose)+ have P2_poly: "poly P2 0 = Re (poly (p*q) a)" "poly P2 1 = Re (poly (p*q) b)" unfolding P2_def pR_def qI_def pI_def qR_def by (simp flip:Re_poly_of_real Im_poly_of_real add:poly_pcompose)+ have P1_poly: "poly P1 0 = Im (poly (p*q) a)" "poly P1 1 = Im (poly (p*q) b)" unfolding P1_def pR_def qI_def pI_def qR_def by (simp flip:Re_poly_of_real Im_poly_of_real add:poly_pcompose)+ have p_nzero:"poly pR 0 \ 0 \ poly pI 0 \ 0" "poly pR 1 \ 0 \ poly pI 1 \ 0" unfolding p_poly using assms(1,2) complex_eqI by force+ have q_nzero:"poly qR 0 \ 0 \ poly qI 0 \ 0" "poly qR 1 \ 0 \ poly qI 1 \ 0" unfolding q_poly using assms(3,4) complex_eqI by force+ have P12_nzero:"poly P2 0 \ 0 \ poly P1 0 \ 0" "poly P2 1 \ 0 \ poly P1 1 \ 0" unfolding P1_poly P2_poly using assms by (metis Im_poly_hom.base.hom_zero Re_poly_hom.base.hom_zero complex_eqI poly_mult_zero_iff)+ define C1 C2 where "C1 = (\p q. cindex_polyE 0 1 p q)" and "C2 = (\p q. real_of_int (cross_alt p q 0 1) /2)" define CR where "CR = C2 P1 (pI * qI) +C2 P2 P1 - C2 pR pI - C2 qR qI" have "cindexP_lineE (p*q) a b = cindex_polyE 0 1 (map_poly Im (cpoly_of pR pI * cpoly_of qR qI)) (map_poly Re (cpoly_of pR pI * cpoly_of qR qI))" proof - have "p \\<^sub>p [:a, b - a:] = cpoly_of pR pI" using cpoly_of_decompose pI_def pR_def by blast moreover have "q \\<^sub>p [:a, b - a:] = cpoly_of qR qI" using cpoly_of_decompose qI_def qR_def by blast ultimately show ?thesis apply (subst cindexP_lineE_polyE) unfolding pcompose_mult by simp qed also have "... = cindex_polyE 0 1 (pR * qI + pI * qR ) (pR * qR - pI * qI)" unfolding cpoly_of_times by (simp add:algebra_simps) also have "... = cindex_polyE 0 1 P1 P2" unfolding P1_def P2_def by simp also have "... = cindex_polyE 0 1 pI pR + cindex_polyE 0 1 qI qR + CR" proof - have "C1 P2 P1 = C1 pR pI + C1 qR qI - C2 P1 (pI * qI)" unfolding P1_def P2_def C1_def C2_def apply (rule cindex_polyE_product) thm cindex_polyE_product by simp fact+ moreover have "C1 P2 P1 = C2 P2 P1 - C1 P1 P2" unfolding C1_def C2_def apply (subst cindex_polyE_inverse_add_cross'[symmetric]) using P12_nzero by simp_all moreover have "C1 pR pI = C2 pR pI - C1 pI pR" unfolding C1_def C2_def apply (subst cindex_polyE_inverse_add_cross'[symmetric]) using p_nzero by simp_all moreover have "C1 qR qI = C2 qR qI - C1 qI qR" unfolding C1_def C2_def apply (subst cindex_polyE_inverse_add_cross'[symmetric]) using q_nzero by simp_all ultimately have "C2 P2 P1 - C1 P1 P2 = (C2 pR pI - C1 pI pR) + (C2 qR qI - C1 qI qR) - C2 P1 (pI * qI)" by auto then have "C1 P1 P2 = C1 pI pR + C1 qI qR + CR" unfolding CR_def by (auto simp:algebra_simps) then show ?thesis unfolding C1_def . qed also have "... = cindexP_lineE p a b +cindexP_lineE q a b + CR" unfolding C1_def pI_def pR_def qI_def qR_def apply (subst (1 2) cindexP_lineE_polyE) by simp also have "... = cindexP_lineE p a b +cindexP_lineE q a b + cdiff_aux p q a b/2" proof - have "CR = cdiff_aux p q a b/2" unfolding CR_def C2_def cross_alt_alt cdiff_aux_def psign_aux_def by (simp add:P1_poly P2_poly p_poly q_poly del:times_complex.sel) then show ?thesis by simp qed finally show ?thesis . qed lemma cindexP_lineE_changes: fixes p::"complex poly" and a b ::complex assumes "p\0" "a\b" shows "cindexP_lineE p a b = (let p1 = pcompose p [:a, b-a:]; pR1 = map_poly Re p1; pI1 = map_poly Im p1; gc1 = gcd pR1 pI1 in real_of_int (changes_alt_itv_smods 0 1 (pR1 div gc1) (pI1 div gc1)) / 2)" proof - define p1 pR1 pI1 gc1 where "p1 = pcompose p [:a, b-a:]" and "pR1 = map_poly Re p1" and "pI1 = map_poly Im p1" and "gc1 = gcd pR1 pI1" have "gc1 \0" proof (rule ccontr) assume "\ gc1 \ 0" then have "pI1 = 0" "pR1 = 0" unfolding gc1_def by auto then have "p1 = 0" unfolding pI1_def pR1_def by (metis cpoly_of_decompose map_poly_0) then have "p=0" unfolding p1_def apply (subst (asm) pcompose_eq_0) using \a\b\ by auto then show False using \p\0\ by auto qed have "cindexP_lineE p a b = cindexE 0 1 (\t. Im (poly p (linepath a b t)) / Re (poly p (linepath a b t)))" unfolding cindexP_lineE_def cindex_pathE_def cindexP_pathE_def by simp also have "... = cindexE 0 1 (\t. poly pI1 t / poly pR1 t)" unfolding pI1_def pR1_def p1_def poly_linepath_comp' by (simp add:Im_poly_of_real Re_poly_of_real) also have "... = cindex_polyE 0 1 pI1 pR1 " by (simp add: cindexE_eq_cindex_polyE) also have "... = cindex_polyE 0 1 (pI1 div gc1) (pR1 div gc1)" using \gc1\0\ apply (subst (2) cindex_polyE_mult_cancel[of gc1,symmetric]) by (simp_all add: gc1_def) also have "... = real_of_int (changes_alt_itv_smods 0 1 (pR1 div gc1) (pI1 div gc1)) / 2" apply (rule cindex_polyE_changes_alt_itv_mods) apply simp by (metis \gc1 \ 0\ div_gcd_coprime gc1_def gcd_eq_0_iff) finally show ?thesis by (metis gc1_def p1_def pI1_def pR1_def) qed lemma cindexP_lineE_code[code]: "cindexP_lineE p a b = (if p\0 \ a\b then (let p1 = pcompose p [:a, b-a:]; pR1 = map_poly Re p1; pI1 = map_poly Im p1; gc1 = gcd pR1 pI1 in real_of_int (changes_alt_itv_smods 0 1 (pR1 div gc1) (pI1 div gc1)) / 2) else Code.abort (STR ''cindexP_lineE fails for now'') (\_. cindexP_lineE p a b))" using cindexP_lineE_changes by auto end diff --git a/thys/Sturm_Tarski/PolyMisc.thy b/thys/Sturm_Tarski/PolyMisc.thy --- a/thys/Sturm_Tarski/PolyMisc.thy +++ b/thys/Sturm_Tarski/PolyMisc.thy @@ -1,165 +1,259 @@ (* Author: Wenda Li *) +section \Misc polynomial lemmas for the Sturm-Tarski theorem\ + theory PolyMisc imports "HOL-Computational_Algebra.Polynomial_Factorial" begin lemma coprime_poly_0: "poly p x \ 0 \ poly q x \ 0" if "coprime p q" for x :: "'a :: field" proof (rule ccontr) assume " \ (poly p x \ 0 \ poly q x \ 0)" then have "[:-x, 1:] dvd p" "[:-x, 1:] dvd q" by (simp_all add: poly_eq_0_iff_dvd) with that have "is_unit [:-x, 1:]" by (rule coprime_common_divisor) then show False by (auto simp add: is_unit_pCons_iff) qed lemma smult_cancel: fixes p::"'a::idom poly" assumes "c\0" and smult: "smult c p = smult c q" shows "p=q" proof - have "smult c (p-q)=0" using smult by (metis diff_self smult_diff_right) thus ?thesis using \c\0\ by auto qed lemma dvd_monic: fixes p q:: "'a :: idom poly" assumes monic:"lead_coeff p=1" and "p dvd (smult c q)" and "c\0" shows "p dvd q" using assms proof (cases "q=0 \ degree p=0") case True thus ?thesis using assms by (auto elim!: degree_eq_zeroE simp add: const_poly_dvd_iff) next case False hence "q\0" and "degree p\0" by auto obtain k where k:"smult c q = p*k" using assms dvd_def by metis hence "k\0" by (metis False assms(3) mult_zero_right smult_eq_0_iff) hence deg_eq:"degree q=degree p + degree k" by (metis False assms(3) degree_0 degree_mult_eq degree_smult_eq k) have c_dvd:"\n\degree k. c dvd coeff k (degree k - n)" proof (rule,rule) fix n assume "n \ degree k " thus "c dvd coeff k (degree k - n)" proof (induct n rule:nat_less_induct) case (1 n) define T where "T\(\i. coeff p i * coeff k (degree p+degree k - n - i))" have "c * coeff q (degree q - n) = (\i\degree q - n. coeff p i * coeff k (degree q - n - i))" using coeff_mult[of p k "degree q - n"] k coeff_smult[of c q "degree q -n"] by auto also have "...=(\i\degree p+degree k - n. T i)" using deg_eq unfolding T_def by auto also have "...=(\i\{0..{{0..A\C. finite A" unfolding C_def by auto moreover have "\A\C. \B\C. A \ B \ A \ B = {}" unfolding C_def by auto ultimately have "sum T (\C) = sum (sum T) C" using sum.Union_disjoint by auto moreover have "\C={..degree p + degree k - n}" using \n \ degree k\ unfolding C_def by auto moreover have "sum (sum T) C= sum T {0..{degree p}" by (metis atLeast0LessThan insertI1 lessThan_iff less_imp_not_eq) moreover have "{degree p}\{degree p + 1..degree p + degree k - n}" by (metis add.commute add_diff_cancel_right' atLeastAtMost_singleton_iff diff_self_eq_0 eq_imp_le not_one_le_zero) moreover have "{0..{degree p + 1..degree p + degree k - n}" using \degree k\n\ \degree p\0\ by fastforce ultimately show ?thesis unfolding C_def by auto qed ultimately show ?thesis by auto qed also have "...=(\i\{0..x\{degree p + 1..degree p + degree k - n}. T x=0" using coeff_eq_0[of p] unfolding T_def by simp hence "sum T {degree p + 1..degree p + degree k - n}=0" by auto moreover have "T (degree p)=coeff k (degree k - n)" using monic by (simp add: T_def) ultimately show ?thesis by auto qed finally have c_coeff: "c * coeff q (degree q - n) = sum T {0..0\c dvd sum T {0.. {0..0" hence "(n+i-degree p)\degree k" using \n \ degree k\ by auto moreover have "n + i - degree p n\0\ by auto ultimately have "c dvd coeff k (degree k - (n+i-degree p))" using 1(1) by auto hence "c dvd coeff k (degree p + degree k - n - i)" by (metis add_diff_cancel_left' deg_eq diff_diff_left dvd_0_right le_degree le_diff_conv add.commute ordered_cancel_comm_monoid_diff_class.diff_diff_right) thus "c dvd T i" unfolding T_def by auto qed moreover have "n=0 \?case" proof - assume "n=0" hence "\i\{0..n. c dvd coeff k n" by (metis diff_diff_cancel dvd_0_right le_add2 le_add_diff_inverse le_degree) then obtain f where f:"\n. c * f n=coeff k n" unfolding dvd_def by metis have " \\<^sub>\ n. f n = 0 " by (metis (mono_tags, lifting) MOST_coeff_eq_0 MOST_mono assms(3) f mult_eq_0_iff) hence "smult c (Abs_poly f)=k" using f smult.abs_eq[of c "Abs_poly f"] Abs_poly_inverse[of f] coeff_inverse[of k] by simp hence "q=p* Abs_poly f" using k \c\0\ smult_cancel by auto thus ?thesis unfolding dvd_def by auto qed lemma poly_power_n_eq: fixes x::"'a :: idom" assumes "n\0" shows "poly ([:-a,1:]^n) x=0 \ (x=a)" using assms by (induct n,auto) lemma poly_power_n_odd: fixes x a:: real assumes "odd n" shows "poly ([:-a,1:]^n) x>0 \ (x>a)" using assms proof - have "poly ([:-a,1:]^n) x\0 = (poly [:- a, 1:] x \0)" unfolding poly_power using zero_le_odd_power[OF \odd n\] by blast also have "(poly [:- a, 1:] x \0) = (x\a)" by fastforce finally have "poly ([:-a,1:]^n) x\0 = (x\a)" . moreover have "poly ([:-a,1:]^n) x=0 = (x=a)" by(rule poly_power_n_eq, metis assms even_zero) ultimately show ?thesis by linarith qed lemma gcd_coprime_poly: fixes p q::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize} poly" assumes nz: "p \ 0 \ q \ 0" and p': "p = p' * gcd p q" and q': "q = q' * gcd p q" shows "coprime p' q'" using gcd_coprime nz p' q' by auto lemma poly_mod: "poly (p mod q) x = poly p x" if "poly q x = 0" proof - from that have "poly (p mod q) x = poly (p div q * q) x + poly (p mod q) x" by simp also have "\ = poly p x" by (simp only: poly_add [symmetric]) simp finally show ?thesis . qed +lemma pseudo_divmod_0[simp]: "pseudo_divmod f 0 = (0,f)" + unfolding pseudo_divmod_def by auto + +lemma map_poly_eq_iff: + assumes "f 0=0" "inj f" + shows "map_poly f x =map_poly f y \ x=y" + using assms + by (auto simp: poly_eq_iff coeff_map_poly dest:injD) + +lemma pseudo_mod_0[simp]: + shows "pseudo_mod p 0= p" "pseudo_mod 0 q = 0" + unfolding pseudo_mod_def pseudo_divmod_def by (auto simp add: length_coeffs_degree) + +lemma pseudo_mod_mod: + assumes "g\0" + shows "smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g" +proof - + define a where "a=lead_coeff g ^ (Suc (degree f) - degree g)" + have "a\0" unfolding a_def by (simp add: assms) + define r where "r = pseudo_mod f g" + define r' where "r' = pseudo_mod (smult (1/a) f) g" + obtain q where pdm: "pseudo_divmod f g = (q,r)" using r_def[unfolded pseudo_mod_def] + apply (cases "pseudo_divmod f g") + by auto + obtain q' where pdm': "pseudo_divmod (smult (1/a) f) g = (q',r')" using r'_def[unfolded pseudo_mod_def] + apply (cases "pseudo_divmod (smult (1/a) f) g") + by auto + have "smult a f = q * g + r" and deg_r:"r = 0 \ degree r < degree g" + using pseudo_divmod[OF assms pdm] unfolding a_def by auto + moreover have "f = q' * g + r'" and deg_r':"r' = 0 \ degree r' < degree g" + using \a\0\ pseudo_divmod[OF assms pdm'] unfolding a_def degree_smult_eq + by auto + ultimately have gr:"(smult a q' - q) * g = r - smult a r'" + by (auto simp add:smult_add_right algebra_simps) + have "smult a r' = r" when "r=0" "r'=0" + using that by auto + moreover have "smult a r' = r" when "r\0 \ r'\0" + proof - + have "smult a q' - q =0" + proof (rule ccontr) + assume asm:"smult a q' - q \ 0 " + have "degree (r - smult a r') < degree g" + using deg_r deg_r' degree_diff_less that by force + also have "... \ degree (( smult a q' - q)*g)" + using degree_mult_right_le[OF asm,of g] by (simp add: mult.commute) + also have "... = degree (r - smult a r')" + using gr by auto + finally have "degree (r - smult a r') < degree (r - smult a r')" . + then show False by simp + qed + then show ?thesis using gr by auto + qed + ultimately have "smult a r' = r" by argo + then show ?thesis unfolding r_def r'_def a_def mod_poly_def + using assms by (auto simp add:field_simps) +qed + +lemma poly_pseudo_mod: + assumes "poly q x=0" "q\0" + shows "poly (pseudo_mod p q) x = (lead_coeff q ^ (Suc (degree p) - degree q)) * poly p x" +proof - + define a where "a=coeff q (degree q) ^ (Suc (degree p) - degree q)" + obtain f r where fr:"pseudo_divmod p q = (f, r)" by fastforce + then have "smult a p = q * f + r" "r = 0 \ degree r < degree q" + using pseudo_divmod[OF \q\0\] unfolding a_def by auto + then have "poly (q*f+r) x = poly (smult a p) x" by auto + then show ?thesis + using assms(1) fr unfolding pseudo_mod_def a_def + by auto +qed + +lemma degree_less_timesD: + fixes q::"'a::idom poly" + assumes "q*g=r" and deg:"r=0 \ degree g>degree r" and "g\0" + shows "q=0 \ r=0" +proof - + have ?thesis when "r=0" + using assms(1) assms(3) no_zero_divisors that by blast + moreover have False when "r\0" + proof - + have "degree r < degree g" + using deg that by auto + also have "... \ degree (q*g)" + by (metis assms(1) degree_mult_right_le mult.commute mult_not_zero that) + also have "... = degree r" + using assms(1) by simp + finally have "degree rAn implementation for calculating pseudo remainder sequences\ + +theory Pseudo_Remainder_Sequence + imports Sturm_Tarski + "HOL-Computational_Algebra.Computational_Algebra" + + (*TODO: we should consider to move this to the standard library*) + "Polynomial_Interpolation.Ring_Hom_Poly" +begin + +subsection \Misc\ + +function spmods :: "'a::idom poly \ 'a poly \ ('a poly) list" where + "spmods p q= (if p=0 then [] else + let + m=(if even(degree p+1-degree q) then -1 else -lead_coeff q) + in + Cons p (spmods q (smult m (pseudo_mod p q))))" +by auto +termination + apply (relation "measure (\(p,q).if p=0 then 0 else if q=0 then 1 else 2+degree q)") + by (simp_all add: degree_pseudo_mod_less) + +declare spmods.simps[simp del] + +lemma spmods_0[simp]: + "spmods 0 q = []" + "spmods p 0 = (if p=0 then [] else [p])" +by (auto simp:spmods.simps) + +lemma spmods_nil_eq:"spmods p q = [] \ (p=0)" + by (metis list.distinct(1) spmods.elims) + +lemma changes_poly_at_alternative: + "changes_poly_at ps a= changes (map (\p. sign(poly p a)) ps)" + "changes_poly_at ps a= changes (map (\p. sgn(poly p a)) ps)" + unfolding changes_poly_at_def + subgoal by (subst changes_map_sign_eq) (auto simp add:comp_def) + subgoal by (subst changes_map_sgn_eq) (auto simp add:comp_def) + done + +lemma smods_smult_length: + assumes "a\0" "b\0" + shows "length (smods p q) = length (smods (smult a p) (smult b q))" using assms +proof (induct "smods p q" arbitrary:p q a b ) + case Nil + thus ?case by (simp split:if_splits) +next + case (Cons x xs) + hence "p\0" by auto + define r where "r\- (p mod q)" + have "smods q r = xs" using Cons.hyps(2) `p\0` unfolding r_def by auto + hence "length (smods q r) = length (smods (smult b q) (smult a r))" + using Cons.hyps(1)[of q r b a] Cons by auto + moreover have "smult a p\0" using `a\0` `p\0` by auto + moreover have "-((smult a p) mod (smult b q)) = (smult a r)" + using Polynomial.mod_smult_left Polynomial.mod_smult_right[OF `b\0`] + unfolding r_def by simp + ultimately show ?case + unfolding r_def by auto +qed + +lemma smods_smult_nth[rule_format]: + fixes p q::"real poly" + assumes "a\0" "b\0" + defines "xs\smods p q" and "ys\smods (smult a p) (smult b q)" + shows "\n0" by auto + define r where "r\- (p mod q)" + have xs:"xs=smods q r" "p#xs=smods p q" using Cons.hyps(2) `p\0` unfolding r_def by auto + define ys where "ys\smods (smult b q) (smult a r)" + have "- ((smult a p) mod (smult b q)) = smult a r" + using mod_smult_right[OF `b\0`, of "smult a p" q,unfolded mod_smult_left[where y=q]] + unfolding r_def by auto + hence ys:"smult a p # ys = smods (smult a p) (smult b q)" using `p\0` `a\0` + unfolding ys_def r_def by auto + have hyps:"\n. n ys ! n = (if even n then smult b (xs ! n) else smult a (xs ! n))" + using Cons.hyps(1)[of q r b a,folded xs ys_def] `a\0` `b\0` by auto + thus ?case + apply (fold xs ys) + apply auto + by (case_tac n,auto)+ +qed + +lemma smods_smult_sgn_map_eq: + fixes x::real + assumes "m>0" + defines "f\\p. sgn(poly p x)" + shows "map f (smods p (smult m q)) = map f (smods p q)" + "map sgn_pos_inf (smods p (smult m q)) = map sgn_pos_inf (smods p q)" + "map sgn_neg_inf (smods p (smult m q)) = map sgn_neg_inf (smods p q)" +proof - + define xs ys where "xs\smods p q" and "ys\smods p (smult m q)" + have "m\0" using `m>0` by simp + have len_eq:"length xs =length ys" + using smods_smult_length[of 1 m] `m>0` unfolding xs_def ys_def by auto + moreover have + "(map f xs) ! i = (map f ys) ! i" + "(map sgn_pos_inf xs) ! i = (map sgn_pos_inf ys) ! i" + "(map sgn_neg_inf xs) ! i = (map sgn_neg_inf ys) ! i" + when "i0`,of _ p q,unfolded smult_1_left, + folded xs_def ys_def,OF `i0` + by (auto simp add:sgn_mult sgn_pos_inf_def sgn_neg_inf_def lead_coeff_smult) + qed + ultimately show "map f (smods p (smult m q)) = map f (smods p q)" + "map sgn_pos_inf (smods p (smult m q)) = map sgn_pos_inf (smods p q)" + "map sgn_neg_inf (smods p (smult m q)) = map sgn_neg_inf (smods p q)" + apply (fold xs_def ys_def) + by (auto intro: nth_equalityI) +qed + +lemma changes_poly_at_smods_smult: + assumes "m>0" + shows "changes_poly_at (smods p (smult m q)) x =changes_poly_at (smods p q) x " + using smods_smult_sgn_map_eq[OF `m>0`] + by (metis changes_poly_at_alternative(2)) + +lemma spmods_smods_sgn_map_eq: + fixes p q::"real poly" and x::real + defines "f\\p. sgn (poly p x)" + shows "map f (smods p q) = map f (spmods p q)" + "map sgn_pos_inf (smods p q) = map sgn_pos_inf (spmods p q)" + "map sgn_neg_inf (smods p q) = map sgn_neg_inf (spmods p q)" +proof (induct "spmods p q" arbitrary:p q) + case Nil + hence "p=0" using spmods_nil_eq by metis + thus "map f (smods p q) = map f (spmods p q)" + "map sgn_pos_inf (smods p q) = map sgn_pos_inf (spmods p q)" + "map sgn_neg_inf (smods p q) = map sgn_neg_inf (spmods p q)" + by auto +next + case (Cons p' xs) + hence "p\0" by auto + define r where "r\- (p mod q)" + define exp where " exp\degree p +1 - degree q" + define m where "m\(if even exp then 1 else lead_coeff q) + * (lead_coeff q ^ exp)" + have xs1:"p#xs=spmods p q" + by (metis (no_types) Cons.hyps(4) list.distinct(1) list.inject spmods.simps) + have xs2:"xs=spmods q (smult m r)" when "q\0" + proof - + define m' where "m'\if even exp then - 1 else - lead_coeff q" + have "smult m' (pseudo_mod p q) = smult m r" + unfolding m_def m'_def r_def + apply (subst pseudo_mod_mod[symmetric]) + using that exp_def by auto + thus ?thesis using `p\0` xs1 unfolding r_def + by (simp add:spmods.simps[of p q,folded exp_def, folded m'_def] del:spmods.simps) + qed + define ys where "ys\smods q r" + have ys:"p#ys=smods p q" using `p\0` unfolding ys_def r_def by auto + have qm:"q\0 \ m>0" + using `p\0` unfolding m_def + apply auto + subgoal by (simp add: zero_less_power_eq) + subgoal using zero_less_power_eq by fastforce + done + show "map f (smods p q) = map f (spmods p q)" + proof (cases "q\0") + case True + then have "map f (spmods q (smult m r)) = map f (smods q r)" + using smods_smult_sgn_map_eq(1)[of m x q r,folded f_def] qm + Cons.hyps(1)[OF xs2,folded f_def] + by simp + thus ?thesis + apply (fold xs1 xs2[OF True] ys ys_def) + by auto + next + case False + thus ?thesis by auto + qed + show "map sgn_pos_inf (smods p q) = map sgn_pos_inf (spmods p q)" + proof (cases "q\0") + case True + then have "map sgn_pos_inf (spmods q (smult m r)) = map sgn_pos_inf (smods q r)" + using Cons.hyps(2)[OF xs2,folded f_def] qm[OF True] + smods_smult_sgn_map_eq(2)[of m q r,folded f_def] by auto + thus ?thesis + apply (fold xs1 xs2[OF True] ys ys_def) + by (simp add:f_def) + next + case False + thus ?thesis by auto + qed + show "map sgn_neg_inf (smods p q) = map sgn_neg_inf (spmods p q)" + proof (cases "q\0") + case True + then have "map sgn_neg_inf (spmods q (smult m r)) = map sgn_neg_inf (smods q r)" + using Cons.hyps(3)[OF xs2,folded f_def] qm[OF True] + smods_smult_sgn_map_eq(3)[of m q r,folded f_def] by auto + thus ?thesis + apply (fold xs1 xs2[OF True] ys ys_def) + by (simp add:f_def) + next + case False + thus ?thesis by auto + qed +qed + +subsection \Converting @{typ "rat poly"} to @{typ "int poly"} by clearing the denominators\ + +definition int_of_rat::"rat \ int" where + "int_of_rat = inv of_int" + +lemma of_rat_inj[simp]: "inj of_rat" +by (simp add: linorder_injI) + +lemma (in ring_char_0) of_int_inj[simp]: "inj of_int" + by (simp add: inj_on_def) + +lemma int_of_rat_id: "int_of_rat o of_int = id" + unfolding int_of_rat_def + by auto + +lemma int_of_rat_0[simp]:"int_of_rat 0 = 0" + by (metis id_apply int_of_rat_id o_def of_int_0) + +lemma int_of_rat_inv:"r\\ \ of_int (int_of_rat r) = r" +unfolding int_of_rat_def +by (simp add: Ints_def f_inv_into_f) + +lemma int_of_rat_0_iff:"x\\ \ int_of_rat x = 0 \ x = 0" +using int_of_rat_inv by force + +lemma [code]:"int_of_rat r = (let (a,b) = quotient_of r in + if b=1 then a else Code.abort (STR ''Failed to convert rat to int'') + (\_. int_of_rat r))" + apply (auto simp add:split_beta int_of_rat_def) + by (metis Fract_of_int_quotient inv_f_eq of_int_inj of_int_rat quotient_of_div surjective_pairing) + +definition de_lcm::"rat poly \ int" where + "de_lcm p = Lcm(set(map (\x. snd (quotient_of x)) (coeffs p)))" + +lemma de_lcm_pCons:"de_lcm (pCons a p) = lcm (snd (quotient_of a)) (de_lcm p)" + unfolding de_lcm_def + by (cases "a=0\p=0",auto) + +lemma de_lcm_0[simp]:"de_lcm 0 = 1" unfolding de_lcm_def by auto + +lemma de_lcm_pos[simp]:"de_lcm p > 0" + apply (induct p) + apply (auto simp add:de_lcm_pCons) + by (metis lcm_pos_int less_numeral_extra(3) quotient_of_denom_pos')+ + +lemma de_lcm_ints: + fixes x::rat + shows "x\set (coeffs p) \ rat_of_int (de_lcm p) * x \ \" +proof (induct p) + case 0 + then show ?case by auto +next + case (pCons a p) + define a1 a2 where "a1\fst (quotient_of a)" and "a2\snd (quotient_of a)" + have a:"a=(rat_of_int a1)/(rat_of_int a2)" and "a2>0" + using quotient_of_denom_pos'[of a] unfolding a1_def a2_def + by (auto simp add: quotient_of_div) + define mp1 where "mp1\a2 div gcd (de_lcm p) a2" + define mp2 where "mp2\de_lcm p div gcd a2 (de_lcm p) " + have lcm_times1:"lcm a2 (de_lcm p) = de_lcm p * mp1" + using lcm_altdef_int[of "de_lcm p" a2,folded mp1_def] `a2>0` + unfolding mp1_def + apply (subst div_mult_swap) + by (auto simp add: abs_of_pos gcd.commute lcm_altdef_int mult.commute) + have lcm_times2:"lcm a2 (de_lcm p) = a2 * mp2" + using lcm_altdef_int[of a2 "de_lcm p",folded mp1_def] `a2>0` + unfolding mp2_def by (subst div_mult_swap, auto simp add:abs_of_pos) + show ?case + proof (cases "x \ set (coeffs p)") + case True + show ?thesis using pCons(2)[OF True] + by (smt Ints_mult Ints_of_int a2_def de_lcm_pCons lcm_times1 + mult.assoc mult.commute of_int_mult) + next + case False + then have "x=a" + using pCons cCons_not_0_eq coeffs_pCons_eq_cCons insert_iff list.set(2) not_0_cCons_eq + by fastforce + show ?thesis unfolding `x=a` de_lcm_pCons + apply (fold a2_def,unfold a) + by (simp add: de_lcm_pCons lcm_times2 of_rat_divide) + qed +qed + +definition clear_de::"rat poly \ int poly" where + "clear_de p = (SOME q. (map_poly of_int q) = smult (of_int (de_lcm p)) p)" + +lemma clear_de:"of_int_poly(clear_de p) = smult (of_int (de_lcm p)) p" +proof - + have "\q. (of_int_poly q) = smult (of_int (de_lcm p)) p" + proof (induct p) + case 0 + show ?case by (metis map_poly_0 smult_0_right) + next + case (pCons a p) + then obtain q1::"int poly" where q1:"of_int_poly q1 = smult (rat_of_int (de_lcm p)) p" + by auto + define a1 a2 where "a1\fst (quotient_of a)" and "a2\snd (quotient_of a)" + have a:"a=(rat_of_int a1)/ (rat_of_int a2)" and "a2>0" + using quotient_of_denom_pos' quotient_of_div + unfolding a1_def a2_def by auto + define mp1 where "mp1\a2 div gcd (de_lcm p) a2" + define mp2 where "mp2\de_lcm p div gcd a2 (de_lcm p) " + have lcm_times1:"lcm a2 (de_lcm p) = de_lcm p * mp1" + using lcm_altdef_int[of "de_lcm p" a2,folded mp1_def] `a2>0` + unfolding mp1_def + by (subst div_mult_swap, auto simp add: abs_of_pos gcd.commute lcm_altdef_int mult.commute) + have lcm_times2:"lcm a2 (de_lcm p) = a2 * mp2" + using lcm_altdef_int[of a2 "de_lcm p",folded mp1_def] `a2>0` + unfolding mp2_def by (subst div_mult_swap, auto simp add:abs_of_pos) + define q2 where "q2\pCons (mp2 * a1) (smult mp1 q1)" + have "of_int_poly q2 = smult (rat_of_int (de_lcm (pCons a p))) (pCons a p)" using `a2>0` + apply (simp add:de_lcm_pCons ) + apply (fold a2_def) + apply (unfold a) + apply (subst lcm_times2,subst lcm_times1) + by (simp add: Polynomial.map_poly_pCons mult.commute of_int_hom.map_poly_hom_smult q1 q2_def) + then show ?case by auto + qed + then show ?thesis unfolding clear_de_def by (meson someI_ex) +qed + +lemma clear_de_0[simp]:"clear_de 0 = 0" + using clear_de[of 0] by auto + +lemma [code abstract]: "coeffs (clear_de p) = + (let lcm = de_lcm p in map (\x. int_of_rat (of_int lcm * x)) (coeffs p))" +proof - + define mul where "mul\rat_of_int (de_lcm p)" + have "map_poly int_of_rat (of_int_poly q) = q" for q + apply (subst map_poly_map_poly) + by (auto simp add:int_of_rat_id) + then have clear_eq:"clear_de p = map_poly int_of_rat (smult (of_int (de_lcm p)) p)" + using arg_cong[where f="map_poly int_of_rat",OF clear_de] + by auto + show ?thesis + proof (cases "p=0") + case True + then show ?thesis by auto + next + case False + define g where "g\(\x. int_of_rat (rat_of_int (de_lcm p) * x))" + have "de_lcm p \ 0" using de_lcm_pos by (metis less_irrefl) + moreover have "last (coeffs p) \0" + by (simp add: False last_coeffs_eq_coeff_degree) + have False when asm:"last (map g (coeffs p)) =0" + proof - + have "coeffs p \[]" using False by auto + hence "g (last (coeffs p)) = 0" using asm last_map[of "coeffs p" g] by auto + hence "last (coeffs p) = 0" + unfolding g_def using `coeffs p \[]` `de_lcm p \ 0` + apply (subst (asm) int_of_rat_0_iff) + by (auto intro!: de_lcm_ints ) + thus False using `last (coeffs p) \0` by simp + qed + ultimately show ?thesis + apply (auto simp add: coeffs_smult clear_eq comp_def smult_conv_map_poly map_poly_map_poly coeffs_map_poly) + apply (fold g_def) + by (metis False Ring_Hom_Poly.coeffs_map_poly coeffs_eq_Nil last_coeffs_eq_coeff_degree + last_map) + qed +qed + + +subsection \Sign variations for pseudo-remainder sequences\ + +locale order_hom = + fixes hom :: "'a :: ord \ 'b :: ord" + assumes hom_less: "x < y \ hom x < hom y" + and hom_less_eq: "x \ y \ hom x \ hom y" + +locale linordered_idom_hom = order_hom hom + inj_idom_hom hom + for hom :: "'a :: linordered_idom \ 'b :: linordered_idom" +begin + +lemma sgn_sign:"sgn (hom x) = of_int (sign x)" + by (simp add: sign_def hom_less sgn_if) + +end + +locale hom_pseudo_smods= comm_semiring_hom hom + + r1:linordered_idom_hom R\<^sub>1 + r2:linordered_idom_hom R\<^sub>2 + for hom::"'a::linordered_idom \ 'b::{comm_semiring_1,linordered_idom}" + and R\<^sub>1::"'a \ real" + and R\<^sub>2::"'b \ real" + + assumes R_hom:"R\<^sub>1 x = R\<^sub>2 (hom x)" +begin + +(* + hom R2 + +'a \ 'b \ real + rat/float +int +p + x +*) + +lemma map_poly_R_hom_commute: + "poly (map_poly R\<^sub>1 p) (R\<^sub>2 x) = R\<^sub>2 (poly (map_poly hom p) x)" +apply (induct p) +using r2.hom_add r2.hom_mult R_hom by auto + +definition changes_hpoly_at::"'a poly list \ 'b \ int" where + "changes_hpoly_at ps a= changes (map (\p. eval_poly hom p a) ps)" + +lemma changes_hpoly_at_Nil[simp]: "changes_hpoly_at [] a = 0" + unfolding changes_hpoly_at_def by simp + +definition changes_itv_spmods:: "'b \ 'b \ 'a poly \ 'a poly \ int" where + "changes_itv_spmods a b p q= (let ps = spmods p q in + changes_hpoly_at ps a - changes_hpoly_at ps b)" + +definition changes_gt_spmods:: "'b \ 'a poly \ 'a poly \ int" where + "changes_gt_spmods a p q= (let ps = spmods p q in + changes_hpoly_at ps a - changes_poly_pos_inf ps)" + +definition changes_le_spmods:: "'b \ 'a poly \ 'a poly \ int" where + "changes_le_spmods b p q= (let ps = spmods p q in + changes_poly_neg_inf ps - changes_hpoly_at ps b)" + +definition changes_R_spmods:: "'a poly \ 'a poly \ int" where + "changes_R_spmods p q= (let ps= spmods p q in changes_poly_neg_inf ps + - changes_poly_pos_inf ps)" + +lemma changes_spmods_smods: + shows "changes_itv_spmods a b p q + = changes_itv_smods (R\<^sub>2 a) (R\<^sub>2 b) (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + and "changes_R_spmods p q = changes_R_smods (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + and "changes_gt_spmods a p q = changes_gt_smods (R\<^sub>2 a) (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + and "changes_le_spmods b p q = changes_le_smods (R\<^sub>2 b) (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" +proof - + define pp qq where "pp = map_poly R\<^sub>1 p" and "qq = map_poly R\<^sub>1 q" + + have spmods_eq:"spmods (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q) = map (map_poly R\<^sub>1) (spmods p q)" + proof (induct "spmods p q" arbitrary:p q ) + case Nil + thus ?case by (metis list.simps(8) map_poly_0 spmods_nil_eq) + next + case (Cons p' xs) + hence "p\0" by auto + define m where "m\(if even (degree p + 1 - degree q) then - 1 else - lead_coeff q)" + define r where "r\smult m (pseudo_mod p q)" + have xs1:"p#xs=spmods p q" + by (metis (no_types) Cons.hyps(2) list.distinct(1) list.inject spmods.simps) + have xs2:"xs=spmods q r" using xs1 \p\0\ r_def + by (auto simp add:spmods.simps[of p q,folded exp_def,folded m_def]) + define ys where "ys\spmods (map_poly R\<^sub>1 q) (map_poly R\<^sub>1 r)" + have ys:"(map_poly R\<^sub>1 p)#ys=spmods (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + using \p\0\ unfolding ys_def r_def + apply (subst (2) spmods.simps) + unfolding m_def by (auto simp:r1.pseudo_mod_hom hom_distribs) + show ?case using Cons.hyps(1)[OF xs2] + apply (fold xs1 xs2 ys ys_def) + by auto + qed + + have changes_eq_at:"changes_poly_at (smods pp qq) (R\<^sub>2 x) = changes_hpoly_at (spmods p q) x" + (is "?L=?R") + for x + proof - + define ff where "ff = (\p. sgn (poly p (R\<^sub>2 x)))" + have "?L = changes (map ff (smods pp qq))" + using changes_poly_at_alternative unfolding ff_def by blast + also have "... = changes (map ff (spmods pp qq))" + unfolding ff_def using spmods_smods_sgn_map_eq by simp + also have "... = changes (map ff (map (map_poly R\<^sub>1) (spmods p q)))" + unfolding pp_def qq_def using spmods_eq by simp + also have "... = ?R" + proof - + have "ff \ map_poly R\<^sub>1 = sign \ (\p. eval_poly hom p x)" + unfolding ff_def comp_def + by (simp add: map_poly_R_hom_commute poly_map_poly_eval_poly r2.sgn_sign) + then show ?thesis + unfolding changes_hpoly_at_def + apply (subst (2) changes_map_sign_of_int_eq) + by (simp add:comp_def) + qed + finally show ?thesis . + qed + + have changes_eq_neg_inf: + "changes_poly_neg_inf (smods pp qq) = changes_poly_neg_inf (spmods p q)" + (is "?L=?R") + proof - + have "?L = changes (map sgn_neg_inf (map (map_poly R\<^sub>1) (spmods p q)))" + unfolding changes_poly_neg_inf_def spmods_smods_sgn_map_eq + by (simp add: spmods_eq[folded pp_def qq_def]) + also have "... = changes (map (sgn_neg_inf \ (map_poly R\<^sub>1)) (spmods p q))" + using map_map by simp + also have "... = changes (map ((sign:: _ \ real) \ sgn_neg_inf) (spmods p q))" + proof - + have "(sgn_neg_inf \ (map_poly R\<^sub>1)) = of_int o sign \ sgn_neg_inf" + unfolding sgn_neg_inf_def comp_def + by (auto simp:r1.sgn_sign) + then show ?thesis by (simp add:comp_def) + qed + also have "... = changes (map sgn_neg_inf (spmods p q))" + apply (subst (2) changes_map_sign_of_int_eq) + by (simp add:comp_def) + also have "... = ?R" + unfolding changes_poly_neg_inf_def by simp + finally show ?thesis . + qed + + have changes_eq_pos_inf: + "changes_poly_pos_inf (smods pp qq) = changes_poly_pos_inf (spmods p q)" + (is "?L=?R") + proof - + have "?L = changes (map sgn_pos_inf (map (map_poly R\<^sub>1) (spmods p q)))" + unfolding changes_poly_pos_inf_def spmods_smods_sgn_map_eq + by (simp add: spmods_eq[folded pp_def qq_def]) + also have "... = changes (map (sgn_pos_inf \ (map_poly R\<^sub>1)) (spmods p q))" + using map_map by simp + also have "... = changes (map ((sign:: _ \ real) \ sgn_pos_inf) (spmods p q))" + proof - + have "(sgn_pos_inf \ (map_poly R\<^sub>1)) = of_int o sign \ sgn_pos_inf" + unfolding sgn_pos_inf_def comp_def + by (auto simp:r1.sgn_sign) + then show ?thesis by (auto simp:comp_def) + qed + also have "... = changes (map sgn_pos_inf (spmods p q))" + apply (subst (2) changes_map_sign_of_int_eq) + by (simp add:comp_def) + also have "... = ?R" + unfolding changes_poly_pos_inf_def by simp + finally show ?thesis . + qed + + show "changes_itv_spmods a b p q + = changes_itv_smods (R\<^sub>2 a) (R\<^sub>2 b) (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + unfolding changes_itv_spmods_def changes_itv_smods_def + using changes_eq_at by (simp add: Let_def pp_def qq_def) + show "changes_R_spmods p q = changes_R_smods (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + unfolding changes_R_spmods_def changes_R_smods_def Let_def + using changes_eq_neg_inf changes_eq_pos_inf + by (simp add: pp_def qq_def) + show "changes_gt_spmods a p q = changes_gt_smods + (R\<^sub>2 a) (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + unfolding changes_gt_spmods_def changes_gt_smods_def Let_def + using changes_eq_at changes_eq_pos_inf + by (simp add: pp_def qq_def) + show "changes_le_spmods b p q = changes_le_smods + (R\<^sub>2 b) (map_poly R\<^sub>1 p) (map_poly R\<^sub>1 q)" + unfolding changes_le_spmods_def changes_le_smods_def Let_def + using changes_eq_at changes_eq_neg_inf + by (simp add: pp_def qq_def) +qed + +end + +end \ No newline at end of file diff --git a/thys/Sturm_Tarski/Sturm_Tarski.thy b/thys/Sturm_Tarski/Sturm_Tarski.thy --- a/thys/Sturm_Tarski/Sturm_Tarski.thy +++ b/thys/Sturm_Tarski/Sturm_Tarski.thy @@ -1,1676 +1,1705 @@ (* Title: Sturm-Tarski Theorem Author: Wenda Li *) section "Sturm-Tarski Theorem" theory Sturm_Tarski imports Complex_Main PolyMisc "HOL-Computational_Algebra.Field_as_Ring" begin -section\Misc\ +subsection\Misc\ lemma eventually_at_right: fixes x::"'a::{archimedean_field,linorder_topology}" shows "eventually P (at_right x) \ (\b>x. \y>x. y < b \ P y)" proof - obtain y where "y>x" using ex_less_of_int by auto thus ?thesis using eventually_at_right[OF \y>x\] by auto qed lemma eventually_at_left: fixes x::"'a::{archimedean_field,linorder_topology}" shows "eventually P (at_left x) \ (\by>b. y < x \ P y)" proof - obtain y where "yy] by auto qed lemma eventually_neg: assumes "F\bot" and eve:"eventually (\x. P x) F" shows "\ eventually (\x. \ P x) F" proof (rule ccontr) assume "\ \ eventually (\x. \ P x) F" hence "eventually (\x. \ P x) F" by auto hence "eventually (\x. False) F" using eventually_conj[OF eve,of "(\x. \ P x)"] by auto thus False using \F\bot\ eventually_False by auto qed lemma poly_tendsto[simp]: "(poly p \ poly p x) (at (x::real))" "(poly p \ poly p x) (at_left (x::real))" "(poly p \ poly p x) (at_right (x::real))" using isCont_def[where f="poly p"] by (auto simp add:filterlim_at_split) lemma not_eq_pos_or_neg_iff_1: fixes p::"real poly" shows "(\z. lbz\ub\poly p z\0) \ (\z. lbz\ub\poly p z>0)\(\z. lbz\ub\poly p z<0)" (is "?Q \ ?P") proof (rule,rule ccontr) assume "?Q" "\?P" then obtain z1 z2 where z1:"lbub" "poly p z1\0" and z2:"lbub" "poly p z2\0" by auto hence "\z. lbz\ub\poly p z=0" proof (cases "poly p z1 = 0 \ poly p z2 =0 \ z1=z2") case True thus ?thesis using z1 z2 by auto next case False hence "poly p z1<0" and "poly p z2>0" and "z1\z2" using z1(3) z2(3) by auto hence "(\z>z1. z < z2 \ poly p z = 0) \ (\z>z2. z < z1 \ poly p z = 0)" using poly_IVT_neg poly_IVT_pos by (subst (asm) linorder_class.neq_iff,auto) thus ?thesis using z1(1,2) z2(1,2) by (metis less_eq_real_def order.strict_trans2) qed thus False using \?Q\ by auto next assume "?P" thus ?Q by auto qed lemma not_eq_pos_or_neg_iff_2: fixes p::"real poly" shows "(\z. lb\z\zpoly p z\0) \(\z. lb\z\zpoly p z>0)\(\z. lb\z\zpoly p z<0)" (is "?Q\?P") proof (rule,rule ccontr) assume "?Q" "\?P" then obtain z1 z2 where z1:"lb\z1" "z10" and z2:"lb\z2" "z20" by auto hence "\z. lb\z\zpoly p z=0" proof (cases "poly p z1 = 0 \ poly p z2 =0 \ z1=z2") case True thus ?thesis using z1 z2 by auto next case False hence "poly p z1<0" and "poly p z2>0" and "z1\z2" using z1(3) z2(3) by auto hence "(\z>z1. z < z2 \ poly p z = 0) \ (\z>z2. z < z1 \ poly p z = 0)" using poly_IVT_neg poly_IVT_pos by (subst (asm) linorder_class.neq_iff,auto) thus ?thesis using z1(1,2) z2(1,2) by (meson dual_order.strict_trans not_le) qed thus False using \?Q\ by auto next assume "?P" thus ?Q by auto qed lemma next_non_root_interval: fixes p::"real poly" assumes "p\0" obtains ub where "ub>lb" and "(\z. lbz\ub\poly p z\0)" proof (cases "(\ r. poly p r=0 \ r>lb)") case False thus ?thesis by (intro that[of "lb+1"],auto) next case True define lr where "lr\Min {r . poly p r=0 \ r>lb}" have "\z. lbzpoly p z\0" and "lr>lb" using True lr_def poly_roots_finite[OF \p\0\] by auto thus ?thesis using that[of "(lb+lr)/2"] by auto qed lemma last_non_root_interval: fixes p::"real poly" assumes "p\0" obtains lb where "lbz. lb\z\zpoly p z\0)" proof (cases "(\ r. poly p r=0 \ rMax {r . poly p r=0 \ rz. mrzpoly p z\0" and "mrp\0\] by auto thus ?thesis using that[of "(mr+ub)/2"] \mr by auto qed -section\Bound of polynomials\ +subsection\Sign\ + +definition sign:: "'a::{zero,linorder} \ int" where + "sign x\(if x>0 then 1 else if x=0 then 0 else -1)" + +lemma sign_simps[simp]: + "x>0 \ sign x=1" + "x=0 \ sign x=0" + "x<0 \ sign x=-1" +unfolding sign_def by auto + +lemma sign_cases [case_names neg zero pos]: + "(sign x = -1 \ P) \ (sign x = 0 \ P) \ (sign x =1 \ P) \ P" +unfolding Sturm_Tarski.sign_def by argo + +lemma sign_times: + fixes x::"'a::linordered_ring_strict" + shows "sign (x*y) = sign x * sign y" + unfolding Sturm_Tarski.sign_def + by (auto simp add:zero_less_mult_iff) + +lemma sign_power: + fixes x::"'a::linordered_idom" + shows "sign (x^n) = (if n=0 then 1 else if even n then \sign x\ else sign x)" + by (simp add: Sturm_Tarski.sign_def zero_less_power_eq) + +(* +lemma sgn_sign_eq: + fixes x::"'a::{linordered_idom}" + shows "sgn x = of_int (sign x)" + unfolding sgn_if by auto +*) + +lemma sgn_sign_eq:"sgn = sign" + unfolding sign_def sgn_if by auto + +lemma sign_sgn[simp]: "sign (sgn x) = sign (x::'b::linordered_idom)" + by (simp add: sign_def) + +lemma sign_uminus[simp]:"sign (- x) = - sign (x::'b::linordered_idom)" + by (simp add: sign_def) + + +subsection\Bound of polynomials\ definition sgn_pos_inf :: "('a ::linordered_idom) poly \ 'a" where "sgn_pos_inf p \ sgn (lead_coeff p)" definition sgn_neg_inf :: "('a ::linordered_idom) poly \ 'a" where "sgn_neg_inf p \ if even (degree p) then sgn (lead_coeff p) else -sgn (lead_coeff p)" lemma sgn_inf_sym: fixes p::"real poly" shows "sgn_pos_inf (pcompose p [:0,-1:]) = sgn_neg_inf p" (is "?L=?R") proof - have "?L= sgn (lead_coeff p * (- 1) ^ degree p)" unfolding sgn_pos_inf_def by (subst lead_coeff_comp,auto) thus ?thesis unfolding sgn_neg_inf_def by (metis mult.right_neutral mult_minus1_right neg_one_even_power neg_one_odd_power sgn_minus) qed lemma poly_pinfty_gt_lc: fixes p:: "real poly" assumes "lead_coeff p > 0" shows "\ n. \ x \ n. poly p x \ lead_coeff p" using assms proof (induct p) case 0 thus ?case by auto next case (pCons a p) have "\a\0;p=0\ \ ?case" by auto moreover have "p\0 \ ?case" proof - assume "p\0" then obtain n1 where gte_lcoeff:"\x\n1. lead_coeff p \ poly p x" using that pCons by auto have gt_0:"lead_coeff p >0" using pCons(3) \p\0\ by auto define n where "n\max n1 (1+ \a\/(lead_coeff p))" show ?thesis proof (rule_tac x=n in exI,rule,rule) fix x assume "n \ x" hence "lead_coeff p \ poly p x" using gte_lcoeff unfolding n_def by auto hence " \a\/(lead_coeff p) \ \a\/(poly p x)" and "poly p x>0" using gt_0 by (intro frac_le,auto) hence "x\1+ \a\/(poly p x)" using \n\x\[unfolded n_def] by auto thus "lead_coeff (pCons a p) \ poly (pCons a p) x" using \lead_coeff p \ poly p x\ \poly p x>0\ \p\0\ by (auto simp add:field_simps) qed qed ultimately show ?case by fastforce qed lemma poly_sgn_eventually_at_top: fixes p::"real poly" shows "eventually (\x. sgn (poly p x) = sgn_pos_inf p) at_top" proof (cases "p=0") case True thus ?thesis unfolding sgn_pos_inf_def by auto next case False obtain ub where ub:"\x\ub. sgn (poly p x) = sgn_pos_inf p" proof (cases "lead_coeff p>0") case True thus ?thesis using that poly_pinfty_gt_lc[of p] unfolding sgn_pos_inf_def by fastforce next case False hence "lead_coeff (-p) > 0" and "lead_coeff p < 0" unfolding lead_coeff_minus using leading_coeff_neq_0[OF \p\0\] by (auto simp add:not_less_iff_gr_or_eq) then obtain n where "\x\n. lead_coeff p \ poly p x" using poly_pinfty_gt_lc[of "-p"] unfolding lead_coeff_minus by auto thus ?thesis using \lead_coeff p<0\ that[of n] unfolding sgn_pos_inf_def by fastforce qed thus ?thesis unfolding eventually_at_top_linorder by auto qed lemma poly_sgn_eventually_at_bot: fixes p::"real poly" shows "eventually (\x. sgn (poly p x) = sgn_neg_inf p) at_bot" using poly_sgn_eventually_at_top[of "pcompose p [:0,-1:]",unfolded poly_pcompose sgn_inf_sym,simplified] eventually_filtermap[of _ uminus "at_bot::real filter",folded at_top_mirror] by auto lemma root_ub: fixes p:: "real poly" assumes "p\0" obtains ub where "\x. poly p x=0 \ xx\ub. sgn (poly p x) = sgn_pos_inf p" proof - obtain ub1 where ub1:"\x. poly p x=0 \ x r. poly p r=0") case False thus ?thesis using that by auto next case True define max_r where "max_r\Max {x . poly p x=0}" hence "\x. poly p x=0 \ x\max_r" using poly_roots_finite[OF \p\0\] True by auto thus ?thesis using that[of "max_r+1"] by (metis add.commute add_strict_increasing zero_less_one) qed obtain ub2 where ub2:"\x\ub2. sgn (poly p x) = sgn_pos_inf p" using poly_sgn_eventually_at_top[unfolded eventually_at_top_linorder] by auto define ub where "ub\max ub1 ub2" have "\x. poly p x=0 \ x0" obtains lb where "\x. poly p x=0 \ x>lb" and "\x\lb. sgn (poly p x) = sgn_neg_inf p" proof - obtain lb1 where lb1:"\x. poly p x=0 \ x>lb1" proof (cases "\ r. poly p r=0") case False thus ?thesis using that by auto next case True define min_r where "min_r\Min {x . poly p x=0}" hence "\x. poly p x=0 \ x\min_r" using poly_roots_finite[OF \p\0\] True by auto thus ?thesis using that[of "min_r - 1"] by (metis lt_ex order.strict_trans2 that) qed obtain lb2 where lb2:"\x\lb2. sgn (poly p x) = sgn_neg_inf p" using poly_sgn_eventually_at_bot[unfolded eventually_at_bot_linorder] by auto define lb where "lb\min lb1 lb2" have "\x. poly p x=0 \ x>lb" using lb1 lb_def by (metis (poly_guards_query) less_not_sym min_less_iff_conj neq_iff) thus ?thesis using that[of lb] lb2 lb_def by auto qed -section\Sign\ - -definition sign:: "'a::{zero,linorder} \ int" where - "sign x\(if x>0 then 1 else if x=0 then 0 else -1)" - -lemma sign_simps[simp]: - "x>0 \ sign x=1" - "x=0 \ sign x=0" - "x<0 \ sign x=-1" -unfolding sign_def by auto - -lemma sign_cases [case_names neg zero pos]: - "(sign x = -1 \ P) \ (sign x = 0 \ P) \ (sign x =1 \ P) \ P" -unfolding Sturm_Tarski.sign_def by argo - -lemma sign_times: - fixes x::"'a::linordered_ring_strict" - shows "sign (x*y) = sign x * sign y" - unfolding Sturm_Tarski.sign_def - by (auto simp add:zero_less_mult_iff) - -lemma sign_power: - fixes x::"'a::linordered_idom" - shows "sign (x^n) = (if n=0 then 1 else if even n then \sign x\ else sign x)" - by (simp add: Sturm_Tarski.sign_def zero_less_power_eq) - -lemma sgn_sign_eq: - fixes x::"'a::{linordered_idom}" - shows "sgn x = of_int (sign x)" - unfolding sgn_if by auto - -section \Variation and cross\ +subsection \Variation and cross\ definition variation :: "real \ real \ int" where "variation x y=(if x*y\0 then 0 else if x real \ real \ int" where "cross p a b=variation (poly p a) (poly p b)" lemma variation_0[simp]: "variation 0 y=0" "variation x 0=0" unfolding variation_def by auto lemma variation_comm: "variation x y= - variation y x" unfolding variation_def by (auto simp add: mult.commute) lemma cross_0[simp]: "cross 0 a b=0" unfolding cross_def by auto lemma variation_cases: "\x>0;y>0\\variation x y = 0" "\x>0;y<0\\variation x y = -1" "\x<0;y>0\\variation x y = 1" "\x<0;y<0\\variation x y = 0" proof - show "\x>0;y>0\\variation x y = 0" unfolding variation_def by auto show "\x>0;y<0\\variation x y = -1" unfolding variation_def using mult_pos_neg by fastforce show "\x<0;y>0\\variation x y = 1" unfolding variation_def using mult_neg_pos by fastforce show "\x<0;y<0\\variation x y = 0" unfolding variation_def using mult_neg_neg by fastforce qed lemma variation_congr: assumes "sgn x=sgn x'" "sgn y=sgn y'" shows "variation x y=variation x' y'" using assms proof - have " 0 \ x * y = (0\ x' * y')" using assms by (metis Real_Vector_Spaces.sgn_mult zero_le_sgn_iff) moreover hence "\ 0\x * y \ x < y = (x' < y')" using assms by (metis less_eq_real_def mult_nonneg_nonneg mult_nonpos_nonpos not_le order.strict_trans2 zero_le_sgn_iff) ultimately show ?thesis unfolding variation_def by auto qed lemma variation_mult_pos: assumes "c>0" shows "variation (c*x) y =variation x y" and "variation x (c*y) =variation x y" proof - have "sgn (c*x) = sgn x" using \c>0\ by (simp add: Real_Vector_Spaces.sgn_mult) thus "variation (c*x) y =variation x y" using variation_congr by blast next have "sgn (c*y) = sgn y" using \c>0\ by (simp add: Real_Vector_Spaces.sgn_mult) thus "variation x (c*y) =variation x y" using variation_congr by blast qed lemma variation_mult_neg_1: assumes "c<0" shows "variation (c*x) y =variation x y + (if y=0 then 0 else sign x)" apply (cases x rule:linorder_cases[of 0] ) apply (cases y rule:linorder_cases[of 0], auto simp add: variation_cases mult_neg_pos[OF \c<0\,of x] mult_neg_neg[OF \c<0\,of x])+ done lemma variation_mult_neg_2: assumes "c<0" shows "variation x (c*y) = variation x y + (if x=0 then 0 else - sign y)" unfolding variation_comm[of x "c*y", unfolded variation_mult_neg_1[OF \c<0\, of y x] ] by (auto,subst variation_comm,simp) lemma cross_no_root: assumes "ax. ax poly p x\0" shows "cross p a b=0" proof - have "\poly p a>0;poly p b<0\ \ False" using poly_IVT_neg[OF \a] no_root by auto moreover have "\poly p a<0;poly p b>0\ \ False" using poly_IVT_pos[OF \a] no_root by auto ultimately have "0 \ poly p a * poly p b" by (metis less_eq_real_def linorder_neqE_linordered_idom mult_less_0_iff) thus ?thesis unfolding cross_def variation_def by simp qed -section \Tarski query\ +subsection \Tarski query\ definition taq :: "'a::linordered_idom set \ 'a poly \ int" where "taq s q \ \x\s. sign (poly q x)" -section \Sign at the right\ +subsection \Sign at the right\ definition sign_r_pos :: "real poly \ real \ bool " where "sign_r_pos p x\ (eventually (\x. poly p x>0) (at_right x))" lemma sign_r_pos_rec: fixes p:: "real poly" assumes "p\0" shows "sign_r_pos p x= (if poly p x=0 then sign_r_pos (pderiv p) x else poly p x>0 )" proof (cases "poly p x=0") case True have "sign_r_pos (pderiv p) x \ sign_r_pos p x" proof (rule ccontr) assume "sign_r_pos (pderiv p) x" "\ sign_r_pos p x" obtain b where "b>x" and b:"\z. x < z \ z < b \ 0 < poly (pderiv p) z" using \sign_r_pos (pderiv p) x\ unfolding sign_r_pos_def eventually_at_right by auto have "\b>x. \z>x. z < b \ \ 0 < poly p z" using \\ sign_r_pos p x\ unfolding sign_r_pos_def eventually_at_right by auto then obtain z where "z>x" and "z0" using \b>x\ b by auto hence "\z'>x. z' < z \ poly p z = (z - x) * poly (pderiv p) z'" using poly_MVT[OF \z>x\] True by (metis diff_0_right) hence "\z'>x. z' < z \ poly (pderiv p) z' \0" using \poly p z\0\\z>x\ by (metis leD le_iff_diff_le_0 mult_le_0_iff) thus False using b by (metis \z < b\ dual_order.strict_trans not_le) qed moreover have "sign_r_pos p x \ sign_r_pos (pderiv p) x" proof - assume "sign_r_pos p x" have "pderiv p\0" using \poly p x=0\ \p\0\ by (metis monoid_add_class.add.right_neutral monom_0 monom_eq_0 mult_zero_right pderiv_iszero poly_0 poly_pCons) obtain ub where "ub>x" and ub: "(\z. xzpoly (pderiv p) z>0) \ (\z. xzpoly (pderiv p) z<0)" using next_non_root_interval[OF \pderiv p\0\, of x,unfolded not_eq_pos_or_neg_iff_1] by (metis order.strict_implies_order) have "\z. xzpoly (pderiv p) z<0 \ False" proof - assume assm:"\z. xzpoly (pderiv p) z<0" obtain ub' where "ub'>x" and ub':"\z. x < z \ z < ub' \ 0 < poly p z" using \sign_r_pos p x\ unfolding sign_r_pos_def eventually_at_right by auto obtain z' where "xub'>x\ \ub>x\ True by auto moreover have "0 < poly p ((x+min ub' ub)/2)" using ub'[THEN HOL.spec,of "(x+(min ub' ub))/2"] \z' < (x+min ub' ub)/2\ \x by auto moreover have "(x+min ub' ub)/2 - x>0" using \ub'>x\ \ub>x\ by auto ultimately have "poly (pderiv p) z'>0" by (metis zero_less_mult_pos) thus False using assm[THEN spec,of z'] \x \z' < (x+(min ub' ub))/2\ by auto qed hence "\z. xzpoly (pderiv p) z>0" using ub by auto thus "sign_r_pos (pderiv p) x" unfolding sign_r_pos_def eventually_at_right using \ub>x\ by auto qed ultimately show ?thesis using True by auto next case False have "sign_r_pos p x \ poly p x>0" proof (rule ccontr) assume "sign_r_pos p x" "\ 0 < poly p x" then obtain ub where "ub>x" and ub: "\z. x < z \ z < ub \ 0 < poly p z" unfolding sign_r_pos_def eventually_at_right by auto hence "poly p ((ub+x)/2) > 0" by auto moreover have "poly p x<0" using \\ 0 < poly p x\ False by auto ultimately have "\z>x. z < (ub + x) / 2 \ poly p z = 0" using poly_IVT_pos[of x "((ub + x) / 2)" p] \ub>x\ by auto thus False using ub by auto qed moreover have "poly p x>0 \ sign_r_pos p x" unfolding sign_r_pos_def using order_tendstoD(1)[OF poly_tendsto(1),of 0 p x] eventually_at_split by auto ultimately show ?thesis using False by auto qed lemma sign_r_pos_0[simp]:"\ sign_r_pos 0 (x::real)" using eventually_False[of "at_right x"] unfolding sign_r_pos_def by auto lemma sign_r_pos_minus: fixes p:: "real poly" assumes "p\0" shows "sign_r_pos p x = (\ sign_r_pos (-p) x)" proof - have "sign_r_pos p x \ sign_r_pos (-p) x" unfolding sign_r_pos_def eventually_at_right using next_non_root_interval[OF \p\0\,unfolded not_eq_pos_or_neg_iff_1] by (metis (erased, opaque_lifting) le_less minus_zero neg_less_iff_less poly_minus) moreover have "sign_r_pos p x \ \ sign_r_pos (-p) x" unfolding sign_r_pos_def using eventually_neg[OF trivial_limit_at_right_real, of "\x. poly p x > 0" x] poly_minus by (metis (lifting) eventually_mono less_asym neg_less_0_iff_less) ultimately show ?thesis by auto qed lemma sign_r_pos_smult: fixes p :: "real poly" assumes "c\0" "p\0" shows "sign_r_pos (smult c p) x= (if c>0 then sign_r_pos p x else \ sign_r_pos p x)" (is "?L=?R") proof (cases "c>0") assume "c>0" hence "\x. (0 < poly (smult c p) x) = (0 < poly p x)" by (subst poly_smult,metis mult_pos_pos zero_less_mult_pos) thus ?thesis unfolding sign_r_pos_def using \c>0\ by auto next assume "\(c>0)" hence "\x. (0 < poly (smult c p) x) = (0 < poly (-p) x)" by (subst poly_smult, metis assms(1) linorder_neqE_linordered_idom mult_neg_neg mult_zero_right neg_0_less_iff_less poly_minus zero_less_mult_pos2) hence "sign_r_pos (smult c p) x=sign_r_pos (-p) x" unfolding sign_r_pos_def using \\ c>0\ by auto thus ?thesis using sign_r_pos_minus[OF \p\0\, of x] \\ c>0\ by auto qed lemma sign_r_pos_mult: fixes p q :: "real poly" assumes "p\0" "q\0" shows "sign_r_pos (p*q) x= (sign_r_pos p x \ sign_r_pos q x)" proof - obtain ub where "ub>x" and ub:"(\z. x < z \ z < ub \ 0 < poly p z) \ (\z. x < z \ z < ub \ poly p z < 0)" using next_non_root_interval[OF \p\0\,of x,unfolded not_eq_pos_or_neg_iff_1] by (metis order.strict_implies_order) obtain ub' where "ub'>x" and ub':"(\z. x < z \ z < ub' \ 0 < poly q z) \ (\z. x < z \ z < ub' \ poly q z < 0)" using next_non_root_interval[OF \q\0\,unfolded not_eq_pos_or_neg_iff_1] by (metis order.strict_implies_order) have "(\z. x < z \ z < ub \ 0 < poly p z) \ (\z. x < z \ z < ub' \ 0 < poly q z) \ ?thesis" proof - assume "(\z. x < z \ z < ub \ 0 < poly p z)" "(\z. x < z \ z < ub' \ 0 < poly q z)" hence "sign_r_pos p x" and "sign_r_pos q x" unfolding sign_r_pos_def eventually_at_right using \ub>x\ \ub'>x\ by auto moreover hence "eventually (\z. poly p z>0 \ poly q z>0) (at_right x)" unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto hence "sign_r_pos (p*q) x" unfolding sign_r_pos_def poly_mult by (metis (lifting, mono_tags) eventually_mono mult_pos_pos) ultimately show ?thesis by auto qed moreover have "(\z. x < z \ z < ub \ 0 > poly p z) \ (\z. x < z \ z < ub' \ 0 < poly q z) \ ?thesis" proof - assume "(\z. x < z \ z < ub \ 0 > poly p z)" "(\z. x < z \ z < ub' \ 0 < poly q z)" hence "sign_r_pos (-p) x" and "sign_r_pos q x" unfolding sign_r_pos_def eventually_at_right using \ub>x\ \ub'>x\ by auto moreover hence "eventually (\z. poly (-p) z>0 \ poly q z>0) (at_right x)" unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto hence "sign_r_pos (- p*q) x" unfolding sign_r_pos_def poly_mult by (metis (lifting, mono_tags) eventually_mono mult_pos_pos) ultimately show ?thesis using sign_r_pos_minus \p\0\ \q\0\ by (metis minus_mult_left no_zero_divisors) qed moreover have "(\z. x < z \ z < ub \ 0 < poly p z) \ (\z. x < z \ z < ub' \ 0 > poly q z) \ ?thesis" proof - assume "(\z. x < z \ z < ub \ 0 < poly p z)" "(\z. x < z \ z < ub' \ 0 > poly q z)" hence "sign_r_pos p x" and "sign_r_pos (-q) x" unfolding sign_r_pos_def eventually_at_right using \ub>x\ \ub'>x\ by auto moreover hence "eventually (\z. poly p z>0 \ poly (-q) z>0) (at_right x)" unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto hence "sign_r_pos ( p * (- q)) x" unfolding sign_r_pos_def poly_mult by (metis (lifting, mono_tags) eventually_mono mult_pos_pos) ultimately show ?thesis using sign_r_pos_minus \p\0\ \q\0\ by (metis minus_mult_right no_zero_divisors) qed moreover have "(\z. x < z \ z < ub \ 0 > poly p z) \ (\z. x < z \ z < ub' \ 0 > poly q z) \ ?thesis" proof - assume "(\z. x < z \ z < ub \ 0 > poly p z)" "(\z. x < z \ z < ub' \ 0 > poly q z)" hence "sign_r_pos (-p) x" and "sign_r_pos (-q) x" unfolding sign_r_pos_def eventually_at_right using \ub>x\ \ub'>x\ by auto moreover hence "eventually (\z. poly (-p) z>0 \ poly (-q) z>0) (at_right x)" unfolding sign_r_pos_def using eventually_conj_iff[of _ _ "at_right x"] by auto hence "sign_r_pos (p * q) x" unfolding sign_r_pos_def poly_mult poly_minus apply (elim eventually_mono[of _ "at_right x"]) by (auto intro:mult_neg_neg) ultimately show ?thesis using sign_r_pos_minus \p\0\ \q\0\ by metis qed ultimately show ?thesis using ub ub' by auto qed lemma sign_r_pos_add: fixes p q :: "real poly" assumes "poly p x=0" "poly q x\0" shows "sign_r_pos (p+q) x=sign_r_pos q x" proof (cases "poly (p+q) x=0") case False hence "p+q\0" by (metis poly_0) have "sign_r_pos (p+q) x = (poly q x > 0)" using sign_r_pos_rec[OF \p+q\0\] False poly_add \poly p x=0\ by auto moreover have "sign_r_pos q x=(poly q x > 0)" using sign_r_pos_rec[of q x] \poly q x\0\ poly_0 by force ultimately show ?thesis by auto next case True hence False using \poly p x=0\ \poly q x\0\ poly_add by auto thus ?thesis by auto qed lemma sign_r_pos_mod: fixes p q :: "real poly" assumes "poly p x=0" "poly q x\0" shows "sign_r_pos (q mod p) x=sign_r_pos q x" proof - have "poly (q div p * p) x=0" using \poly p x=0\ poly_mult by auto moreover hence "poly (q mod p) x \ 0" using \poly q x\0\ by (simp add: assms(1) poly_mod) ultimately show ?thesis by (metis div_mult_mod_eq sign_r_pos_add) qed lemma sign_r_pos_pderiv: fixes p:: "real poly" assumes "poly p x=0" "p\0" shows "sign_r_pos (pderiv p * p) x" proof - have "pderiv p \0" by (metis assms(1) assms(2) monoid_add_class.add.right_neutral mult_zero_right pCons_0_0 pderiv_iszero poly_0 poly_pCons) have "?thesis = (sign_r_pos (pderiv p) x \ sign_r_pos p x)" using sign_r_pos_mult[OF \pderiv p \ 0\ \p\0\] by auto also have "...=((sign_r_pos (pderiv p) x \ sign_r_pos (pderiv p) x))" using sign_r_pos_rec[OF \p\0\] \poly p x=0\ by auto finally show ?thesis by auto qed lemma sign_r_pos_power: fixes p:: "real poly" and a::real shows "sign_r_pos ([:-a,1:]^n) a" proof (induct n) case 0 thus ?case unfolding sign_r_pos_def eventually_at_right by (simp,metis gt_ex) next case (Suc n) have "pderiv ([:-a,1:]^Suc n) = smult (Suc n) ([:-a,1:]^n)" proof - have "pderiv [:- a, 1::real:] = 1" by (simp add: pderiv.simps) thus ?thesis unfolding pderiv_power_Suc by (metis mult_cancel_left1) qed moreover have " poly ([:- a, 1:] ^ Suc n) a=0" by (metis old.nat.distinct(2) poly_power_n_eq) hence "sign_r_pos ([:- a, 1:] ^ Suc n) a = sign_r_pos (smult (Suc n) ([:-a,1:]^n)) a" using sign_r_pos_rec by (metis (erased, opaque_lifting) calculation pderiv_0) hence "sign_r_pos ([:- a, 1:] ^ Suc n) a = sign_r_pos ([:-a,1:]^n) a" using sign_r_pos_smult by auto ultimately show ?case using Suc.hyps by auto qed -section\Jump\ + +subsection\Jump\ definition jump_poly :: "real poly \ real poly \real \ int" where " jump_poly q p x\ (if p\0 \ q\0 \ odd((order x p) - (order x q) ) then if sign_r_pos (q*p) x then 1 else -1 else 0 )" lemma jump_poly_not_root:"poly p x\0\ jump_poly q p x=0" unfolding jump_poly_def by (metis even_zero order_root zero_diff) lemma jump_poly0[simp]: "jump_poly 0 p x = 0" "jump_poly q 0 x = 0" unfolding jump_poly_def by auto lemma jump_poly_smult_1: fixes p q::"real poly" and c::real shows "jump_poly (smult c q) p x= sign c * jump_poly q p x" (is "?L=?R") proof (cases "c=0\ q=0") case True thus ?thesis unfolding jump_poly_def by auto next case False hence "c\0" and "q\0" by auto thus ?thesis unfolding jump_poly_def using order_smult[OF \c\0\] sign_r_pos_smult[OF \c\0\, of "q*p" x] \q\0\ by auto qed lemma jump_poly_mult: fixes p q p'::"real poly" assumes "p'\0" shows "jump_poly (p'*q) (p'*p) x= jump_poly q p x" proof (cases "q=0 \ p=0") case True thus ?thesis unfolding jump_poly_def by fastforce next case False then have "q\0" "p\0" by auto have "sign_r_pos (p' * q * (p' * p)) x=sign_r_pos (q * p) x" proof (unfold sign_r_pos_def,rule eventually_subst,unfold eventually_at_right) obtain b where "b>x" and b:"\z. x < z \ z < b \ poly (p' * p') z >0" proof (cases "\z. poly p' z=0 \ z>x") case True define lr where "lr\Min {r . poly p' r=0 \ r>x}" have "\z. xzpoly p' z\0" and "lr>x" using True lr_def poly_roots_finite[OF \p'\0\] by auto hence "\z. x < z \ z < lr \ 0 < poly (p' * p') z" by (metis not_real_square_gt_zero poly_mult) thus ?thesis using that[OF \lr>x\] by auto next case False have "\z. xzpoly p' z\0" and "x+1>x" using False poly_roots_finite[OF \p'\0\] by auto hence "\z. x < z \ z < x+1 \ 0 < poly (p' * p') z" by (metis not_real_square_gt_zero poly_mult) thus ?thesis using that[OF \x+1>x\] by auto qed show "\b>x. \z>x. z < b \ (0 < poly (p' * q * (p' * p)) z) = (0 < poly (q * p) z)" proof (rule_tac x="b" in exI, rule conjI[OF \b>x\],rule allI,rule impI,rule impI) fix z assume "x < z" "z < b" hence "00 by (metis mult_pos_pos zero_less_mult_pos) finally show "(0 < poly (p' * q * (p' * p)) z) = (0 < poly (q * p) z)" . qed qed moreover have " odd (order x (p' * p) - order x (p' * q)) = odd (order x p - order x q)" using False \p'\0\ \p\0\ mult_eq_0_iff order_mult by (metis add_diff_cancel_left) moreover have " p' * q \ 0 \ q \ 0" by (metis \p'\0\ mult_eq_0_iff) ultimately show "jump_poly (p' * q) (p' * p) x = jump_poly q p x" unfolding jump_poly_def by auto qed lemma jump_poly_1_mult: fixes p1 p2::"real poly" assumes "poly p1 x\0 \ poly p2 x\0" shows "jump_poly 1 (p1*p2) x= sign (poly p2 x) * jump_poly 1 p1 x + sign (poly p1 x) * jump_poly 1 p2 x" (is "?L=?R") proof (cases "p1=0 \ p2 =0") case True then show ?thesis by auto next case False then have "p1\0" "p2\0" "p1*p2\0" by auto have ?thesis when "poly p1 x\0" proof - have [simp]:"order x p1 = 0" using that order_root by blast define simpL where "simpL\(if p2\0 \ odd (order x p2) then if (poly p1 x>0) \ sign_r_pos p2 x then 1::int else -1 else 0)" have "?L=simpL" unfolding simpL_def jump_poly_def using order_mult[OF \p1*p2\0\] sign_r_pos_mult[OF \p1\0\ \p2\0\] sign_r_pos_rec[OF \p1\0\] \poly p1 x\0\ by auto moreover have "poly p1 x>0 \ simpL =?R" unfolding simpL_def jump_poly_def using jump_poly_not_root[OF \poly p1 x\0\] by auto moreover have "poly p1 x<0 \ simpL =?R" unfolding simpL_def jump_poly_def using jump_poly_not_root[OF \poly p1 x\0\] by auto ultimately show "?L=?R" using \poly p1 x\0\ by (metis linorder_neqE_linordered_idom) qed moreover have ?thesis when "poly p2 x\0" proof - have [simp]:"order x p2 = 0" using that order_root by blast define simpL where "simpL\(if p1\0 \ odd (order x p1) then if (poly p2 x>0) \ sign_r_pos p1 x then 1::int else -1 else 0)" have "?L=simpL" unfolding simpL_def jump_poly_def using order_mult[OF \p1*p2\0\] sign_r_pos_mult[OF \p1\0\ \p2\0\] sign_r_pos_rec[OF \p2\0\] \poly p2 x\0\ by auto moreover have "poly p2 x>0 \ simpL =?R" unfolding simpL_def jump_poly_def using jump_poly_not_root[OF \poly p2 x\0\] by auto moreover have "poly p2 x<0 \ simpL =?R" unfolding simpL_def jump_poly_def using jump_poly_not_root[OF \poly p2 x\0\] by auto ultimately show "?L=?R" using \poly p2 x\0\ by (metis linorder_neqE_linordered_idom) qed ultimately show ?thesis using assms by auto qed lemma jump_poly_mod: fixes p q::"real poly" shows "jump_poly q p x= jump_poly (q mod p) p x" proof (cases "q=0 \ p=0") case True thus ?thesis by fastforce next case False then have "p\0" "q\0" by auto define n where "n\min (order x q) (order x p)" obtain q' where q':"q=[:-x,1:]^n * q'" using n_def power_le_dvd[OF order_1[of x q], of n] by (metis dvdE min.cobounded2 min.commute) obtain p' where p':"p=[:-x,1:]^n * p'" using n_def power_le_dvd[OF order_1[of x p], of n] by (metis dvdE min.cobounded2) have "q'\0" and "p'\0" using q' p' \p\0\ \q\0\ by auto have "order x q'=0 \ order x p'=0" proof (rule ccontr) assume "\ (order x q' = 0 \ order x p' = 0)" hence "order x q' > 0" and "order x p' > 0" by auto hence "order x q>n" and "order x p>n" unfolding q' p' using order_mult[OF \q\0\[unfolded q'],of x] order_mult[OF \p\0\[unfolded p'],of x] order_power_n_n[of x n] by auto thus False using n_def by auto qed have cond:"q' \ 0 \ odd (order x p' - order x q') = (q' mod p' \0 \ odd(order x p' - order x (q' mod p')))" proof (cases "order x p'=0") case True thus ?thesis by (metis \q' \ 0\ even_zero zero_diff) next case False hence "order x q'=0" using \order x q'=0 \ order x p'=0\ by auto hence "\ [:-x,1:] dvd q'" by (metis \q' \ 0\ order_root poly_eq_0_iff_dvd) moreover have "[:-x,1:] dvd p'" using False by (metis order_root poly_eq_0_iff_dvd) ultimately have "\ [:-x,1:] dvd (q' mod p')" by (metis dvd_mod_iff) hence "order x (q' mod p') = 0" and "q' mod p' \0" apply (metis order_root poly_eq_0_iff_dvd) by (metis \\ [:- x, 1:] dvd q' mod p'\ dvd_0_right) thus ?thesis using \order x q'=0\ by auto qed moreover have "q' mod p'\0 \ poly p' x = 0 \ sign_r_pos (q' * p') x= sign_r_pos (q' mod p' * p') x" proof - assume "q' mod p'\0" "poly p' x = 0" hence "poly q' x\0" using \order x q'=0 \ order x p'=0\ by (metis \p' \ 0\ \q' \ 0\ order_root) hence "sign_r_pos q' x= sign_r_pos (q' mod p') x" using sign_r_pos_mod[OF \poly p' x=0\] by auto thus ?thesis unfolding sign_r_pos_mult[OF \q'\0\ \p'\0\] sign_r_pos_mult[OF \q' mod p'\0\ \p'\0\] by auto qed moreover have "q' mod p' = 0 \ poly p' x \ 0 \ jump_poly q' p' x = jump_poly (q' mod p') p' x" proof - assume assm:"q' mod p' = 0 \ poly p' x \ 0" have "q' mod p' = 0 \ ?thesis" unfolding jump_poly_def using cond by auto moreover have "poly p' x \ 0 \ \ odd (order x p' - order x q') \ \ odd(order x p' - order x (q' mod p'))" by (metis even_zero order_root zero_diff) hence "poly p' x \ 0 \ ?thesis" unfolding jump_poly_def by auto ultimately show ?thesis using assm by auto qed ultimately have " jump_poly q' p' x = jump_poly (q' mod p') p' x" unfolding jump_poly_def by force thus ?thesis using p' q' jump_poly_mult by auto qed lemma jump_poly_coprime: fixes p q:: "real poly" assumes "poly p x=0" "coprime p q" shows "jump_poly q p x= jump_poly 1 (q*p) x" proof (cases "p=0 \ q=0") case True then show ?thesis by auto next case False then have "p\0" "q\0" by auto then have "poly p x\0 \ poly q x\0" using coprime_poly_0[OF \coprime p q\] by auto then have "poly q x\0" using \poly p x=0\ by auto then have "order x q=0" using order_root by blast then have "order x p - order x q = order x (q * p)" using \p\0\ \q\0\ order_mult [of q p x] by auto then show ?thesis unfolding jump_poly_def using \q\0\ by auto qed lemma jump_poly_sgn: fixes p q:: "real poly" assumes "p\0" "poly p x=0" shows "jump_poly (pderiv p * q) p x = sign (poly q x)" proof (cases "q=0") case True thus ?thesis by auto next case False have "pderiv p\0" using \p\0\ \poly p x=0\ by (metis mult_poly_0_left sign_r_pos_0 sign_r_pos_pderiv) have elim_p_order: "order x p - order x (pderiv p * q)=1 - order x q" proof - have "order x p - order x (pderiv p * q) = order x p - order x (pderiv p) - order x q" using order_mult \pderiv p\0\ False by (metis diff_diff_left mult_eq_0_iff) moreover have "order x p - order x (pderiv p) = 1" using order_pderiv[OF \pderiv p\0\, of x] \poly p x=0\ order_root[of p x] \p\0\ by auto ultimately show ?thesis by auto qed have elim_p_sign_r_pos:"sign_r_pos (pderiv p * q * p) x=sign_r_pos q x" proof - have "sign_r_pos (pderiv p * q * p) x = (sign_r_pos (pderiv p* p) x \ sign_r_pos q x)" by (metis \q \ 0\ \pderiv p \ 0\ assms(1) no_zero_divisors sign_r_pos_mult) thus ?thesis using sign_r_pos_pderiv[OF \poly p x=0\ \p\0\] by auto qed define simpleL where "simpleL\if pderiv p * q \ 0 \ odd (1 - order x q) then if sign_r_pos q x then 1::int else - 1 else 0" have " jump_poly (pderiv p * q) p x =simpleL" unfolding simpleL_def jump_poly_def by (subst elim_p_order, subst elim_p_sign_r_pos,simp) moreover have "poly q x=0 \ simpleL=sign (poly q x)" proof - assume "poly q x=0" hence "1-order x q = 0" using \q\0\ by (metis less_one not_gr0 order_root zero_less_diff) hence "simpleL=0" unfolding simpleL_def by auto moreover have "sign (poly q x)=0" using \poly q x=0\ by auto ultimately show ?thesis by auto qed moreover have "poly q x\0\ simpleL=sign (poly q x)" proof - assume "poly q x\0" hence "odd (1 - order x q)" by (simp add: order_root) moreover have "pderiv p * q \ 0" by (metis False \pderiv p \ 0\ no_zero_divisors) moreover have "sign_r_pos q x = (poly q x > 0)" using sign_r_pos_rec[OF False] \poly q x\0\ by auto ultimately have "simpleL=(if poly q x>0 then 1 else - 1)" unfolding simpleL_def by auto thus ?thesis using \poly q x\0\ by auto qed ultimately show ?thesis by force qed -section \Cauchy index\ +subsection \Cauchy index\ definition cindex_poly:: "real \ real \ real poly \ real poly \ int" where "cindex_poly a b q p\ (\x\{x. poly p x=0 \ a< x\ x< b}. jump_poly q p x)" lemma cindex_poly_0[simp]: "cindex_poly a b 0 p = 0" "cindex_poly a b q 0 = 0" unfolding cindex_poly_def by auto lemma cindex_poly_cross: fixes p::"real poly" and a b::real assumes "a0" "poly p b\0" shows "cindex_poly a b 1 p = cross p a b" using \poly p a\0\ \poly p b\0\ proof (cases "{x. poly p x=0 \ a< x\ x< b}\{}", induct "degree p" arbitrary:p rule:nat_less_induct) case 1 then have "p\0" by force define roots where "roots\{x. poly p x=0 \ a< x\ x< b}" have "finite roots" unfolding roots_def using poly_roots_finite[OF \p\0\] by auto define max_r where "max_r\Max roots" hence "poly p max_r=0" and "afinite roots\] "1.prems" unfolding roots_def by auto define max_rp where "max_rp\[:-max_r,1:]^order max_r p" then obtain p' where p':"p=p'*max_rp" and not_dvd:"\ [:-max_r,1:] dvd p'" by (metis \p\0\ mult.commute order_decomp) hence "p'\0" and "max_rp\0" and "poly p' a\0" and "poly p' b\0" and "poly max_rp a\0" and "poly max_rp b\0" using \p\0\ \poly p a\0\ \poly p b\0\ by auto define max_r_sign where "max_r_sign\if odd(order max_r p) then -1 else 1::int" define roots' where "roots'\{x. a< x\ x< b \ poly p' x=0}" have "(\x\roots. jump_poly 1 p x)= (\x\roots'. jump_poly 1 p x)+ jump_poly 1 p max_r" proof - have "roots=roots' \ {x. a< x\ x< b \ poly max_rp x=0 }" unfolding roots_def roots'_def p' by auto moreover have "{x. a < x \ x < b \ poly max_rp x = 0 }={max_r}" unfolding max_rp_def using \poly p max_r=0\ by (auto simp add: \a \max_r,metis "1.prems"(1) neq0_conv order_root) moreover hence "roots' \ {x. a< x\ x< b \ poly max_rp x=0} ={}" unfolding roots'_def using \\ [:-max_r,1:] dvd p'\ by (metis (mono_tags) Int_insert_right_if0 inf_bot_right mem_Collect_eq poly_eq_0_iff_dvd) moreover have "finite roots'" using p' \p\0\ by (metis \finite roots\ calculation(1) calculation(2) finite_Un) ultimately show ?thesis using sum.union_disjoint by auto qed moreover have "(\x\roots'. jump_poly 1 p x) = max_r_sign * cross p' a b" proof - have "(\x\roots'. jump_poly 1 p x) = (\x\roots'. max_r_sign * jump_poly 1 p' x)" proof (rule sum.cong,rule refl) fix x assume "x \ roots'" hence "x\max_r" using not_dvd unfolding roots'_def by (metis (mono_tags, lifting) mem_Collect_eq poly_eq_0_iff_dvd ) hence "poly max_rp x\0" using poly_power_n_eq unfolding max_rp_def by auto hence "order x max_rp=0" by (metis order_root) moreover have "jump_poly 1 max_rp x=0" using \poly max_rp x\0\ by (metis jump_poly_not_root) moreover have "x\roots" using \x \ roots'\ unfolding roots_def roots'_def p' by auto hence "xfinite roots\,of x] \x\max_r\ by (fold max_r_def,auto) hence "sign (poly max_rp x) = max_r_sign" using \poly max_rp x \ 0\ unfolding max_r_sign_def max_rp_def sign_def by (subst poly_power,simp add:linorder_class.not_less zero_less_power_eq) ultimately show "jump_poly 1 p x = max_r_sign * jump_poly 1 p' x" using jump_poly_1_mult[of p' x max_rp] unfolding p' by (simp add: \poly max_rp x \ 0\) qed also have "... = max_r_sign * (\x\roots'. jump_poly 1 p' x)" by (simp add: sum_distrib_left) also have "... = max_r_sign * cross p' a b" proof (cases "roots'={}") case True hence "cross p' a b=0" unfolding roots'_def using cross_no_root[OF \a] by auto thus ?thesis using True by simp next case False moreover have "degree max_rp\0" unfolding max_rp_def degree_linear_power by (metis "1.prems"(1) \poly p max_r = 0\ order_root) hence "degree p' < degree p" unfolding p' degree_mult_eq[OF \p'\0\ \max_rp\0\] by auto ultimately have "cindex_poly a b 1 p' = cross p' a b" unfolding roots'_def using "1.hyps"[rule_format,of "degree p'" p'] \p'\0\ \poly p' a\0\ \poly p' b\0\ by auto moreover have "cindex_poly a b 1 p' = sum (jump_poly 1 p') roots'" unfolding cindex_poly_def roots'_def apply simp by (metis (no_types, lifting) ) ultimately show ?thesis by auto qed finally show ?thesis . qed moreover have "max_r_sign * cross p' a b + jump_poly 1 p max_r = cross p a b" (is "?L=?R") proof (cases "odd (order max_r p)") case True have "poly max_rp a < 0" using poly_power_n_odd[OF True,of max_r a] \poly max_rp a\0\ \max_r>a\ unfolding max_rp_def by linarith moreover have "poly max_rp b>0 " using poly_power_n_odd[OF True,of max_r b] \max_r unfolding max_rp_def by linarith ultimately have "?R=cross p' a b + sign (poly p' a)" unfolding p' cross_def poly_mult using variation_mult_neg_1[of "poly max_rp a", simplified mult.commute] variation_mult_pos(2)[of "poly max_rp b", simplified mult.commute] \poly p' b\0\ by auto moreover have "?L=- cross p' a b + sign (poly p' b)" proof - have " sign_r_pos p' max_r = (poly p' max_r >0)" using sign_r_pos_rec[OF \p'\0\] not_dvd by (metis poly_eq_0_iff_dvd) moreover have "(poly p' max_r>0) = (poly p' b>0)" proof (rule ccontr) assume "(0 < poly p' max_r) \ (0 < poly p' b)" hence "poly p' max_r * poly p' b <0" using \poly p' b\0\ not_dvd[folded poly_eq_0_iff_dvd] by (metis (poly_guards_query) linorder_neqE_linordered_idom mult_less_0_iff) then obtain r where "r>max_r" and "rmax_r] by auto hence "r\roots" unfolding roots_def p' using \max_r>a\ by auto thus False using \r>max_r\ Max_ge[OF \finite roots\,of r] unfolding max_r_def by auto qed moreover have "sign_r_pos max_rp max_r" using sign_r_pos_power unfolding max_rp_def by auto ultimately show ?thesis using True \poly p' b\0\ \max_rp\0\ \p'\0\ sign_r_pos_mult[OF \p'\0\ \max_rp\0\] unfolding max_r_sign_def p' jump_poly_def by simp qed moreover have "variation (poly p' a) (poly p' b) + sign (poly p' a) = - variation (poly p' a) (poly p' b) + sign (poly p' b)" unfolding cross_def by (cases "poly p' b" rule:linorder_cases[of 0], (cases "poly p' a" rule:linorder_cases[of 0], auto simp add:variation_cases \poly p' a \ 0\ \poly p' b \ 0\)+) ultimately show ?thesis unfolding cross_def by auto next case False hence "poly max_rp a > 0" and "poly max_rp b > 0" unfolding max_rp_def poly_power using \poly max_rp a\0\ \poly max_rp b \ 0\ "1.prems"(1-2) \poly p max_r = 0\ apply (unfold zero_less_power_eq) by auto moreover have "poly max_rp b > 0" unfolding max_rp_def poly_power using \poly max_rp b \ 0\ False max_rp_def poly_power zero_le_even_power[of "order max_r p" "b - max_r"] by (auto simp add: le_less) ultimately have "?R=cross p' a b" apply (simp only: p' mult.commute cross_def) using variation_mult_pos by auto thus ?thesis unfolding max_r_sign_def jump_poly_def using False by auto qed ultimately have "sum (jump_poly 1 p) roots = cross p a b " by auto then show ?case unfolding roots_def cindex_poly_def by simp next case False hence "cross p a b=0" using cross_no_root[OF \a] by auto thus ?thesis using False unfolding cindex_poly_def by (metis sum.empty) qed lemma cindex_poly_mult: fixes p q p'::"real poly" assumes "p'\ 0" shows "cindex_poly a b (p' * q ) (p' * p) = cindex_poly a b q p" proof (cases "p=0") case True then show ?thesis by auto next case False show ?thesis unfolding cindex_poly_def apply (rule sum.mono_neutral_cong_right) subgoal using \p\0\ \p'\0\ by (simp add: poly_roots_finite) subgoal by auto subgoal using jump_poly_mult jump_poly_not_root assms by fastforce subgoal for x using jump_poly_mult[OF \p'\0\] by auto done qed lemma cindex_poly_smult_1: fixes p q::"real poly" and c::real shows "cindex_poly a b (smult c q) p = (sign c) * cindex_poly a b q p" unfolding cindex_poly_def using sum_distrib_left[THEN sym, of "sign c" "\x. jump_poly q p x" "{x. poly p x = (0::real) \ a < x \ x < b}"] jump_poly_smult_1 by auto lemma cindex_poly_mod: fixes p q::"real poly" shows "cindex_poly a b q p = cindex_poly a b (q mod p) p" unfolding cindex_poly_def using jump_poly_mod by auto lemma cindex_poly_inverse_add: fixes p q::"real poly" assumes "coprime p q" shows "cindex_poly a b q p + cindex_poly a b p q=cindex_poly a b 1 (q*p)" (is "?L=?R") proof (cases "p=0 \ q=0") case True then show ?thesis by auto next case False then have "p\0" "q\0" by auto define A where "A\{x. poly p x = 0 \ a < x \ x < b}" define B where "B\{x. poly q x = 0 \ a < x \ x < b}" have "?L = sum (\x. jump_poly 1 (q*p) x) A + sum (\x. jump_poly 1 (q*p) x) B" proof - have "cindex_poly a b q p = sum (\x. jump_poly 1 (q*p) x) A" unfolding A_def cindex_poly_def using jump_poly_coprime[OF _ \coprime p q\] by auto moreover have "coprime q p" using \coprime p q\ by (simp add: ac_simps) hence "cindex_poly a b p q = sum (\x. jump_poly 1 (q*p) x) B" unfolding B_def cindex_poly_def using jump_poly_coprime [of q _ p] by (auto simp add: ac_simps) ultimately show ?thesis by auto qed moreover have "A \ B= {x. poly (q*p) x=0 \ a x B={}" proof (rule ccontr) assume "A \ B\{}" then obtain x where "x\A" and "x\B" by auto hence "poly p x=0" and "poly q x=0" unfolding A_def B_def by auto hence "gcd p q\1" by (metis poly_1 poly_eq_0_iff_dvd gcd_greatest zero_neq_one) thus False using \coprime p q\ by auto qed moreover have "finite A" and "finite B" unfolding A_def B_def using poly_roots_finite \p\0\ \q\0\ by fast+ ultimately have "cindex_poly a b q p + cindex_poly a b p q = sum (jump_poly 1 (q * p)) {x. poly (q*p) x=0 \ a x0" "poly (p * q) b \0" shows "cindex_poly a b q p + cindex_poly a b p q = cross (p * q) a b" (is "?L=?R") proof - have "p\0" and "q\0" using \poly (p * q) a \0\ by auto define g where "g\gcd p q" obtain p' q' where p':"p= p'*g" and q':"q=q'*g" using gcd_dvd1 gcd_dvd2 dvd_def[of "gcd p q", simplified mult.commute] g_def by metis hence "coprime p' q'" using gcd_coprime \p\0\ unfolding g_def by auto have "p'\0" "q'\0" "g \0" using p' q' \p\0\ \q\0\ by auto have "?L=cindex_poly a b q' p' + cindex_poly a b p' q'" apply (simp only: p' q' mult.commute) using cindex_poly_mult[OF \g\0\] cindex_poly_mult[OF \g\0\] by auto also have "... = cindex_poly a b 1 (q' * p')" using cindex_poly_inverse_add[OF \coprime p' q'\, of a b] . also have "... = cross (p' * q') a b" using cindex_poly_cross[OF \a, of "q'*p'"] \p'\0\ \q'\0\ \poly (p * q) a \0\ \poly (p * q) b \0\ unfolding p' q' apply (subst (2) mult.commute) by auto also have "... = ?R" proof - have "poly (p * q) a = poly (g*g) a * poly (p' * q') a" and "poly (p * q) b = poly (g*g) b * poly (p' * q') b" unfolding p' q' by auto moreover have "poly g a\0" using \poly (p * q) a \0\ unfolding p' by auto hence "poly (g*g) a>0" by (metis (poly_guards_query) not_real_square_gt_zero poly_mult) moreover have "poly g b\0" using \poly (p * q) b \0\ unfolding p' by auto hence "poly (g*g) b>0" by (metis (poly_guards_query) not_real_square_gt_zero poly_mult) ultimately show ?thesis unfolding cross_def using variation_mult_pos by auto qed finally show "?L = ?R" . qed lemma cindex_poly_rec: fixes p q::"real poly" assumes "a < b" "poly (p * q) a \0" "poly (p * q) b \0" shows "cindex_poly a b q p = cross (p * q) a b + cindex_poly a b (- (p mod q)) q" (is "?L=?R") proof - have "q\0" using \poly (p * q) a \0\ by auto note cindex_poly_inverse_add_cross[OF assms] moreover have "- cindex_poly a b p q = cindex_poly a b (- (p mod q)) q" using cindex_poly_mod cindex_poly_smult_1[of a b "-1"] by auto ultimately show ?thesis by auto qed lemma cindex_poly_congr: fixes p q:: "real poly" assumes "ax. ((ax\a') \ (b'\x \ x poly p x \0" shows "cindex_poly a b q p=cindex_poly a' b' q p" proof (cases "p=0") case True then show ?thesis by auto next case False show ?thesis unfolding cindex_poly_def apply (rule sum.mono_neutral_right) subgoal using poly_roots_finite[OF \p\0\] by auto subgoal using assms by auto subgoal using assms(4) by fastforce done qed lemma greaterThanLessThan_unfold:"{a<.. x a < x \ x < b} q=cindex_poly a b (pderiv p * q) p" proof (cases "p=0") case True define S where "S={x. poly p x = 0 \ a < x \ x < b}" have ?thesis when "a\b" proof - have "S = {}" using that unfolding S_def by auto then show ?thesis using True unfolding taq_def by (fold S_def,simp) qed moreover have ?thesis when "a xa] unfolding greaterThanLessThan_unfold by simp then have "infinite S" unfolding S_def using True by auto then show ?thesis using True unfolding taq_def by (fold S_def,simp) qed ultimately show ?thesis by fastforce next case False show ?thesis unfolding cindex_poly_def taq_def by (rule sum.cong,auto simp add:jump_poly_sgn[OF \p\0\]) qed -section\Signed remainder sequence\ +subsection\Signed remainder sequence\ function smods:: "real poly \ real poly \ (real poly) list" where "smods p q= (if p=0 then [] else Cons p (smods q (-(p mod q))))" by auto termination apply (relation "measure (\(p,q).if p=0 then 0 else if q=0 then 1 else 2+degree q)") apply simp_all apply (metis degree_mod_less) done lemma smods_nil_eq:"smods p q = [] \ (p=0)" by auto lemma smods_singleton:"[x] = smods p q \ (p\0 \ q=0 \ x=p)" by (metis list.discI list.inject smods.elims) lemma smods_0[simp]: "smods 0 q = []" "smods p 0 = (if p=0 then [] else [p])" by auto lemma no_0_in_smods: "0\set (smods p q)" apply (induct "smods p q" arbitrary:p q) by (simp,metis list.inject neq_Nil_conv set_ConsD smods.elims) fun changes:: "('a ::linordered_idom) list \ int" where "changes [] = 0"| "changes [_] = 0" | "changes (x1#x2#xs) = (if x1*x2<0 then 1+changes (x2#xs) else if x2=0 then changes (x1#xs) else changes (x2#xs))" lemma changes_map_sgn_eq: "changes xs = changes (map sgn xs)" proof (induct xs rule:changes.induct) - case 1 - show ?case by simp -next - case 2 - show ?case by simp -next case (3 x1 x2 xs) moreover have "x1*x2<0 \ sgn x1 * sgn x2 < 0" by (unfold mult_less_0_iff sgn_less sgn_greater,simp) moreover have "x2=0 \ sgn x2 =0" by (rule sgn_0_0[symmetric]) ultimately show ?case by auto -qed +qed simp_all + +lemma changes_map_sign_eq: + "changes xs = changes (map sign xs)" +proof (induct xs rule:changes.induct) + case (3 x1 x2 xs) + moreover have "x1*x2<0 \ sign x1 * sign x2 < 0" + by (simp add: mult_less_0_iff sign_def) + moreover have "x2=0 \ sign x2 =0" by (simp add: sign_def) + ultimately show ?case by auto +qed simp_all + +lemma changes_map_sign_of_int_eq: + "changes xs = changes (map ((of_int::_\'c::{ring_1,linordered_idom}) o sign) xs)" +proof (induct xs rule:changes.induct) + case (3 x1 x2 xs) + moreover have "x1*x2<0 \ + ((of_int::_\'c::{ring_1,linordered_idom}) o sign) x1 + * ((of_int::_\'c::{ring_1,linordered_idom}) o sign) x2 < 0" + by (simp add: mult_less_0_iff sign_def) + moreover have "x2=0 \ (of_int o sign) x2 =0" by (simp add: sign_def) + ultimately show ?case by auto +qed simp_all definition changes_poly_at::"('a ::linordered_idom) poly list \ 'a \ int" where "changes_poly_at ps a= changes (map (\p. poly p a) ps)" definition changes_poly_pos_inf:: "('a ::linordered_idom) poly list \ int" where "changes_poly_pos_inf ps = changes (map sgn_pos_inf ps)" definition changes_poly_neg_inf:: "('a ::linordered_idom) poly list \ int" where "changes_poly_neg_inf ps = changes (map sgn_neg_inf ps)" lemma changes_poly_at_0[simp]: "changes_poly_at [] a =0" "changes_poly_at [p] a=0" unfolding changes_poly_at_def by auto definition changes_itv_smods:: "real \ real \real poly \ real poly \ int" where "changes_itv_smods a b p q= (let ps= smods p q in changes_poly_at ps a - changes_poly_at ps b)" definition changes_gt_smods:: "real \real poly \ real poly \ int" where "changes_gt_smods a p q= (let ps= smods p q in changes_poly_at ps a - changes_poly_pos_inf ps)" definition changes_le_smods:: "real \real poly \ real poly \ int" where "changes_le_smods b p q= (let ps= smods p q in changes_poly_neg_inf ps - changes_poly_at ps b)" definition changes_R_smods:: "real poly \ real poly \ int" where "changes_R_smods p q= (let ps= smods p q in changes_poly_neg_inf ps - changes_poly_pos_inf ps)" lemma changes_R_smods_0[simp]: "changes_R_smods 0 q = 0" "changes_R_smods p 0 = 0" unfolding changes_R_smods_def changes_poly_neg_inf_def changes_poly_pos_inf_def by auto lemma changes_itv_smods_0[simp]: "changes_itv_smods a b 0 q = 0" "changes_itv_smods a b p 0 = 0" unfolding changes_itv_smods_def by auto lemma changes_itv_smods_rec: assumes "a0" "poly (p*q) b\0" shows "changes_itv_smods a b p q = cross (p*q) a b + changes_itv_smods a b q (-(p mod q))" proof (cases "p=0 \ q=0 \ p mod q = 0") case True moreover have "p=0 \ q=0 \ ?thesis" unfolding changes_itv_smods_def changes_poly_at_def by (erule HOL.disjE,auto) moreover have "p mod q = 0 \ ?thesis" unfolding changes_itv_smods_def changes_poly_at_def cross_def apply (insert assms(2,3)) apply (subst (asm) (1 2) neq_iff) by (auto simp add: variation_cases) ultimately show ?thesis by auto next case False hence "p\0" "q\0" "p mod q\0" by auto then obtain ps where ps:"smods p q=p#q#-(p mod q)#ps" "smods q (-(p mod q)) = q#-(p mod q)#ps" by auto define changes_diff where "changes_diff\\x. changes_poly_at (p#q#-(p mod q)#ps) x - changes_poly_at (q#-(p mod q)#ps) x" have "\x. poly p x*poly q x<0 \ changes_diff x=1" unfolding changes_diff_def changes_poly_at_def by auto moreover have "\x. poly p x*poly q x>0 \ changes_diff x=0" unfolding changes_diff_def changes_poly_at_def by auto ultimately have "changes_diff a - changes_diff b=cross (p*q) a b" unfolding cross_def apply (cases rule:neqE[OF \poly (p*q) a\0\]) by (cases rule:neqE[OF \poly (p*q) b\0\],auto simp add:variation_cases)+ thus ?thesis unfolding changes_itv_smods_def changes_diff_def changes_poly_at_def using ps by auto qed lemma changes_smods_congr: fixes p q:: "real poly" assumes "a\a'" "poly p a\0" assumes "\p\set (smods p q). \x. ((ax\a') \ (a'\x \ x poly p x \0" shows "changes_poly_at (smods p q) a = changes_poly_at (smods p q) a'" using assms(2-3) proof (induct "smods p q" arbitrary:p q rule:length_induct) case 1 have "p\0" using \poly p a \0\ by auto define r1 where "r1\- (p mod q)" have a_a'_rel:"\pp\set (smods p q). poly pp a * poly pp a' \0" proof (rule ccontr) assume "\ (\pp\set (smods p q). 0 \ poly pp a * poly pp a')" then obtain pp where pp:"pp\set (smods p q)" " poly pp a * poly pp a'<0" using \p\0\ by (metis less_eq_real_def linorder_neqE_linordered_idom) hence "a False" using "1.prems"(2) poly_IVT[of a a' pp] by auto moreover have "a'False" using pp[unfolded mult.commute[of "poly pp a"]] "1.prems"(2) poly_IVT[of a' a pp] by auto ultimately show False using \a\a'\ by force qed have "q=0 \ ?case" by auto moreover have "\q\0;poly q a=0\ \ ?case" proof - assume "q\0" "poly q a=0" define r2 where "r2\- (q mod r1)" have "- poly r1 a = poly p a " by (metis \poly q a = 0\ add.inverse_inverse add.left_neutral div_mult_mod_eq mult_zero_right poly_add poly_minus poly_mult r1_def) hence "r1\0" and "poly r1 a\0" and "poly p a*poly r1 a<0" using \poly p a\0\ apply auto using mult_less_0_iff by fastforce then obtain ps where ps:"smods p q=p#q#r1#ps" "smods r1 r2=r1#ps" by (metis \p\0\ \q \ 0\ r1_def r2_def smods.simps) hence "length (smods r1 r2)p\set (smods r1 r2). \x. a < x \ x \ a' \ a' \ x \ x < a \ poly p x \ 0)" using "1.prems"(2) unfolding ps by auto ultimately have "changes_poly_at (smods r1 r2) a = changes_poly_at (smods r1 r2) a'" using "1.hyps" \r1\0\ \poly r1 a\0\ by metis moreover have "changes_poly_at (smods p q) a = 1+changes_poly_at (smods r1 r2) a" unfolding ps changes_poly_at_def using \poly q a=0\ \poly p a*poly r1 a<0\ by auto moreover have "changes_poly_at (smods p q) a' = 1+changes_poly_at (smods r1 r2) a'" proof - have "poly p a * poly p a' \0" and "poly r1 a*poly r1 a'\0" using a_a'_rel unfolding ps by auto moreover have "poly p a'\0" and "poly q a'\0" and "poly r1 a'\0" using "1.prems"(2)[unfolded ps] \a\a'\ by auto ultimately show ?thesis using \poly p a*poly r1 a<0\ unfolding ps changes_poly_at_def by (auto simp add: zero_le_mult_iff, auto simp add: mult_less_0_iff) qed ultimately show ?thesis by simp qed moreover have "\q\0;poly q a\0\ \ ?case" proof - assume "q\0" "poly q a\0" then obtain ps where ps:"smods p q=p#q#ps" "smods q r1=q#ps" by (metis \p\0\ r1_def smods.simps) hence "length (smods q r1) < length (smods p q)" by auto moreover have "(\p\set (smods q r1). \x. a < x \ x \ a' \ a' \ x \ x < a \ poly p x \ 0)" using "1.prems"(2) unfolding ps by auto ultimately have "changes_poly_at (smods q r1) a = changes_poly_at (smods q r1) a'" using "1.hyps" \q\0\ \poly q a\0\ by metis moreover have "poly p a'\0" and "poly q a'\0" using "1.prems"(2)[unfolded ps] \a\a'\ by auto moreover have "poly p a * poly p a' \0" and "poly q a*poly q a'\0" using a_a'_rel unfolding ps by auto ultimately show ?thesis unfolding ps changes_poly_at_def using \poly q a\0\ \poly p a\0\ by (auto simp add: zero_le_mult_iff,auto simp add: mult_less_0_iff) qed ultimately show ?case by blast qed lemma changes_itv_smods_congr: fixes p q:: "real poly" assumes "a0" "poly p b\0" assumes no_root:"\p\set (smods p q). \x. ((ax\a') \ (b'\x \ x poly p x \0" shows "changes_itv_smods a b p q=changes_itv_smods a' b' p q" proof - have "changes_poly_at (smods p q) a = changes_poly_at (smods p q) a'" apply (rule changes_smods_congr[OF order.strict_implies_not_eq[OF \a] \poly p a\0\]) by (metis assms(1) less_eq_real_def less_irrefl less_trans no_root) moreover have "changes_poly_at (smods p q) b = changes_poly_at (smods p q) b'" apply (rule changes_smods_congr[OF order.strict_implies_not_eq[OF \b', symmetric] \poly p b\0\]) by (metis assms(3) less_eq_real_def less_trans no_root) ultimately show ?thesis unfolding changes_itv_smods_def Let_def by auto qed lemma cindex_poly_changes_itv_mods: assumes "a0" "poly p b\0" shows "cindex_poly a b q p = changes_itv_smods a b p q" using assms proof (induct "smods p q" arbitrary:p q a b) case Nil hence "p=0" by (metis smods_nil_eq) thus ?case using \poly p a \ 0\ by simp next case (Cons x1 xs) have "p\0" using \poly p a \ 0\ by auto obtain a' b' where "ap\set (smods p q). \x. ((ax\a') \ (b'\x \ x poly p x \0" proof (induct "smods p q" arbitrary:p q thesis) case Nil define a' b' where "a'\2/3 * a + 1/3 * b" and "b'\1/3*a + 2/3*b" have "a < a'" and "a' < b'" and "b' < b" unfolding a'_def b'_def using \a by auto moreover have "\p\set (smods p q). \x. a < x \ x \ a' \ b' \ x \ x < b \ poly p x \ 0" unfolding \[] = smods p q\[symmetric] by auto ultimately show ?case using Nil by auto next case (Cons x1 xs) define r where "r\- (p mod q)" then have "smods p q = p # xs" and "smods q r = xs" and "p \ 0" using \x1 # xs = smods p q\ by (auto simp del: smods.simps simp add: smods.simps [of p q] split: if_splits) obtain a1 b1 where "a < a1" "a1 < b1" "b1 < b" and a1_b1_no_root:"\p\set xs. \x. a < x \ x \ a1 \ b1 \ x \ x < b \ poly p x \ 0" using Cons(1)[OF \smods q r=xs\[symmetric]] \smods q r=xs\ by auto obtain a2 b2 where "ax. a x\a2 \ poly p x \ 0" "b2x. b2\x \ x poly p x \ 0" using next_non_root_interval[OF \p\0\] last_non_root_interval[OF \p\0\] by (metis less_numeral_extra(3)) define a' b' where "a'\ if b2>a then Min{a1, b2, a2} else min a1 a2" and "b'\if a2 a < a1\ \a1 < b1\ \b1 < b\ \a \b2 \a by auto moreover have "\p\set xs. \x. a < x \ x \ a' \ b' \ x \ x < b \ poly p x \ 0" using a1_b1_no_root unfolding a'_def b'_def by auto moreover have "\x. a < x \ x \ a' \ b' \ x \ x < b \ poly p x \ 0" using a2 b2 unfolding a'_def b'_def by auto ultimately show ?case using Cons(3)[unfolded \smods p q=p#xs\] by auto qed have "q=0 \ ?case" by simp moreover have "q\0 \ ?case" proof - assume "q\0" define r where "r\- (p mod q)" obtain ps where ps:"smods p q=p#q#ps" "smods q r=q#ps" and "xs=q#ps" unfolding r_def using \q\0\ \p\0\ \x1 # xs = smods p q\ by (metis list.inject smods.simps) have "poly p a' \ 0" "poly p b' \ 0" "poly q a' \ 0" "poly q b' \ 0" using no_root[unfolded ps] \a'>a\ \b' by auto moreover hence "changes_itv_smods a' b' p q = cross (p * q) a' b' + changes_itv_smods a' b' q r" "cindex_poly a' b' q p = cross (p * q) a' b' + cindex_poly a' b' r q" using changes_itv_smods_rec[OF \a',of p q,folded r_def] cindex_poly_rec[OF \a',of p q,folded r_def] by auto moreover have "changes_itv_smods a' b' q r = cindex_poly a' b' r q" using Cons.hyps(1)[of q r a' b'] \a' < b'\ \q \ 0\ \xs = q # ps\ ps(2) \poly q a' \ 0\ \poly q b' \ 0\ by simp ultimately have "changes_itv_smods a' b' p q = cindex_poly a' b' q p" by auto thus ?thesis using changes_itv_smods_congr[OF \a \a' \b' Cons(4,5),of q] no_root cindex_poly_congr[OF \a \a' \b' ] ps by (metis insert_iff list.set(2)) qed ultimately show ?case by metis qed lemma root_list_ub: fixes ps:: "(real poly) list" and a::real assumes "0\set ps" obtains ub where "\p\set ps. \x. poly p x=0 \ xx\ub. \p\set ps. sgn (poly p x) = sgn_pos_inf p" and "ub>a" using assms proof (induct ps arbitrary:thesis) case Nil show ?case using Nil(1)[of "a+1"] by auto next case (Cons p ps) hence "p\0" and "0\set ps" by auto then obtain ub1 where ub1:"\p\set ps. \x. poly p x = 0 \ x < ub1" and ub1_sgn:"\x\ub1. \p\set ps. sgn (poly p x) = sgn_pos_inf p" and "ub1>a" using Cons.hyps by auto obtain ub2 where ub2:"\x. poly p x = 0 \ x < ub2" and ub2_sgn: "\x\ub2. sgn (poly p x) = sgn_pos_inf p" using root_ub[OF \p\0\] by auto define ub where "ub\max ub1 ub2" have "\p\set (p # ps). \x. poly p x = 0 \ x < ub" using ub1 ub2 ub_def by force moreover have "\x\ub. \p\set (p # ps). sgn (poly p x) = sgn_pos_inf p" using ub1_sgn ub2_sgn ub_def by auto ultimately show ?case using Cons(2)[of ub] \ub1>a\ ub_def by auto qed lemma root_list_lb: fixes ps:: "(real poly) list" and b::real assumes "0\set ps" obtains lb where "\p\set ps. \x. poly p x=0 \ x>lb" and "\x\lb. \p\set ps. sgn (poly p x) = sgn_neg_inf p" and "lb0" and "0\set ps" by auto then obtain lb1 where lb1:"\p\set ps. \x. poly p x = 0 \ x > lb1" and lb1_sgn:"\x\lb1. \p\set ps. sgn (poly p x) = sgn_neg_inf p" and "lb1x. poly p x = 0 \ x > lb2" and lb2_sgn: "\x\lb2. sgn (poly p x) = sgn_neg_inf p" using root_lb[OF \p\0\] by auto define lb where "lb\min lb1 lb2" have "\p\set (p # ps). \x. poly p x = 0 \ x > lb" using lb1 lb2 lb_def by force moreover have "\x\lb. \p\set (p # ps). sgn (poly p x) = sgn_neg_inf p" using lb1_sgn lb2_sgn lb_def by auto ultimately show ?case using Cons(2)[of lb] \lb1 lb_def by auto qed theorem sturm_tarski_interval: assumes "a0" "poly p b\0" shows "taq {x. poly p x=0 \ a x0" using \poly p a\0\ by auto thus ?thesis using cindex_poly_taq cindex_poly_changes_itv_mods[OF assms] by auto qed theorem sturm_tarski_above: assumes "poly p a\0" shows "taq {x. poly p x=0 \ asmods p (pderiv p * q)" have "p\0" and "p\set ps" using \poly p a\0\ ps_def by auto obtain ub where ub:"\p\set ps. \x. poly p x=0 \ xx\ub. \p\set ps. sgn (poly p x) = sgn_pos_inf p" and "ub>a" using root_list_ub[OF no_0_in_smods,of p "pderiv p * q",folded ps_def] by auto have "taq {x. poly p x=0 \ a a xp\set ps\,auto) moreover have "changes_gt_smods a p (pderiv p * q) = changes_itv_smods a ub p (pderiv p * q)" proof - have "map (sgn \ (\p. poly p ub)) ps = map sgn_pos_inf ps" using ub_sgn[THEN spec,of ub,simplified] by (metis (mono_tags, lifting) comp_def list.map_cong0) hence "changes_poly_at ps ub=changes_poly_pos_inf ps" unfolding changes_poly_pos_inf_def changes_poly_at_def by (subst changes_map_sgn_eq,metis map_map) thus ?thesis unfolding changes_gt_smods_def changes_itv_smods_def ps_def by metis qed moreover have "poly p ub\0" using ub \p\set ps\ by auto ultimately show ?thesis using sturm_tarski_interval[OF \ub>a\ assms] by auto qed theorem sturm_tarski_below: assumes "poly p b\0" shows "taq {x. poly p x=0 \ xsmods p (pderiv p * q)" have "p\0" and "p\set ps" using \poly p b\0\ ps_def by auto obtain lb where lb:"\p\set ps. \x. poly p x=0 \ x>lb" and lb_sgn:"\x\lb. \p\set ps. sgn (poly p x) = sgn_neg_inf p" and "lb x lb xp\set ps\,auto) moreover have "changes_le_smods b p (pderiv p * q) = changes_itv_smods lb b p (pderiv p * q)" proof - have "map (sgn \ (\p. poly p lb)) ps = map sgn_neg_inf ps" using lb_sgn[THEN spec,of lb,simplified] by (metis (mono_tags, lifting) comp_def list.map_cong0) hence "changes_poly_at ps lb=changes_poly_neg_inf ps" unfolding changes_poly_neg_inf_def changes_poly_at_def by (subst changes_map_sgn_eq,metis map_map) thus ?thesis unfolding changes_le_smods_def changes_itv_smods_def ps_def by metis qed moreover have "poly p lb\0" using lb \p\set ps\ by auto ultimately show ?thesis using sturm_tarski_interval[OF \lb _ assms] by auto qed theorem sturm_tarski_R: shows "taq {x. poly p x=0} q = changes_R_smods p (pderiv p * q)" proof (cases "p=0") case True then show ?thesis unfolding taq_def using infinite_UNIV_char_0 by (auto intro!:sum.infinite) next case False define ps where "ps\smods p (pderiv p * q)" have "p\set ps" using ps_def \p\0\ by auto obtain lb where lb:"\p\set ps. \x. poly p x=0 \ x>lb" and lb_sgn:"\x\lb. \p\set ps. sgn (poly p x) = sgn_neg_inf p" and "lb<0" using root_list_lb[OF no_0_in_smods,of p "pderiv p * q",folded ps_def] by auto obtain ub where ub:"\p\set ps. \x. poly p x=0 \ xx\ub. \p\set ps. sgn (poly p x) = sgn_pos_inf p" and "ub>0" using root_list_ub[OF no_0_in_smods,of p "pderiv p * q",folded ps_def] by auto have "taq {x. poly p x=0} q = taq {x. poly p x=0 \ lb xp\set ps\,auto) moreover have "changes_R_smods p (pderiv p * q) = changes_itv_smods lb ub p (pderiv p * q)" proof - have "map (sgn \ (\p. poly p lb)) ps = map sgn_neg_inf ps" and "map (sgn \ (\p. poly p ub)) ps = map sgn_pos_inf ps" using lb_sgn[THEN spec,of lb,simplified] ub_sgn[THEN spec,of ub,simplified] by (metis (mono_tags, lifting) comp_def list.map_cong0)+ hence "changes_poly_at ps lb=changes_poly_neg_inf ps \ changes_poly_at ps ub=changes_poly_pos_inf ps" unfolding changes_poly_neg_inf_def changes_poly_at_def changes_poly_pos_inf_def by (subst (1 3) changes_map_sgn_eq,metis map_map) thus ?thesis unfolding changes_R_smods_def changes_itv_smods_def ps_def by metis qed moreover have "poly p lb\0" and "poly p ub\0" using lb ub \p\set ps\ by auto moreover have "lblb<0\ \0 by auto ultimately show ?thesis using sturm_tarski_interval by auto qed theorem sturm_interval: assumes "a < b" "poly p a \ 0" "poly p b \ 0" shows "card {x. poly p x = 0 \ a < x \ x < b} = changes_itv_smods a b p (pderiv p)" using sturm_tarski_interval[OF assms, unfolded taq_def,of 1] by force theorem sturm_above: assumes "poly p a \ 0" shows "card {x. poly p x = 0 \ a < x} = changes_gt_smods a p (pderiv p)" using sturm_tarski_above[OF assms, unfolded taq_def,of 1] by force theorem sturm_below: assumes "poly p b \ 0" shows "card {x. poly p x = 0 \ x < b} = changes_le_smods b p (pderiv p)" using sturm_tarski_below[OF assms, unfolded taq_def,of 1] by force theorem sturm_R: shows "card {x. poly p x=0} = changes_R_smods p (pderiv p)" using sturm_tarski_R[of _ 1,unfolded taq_def] by force end diff --git a/thys/Sturm_Tarski/Tarski_Query_Impl.thy b/thys/Sturm_Tarski/Tarski_Query_Impl.thy new file mode 100644 --- /dev/null +++ b/thys/Sturm_Tarski/Tarski_Query_Impl.thy @@ -0,0 +1,241 @@ +(* + File: Pseudo_Remainder_Sequence.thy + Author: Wenda Li +*) + +section \TaQ for polynomials with rational coefficients\ + +theory Tarski_Query_Impl imports + Pseudo_Remainder_Sequence Sturm_Tarski +begin + +global_interpretation rat_int:hom_pseudo_smods rat_of_int real_of_int real_of_rat + defines + ri_changes_itv_spmods = rat_int.changes_itv_spmods and + ri_changes_gt_spmods = rat_int.changes_gt_spmods and + ri_changes_le_spmods = rat_int.changes_le_spmods and + ri_changes_R_spmods = rat_int.changes_R_spmods + apply unfold_locales + by (simp_all add: of_rat_less of_rat_less_eq) + +definition TaQ_R_rats::"rat poly \ rat poly \ int" where + "TaQ_R_rats p q = taq {x. poly (map_poly real_of_rat p) x = (0::real)} + (map_poly real_of_rat q)" + +definition TaQ_itv_rats::"rat \ rat \ rat poly \ rat poly \ int" where + "TaQ_itv_rats a b p q = taq {x. poly (map_poly real_of_rat p) x = (0::real) + \ of_rat a < x \ x < of_rat b} (map_poly real_of_rat q)" + +definition TaQ_gt_rats::" rat \ rat poly \ rat poly \ int" where + "TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat p) x = (0::real) + \ of_rat a < x } (map_poly real_of_rat q)" + +definition TaQ_le_rats::"rat \ rat poly \ rat poly \ int" where + "TaQ_le_rats b p q = taq {x. poly (map_poly real_of_rat p) x = (0::real) + \ x < of_rat b} (map_poly real_of_rat q)" + +lemma taq_smult_pos: + assumes "a>0" + shows "taq s (smult a p) = taq s p" + unfolding taq_def by (simp add: assms sign_times) + +lemma taq_proots_R_code[code]: + "TaQ_R_rats p q = (let + ip = clear_de p; + iq = clear_de q + in ri_changes_R_spmods ip (pderiv ip * iq))" +proof - + define ip iq where "ip = clear_de p" and "iq = clear_de q" + define dp dq where "dp = rat_of_int (de_lcm p)" and "dq = rat_of_int (de_lcm q)" + + have "dp > 0" "dq>0" + unfolding dp_def dq_def by simp_all + have ip:"of_int_poly ip = smult dp p" and iq:"of_int_poly iq = smult dq q" + using clear_de unfolding ip_def iq_def dp_def dq_def by auto + + have "TaQ_R_rats p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0} + (map_poly real_of_rat (of_int_poly iq))" + unfolding TaQ_R_rats_def ip iq using \dp > 0\ \dq >0\ + by (simp add:of_rat_hom.map_poly_hom_smult taq_smult_pos) + also have "... = taq {x. poly (of_int_poly ip) x = (0::real)} (of_int_poly iq)" + by (simp add:map_poly_map_poly comp_def) + also have "... = changes_R_smods (of_int_poly ip) (pderiv (of_int_poly ip) * of_int_poly iq)" + using sturm_tarski_R by simp + also have "... = changes_R_smods (of_int_poly ip) (of_int_poly (pderiv ip * iq))" + by (simp add: of_int_hom.map_poly_pderiv of_int_poly_hom.hom_mult) + also have "... = ri_changes_R_spmods ip (pderiv ip * iq)" + using rat_int.changes_spmods_smods by simp + finally have "TaQ_R_rats p q = ri_changes_R_spmods ip (pderiv ip * iq) " . + then show ?thesis unfolding Let_def ip_def iq_def . +qed + +lemma taq_proots_itv_code[code]: + "TaQ_itv_rats a b p q = (if a\b then + 0 + else if poly p a \ 0 \ poly p b \0 then + (let + ip = clear_de p; + iq = clear_de q + in ri_changes_itv_spmods a b ip (pderiv ip * iq)) + else + Code.abort (STR ''Roots at border yet to be supported'') + (\_. TaQ_itv_rats a b p q) + )" +proof (cases "a\b \ poly p a = 0 \ poly p b = 0") + case True + moreover have ?thesis if "a\b" + proof - + have "{x. poly (map_poly of_rat p) x = 0 \ real_of_rat a < x \ x < real_of_rat b} + = {}" + using that rat_int.r2.hom_less_eq by fastforce + then have "TaQ_itv_rats a b p q = taq {} (map_poly real_of_rat q)" + unfolding TaQ_itv_rats_def by metis + also have "... = 0" + unfolding taq_def by simp + finally show ?thesis using that by auto + qed + moreover have ?thesis if "\ a\b" "poly p a = 0 \ poly p b = 0" + using that by auto + ultimately show ?thesis by auto +next + case False + + define ip iq where "ip = clear_de p" and "iq = clear_de q" + define dp dq where "dp = rat_of_int (de_lcm p)" and "dq = rat_of_int (de_lcm q)" + define aa bb where "aa = real_of_rat a" and "bb = real_of_rat b" + + have "dp > 0" "dq>0" + unfolding dp_def dq_def by simp_all + have ip:"of_int_poly ip = smult dp p" and iq:"of_int_poly iq = smult dq q" + using clear_de unfolding ip_def iq_def dp_def dq_def by auto + + have "TaQ_itv_rats a b p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 + \ aa < x \ x < bb} + (map_poly real_of_rat (of_int_poly iq))" + unfolding TaQ_itv_rats_def ip iq aa_def bb_def using \dp > 0\ \dq >0\ + by (simp add:of_rat_hom.map_poly_hom_smult taq_smult_pos) + also have "... = taq {x. poly (of_int_poly ip) x = (0::real) + \ aa < x \ x < bb} (of_int_poly iq)" + by (simp add:map_poly_map_poly comp_def) + also have "... = changes_itv_smods aa bb (of_int_poly ip) + (pderiv (of_int_poly ip) * of_int_poly iq)" + proof - + have "aa < bb" "poly (map_poly of_int ip) aa \ 0" + "poly (map_poly of_int ip) bb \ 0" + unfolding aa_def bb_def + subgoal by (meson False not_less of_rat_less) + subgoal using False \0 < dp\ ip rat_int.map_poly_R_hom_commute by force + subgoal using False \0 < dp\ ip rat_int.map_poly_R_hom_commute by force + done + from sturm_tarski_interval[OF this] + show ?thesis by auto + qed + also have "... = changes_itv_smods aa bb (of_int_poly ip) (of_int_poly (pderiv ip * iq))" + by (simp add: of_int_hom.map_poly_pderiv of_int_poly_hom.hom_mult) + also have "... = ri_changes_itv_spmods a b ip (pderiv ip * iq)" + using rat_int.changes_spmods_smods unfolding aa_def bb_def by simp + finally have "TaQ_itv_rats a b p q = ri_changes_itv_spmods a b ip (pderiv ip * iq) " . + then show ?thesis unfolding Let_def ip_def iq_def using False by presburger +qed + +lemma taq_proots_gt_code[code]: + "TaQ_gt_rats a p q = ( + if poly p a \ 0 then + (let + ip = clear_de p; + iq = clear_de q + in ri_changes_gt_spmods a ip (pderiv ip * iq)) + else + Code.abort (STR ''Roots at border yet to be supported'') + (\_. TaQ_gt_rats a p q) + )" +proof (cases "poly p a = 0") + case True + then show ?thesis by auto +next + case False + + define ip iq where "ip = clear_de p" and "iq = clear_de q" + define dp dq where "dp = rat_of_int (de_lcm p)" and "dq = rat_of_int (de_lcm q)" + define aa where "aa = real_of_rat a" + + have "dp > 0" "dq>0" + unfolding dp_def dq_def by simp_all + have ip:"of_int_poly ip = smult dp p" and iq:"of_int_poly iq = smult dq q" + using clear_de unfolding ip_def iq_def dp_def dq_def by auto + + have "TaQ_gt_rats a p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 + \ aa < x} + (map_poly real_of_rat (of_int_poly iq))" + unfolding TaQ_gt_rats_def ip iq aa_def using \dp > 0\ \dq >0\ + by (simp add:of_rat_hom.map_poly_hom_smult taq_smult_pos) + also have "... = taq {x. poly (of_int_poly ip) x = (0::real) + \ aa < x } (of_int_poly iq)" + by (simp add:map_poly_map_poly comp_def) + also have "... = changes_gt_smods aa (of_int_poly ip) + (pderiv (of_int_poly ip) * of_int_poly iq)" + proof - + have "poly (map_poly of_int ip) aa \ 0" + unfolding aa_def using False \0 < dp\ ip rat_int.map_poly_R_hom_commute by force + from sturm_tarski_above[OF this] + show ?thesis by auto + qed + also have "... = changes_gt_smods aa (of_int_poly ip) (of_int_poly (pderiv ip * iq))" + by (simp add: of_int_hom.map_poly_pderiv of_int_poly_hom.hom_mult) + also have "... = ri_changes_gt_spmods a ip (pderiv ip * iq)" + using rat_int.changes_spmods_smods unfolding aa_def by simp + finally have "TaQ_gt_rats a p q = ri_changes_gt_spmods a ip (pderiv ip * iq) " . + then show ?thesis unfolding Let_def ip_def iq_def using False by presburger +qed + +lemma taq_proots_le_code[code]: + "TaQ_le_rats b p q = ( + if poly p b \0 then + (let + ip = clear_de p; + iq = clear_de q + in ri_changes_le_spmods b ip (pderiv ip * iq)) + else + Code.abort (STR ''Roots at border yet to be supported'') + (\_. TaQ_le_rats b p q) + )" +proof (cases "poly p b = 0") + case True + then show ?thesis by auto +next + case False + + define ip iq where "ip = clear_de p" and "iq = clear_de q" + define dp dq where "dp = rat_of_int (de_lcm p)" and "dq = rat_of_int (de_lcm q)" + define bb where "bb = real_of_rat b" + + have "dp > 0" "dq>0" + unfolding dp_def dq_def by simp_all + have ip:"of_int_poly ip = smult dp p" and iq:"of_int_poly iq = smult dq q" + using clear_de unfolding ip_def iq_def dp_def dq_def by auto + + have "TaQ_le_rats b p q = taq {x. poly (map_poly real_of_rat (of_int_poly ip)) x = 0 + \ x < bb} + (map_poly real_of_rat (of_int_poly iq))" + unfolding TaQ_le_rats_def ip iq bb_def using \dp > 0\ \dq >0\ + by (simp add:of_rat_hom.map_poly_hom_smult taq_smult_pos) + also have "... = taq {x. poly (of_int_poly ip) x = (0::real) + \ x < bb} (of_int_poly iq)" + by (simp add:map_poly_map_poly comp_def) + also have "... = changes_le_smods bb (of_int_poly ip) + (pderiv (of_int_poly ip) * of_int_poly iq)" + proof - + have "poly (map_poly of_int ip) bb \ 0" + unfolding bb_def using False \0 < dp\ ip rat_int.map_poly_R_hom_commute by force + from sturm_tarski_below[OF this] + show ?thesis by auto + qed + also have "... = changes_le_smods bb (of_int_poly ip) (of_int_poly (pderiv ip * iq))" + by (simp add: of_int_hom.map_poly_pderiv of_int_poly_hom.hom_mult) + also have "... = ri_changes_le_spmods b ip (pderiv ip * iq)" + using rat_int.changes_spmods_smods unfolding bb_def by simp + finally have "TaQ_le_rats b p q = ri_changes_le_spmods b ip (pderiv ip * iq) " . + then show ?thesis unfolding Let_def ip_def iq_def using False by presburger +qed + +end \ No newline at end of file