Theory Sturm_Tarski.Sturm_Tarski

(*  Title: Sturm-Tarski Theorem
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section "Sturm--Tarski Theorem"

theory Sturm_Tarski
  imports Complex_Main PolyMisc "HOL-Computational_Algebra.Field_as_Ring"
begin

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)  (b<x. y>b. y < x  P y)"
proof -
  obtain y where "y<x" 
    using linordered_field_no_lb by auto
  thus ?thesis using eventually_at_left[OF y<x] by auto
qed

lemma eventually_neg:
  assumes "Fbot"  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 Fbot 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. lb<zzubpoly p z0)  
    (z. lb<zzubpoly p z>0)(z. lb<zzubpoly p z<0)" (is "?Q  ?P")
proof (rule,rule ccontr)
  assume "?Q" "¬?P" 
  then obtain z1 z2 where z1:"lb<z1" "z1ub" "poly p z10" 
                      and z2:"lb<z2" "z2ub" "poly p z20"
    by auto
  hence "z. lb<zzubpoly 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 "z1z2" 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. lbzz<ubpoly p z0) 
    (z. lbzz<ubpoly p z>0)(z. lbzz<ubpoly p z<0)" (is "?Q?P")
proof (rule,rule ccontr)
  assume "?Q" "¬?P"
  then obtain z1 z2 where z1:"lbz1" "z1<ub" "poly p z10" 
                      and z2:"lbz2" "z2<ub" "poly p z20"
    by auto
  hence "z. lbzz<ubpoly 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 "z1z2" 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 "p0"
  obtains ub where "ub>lb" and "(z. lb<zzubpoly p z0)" 
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 "lrMin {r . poly p r=0  r>lb}" 
  have "z. lb<zz<lrpoly p z0" and "lr>lb" 
    using True lr_def poly_roots_finite[OF p0] by auto
  thus ?thesis using that[of "(lb+lr)/2"] by auto 
qed

lemma last_non_root_interval:
  fixes p::"real poly"
  assumes "p0"
  obtains lb where "lb<ub" and "(z. lbzz<ubpoly p z0)"
proof (cases "( r. poly p r=0  r<ub)")
  case False
  thus ?thesis by (intro that[of "ub - 1"]) auto
next
  case True
  define mr where  "mrMax {r . poly p r=0  r<ub}" 
  have "z. mr<zz<ubpoly p z0" and "mr<ub" 
    using True mr_def poly_roots_finite[OF p0] by auto
  thus ?thesis using that[of "(mr+ub)/2"] mr<ub by auto
qed

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 "a0;p=0  ?case" by auto
  moreover have "p0  ?case"
  proof -
    assume "p0"
    then obtain n1 where gte_lcoeff:"xn1. lead_coeff p  poly p x" using that pCons by auto
    have gt_0:"lead_coeff p >0" using pCons(3) p0 by auto
    define n where "nmax 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 "x1+ ¦a¦/(poly p x)" using nx[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 p0
        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:"xub. 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 p0] 
      by (auto simp add:not_less_iff_gr_or_eq)
    then obtain n where "xn. 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 "p0"
  obtains ub where "x. poly p x=0  x<ub"
    and "xub. sgn (poly p x) = sgn_pos_inf p"
proof -
  obtain ub1 where ub1:"x. poly p x=0  x<ub1"
  proof (cases " r. poly p r=0")
    case False
    thus ?thesis using that by auto
  next
    case True
    define max_r where "max_rMax {x . poly p x=0}"
    hence "x. poly p x=0  xmax_r"
      using  poly_roots_finite[OF p0] 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:"xub2. sgn (poly p x) = sgn_pos_inf p"
    using poly_sgn_eventually_at_top[unfolded eventually_at_top_linorder] by auto
  define ub where "ubmax ub1 ub2"
  have "x. poly p x=0  x<ub" using ub1 ub_def 
    by (metis eq_iff less_eq_real_def less_linear max.bounded_iff)
  thus ?thesis using that[of ub] ub2 ub_def by auto
qed

lemma root_lb:
  fixes p:: "real poly"
  assumes "p0"
  obtains lb where "x. poly p x=0  x>lb"
    and "xlb. 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_rMin {x . poly p x=0}"
    hence "x. poly p x=0  xmin_r"
      using  poly_roots_finite[OF p0] True by auto
    thus ?thesis using that[of "min_r - 1"] by (metis lt_ex order.strict_trans2 that) 
  qed
  obtain lb2 where lb2:"xlb2. sgn (poly p x) = sgn_neg_inf p"
    using poly_sgn_eventually_at_bot[unfolded eventually_at_bot_linorder] by auto
  define lb where  "lbmin 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

subsection ‹Variation and cross›

definition variation :: "real   real  int" where
  "variation x y=(if x*y0 then 0 else if x<y then 1 else -1)" 

definition cross :: "real poly  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>0variation x y = 0" 
  "x>0;y<0variation x y = -1"
  "x<0;y>0variation x y = 1"
  "x<0;y<0variation x y = 0"
proof -
  show "x>0;y>0variation x y = 0"  unfolding variation_def by auto
  show "x>0;y<0variation x y = -1" unfolding variation_def  
    using mult_pos_neg by fastforce
  show "x<0;y>0variation x y = 1" unfolding variation_def 
    using mult_neg_pos by fastforce
  show "x<0;y<0variation 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 "¬ 0x * 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 "a<b" and no_root:"x. a<xx<b  poly p x0"
  shows "cross p a b=0"
proof -
  have "poly p a>0;poly p b<0  False" using poly_IVT_neg[OF a<b] no_root by auto
  moreover have "poly p a<0;poly p b>0  False" using poly_IVT_pos[OF a<b] 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

subsection ‹Tarski query›

definition taq :: "'a::linordered_idom set  'a poly  int" where
  "taq s q  xs. sign (poly q x)"

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 "p0"
  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 "z<b" and "poly p 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 z0z>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 p0" using poly p x=0 p0 
      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. x<zz<ubpoly (pderiv p) z>0) 
           (z. x<zz<ubpoly (pderiv p) z<0)"
      using next_non_root_interval[OF pderiv p0, of x,unfolded not_eq_pos_or_neg_iff_1] 
      by (metis order.strict_implies_order)
    have "z. x<zz<ubpoly (pderiv p) z<0  False" 
    proof -
      assume assm:"z. x<zz<ubpoly (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 "x<z'" and "z' < (x+(min ub' ub))/2"
          and z':"poly p ((x+min ub' ub)/2) = ((x+min ub' ub)/2 - x) * poly (pderiv p) z'"       
        using poly_MVT[of x "(x+min ub' ub)/2" p] ub'>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<z'
        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' z' < (x+(min ub' ub))/2 by auto
    qed
    hence "z. x<zz<ubpoly (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 "p0"
  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 p0,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 "c0" "p0"
  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 p0, of x] ¬ c>0 by auto
qed

lemma sign_r_pos_mult:
  fixes p q :: "real poly"
  assumes "p0" "q0"
  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 p0,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 q0,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 p0 q0 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 p0 q0 
      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 p0 q0 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 x0"
  shows "sign_r_pos (p+q) x=sign_r_pos q x"
proof (cases "poly (p+q) x=0")
  case False
  hence "p+q0" by (metis poly_0)
  have "sign_r_pos (p+q) x = (poly q x > 0)"  
    using sign_r_pos_rec[OF p+q0] 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 x0 poly_0 by force
  ultimately show ?thesis by auto
next
  case True
  hence False using poly p x=0 poly q x0 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 x0"
  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 x0 
    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" "p0"
  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 p0] by auto
  also have "...=((sign_r_pos (pderiv p) x  sign_r_pos (pderiv p) x))"
    using sign_r_pos_rec[OF p0] 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

subsection‹Jump›

definition jump_poly :: "real poly  real poly real  int"
 where 
 " jump_poly q p x (if p0  q0  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 x0 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 "c0" and "q0" by auto
  thus ?thesis unfolding jump_poly_def
     using order_smult[OF c0] sign_r_pos_smult[OF c0, of "q*p" x] q0 
     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 "q0" "p0" 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 "lrMin {r . poly p' r=0  r>x}" 
      have "z. x<zz<lrpoly p' z0" 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. x<zz<x+1poly p' z0" 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 "0<poly (p'*p') z" using b by auto
      have " (0 < poly (p' * q * (p' * p)) z)=(0<poly (p'*p') z * poly (q*p) z)" 
        by (simp add: mult.commute mult.left_commute)
      also have "...=(0<poly (q*p) z)"
        using 0<poly (p'*p') z 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 p0 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 x0  poly p2 x0" 
  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 "p10" "p20" "p1*p20" by auto
  have ?thesis when "poly p1 x0"
  proof -
    have [simp]:"order x p1 = 0" using that order_root by blast
    define simpL where "simpL(if p20  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*p20]
        sign_r_pos_mult[OF p10 p20] sign_r_pos_rec[OF p10] poly p1 x0
      by auto
    moreover have "poly p1 x>0  simpL =?R" 
      unfolding simpL_def jump_poly_def using jump_poly_not_root[OF poly p1 x0] 
      by auto
    moreover have "poly p1 x<0  simpL =?R" 
      unfolding simpL_def jump_poly_def using jump_poly_not_root[OF poly p1 x0] 
      by auto
    ultimately show "?L=?R" using poly p1 x0 by (metis linorder_neqE_linordered_idom)
  qed
  moreover have ?thesis when "poly p2 x0"
  proof -
    have [simp]:"order x p2 = 0" using that order_root by blast
    define simpL where "simpL(if p10  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*p20]
        sign_r_pos_mult[OF p10 p20] sign_r_pos_rec[OF p20] poly p2 x0
      by auto
    moreover have "poly p2 x>0  simpL =?R" 
      unfolding simpL_def jump_poly_def using jump_poly_not_root[OF poly p2 x0] 
      by auto
    moreover have "poly p2 x<0  simpL =?R" 
      unfolding simpL_def jump_poly_def using jump_poly_not_root[OF poly p2 x0] 
      by auto
    ultimately show "?L=?R" using poly p2 x0 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 "p0" "q0" by auto
  define n where "nmin (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' p0 q0 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 q0[unfolded q'],of x] order_mult[OF p0[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' x0" 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 "p0" "q0" by auto
  then have "poly p x0  poly q x0" using coprime_poly_0[OF coprime p q] by auto    
  then have "poly q x0" 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 p0 q0 order_mult [of q p x] by auto
  then show ?thesis unfolding jump_poly_def using q0 by auto   
qed    
 
lemma jump_poly_sgn:
  fixes p q:: "real poly"
  assumes "p0" "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 p0" using p0 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 p0 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 p0, of x] poly p x=0 order_root[of p x] p0 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 p0] by auto
  qed 
  define simpleL where "simpleLif 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 q0 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 x0 simpleL=sign (poly q x)"
  proof -
    assume "poly q x0"
    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 x0 by auto 
    ultimately have "simpleL=(if poly q x>0 then 1 else - 1)" unfolding simpleL_def by auto
    thus ?thesis using poly q x0 by auto
  qed
  ultimately show ?thesis by force
qed
 
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  "a<b" "poly p a0" "poly p b0"
  shows "cindex_poly a b 1 p = cross p a b" 
    using poly p a0 poly p b0
proof (cases "{x. poly p x=0  a< x x< b}{}", induct "degree p" arbitrary:p rule:nat_less_induct) 
  case 1
  then have "p0" 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 p0] by auto
  define max_r where "max_rMax roots"
  hence "poly p max_r=0" and "a<max_r" and "max_r<b" 
    using Max_in[OF finite 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 p0 mult.commute order_decomp)
  hence "p'0" and "max_rp0" and "poly p' a0" and "poly p' b0" 
      and  "poly max_rp a0" and "poly max_rp b0" 
    using p0 poly p a0 poly p b0  by auto
  define max_r_sign where "max_r_signif odd(order max_r p) then -1 else 1::int"
  define roots' where "roots'{x.  a< x x< b  poly p' x=0}"
  have "(xroots. jump_poly 1 p x)= (xroots'. 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 max_r<b,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' p0 by (metis finite roots calculation(1) calculation(2) finite_Un)
    ultimately show ?thesis using sum.union_disjoint by auto
  qed
  moreover have "(xroots'. jump_poly 1 p x) = max_r_sign * cross p' a b"
  proof -
    have "(xroots'. jump_poly 1 p x) = (xroots'. max_r_sign * jump_poly 1 p' x)"
    proof (rule sum.cong,rule refl)
      fix x assume "x  roots'" 
      hence "xmax_r" using not_dvd unfolding roots'_def 
        by (metis (mono_tags, lifting) mem_Collect_eq poly_eq_0_iff_dvd )
      hence "poly max_rp x0" 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 x0 by (metis jump_poly_not_root)
      moreover have "xroots"
        using x  roots' unfolding roots_def roots'_def p' by auto
      hence "x<max_r" 
        using Max_ge[OF finite roots,of x] xmax_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 * (xroots'. 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<b] by auto 
        thus ?thesis using True by simp
      next
        case False
        moreover have "degree max_rp0" 
          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_rp0]
          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' a0 poly p' b0 
          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 a0 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<b  
        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' b0
        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' b0 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 "r<b" and "poly p' r=0"
            using poly_IVT[OF max_r<b] by auto
          hence "rroots" 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' b0 max_rp0 p'0 sign_r_pos_mult[OF p'0 max_rp0]
          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 a0 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<b] 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 p0 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 "p0" "q0" 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  x<b }" unfolding poly_mult A_def B_def by auto
  moreover have "A  B={}" 
  proof (rule ccontr)
    assume "A  B{}"
    then obtain x where "xA" and "xB" by auto
    hence "poly p x=0" and "poly q x=0" unfolding A_def B_def by auto
    hence "gcd p q1" 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 p0 q0 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<x  x<b}"
    using sum.union_disjoint by metis 
  then show ?thesis unfolding cindex_poly_def by auto 
qed  

lemma cindex_poly_inverse_add_cross:
  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 + cindex_poly a b p q = cross (p * q) a b" (is "?L=?R")
proof -
  have "p0" and "q0" using poly (p * q) a 0 by auto
  define g where "ggcd 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 p0 unfolding g_def by auto
  have "p'0" "q'0" "g 0" using p' q' p0 q0 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 g0] cindex_poly_mult[OF g0]
    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<b, 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 a0" 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 b0" 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 "q0" 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 "a<a'" "a'<b'" "b'<b" 
  assumes "x. ((a<xxa')  (b'x  x<b))  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 p0] by auto
    subgoal using assms by auto
    subgoal using assms(4) by fastforce
    done
qed    
  
lemma greaterThanLessThan_unfold:"{a<..<b} = {x. a<x  x<b}" 
  by fastforce
  
lemma cindex_poly_taq:
  fixes p q::"real poly"
  shows "taq {x. poly p x = 0  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 "ab" 
  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<b"
  proof -
    have "infinite {x. a<x  x<b}" using infinite_Ioo[OF a<b] 
      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 p0]) 
qed  

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  (p0  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: "0set (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 (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 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 "a<b" "poly (p*q) a0" "poly (p*q) b0"
  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 "p0" "q0" "p mod q0" 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) a0])
    by (cases rule:neqE[OF poly (p*q) b0],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 "aa'" "poly p a0"
  assumes "pset (smods p q). x. ((a<xxa')  (a'x  x<a))  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 "p0" using poly p a 0 by auto
  define r1 where "r1- (p mod q)"
  have a_a'_rel:"ppset (smods p q). poly pp a * poly pp a' 0"
  proof (rule ccontr)
    assume "¬ (ppset (smods p q). 0  poly pp a * poly pp a')"
    then obtain pp where pp:"ppset (smods p q)" " poly pp a * poly pp a'<0"
      using p0 by (metis less_eq_real_def linorder_neqE_linordered_idom)
    hence "a<a'  False" using "1.prems"(2) poly_IVT[of a a' pp] by auto
    moreover have "a'<aFalse" 
      using pp[unfolded mult.commute[of "poly pp a"]] "1.prems"(2) poly_IVT[of a' a pp] by auto
    ultimately show False using aa' by force
  qed
  have "q=0  ?case" by auto
  moreover have "q0;poly q a=0  ?case"
  proof -     
    assume "q0" "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 "r10" and "poly r1 a0" and "poly p a*poly r1 a<0" using poly p a0 
      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 p0 q  0 r1_def r2_def smods.simps)
    hence "length (smods r1 r2)<length (smods p q)" by auto
    moreover have "(pset (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" r10 poly r1 a0 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] aa' 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 "q0;poly q a0  ?case"
  proof -
    assume "q0" "poly q a0"
    then obtain ps where ps:"smods p q=p#q#ps" "smods q r1=q#ps" 
      by (metis p0 r1_def smods.simps)
    hence "length (smods q r1) < length (smods p q)" by auto
    moreover have "(pset (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" q0 poly q a0 by metis
    moreover have "poly p a'0" and "poly q a'0" 
      using "1.prems"(2)[unfolded ps] aa' 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 a0 poly p a0
      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 "a<a'" "a'<b'" "b'<b" "poly p a0" "poly p b0"
  assumes no_root:"pset (smods p q). x. ((a<xxa')  (b'x  x<b))  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<a'] poly p a0])
    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'<b, 
        symmetric] poly p b0])
    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 "a<b" "poly p a0" "poly p b0"
  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 "p0" using poly p a  0 by auto
  obtain a' b' where "a<a'" "a'<b'" "b'<b" 
      and no_root:"pset (smods p q). x. ((a<xxa')  (b'x  x<b))  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<b by auto
    moreover have "pset (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:"pset 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
          "a<a2" and a2:"x. a<x  xa2  poly p x  0"
          "b2<b" and b2:"x. b2x  x<b  poly p x  0"
        using next_non_root_interval[OF p0] last_non_root_interval[OF p0] 
        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 <b then Max{ b1, a2, b2} else max b1 b2"
    have "a < a'" "a' < b'" "b' < b" unfolding a'_def b'_def 
        using  a < a1 a1 < b1 b1 < b a<a2 b2<b a<b by auto
    moreover have "pset 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 "q0  ?case"
  proof -
    assume "q0"
    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 q0 p0 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'<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'<b',of p q,folded r_def] 
          cindex_poly_rec[OF a'<b',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' a'<b' b'<b Cons(4,5),of q]
          no_root cindex_poly_congr[OF a<a' a'<b' b'<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 "0set ps"
  obtains ub where "pset ps. x. poly p x=0  x<ub"
    and "xub. pset 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 "p0" and "0set ps" by auto
  then obtain ub1 where ub1:"pset ps. x. poly p x = 0  x < ub1" and
      ub1_sgn:"xub1. pset 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: "xub2. sgn (poly p x) = sgn_pos_inf p"
    using root_ub[OF p0] by auto
  define ub where "ubmax ub1 ub2"
  have "pset (p # ps). x. poly p x = 0  x < ub" using ub1 ub2 ub_def by force
  moreover have "xub. pset (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 "0set ps"
  obtains lb where "pset ps. x. poly p x=0  x>lb"
    and "xlb. pset ps. sgn (poly p x) = sgn_neg_inf p" and "lb<b"
    using assms
proof (induct ps arbitrary:thesis)
  case Nil
  show ?case using Nil(1)[of "b - 1"] by auto
next
  case (Cons p ps)
  hence "p0" and "0set ps" by auto
  then obtain lb1 where lb1:"pset ps. x. poly p x = 0  x > lb1" and
      lb1_sgn:"xlb1. pset ps. sgn (poly p x) = sgn_neg_inf p" and "lb1<b"
    using Cons.hyps by auto
  obtain lb2 where lb2:"x. poly p x = 0  x > lb2" 
      and lb2_sgn: "xlb2. sgn (poly p x) = sgn_neg_inf p"
    using root_lb[OF p0] by auto
  define lb where "lbmin lb1 lb2"
  have "pset (p # ps). x. poly p x = 0  x > lb" using lb1 lb2 lb_def by force
  moreover have "xlb. pset (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<b lb_def by auto
qed

theorem sturm_tarski_interval: 
  assumes "a<b" "poly p a0" "poly p b0"
  shows "taq {x. poly p x=0  a<x  x<b} q = changes_itv_smods a b p (pderiv p * q)" 
proof -
  have "p0" using poly p a0 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 a0" 
  shows "taq {x. poly p x=0  a<x} q = changes_gt_smods a p (pderiv p * q)"
proof -
  define ps where "pssmods p (pderiv p * q)"
  have "p0" and "pset ps" using poly p a0 ps_def by auto
  obtain ub where ub:"pset ps. x. poly p x=0  x<ub"
      and ub_sgn:"xub. pset 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<x} q = taq {x. poly p x=0  a<x  x<ub} q"
    unfolding taq_def by (rule sum.cong,insert ub pset 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 ub0" using ub pset ps by auto
  ultimately show ?thesis using sturm_tarski_interval[OF ub>a assms] by auto
qed

theorem sturm_tarski_below: 
  assumes "poly p b0" 
  shows "taq {x. poly p x=0  x<b} q = changes_le_smods b p (pderiv p * q)"
proof -
  define ps where "pssmods p (pderiv p * q)"
  have "p0" and "pset ps" using poly p b0 ps_def by auto
  obtain lb where lb:"pset ps. x. poly p x=0  x>lb"
      and lb_sgn:"xlb. pset ps. sgn (poly p x) = sgn_neg_inf p"
      and "lb<b"
    using root_list_lb[OF no_0_in_smods,of p "pderiv p * q",folded ps_def] 
    by auto
  have "taq {x. poly p x=0  x<b} q = taq {x. poly p x=0  lb<x  x<b} q"
    unfolding taq_def by (rule sum.cong,insert lb pset 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 lb0" using lb pset ps by auto
  ultimately show ?thesis using sturm_tarski_interval[OF lb<b _ 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 "pssmods p (pderiv p * q)"
  have "pset ps" using ps_def p0 by auto
  obtain lb where lb:"pset ps. x. poly p x=0  x>lb"
      and lb_sgn:"xlb. pset 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:"pset ps. x. poly p x=0  x<ub"
      and ub_sgn:"xub. pset 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<x  x<ub} q"
    unfolding taq_def by (rule sum.cong,insert lb ub pset 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 lb0" and "poly p ub0" using lb ub pset ps by auto
  moreover have "lb<ub" using lb<0 0<ub 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