(* 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 "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