Theory PolyMisc
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 "c≠0" 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 ‹c≠0› 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 "c≠0"
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 "q≠0" and "degree p≠0" by auto
obtain k where k:"smult c q = p*k" using assms dvd_def by metis
hence "k≠0" 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:"∀n≤degree 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) = (∑i≤degree 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 "...=(∑i≤degree 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 "∀A∈C. finite A" unfolding C_def by auto
moreover have "∀A∈C. ∀B∈C. 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 k≥n› ‹degree p≠0› 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 "n≠0⟹c dvd sum T {0..<degree p}"
proof (rule dvd_sum)
fix i assume i:"i ∈ {0..<degree p}" and "n≠0"
hence "(n+i-degree p)≤degree k" using ‹n ≤ degree k› by auto
moreover have "n + i - degree p <n" using i ‹n≠0› 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 ‹c≠0› smult_cancel by auto
thus ?thesis unfolding dvd_def by auto
qed
lemma poly_power_n_eq:
fixes x::"'a :: idom"
assumes "n≠0"
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) x≥0 = (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) = (x≥a)" by fastforce
finally have "poly ([:-a,1:]^n) x≥0 = (x≥a)" .
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 "g≠0"
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 "a≠0" 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 ‹a≠0› 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 "r≠0 ∨ 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" "q≠0"
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 ‹q≠0›] 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 "g≠0"
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 "r≠0"
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