Theory PolyMisc
section ‹Misc polynomial lemmas for the Sturm--Tarski theorem›
theory PolyMisc imports
"HOL-Computational_Algebra.Polynomial_Factorial"
begin
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 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 r"
by (metis assms(1) degree_mult_right_le mult.commute mult_zero_right that)
finally have "degree r<degree r" .
then show False ..
qed
ultimately show ?thesis by auto
qed
end