[STATEMENT]
lemma proots_sphere_axis_eq:
  defines "q1\<equiv>[:\<i>,-1:]" and "q2\<equiv>[:\<i>,1:]"
  assumes "p\<noteq>0"
  shows "proots_count p (sphere 0 1 - {- 1}) = proots_count (fcompose p q1 q2) {x. 0 = Im x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (sphere 0 1 - {- 1}) = proots_count (fcompose p q1 q2) {x. 0 = Im x}
[PROOF STEP]
unfolding q1_def q2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (sphere 0 1 - {- 1}) = proots_count (fcompose p [:\<i>, - 1:] [:\<i>, 1:]) {x. 0 = Im x}
[PROOF STEP]
proof (rule proots_fcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 = Im x} (sphere 0 1 - {- 1})
 2. \<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0
 3. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 4. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 5. infinite UNIV
[PROOF STEP]
show "\<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0
[PROOF STEP]
by (simp add: Complex_eq_0 plus_complex.code)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0

goal (4 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 = Im x} (sphere 0 1 - {- 1})
 2. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 3. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 4. infinite UNIV
[PROOF STEP]
show "infinite (UNIV::complex set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
by (simp add: infinite_UNIV_char_0)
[PROOF STATE]
proof (state)
this:
infinite UNIV

goal (3 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 = Im x} (sphere 0 1 - {- 1})
 2. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 3. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
[PROOF STEP]
qed (use bij_betw_axis_sphere in auto)


[STATEMENT]
lemma proots_card_ball_plane_eq:
  defines "q1\<equiv>[:\<i>,-1:]" and "q2\<equiv>[:\<i>,1:]"
  assumes "p\<noteq>0"
  shows "card (proots_within p (ball 0 1)) = card (proots_within (fcompose p q1 q2) {x. 0 < Im x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (ball 0 1)) = card (proots_within (fcompose p q1 q2) {x. 0 < Im x})
[PROOF STEP]
unfolding q1_def q2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (ball 0 1)) = card (proots_within (fcompose p [:\<i>, - 1:] [:\<i>, 1:]) {x. 0 < Im x})
[PROOF STEP]
proof (rule proots_card_fcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 < Im x} (ball 0 1)
 2. \<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0
 3. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 4. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 5. infinite UNIV
[PROOF STEP]
show "\<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. 0 < Im x \<longrightarrow> \<i> + x \<noteq> 0
[PROOF STEP]
by (metis add_less_same_cancel2 imaginary_unit.simps(2) not_one_less_zero
          plus_complex.simps(2) zero_complex.simps(2))
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{x. 0 < Im x}. poly [:\<i>, 1:] x \<noteq> 0

goal (4 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 < Im x} (ball 0 1)
 2. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 3. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 4. infinite UNIV
[PROOF STEP]
qed (use bij_betw_plane_ball infinite_UNIV_char_0 in auto)


[STATEMENT]
lemma proots_card_sphere_axis_eq:
  defines "q1\<equiv>[:\<i>,-1:]" and "q2\<equiv>[:\<i>,1:]"
  assumes "p\<noteq>0"
  shows "card (proots_within p (sphere 0 1 - {- 1}))
            = card (proots_within (fcompose p q1 q2) {x. 0 = Im x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (sphere 0 1 - {- 1})) = card (proots_within (fcompose p q1 q2) {x. 0 = Im x})
[PROOF STEP]
unfolding q1_def q2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (sphere 0 1 - {- 1})) = card (proots_within (fcompose p [:\<i>, - 1:] [:\<i>, 1:]) {x. 0 = Im x})
[PROOF STEP]
proof (rule proots_card_fcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 = Im x} (sphere 0 1 - {- 1})
 2. \<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0
 3. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 4. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 5. infinite UNIV
[PROOF STEP]
show "\<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0
[PROOF STEP]
by (simp add: Complex_eq_0 plus_complex.code)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{x. 0 = Im x}. poly [:\<i>, 1:] x \<noteq> 0

goal (4 subgoals):
 1. bij_betw (\<lambda>x. poly [:\<i>, - 1:] x / poly [:\<i>, 1:] x) {x. 0 = Im x} (sphere 0 1 - {- 1})
 2. max (degree [:\<i>, - 1:]) (degree [:\<i>, 1:]) \<le> 1
 3. \<forall>c. [:\<i>, - 1:] \<noteq> smult c [:\<i>, 1:]
 4. infinite UNIV
[PROOF STEP]
qed (use bij_betw_axis_sphere infinite_UNIV_char_0 in auto)


[STATEMENT]
lemma proots_uball_eq:
  fixes z0::complex and r::real
  defines "q\<equiv>[:z0, of_real r:]"
  assumes "p\<noteq>0" and "r>0"
  shows "proots_count p (ball z0 r) = proots_count (p \<circ>\<^sub>p q) (ball 0 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (ball z0 r) = proots_count (p \<circ>\<^sub>p q) (ball 0 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_count p (ball z0 r) = proots_count (p \<circ>\<^sub>p q) (ball 0 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (ball z0 r) = proots_count (p \<circ>\<^sub>p q) (ball 0 1)
[PROOF STEP]
apply (rule proots_pcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bij_betw (poly q) (ball 0 1) (ball z0 r)
 2. degree q = 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (poly q) (ball 0 1) (ball z0 r)
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (poly [:z0, complex_of_real r:]) (ball 0 1) (ball z0 r)
[PROOF STEP]
using bij_betw_ball_uball[OF \<open>r>0\<close>,of z0]
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>x. complex_of_real r * x + z0) (ball 0 1) (ball z0 r)

goal (1 subgoal):
 1. bij_betw (poly [:z0, complex_of_real r:]) (ball 0 1) (ball z0 r)
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q = 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q = 1
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree [:z0, complex_of_real r:] = 1
[PROOF STEP]
using \<open>r>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. degree [:z0, complex_of_real r:] = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
proots_count p (ball z0 r) = proots_count (p \<circ>\<^sub>p q) (ball 0 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_card_uball_eq:
  fixes z0::complex and r::real
  defines "q\<equiv>[:z0, of_real r:]"
  assumes "r>0"
  shows "card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
have ?thesis
    when "p=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
have "card (ball z0 r) = 0" "card (ball (0::complex) 1) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (ball z0 r) = 0 &&& card (ball 0 1) = 0
[PROOF STEP]
using infinite_ball[OF \<open>r>0\<close>,of z0] infinite_ball[of 1 "0::complex"]
[PROOF STATE]
proof (prove)
using this:
infinite (ball z0 r)
0 < 1 \<Longrightarrow> infinite (ball 0 1)

goal (1 subgoal):
 1. card (ball z0 r) = 0 &&& card (ball 0 1) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (ball z0 r) = 0
card (ball 0 1) = 0

goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (ball z0 r) = 0
card (ball 0 1) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (ball z0 r) = 0
card (ball 0 1) = 0

goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
card (ball z0 r) = 0
card (ball 0 1) = 0
p = 0

goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p = 0 \<Longrightarrow> card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))

goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p = 0 \<Longrightarrow> card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))

goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
have ?thesis
    when "p\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
apply (rule proots_card_pcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bij_betw (poly q) (ball 0 1) (ball z0 r)
 2. degree q = 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (poly q) (ball 0 1) (ball z0 r)
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (poly [:z0, complex_of_real r:]) (ball 0 1) (ball z0 r)
[PROOF STEP]
using bij_betw_ball_uball[OF \<open>r>0\<close>,of z0]
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>x. complex_of_real r * x + z0) (ball 0 1) (ball z0 r)

goal (1 subgoal):
 1. bij_betw (poly [:z0, complex_of_real r:]) (ball 0 1) (ball z0 r)
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q = 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q = 1
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree [:z0, complex_of_real r:] = 1
[PROOF STEP]
using \<open>r>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. degree [:z0, complex_of_real r:] = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
p \<noteq> 0 \<Longrightarrow> card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))

goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p = 0 \<Longrightarrow> card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
p \<noteq> 0 \<Longrightarrow> card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = 0 \<Longrightarrow> card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
p \<noteq> 0 \<Longrightarrow> card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))

goal (1 subgoal):
 1. card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (proots_within p (ball z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (ball 0 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_card_usphere_eq:
  fixes z0::complex and r::real
  defines "q\<equiv>[:z0, of_real r:]"
  assumes "r>0"
  shows "card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
have ?thesis
    when "p=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
have "card (sphere z0 r) = 0" "card (sphere (0::complex) 1) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sphere z0 r) = 0 &&& card (sphere 0 1) = 0
[PROOF STEP]
using infinite_sphere[OF \<open>r>0\<close>,of z0] infinite_sphere[of 1 "0::complex"]
[PROOF STATE]
proof (prove)
using this:
infinite (sphere z0 r)
0 < 1 \<Longrightarrow> infinite (sphere 0 1)

goal (1 subgoal):
 1. card (sphere z0 r) = 0 &&& card (sphere 0 1) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (sphere z0 r) = 0
card (sphere 0 1) = 0

goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (sphere z0 r) = 0
card (sphere 0 1) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (sphere z0 r) = 0
card (sphere 0 1) = 0

goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
card (sphere z0 r) = 0
card (sphere 0 1) = 0
p = 0

goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p = 0 \<Longrightarrow> card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))

goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p = 0 \<Longrightarrow> card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))

goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
have ?thesis
    when "p\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
apply (rule proots_card_pcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bij_betw (poly q) (sphere 0 1) (sphere z0 r)
 2. degree q = 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (poly q) (sphere 0 1) (sphere z0 r)
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (poly [:z0, complex_of_real r:]) (sphere 0 1) (sphere z0 r)
[PROOF STEP]
using bij_betw_sphere_usphere[OF \<open>r>0\<close>,of z0]
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>x. complex_of_real r * x + z0) (sphere 0 1) (sphere z0 r)

goal (1 subgoal):
 1. bij_betw (poly [:z0, complex_of_real r:]) (sphere 0 1) (sphere z0 r)
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q = 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree q = 1
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree [:z0, complex_of_real r:] = 1
[PROOF STEP]
using \<open>r>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. degree [:z0, complex_of_real r:] = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
p \<noteq> 0 \<Longrightarrow> card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))

goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p = 0 \<Longrightarrow> card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
p \<noteq> 0 \<Longrightarrow> card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
show "card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))"
[PROOF STATE]
proof (prove)
using this:
p = 0 \<Longrightarrow> card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
p \<noteq> 0 \<Longrightarrow> card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))

goal (1 subgoal):
 1. card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (proots_within p (sphere z0 r)) = card (proots_within (p \<circ>\<^sub>p q) (sphere 0 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_proots_open_segments:
  assumes "poly p st \<noteq>0" "poly p tt \<noteq> 0"
  shows "card (proots_within p (open_segment st tt)) =
                (let pc = pcompose p [:st, tt - st:];
                     pR = map_poly Re pc;
                     pI = map_poly Im pc;
                     g  = gcd pR pI
                 in changes_itv_smods 0 1 g (pderiv g))" (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 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. int (card (proots_within p (open_segment 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 changes_itv_smods 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]
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. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
have "?R = changes_itv_smods 0 1 g (pderiv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in changes_itv_smods 0 1 g (pderiv g)) = changes_itv_smods 0 1 g (pderiv g)
[PROOF STEP]
unfolding pc_def g_def pI_def pR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in changes_itv_smods 0 1 g (pderiv g)) = 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:]))))
[PROOF STEP]
by (auto simp add:Let_def)
[PROOF STATE]
proof (state)
this:
(let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in changes_itv_smods 0 1 g (pderiv g)) = changes_itv_smods 0 1 g (pderiv g)

goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(let pc = p \<circ>\<^sub>p [:st, tt - st:]; pR = map_poly Re pc; pI = map_poly Im pc; g = gcd pR pI in changes_itv_smods 0 1 g (pderiv g)) = changes_itv_smods 0 1 g (pderiv g)

goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
have "... = card {t. poly g t = 0 \<and> 0 < t \<and> t < 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. changes_itv_smods 0 1 g (pderiv g) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. changes_itv_smods 0 1 g (pderiv g) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})
[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] assms
[PROOF STATE]
proof (prove)
using this:
(poly g 0 = 0) = (poly pc (complex_of_real 0) = 0)
poly p st \<noteq> 0
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
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) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})
[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) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})
[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] assms
[PROOF STATE]
proof (prove)
using this:
(poly g 1 = 0) = (poly pc (complex_of_real 1) = 0)
poly p st \<noteq> 0
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
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) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})
[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) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})
[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) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
changes_itv_smods 0 1 g (pderiv g) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})

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

goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
changes_itv_smods 0 1 g (pderiv g) = int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1})

goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
have "... = card {t::real. poly pc (of_real t) = 0 \<and> 0 < t \<and> t < 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1}) = int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1})
[PROOF STEP]
unfolding poly_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1}) = int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1})

goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
int (card {t. poly g t = 0 \<and> 0 < t \<and> t < 1}) = int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1})

goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
have "... = ?L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
proof (cases "st=tt")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. st = tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
 2. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
st = tt

goal (2 subgoals):
 1. st = tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
 2. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
st = tt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
st = tt

goal (1 subgoal):
 1. int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
unfolding pc_def poly_pcompose
[PROOF STATE]
proof (prove)
using this:
st = tt

goal (1 subgoal):
 1. int (card {t. poly p (poly [:st, tt - st:] (complex_of_real t)) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
using \<open>poly p tt \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
st = tt
poly p tt \<noteq> 0

goal (1 subgoal):
 1. int (card {t. poly p (poly [:st, tt - st:] (complex_of_real t)) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
st \<noteq> tt

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
define ff where "ff = (\<lambda>t::real. st + t*(tt-st))"
[PROOF STATE]
proof (state)
this:
ff = (\<lambda>x. st + complex_of_real x * (tt - st))

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
define ll where "ll = {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}"
[PROOF STATE]
proof (state)
this:
ll = {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
have "ff ` ll = proots_within p (open_segment st tt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff ` ll = proots_within p (open_segment st tt)
[PROOF STEP]
proof (rule equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ff ` ll \<subseteq> proots_within p (open_segment st tt)
 2. proots_within p (open_segment st tt) \<subseteq> ff ` ll
[PROOF STEP]
show "ff ` ll \<subseteq> proots_within p (open_segment st tt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff ` ll \<subseteq> proots_within p (open_segment st tt)
[PROOF STEP]
unfolding ll_def ff_def pc_def poly_pcompose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. st + complex_of_real x * (tt - st)) ` {t. poly p (poly [:st, tt - st:] (complex_of_real t)) = 0 \<and> 0 < t \<and> t < 1} \<subseteq> proots_within p (open_segment st tt)
[PROOF STEP]
by (auto simp add:in_segment False scaleR_conv_of_real algebra_simps)
[PROOF STATE]
proof (state)
this:
ff ` ll \<subseteq> proots_within p (open_segment st tt)

goal (1 subgoal):
 1. proots_within p (open_segment st tt) \<subseteq> ff ` ll
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_within p (open_segment st tt) \<subseteq> ff ` ll
[PROOF STEP]
show "proots_within p (open_segment st tt) \<subseteq> ff ` ll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_within p (open_segment st tt) \<subseteq> ff ` ll
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
assume asm:"x \<in> proots_within p (open_segment st tt)"
[PROOF STATE]
proof (state)
this:
x \<in> proots_within p (open_segment st tt)

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> proots_within p (open_segment st tt)
[PROOF STEP]
obtain u where "0<u" and "u < 1" and u:"x = (1 - u) *\<^sub>R st + u *\<^sub>R tt"
[PROOF STATE]
proof (prove)
using this:
x \<in> proots_within p (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]
by (auto simp add:in_segment)
[PROOF STATE]
proof (state)
this:
0 < u
u < 1
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < u
u < 1
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt
[PROOF STEP]
have "poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0"
[PROOF STATE]
proof (prove)
using this:
0 < u
u < 1
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (1 subgoal):
 1. poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
0 < u
u < 1
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt
x \<in> proots_within p (open_segment st tt)

goal (1 subgoal):
 1. poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0
[PROOF STEP]
have "u \<in> ll"
[PROOF STATE]
proof (prove)
using this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0

goal (1 subgoal):
 1. u \<in> ll
[PROOF STEP]
unfolding ll_def pc_def poly_pcompose
[PROOF STATE]
proof (prove)
using this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0

goal (1 subgoal):
 1. u \<in> {t. poly p (poly [:st, tt - st:] (complex_of_real t)) = 0 \<and> 0 < t \<and> t < 1}
[PROOF STEP]
by (simp add:scaleR_conv_of_real algebra_simps \<open>0<u\<close> \<open>u<1\<close>)
[PROOF STATE]
proof (state)
this:
u \<in> ll

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<in> ll

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
have "x = ff u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = ff u
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = st + complex_of_real u * (tt - st)
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (1 subgoal):
 1. x = st + complex_of_real u * (tt - st)
[PROOF STEP]
by (auto simp add:algebra_simps scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
x = ff u

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (open_segment st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<in> ll
x = ff u
[PROOF STEP]
show "x \<in> ff ` ll"
[PROOF STATE]
proof (prove)
using this:
u \<in> ll
x = ff u

goal (1 subgoal):
 1. x \<in> ff ` ll
[PROOF STEP]
by (rule rev_image_eqI[of "u"])
[PROOF STATE]
proof (state)
this:
x \<in> ff ` ll

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proots_within p (open_segment st tt) \<subseteq> ff ` ll

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ff ` ll = proots_within p (open_segment st tt)

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ff ` ll = proots_within p (open_segment st tt)

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
have "inj_on ff ll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ff ll
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. st + complex_of_real x * (tt - st)) ll
[PROOF STEP]
using False inj_on_def
[PROOF STATE]
proof (prove)
using this:
st \<noteq> tt
inj_on ?f ?A = (\<forall>x\<in>?A. \<forall>y\<in>?A. ?f x = ?f y \<longrightarrow> x = y)

goal (1 subgoal):
 1. inj_on (\<lambda>x. st + complex_of_real x * (tt - st)) ll
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inj_on ff ll

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ff ` ll = proots_within p (open_segment st tt)
inj_on ff ll
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ff ` ll = proots_within p (open_segment st tt)
inj_on ff ll

goal (1 subgoal):
 1. int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
unfolding ll_def
[PROOF STATE]
proof (prove)
using this:
ff ` {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1} = proots_within p (open_segment st tt)
inj_on ff {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}

goal (1 subgoal):
 1. int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
using card_image[of ff]
[PROOF STATE]
proof (prove)
using this:
ff ` {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1} = proots_within p (open_segment st tt)
inj_on ff {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}
inj_on ff ?A \<Longrightarrow> card (ff ` ?A) = card ?A

goal (1 subgoal):
 1. int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
int (card {t. poly pc (complex_of_real t) = 0 \<and> 0 < t \<and> t < 1}) = int (card (proots_within p (open_segment st tt)))

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

goal (1 subgoal):
 1. int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int (card (proots_within p (open_segment 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 changes_itv_smods 0 1 g (pderiv g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unbounded_line_closed_segment: "closed_segment a b \<subseteq> unbounded_line a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment a b \<subseteq> unbounded_line a b
[PROOF STEP]
unfolding unbounded_line_def closed_segment_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(1 - u) *\<^sub>R a + u *\<^sub>R b |u. 0 \<le> u \<and> u \<le> 1} \<subseteq> {x. \<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b}
[PROOF STEP]
by auto


[STATEMENT]
lemma card_proots_unbounded_line:
  assumes "st\<noteq>tt"
  shows "card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))" (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods 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. card (proots_within p (unbounded_line 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_R_smods 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]
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. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
have "?R = nat (changes_R_smods g (pderiv g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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_R_smods g (pderiv g))) = nat (changes_R_smods g (pderiv g))
[PROOF STEP]
unfolding pc_def g_def pI_def pR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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_R_smods g (pderiv g))) = nat (changes_R_smods (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:])))))
[PROOF STEP]
by (auto simp add:Let_def)
[PROOF STATE]
proof (state)
this:
(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_R_smods g (pderiv g))) = nat (changes_R_smods g (pderiv g))

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(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_R_smods g (pderiv g))) = nat (changes_R_smods g (pderiv g))

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
have "... = card {t. poly g t = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (changes_R_smods g (pderiv g)) = card {t. poly g t = 0}
[PROOF STEP]
using sturm_R[of g]
[PROOF STATE]
proof (prove)
using this:
int (card {x. poly g x = 0}) = changes_R_smods g (pderiv g)

goal (1 subgoal):
 1. nat (changes_R_smods g (pderiv g)) = card {t. poly g t = 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nat (changes_R_smods g (pderiv g)) = card {t. poly g t = 0}

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nat (changes_R_smods g (pderiv g)) = card {t. poly g t = 0}

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
have "... = card {t::real. poly pc t = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {t. poly g t = 0} = card {x. poly pc (complex_of_real x) = 0}
[PROOF STEP]
unfolding poly_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {t. poly pc (complex_of_real t) = 0} = card {x. poly pc (complex_of_real x) = 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {t. poly g t = 0} = card {x. poly pc (complex_of_real x) = 0}

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {t. poly g t = 0} = card {x. poly pc (complex_of_real x) = 0}

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
have "... = ?L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
proof (cases "st=tt")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. st = tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
 2. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
st = tt

goal (2 subgoals):
 1. st = tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
 2. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
st = tt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
st = tt

goal (1 subgoal):
 1. card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
unfolding pc_def poly_pcompose unbounded_line_def
[PROOF STATE]
proof (prove)
using this:
st = tt

goal (1 subgoal):
 1. card {x. poly p (poly [:st, tt - st:] (complex_of_real x)) = 0} = card (proots_within p {x. \<exists>u. x = (1 - u) *\<^sub>R st + u *\<^sub>R tt})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
st = tt
st \<noteq> tt

goal (1 subgoal):
 1. card {x. poly p (poly [:st, tt - st:] (complex_of_real x)) = 0} = card (proots_within p {x. \<exists>u. x = (1 - u) *\<^sub>R st + u *\<^sub>R tt})
[PROOF STEP]
by (auto simp add:proots_within_def)
[PROOF STATE]
proof (state)
this:
card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
st \<noteq> tt

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
define ff where "ff = (\<lambda>t::real. st + t*(tt-st))"
[PROOF STATE]
proof (state)
this:
ff = (\<lambda>x. st + complex_of_real x * (tt - st))

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
define ll where "ll = {t. poly pc (complex_of_real t) = 0}"
[PROOF STATE]
proof (state)
this:
ll = {t. poly pc (complex_of_real t) = 0}

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
have "ff ` ll = proots_within p (unbounded_line st tt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff ` ll = proots_within p (unbounded_line st tt)
[PROOF STEP]
proof (rule equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ff ` ll \<subseteq> proots_within p (unbounded_line st tt)
 2. proots_within p (unbounded_line st tt) \<subseteq> ff ` ll
[PROOF STEP]
show "ff ` ll \<subseteq> proots_within p (unbounded_line st tt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff ` ll \<subseteq> proots_within p (unbounded_line st tt)
[PROOF STEP]
unfolding ll_def ff_def pc_def poly_pcompose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. st + complex_of_real x * (tt - st)) ` {t. poly p (poly [:st, tt - st:] (complex_of_real t)) = 0} \<subseteq> proots_within p (unbounded_line st tt)
[PROOF STEP]
by (auto simp add:unbounded_line_def False scaleR_conv_of_real algebra_simps)
[PROOF STATE]
proof (state)
this:
ff ` ll \<subseteq> proots_within p (unbounded_line st tt)

goal (1 subgoal):
 1. proots_within p (unbounded_line st tt) \<subseteq> ff ` ll
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_within p (unbounded_line st tt) \<subseteq> ff ` ll
[PROOF STEP]
show "proots_within p (unbounded_line st tt) \<subseteq> ff ` ll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_within p (unbounded_line st tt) \<subseteq> ff ` ll
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
assume asm:"x \<in> proots_within p (unbounded_line st tt)"
[PROOF STATE]
proof (state)
this:
x \<in> proots_within p (unbounded_line st tt)

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> proots_within p (unbounded_line st tt)
[PROOF STEP]
obtain u where u:"x = (1 - u) *\<^sub>R st + u *\<^sub>R tt"
[PROOF STATE]
proof (prove)
using this:
x \<in> proots_within p (unbounded_line st tt)

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

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt
[PROOF STEP]
have "poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0"
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (1 subgoal):
 1. poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt
x \<in> proots_within p (unbounded_line st tt)

goal (1 subgoal):
 1. poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0
[PROOF STEP]
have "u \<in> ll"
[PROOF STATE]
proof (prove)
using this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0

goal (1 subgoal):
 1. u \<in> ll
[PROOF STEP]
unfolding ll_def pc_def poly_pcompose
[PROOF STATE]
proof (prove)
using this:
poly p ((1 - u) *\<^sub>R st + u *\<^sub>R tt) = 0

goal (1 subgoal):
 1. u \<in> {t. poly p (poly [:st, tt - st:] (complex_of_real t)) = 0}
[PROOF STEP]
by (simp add:scaleR_conv_of_real algebra_simps unbounded_line_def)
[PROOF STATE]
proof (state)
this:
u \<in> ll

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<in> ll

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
have "x = ff u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = ff u
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = st + complex_of_real u * (tt - st)
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R st + u *\<^sub>R tt

goal (1 subgoal):
 1. x = st + complex_of_real u * (tt - st)
[PROOF STEP]
by (auto simp add:algebra_simps scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
x = ff u

goal (1 subgoal):
 1. \<And>x. x \<in> proots_within p (unbounded_line st tt) \<Longrightarrow> x \<in> ff ` ll
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<in> ll
x = ff u
[PROOF STEP]
show "x \<in> ff ` ll"
[PROOF STATE]
proof (prove)
using this:
u \<in> ll
x = ff u

goal (1 subgoal):
 1. x \<in> ff ` ll
[PROOF STEP]
by (rule rev_image_eqI[of "u"])
[PROOF STATE]
proof (state)
this:
x \<in> ff ` ll

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proots_within p (unbounded_line st tt) \<subseteq> ff ` ll

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ff ` ll = proots_within p (unbounded_line st tt)

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ff ` ll = proots_within p (unbounded_line st tt)

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
have "inj_on ff ll"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ff ll
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. st + complex_of_real x * (tt - st)) ll
[PROOF STEP]
using False inj_on_def
[PROOF STATE]
proof (prove)
using this:
st \<noteq> tt
inj_on ?f ?A = (\<forall>x\<in>?A. \<forall>y\<in>?A. ?f x = ?f y \<longrightarrow> x = y)

goal (1 subgoal):
 1. inj_on (\<lambda>x. st + complex_of_real x * (tt - st)) ll
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inj_on ff ll

goal (1 subgoal):
 1. st \<noteq> tt \<Longrightarrow> card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ff ` ll = proots_within p (unbounded_line st tt)
inj_on ff ll
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ff ` ll = proots_within p (unbounded_line st tt)
inj_on ff ll

goal (1 subgoal):
 1. card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
unfolding ll_def
[PROOF STATE]
proof (prove)
using this:
ff ` {t. poly pc (complex_of_real t) = 0} = proots_within p (unbounded_line st tt)
inj_on ff {t. poly pc (complex_of_real t) = 0}

goal (1 subgoal):
 1. card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
using card_image[of ff]
[PROOF STATE]
proof (prove)
using this:
ff ` {t. poly pc (complex_of_real t) = 0} = proots_within p (unbounded_line st tt)
inj_on ff {t. poly pc (complex_of_real t) = 0}
inj_on ff ?A \<Longrightarrow> card (ff ` ?A) = card ?A

goal (1 subgoal):
 1. card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {x. poly pc (complex_of_real x) = 0} = card (proots_within p (unbounded_line st tt))

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(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_R_smods g (pderiv g))) = card (proots_within p (unbounded_line st tt))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(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_R_smods g (pderiv g))) = card (proots_within p (unbounded_line st tt))

goal (1 subgoal):
 1. card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_count_gcd_eq:
  fixes p::"complex poly" and st tt::complex
    and g::"real poly"
  defines "pc \<equiv> pcompose p [:st, tt - st:]"
  defines "pR \<equiv> map_poly Re pc" and "pI \<equiv> map_poly Im pc"
  defines "g  \<equiv> gcd pR pI"
  assumes "st\<noteq>tt" "p\<noteq>0"
      and s1_def:"s1 = (\<lambda>x. poly [:st, tt - st:] (of_real x)) ` s2"
    shows "proots_count p s1 = proots_count g s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[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]
using assms pc_def pcompose_eq_0
[PROOF STATE]
proof (prove)
using this:
pc \<equiv> p \<circ>\<^sub>p [:st, tt - st:]
pR \<equiv> map_poly Re pc
pI \<equiv> map_poly Im pc
g \<equiv> gcd pR pI
st \<noteq> tt
p \<noteq> 0
s1 = (\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` s2
pc \<equiv> p \<circ>\<^sub>p [:st, tt - st:]
degree ?q \<noteq> 0 \<Longrightarrow> (?p \<circ>\<^sub>p ?q = 0) = (?p = 0)

goal (1 subgoal):
 1. pc \<noteq> 0
[PROOF STEP]
by (metis cancel_comm_monoid_add_class.diff_cancel degree_pCons_eq_if
          diff_eq_diff_eq less_nat_zero_code pCons_eq_0_iff zero_less_Suc)
[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_count p s1 = proots_count g s2
[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_count p s1 = proots_count g s2
[PROOF STEP]
have "proots_count g s2 = proots_count (map_poly complex_of_real g)
            (of_real ` s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count g s2 = proots_count (map_poly complex_of_real g) (complex_of_real ` s2)
[PROOF STEP]
apply (subst proots_count_of_real)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. g \<noteq> 0
 2. proots_count g s2 = proots_count g s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count g s2 = proots_count (map_poly complex_of_real g) (complex_of_real ` s2)

goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proots_count g s2 = proots_count (map_poly complex_of_real g) (complex_of_real ` s2)

goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[PROOF STEP]
have "... = proots_count pc (of_real ` s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count (map_poly complex_of_real g) (complex_of_real ` s2) = proots_count pc (complex_of_real ` s2)
[PROOF STEP]
apply (rule proots_count_cong)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>complex_of_real ` s2. order x (map_poly complex_of_real g) = order x pc
 2. map_poly complex_of_real g \<noteq> 0
 3. pc \<noteq> 0
[PROOF STEP]
by (auto simp add: map_poly_order_of_real order_eq)
[PROOF STATE]
proof (state)
this:
proots_count (map_poly complex_of_real g) (complex_of_real ` s2) = proots_count pc (complex_of_real ` s2)

goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proots_count (map_poly complex_of_real g) (complex_of_real ` s2) = proots_count pc (complex_of_real ` s2)

goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[PROOF STEP]
have "... = proots_count p s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count pc (complex_of_real ` s2) = proots_count p s1
[PROOF STEP]
unfolding pc_def s1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count (p \<circ>\<^sub>p [:st, tt - st:]) (complex_of_real ` s2) = proots_count p ((\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` s2)
[PROOF STEP]
apply (subst proots_pcompose)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. p \<noteq> 0
 2. degree [:st, tt - st:] = 1
 3. proots_count p (poly [:st, tt - st:] ` complex_of_real ` s2) = proots_count p ((\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` s2)
[PROOF STEP]
using \<open>st\<noteq>tt\<close> \<open>p\<noteq>0\<close>
[PROOF STATE]
proof (prove)
using this:
st \<noteq> tt
p \<noteq> 0

goal (3 subgoals):
 1. p \<noteq> 0
 2. degree [:st, tt - st:] = 1
 3. proots_count p (poly [:st, tt - st:] ` complex_of_real ` s2) = proots_count p ((\<lambda>x. poly [:st, tt - st:] (complex_of_real x)) ` s2)
[PROOF STEP]
by (simp_all add:image_image)
[PROOF STATE]
proof (state)
this:
proots_count pc (complex_of_real ` s2) = proots_count p s1

goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proots_count g s2 = proots_count p s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proots_count g s2 = proots_count p s1

goal (1 subgoal):
 1. proots_count p s1 = proots_count g s2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proots_count p s1 = proots_count g s2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_unbounded_line:
  assumes "st\<noteq>tt" "p\<noteq>0"
  shows "(proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))" (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext 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_count p (unbounded_line 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_R_smods_ext 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]
using assms(1) assms(2) pc_def pcompose_eq_0
[PROOF STATE]
proof (prove)
using this:
st \<noteq> tt
p \<noteq> 0
pc = p \<circ>\<^sub>p [:st, tt - st:]
degree ?q \<noteq> 0 \<Longrightarrow> (?p \<circ>\<^sub>p ?q = 0) = (?p = 0)

goal (1 subgoal):
 1. pc \<noteq> 0
[PROOF STEP]
by (metis cancel_comm_monoid_add_class.diff_cancel degree_pCons_eq_if
          diff_eq_diff_eq less_nat_zero_code pCons_eq_0_iff zero_less_Suc)
[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_count p (unbounded_line 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_R_smods_ext 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_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
have "?R = nat (changes_R_smods_ext g (pderiv g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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_R_smods_ext g (pderiv g))) = nat (changes_R_smods_ext g (pderiv g))
[PROOF STEP]
unfolding pc_def g_def pI_def pR_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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_R_smods_ext g (pderiv g))) = nat (changes_R_smods_ext (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:])))))
[PROOF STEP]
by (auto simp add:Let_def)
[PROOF STATE]
proof (state)
this:
(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_R_smods_ext g (pderiv g))) = nat (changes_R_smods_ext g (pderiv g))

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(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_R_smods_ext g (pderiv g))) = nat (changes_R_smods_ext g (pderiv g))

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
have "... = proots_count g UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (changes_R_smods_ext g (pderiv g)) = proots_count g UNIV
[PROOF STEP]
using sturm_ext_R[OF \<open>g\<noteq>0\<close>]
[PROOF STATE]
proof (prove)
using this:
int (proots_count g UNIV) = changes_R_smods_ext g (pderiv g)

goal (1 subgoal):
 1. nat (changes_R_smods_ext g (pderiv g)) = proots_count g UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat (changes_R_smods_ext g (pderiv g)) = proots_count g UNIV

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nat (changes_R_smods_ext g (pderiv g)) = proots_count g UNIV

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
have "... = proots_count (map_poly complex_of_real g) (of_real ` UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count g UNIV = proots_count (map_poly complex_of_real g) (range complex_of_real)
[PROOF STEP]
apply (subst proots_count_of_real)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. g \<noteq> 0
 2. proots_count g UNIV = proots_count g UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count g UNIV = proots_count (map_poly complex_of_real g) (range complex_of_real)

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proots_count g UNIV = proots_count (map_poly complex_of_real g) (range complex_of_real)

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
have "... = proots_count (map_poly complex_of_real g) {x. Im x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count (map_poly complex_of_real g) (range complex_of_real) = proots_count (map_poly complex_of_real g) {x. Im x = 0}
[PROOF STEP]
apply (rule arg_cong2[where f=proots_count])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map_poly complex_of_real g = map_poly complex_of_real g
 2. range complex_of_real = {x. Im x = 0}
[PROOF STEP]
using Reals_def complex_is_Real_iff
[PROOF STATE]
proof (prove)
using this:
\<real> = range of_real
(?z \<in> \<real>) = (Im ?z = 0)

goal (2 subgoals):
 1. map_poly complex_of_real g = map_poly complex_of_real g
 2. range complex_of_real = {x. Im x = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count (map_poly complex_of_real g) (range complex_of_real) = proots_count (map_poly complex_of_real g) {x. Im x = 0}

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proots_count (map_poly complex_of_real g) (range complex_of_real) = proots_count (map_poly complex_of_real g) {x. Im x = 0}

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
have "... = proots_count pc {x. Im x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count (map_poly complex_of_real g) {x. Im x = 0} = proots_count pc {x. Im x = 0}
[PROOF STEP]
apply (rule proots_count_cong)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>{x. Im x = 0}. order x (map_poly complex_of_real g) = order x pc
 2. map_poly complex_of_real g \<noteq> 0
 3. pc \<noteq> 0
[PROOF STEP]
apply (metis (mono_tags) Im_complex_of_real Re_complex_of_real \<open>g \<noteq> 0\<close> complex_surj
            map_poly_order_of_real mem_Collect_eq order_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map_poly complex_of_real g \<noteq> 0
 2. pc \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count (map_poly complex_of_real g) {x. Im x = 0} = proots_count pc {x. Im x = 0}

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proots_count (map_poly complex_of_real g) {x. Im x = 0} = proots_count pc {x. Im x = 0}

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
have "... = proots_count p (unbounded_line st tt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count pc {x. Im x = 0} = proots_count p (unbounded_line st tt)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_count pc {x. Im x = 0} = proots_count p (unbounded_line st tt)
[PROOF STEP]
have "poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt
[PROOF STEP]
unfolding unbounded_line_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly [:st, tt - st:] ` {x. Im x = 0} = {x. \<exists>u. x = (1 - u) *\<^sub>R st + u *\<^sub>R tt}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. Im xa = 0 \<Longrightarrow> \<exists>u. poly [:st, tt - st:] xa = (1 - u) *\<^sub>R st + u *\<^sub>R tt
 2. \<And>x u. (1 - u) *\<^sub>R st + u *\<^sub>R tt \<in> poly [:st, tt - st:] ` {x. Im x = 0}
[PROOF STEP]
subgoal for _ x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = 0 \<Longrightarrow> \<exists>u. poly [:st, tt - st:] x = (1 - u) *\<^sub>R st + u *\<^sub>R tt
[PROOF STEP]
apply (rule_tac x="Re x" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = 0 \<Longrightarrow> poly [:st, tt - st:] x = (1 - Re x) *\<^sub>R st + Re x *\<^sub>R tt
[PROOF STEP]
apply (simp add:algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = 0 \<Longrightarrow> tt * x + Re x *\<^sub>R st = st * x + Re x *\<^sub>R tt
[PROOF STEP]
by (simp add: mult.commute scaleR_complex.code times_complex.code)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x u. (1 - u) *\<^sub>R st + u *\<^sub>R tt \<in> poly [:st, tt - st:] ` {x. Im x = 0}
[PROOF STEP]
subgoal for _ u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - u) *\<^sub>R st + u *\<^sub>R tt \<in> poly [:st, tt - st:] ` {x. Im x = 0}
[PROOF STEP]
apply (rule rev_image_eqI[of "of_real u"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. complex_of_real u \<in> {x. Im x = 0}
 2. (1 - u) *\<^sub>R st + u *\<^sub>R tt = poly [:st, tt - st:] (complex_of_real u)
[PROOF STEP]
by (auto simp:scaleR_conv_of_real algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt

goal (1 subgoal):
 1. proots_count pc {x. Im x = 0} = proots_count p (unbounded_line st tt)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt

goal (1 subgoal):
 1. proots_count pc {x. Im x = 0} = proots_count p (unbounded_line st tt)
[PROOF STEP]
unfolding pc_def
[PROOF STATE]
proof (prove)
using this:
poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt

goal (1 subgoal):
 1. proots_count (p \<circ>\<^sub>p [:st, tt - st:]) {x. Im x = 0} = proots_count p (unbounded_line st tt)
[PROOF STEP]
apply (subst proots_pcompose)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt \<Longrightarrow> p \<noteq> 0
 2. poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt \<Longrightarrow> degree [:st, tt - st:] = 1
 3. poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt \<Longrightarrow> proots_count p (poly [:st, tt - st:] ` {x. Im x = 0}) = proots_count p (unbounded_line st tt)
[PROOF STEP]
using \<open>p\<noteq>0\<close> \<open>st\<noteq>tt\<close>
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
st \<noteq> tt

goal (3 subgoals):
 1. poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt \<Longrightarrow> p \<noteq> 0
 2. poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt \<Longrightarrow> degree [:st, tt - st:] = 1
 3. poly [:st, tt - st:] ` {x. Im x = 0} = unbounded_line st tt \<Longrightarrow> proots_count p (poly [:st, tt - st:] ` {x. Im x = 0}) = proots_count p (unbounded_line st tt)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count pc {x. Im x = 0} = proots_count p (unbounded_line st tt)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proots_count pc {x. Im x = 0} = proots_count p (unbounded_line st tt)

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(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_R_smods_ext g (pderiv g))) = proots_count p (unbounded_line st tt)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(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_R_smods_ext g (pderiv g))) = proots_count p (unbounded_line st tt)

goal (1 subgoal):
 1. proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proots_count p (unbounded_line 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_R_smods_ext g (pderiv g)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_unbounded_line_card_code[code]:
  "proots_unbounded_line_card p st tt =
              (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_R_smods g (pderiv g)))
              else
                  Code.abort (STR ''proots_unbounded_line_card fails due to invalid hyperplanes.'')
                      (\<lambda>_. proots_unbounded_line_card p st tt))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_unbounded_line_card p st tt = (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_R_smods g (pderiv g)) else Code.abort STR ''proots_unbounded_line_card fails due to invalid hyperplanes.'' (\<lambda>_. proots_unbounded_line_card p st tt))
[PROOF STEP]
unfolding proots_unbounded_line_card_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (proots_within p (unbounded_line st tt)) = (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_R_smods g (pderiv g)) else Code.abort STR ''proots_unbounded_line_card fails due to invalid hyperplanes.'' (\<lambda>_. card (proots_within p (unbounded_line st tt))))
[PROOF STEP]
using card_proots_unbounded_line[of st tt p]
[PROOF STATE]
proof (prove)
using this:
st \<noteq> tt \<Longrightarrow> card (proots_within p (unbounded_line 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_R_smods g (pderiv g)))

goal (1 subgoal):
 1. card (proots_within p (unbounded_line st tt)) = (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_R_smods g (pderiv g)) else Code.abort STR ''proots_unbounded_line_card fails due to invalid hyperplanes.'' (\<lambda>_. card (proots_within p (unbounded_line st tt))))
[PROOF STEP]
by auto


[STATEMENT]
lemma proots_unbounded_line_code[code]:
  "proots_unbounded_line p st tt =
              ( if st\<noteq>tt then
                if p\<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 nat (changes_R_smods_ext g (pderiv g)))
                else
                  Code.abort (STR ''proots_unbounded_line fails due to p=0'')
                      (\<lambda>_. proots_unbounded_line p st tt)
                else
                  Code.abort (STR ''proots_unbounded_line fails due to invalid hyperplanes.'')
                      (\<lambda>_. proots_unbounded_line p st tt) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_unbounded_line p st tt = (if st \<noteq> tt then if p \<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 nat (changes_R_smods_ext g (pderiv g)) else Code.abort STR ''proots_unbounded_line fails due to p=0'' (\<lambda>_. proots_unbounded_line p st tt) else Code.abort STR ''proots_unbounded_line fails due to invalid hyperplanes.'' (\<lambda>_. proots_unbounded_line p st tt))
[PROOF STEP]
unfolding proots_unbounded_line_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p (unbounded_line st tt) = (if st \<noteq> tt then if p \<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 nat (changes_R_smods_ext g (pderiv g)) else Code.abort STR ''proots_unbounded_line fails due to p=0'' (\<lambda>_. proots_count p (unbounded_line st tt)) else Code.abort STR ''proots_unbounded_line fails due to invalid hyperplanes.'' (\<lambda>_. proots_count p (unbounded_line st tt)))
[PROOF STEP]
using proots_unbounded_line
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?st \<noteq> ?tt; ?p \<noteq> 0\<rbrakk> \<Longrightarrow> proots_count ?p (unbounded_line ?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_R_smods_ext g (pderiv g)))

goal (1 subgoal):
 1. proots_count p (unbounded_line st tt) = (if st \<noteq> tt then if p \<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 nat (changes_R_smods_ext g (pderiv g)) else Code.abort STR ''proots_unbounded_line fails due to p=0'' (\<lambda>_. proots_count p (unbounded_line st tt)) else Code.abort STR ''proots_unbounded_line fails due to invalid hyperplanes.'' (\<lambda>_. proots_count p (unbounded_line st tt)))
[PROOF STEP]
by auto