[STATEMENT]
lemma no_proots_line_code[code]: "no_proots_line p st tt = (if poly p st \<noteq>0 \<and> poly p tt \<noteq> 0 then
                (let pc = pcompose p [:st, tt - st:];
                     pR = map_poly Re pc;
                     pI = map_poly Im pc;
                     g  = gcd pR pI
                 in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False) else False)"
            (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
proof (cases "poly p st \<noteq>0 \<and> poly p tt \<noteq> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
 2. \<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0) \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0)

goal (2 subgoals):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
 2. \<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0) \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0)

goal (1 subgoal):
 1. no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
unfolding no_proots_line_def
[PROOF STATE]
proof (prove)
using this:
\<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0)

goal (1 subgoal):
 1. (proots_within p (closed_segment st tt) = {}) = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0
[PROOF STEP]
have "poly p st \<noteq> 0" "poly p tt \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. poly p st \<noteq> 0 &&& poly p tt \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly p st \<noteq> 0
poly p tt \<noteq> 0

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
define pc pR pI g where
      "pc = pcompose p [:st, tt-st:]" and
      "pR = map_poly Re pc" and
      "pI = map_poly Im pc" and
      "g  = gcd pR pI"
[PROOF STATE]
proof (state)
this:
pc = p \<circ>\<^sub>p [:st, tt - st:]
pR = map_poly Re pc
pI = map_poly Im pc
g = gcd pR pI

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
have poly_iff:"poly g t=0 \<longleftrightarrow> poly pc t =0" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
have "poly g t = 0 \<longleftrightarrow> poly pR t =0 \<and> poly pI t =0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly g t = 0) = (poly pR t = 0 \<and> poly pI t = 0)
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly (gcd pR pI) t = 0) = (poly pR t = 0 \<and> poly pI t = 0)
[PROOF STEP]
using poly_gcd_0_iff
[PROOF STATE]
proof (prove)
using this:
(poly (gcd ?p ?q) ?x = (0::?'a)) = (poly ?p ?x = (0::?'a) \<and> poly ?q ?x = (0::?'a))

goal (1 subgoal):
 1. (poly (gcd pR pI) t = 0) = (poly pR t = 0 \<and> poly pI t = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(poly g t = 0) = (poly pR t = 0 \<and> poly pI t = 0)

goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(poly g t = 0) = (poly pR t = 0 \<and> poly pI t = 0)

goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
have "... \<longleftrightarrow> poly pc t =0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly pR t = 0 \<and> poly pI t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (poly pR t = 0 \<and> poly pI t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
have "cpoly_of pR pI = pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cpoly_of pR pI = pc
[PROOF STEP]
unfolding pc_def pR_def pI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cpoly_of (map_poly Re (p \<circ>\<^sub>p [:st, tt - st:])) (map_poly Im (p \<circ>\<^sub>p [:st, tt - st:])) = p \<circ>\<^sub>p [:st, tt - st:]
[PROOF STEP]
using cpoly_of_decompose
[PROOF STATE]
proof (prove)
using this:
?p = cpoly_of (map_poly Re ?p) (map_poly Im ?p)

goal (1 subgoal):
 1. cpoly_of (map_poly Re (p \<circ>\<^sub>p [:st, tt - st:])) (map_poly Im (p \<circ>\<^sub>p [:st, tt - st:])) = p \<circ>\<^sub>p [:st, tt - st:]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cpoly_of pR pI = pc

goal (1 subgoal):
 1. (poly pR t = 0 \<and> poly pI t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cpoly_of pR pI = pc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cpoly_of pR pI = pc

goal (1 subgoal):
 1. (poly pR t = 0 \<and> poly pI t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
using poly_cpoly_of_real_iff
[PROOF STATE]
proof (prove)
using this:
cpoly_of pR pI = pc
(poly (cpoly_of ?pR ?pI) (complex_of_real ?t) = 0) = (poly ?pR ?t = 0 \<and> poly ?pI ?t = 0)

goal (1 subgoal):
 1. (poly pR t = 0 \<and> poly pI t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(poly pR t = 0 \<and> poly pI t = 0) = (poly pc (complex_of_real t) = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(poly pR t = 0 \<and> poly pI t = 0) = (poly pc (complex_of_real t) = 0)

goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(poly g t = 0) = (poly pc (complex_of_real t) = 0)

goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(poly g t = 0) = (poly pc (complex_of_real t) = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(poly g ?t = 0) = (poly pc (complex_of_real ?t) = 0)

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
have "?R = (changes_itv_smods 0 1 g (pderiv g) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False) = (changes_itv_smods 0 1 g (pderiv g) = 0)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False) = (changes_itv_smods 0 1 g (pderiv g) = 0)
[PROOF STEP]
unfolding pc_def g_def pI_def pR_def
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False) = (changes_itv_smods 0 1 (gcd (map_poly Re (p \<circ>\<^sub>p [:st, tt - st:])) (map_poly Im (p \<circ>\<^sub>p [:st, tt - st:]))) (pderiv (gcd (map_poly Re (p \<circ>\<^sub>p [:st, tt - st:])) (map_poly Im (p \<circ>\<^sub>p [:st, tt - st:])))) = 0)
[PROOF STEP]
by (auto simp add:Let_def)
[PROOF STATE]
proof (state)
this:
(if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False) = (changes_itv_smods 0 1 g (pderiv g) = 0)

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False) = (changes_itv_smods 0 1 g (pderiv g) = 0)

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
have "... = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)
[PROOF STEP]
have "poly g 0 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly g 0 \<noteq> 0
[PROOF STEP]
using poly_iff[of 0] True
[PROOF STATE]
proof (prove)
using this:
(poly g 0 = 0) = (poly pc (complex_of_real 0) = 0)
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. poly g 0 \<noteq> 0
[PROOF STEP]
unfolding pc_def
[PROOF STATE]
proof (prove)
using this:
(poly g 0 = 0) = (poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real 0) = 0)
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. poly g 0 \<noteq> 0
[PROOF STEP]
by (auto simp add:poly_pcompose)
[PROOF STATE]
proof (state)
this:
poly g 0 \<noteq> 0

goal (1 subgoal):
 1. (changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poly g 0 \<noteq> 0

goal (1 subgoal):
 1. (changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)
[PROOF STEP]
have "poly g 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly g 1 \<noteq> 0
[PROOF STEP]
using poly_iff[of 1] True
[PROOF STATE]
proof (prove)
using this:
(poly g 1 = 0) = (poly pc (complex_of_real 1) = 0)
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. poly g 1 \<noteq> 0
[PROOF STEP]
unfolding pc_def
[PROOF STATE]
proof (prove)
using this:
(poly g 1 = 0) = (poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real 1) = 0)
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. poly g 1 \<noteq> 0
[PROOF STEP]
by (auto simp add:poly_pcompose)
[PROOF STATE]
proof (state)
this:
poly g 1 \<noteq> 0

goal (1 subgoal):
 1. (changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
poly g 0 \<noteq> 0
poly g 1 \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly g 0 \<noteq> 0
poly g 1 \<noteq> 0

goal (1 subgoal):
 1. (changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)
[PROOF STEP]
using sturm_interval[of 0 1 g]
[PROOF STATE]
proof (prove)
using this:
poly g 0 \<noteq> 0
poly g 1 \<noteq> 0
\<lbrakk>0 < 1; poly g 0 \<noteq> 0; poly g 1 \<noteq> 0\<rbrakk> \<Longrightarrow> int (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1}) = changes_itv_smods 0 1 g (pderiv g)

goal (1 subgoal):
 1. (changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(changes_itv_smods 0 1 g (pderiv g) = 0) = (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0)

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
have "... = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})
[PROOF STEP]
have "g\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<noteq> 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> g \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> g \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<not> g \<noteq> 0

goal (1 subgoal):
 1. \<not> g \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> g \<noteq> 0
[PROOF STEP]
have "poly pc 0 =0"
[PROOF STATE]
proof (prove)
using this:
\<not> g \<noteq> 0

goal (1 subgoal):
 1. poly pc 0 = 0
[PROOF STEP]
using poly_iff[of 0]
[PROOF STATE]
proof (prove)
using this:
\<not> g \<noteq> 0
(poly g 0 = 0) = (poly pc (complex_of_real 0) = 0)

goal (1 subgoal):
 1. poly pc 0 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly pc 0 = 0

goal (1 subgoal):
 1. \<not> g \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly pc 0 = 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
poly pc 0 = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
poly pc 0 = 0
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding pc_def
[PROOF STATE]
proof (prove)
using this:
poly (p \<circ>\<^sub>p [:st, tt - st:]) 0 = 0
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp add:poly_pcompose)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<noteq> 0

goal (1 subgoal):
 1. (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})
[PROOF STEP]
from poly_roots_finite[OF this]
[PROOF STATE]
proof (chain)
picking this:
finite {x. poly g x = 0}
[PROOF STEP]
have "finite {x. poly g x = 0 \<and> 0 < x \<and> x < 1}"
[PROOF STATE]
proof (prove)
using this:
finite {x. poly g x = 0}

goal (1 subgoal):
 1. finite {x. poly g x = 0 \<and> 0 < x \<and> x < 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {x. poly g x = 0 \<and> 0 < x \<and> x < 1}

goal (1 subgoal):
 1. (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {x. poly g x = 0 \<and> 0 < x \<and> x < 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {x. poly g x = 0 \<and> 0 < x \<and> x < 1}

goal (1 subgoal):
 1. (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})
[PROOF STEP]
using card_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
finite {x. poly g x = 0 \<and> 0 < x \<and> x < 1}
(card ?A = 0) = (?A = {} \<or> infinite ?A)

goal (1 subgoal):
 1. (card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(card {x. poly g x = 0 \<and> 0 < x \<and> x < 1} = 0) = ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {})

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
have "... = ?L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt
[PROOF STEP]
have "(\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) \<longleftrightarrow>
          (\<exists>t::real. poly pc (of_real t) = 0 \<and> 0 < t \<and> t < 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1)
[PROOF STEP]
using poly_iff
[PROOF STATE]
proof (prove)
using this:
(poly g ?t = 0) = (poly pc (complex_of_real ?t) = 0)

goal (1 subgoal):
 1. (\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1)

goal (1 subgoal):
 1. ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1)

goal (1 subgoal):
 1. ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt
[PROOF STEP]
have "... \<longleftrightarrow> (\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1 \<Longrightarrow> \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
 2. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
assume "\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1"
[PROOF STATE]
proof (state)
this:
\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1

goal (2 subgoals):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1 \<Longrightarrow> \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
 2. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
obtain t where *:"poly pc (of_real t) = 0" and "0 < t" "t < 1"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>poly pc (complex_of_real t) = 0; 0 < t; t < 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly pc (complex_of_real t) = 0
0 < t
t < 1

goal (2 subgoals):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1 \<Longrightarrow> \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
 2. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
define x where "x=poly [:st, tt - st:] t"
[PROOF STATE]
proof (state)
this:
x = poly [:st, tt - st:] (complex_of_real t)

goal (2 subgoals):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1 \<Longrightarrow> \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
 2. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
have "x \<in> closed_segment st tt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> closed_segment st tt
[PROOF STEP]
using \<open>0<t\<close> \<open>t<1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < t
t < 1

goal (1 subgoal):
 1. x \<in> closed_segment st tt
[PROOF STEP]
unfolding x_def in_segment
[PROOF STATE]
proof (prove)
using this:
0 < t
t < 1

goal (1 subgoal):
 1. \<exists>u\<ge>0. u \<le> 1 \<and> poly [:st, tt - st:] (complex_of_real t) = (1 - u) *\<^sub>R st + u *\<^sub>R tt
[PROOF STEP]
by (intro exI[where x=t],auto simp add: algebra_simps scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment st tt

goal (2 subgoals):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1 \<Longrightarrow> \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
 2. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment st tt

goal (2 subgoals):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1 \<Longrightarrow> \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
 2. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
have "poly p x=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly p x = 0
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
poly pc (complex_of_real t) = 0

goal (1 subgoal):
 1. poly p x = 0
[PROOF STEP]
unfolding pc_def x_def
[PROOF STATE]
proof (prove)
using this:
poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real t) = 0

goal (1 subgoal):
 1. poly p (poly [:st, tt - st:] (complex_of_real t)) = 0
[PROOF STEP]
by (auto simp add:poly_pcompose)
[PROOF STATE]
proof (state)
this:
poly p x = 0

goal (2 subgoals):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1 \<Longrightarrow> \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
 2. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> closed_segment st tt
poly p x = 0
[PROOF STEP]
show "\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment st tt
poly p x = 0

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
assume "\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0"
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0
[PROOF STEP]
obtain x where "x \<in> closed_segment st tt" "poly p x = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> closed_segment st tt; poly p x = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment st tt
poly p x = 0

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> closed_segment st tt
poly p x = 0
[PROOF STEP]
obtain t::real where *:"x = (1 - t) *\<^sub>R st + t *\<^sub>R tt" and "0\<le>t" "t\<le>1"
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment st tt
poly p x = 0

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>x = (1 - t) *\<^sub>R st + t *\<^sub>R tt; 0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding in_segment
[PROOF STATE]
proof (prove)
using this:
\<exists>u\<ge>0. u \<le> 1 \<and> x = (1 - u) *\<^sub>R st + u *\<^sub>R tt
poly p x = 0

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>x = (1 - t) *\<^sub>R st + t *\<^sub>R tt; 0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (1 - t) *\<^sub>R st + t *\<^sub>R tt
0 \<le> t
t \<le> 1

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (1 - t) *\<^sub>R st + t *\<^sub>R tt
0 \<le> t
t \<le> 1
[PROOF STEP]
have "x=poly [:st, tt - st:] t"
[PROOF STATE]
proof (prove)
using this:
x = (1 - t) *\<^sub>R st + t *\<^sub>R tt
0 \<le> t
t \<le> 1

goal (1 subgoal):
 1. x = poly [:st, tt - st:] (complex_of_real t)
[PROOF STEP]
by (auto simp add: algebra_simps scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
x = poly [:st, tt - st:] (complex_of_real t)

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = poly [:st, tt - st:] (complex_of_real t)
[PROOF STEP]
have "poly pc (complex_of_real t) = 0"
[PROOF STATE]
proof (prove)
using this:
x = poly [:st, tt - st:] (complex_of_real t)

goal (1 subgoal):
 1. poly pc (complex_of_real t) = 0
[PROOF STEP]
using \<open>poly p x=0\<close>
[PROOF STATE]
proof (prove)
using this:
x = poly [:st, tt - st:] (complex_of_real t)
poly p x = 0

goal (1 subgoal):
 1. poly pc (complex_of_real t) = 0
[PROOF STEP]
unfolding pc_def
[PROOF STATE]
proof (prove)
using this:
x = poly [:st, tt - st:] (complex_of_real t)
poly p x = 0

goal (1 subgoal):
 1. poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real t) = 0
[PROOF STEP]
by (auto simp add:poly_pcompose)
[PROOF STATE]
proof (state)
this:
poly pc (complex_of_real t) = 0

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poly pc (complex_of_real t) = 0

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
have "t\<noteq>0" "t\<noteq>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> 0 &&& t \<noteq> 1
[PROOF STEP]
using True *  \<open>poly p x=0\<close>
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0
x = (1 - t) *\<^sub>R st + t *\<^sub>R tt
poly p x = 0

goal (1 subgoal):
 1. t \<noteq> 0 &&& t \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<noteq> 0
t \<noteq> 1

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> 0
t \<noteq> 1
[PROOF STEP]
have "0<t" "t<1"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> 0
t \<noteq> 1

goal (1 subgoal):
 1. 0 < t &&& t < 1
[PROOF STEP]
using \<open>0\<le>t\<close> \<open>t\<le>1\<close>
[PROOF STATE]
proof (prove)
using this:
t \<noteq> 0
t \<noteq> 1
0 \<le> t
t \<le> 1

goal (1 subgoal):
 1. 0 < t &&& t < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < t
t < 1

goal (1 subgoal):
 1. \<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0 \<Longrightarrow> \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
poly pc (complex_of_real t) = 0
0 < t
t < 1
[PROOF STEP]
show "\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1"
[PROOF STATE]
proof (prove)
using this:
poly pc (complex_of_real t) = 0
0 < t
t < 1

goal (1 subgoal):
 1. \<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0)

goal (1 subgoal):
 1. ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0)

goal (1 subgoal):
 1. ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt
[PROOF STEP]
unfolding no_proots_line_def proots_within_def
[PROOF STATE]
proof (prove)
using this:
(\<exists>t. poly g (of_real t) = 0 \<and> 0 < t \<and> t < 1) = (\<exists>x. x \<in> closed_segment st tt \<and> poly p x = 0)

goal (1 subgoal):
 1. ({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = ({x \<in> closed_segment st tt. poly p x = 0} = {})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
({x. poly g (of_real x) = 0 \<and> 0 < x \<and> x < 1} = {}) = no_proots_line p st tt

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<Longrightarrow> no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False) = no_proots_line p st tt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False) = no_proots_line p st tt

goal (1 subgoal):
 1. no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
no_proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in if changes_itv_smods 0 1 g (pderiv g) = 0 then True else False else False)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_line_commute:
  "proots_line p st tt = proots_line p tt st"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_line p st tt = proots_line p tt st
[PROOF STEP]
unfolding proots_line_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (open_segment st tt) = proots_count p (open_segment tt st)
[PROOF STEP]
by (simp add: open_segment_commute)


[STATEMENT]
lemma proots_line_smods:
  assumes "poly p st \<noteq>0" "poly p tt \<noteq> 0" "st\<noteq>tt"
  shows "proots_line p st tt =
                        (let pc = pcompose p [:st, tt - st:];
                             pR = map_poly Re pc;
                             pI = map_poly Im pc;
                             g  = gcd pR pI
                         in nat (changes_itv_smods_ext 0 1 g (pderiv g)))"
  (is "_=?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have "p\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
using assms(2) poly_0
[PROOF STATE]
proof (prove)
using this:
poly p tt \<noteq> 0
poly 0 ?x = (0::?'a)

goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
define pc pR pI g where
      "pc = pcompose p [:st, tt-st:]" and
      "pR = map_poly Re pc" and
      "pI = map_poly Im pc" and
      "g  = gcd pR pI"
[PROOF STATE]
proof (state)
this:
pc = p \<circ>\<^sub>p [:st, tt - st:]
pR = map_poly Re pc
pI = map_poly Im pc
g = gcd pR pI

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have [simp]: "g\<noteq>0" "pc\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<noteq> 0 &&& pc \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g \<noteq> 0
 2. pc \<noteq> 0
[PROOF STEP]
show "pc\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc \<noteq> 0
[PROOF STEP]
by (metis assms(1) coeff_pCons_0 pCons_0_0 pc_def pcompose_coeff_0)
[PROOF STATE]
proof (state)
this:
pc \<noteq> 0

goal (1 subgoal):
 1. g \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc \<noteq> 0
[PROOF STEP]
have "pR\<noteq>0 \<or> pI\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
pc \<noteq> 0

goal (1 subgoal):
 1. pR \<noteq> 0 \<or> pI \<noteq> 0
[PROOF STEP]
unfolding pR_def pI_def
[PROOF STATE]
proof (prove)
using this:
pc \<noteq> 0

goal (1 subgoal):
 1. map_poly Re pc \<noteq> 0 \<or> map_poly Im pc \<noteq> 0
[PROOF STEP]
by (metis cpoly_of_decompose map_poly_0)
[PROOF STATE]
proof (state)
this:
pR \<noteq> 0 \<or> pI \<noteq> 0

goal (1 subgoal):
 1. g \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pR \<noteq> 0 \<or> pI \<noteq> 0
[PROOF STEP]
show "g\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
pR \<noteq> 0 \<or> pI \<noteq> 0

goal (1 subgoal):
 1. g \<noteq> 0
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
pR \<noteq> 0 \<or> pI \<noteq> 0

goal (1 subgoal):
 1. gcd pR pI \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<noteq> 0
pc \<noteq> 0

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have order_eq:"order t g = order t pc" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order t g = order (complex_of_real t) pc
[PROOF STEP]
apply (subst order_cpoly_gcd_eq[of pR pI,folded g_def,symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pR \<noteq> 0 \<or> pI \<noteq> 0
 2. order (complex_of_real t) (cpoly_of pR pI) = order (complex_of_real t) pc
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pR \<noteq> 0 \<or> pI \<noteq> 0
[PROOF STEP]
using \<open>g\<noteq>0\<close>
[PROOF STATE]
proof (prove)
using this:
g \<noteq> 0

goal (1 subgoal):
 1. pR \<noteq> 0 \<or> pI \<noteq> 0
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
gcd pR pI \<noteq> 0

goal (1 subgoal):
 1. pR \<noteq> 0 \<or> pI \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (complex_of_real t) (cpoly_of pR pI) = order (complex_of_real t) pc
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (complex_of_real t) (cpoly_of pR pI) = order (complex_of_real t) pc
[PROOF STEP]
unfolding pR_def pI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (complex_of_real t) (cpoly_of (map_poly Re pc) (map_poly Im pc)) = order (complex_of_real t) pc
[PROOF STEP]
by (simp add:cpoly_of_decompose[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
order ?t g = order (complex_of_real ?t) pc

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have poly_iff:"poly g t=0 \<longleftrightarrow> poly pc t =0" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
using order_eq
[PROOF STATE]
proof (prove)
using this:
order ?t g = order (complex_of_real ?t) pc

goal (1 subgoal):
 1. (poly g t = 0) = (poly pc (complex_of_real t) = 0)
[PROOF STEP]
by (simp add: order_root)
[PROOF STATE]
proof (state)
this:
(poly g ?t = 0) = (poly pc (complex_of_real ?t) = 0)

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have "poly g 0 \<noteq> 0" "poly g 1 \<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly g 0 \<noteq> 0 &&& poly g 1 \<noteq> 0
[PROOF STEP]
unfolding poly_iff pc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real 0) \<noteq> 0 &&& poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real 1) \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0
poly p tt \<noteq> 0
st \<noteq> tt

goal (1 subgoal):
 1. poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real 0) \<noteq> 0 &&& poly (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real 1) \<noteq> 0
[PROOF STEP]
by (simp_all add:poly_pcompose)
[PROOF STATE]
proof (state)
this:
poly g 0 \<noteq> 0
poly g 1 \<noteq> 0

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have "?R = changes_itv_smods_ext 0 1 g (pderiv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g))) = changes_itv_smods_ext 0 1 g (pderiv g)
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (nat (changes_itv_smods_ext 0 1 (gcd (map_poly Re (p \<circ>\<^sub>p [:st, tt - st:])) (map_poly Im (p \<circ>\<^sub>p [:st, tt - st:]))) (pderiv (gcd (map_poly Re (p \<circ>\<^sub>p [:st, tt - st:])) (map_poly Im (p \<circ>\<^sub>p [:st, tt - st:])))))) = changes_itv_smods_ext 0 1 g (pderiv g)
[PROOF STEP]
apply (fold pc_def g_def pI_def pR_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (nat (changes_itv_smods_ext 0 1 g (pderiv g))) = changes_itv_smods_ext 0 1 g (pderiv g)
[PROOF STEP]
using assms changes_itv_smods_ext_geq_0[OF _ \<open>poly g  0\<noteq>0\<close> \<open>poly g 1\<noteq>0\<close>]
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0
poly p tt \<noteq> 0
st \<noteq> tt
0 < 1 \<Longrightarrow> 0 \<le> changes_itv_smods_ext 0 1 g (pderiv g)

goal (1 subgoal):
 1. int (nat (changes_itv_smods_ext 0 1 g (pderiv g))) = changes_itv_smods_ext 0 1 g (pderiv g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g))) = changes_itv_smods_ext 0 1 g (pderiv g)

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g))) = changes_itv_smods_ext 0 1 g (pderiv g)

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have "... = int (proots_count g {x. 0 < x \<and> x < 1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. changes_itv_smods_ext 0 1 g (pderiv g) = int (proots_count g {x. 0 < x \<and> x < 1})
[PROOF STEP]
apply (rule sturm_ext_interval[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 < 1
 2. poly g 0 \<noteq> 0
 3. poly g 1 \<noteq> 0
[PROOF STEP]
by simp fact+
[PROOF STATE]
proof (state)
this:
changes_itv_smods_ext 0 1 g (pderiv g) = int (proots_count g {x. 0 < x \<and> x < 1})

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
changes_itv_smods_ext 0 1 g (pderiv g) = int (proots_count g {x. 0 < x \<and> x < 1})

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have "... =  int (proots_count p (open_segment st tt))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
define f where "f = (\<lambda>x. poly [:st, tt - st:] (complex_of_real x))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x. poly [:st, tt - st:] (complex_of_real x))

goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
have "x\<in>f ` {x. 0 < x \<and> x < 1}"  if "x\<in>open_segment st tt" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> f ` {x. 0 < x \<and> x < 1}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> f ` {x. 0 < x \<and> x < 1}
[PROOF STEP]
obtain u where u:"u>0" "u < 1" "x = (1 - u) *\<^sub>R st + u *\<^sub>R tt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>0 < u; u < 1; x = (1 - u) *\<^sub>R st + u *\<^sub>R tt\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x\<in>open_segment st tt\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> open_segment st tt

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>0 < u; u < 1; x = (1 - u) *\<^sub>R st + u *\<^sub>R tt\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding in_segment
[PROOF STATE]
proof (prove)
using this:
st \<noteq> tt \<and> (\<exists>u>0. u < 1 \<and> x = (1 - u) *\<^sub>R st + u *\<^sub>R tt)

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>0 < u; u < 1; x = (1 - u) *\<^sub>R st + u *\<^sub>R tt\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < u
u < 1
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (1 subgoal):
 1. x \<in> f ` {x. 0 < x \<and> x < 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> f ` {x. 0 < x \<and> x < 1}
[PROOF STEP]
apply (rule rev_image_eqI[where x=u])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. u \<in> {x. 0 < x \<and> x < 1}
 2. x = f u
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
0 < u
u < 1
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (2 subgoals):
 1. u \<in> {x. 0 < x \<and> x < 1}
 2. x = f u
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
0 < u
u < 1
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (2 subgoals):
 1. u \<in> {x. 0 < x \<and> x < 1}
 2. x = poly [:st, tt - st:] (complex_of_real u)
[PROOF STEP]
by (auto simp:algebra_simps scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
x \<in> f ` {x. 0 < x \<and> x < 1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> open_segment st tt \<Longrightarrow> ?x \<in> f ` {x. 0 < x \<and> x < 1}

goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> open_segment st tt \<Longrightarrow> ?x \<in> f ` {x. 0 < x \<and> x < 1}

goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
have "x\<in>open_segment st tt" if "x\<in>f ` {x. 0 < x \<and> x < 1}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> open_segment st tt
[PROOF STEP]
using that \<open>st\<noteq>tt\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> f ` {x. 0 < x \<and> x < 1}
st \<noteq> tt

goal (1 subgoal):
 1. x \<in> open_segment st tt
[PROOF STEP]
unfolding in_segment f_def
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` {x. 0 < x \<and> x < 1}
st \<noteq> tt

goal (1 subgoal):
 1. st \<noteq> tt \<and> (\<exists>u>0. u < 1 \<and> x = (1 - u) *\<^sub>R st + u *\<^sub>R tt)
[PROOF STEP]
by (auto simp:scaleR_conv_of_real algebra_simps)
[PROOF STATE]
proof (state)
this:
?x \<in> f ` {x. 0 < x \<and> x < 1} \<Longrightarrow> ?x \<in> open_segment st tt

goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x \<in> open_segment st tt \<Longrightarrow> ?x \<in> f ` {x. 0 < x \<and> x < 1}
?x \<in> f ` {x. 0 < x \<and> x < 1} \<Longrightarrow> ?x \<in> open_segment st tt
[PROOF STEP]
have "open_segment st tt = f ` {x. 0 < x \<and> x < 1}"
[PROOF STATE]
proof (prove)
using this:
?x \<in> open_segment st tt \<Longrightarrow> ?x \<in> f ` {x. 0 < x \<and> x < 1}
?x \<in> f ` {x. 0 < x \<and> x < 1} \<Longrightarrow> ?x \<in> open_segment st tt

goal (1 subgoal):
 1. open_segment st tt = f ` {x. 0 < x \<and> x < 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open_segment st tt = f ` {x. 0 < x \<and> x < 1}

goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open_segment st tt = f ` {x. 0 < x \<and> x < 1}
[PROOF STEP]
have "proots_count p (open_segment st tt)
              = proots_count g {x. 0 < x \<and> x < 1}"
[PROOF STATE]
proof (prove)
using this:
open_segment st tt = f ` {x. 0 < x \<and> x < 1}

goal (1 subgoal):
 1. proots_count p (open_segment st tt) = proots_count g {x. 0 < x \<and> x < 1}
[PROOF STEP]
using proots_count_gcd_eq[OF \<open>st\<noteq>tt\<close> \<open>p\<noteq>0\<close>,
              folded pc_def pR_def pI_def g_def]
[PROOF STATE]
proof (prove)
using this:
open_segment st tt = f ` {x. 0 < x \<and> x < 1}
?s1.0 = (\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` ?s2.0 \<Longrightarrow> proots_count p ?s1.0 = proots_count g ?s2.0

goal (1 subgoal):
 1. proots_count p (open_segment st tt) = proots_count g {x. 0 < x \<and> x < 1}
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
open_segment st tt = (\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` {x. 0 < x \<and> x < 1}
?s1.0 = (\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` ?s2.0 \<Longrightarrow> proots_count p ?s1.0 = proots_count g ?s2.0

goal (1 subgoal):
 1. proots_count p (open_segment st tt) = proots_count g {x. 0 < x \<and> x < 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count p (open_segment st tt) = proots_count g {x. 0 < x \<and> x < 1}

goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proots_count p (open_segment st tt) = proots_count g {x. 0 < x \<and> x < 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proots_count p (open_segment st tt) = proots_count g {x. 0 < x \<and> x < 1}

goal (1 subgoal):
 1. int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (proots_count g {x. 0 < x \<and> x < 1}) = int (proots_count p (open_segment st tt))

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
have "... =proots_line p st tt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (proots_count p (open_segment st tt)) = int (proots_line p st tt)
[PROOF STEP]
unfolding proots_line_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (proots_count p (open_segment st tt)) = int (proots_count p (open_segment st tt))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int (proots_count p (open_segment st tt)) = int (proots_line p st tt)

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
int (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g))) = int (proots_line p st tt)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
int (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g))) = int (proots_line p st tt)

goal (1 subgoal):
 1. proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proots_line p st tt = (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_line_code[code]:
    "proots_line p st tt =
        (if poly p st \<noteq>0 \<and> poly p tt \<noteq> 0 then
            (if st\<noteq>tt then
                (let pc = pcompose p [:st, tt - st:];
                     pR = map_poly Re pc;
                     pI = map_poly Im pc;
                     g  = gcd pR pI
                 in nat (changes_itv_smods_ext 0 1 g (pderiv g)))
            else 0)
   else  Code.abort (STR ''prootsline does not handle vanishing endpoints for now'')
                      (\<lambda>_. proots_line p st tt))" (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
proof (cases "poly p st \<noteq>0 \<and> poly p tt \<noteq> 0 \<and> st\<noteq>tt")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
 2. \<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt) \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt)

goal (2 subgoals):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
 2. \<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt) \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt)

goal (2 subgoals):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
 2. \<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt) \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
have ?thesis if "st=tt" "p\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
st = tt
p \<noteq> 0

goal (1 subgoal):
 1. proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
unfolding proots_line_def
[PROOF STATE]
proof (prove)
using this:
st = tt
p \<noteq> 0

goal (1 subgoal):
 1. proots_count p (open_segment st tt) = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_count p (open_segment st tt)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>st = tt; p \<noteq> 0\<rbrakk> \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))

goal (2 subgoals):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
 2. \<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt) \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt)
\<lbrakk>st = tt; p \<noteq> 0\<rbrakk> \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt)
\<lbrakk>st = tt; p \<noteq> 0\<rbrakk> \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))

goal (1 subgoal):
 1. proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt

goal (1 subgoal):
 1. poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt \<Longrightarrow> proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt

goal (1 subgoal):
 1. proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
using proots_line_smods
[PROOF STATE]
proof (prove)
using this:
poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 \<and> st \<noteq> tt
\<lbrakk>poly ?p ?st \<noteq> 0; poly ?p ?tt \<noteq> 0; ?st \<noteq> ?tt\<rbrakk> \<Longrightarrow> proots_line ?p ?st ?tt = (let pc = ?p \<circ>\<^sub>p [:?st, ?tt - ?st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)))

goal (1 subgoal):
 1. proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_line p st tt = (if poly p st \<noteq> 0 \<and> poly p tt \<noteq> 0 then if st \<noteq> tt then let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in nat (changes_itv_smods_ext 0 1 g (pderiv g)) else 0 else Code.abort STR ''prootsline does not handle vanishing endpoints for now'' (\<lambda>_. proots_line p st tt))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iarray_cong: "n = m \<Longrightarrow> (\<And> i. i < m \<Longrightarrow> f i = g i) \<Longrightarrow> IArray.of_fun f n = IArray.of_fun g m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = m; \<And>i. i < m \<Longrightarrow> f i = g i\<rbrakk> \<Longrightarrow> IArray.of_fun f n = IArray.of_fun g m
[PROOF STEP]
by auto


[STATEMENT]
lemma iarray_cong': "(\<And> i. i < n \<Longrightarrow> f i = g i) \<Longrightarrow> IArray.of_fun f n = IArray.of_fun g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i < n \<Longrightarrow> f i = g i) \<Longrightarrow> IArray.of_fun f n = IArray.of_fun g n
[PROOF STEP]
by (rule iarray_cong, auto)


[STATEMENT]
lemma iarray_update_length[simp]: "IArray.length (iarray_update a i x) = IArray.length a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (iarray_update a i x) = IArray.length a
[PROOF STEP]
unfolding iarray_update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (IArray.of_fun (\<lambda>j. if j = i then x else a !! j) (IArray.length a)) = IArray.length a
[PROOF STEP]
by simp


[STATEMENT]
lemma iarray_length_of_fun[simp]: "IArray.length (IArray.of_fun f n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (IArray.of_fun f n) = n
[PROOF STEP]
by simp


[STATEMENT]
lemma iarray_update_of_fun[simp]: "iarray_update (IArray.of_fun f n) i x = IArray.of_fun (f (i := x)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iarray_update (IArray.of_fun f n) i x = IArray.of_fun (f(i := x)) n
[PROOF STEP]
unfolding iarray_update_def iarray_length_of_fun
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.of_fun (\<lambda>j. if j = i then x else IArray.of_fun f n !! j) n = IArray.of_fun (f(i := x)) n
[PROOF STEP]
by (rule iarray_cong, auto)


[STATEMENT]
lemma iarray_append_code[code]: "iarray_append xs x = IArray (IArray.list_of xs @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iarray_append xs x = IArray (IArray.list_of xs @ [x])
[PROOF STEP]
by (cases xs, auto)


[STATEMENT]
lemma iarray_append_of_fun[simp]: "iarray_append (IArray.of_fun f n) x = IArray.of_fun (f (n := x)) (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iarray_append (IArray.of_fun f n) x = IArray.of_fun (f(n := x)) (Suc n)
[PROOF STEP]
by auto


[STATEMENT]
lemma iarray_of_fun_sub[simp]: "i < n \<Longrightarrow> IArray.of_fun f n !! i = f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> IArray.of_fun f n !! i = f i
[PROOF STEP]
by auto


[STATEMENT]
lemma IArray_of_fun_conv: "IArray xs = IArray.of_fun (\<lambda> i. xs ! i) (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray xs = IArray.of_fun ((!) xs) (length xs)
[PROOF STEP]
by (auto intro!: nth_equalityI)