(* Title: HOL/Library/Poly_Deriv.thy Author: Amine Chaieb Author: Brian Huffman *) section‹Polynomials and Differentiation› theory Poly_Deriv imports Deriv Polynomial begin subsection ‹Derivatives of univariate polynomials› function pderiv :: "('a :: semidom) poly ⇒ 'a poly" where [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))" by (auto intro: pCons_cases) termination pderiv by (relation "measure degree") simp_all lemma pderiv_0 [simp]: "pderiv 0 = 0" using pderiv.simps [of 0 0] by simp lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)" by (simp add: pderiv.simps) lemma pderiv_1 [simp]: "pderiv 1 = 0" unfolding one_poly_def by (simp add: pderiv_pCons) lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0" and pderiv_numeral [simp]: "pderiv (numeral m) = 0" by (simp_all add: of_nat_poly numeral_poly pderiv_pCons) lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)" by (induct p arbitrary: n) (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split) fun pderiv_coeffs_code :: "('a :: semidom) ⇒ 'a list ⇒ 'a list" where "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)" | "pderiv_coeffs_code f [] = []" definition pderiv_coeffs :: "('a :: semidom) list ⇒ 'a list" where "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)" (* Efficient code for pderiv contributed by RenĂ© Thiemann and Akihisa Yamada *) lemma pderiv_coeffs_code: "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * (nth_default 0 xs n)" proof (induct xs arbitrary: f n) case (Cons x xs f n) show ?case proof (cases n) case 0 thus ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] ∧ f * x = 0", auto simp: cCons_def) next case (Suc m) note n = this show ?thesis proof (cases "pderiv_coeffs_code (f + 1) xs = [] ∧ f * x = 0") case False hence "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" by (auto simp: cCons_def n) also have "… = (f + of_nat n) * (nth_default 0 xs m)" unfolding Cons by (simp add: n add_ac) finally show ?thesis by (simp add: n) next case True { fix g have "pderiv_coeffs_code g xs = [] ⟹ g + of_nat m = 0 ∨ nth_default 0 xs m = 0" proof (induct xs arbitrary: g m) case (Cons x xs g) from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []" and g: "(g = 0 ∨ x = 0)" by (auto simp: cCons_def split: if_splits) note IH = Cons(1)[OF empty] from IH[of m] IH[of "m - 1"] g show ?case by (cases m, auto simp: field_simps) qed simp } note empty = this from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0" by (auto simp: cCons_def n) moreover have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" using True by (simp add: n, insert empty[of "f+1"], auto simp: field_simps) ultimately show ?thesis by simp qed qed qed simp lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (λ i. f (Suc i)) [0 ..< n]" by (induct n arbitrary: f, auto) lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases) case (1 n) have id: "coeff p (Suc n) = nth_default 0 (map (λi. coeff p (Suc i)) [0..<degree p]) n" by (cases "n < degree p", auto simp: nth_default_def coeff_eq_0) show ?case unfolding coeffs_def map_upt_Suc by (auto simp: id) next case 2 obtain n xs where id: "tl (coeffs p) = xs" "(1 :: 'a) = n" by auto from 2 show ?case unfolding id by (induct xs arbitrary: n, auto simp: cCons_def) qed context assumes "SORT_CONSTRAINT('a::{semidom, semiring_char_0})" begin lemma pderiv_eq_0_iff: "pderiv (p :: 'a poly) = 0 ⟷ degree p = 0" apply (rule iffI) apply (cases p, simp) apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc) apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0) done lemma degree_pderiv: "degree (pderiv (p :: 'a poly)) = degree p - 1" apply (rule order_antisym [OF degree_le]) apply (simp add: coeff_pderiv coeff_eq_0) apply (cases "degree p", simp) apply (rule le_degree) apply (simp add: coeff_pderiv del: of_nat_Suc) apply (metis degree_0 leading_coeff_0_iff nat.distinct(1)) done lemma not_dvd_pderiv: assumes "degree (p :: 'a poly) ≠ 0" shows "¬ p dvd pderiv p" proof assume dvd: "p dvd pderiv p" then obtain q where p: "pderiv p = p * q" unfolding dvd_def by auto from dvd have le: "degree p ≤ degree (pderiv p)" by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff) from this[unfolded degree_pderiv] assms show False by auto qed lemma dvd_pderiv_iff [simp]: "(p :: 'a poly) dvd pderiv p ⟷ degree p = 0" using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric]) end lemma pderiv_singleton [simp]: "pderiv [:a:] = 0" by (simp add: pderiv_pCons) lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q" by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p" by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q" by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)" by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p" by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps) lemma pderiv_power_Suc: "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p" apply (induct n) apply simp apply (subst power_Suc) apply (subst pderiv_mult) apply (erule ssubst) apply (simp only: of_nat_Suc smult_add_left smult_1_left) apply (simp add: algebra_simps) done lemma pderiv_setprod: "pderiv (setprod f (as)) = (∑a ∈ as. setprod f (as - {a}) * pderiv (f a))" proof (induct as rule: infinite_finite_induct) case (insert a as) hence id: "setprod f (insert a as) = f a * setprod f as" "⋀ g. setsum g (insert a as) = g a + setsum g as" "insert a as - {a} = as" by auto { fix b assume "b ∈ as" hence id2: "insert a as - {b} = insert a (as - {b})" using ‹a ∉ as› by auto have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})" unfolding id2 by (subst setprod.insert, insert insert, auto) } note id2 = this show ?case unfolding id pderiv_mult insert(3) setsum_right_distrib by (auto simp add: ac_simps id2 intro!: setsum.cong) qed auto lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)" by (rule DERIV_cong, rule DERIV_pow, simp) declare DERIV_pow2 [simp] DERIV_pow [simp] lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: 'a::real_normed_field) x :> D" by (rule DERIV_cong, rule DERIV_add, auto) lemma poly_DERIV [simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons) lemma continuous_on_poly [continuous_intros]: fixes p :: "'a :: {real_normed_field} poly" assumes "continuous_on A f" shows "continuous_on A (λx. poly p (f x))" proof - have "continuous_on A (λx. (∑i≤degree p. (f x) ^ i * coeff p i))" by (intro continuous_intros assms) also have "… = (λx. poly p (f x))" by (intro ext) (simp add: poly_altdef mult_ac) finally show ?thesis . qed text‹Consequences of the derivative theorem above› lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)" apply (simp add: real_differentiable_def) apply (blast intro: poly_DERIV) done lemma poly_isCont[simp]: "isCont (%x. poly p x) (x::real)" by (rule poly_DERIV [THEN DERIV_isCont]) lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |] ==> ∃x. a < x & x < b & (poly p x = 0)" using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less) lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |] ==> ∃x. a < x & x < b & (poly p x = 0)" by (insert poly_IVT_pos [where p = "- p" ]) simp lemma poly_IVT: fixes p::"real poly" assumes "a<b" and "poly p a * poly p b < 0" shows "∃x>a. x < b ∧ poly p x = 0" by (metis assms(1) assms(2) less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos) lemma poly_MVT: "(a::real) < b ==> ∃x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)" using MVT [of a b "poly p"] apply auto apply (rule_tac x = z in exI) apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique]) done lemma poly_MVT': assumes "{min a b..max a b} ⊆ A" shows "∃x∈A. poly p b - poly p a = (b - a) * poly (pderiv p) (x::real)" proof (cases a b rule: linorder_cases) case less from poly_MVT[OF less, of p] guess x by (elim exE conjE) thus ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms]) next case greater from poly_MVT[OF greater, of p] guess x by (elim exE conjE) thus ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms]) qed (insert assms, auto) lemma poly_pinfty_gt_lc: fixes p:: "real poly" assumes "lead_coeff p > 0" shows "∃ n. ∀ x ≥ n. poly p x ≥ lead_coeff p" using assms proof (induct p) case 0 thus ?case by auto next case (pCons a p) have "⟦a≠0;p=0⟧ ⟹ ?case" by auto moreover have "p≠0 ⟹ ?case" proof - assume "p≠0" then obtain n1 where gte_lcoeff:"∀x≥n1. lead_coeff p ≤ poly p x" using that pCons by auto have gt_0:"lead_coeff p >0" using pCons(3) ‹p≠0› by auto def n≡"max n1 (1+ ¦a¦/(lead_coeff p))" show ?thesis proof (rule_tac x=n in exI,rule,rule) fix x assume "n ≤ x" hence "lead_coeff p ≤ poly p x" using gte_lcoeff unfolding n_def by auto hence " ¦a¦/(lead_coeff p) ≥ ¦a¦/(poly p x)" and "poly p x>0" using gt_0 by (intro frac_le,auto) hence "x≥1+ ¦a¦/(poly p x)" using ‹n≤x›[unfolded n_def] by auto thus "lead_coeff (pCons a p) ≤ poly (pCons a p) x" using ‹lead_coeff p ≤ poly p x› ‹poly p x>0› ‹p≠0› by (auto simp add:field_simps) qed qed ultimately show ?case by fastforce qed subsection ‹Algebraic numbers› text ‹ Algebraic numbers can be defined in two equivalent ways: all real numbers that are roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry uses the rational definition, but we need the integer definition. The equivalence is obvious since any rational polynomial can be multiplied with the LCM of its coefficients, yielding an integer polynomial with the same roots. › subsection ‹Algebraic numbers› definition algebraic :: "'a :: field_char_0 ⇒ bool" where "algebraic x ⟷ (∃p. (∀i. coeff p i ∈ ℤ) ∧ p ≠ 0 ∧ poly p x = 0)" lemma algebraicI: assumes "⋀i. coeff p i ∈ ℤ" "p ≠ 0" "poly p x = 0" shows "algebraic x" using assms unfolding algebraic_def by blast lemma algebraicE: assumes "algebraic x" obtains p where "⋀i. coeff p i ∈ ℤ" "p ≠ 0" "poly p x = 0" using assms unfolding algebraic_def by blast lemma quotient_of_denom_pos': "snd (quotient_of x) > 0" using quotient_of_denom_pos[OF surjective_pairing] . lemma of_int_div_in_Ints: "b dvd a ⟹ of_int a div of_int b ∈ (ℤ :: 'a :: ring_div set)" proof (cases "of_int b = (0 :: 'a)") assume "b dvd a" "of_int b ≠ (0::'a)" then obtain c where "a = b * c" by (elim dvdE) with ‹of_int b ≠ (0::'a)› show ?thesis by simp qed auto lemma of_int_divide_in_Ints: "b dvd a ⟹ of_int a / of_int b ∈ (ℤ :: 'a :: field set)" proof (cases "of_int b = (0 :: 'a)") assume "b dvd a" "of_int b ≠ (0::'a)" then obtain c where "a = b * c" by (elim dvdE) with ‹of_int b ≠ (0::'a)› show ?thesis by simp qed auto lemma algebraic_altdef: fixes p :: "'a :: field_char_0 poly" shows "algebraic x ⟷ (∃p. (∀i. coeff p i ∈ ℚ) ∧ p ≠ 0 ∧ poly p x = 0)" proof safe fix p assume rat: "∀i. coeff p i ∈ ℚ" and root: "poly p x = 0" and nz: "p ≠ 0" def cs ≡ "coeffs p" from rat have "∀c∈range (coeff p). ∃c'. c = of_rat c'" unfolding Rats_def by blast then obtain f where f: "⋀i. coeff p i = of_rat (f (coeff p i))" by (subst (asm) bchoice_iff) blast def cs' ≡ "map (quotient_of ∘ f) (coeffs p)" def d ≡ "Lcm (set (map snd cs'))" def p' ≡ "smult (of_int d) p" have "∀n. coeff p' n ∈ ℤ" proof fix n :: nat show "coeff p' n ∈ ℤ" proof (cases "n ≤ degree p") case True def c ≡ "coeff p n" def a ≡ "fst (quotient_of (f (coeff p n)))" and b ≡ "snd (quotient_of (f (coeff p n)))" have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp have "coeff p' n = of_int d * coeff p n" by (simp add: p'_def) also have "coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def by (subst quotient_of_div [of "f (coeff p n)", symmetric]) (simp_all add: f [symmetric]) also have "of_int d * … = of_rat (of_int (a*d) / of_int b)" by (simp add: of_rat_mult of_rat_divide) also from nz True have "b ∈ snd ` set cs'" unfolding cs'_def by (force simp: o_def b_def coeffs_def simp del: upt_Suc) hence "b dvd (a * d)" unfolding d_def by simp hence "of_int (a * d) / of_int b ∈ (ℤ :: rat set)" by (rule of_int_divide_in_Ints) hence "of_rat (of_int (a * d) / of_int b) ∈ ℤ" by (elim Ints_cases) auto finally show ?thesis . qed (auto simp: p'_def not_le coeff_eq_0) qed moreover have "set (map snd cs') ⊆ {0<..}" unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) hence "d ≠ 0" unfolding d_def by (induction cs') simp_all with nz have "p' ≠ 0" by (simp add: p'_def) moreover from root have "poly p' x = 0" by (simp add: p'_def) ultimately show "algebraic x" unfolding algebraic_def by blast next assume "algebraic x" then obtain p where p: "⋀i. coeff p i ∈ ℤ" "poly p x = 0" "p ≠ 0" by (force simp: algebraic_def) moreover have "coeff p i ∈ ℤ ⟹ coeff p i ∈ ℚ" for i by (elim Ints_cases) simp ultimately show "(∃p. (∀i. coeff p i ∈ ℚ) ∧ p ≠ 0 ∧ poly p x = 0)" by auto qed text‹Lemmas for Derivatives› lemma order_unique_lemma: fixes p :: "'a::idom poly" assumes "[:-a, 1:] ^ n dvd p" "¬ [:-a, 1:] ^ Suc n dvd p" shows "n = order a p" unfolding Polynomial.order_def apply (rule Least_equality [symmetric]) apply (fact assms) apply (rule classical) apply (erule notE) unfolding not_less_eq_eq using assms(1) apply (rule power_le_dvd) apply assumption done lemma lemma_order_pderiv1: "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q + smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)" apply (simp only: pderiv_mult pderiv_power_Suc) apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons) done lemma lemma_order_pderiv: fixes p :: "'a :: field_char_0 poly" assumes n: "0 < n" and pd: "pderiv p ≠ 0" and pe: "p = [:- a, 1:] ^ n * q" and nd: "~ [:- a, 1:] dvd q" shows "n = Suc (order a (pderiv p))" using n proof - have "pderiv ([:- a, 1:] ^ n * q) ≠ 0" using assms by auto obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) ≠ 0" using assms by (cases n) auto have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l ⟹ k dvd l" by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff) have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" proof (rule order_unique_lemma) show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)" apply (subst lemma_order_pderiv1) apply (rule dvd_add) apply (metis dvdI dvd_mult2 power_Suc2) apply (metis dvd_smult dvd_triv_right) done next show "¬ [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)" apply (subst lemma_order_pderiv1) by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one) qed then show ?thesis by (metis ‹n = Suc n'› pe) qed lemma order_decomp: assumes "p ≠ 0" shows "∃q. p = [:- a, 1:] ^ order a p * q ∧ ¬ [:- a, 1:] dvd q" proof - from assms have A: "[:- a, 1:] ^ order a p dvd p" and B: "¬ [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order) from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" .. with B have "¬ [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q" by simp then have "¬ [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q" by simp then have D: "¬ [:- a, 1:] dvd q" using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q] by auto from C D show ?thesis by blast qed lemma order_pderiv: "⟦pderiv p ≠ 0; order a (p :: 'a :: field_char_0 poly) ≠ 0⟧ ⟹ (order a p = Suc (order a (pderiv p)))" apply (case_tac "p = 0", simp) apply (drule_tac a = a and p = p in order_decomp) using neq0_conv apply (blast intro: lemma_order_pderiv) done lemma order_mult: "p * q ≠ 0 ⟹ order a (p * q) = order a p + order a q" proof - def i ≡ "order a p" def j ≡ "order a q" def t ≡ "[:-a, 1:]" have t_dvd_iff: "⋀u. t dvd u ⟷ poly u a = 0" unfolding t_def by (simp add: dvd_iff_poly_eq_0) assume "p * q ≠ 0" then show "order a (p * q) = i + j" apply clarsimp apply (drule order [where a=a and p=p, folded i_def t_def]) apply (drule order [where a=a and p=q, folded j_def t_def]) apply clarify apply (erule dvdE)+ apply (rule order_unique_lemma [symmetric], fold t_def) apply (simp_all add: power_add t_dvd_iff) done qed lemma order_smult: assumes "c ≠ 0" shows "order x (smult c p) = order x p" proof (cases "p = 0") case False have "smult c p = [:c:] * p" by simp also from assms False have "order x … = order x [:c:] + order x p" by (subst order_mult) simp_all also from assms have "order x [:c:] = 0" by (intro order_0I) auto finally show ?thesis by simp qed simp (* Next two lemmas contributed by Wenda Li *) lemma order_1_eq_0 [simp]:"order x 1 = 0" by (metis order_root poly_1 zero_neq_one) lemma order_power_n_n: "order a ([:-a,1:]^n)=n" proof (induct n) (*might be proved more concisely using nat_less_induct*) case 0 thus ?case by (metis order_root poly_1 power_0 zero_neq_one) next case (Suc n) have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right) moreover have "order a [:-a,1:]=1" unfolding order_def proof (rule Least_equality,rule ccontr) assume "¬ ¬ [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp hence "degree ([:- a, 1:] ^ Suc 1) ≤ degree ([:- a, 1:] )" by (rule dvd_imp_degree_le,auto) thus False by auto next fix y assume asm:"¬ [:- a, 1:] ^ Suc y dvd [:- a, 1:]" show "1 ≤ y" proof (rule ccontr) assume "¬ 1 ≤ y" hence "y=0" by auto hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto thus False using asm by auto qed qed ultimately show ?case using Suc by auto qed text‹Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').› lemma order_divides: "[:-a, 1:] ^ n dvd p ⟷ p = 0 ∨ n ≤ order a p" apply (cases "p = 0", auto) apply (drule order_2 [where a=a and p=p]) apply (metis not_less_eq_eq power_le_dvd) apply (erule power_le_dvd [OF order_1]) done lemma poly_squarefree_decomp_order: assumes "pderiv (p :: 'a :: field_char_0 poly) ≠ 0" and p: "p = q * d" and p': "pderiv p = e * d" and d: "d = r * p + s * pderiv p" shows "order a q = (if order a p = 0 then 0 else 1)" proof (rule classical) assume 1: "order a q ≠ (if order a p = 0 then 0 else 1)" from ‹pderiv p ≠ 0› have "p ≠ 0" by auto with p have "order a p = order a q + order a d" by (simp add: order_mult) with 1 have "order a p ≠ 0" by (auto split: if_splits) have "order a (pderiv p) = order a e + order a d" using ‹pderiv p ≠ 0› ‹pderiv p = e * d› by (simp add: order_mult) have "order a p = Suc (order a (pderiv p))" using ‹pderiv p ≠ 0› ‹order a p ≠ 0› by (rule order_pderiv) have "d ≠ 0" using ‹p ≠ 0› ‹p = q * d› by simp have "([:-a, 1:] ^ (order a (pderiv p))) dvd d" apply (simp add: d) apply (rule dvd_add) apply (rule dvd_mult) apply (simp add: order_divides ‹p ≠ 0› ‹order a p = Suc (order a (pderiv p))›) apply (rule dvd_mult) apply (simp add: order_divides) done then have "order a (pderiv p) ≤ order a d" using ‹d ≠ 0› by (simp add: order_divides) show ?thesis using ‹order a p = order a q + order a d› using ‹order a (pderiv p) = order a e + order a d› using ‹order a p = Suc (order a (pderiv p))› using ‹order a (pderiv p) ≤ order a d› by auto qed lemma poly_squarefree_decomp_order2: "⟦pderiv p ≠ (0 :: 'a :: field_char_0 poly); p = q * d; pderiv p = e * d; d = r * p + s * pderiv p ⟧ ⟹ ∀a. order a q = (if order a p = 0 then 0 else 1)" by (blast intro: poly_squarefree_decomp_order) lemma order_pderiv2: "⟦pderiv p ≠ 0; order a (p :: 'a :: field_char_0 poly) ≠ 0⟧ ⟹ (order a (pderiv p) = n) = (order a p = Suc n)" by (auto dest: order_pderiv) definition rsquarefree :: "'a::idom poly => bool" where "rsquarefree p = (p ≠ 0 & (∀a. (order a p = 0) | (order a p = 1)))" lemma pderiv_iszero: "pderiv p = 0 ⟹ ∃h. p = [:h :: 'a :: {semidom,semiring_char_0}:]" apply (simp add: pderiv_eq_0_iff) apply (case_tac p, auto split: if_splits) done lemma rsquarefree_roots: fixes p :: "'a :: field_char_0 poly" shows "rsquarefree p = (∀a. ¬(poly p a = 0 ∧ poly (pderiv p) a = 0))" apply (simp add: rsquarefree_def) apply (case_tac "p = 0", simp, simp) apply (case_tac "pderiv p = 0") apply simp apply (drule pderiv_iszero, clarsimp) apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree) apply (force simp add: order_root order_pderiv2) done lemma poly_squarefree_decomp: assumes "pderiv (p :: 'a :: field_char_0 poly) ≠ 0" and "p = q * d" and "pderiv p = e * d" and "d = r * p + s * pderiv p" shows "rsquarefree q & (∀a. (poly q a = 0) = (poly p a = 0))" proof - from ‹pderiv p ≠ 0› have "p ≠ 0" by auto with ‹p = q * d› have "q ≠ 0" by simp have "∀a. order a q = (if order a p = 0 then 0 else 1)" using assms by (rule poly_squarefree_decomp_order2) with ‹p ≠ 0› ‹q ≠ 0› show ?thesis by (simp add: rsquarefree_def order_root) qed end