Quelle  BF_Misc.thy

(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section "Misc results for polynomials and sign variations"

theory BF_Misc imports
  "HOL-Computational_Algebra.Polynomial_Factorial"
  "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
  Sturm_Tarski.Sturm_Tarski
begin

subsection ‹Induction on polynomial roots›

(*adapted from the poly_root_induct in Polynomial.thy.*)
lemma poly_root_induct_alt [case_names 0 no_proots root]:
  fixes p :: "'a :: idom poly"
  assumes "Q 0"
  assumes "∧p. (∧a. poly p a ≠ 0) ==> Q p"
  assumes "∧a p. Q p ==> Q ([:-a, 1:] * p)"
  shows   "Q p"
proof (induction "degree p" arbitrary: p rule: less_induct)
  case (less p)
  have ?case when "p=0" using ‹Q 0› that by auto
  moreover have ?case when "∄a. poly p a = 0"
    using assms(2) that by blast
  moreover have ?case when "∃a. poly p a = 0" "p≠0"
  proof -
    obtain a where "poly p a =0" using ‹∃a. poly p a = 0› by auto
    then obtain q where pq:"p= [:-a,1:] * q" by (meson dvdE poly_eq_0_iff_dvd)
    then have "q≠0" using ‹p≠0› by auto
    then have "degree q<degree p" unfolding pq by (subst degree_mult_eq,auto)
    then have "Q q" using less by auto
    then show ?case using assms(3) unfolding pq by auto
  qed
  ultimately show ?case by auto
qed

subsection ‹Misc›

lemma lead_coeff_pderiv:
  fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly"
  shows "lead_coeff (pderiv p) = of_nat (degree p) * lead_coeff p"
  apply (auto simp:degree_pderiv coeff_pderiv)
  apply (cases "degree p")
  by (auto simp add: coeff_eq_0)

lemma gcd_degree_le_min:
  assumes "p≠0" "q≠0"
  shows "degree (gcd p q) ≤ min (degree p) (degree q)"
  by (simp add: assms(1) assms(2) dvd_imp_degree_le)

lemma lead_coeff_normalize_field:
  fixes p::"'a::{field,semidom_divide_unit_factor} poly"
  assumes "p≠0"
  shows "lead_coeff (normalize p) = 1"
  by (metis (no_types, lifting) assms coeff_normalize divide_self_if dvd_field_iff 
      is_unit_unit_factor leading_coeff_0_iff normalize_eq_0_iff normalize_idem)

lemma smult_normalize_field_eq:
  fixes p::"'a::{field,semidom_divide_unit_factor} poly"
  shows "p = smult (lead_coeff p) (normalize p)"
proof (rule poly_eqI)
  fix n
  have "unit_factor (lead_coeff p) = lead_coeff p"
    by (metis dvd_field_iff is_unit_unit_factor unit_factor_0)
  then show "coeff p n = coeff (smult (lead_coeff p) (normalize p)) n"
    by simp
qed

lemma lead_coeff_gcd_field:
  fixes p q::"'a::field_gcd poly"
  assumes "p≠0 ∨ q≠0"
  shows "lead_coeff (gcd p q) = 1"
  using assms by (metis gcd.normalize_idem gcd_eq_0_iff lead_coeff_normalize_field)

lemma poly_gcd_0_iff:
  "poly (gcd p q) x = 0 ⟷ poly p x=0 ∧ poly q x=0"
  by (simp add:poly_eq_0_iff_dvd)

lemma degree_eq_oneE:
  fixes p :: "'a::zero poly"
  assumes "degree p = 1"
  obtains a b where "p = [:a,b:]" "b≠0"
proof -
  obtain a b q where p:"p=pCons a (pCons b q)"
    by (metis pCons_cases)
  with assms have "q=0" by (cases "q = 0") simp_all
  with p have "p=[:a,b:]" by auto
  moreover then have "b≠0" using assms by auto
  ultimately show ?thesis ..
qed

subsection ‹More results about sign variations (i.e. @{term changes}›

lemma changes_0[simp]:"changes (0#xs) = changes xs"
  by (cases xs) auto

lemma changes_Cons:"changes (x#xs) = (if filter (λx. x≠0) xs = [] then
                            0
                          else if x* hd (filter (λx. x≠0) xs) < 0 then
                            1 + changes xs
                          else changes xs)"
  apply (induct xs)
  by auto

lemma changes_filter_eq:
  "changes (filter (λx. x≠0) xs) = changes xs"
  apply (induct xs)
  by (auto simp add:changes_Cons)

lemma changes_filter_empty:
  assumes "filter (λx. x≠0) xs = []"
  shows "changes xs = 0" "changes (a#xs) = 0" using assms
  apply (induct xs)
  apply auto
  by (metis changes_0 neq_Nil_conv)

lemma changes_append:
  assumes "xs≠ [] ∧ ys≠ [] ⟶ (last xs = hd ys ∧ last xs≠0)"
  shows "changes (xs@ys) = changes xs + changes ys"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  have ?case when "xs=[]"
    using that Cons 
    apply (cases ys)
    by auto
  moreover have ?case when "ys=[]"
    using that Cons by auto
  moreover have ?case when "xs≠[]" "ys≠[]"
  proof -
    have "filter (λx. x ≠ 0) xs ≠[]"
      using that Cons 
      apply auto 
      by (metis (mono_tags, lifting) filter.simps(1) filter.simps(2) filter_append snoc_eq_iff_butlast)
    then have "changes (a # xs @ ys) = changes (a # xs) + changes ys"
      apply (subst (1 2) changes_Cons)
      using that Cons by auto
    then show ?thesis by auto
  qed
  ultimately show ?case by blast
qed

lemma changes_drop_dup:
  assumes "xs≠ []" "ys≠ [] ⟶ last xs=hd ys"
  shows "changes (xs@ys) = changes (xs@ tl ys)"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  have ?case when "ys=[]"
    using that by simp
  moreover have ?case when "ys≠[]" "xs=[]"
    using that Cons
    apply auto
    by (metis changes.simps(3) list.exhaust_sel not_square_less_zero)
  moreover have ?case when "ys≠[]" "xs≠[]"
  proof -
    define ts ts' where "ts = filter (λx. x ≠ 0) (xs @ ys)"
      and "ts' = filter (λx. x ≠ 0) (xs @ tl ys)"
    have "(ts = [] ⟷ ts' = []) ∧ hd ts = hd ts'"
    proof (cases "filter (λx. x ≠ 0) xs = []")
      case True
      then have "last xs = 0" using ‹xs≠[]›
        by (metis (mono_tags, lifting) append_butlast_last_id append_is_Nil_conv 
            filter.simps(2) filter_append list.simps(3))
      then have "hd ys=0" using Cons(3)[rule_format, OF ‹ys≠[]›] ‹xs≠[]› by auto
      then have "filter (λx. x ≠ 0) ys = filter (λx. x ≠ 0) (tl ys)"
        by (metis (mono_tags, lifting) filter.simps(2) list.exhaust_sel that(1))
      then show ?thesis unfolding ts_def ts'_def by auto
    next
      case False
      then show ?thesis unfolding ts_def ts'_def by auto
    qed
    moreover have "changes (xs @ ys) = changes (xs @ tl ys)"
      apply (rule Cons(1))
      using that Cons(3) by auto
    moreover have "changes (a # xs @ ys) = (if ts = [] then 0 else if a * hd ts < 0
            then 1 + changes (xs @ ys) else changes (xs @ ys))"
      using changes_Cons[of a "xs @ ys",folded ts_def] .
    moreover have "changes (a # xs @ tl ys) = (if ts' = [] then 0 else if a * hd ts' < 0
            then 1 + changes (xs @ tl ys) else changes (xs @ tl ys))"
      using changes_Cons[of a "xs @ tl ys",folded ts'_def] .
    ultimately show ?thesis by auto
  qed
  ultimately show ?case by blast
qed

(*
  TODO: the following lemmas contain duplicates of some lemmas in 
          Winding_Number_Eval/Missing_Algebraic.thy
  Will resolve later.  
*)

lemma Im_poly_of_real:
  "Im (poly p (of_real x)) = poly (map_poly Im p) x"
  apply (induct p)
  by (auto simp add:map_poly_pCons)
 
lemma Re_poly_of_real:
  "Re (poly p (of_real x)) = poly (map_poly Re p) x"
  apply (induct p)
  by (auto simp add:map_poly_pCons)

subsection ‹More about @{term map_poly} and @{term of_real}›

lemma of_real_poly_map_pCons[simp]:"map_poly of_real (pCons a p) = pCons (of_real a) (map_poly of_real p)" 
  by (simp add: map_poly_pCons)    
    
lemma of_real_poly_map_plus[simp]: "map_poly of_real (p + q) = map_poly of_real p + map_poly of_real q" 
  apply (rule poly_eqI)
  by (auto simp add: coeff_map_poly)  
 
lemma of_real_poly_map_smult[simp]:"map_poly of_real (smult s p) = smult (of_real s) (map_poly of_real p)" 
  apply (rule poly_eqI)
  by (auto simp add: coeff_map_poly)    

lemma of_real_poly_map_mult[simp]:"map_poly of_real (p*q) = map_poly of_real p * map_poly of_real q"
  by (induct p,intro poly_eqI,auto)
    
lemma of_real_poly_map_poly:
  "of_real (poly p x) = poly (map_poly of_real p) (of_real x)" 
  by (induct p,auto)    

lemma of_real_poly_map_power:"map_poly of_real (p^n) = (map_poly of_real p) ^ n"
  by (induct n,auto)

(*FIXME: not duplicate*)
lemma of_real_poly_eq_iff [simp]: "map_poly of_real p = map_poly of_real q ⟷ p = q"
  by (auto simp: poly_eq_iff coeff_map_poly)

(*FIXME: not duplicate*)
lemma of_real_poly_eq_0_iff [simp]: "map_poly of_real p = 0 ⟷ p = 0"
  by (auto simp: poly_eq_iff coeff_map_poly)

subsection ‹More about @{term order}›

lemma order_multiplicity_eq:
  assumes "p≠0"
  shows "order a p = multiplicity [:-a,1:] p"
  by (metis assms multiplicity_eqI order_1 order_2)

lemma order_gcd:
  assumes "p≠0" "q≠0"
  shows "order x (gcd p q) = min (order x p) (order x q)"
proof -
  have "prime [:- x, 1:]" 
    apply (auto simp add: prime_elem_linear_poly normalize_poly_def  intro!:primeI)
    by (simp add: pCons_one)
  then show ?thesis  
    using assms
    by (auto simp add:order_multiplicity_eq intro:multiplicity_gcd)
qed

lemma order_linear[simp]: "order x [:-a,1:] = (if x=a then 1 else 0)"
  by (auto simp add:order_power_n_n[where n=1,simplified] order_0I)
  
lemma map_poly_order_of_real:
  assumes "p≠0"
  shows "order (of_real t) (map_poly of_real p) = order t p" using assms
proof (induct p rule:poly_root_induct_alt)
  case 0
  then show ?case by simp
next
  case (no_proots p)
  then have "order t p = 0" using order_root by blast
  moreover have "poly (map_poly of_real p) (of_real x) ≠0" for x
    apply (subst of_real_poly_map_poly[symmetric])
    using no_proots order_root by simp
  then have "order (of_real t) (map_poly of_real p) = 0"
    using order_root by blast
  ultimately show ?case by auto
next
  case (root a p)
  define a1 where "a1=[:-a,1:]"
  have [simp]:"a1≠0" "p≠0" unfolding a1_def using root(2) by auto
  have "order (of_real t) (map_poly of_real a1) = order t a1"
    unfolding a1_def by simp
  then show ?case 
    apply (fold a1_def)
    by (simp add:order_mult root)
qed

lemma order_pcompose:
  assumes "pcompose p q≠0"
  shows "order x (pcompose p q) = order x (q-[:poly q x:]) * order (poly q x) p" 
  using ‹pcompose p q≠0›
proof (induct p rule:poly_root_induct_alt)
  case 0
  then show ?case by simp
next
  case (no_proots p)
  have "order x (p ∘_p q) = 0"
    apply (rule order_0I)
    using no_proots by (auto simp:poly_pcompose)
  moreover have "order (poly q x) p = 0"
    apply (rule order_0I)
    using no_proots by (auto simp:poly_pcompose)
  ultimately show ?case by auto
next
  case (root a p)
  define a1 where "a1=[:-a,1:]"
  have [simp]: "a1≠0" "p≠0" "a1 ∘_p q ≠0" "p ∘_p q ≠ 0" 
    subgoal using root(2) unfolding a1_def by simp
    subgoal using root(2) by auto
    using root(2) by (fold a1_def,auto simp:pcompose_mult)
  have "order x ((a1 * p) ∘_p q) = order x (a1 ∘_p q) + order x (p ∘_p q)"
    unfolding pcompose_mult by (auto simp: order_mult)
  also have "... = order x (q-[:poly q x:]) * (order (poly q x) a1 + order (poly q x) p)"
  proof -
    have "order x (a1 ∘_p q) = order x (q-[:poly q x:]) * order (poly q x) a1"
      unfolding a1_def 
      apply (auto simp: pcompose_pCons algebra_simps diff_conv_add_uminus )
      by (simp add: order_0I)
    moreover have "order x (p ∘_p q) = order x (q - [:poly q x:]) * order (poly q x) p"
      apply (rule root.hyps)
      by auto
    ultimately show ?thesis by (auto simp:algebra_simps)
  qed
  also have "... = order x (q - [:poly q x:]) * order (poly q x) (a1 * p)"
    by (auto simp:order_mult)
  finally show ?case unfolding a1_def .
qed

subsection ‹Polynomial roots / zeros›

definition proots_within::"'a::comm_semiring_0 poly ==> 'a set ==> 'a set" where
  "proots_within p s = {x∈s. poly p x=0}"

abbreviation proots::"'a::comm_semiring_0 poly ==> 'a set" where
  "proots p ≡ proots_within p UNIV"

lemma proots_def: "proots p = {x. poly p x=0}" 
  unfolding proots_within_def by auto 

lemma proots_within_empty[simp]:
  "proots_within p {} = {}" unfolding proots_within_def by auto

lemma proots_within_0[simp]:
  "proots_within 0 s = s" unfolding proots_within_def by auto

lemma proots_withinI[intro,simp]:
  "poly p x=0 ==> x∈s ==> x∈proots_within p s"
  unfolding proots_within_def by auto

lemma proots_within_iff[simp]:
  "x∈proots_within p s ⟷ poly p x=0 ∧ x∈s"
  unfolding proots_within_def by auto

lemma proots_within_union:
  "proots_within p A ∪ proots_within p B = proots_within p (A ∪ B)"
  unfolding proots_within_def by auto

lemma proots_within_times:
  fixes s::"'a::{semiring_no_zero_divisors,comm_semiring_0} set"
  shows "proots_within (p*q) s = proots_within p s ∪ proots_within q s"
  unfolding proots_within_def by auto

lemma proots_within_gcd:
  fixes s::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize} set"
  shows "proots_within (gcd p q) s= proots_within p s ∩ proots_within q s"
  unfolding proots_within_def 
  by (auto simp add: poly_eq_0_iff_dvd) 

lemma proots_within_inter:
  "NO_MATCH UNIV s ==> proots_within p s = proots p ∩ s" 
  unfolding proots_within_def by auto

lemma proots_within_proots[simp]:
  "proots_within p s ⊆ proots p"
  unfolding proots_within_def by auto

lemma finite_proots[simp]: 
  fixes p :: "'a::idom poly"
  shows "p≠0 ==> finite (proots_within p s)"
  unfolding proots_within_def using poly_roots_finite by fast

lemma proots_within_pCons_1_iff:
  fixes a::"'a::idom"
  shows "proots_within [:-a,1:] s = (if a∈s then {a} else {})"
    "proots_within [:a,-1:] s = (if a∈s then {a} else {})"
  by (cases "a∈s",auto)

lemma proots_within_uminus[simp]:
  fixes p :: "'a::comm_ring poly"
  shows "proots_within (- p) s = proots_within p s"
  by auto

lemma proots_within_smult:
  fixes a::"'a::{semiring_no_zero_divisors,comm_semiring_0}"
  assumes "a≠0"
  shows "proots_within (smult a p) s = proots_within p s"
  unfolding proots_within_def using assms by auto 

subsection ‹Polynomial roots counting multiplicities.›

(*counting the number of proots WITH MULTIPLICITIES within a set*)
definition proots_count::"'a::idom poly ==> 'a set ==> nat" where
  "proots_count p s = (∑r∈proots_within p s. order r p)"  

lemma proots_count_emtpy[simp]:"proots_count p {} = 0"
  unfolding proots_count_def by auto

lemma proots_count_times:
  fixes s :: "'a::idom set"
  assumes "p*q≠0"
  shows "proots_count (p*q) s = proots_count p s + proots_count q s"
proof -
  define pts where "pts=proots_within p s" 
  define qts where "qts=proots_within q s"
  have [simp]: "finite pts" "finite qts" 
    using ‹p*q≠0› unfolding pts_def qts_def by auto
  have "(∑r∈pts ∪ qts. order r p) = (∑r∈pts. order r p)" 
  proof (rule comm_monoid_add_class.sum.mono_neutral_cong_right,simp_all)
    show "∀i∈pts ∪ qts - pts. order i p = 0" 
      unfolding pts_def qts_def proots_within_def using order_root by fastforce
  qed
  moreover have "(∑r∈pts ∪ qts. order r q) = (∑r∈qts. order r q)" 
  proof (rule comm_monoid_add_class.sum.mono_neutral_cong_right,simp_all)
    show "∀i∈pts ∪ qts - qts. order i q = 0" 
      unfolding pts_def qts_def proots_within_def using order_root by fastforce
  qed
  ultimately show ?thesis unfolding proots_count_def
    apply (simp add:proots_within_times order_mult[OF ‹p*q≠0›] sum.distrib)
    apply (fold pts_def qts_def)
    by auto
qed

lemma proots_count_power_n_n:
  shows "proots_count ([:- a, 1:]^n) s = (if a∈s ∧ n>0 then n else 0)"
proof -
  have "proots_within ([:- a, 1:] ^ n) s= (if a∈s ∧ n>0 then {a} else {})"
    unfolding proots_within_def by auto
  thus ?thesis unfolding proots_count_def using order_power_n_n by auto
qed

lemma degree_proots_count:
  fixes p::"complex poly"
  shows "degree p = proots_count p UNIV"
proof (induct "degree p" arbitrary:p )
  case 0
  then obtain c where c_def:"p=[:c:]" using degree_eq_zeroE by auto
  then show ?case unfolding proots_count_def 
    apply (cases "c=0")
    by (auto intro!:sum.infinite simp add:infinite_UNIV_char_0 order_0I)
next
  case (Suc n)
  then have "degree p≠0" and "p≠0" by auto
  obtain z where "poly p z = 0" 
    using Fundamental_Theorem_Algebra.fundamental_theorem_of_algebra ‹degree p≠0› constant_degree[of p]
    by auto
  define onez where "onez=[:-z,1:]" 
  have [simp]: "onez≠0" "degree onez = 1" unfolding onez_def by auto
  obtain q where q_def:"p= onez * q" 
    using poly_eq_0_iff_dvd ‹poly p z = 0› dvdE unfolding onez_def by blast
  hence "q≠0" using ‹p≠0› by auto
  hence "n=degree q" using degree_mult_eq[of onez q] ‹Suc n = degree p›
    apply (fold q_def)
    by auto
  hence "degree q = proots_count q UNIV" using Suc.hyps(1) by simp
  moreover have " Suc 0 = proots_count onez UNIV" 
    unfolding onez_def using proots_count_power_n_n[of z 1 UNIV]
    by auto
  ultimately show ?case 
    unfolding q_def using degree_mult_eq[of onez q] proots_count_times[of onez q UNIV] ‹q≠0›
    by auto
qed

lemma proots_count_smult:
  fixes a::"'a::{semiring_no_zero_divisors,idom}"
  assumes "a≠0"
  shows "proots_count (smult a p) s= proots_count p s"
proof (cases "p=0")
  case True
  then show ?thesis by auto
next
  case False
  then show ?thesis 
    unfolding proots_count_def
    using order_smult[OF assms] proots_within_smult[OF assms] by auto
qed


lemma proots_count_pCons_1_iff:
  fixes a::"'a::idom"
  shows "proots_count [:-a,1:] s = (if a∈s then 1 else 0)"
  unfolding proots_count_def 
  by (cases "a∈s",auto simp add:proots_within_pCons_1_iff order_power_n_n[of _ 1,simplified])

lemma proots_count_uminus[simp]:
  "proots_count (- p) s = proots_count p s"
  unfolding proots_count_def by simp

lemma card_proots_within_leq:
  assumes "p≠0"
  shows "proots_count p s ≥ card (proots_within p s)" using assms
proof (induct rule:poly_root_induct[of _ "λx. x∈s"])
  case 0
  then show ?case unfolding proots_within_def proots_count_def by auto
next
  case (no_roots p)
  then have "proots_within p s = {}" by auto
  then show ?case unfolding proots_count_def by auto
next
  case (root a p)
  have "card (proots_within ([:- a, 1:] * p) s)
      ≤ card (proots_within [:- a, 1:] s)+card (proots_within p s)" 
    unfolding proots_within_times by (auto simp add:card_Un_le)
  also have "... ≤ 1+ proots_count p s"
  proof -
    have "card (proots_within [:- a, 1:] s) ≤ 1"
    proof (cases "a∈s")
      case True
      then have "proots_within [:- a, 1:] s = {a}" by auto
      then show ?thesis by auto
    next
      case False
      then have "proots_within [:- a, 1:] s = {}" by auto
      then show ?thesis by auto
    qed
    moreover have "card (proots_within p s) ≤ proots_count p s"
      apply (rule root.hyps)
      using root by auto
    ultimately show ?thesis by auto
  qed
  also have "... = proots_count ([:- a,1:] * p) s"
    apply (subst proots_count_times)
    subgoal by (metis mult_eq_0_iff pCons_eq_0_iff root.prems zero_neq_one)  
    using root by (auto simp add:proots_count_pCons_1_iff)
  finally have "card (proots_within ([:- a, 1:] * p) s) ≤ proots_count ([:- a, 1:] * p) s" .
  then show ?case 
    by (metis (no_types, opaque_lifting) add.inverse_inverse add.inverse_neutral minus_pCons 
        mult_minus_left proots_count_uminus proots_within_uminus)
qed

(*FIXME: not duplicate*)
lemma proots_count_0_imp_empty:
  assumes "proots_count p s=0" "p≠0"
  shows "proots_within p s = {}"
proof -
  have "card (proots_within p s) = 0"
    using card_proots_within_leq[OF ‹p≠0›,of s] ‹proots_count p s=0› by auto
  moreover have "finite (proots_within p s)" using ‹p≠0› by auto
  ultimately show ?thesis by auto
qed

lemma proots_count_leq_degree:
  assumes "p≠0"
  shows "proots_count p s≤ degree p" using assms
proof (induct rule:poly_root_induct[of _ "λx. x∈s"])
  case 0
  then show ?case by auto
next
  case (no_roots p)
  then have "proots_within p s = {}" by auto
  then show ?case unfolding proots_count_def by auto
next
  case (root a p)
  have "proots_count ([:a, - 1:] * p) s = proots_count [:a, - 1:] s + proots_count p s"
    apply (subst proots_count_times)
    using root by auto
  also have "... = 1 + proots_count p s"
  proof -
    have "proots_count [:a, - 1:] s =1"
      by (metis (no_types, lifting) add.inverse_inverse add.inverse_neutral minus_pCons 
          proots_count_pCons_1_iff proots_count_uminus root.hyps(1))
    then show ?thesis by auto
  qed
  also have "... ≤ degree ([:a,-1:] * p)" 
    apply (subst degree_mult_eq)
    subgoal by auto
    subgoal using root by auto
    subgoal using root by (simp add: ‹p ≠ 0›)
    done
  finally show ?case .
qed

(*TODO: not a duplicate*)
lemma proots_count_union_disjoint:
  assumes "A ∩ B = {}" "p≠0"
  shows "proots_count p (A ∪ B) = proots_count p A + proots_count p B"
  unfolding proots_count_def 
  apply (subst proots_within_union[symmetric])
  apply (subst sum.union_disjoint)
  using assms by auto

lemma proots_count_cong:
  assumes order_eq:"∀x∈s. order x p = order x q" and "p≠0" and "q≠0"
  shows "proots_count p s = proots_count q s" unfolding proots_count_def
proof (rule sum.cong)
  have "poly p x = 0 ⟷ poly q x = 0" when "x∈s" for x
    using order_eq that by (simp add: assms(2) assms(3) order_root)
  then show "proots_within p s = proots_within q s" by auto
  show "∧x. x ∈ proots_within q s ==> order x p = order x q"
    using order_eq by auto
qed

lemma proots_count_of_real:
  assumes "p≠0"
  shows "proots_count (map_poly of_real p) ((of_real::_==>'a::{real_algebra_1,idom}) ` s)
            = proots_count p s"
proof -
  define k where "k=(of_real::_==>'a)"
  have "proots_within (map_poly of_real p) (k ` s) =k ` (proots_within p s)"
    unfolding proots_within_def k_def by (auto simp add:of_real_poly_map_poly[symmetric])
  then have "proots_count (map_poly of_real p) (k ` s)
                = (∑r∈k ` (proots_within p s). order r (map_poly of_real p))"
    unfolding proots_count_def by simp
  also have "... = sum ((λr. order r (map_poly of_real p)) ∘ k) (proots_within p s)"
    apply (subst sum.reindex) 
    unfolding k_def by (auto simp add: inj_on_def)
  also have "... = proots_count p s" unfolding proots_count_def
    apply (rule sum.cong)
    unfolding k_def comp_def using ‹p≠0› by (auto simp add:map_poly_order_of_real) 
  finally show ?thesis unfolding k_def .
qed

(*Is field really necessary here?*)
lemma proots_pcompose:
  fixes p q::"'a::field poly"
  assumes "p≠0" "degree q=1"
  shows "proots_count (pcompose p q) s = proots_count p (poly q ` s)"
proof -
  obtain a b where ab:"q=[:a,b:]" "b≠0"
    using ‹degree q=1› degree_eq_oneE by metis
  define f where "f=(λy. (y-a)/b)"
  have f_eq:"f (poly q x) = x" "poly q (f x) = x" for x
    unfolding f_def using ab by auto
  have "proots_count (p ∘<sub>p</sub> q) s = (∑r∈ f ` proots_within p (poly q ` s). order r (p ∘<sub>p</sub> q))" 
    unfolding proots_count_def
    apply (rule arg_cong2[where f =sum])
    apply (auto simp:poly_pcompose proots_within_def f_eq)
    by (metis (mono_tags, lifting) f_eq(1) image_eqI mem_Collect_eq)
  also have "... = (∑x∈proots_within p (poly q ` s). order (f x) (p ∘_p q))"
    apply (subst sum.reindex)
    subgoal unfolding f_def inj_on_def using ‹b≠0› by auto
    by simp
  also have "... = (∑x∈proots_within p (poly q ` s). order x p)"
  proof -
    have "p ∘<sub>p</sub> q ≠ 0" using assms(1) assms(2) pcompose_eq_0 by force
    moreover have "order (f x) (q - [:x:]) = 1" for x 
    proof -
      have "order (f x) (q - [:x:]) = order (f x) (smult b [:-((x - a) / b),1:])"
        unfolding f_def using ab by auto
      also have "... = 1"
        apply (subst order_smult)
        using ‹b≠0› unfolding f_def by auto
      finally show ?thesis .
    qed
    ultimately have "order (f x) (p ∘<sub>p</sub> q) = order x p" for x
      apply (subst order_pcompose)
      using f_eq by auto
    then show ?thesis by auto
  qed
  also have "... = proots_count p (poly q ` s)"
    unfolding proots_count_def by auto
  finally show ?thesis .
qed

subsection ‹Composition of a polynomial and a rational function›

(*composition of a polynomial and a rational function. Maybe a more general version in the future?*)
definition fcompose::"'a ::field poly ==> 'a poly ==> 'a poly ==> 'a poly" where
  "fcompose p q r = fst (fold_coeffs (λa (c,d). (d*[:a:] + q * c,r*d)) p (0,1))"

lemma fcompose_0 [simp]: "fcompose 0 q r = 0"
  by (simp add: fcompose_def)

lemma fcompose_const[simp]:"fcompose [:a:] q r = [:a:]"
  unfolding fcompose_def by (cases "a=0") auto

lemma fcompose_pCons: 
  "fcompose (pCons a p) q1 q2 = smult a (q2^(degree (pCons a p))) + q1 * fcompose p q1 q2"
proof (cases "p=0")
  case False
  define ff where "ff=(λa (c, d). (d * [:a:] + q1 * c, q2 * d))"
  define fc where "fc=fold_coeffs ff p (0, 1)"
  have snd_ff:"snd fc = (if p=0 then 1 else q2^(degree p + 1))" unfolding fc_def
    apply (induct p)
    subgoal by simp
    subgoal for a p
      by (auto simp add:ff_def split:if_splits prod.splits)
    done

  have "fcompose (pCons a p) q1 q2 = fst (fold_coeffs ff (pCons a p) (0, 1))"
    unfolding fcompose_def ff_def by simp
  also have "... = fst (ff a fc)"
    using False unfolding fc_def by auto
  also have "... = snd fc * [:a:] + q1 * fst fc"
    unfolding ff_def by (auto split:prod.splits)
  also have "... = smult a (q2^(degree (pCons a p))) + q1 * fst fc"
    using snd_ff False by auto
  also have "... = smult a (q2^(degree (pCons a p))) + q1 * fcompose p q1 q2"
    unfolding fc_def ff_def fcompose_def by simp
  finally show ?thesis .
qed simp

lemma fcompose_uminus:
  "fcompose (-p) q r = - fcompose p q r"
  by (induct p) (auto simp:fcompose_pCons)

lemma fcompose_add_less:
  assumes "degree p1 > degree p2"
  shows "fcompose (p1+p2) q1 q2
            = fcompose p1 q1 q2 + q2^(degree p1-degree p2) * fcompose p2 q1 q2"
  using assms
proof (induction p1 p2 rule: poly_induct2)
  case (pCons a1 p1 a2 p2)
  have ?case when "p2=0"
    using that by (simp add:fcompose_pCons smult_add_left)
  moreover have ?case when "p2≠0" "¬ degree p2 < degree p1"
    using that pCons(2) by auto
  moreover have ?case when "p2≠0" "degree p2< degree p1"
  proof -
    define d1 d2 where "d1=degree (pCons a1 p1)" and "d2=degree (pCons a2 p2) "
    define fp1 fp2 where "fp1= fcompose p1 q1 q2" and "fp2=fcompose p2 q1 q2"

    have "fcompose (pCons a1 p1 + pCons a2 p2) q1 q2
            = fcompose (pCons (a1+a2) (p1+p2)) q1 q2"
      by simp
    also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * fcompose (p1 + p2) q1 q2"
    proof -
      have "degree (pCons (a1 + a2) (p1 + p2)) = d1"
        unfolding d1_def using that degree_add_eq_left by fastforce
      then show ?thesis unfolding fcompose_pCons by simp
    qed
    also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * (fp1 + q2 ^ (d1 - d2) * fp2)"
    proof -
      have "degree p1 - degree p2 = d1 - d2"
        unfolding d1_def d2_def using that by simp
      then show ?thesis 
        unfolding pCons(1)[OF that(2),folded fp1_def fp2_def] by simp
    qed
    also have "... = fcompose (pCons a1 p1) q1 q2 + q2 ^ (d1 - d2)
                        * fcompose (pCons a2 p2) q1 q2"
    proof -
      have "d1 > d2" unfolding d1_def d2_def using that by auto
      then show ?thesis
        unfolding fcompose_pCons
        apply (fold d1_def d2_def fp1_def fp2_def)
        by (simp add:algebra_simps smult_add_left power_add[symmetric])
    qed
    finally show ?thesis unfolding d1_def d2_def .
  qed
  ultimately show ?case by blast
qed simp

lemma fcompose_add_eq:
  assumes "degree p1 = degree p2"
  shows "q2^(degree p1 - degree (p1+p2)) * fcompose (p1+p2) q1 q2
            = fcompose p1 q1 q2 + fcompose p2 q1 q2"
  using assms
proof (induction p1 p2 rule: poly_induct2)
  case (pCons a1 p1 a2 p2)
  have ?case when "p1+p2=0"
  proof -
    have "p2=-p1" using that by algebra
    then show ?thesis by (simp add:fcompose_pCons fcompose_uminus smult_add_left)
  qed
  moreover have ?case when "p1=0"
  proof -
    have "p2=0"
      using pCons(2) that by (auto split:if_splits)
    then show ?thesis using that by simp
  qed
  moreover have ?case when "p1≠0" "p1+p2≠0"
  proof -
    define d1 d2 dp where "d1=degree (pCons a1 p1)" and "d2=degree (pCons a2 p2)"
                            and "dp = degree p1 - degree (p1+p2)"
    define fp1 fp2 where "fp1= fcompose p1 q1 q2" and "fp2=fcompose p2 q1 q2"

    have "q2 ^ (degree (pCons a1 p1) - degree (pCons a1 p1 + pCons a2 p2)) *
             fcompose (pCons a1 p1 + pCons a2 p2) q1 q2
                = q2 ^ dp * fcompose (pCons (a1+a2) (p1 +p2)) q1 q2"
      unfolding dp_def using that by auto
    also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * (q2 ^ dp * fcompose (p1 + p2) q1 q2)"
    proof -
      have "degree p1 ≥ degree (p1 + p2)" 
        by (metis degree_add_le degree_pCons_eq_if not_less_eq_eq order_refl pCons.prems zero_le)
      then show ?thesis 
        unfolding fcompose_pCons dp_def d1_def using that
        by (simp add:algebra_simps power_add[symmetric])
    qed
    also have "... = smult (a1 + a2) (q2 ^ d1) + q1 * (fp1 + fp2)"
      apply (subst pCons(1)[folded dp_def fp1_def fp2_def])
      subgoal by (metis degree_pCons_eq_if diff_Suc_Suc diff_zero not_less_eq_eq pCons.prems zero_le)
      subgoal by simp
      done
    also have "... = fcompose (pCons a1 p1) q1 q2 + fcompose (pCons a2 p2) q1 q2"
    proof -
      have *:"d1 = degree (pCons a2 p2)"
        unfolding d1_def using pCons(2) by simp
      show ?thesis 
        unfolding fcompose_pCons
        apply (fold d1_def fp1_def fp2_def *)
        by (simp add:smult_add_left algebra_simps)
    qed
    finally show ?thesis .
  qed
  ultimately show ?case by blast
qed simp

lemma fcompose_add_const:
  "fcompose ([:a:] + p) q1 q2 = smult a (q2 ^ degree p) + fcompose p q1 q2"
  apply (cases p)
  by (auto simp add:fcompose_pCons smult_add_left)

lemma fcompose_smult: "fcompose (smult a p) q1 q2 = smult a (fcompose p q1 q2)"
  by (induct p) (simp_all add:fcompose_pCons smult_add_right)

lemma fcompose_mult: "fcompose (p1*p2) q1 q2 = fcompose p1 q1 q2 * fcompose p2 q1 q2"
proof (induct p1)
  case 0
  then show ?case by simp
next
  case (pCons a p1)
  have ?case when "p1=0 ∨ p2=0" 
    using that by (auto simp add:fcompose_smult)
  moreover have ?case when "p1≠0" "p2≠0" "a=0"
    using that by (simp add:fcompose_pCons pCons)
  moreover have ?case when "p1≠0" "p2≠0" "a≠0"
  proof -
    have "fcompose (pCons a p1 * p2) q1 q2
            = fcompose (pCons 0 (p1 * p2) + smult a p2) q1 q2"
      by (simp add:algebra_simps)
    also have "... = fcompose (pCons 0 (p1 * p2)) q1 q2
                        + q2 ^ (degree p1 +1) * fcompose (smult a p2) q1 q2"
    proof -
      have "degree (pCons 0 (p1 * p2)) > degree (smult a p2)"
        using that by (simp add: degree_mult_eq)
      from fcompose_add_less[OF this,of q1 q2] that 
      show ?thesis by (simp add:degree_mult_eq)
    qed
    also have "... = fcompose (pCons a p1) q1 q2 * fcompose p2 q1 q2"
      using that by (simp add:fcompose_pCons fcompose_smult pCons algebra_simps)
    finally show ?thesis .
  qed
  ultimately show ?case by blast
qed

lemma fcompose_poly:
  assumes "poly q2 x≠0"
  shows "poly p (poly q1 x/poly q2 x) = poly (fcompose p q1 q2) x / poly (q2^(degree p)) x"
  apply (induct p)
  using assms by (simp_all add:fcompose_pCons field_simps)

lemma poly_fcompose:
   assumes "poly q2 x≠0"
   shows "poly (fcompose p q1 q2) x = poly p (poly q1 x/poly q2 x) * (poly q2 x)^(degree p)"
  using fcompose_poly[OF assms] assms by (auto simp add:field_simps)
lemma poly_fcompose_0_denominator:
  assumes "poly q2 x=0"
  shows "poly (fcompose p q1 q2) x = poly q1 x ^ degree p * lead_coeff p"
  apply (induct p)
  using assms by (auto simp add:fcompose_pCons)

lemma fcompose_0_denominator:"fcompose p q1 0 = smult (lead_coeff p) (q1^degree p)"
  apply (induct p)
  by (auto simp:fcompose_pCons)

lemma fcompose_nzero:
  fixes p::"'a::field poly"
  assumes "p≠0" and "q2≠0" and nconst:"∀c. q1 ≠ smult c q2"
      and infi:"infinite (UNIV::'a set)"
  shows "fcompose p q1 q2 ≠ 0" using ‹p≠0›
proof (induct p rule:poly_root_induct_alt)
  case 0
  then show ?case by simp
next
  case (no_proots p)
  have False when "fcompose p q1 q2 = 0"
  proof -
    obtain x where "poly q2 x≠0" 
    proof -
      have "finite (proots q2)" using ‹q2≠0› by auto
      then have "∃x. poly q2 x≠0" 
        by (meson UNIV_I ex_new_if_finite infi proots_withinI)
      then show ?thesis using that by auto
    qed
    define y where "y = poly q1 x / poly q2 x"
    have "poly p y = 0"
      using ‹fcompose p q1 q2 = 0› fcompose_poly[OF ‹poly q2 x≠0›,of p q1,folded y_def] 
      by simp
    then show False using no_proots(1) by auto
  qed
  then show ?case by auto
next
  case (root a p)
  have "fcompose [:- a, 1:] q1 q2 ≠ 0" 
    unfolding fcompose_def using nconst[rule_format,of a]
    by simp
  moreover have "fcompose p q1 q2 ≠ 0" 
    using root by fastforce
  ultimately show ?case unfolding fcompose_mult by auto
qed

subsection ‹Bijection (@{term bij_betw}) and the number of polynomial roots›

lemma proots_fcompose_bij_eq:
  fixes p::"'a::field poly"
  assumes bij:"bij_betw (λx. poly q1 x/poly q2 x) A B" and "p≠0" 
      and nzero:"∀x∈A. poly q2 x≠0"
      and max_deg: "max (degree q1) (degree q2) ≤ 1"
      and nconst:"∀c. q1 ≠ smult c q2"
      and infi:"infinite (UNIV::'a set)"
  shows "proots_count p B = proots_count (fcompose p q1 q2) A"
  using ‹p≠0›
proof (induct p rule:poly_root_induct_alt)
  case 0
  then show ?case by simp
next
  case (no_proots p)
  have "proots_count p B = 0"
  proof -
    have "proots_within p B = {}"
      using no_proots by auto
    then show ?thesis unfolding proots_count_def by auto
  qed
  moreover have "proots_count (fcompose p q1 q2) A = 0"
  proof -
    have "proots_within (fcompose p q1 q2) A = {}"
      using no_proots unfolding proots_within_def
      by (smt (verit) div_0 empty_Collect_eq fcompose_poly nzero)
    then show ?thesis unfolding proots_count_def by auto
  qed
  ultimately show ?case by auto
next
  case (root b p)
  have "proots_count ([:- b, 1:] * p) B = proots_count [:- b, 1:] B + proots_count p B"
    using proots_count_times[OF ‹[:- b, 1:] * p ≠ 0›] by simp
  also have "... = proots_count (fcompose [:- b, 1:] q1 q2) A
                    + proots_count (fcompose p q1 q2) A" 
  proof -
    define g where "g=(λx. poly q1 x/poly q2 x)"

    have "proots_count [:- b, 1:] B = proots_count (fcompose [:- b, 1:] q1 q2) A" 
    proof (cases "b∈B")
      case True
      then have "proots_count [:- b, 1:] B = 1"
        unfolding proots_count_pCons_1_iff by simp
      moreover have "proots_count (fcompose [:- b, 1:] q1 q2) A = 1"
      proof -
        obtain a where "b=g a" "a∈A"
          using bij[folded g_def] True 
          by (metis bij_betwE bij_betw_the_inv_into f_the_inv_into_f_bij_betw)
        define qq where "qq=q1 - smult b q2"
        have qq_0:"poly qq a=0" and qq_deg: "degree qq≤1" and ‹qq≠0›
          unfolding qq_def
          subgoal using ‹b=g a› nzero[rule_format,OF ‹a∈A›] unfolding g_def by auto
          subgoal using max_deg by (simp add: degree_diff_le)
          subgoal using nconst[rule_format,of b] by auto
          done
        have "proots_within qq A = {a}" 
        proof -
          have "a∈proots_within qq A" 
            using qq_0 ‹a∈A› by auto
          moreover have "card (proots_within qq A) = 1" 
          proof -
            have "finite (proots_within qq A)" using ‹qq≠0› by simp
            moreover have "proots_within qq A ≠ {}"
              using ‹a∈proots_within qq A› by auto
            ultimately have "card (proots_within qq A) ≠0" by auto
            moreover have "card (proots_within qq A) ≤ 1" 
              by (meson ‹qq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree qq_deg)
            ultimately show ?thesis by auto
          qed
          ultimately show ?thesis by (metis card_1_singletonE singletonD)
        qed
        moreover have "order a qq=1" 
          by (metis One_nat_def ‹qq ≠ 0› le_antisym le_zero_eq not_less_eq_eq order_degree
                order_root qq_0 qq_deg)
        ultimately show ?thesis unfolding fcompose_def proots_count_def qq_def  
          by auto
      qed
      ultimately show ?thesis by auto
    next
      case False
      then have "proots_count [:- b, 1:] B = 0"
        unfolding proots_count_pCons_1_iff by simp
      moreover have "proots_count (fcompose [:- b, 1:] q1 q2) A = 0"
      proof -
        have "proots_within (fcompose [:- b, 1:] q1 q2) A = {}"
        proof (rule ccontr)
          assume "proots_within (fcompose [:- b, 1:] q1 q2) A ≠ {}"
          then obtain a where "a∈A" "poly q1 a = b * poly q2 a"
            unfolding fcompose_def proots_within_def by auto
          then have "b = g a"
            unfolding g_def using nzero[rule_format,OF ‹a∈A›] by auto
          then have "b∈B" using ‹a∈A› bij[folded g_def] using bij_betwE by blast
          then show False using False by auto
        qed  
        then show ?thesis unfolding proots_count_def by auto
      qed      
      ultimately show ?thesis by simp
    qed
    moreover have "proots_count p B = proots_count (fcompose p q1 q2) A" 
      apply (rule root.hyps)
      using mult_eq_0_iff root.prems by blast
    ultimately show ?thesis by auto
  qed
  also have "... = proots_count (fcompose ([:- b, 1:] * p) q1 q2) A"
  proof (cases "A={}")
    case False
    have "fcompose [:- b, 1:] q1 q2 ≠0" 
      using nconst[rule_format,of b] unfolding fcompose_def by auto
    moreover have "fcompose p q1 q2 ≠ 0" 
      apply (rule fcompose_nzero[OF _ _ nconst infi])
      subgoal using ‹[:- b, 1:] * p ≠ 0› by auto
      subgoal using nzero False by auto
      done
    ultimately show ?thesis unfolding fcompose_mult
      apply (subst proots_count_times)
      by auto
  qed auto
  finally show ?case .
qed

lemma proots_card_fcompose_bij_eq:
  fixes p::"'a::field poly"
  assumes bij:"bij_betw (λx. poly q1 x/poly q2 x) A B" and "p≠0" 
      and nzero:"∀x∈A. poly q2 x≠0"
      and max_deg: "max (degree q1) (degree q2) ≤ 1"
      and nconst:"∀c. q1 ≠ smult c q2"
      and infi:"infinite (UNIV::'a set)"
  shows "card (proots_within p B) = card (proots_within (fcompose p q1 q2) A)"
  using ‹p≠0›
proof (induct p rule:poly_root_induct_alt)
  case 0
  then show ?case by simp
next
  case (no_proots p)
  have "proots_within p B = {}" using no_proots by auto
  moreover have "proots_within (fcompose p q1 q2) A = {}" 
    using no_proots fcompose_poly 
    by (smt (verit) Collect_empty_eq divide_eq_0_iff nzero proots_within_def)
  ultimately show ?case by auto
next
  case (root b p)
  then have [simp]:"p≠0" by auto

  have ?case when "b∉B ∨ poly p b=0"
  proof -
    have "proots_within ([:- b, 1:] * p) B = proots_within p B"
      using that by auto
    moreover have "proots_within (fcompose ([:- b, 1:] * p) q1 q2) A
        = proots_within (fcompose p q1 q2) A"
      using that nzero unfolding fcompose_mult proots_within_times 
      apply (auto simp add: poly_fcompose)
      using bij bij_betwE by blast
    ultimately show ?thesis using root by auto
  qed
  moreover have ?case when "b∈B" "poly p b≠0"
  proof -
    define bb where "bb=[:- b, 1:]"
    have "card (proots_within (bb * p) B) = card {b} + card (proots_within p B)"
    proof -
      have "proots_within bb B = {b}" 
        using that unfolding bb_def by auto
      then show ?thesis unfolding proots_within_times
        apply (subst card_Un_disjoint)
        by (use that in auto)
    qed
    also have "... = 1 + card (proots_within (fcompose p q1 q2) A)"
      using root.hyps by simp
    also have "... = card (proots_within (fcompose (bb * p) q1 q2) A)"
      unfolding proots_within_times fcompose_mult
    proof (subst card_Un_disjoint) 
      obtain a where b_poly:"b=poly q1 a / poly q2 a" and "a∈A" 
        by (metis (no_types, lifting) ‹b ∈ B› bij bij_betwE bij_betw_the_inv_into 
            f_the_inv_into_f_bij_betw)
      define bbq pq where "bbq=fcompose bb q1 q2" and "pq=fcompose p q1 q2"
      have bbq_0:"poly bbq a=0" and bbq_deg: "degree bbq≤1" and "bbq≠0"
        unfolding bbq_def bb_def 
        subgoal using ‹a ∈ A› b_poly nzero poly_fcompose by fastforce
        subgoal by (metis (no_types, lifting) degree_add_le degree_pCons_eq_if degree_smult_le 
           dual_order.trans fcompose_const fcompose_pCons max.boundedE max_deg mult_cancel_left2 
           one_neq_zero one_poly_eq_simps(1) power.simps)
        subgoal by (metis ‹a ∈ A› ‹poly (fcompose [:- b, 1:] q1 q2) a = 0› fcompose_nzero infi 
                  nconst nzero one_neq_zero pCons_eq_0_iff)
        done
      show "finite (proots_within bbq A)" using ‹bbq≠0› by simp
      show "finite (proots_within pq A)" unfolding pq_def 
        by (metis ‹a ∈ A› ‹p ≠ 0› fcompose_nzero finite_proots infi nconst nzero poly_0 pq_def)
      have bbq_a:"proots_within bbq A = {a}"
      proof -
        have "a∈proots_within bbq A" 
          by (simp add: ‹a ∈ A› bbq_0)
        moreover have "card (proots_within bbq A) = 1" 
        proof -
          have "card (proots_within bbq A) ≠0" 
            using ‹a∈proots_within bbq A› ‹finite (proots_within bbq A)›
            by auto
          moreover have "card (proots_within bbq A) ≤ 1" 
            by (meson ‹bbq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree bbq_deg)
          ultimately show ?thesis by auto
        qed
        ultimately show ?thesis by (metis card_1_singletonE singletonD)
      qed
      show "proots_within (bbq) A ∩ proots_within (pq) A = {}" 
        using b_poly bbq_a fcompose_poly nzero pq_def that(2) by fastforce
      show "1 + card (proots_within pq A) = card (proots_within bbq A) + card (proots_within pq A)"
        using bbq_a by simp
    qed
    finally show ?thesis unfolding bb_def .
  qed
  ultimately show ?case by auto
qed 

lemma proots_pcompose_bij_eq:
  fixes p::"'a::idom poly"
  assumes bij:"bij_betw (λx. poly q x) A B" and "p≠0" 
      and q_deg: "degree q = 1"
  shows "proots_count p B = proots_count (p ∘_p q) A" using ‹p≠0›
proof (induct p rule:poly_root_induct_alt)
  case 0
  then show ?case by simp
next
  case (no_proots p)
  have "proots_count p B = 0"
  proof -
    have "proots_within p B = {}"
      using no_proots by auto
    then show ?thesis unfolding proots_count_def by auto
  qed
  moreover have "proots_count (p ∘_p q) A = 0"
  proof -
    have "proots_within (p ∘_p q) A = {}"
      using no_proots unfolding proots_within_def
      by (auto simp:poly_pcompose)
    then show ?thesis unfolding proots_count_def by auto
  qed
  ultimately show ?case by auto
next
  case (root b p)
  have "proots_count ([:- b, 1:] * p) B = proots_count [:- b, 1:] B + proots_count p B"
    using proots_count_times[OF ‹[:- b, 1:] * p ≠ 0›] by simp
  also have "... = proots_count ([:- b, 1:] ∘_p q) A + proots_count (p ∘_p q) A"
  proof -
    have "proots_count [:- b, 1:] B = proots_count ([:- b, 1:] ∘_p q) A"
    proof (cases "b∈B")
      case True
      then have "proots_count [:- b, 1:] B = 1" 
        unfolding proots_count_pCons_1_iff by simp
      moreover have "proots_count ([:- b, 1:] ∘_p q) A = 1" 
      proof -
        obtain a where "b=poly q a" "a∈A"
          using True bij by (metis bij_betwE bij_betw_the_inv_into f_the_inv_into_f_bij_betw)
        define qq where "qq=[:- b:] + q"
        have qq_0:"poly qq a=0" and qq_deg: "degree qq≤1" and ‹qq≠0›
          unfolding qq_def
          subgoal using ‹b=poly q a› by auto
          subgoal using q_deg by (simp add: degree_add_le)
          subgoal using q_deg add.inverse_unique by force
          done
        have "proots_within qq A = {a}" 
        proof -
          have "a∈proots_within qq A" 
            using qq_0 ‹a∈A› by auto
          moreover have "card (proots_within qq A) = 1" 
          proof -
            have "finite (proots_within qq A)" using ‹qq≠0› by simp
            moreover have "proots_within qq A ≠ {}"
              using ‹a∈proots_within qq A› by auto
            ultimately have "card (proots_within qq A) ≠0" by auto
            moreover have "card (proots_within qq A) ≤ 1" 
              by (meson ‹qq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree qq_deg)
            ultimately show ?thesis by auto
          qed
          ultimately show ?thesis by (metis card_1_singletonE singletonD)
        qed
        moreover have "order a qq=1" 
          by (metis One_nat_def ‹qq ≠ 0› le_antisym le_zero_eq not_less_eq_eq order_degree
                order_root qq_0 qq_deg)
        ultimately show ?thesis unfolding pcompose_def proots_count_def qq_def  
          by auto
      qed
      ultimately show ?thesis by auto
    next
      case False
      then have "proots_count [:- b, 1:] B = 0"
        unfolding proots_count_pCons_1_iff by simp
      moreover have "proots_count ([:- b, 1:] ∘_p q) A = 0"
      proof -
        have "proots_within ([:- b, 1:] ∘_p q) A = {}"
          unfolding pcompose_def 
          apply auto
          using False bij bij_betwE by blast
        then show ?thesis unfolding proots_count_def by auto
      qed      
      ultimately show ?thesis by simp
    qed
    moreover have "proots_count p B = proots_count (p ∘_p q) A"
      apply (rule root.hyps)
      using ‹[:- b, 1:] * p ≠ 0› by auto
    ultimately show ?thesis by auto
  qed
  also have "... = proots_count (([:- b, 1:] * p) ∘_p q) A"
    unfolding pcompose_mult
    apply (subst proots_count_times)
    subgoal by (metis (no_types, lifting) One_nat_def add.right_neutral degree_0 degree_mult_eq
      degree_pCons_eq_if degree_pcompose mult_eq_0_iff one_neq_zero one_pCons pcompose_mult
      q_deg root.prems)
    by simp
  finally show ?case .
qed

lemma proots_card_pcompose_bij_eq:
  fixes p::"'a::idom poly"
  assumes bij:"bij_betw (λx. poly q x) A B" and "p≠0" 
      and q_deg: "degree q = 1"
  shows "card (proots_within p B) = card (proots_within (p ∘_p q) A)" using ‹p≠0›
proof (induct p rule:poly_root_induct_alt)
  case 0
  then show ?case by auto
next
  case (no_proots p)
  have "proots_within p B = {}" using no_proots by auto
  moreover have "proots_within (p ∘_p q) A = {}" using no_proots 
    by (simp add: poly_pcompose proots_within_def)
  ultimately show ?case by auto
next
  case (root b p)
  then have [simp]:"p≠0" by auto
  have ?case when "b∉B ∨ poly p b=0"
  proof -
    have "proots_within ([:- b, 1:] * p) B = proots_within p B"
      using that by auto
    moreover have "proots_within (([:- b, 1:] * p) ∘_p q) A = proots_within (p ∘_p q) A"
      using that unfolding pcompose_mult proots_within_times
      apply (auto simp add: poly_pcompose)
      using bij bij_betwE by blast
    ultimately show ?thesis using root.hyps[OF ‹p≠0›] by auto
  qed
  moreover have ?case when "b∈B" "poly p b≠0"
  proof -
    define bb where "bb=[:- b, 1:]"
    have "card (proots_within (bb * p) B) = card {b} + card (proots_within p B)"
    proof -
      have "proots_within bb B = {b}" 
        using that unfolding bb_def by auto
      then show ?thesis unfolding proots_within_times
        apply (subst card_Un_disjoint)
        by (use that in auto)
    qed
    also have "... = 1 + card (proots_within (p ∘_p q) A)"
      using root.hyps by simp
    also have "... = card (proots_within ((bb * p) ∘_p q) A)"
      unfolding proots_within_times pcompose_mult
    proof (subst card_Un_disjoint) 
      obtain a where "b=poly q a" "a∈A" 
        by (metis ‹b ∈ B› bij bij_betwE bij_betw_the_inv_into f_the_inv_into_f_bij_betw)
      define bbq pq where "bbq=bb ∘_p q" and "pq=p ∘_p q"
      have bbq_0:"poly bbq a=0" and bbq_deg: "degree bbq≤1" and "bbq≠0"
        unfolding bbq_def bb_def poly_pcompose
        subgoal using ‹b=poly q a› by auto
        subgoal using q_deg by (simp add: degree_add_le degree_pcompose)
        subgoal using pcompose_eq_0 q_deg by fastforce
        done
      show "finite (proots_within bbq A)" using ‹bbq≠0› by simp
      show "finite (proots_within pq A)" unfolding pq_def 
        by (metis ‹p ≠ 0› finite_proots pcompose_eq_0 q_deg zero_less_one) 
      have bbq_a:"proots_within bbq A = {a}"
      proof -
        have "a∈proots_within bbq A" 
          unfolding bb_def proots_within_def poly_pcompose bbq_def 
          using ‹b=poly q a› ‹a∈A› by simp
        moreover have "card (proots_within bbq A) = 1" 
        proof -
          have "card (proots_within bbq A) ≠0" 
            using ‹a∈proots_within bbq A› ‹finite (proots_within bbq A)›
            by auto
          moreover have "card (proots_within bbq A) ≤ 1" 
            by (meson ‹bbq ≠ 0› card_proots_within_leq le_trans proots_count_leq_degree bbq_deg)
          ultimately show ?thesis by auto
        qed
        ultimately show ?thesis by (metis card_1_singletonE singletonD)
      qed
      show "proots_within (bbq) A ∩ proots_within (pq) A = {}" 
        using bbq_a ‹b = poly q a› that(2) unfolding pq_def by (simp add:poly_pcompose)
      show "1 + card (proots_within pq A) = card (proots_within bbq A) + card (proots_within pq A)"
        using bbq_a by simp
    qed
    finally show ?thesis unfolding bb_def .
  qed
  ultimately show ?case by auto
qed

end