src/HOL/Library/Poly_Deriv.thy
 author eberlm Mon Jan 11 16:38:39 2016 +0100 (2016-01-11) changeset 62128 3201ddb00097 parent 62072 bf3d9f113474 child 62175 8ffc4d0e652d permissions -rw-r--r--
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
 wenzelm@41959 ` 1` ```(* Title: HOL/Library/Poly_Deriv.thy ``` huffman@29985 ` 2` ``` Author: Amine Chaieb ``` wenzelm@41959 ` 3` ``` Author: Brian Huffman ``` huffman@29985 ` 4` ```*) ``` huffman@29985 ` 5` wenzelm@60500 ` 6` ```section\Polynomials and Differentiation\ ``` huffman@29985 ` 7` huffman@29985 ` 8` ```theory Poly_Deriv ``` huffman@29985 ` 9` ```imports Deriv Polynomial ``` huffman@29985 ` 10` ```begin ``` huffman@29985 ` 11` wenzelm@60500 ` 12` ```subsection \Derivatives of univariate polynomials\ ``` huffman@29985 ` 13` eberlm@62128 ` 14` ```function pderiv :: "('a :: semidom) poly \ 'a poly" ``` haftmann@52380 ` 15` ```where ``` haftmann@52380 ` 16` ``` [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))" ``` haftmann@52380 ` 17` ``` by (auto intro: pCons_cases) ``` haftmann@52380 ` 18` haftmann@52380 ` 19` ```termination pderiv ``` haftmann@52380 ` 20` ``` by (relation "measure degree") simp_all ``` huffman@29985 ` 21` haftmann@52380 ` 22` ```lemma pderiv_0 [simp]: ``` haftmann@52380 ` 23` ``` "pderiv 0 = 0" ``` haftmann@52380 ` 24` ``` using pderiv.simps [of 0 0] by simp ``` huffman@29985 ` 25` haftmann@52380 ` 26` ```lemma pderiv_pCons: ``` haftmann@52380 ` 27` ``` "pderiv (pCons a p) = p + pCons 0 (pderiv p)" ``` haftmann@52380 ` 28` ``` by (simp add: pderiv.simps) ``` huffman@29985 ` 29` eberlm@62128 ` 30` ```lemma pderiv_1 [simp]: "pderiv 1 = 0" ``` eberlm@62128 ` 31` ``` unfolding one_poly_def by (simp add: pderiv_pCons) ``` eberlm@62128 ` 32` eberlm@62128 ` 33` ```lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0" ``` eberlm@62128 ` 34` ``` and pderiv_numeral [simp]: "pderiv (numeral m) = 0" ``` eberlm@62128 ` 35` ``` by (simp_all add: of_nat_poly numeral_poly pderiv_pCons) ``` eberlm@62128 ` 36` huffman@29985 ` 37` ```lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)" ``` lp15@56383 ` 38` ``` by (induct p arbitrary: n) ``` lp15@56383 ` 39` ``` (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split) ``` huffman@29985 ` 40` eberlm@62128 ` 41` ```fun pderiv_coeffs_code :: "('a :: semidom) \ 'a list \ 'a list" where ``` eberlm@62128 ` 42` ``` "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)" ``` eberlm@62128 ` 43` ```| "pderiv_coeffs_code f [] = []" ``` eberlm@62128 ` 44` eberlm@62128 ` 45` ```definition pderiv_coeffs :: "('a :: semidom) list \ 'a list" where ``` eberlm@62128 ` 46` ``` "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)" ``` haftmann@52380 ` 47` eberlm@62128 ` 48` ```(* Efficient code for pderiv contributed by RenĂ© Thiemann and Akihisa Yamada *) ``` eberlm@62128 ` 49` ```lemma pderiv_coeffs_code: ``` eberlm@62128 ` 50` ``` "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * (nth_default 0 xs n)" ``` eberlm@62128 ` 51` ```proof (induct xs arbitrary: f n) ``` eberlm@62128 ` 52` ``` case (Cons x xs f n) ``` eberlm@62128 ` 53` ``` show ?case ``` eberlm@62128 ` 54` ``` proof (cases n) ``` eberlm@62128 ` 55` ``` case 0 ``` eberlm@62128 ` 56` ``` thus ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] \ f * x = 0", auto simp: cCons_def) ``` eberlm@62128 ` 57` ``` next ``` eberlm@62128 ` 58` ``` case (Suc m) note n = this ``` eberlm@62128 ` 59` ``` show ?thesis ``` eberlm@62128 ` 60` ``` proof (cases "pderiv_coeffs_code (f + 1) xs = [] \ f * x = 0") ``` eberlm@62128 ` 61` ``` case False ``` eberlm@62128 ` 62` ``` hence "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = ``` eberlm@62128 ` 63` ``` nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" ``` eberlm@62128 ` 64` ``` by (auto simp: cCons_def n) ``` eberlm@62128 ` 65` ``` also have "\ = (f + of_nat n) * (nth_default 0 xs m)" ``` eberlm@62128 ` 66` ``` unfolding Cons by (simp add: n add_ac) ``` eberlm@62128 ` 67` ``` finally show ?thesis by (simp add: n) ``` eberlm@62128 ` 68` ``` next ``` eberlm@62128 ` 69` ``` case True ``` eberlm@62128 ` 70` ``` { ``` eberlm@62128 ` 71` ``` fix g ``` eberlm@62128 ` 72` ``` have "pderiv_coeffs_code g xs = [] \ g + of_nat m = 0 \ nth_default 0 xs m = 0" ``` eberlm@62128 ` 73` ``` proof (induct xs arbitrary: g m) ``` eberlm@62128 ` 74` ``` case (Cons x xs g) ``` eberlm@62128 ` 75` ``` from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []" ``` eberlm@62128 ` 76` ``` and g: "(g = 0 \ x = 0)" ``` eberlm@62128 ` 77` ``` by (auto simp: cCons_def split: if_splits) ``` eberlm@62128 ` 78` ``` note IH = Cons(1)[OF empty] ``` eberlm@62128 ` 79` ``` from IH[of m] IH[of "m - 1"] g ``` eberlm@62128 ` 80` ``` show ?case by (cases m, auto simp: field_simps) ``` eberlm@62128 ` 81` ``` qed simp ``` eberlm@62128 ` 82` ``` } note empty = this ``` eberlm@62128 ` 83` ``` from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0" ``` eberlm@62128 ` 84` ``` by (auto simp: cCons_def n) ``` eberlm@62128 ` 85` ``` moreover have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" using True ``` eberlm@62128 ` 86` ``` by (simp add: n, insert empty[of "f+1"], auto simp: field_simps) ``` eberlm@62128 ` 87` ``` ultimately show ?thesis by simp ``` eberlm@62128 ` 88` ``` qed ``` eberlm@62128 ` 89` ``` qed ``` eberlm@62128 ` 90` ```qed simp ``` haftmann@52380 ` 91` eberlm@62128 ` 92` ```lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\ i. f (Suc i)) [0 ..< n]" ``` eberlm@62128 ` 93` ``` by (induct n arbitrary: f, auto) ``` eberlm@62128 ` 94` eberlm@62128 ` 95` ```lemma coeffs_pderiv_code [code abstract]: ``` eberlm@62128 ` 96` ``` "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def ``` eberlm@62128 ` 97` ```proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases) ``` eberlm@62128 ` 98` ``` case (1 n) ``` eberlm@62128 ` 99` ``` have id: "coeff p (Suc n) = nth_default 0 (map (\i. coeff p (Suc i)) [0.. degree p = 0" ``` huffman@29985 ` 115` ``` apply (rule iffI) ``` huffman@29985 ` 116` ``` apply (cases p, simp) ``` haftmann@52380 ` 117` ``` apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc) ``` haftmann@52380 ` 118` ``` apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0) ``` huffman@29985 ` 119` ``` done ``` huffman@29985 ` 120` eberlm@62128 ` 121` ```lemma degree_pderiv: "degree (pderiv (p :: 'a poly)) = degree p - 1" ``` huffman@29985 ` 122` ``` apply (rule order_antisym [OF degree_le]) ``` huffman@29985 ` 123` ``` apply (simp add: coeff_pderiv coeff_eq_0) ``` huffman@29985 ` 124` ``` apply (cases "degree p", simp) ``` huffman@29985 ` 125` ``` apply (rule le_degree) ``` huffman@29985 ` 126` ``` apply (simp add: coeff_pderiv del: of_nat_Suc) ``` lp15@56383 ` 127` ``` apply (metis degree_0 leading_coeff_0_iff nat.distinct(1)) ``` huffman@29985 ` 128` ``` done ``` huffman@29985 ` 129` eberlm@62128 ` 130` ```lemma not_dvd_pderiv: ``` eberlm@62128 ` 131` ``` assumes "degree (p :: 'a poly) \ 0" ``` eberlm@62128 ` 132` ``` shows "\ p dvd pderiv p" ``` eberlm@62128 ` 133` ```proof ``` eberlm@62128 ` 134` ``` assume dvd: "p dvd pderiv p" ``` eberlm@62128 ` 135` ``` then obtain q where p: "pderiv p = p * q" unfolding dvd_def by auto ``` eberlm@62128 ` 136` ``` from dvd have le: "degree p \ degree (pderiv p)" ``` eberlm@62128 ` 137` ``` by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff) ``` eberlm@62128 ` 138` ``` from this[unfolded degree_pderiv] assms show False by auto ``` eberlm@62128 ` 139` ```qed ``` eberlm@62128 ` 140` eberlm@62128 ` 141` ```lemma dvd_pderiv_iff [simp]: "(p :: 'a poly) dvd pderiv p \ degree p = 0" ``` eberlm@62128 ` 142` ``` using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric]) ``` eberlm@62128 ` 143` eberlm@62128 ` 144` ```end ``` eberlm@62128 ` 145` huffman@29985 ` 146` ```lemma pderiv_singleton [simp]: "pderiv [:a:] = 0" ``` huffman@29985 ` 147` ```by (simp add: pderiv_pCons) ``` huffman@29985 ` 148` huffman@29985 ` 149` ```lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q" ``` haftmann@52380 ` 150` ```by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) ``` huffman@29985 ` 151` eberlm@62128 ` 152` ```lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p" ``` eberlm@62128 ` 153` ```by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) ``` huffman@29985 ` 154` huffman@29985 ` 155` ```lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q" ``` haftmann@52380 ` 156` ```by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) ``` huffman@29985 ` 157` huffman@29985 ` 158` ```lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)" ``` haftmann@52380 ` 159` ```by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) ``` huffman@29985 ` 160` huffman@29985 ` 161` ```lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p" ``` lp15@56383 ` 162` ```by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps) ``` huffman@29985 ` 163` huffman@29985 ` 164` ```lemma pderiv_power_Suc: ``` huffman@29985 ` 165` ``` "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p" ``` huffman@29985 ` 166` ```apply (induct n) ``` huffman@29985 ` 167` ```apply simp ``` huffman@29985 ` 168` ```apply (subst power_Suc) ``` huffman@29985 ` 169` ```apply (subst pderiv_mult) ``` huffman@29985 ` 170` ```apply (erule ssubst) ``` huffman@47108 ` 171` ```apply (simp only: of_nat_Suc smult_add_left smult_1_left) ``` lp15@56383 ` 172` ```apply (simp add: algebra_simps) ``` huffman@29985 ` 173` ```done ``` huffman@29985 ` 174` eberlm@62128 ` 175` ```lemma pderiv_setprod: "pderiv (setprod f (as)) = ``` eberlm@62128 ` 176` ``` (\a \ as. setprod f (as - {a}) * pderiv (f a))" ``` eberlm@62128 ` 177` ```proof (induct as rule: infinite_finite_induct) ``` eberlm@62128 ` 178` ``` case (insert a as) ``` eberlm@62128 ` 179` ``` hence id: "setprod f (insert a as) = f a * setprod f as" ``` eberlm@62128 ` 180` ``` "\ g. setsum g (insert a as) = g a + setsum g as" ``` eberlm@62128 ` 181` ``` "insert a as - {a} = as" ``` eberlm@62128 ` 182` ``` by auto ``` eberlm@62128 ` 183` ``` { ``` eberlm@62128 ` 184` ``` fix b ``` eberlm@62128 ` 185` ``` assume "b \ as" ``` eberlm@62128 ` 186` ``` hence id2: "insert a as - {b} = insert a (as - {b})" using `a \ as` by auto ``` eberlm@62128 ` 187` ``` have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})" ``` eberlm@62128 ` 188` ``` unfolding id2 ``` eberlm@62128 ` 189` ``` by (subst setprod.insert, insert insert, auto) ``` eberlm@62128 ` 190` ``` } note id2 = this ``` eberlm@62128 ` 191` ``` show ?case ``` eberlm@62128 ` 192` ``` unfolding id pderiv_mult insert(3) setsum_right_distrib ``` eberlm@62128 ` 193` ``` by (auto simp add: ac_simps id2 intro!: setsum.cong) ``` eberlm@62128 ` 194` ```qed auto ``` eberlm@62128 ` 195` huffman@29985 ` 196` ```lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)" ``` huffman@44317 ` 197` ```by (rule DERIV_cong, rule DERIV_pow, simp) ``` huffman@29985 ` 198` ```declare DERIV_pow2 [simp] DERIV_pow [simp] ``` huffman@29985 ` 199` huffman@29985 ` 200` ```lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: 'a::real_normed_field) x :> D" ``` huffman@44317 ` 201` ```by (rule DERIV_cong, rule DERIV_add, auto) ``` huffman@29985 ` 202` eberlm@62128 ` 203` ```lemma poly_DERIV [simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" ``` hoelzl@56381 ` 204` ``` by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons) ``` huffman@29985 ` 205` eberlm@62065 ` 206` ```lemma continuous_on_poly [continuous_intros]: ``` eberlm@62065 ` 207` ``` fixes p :: "'a :: {real_normed_field} poly" ``` eberlm@62065 ` 208` ``` assumes "continuous_on A f" ``` eberlm@62065 ` 209` ``` shows "continuous_on A (\x. poly p (f x))" ``` eberlm@62065 ` 210` ```proof - ``` eberlm@62065 ` 211` ``` have "continuous_on A (\x. (\i\degree p. (f x) ^ i * coeff p i))" ``` eberlm@62065 ` 212` ``` by (intro continuous_intros assms) ``` eberlm@62065 ` 213` ``` also have "\ = (\x. poly p (f x))" by (intro ext) (simp add: poly_altdef mult_ac) ``` eberlm@62065 ` 214` ``` finally show ?thesis . ``` eberlm@62065 ` 215` ```qed ``` eberlm@62065 ` 216` wenzelm@60500 ` 217` ```text\Consequences of the derivative theorem above\ ``` huffman@29985 ` 218` hoelzl@56181 ` 219` ```lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)" ``` hoelzl@56181 ` 220` ```apply (simp add: real_differentiable_def) ``` huffman@29985 ` 221` ```apply (blast intro: poly_DERIV) ``` huffman@29985 ` 222` ```done ``` huffman@29985 ` 223` huffman@29985 ` 224` ```lemma poly_isCont[simp]: "isCont (%x. poly p x) (x::real)" ``` huffman@29985 ` 225` ```by (rule poly_DERIV [THEN DERIV_isCont]) ``` huffman@29985 ` 226` huffman@29985 ` 227` ```lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |] ``` huffman@29985 ` 228` ``` ==> \x. a < x & x < b & (poly p x = 0)" ``` lp15@56383 ` 229` ```using IVT_objl [of "poly p" a 0 b] ``` lp15@56383 ` 230` ```by (auto simp add: order_le_less) ``` huffman@29985 ` 231` huffman@29985 ` 232` ```lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |] ``` huffman@29985 ` 233` ``` ==> \x. a < x & x < b & (poly p x = 0)" ``` huffman@29985 ` 234` ```by (insert poly_IVT_pos [where p = "- p" ]) simp ``` huffman@29985 ` 235` eberlm@62065 ` 236` ```lemma poly_IVT: ``` eberlm@62065 ` 237` ``` fixes p::"real poly" ``` eberlm@62065 ` 238` ``` assumes "ax>a. x < b \ poly p x = 0" ``` eberlm@62065 ` 240` ```by (metis assms(1) assms(2) less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos) ``` eberlm@62065 ` 241` huffman@29985 ` 242` ```lemma poly_MVT: "(a::real) < b ==> ``` huffman@29985 ` 243` ``` \x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)" ``` lp15@56383 ` 244` ```using MVT [of a b "poly p"] ``` lp15@56383 ` 245` ```apply auto ``` huffman@29985 ` 246` ```apply (rule_tac x = z in exI) ``` lp15@56217 ` 247` ```apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique]) ``` huffman@29985 ` 248` ```done ``` huffman@29985 ` 249` eberlm@62065 ` 250` ```lemma poly_MVT': ``` eberlm@62065 ` 251` ``` assumes "{min a b..max a b} \ A" ``` eberlm@62065 ` 252` ``` shows "\x\A. poly p b - poly p a = (b - a) * poly (pderiv p) (x::real)" ``` eberlm@62065 ` 253` ```proof (cases a b rule: linorder_cases) ``` eberlm@62065 ` 254` ``` case less ``` eberlm@62065 ` 255` ``` from poly_MVT[OF less, of p] guess x by (elim exE conjE) ``` eberlm@62065 ` 256` ``` thus ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms]) ``` eberlm@62065 ` 257` eberlm@62065 ` 258` ```next ``` eberlm@62065 ` 259` ``` case greater ``` eberlm@62065 ` 260` ``` from poly_MVT[OF greater, of p] guess x by (elim exE conjE) ``` eberlm@62065 ` 261` ``` thus ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms]) ``` eberlm@62065 ` 262` ```qed (insert assms, auto) ``` eberlm@62065 ` 263` eberlm@62065 ` 264` ```lemma poly_pinfty_gt_lc: ``` eberlm@62065 ` 265` ``` fixes p:: "real poly" ``` eberlm@62065 ` 266` ``` assumes "lead_coeff p > 0" ``` eberlm@62065 ` 267` ``` shows "\ n. \ x \ n. poly p x \ lead_coeff p" using assms ``` eberlm@62065 ` 268` ```proof (induct p) ``` eberlm@62065 ` 269` ``` case 0 ``` eberlm@62065 ` 270` ``` thus ?case by auto ``` eberlm@62065 ` 271` ```next ``` eberlm@62065 ` 272` ``` case (pCons a p) ``` eberlm@62065 ` 273` ``` have "\a\0;p=0\ \ ?case" by auto ``` eberlm@62065 ` 274` ``` moreover have "p\0 \ ?case" ``` eberlm@62065 ` 275` ``` proof - ``` eberlm@62065 ` 276` ``` assume "p\0" ``` eberlm@62065 ` 277` ``` then obtain n1 where gte_lcoeff:"\x\n1. lead_coeff p \ poly p x" using that pCons by auto ``` wenzelm@62072 ` 278` ``` have gt_0:"lead_coeff p >0" using pCons(3) \p\0\ by auto ``` eberlm@62065 ` 279` ``` def n\"max n1 (1+ \a\/(lead_coeff p))" ``` eberlm@62065 ` 280` ``` show ?thesis ``` eberlm@62065 ` 281` ``` proof (rule_tac x=n in exI,rule,rule) ``` eberlm@62065 ` 282` ``` fix x assume "n \ x" ``` eberlm@62065 ` 283` ``` hence "lead_coeff p \ poly p x" ``` eberlm@62065 ` 284` ``` using gte_lcoeff unfolding n_def by auto ``` eberlm@62065 ` 285` ``` hence " \a\/(lead_coeff p) \ \a\/(poly p x)" and "poly p x>0" using gt_0 ``` eberlm@62065 ` 286` ``` by (intro frac_le,auto) ``` wenzelm@62072 ` 287` ``` hence "x\1+ \a\/(poly p x)" using \n\x\[unfolded n_def] by auto ``` eberlm@62065 ` 288` ``` thus "lead_coeff (pCons a p) \ poly (pCons a p) x" ``` wenzelm@62072 ` 289` ``` using \lead_coeff p \ poly p x\ \poly p x>0\ \p\0\ ``` eberlm@62065 ` 290` ``` by (auto simp add:field_simps) ``` eberlm@62065 ` 291` ``` qed ``` eberlm@62065 ` 292` ``` qed ``` eberlm@62065 ` 293` ``` ultimately show ?case by fastforce ``` eberlm@62065 ` 294` ```qed ``` eberlm@62065 ` 295` eberlm@62065 ` 296` eberlm@62128 ` 297` ```subsection \Algebraic numbers\ ``` eberlm@62128 ` 298` eberlm@62128 ` 299` ```text \ ``` eberlm@62128 ` 300` ``` Algebraic numbers can be defined in two equivalent ways: all real numbers that are ``` eberlm@62128 ` 301` ``` roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry ``` eberlm@62128 ` 302` ``` uses the rational definition, but we need the integer definition. ``` eberlm@62128 ` 303` eberlm@62128 ` 304` ``` The equivalence is obvious since any rational polynomial can be multiplied with the ``` eberlm@62128 ` 305` ``` LCM of its coefficients, yielding an integer polynomial with the same roots. ``` eberlm@62128 ` 306` ```\ ``` eberlm@62128 ` 307` ```subsection \Algebraic numbers\ ``` eberlm@62128 ` 308` eberlm@62128 ` 309` ```definition algebraic :: "'a :: field_char_0 \ bool" where ``` eberlm@62128 ` 310` ``` "algebraic x \ (\p. (\i. coeff p i \ \) \ p \ 0 \ poly p x = 0)" ``` eberlm@62128 ` 311` eberlm@62128 ` 312` ```lemma algebraicI: ``` eberlm@62128 ` 313` ``` assumes "\i. coeff p i \ \" "p \ 0" "poly p x = 0" ``` eberlm@62128 ` 314` ``` shows "algebraic x" ``` eberlm@62128 ` 315` ``` using assms unfolding algebraic_def by blast ``` eberlm@62128 ` 316` ``` ``` eberlm@62128 ` 317` ```lemma algebraicE: ``` eberlm@62128 ` 318` ``` assumes "algebraic x" ``` eberlm@62128 ` 319` ``` obtains p where "\i. coeff p i \ \" "p \ 0" "poly p x = 0" ``` eberlm@62128 ` 320` ``` using assms unfolding algebraic_def by blast ``` eberlm@62128 ` 321` eberlm@62128 ` 322` ```lemma quotient_of_denom_pos': "snd (quotient_of x) > 0" ``` eberlm@62128 ` 323` ``` using quotient_of_denom_pos[OF surjective_pairing] . ``` eberlm@62128 ` 324` ``` ``` eberlm@62128 ` 325` ```lemma of_int_div_in_Ints: ``` eberlm@62128 ` 326` ``` "b dvd a \ of_int a div of_int b \ (\ :: 'a :: ring_div set)" ``` eberlm@62128 ` 327` ```proof (cases "of_int b = (0 :: 'a)") ``` eberlm@62128 ` 328` ``` assume "b dvd a" "of_int b \ (0::'a)" ``` eberlm@62128 ` 329` ``` then obtain c where "a = b * c" by (elim dvdE) ``` eberlm@62128 ` 330` ``` with \of_int b \ (0::'a)\ show ?thesis by simp ``` eberlm@62128 ` 331` ```qed auto ``` eberlm@62128 ` 332` eberlm@62128 ` 333` ```lemma of_int_divide_in_Ints: ``` eberlm@62128 ` 334` ``` "b dvd a \ of_int a / of_int b \ (\ :: 'a :: field set)" ``` eberlm@62128 ` 335` ```proof (cases "of_int b = (0 :: 'a)") ``` eberlm@62128 ` 336` ``` assume "b dvd a" "of_int b \ (0::'a)" ``` eberlm@62128 ` 337` ``` then obtain c where "a = b * c" by (elim dvdE) ``` eberlm@62128 ` 338` ``` with \of_int b \ (0::'a)\ show ?thesis by simp ``` eberlm@62128 ` 339` ```qed auto ``` eberlm@62128 ` 340` eberlm@62128 ` 341` ```lemma algebraic_altdef: ``` eberlm@62128 ` 342` ``` fixes p :: "'a :: field_char_0 poly" ``` eberlm@62128 ` 343` ``` shows "algebraic x \ (\p. (\i. coeff p i \ \) \ p \ 0 \ poly p x = 0)" ``` eberlm@62128 ` 344` ```proof safe ``` eberlm@62128 ` 345` ``` fix p assume rat: "\i. coeff p i \ \" and root: "poly p x = 0" and nz: "p \ 0" ``` eberlm@62128 ` 346` ``` def cs \ "coeffs p" ``` eberlm@62128 ` 347` ``` from rat have "\c\range (coeff p). \c'. c = of_rat c'" unfolding Rats_def by blast ``` eberlm@62128 ` 348` ``` then obtain f where f: "\i. coeff p i = of_rat (f (coeff p i))" ``` eberlm@62128 ` 349` ``` by (subst (asm) bchoice_iff) blast ``` eberlm@62128 ` 350` ``` def cs' \ "map (quotient_of \ f) (coeffs p)" ``` eberlm@62128 ` 351` ``` def d \ "Lcm (set (map snd cs'))" ``` eberlm@62128 ` 352` ``` def p' \ "smult (of_int d) p" ``` eberlm@62128 ` 353` ``` ``` eberlm@62128 ` 354` ``` have "\n. coeff p' n \ \" ``` eberlm@62128 ` 355` ``` proof ``` eberlm@62128 ` 356` ``` fix n :: nat ``` eberlm@62128 ` 357` ``` show "coeff p' n \ \" ``` eberlm@62128 ` 358` ``` proof (cases "n \ degree p") ``` eberlm@62128 ` 359` ``` case True ``` eberlm@62128 ` 360` ``` def c \ "coeff p n" ``` eberlm@62128 ` 361` ``` def a \ "fst (quotient_of (f (coeff p n)))" and b \ "snd (quotient_of (f (coeff p n)))" ``` eberlm@62128 ` 362` ``` have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp ``` eberlm@62128 ` 363` ``` have "coeff p' n = of_int d * coeff p n" by (simp add: p'_def) ``` eberlm@62128 ` 364` ``` also have "coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def ``` eberlm@62128 ` 365` ``` by (subst quotient_of_div [of "f (coeff p n)", symmetric]) ``` eberlm@62128 ` 366` ``` (simp_all add: f [symmetric]) ``` eberlm@62128 ` 367` ``` also have "of_int d * \ = of_rat (of_int (a*d) / of_int b)" ``` eberlm@62128 ` 368` ``` by (simp add: of_rat_mult of_rat_divide) ``` eberlm@62128 ` 369` ``` also from nz True have "b \ snd ` set cs'" unfolding cs'_def ``` eberlm@62128 ` 370` ``` by (force simp: o_def b_def coeffs_def simp del: upt_Suc) ``` eberlm@62128 ` 371` ``` hence "b dvd (a * d)" unfolding d_def by simp ``` eberlm@62128 ` 372` ``` hence "of_int (a * d) / of_int b \ (\ :: rat set)" ``` eberlm@62128 ` 373` ``` by (rule of_int_divide_in_Ints) ``` eberlm@62128 ` 374` ``` hence "of_rat (of_int (a * d) / of_int b) \ \" by (elim Ints_cases) auto ``` eberlm@62128 ` 375` ``` finally show ?thesis . ``` eberlm@62128 ` 376` ``` qed (auto simp: p'_def not_le coeff_eq_0) ``` eberlm@62128 ` 377` ``` qed ``` eberlm@62128 ` 378` ``` ``` eberlm@62128 ` 379` ``` moreover have "set (map snd cs') \ {0<..}" ``` eberlm@62128 ` 380` ``` unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) ``` eberlm@62128 ` 381` ``` hence "d \ 0" unfolding d_def by (induction cs') simp_all ``` eberlm@62128 ` 382` ``` with nz have "p' \ 0" by (simp add: p'_def) ``` eberlm@62128 ` 383` ``` moreover from root have "poly p' x = 0" by (simp add: p'_def) ``` eberlm@62128 ` 384` ``` ultimately show "algebraic x" unfolding algebraic_def by blast ``` eberlm@62128 ` 385` ```next ``` eberlm@62128 ` 386` eberlm@62128 ` 387` ``` assume "algebraic x" ``` eberlm@62128 ` 388` ``` then obtain p where p: "\i. coeff p i \ \" "poly p x = 0" "p \ 0" ``` eberlm@62128 ` 389` ``` by (force simp: algebraic_def) ``` eberlm@62128 ` 390` ``` moreover have "coeff p i \ \ \ coeff p i \ \" for i by (elim Ints_cases) simp ``` eberlm@62128 ` 391` ``` ultimately show "(\p. (\i. coeff p i \ \) \ p \ 0 \ poly p x = 0)" by auto ``` eberlm@62128 ` 392` ```qed ``` eberlm@62128 ` 393` eberlm@62128 ` 394` wenzelm@60500 ` 395` ```text\Lemmas for Derivatives\ ``` huffman@29985 ` 396` huffman@29985 ` 397` ```lemma order_unique_lemma: ``` huffman@29985 ` 398` ``` fixes p :: "'a::idom poly" ``` lp15@56383 ` 399` ``` assumes "[:-a, 1:] ^ n dvd p" "\ [:-a, 1:] ^ Suc n dvd p" ``` huffman@29985 ` 400` ``` shows "n = order a p" ``` huffman@29985 ` 401` ```unfolding Polynomial.order_def ``` huffman@29985 ` 402` ```apply (rule Least_equality [symmetric]) ``` haftmann@58199 ` 403` ```apply (fact assms) ``` haftmann@58199 ` 404` ```apply (rule classical) ``` haftmann@58199 ` 405` ```apply (erule notE) ``` haftmann@58199 ` 406` ```unfolding not_less_eq_eq ``` haftmann@58199 ` 407` ```using assms(1) apply (rule power_le_dvd) ``` haftmann@58199 ` 408` ```apply assumption ``` haftmann@58199 ` 409` ```done ``` huffman@29985 ` 410` huffman@29985 ` 411` ```lemma lemma_order_pderiv1: ``` huffman@29985 ` 412` ``` "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q + ``` huffman@29985 ` 413` ``` smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)" ``` huffman@29985 ` 414` ```apply (simp only: pderiv_mult pderiv_power_Suc) ``` huffman@30273 ` 415` ```apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons) ``` huffman@29985 ` 416` ```done ``` huffman@29985 ` 417` lp15@56383 ` 418` ```lemma lemma_order_pderiv: ``` eberlm@62128 ` 419` ``` fixes p :: "'a :: field_char_0 poly" ``` lp15@56383 ` 420` ``` assumes n: "0 < n" ``` lp15@56383 ` 421` ``` and pd: "pderiv p \ 0" ``` lp15@56383 ` 422` ``` and pe: "p = [:- a, 1:] ^ n * q" ``` lp15@56383 ` 423` ``` and nd: "~ [:- a, 1:] dvd q" ``` lp15@56383 ` 424` ``` shows "n = Suc (order a (pderiv p))" ``` lp15@56383 ` 425` ```using n ``` lp15@56383 ` 426` ```proof - ``` lp15@56383 ` 427` ``` have "pderiv ([:- a, 1:] ^ n * q) \ 0" ``` lp15@56383 ` 428` ``` using assms by auto ``` lp15@56383 ` 429` ``` obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \ 0" ``` lp15@56383 ` 430` ``` using assms by (cases n) auto ``` eberlm@62128 ` 431` ``` have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \ k dvd l" ``` eberlm@62128 ` 432` ``` by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff) ``` lp15@56383 ` 433` ``` have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" ``` lp15@56383 ` 434` ``` proof (rule order_unique_lemma) ``` lp15@56383 ` 435` ``` show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)" ``` lp15@56383 ` 436` ``` apply (subst lemma_order_pderiv1) ``` lp15@56383 ` 437` ``` apply (rule dvd_add) ``` lp15@56383 ` 438` ``` apply (metis dvdI dvd_mult2 power_Suc2) ``` lp15@56383 ` 439` ``` apply (metis dvd_smult dvd_triv_right) ``` lp15@56383 ` 440` ``` done ``` lp15@56383 ` 441` ``` next ``` lp15@56383 ` 442` ``` show "\ [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)" ``` lp15@56383 ` 443` ``` apply (subst lemma_order_pderiv1) ``` haftmann@60867 ` 444` ``` by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one) ``` lp15@56383 ` 445` ``` qed ``` lp15@56383 ` 446` ``` then show ?thesis ``` wenzelm@60500 ` 447` ``` by (metis \n = Suc n'\ pe) ``` lp15@56383 ` 448` ```qed ``` huffman@29985 ` 449` huffman@29985 ` 450` ```lemma order_decomp: ``` haftmann@60688 ` 451` ``` assumes "p \ 0" ``` haftmann@60688 ` 452` ``` shows "\q. p = [:- a, 1:] ^ order a p * q \ \ [:- a, 1:] dvd q" ``` haftmann@60688 ` 453` ```proof - ``` haftmann@60688 ` 454` ``` from assms have A: "[:- a, 1:] ^ order a p dvd p" ``` haftmann@60688 ` 455` ``` and B: "\ [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order) ``` haftmann@60688 ` 456` ``` from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" .. ``` haftmann@60688 ` 457` ``` with B have "\ [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q" ``` haftmann@60688 ` 458` ``` by simp ``` haftmann@60688 ` 459` ``` then have "\ [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q" ``` haftmann@60688 ` 460` ``` by simp ``` haftmann@60688 ` 461` ``` then have D: "\ [:- a, 1:] dvd q" ``` haftmann@60688 ` 462` ``` using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q] ``` haftmann@60688 ` 463` ``` by auto ``` haftmann@60688 ` 464` ``` from C D show ?thesis by blast ``` haftmann@60688 ` 465` ```qed ``` huffman@29985 ` 466` eberlm@62128 ` 467` ```lemma order_pderiv: ``` eberlm@62128 ` 468` ``` "\pderiv p \ 0; order a (p :: 'a :: field_char_0 poly) \ 0\ \ ``` eberlm@62128 ` 469` ``` (order a p = Suc (order a (pderiv p)))" ``` huffman@29985 ` 470` ```apply (case_tac "p = 0", simp) ``` huffman@29985 ` 471` ```apply (drule_tac a = a and p = p in order_decomp) ``` huffman@29985 ` 472` ```using neq0_conv ``` huffman@29985 ` 473` ```apply (blast intro: lemma_order_pderiv) ``` huffman@29985 ` 474` ```done ``` huffman@29985 ` 475` huffman@29985 ` 476` ```lemma order_mult: "p * q \ 0 \ order a (p * q) = order a p + order a q" ``` huffman@29985 ` 477` ```proof - ``` huffman@29985 ` 478` ``` def i \ "order a p" ``` huffman@29985 ` 479` ``` def j \ "order a q" ``` huffman@29985 ` 480` ``` def t \ "[:-a, 1:]" ``` huffman@29985 ` 481` ``` have t_dvd_iff: "\u. t dvd u \ poly u a = 0" ``` huffman@29985 ` 482` ``` unfolding t_def by (simp add: dvd_iff_poly_eq_0) ``` huffman@29985 ` 483` ``` assume "p * q \ 0" ``` huffman@29985 ` 484` ``` then show "order a (p * q) = i + j" ``` huffman@29985 ` 485` ``` apply clarsimp ``` huffman@29985 ` 486` ``` apply (drule order [where a=a and p=p, folded i_def t_def]) ``` huffman@29985 ` 487` ``` apply (drule order [where a=a and p=q, folded j_def t_def]) ``` huffman@29985 ` 488` ``` apply clarify ``` lp15@56383 ` 489` ``` apply (erule dvdE)+ ``` huffman@29985 ` 490` ``` apply (rule order_unique_lemma [symmetric], fold t_def) ``` lp15@56383 ` 491` ``` apply (simp_all add: power_add t_dvd_iff) ``` huffman@29985 ` 492` ``` done ``` huffman@29985 ` 493` ```qed ``` huffman@29985 ` 494` eberlm@62065 ` 495` ```lemma order_smult: ``` eberlm@62065 ` 496` ``` assumes "c \ 0" ``` eberlm@62065 ` 497` ``` shows "order x (smult c p) = order x p" ``` eberlm@62065 ` 498` ```proof (cases "p = 0") ``` eberlm@62065 ` 499` ``` case False ``` eberlm@62065 ` 500` ``` have "smult c p = [:c:] * p" by simp ``` eberlm@62065 ` 501` ``` also from assms False have "order x \ = order x [:c:] + order x p" ``` eberlm@62065 ` 502` ``` by (subst order_mult) simp_all ``` eberlm@62065 ` 503` ``` also from assms have "order x [:c:] = 0" by (intro order_0I) auto ``` eberlm@62065 ` 504` ``` finally show ?thesis by simp ``` eberlm@62065 ` 505` ```qed simp ``` eberlm@62065 ` 506` eberlm@62065 ` 507` ```(* Next two lemmas contributed by Wenda Li *) ``` eberlm@62065 ` 508` ```lemma order_1_eq_0 [simp]:"order x 1 = 0" ``` eberlm@62065 ` 509` ``` by (metis order_root poly_1 zero_neq_one) ``` eberlm@62065 ` 510` eberlm@62065 ` 511` ```lemma order_power_n_n: "order a ([:-a,1:]^n)=n" ``` eberlm@62065 ` 512` ```proof (induct n) (*might be proved more concisely using nat_less_induct*) ``` eberlm@62065 ` 513` ``` case 0 ``` eberlm@62065 ` 514` ``` thus ?case by (metis order_root poly_1 power_0 zero_neq_one) ``` eberlm@62065 ` 515` ```next ``` eberlm@62065 ` 516` ``` case (Suc n) ``` eberlm@62065 ` 517` ``` have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" ``` eberlm@62065 ` 518` ``` by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral ``` eberlm@62065 ` 519` ``` one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right) ``` eberlm@62065 ` 520` ``` moreover have "order a [:-a,1:]=1" unfolding order_def ``` eberlm@62065 ` 521` ``` proof (rule Least_equality,rule ccontr) ``` eberlm@62065 ` 522` ``` assume "\ \ [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" ``` eberlm@62065 ` 523` ``` hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp ``` eberlm@62065 ` 524` ``` hence "degree ([:- a, 1:] ^ Suc 1) \ degree ([:- a, 1:] )" ``` eberlm@62065 ` 525` ``` by (rule dvd_imp_degree_le,auto) ``` eberlm@62065 ` 526` ``` thus False by auto ``` eberlm@62065 ` 527` ``` next ``` eberlm@62065 ` 528` ``` fix y assume asm:"\ [:- a, 1:] ^ Suc y dvd [:- a, 1:]" ``` eberlm@62065 ` 529` ``` show "1 \ y" ``` eberlm@62065 ` 530` ``` proof (rule ccontr) ``` eberlm@62065 ` 531` ``` assume "\ 1 \ y" ``` eberlm@62065 ` 532` ``` hence "y=0" by auto ``` eberlm@62065 ` 533` ``` hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto ``` eberlm@62065 ` 534` ``` thus False using asm by auto ``` eberlm@62065 ` 535` ``` qed ``` eberlm@62065 ` 536` ``` qed ``` eberlm@62065 ` 537` ``` ultimately show ?case using Suc by auto ``` eberlm@62065 ` 538` ```qed ``` eberlm@62065 ` 539` wenzelm@60500 ` 540` ```text\Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\ ``` huffman@29985 ` 541` huffman@29985 ` 542` ```lemma order_divides: "[:-a, 1:] ^ n dvd p \ p = 0 \ n \ order a p" ``` huffman@29985 ` 543` ```apply (cases "p = 0", auto) ``` huffman@29985 ` 544` ```apply (drule order_2 [where a=a and p=p]) ``` lp15@56383 ` 545` ```apply (metis not_less_eq_eq power_le_dvd) ``` huffman@29985 ` 546` ```apply (erule power_le_dvd [OF order_1]) ``` huffman@29985 ` 547` ```done ``` huffman@29985 ` 548` huffman@29985 ` 549` ```lemma poly_squarefree_decomp_order: ``` eberlm@62128 ` 550` ``` assumes "pderiv (p :: 'a :: field_char_0 poly) \ 0" ``` huffman@29985 ` 551` ``` and p: "p = q * d" ``` huffman@29985 ` 552` ``` and p': "pderiv p = e * d" ``` huffman@29985 ` 553` ``` and d: "d = r * p + s * pderiv p" ``` huffman@29985 ` 554` ``` shows "order a q = (if order a p = 0 then 0 else 1)" ``` huffman@29985 ` 555` ```proof (rule classical) ``` huffman@29985 ` 556` ``` assume 1: "order a q \ (if order a p = 0 then 0 else 1)" ``` wenzelm@60500 ` 557` ``` from \pderiv p \ 0\ have "p \ 0" by auto ``` huffman@29985 ` 558` ``` with p have "order a p = order a q + order a d" ``` huffman@29985 ` 559` ``` by (simp add: order_mult) ``` huffman@29985 ` 560` ``` with 1 have "order a p \ 0" by (auto split: if_splits) ``` huffman@29985 ` 561` ``` have "order a (pderiv p) = order a e + order a d" ``` wenzelm@60500 ` 562` ``` using \pderiv p \ 0\ \pderiv p = e * d\ by (simp add: order_mult) ``` huffman@29985 ` 563` ``` have "order a p = Suc (order a (pderiv p))" ``` wenzelm@60500 ` 564` ``` using \pderiv p \ 0\ \order a p \ 0\ by (rule order_pderiv) ``` wenzelm@60500 ` 565` ``` have "d \ 0" using \p \ 0\ \p = q * d\ by simp ``` huffman@29985 ` 566` ``` have "([:-a, 1:] ^ (order a (pderiv p))) dvd d" ``` huffman@29985 ` 567` ``` apply (simp add: d) ``` huffman@29985 ` 568` ``` apply (rule dvd_add) ``` huffman@29985 ` 569` ``` apply (rule dvd_mult) ``` wenzelm@60500 ` 570` ``` apply (simp add: order_divides \p \ 0\ ``` wenzelm@60500 ` 571` ``` \order a p = Suc (order a (pderiv p))\) ``` huffman@29985 ` 572` ``` apply (rule dvd_mult) ``` huffman@29985 ` 573` ``` apply (simp add: order_divides) ``` huffman@29985 ` 574` ``` done ``` huffman@29985 ` 575` ``` then have "order a (pderiv p) \ order a d" ``` wenzelm@60500 ` 576` ``` using \d \ 0\ by (simp add: order_divides) ``` huffman@29985 ` 577` ``` show ?thesis ``` wenzelm@60500 ` 578` ``` using \order a p = order a q + order a d\ ``` wenzelm@60500 ` 579` ``` using \order a (pderiv p) = order a e + order a d\ ``` wenzelm@60500 ` 580` ``` using \order a p = Suc (order a (pderiv p))\ ``` wenzelm@60500 ` 581` ``` using \order a (pderiv p) \ order a d\ ``` huffman@29985 ` 582` ``` by auto ``` huffman@29985 ` 583` ```qed ``` huffman@29985 ` 584` eberlm@62128 ` 585` ```lemma poly_squarefree_decomp_order2: ``` eberlm@62128 ` 586` ``` "\pderiv p \ (0 :: 'a :: field_char_0 poly); ``` eberlm@62128 ` 587` ``` p = q * d; ``` eberlm@62128 ` 588` ``` pderiv p = e * d; ``` eberlm@62128 ` 589` ``` d = r * p + s * pderiv p ``` eberlm@62128 ` 590` ``` \ \ \a. order a q = (if order a p = 0 then 0 else 1)" ``` lp15@56383 ` 591` ```by (blast intro: poly_squarefree_decomp_order) ``` huffman@29985 ` 592` eberlm@62128 ` 593` ```lemma order_pderiv2: ``` eberlm@62128 ` 594` ``` "\pderiv p \ 0; order a (p :: 'a :: field_char_0 poly) \ 0\ ``` eberlm@62128 ` 595` ``` \ (order a (pderiv p) = n) = (order a p = Suc n)" ``` lp15@56383 ` 596` ```by (auto dest: order_pderiv) ``` huffman@29985 ` 597` huffman@29985 ` 598` ```definition ``` huffman@29985 ` 599` ``` rsquarefree :: "'a::idom poly => bool" where ``` huffman@29985 ` 600` ``` "rsquarefree p = (p \ 0 & (\a. (order a p = 0) | (order a p = 1)))" ``` huffman@29985 ` 601` eberlm@62128 ` 602` ```lemma pderiv_iszero: "pderiv p = 0 \ \h. p = [:h :: 'a :: {semidom,semiring_char_0}:]" ``` huffman@29985 ` 603` ```apply (simp add: pderiv_eq_0_iff) ``` huffman@29985 ` 604` ```apply (case_tac p, auto split: if_splits) ``` huffman@29985 ` 605` ```done ``` huffman@29985 ` 606` huffman@29985 ` 607` ```lemma rsquarefree_roots: ``` eberlm@62128 ` 608` ``` fixes p :: "'a :: field_char_0 poly" ``` eberlm@62128 ` 609` ``` shows "rsquarefree p = (\a. \(poly p a = 0 \ poly (pderiv p) a = 0))" ``` huffman@29985 ` 610` ```apply (simp add: rsquarefree_def) ``` huffman@29985 ` 611` ```apply (case_tac "p = 0", simp, simp) ``` huffman@29985 ` 612` ```apply (case_tac "pderiv p = 0") ``` huffman@29985 ` 613` ```apply simp ``` lp15@56383 ` 614` ```apply (drule pderiv_iszero, clarsimp) ``` lp15@56383 ` 615` ```apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree) ``` lp15@56383 ` 616` ```apply (force simp add: order_root order_pderiv2) ``` huffman@29985 ` 617` ```done ``` huffman@29985 ` 618` huffman@29985 ` 619` ```lemma poly_squarefree_decomp: ``` eberlm@62128 ` 620` ``` assumes "pderiv (p :: 'a :: field_char_0 poly) \ 0" ``` huffman@29985 ` 621` ``` and "p = q * d" ``` huffman@29985 ` 622` ``` and "pderiv p = e * d" ``` huffman@29985 ` 623` ``` and "d = r * p + s * pderiv p" ``` huffman@29985 ` 624` ``` shows "rsquarefree q & (\a. (poly q a = 0) = (poly p a = 0))" ``` huffman@29985 ` 625` ```proof - ``` wenzelm@60500 ` 626` ``` from \pderiv p \ 0\ have "p \ 0" by auto ``` wenzelm@60500 ` 627` ``` with \p = q * d\ have "q \ 0" by simp ``` huffman@29985 ` 628` ``` have "\a. order a q = (if order a p = 0 then 0 else 1)" ``` huffman@29985 ` 629` ``` using assms by (rule poly_squarefree_decomp_order2) ``` wenzelm@60500 ` 630` ``` with \p \ 0\ \q \ 0\ show ?thesis ``` huffman@29985 ` 631` ``` by (simp add: rsquarefree_def order_root) ``` huffman@29985 ` 632` ```qed ``` huffman@29985 ` 633` huffman@29985 ` 634` ```end ```