Theory Sturm_Tarski.PolyMisc

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

section ‹Misc polynomial lemmas for the Sturm--Tarski theorem›

theory PolyMisc imports
  "HOL-Computational_Algebra.Polynomial_Factorial"
begin
  
lemma coprime_poly_0:
  "poly p x  0  poly q x  0" if "coprime p q"
  for x :: "'a :: field"
proof (rule ccontr)
  assume " ¬ (poly p x  0  poly q x  0)"
  then have "[:-x, 1:] dvd p" "[:-x, 1:] dvd q"
    by (simp_all add: poly_eq_0_iff_dvd)
  with that have "is_unit [:-x, 1:]"
    by (rule coprime_common_divisor)
  then show False
    by (auto simp add: is_unit_pCons_iff)
qed

lemma smult_cancel:
  fixes p::"'a::idom poly"
  assumes "c0" and smult: "smult c p = smult c q" 
  shows "p=q" 
proof -
  have "smult c (p-q)=0" using smult by (metis diff_self smult_diff_right)
  thus ?thesis using c0 by auto
qed

lemma dvd_monic:
  fixes p q:: "'a :: idom poly" 
  assumes monic:"lead_coeff p=1" and "p dvd (smult c q)" and "c0"
  shows "p dvd q" using assms
proof (cases "q=0  degree p=0")
  case True
  thus ?thesis using assms
    by (auto elim!: degree_eq_zeroE simp add: const_poly_dvd_iff)
next
  case False
  hence "q0" and "degree p0" by auto
  obtain k where k:"smult c q = p*k" using assms dvd_def by metis
  hence "k0" by (metis False assms(3) mult_zero_right smult_eq_0_iff)
  hence deg_eq:"degree q=degree p + degree k"
    by (metis False assms(3) degree_0 degree_mult_eq degree_smult_eq k)
  have c_dvd:"ndegree k. c dvd coeff k (degree k - n)" 
  proof (rule,rule)
    fix n assume "n  degree k "
    thus "c dvd coeff k (degree k - n)"
    proof (induct n rule:nat_less_induct) 
      case (1 n) 
      define T where "T(λi. coeff p i * coeff k (degree p+degree k - n - i))"
      have "c * coeff q (degree q - n) = (idegree q - n. coeff p i * coeff k (degree q - n - i))"
        using coeff_mult[of p k "degree q - n"] k coeff_smult[of c q "degree q -n"] by auto
      also have "...=(idegree p+degree k - n. T i)"
        using deg_eq unfolding T_def by auto 
      also have "...=(i{0..<degree p}. T i) + sum T {(degree p)}+ 
                  sum T {degree p + 1..degree p + degree k - n}" 
      proof -
        define C where "C{{0..<degree p}, {degree p},{degree p+1..degree p+degree k-n}}"
        have "AC. finite A" unfolding C_def by auto
        moreover have "AC. BC. A  B  A  B = {}"
          unfolding C_def by auto
        ultimately have "sum T (C) = sum (sum T) C" 
          using sum.Union_disjoint by auto
        moreover have "C={..degree p + degree k - n}" 
          using n  degree k unfolding C_def by auto
        moreover have  "sum (sum T) C= sum T {0..<degree p} + sum T {(degree p)} + 
                  sum T {degree p + 1..degree p + degree k - n}"
        proof -
          have "{0..<degree p}{degree p}" 
            by (metis atLeast0LessThan insertI1 lessThan_iff less_imp_not_eq)  
          moreover have "{degree p}{degree p + 1..degree p + degree k - n}" 
            by (metis add.commute add_diff_cancel_right' atLeastAtMost_singleton_iff 
                  diff_self_eq_0 eq_imp_le not_one_le_zero)
          moreover have "{0..<degree p}{degree p + 1..degree p + degree k - n}" 
            using degree kn degree p0 by fastforce
          ultimately show ?thesis unfolding C_def by auto
        qed
        ultimately show ?thesis by auto
      qed
      also have "...=(i{0..<degree p}. T i) +  coeff k (degree k - n)"
      proof -
        have "x{degree p + 1..degree p + degree k - n}. T x=0" 
          using coeff_eq_0[of p] unfolding T_def by simp
        hence "sum T {degree p + 1..degree p + degree k - n}=0" by auto
        moreover have "T (degree p)=coeff k (degree k - n)"
          using monic by (simp add: T_def)
        ultimately show ?thesis by auto
      qed
      finally have c_coeff: "c * coeff q (degree q - n) = sum T {0..<degree p} 
              + coeff k (degree k - n)" .
      moreover have "n0c dvd sum T {0..<degree p}" 
      proof (rule dvd_sum)
        fix i assume i:"i  {0..<degree p}" and "n0"
        hence "(n+i-degree p)degree k" using n  degree k by auto
        moreover have "n + i - degree p <n" using i n0 by auto 
        ultimately have "c dvd coeff k (degree k - (n+i-degree p))"
          using 1(1) by auto
        hence "c dvd coeff k (degree p + degree k - n - i)"
          by (metis add_diff_cancel_left' deg_eq diff_diff_left dvd_0_right le_degree 
                  le_diff_conv add.commute ordered_cancel_comm_monoid_diff_class.diff_diff_right)
        thus "c dvd T i" unfolding T_def by auto
      qed
      moreover have "n=0 ?case"
      proof -
        assume "n=0"
        hence "i{0..<degree p}. coeff k (degree p + degree k - n - i) =0" 
          using coeff_eq_0[of k] by simp
        hence "c * coeff q (degree q - n) = coeff k (degree k - n)"
          using c_coeff unfolding T_def by auto
        thus ?thesis by (metis dvdI)
      qed
      ultimately show ?case by (metis dvd_add_right_iff dvd_triv_left)
    qed
  qed
  hence "n. c dvd coeff k n"
    by (metis diff_diff_cancel dvd_0_right le_add2 le_add_diff_inverse le_degree)
  then obtain f where f:"n. c * f n=coeff k n" unfolding dvd_def by metis
  have "  n. f n = 0 "  
    by (metis (mono_tags, lifting) MOST_coeff_eq_0 MOST_mono assms(3) f mult_eq_0_iff)
  hence "smult c (Abs_poly f)=k" 
    using f smult.abs_eq[of c "Abs_poly f"] Abs_poly_inverse[of f] coeff_inverse[of k]
    by simp
  hence "q=p* Abs_poly f" using k c0 smult_cancel by auto
  thus ?thesis unfolding dvd_def by auto
qed

lemma poly_power_n_eq:
  fixes x::"'a :: idom"
  assumes "n0"
  shows "poly ([:-a,1:]^n) x=0  (x=a)" using assms 
by (induct n,auto)

lemma poly_power_n_odd:
  fixes x a:: real
  assumes "odd n"
  shows "poly ([:-a,1:]^n) x>0  (x>a)" using assms 
proof -
  have "poly ([:-a,1:]^n) x0 = (poly [:- a, 1:] x 0)" 
    unfolding poly_power using zero_le_odd_power[OF odd n] by blast
  also have "(poly [:- a, 1:] x 0) = (xa)" by fastforce
  finally have "poly ([:-a,1:]^n) x0 = (xa)" .
  moreover have "poly ([:-a,1:]^n) x=0 = (x=a)" by(rule poly_power_n_eq, metis assms even_zero)    
  ultimately show ?thesis by linarith
qed

lemma gcd_coprime_poly:
  fixes p q::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
  assumes nz: "p  0  q  0" and p': "p = p' * gcd p q" and
    q': "q = q' * gcd p q"
  shows "coprime p' q'" 
using gcd_coprime nz p' q' by auto

lemma poly_mod:
  "poly (p mod q) x = poly p x" if "poly q x = 0"
proof -
  from that have "poly (p mod q) x = poly (p div q * q) x + poly (p mod q) x"
    by simp
  also have " = poly p x"
    by (simp only: poly_add [symmetric]) simp
  finally show ?thesis .
qed

lemma pseudo_divmod_0[simp]: "pseudo_divmod f 0 = (0,f)"
  unfolding pseudo_divmod_def by auto

lemma map_poly_eq_iff:
  assumes "f 0=0" "inj f"
  shows "map_poly f x =map_poly f y  x=y" 
  using assms
  by (auto simp: poly_eq_iff coeff_map_poly dest:injD)
      
lemma pseudo_mod_0[simp]:
  shows "pseudo_mod p 0= p" "pseudo_mod 0 q = 0"
  unfolding pseudo_mod_def pseudo_divmod_def by (auto simp add: length_coeffs_degree)

lemma pseudo_mod_mod:
  assumes "g0"
  shows "smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g"
proof -
  define a where "a=lead_coeff g ^ (Suc (degree f) - degree g)"
  have "a0" unfolding a_def by (simp add: assms)  
  define r where "r = pseudo_mod f g" 
  define r' where "r' = pseudo_mod (smult (1/a) f) g"
  obtain q where pdm: "pseudo_divmod f g = (q,r)" using r_def[unfolded pseudo_mod_def]
    apply (cases "pseudo_divmod f g")
    by auto
  obtain q' where pdm': "pseudo_divmod (smult (1/a) f) g = (q',r')" using r'_def[unfolded pseudo_mod_def] 
    apply (cases "pseudo_divmod (smult (1/a) f) g")
    by auto
  have "smult a f = q * g + r" and deg_r:"r = 0  degree r < degree g"
    using pseudo_divmod[OF assms pdm] unfolding a_def by auto
  moreover have "f = q' * g + r'" and deg_r':"r' = 0  degree r' < degree g"
    using a0  pseudo_divmod[OF assms pdm'] unfolding a_def degree_smult_eq 
    by auto  
  ultimately have gr:"(smult a q' - q) * g =  r - smult a r'" 
    by (auto simp add:smult_add_right algebra_simps)
  have "smult a r' = r" when "r=0" "r'=0"
    using that by auto
  moreover have "smult a r' = r" when "r0  r'0"
  proof -
    have "smult a q' - q =0"
    proof (rule ccontr)
      assume asm:"smult a q' - q  0 "
      have "degree (r - smult a r') < degree g"
        using deg_r deg_r' degree_diff_less that by force
      also have "...  degree (( smult a q' - q)*g)"
        using degree_mult_right_le[OF asm,of g] by (simp add: mult.commute) 
      also have "... = degree (r - smult a r')"
        using gr by auto
      finally have "degree (r - smult a r') < degree (r - smult a r')" .
      then show False by simp
    qed
    then show ?thesis using gr by auto
  qed
  ultimately have "smult a r' = r" by argo
  then show ?thesis unfolding r_def r'_def a_def mod_poly_def 
    using assms by (auto simp add:field_simps)
qed    
    
lemma poly_pseudo_mod:
  assumes "poly q x=0" "q0"
  shows "poly (pseudo_mod p q) x = (lead_coeff q ^ (Suc (degree p) - degree q)) * poly p x"
proof -
  define a where "a=coeff q (degree q) ^ (Suc (degree p) - degree q)"
  obtain f r where fr:"pseudo_divmod p q = (f, r)" by fastforce
  then have "smult a p = q * f + r" "r = 0  degree r < degree q"
    using pseudo_divmod[OF q0] unfolding a_def by auto
  then have "poly (q*f+r) x = poly (smult a p) x" by auto    
  then show ?thesis
    using assms(1) fr unfolding pseudo_mod_def a_def
    by auto
qed  

lemma degree_less_timesD:
  fixes q::"'a::idom poly"
  assumes "q*g=r" and deg:"r=0  degree g>degree r" and "g0"
  shows "q=0  r=0"
proof -
  have ?thesis when "r=0"
    using assms(1) assms(3) no_zero_divisors that by blast    
  moreover have False when "r0"
  proof -
    have "degree r < degree g"
      using deg that by auto
    also have "...  degree (q*g)"
      by (metis assms(1) degree_mult_right_le mult.commute mult_not_zero that)
    also have "... = degree r"
      using assms(1) by simp
    finally have "degree r<degree r" .
    then show False by auto
  qed
  ultimately show ?thesis by auto
qed

end