src/HOL/Library/Univ_Poly.thy
 author chaieb Mon Feb 25 11:27:27 2008 +0100 (2008-02-25) changeset 26124 2514f0ade8bc child 26194 b9763c3272cb permissions -rw-r--r--
A library for univariate polynomials -- generalizes old Hyperreal/Poly.thy from reals to locales
 chaieb@26124 1 (* Title: Univ_Poly.thy chaieb@26124 2 ID: \$Id\$ chaieb@26124 3 Author: Amine Chaieb chaieb@26124 4 *) chaieb@26124 5 chaieb@26124 6 header{*Univariate Polynomials*} chaieb@26124 7 chaieb@26124 8 theory Univ_Poly chaieb@26124 9 imports Main chaieb@26124 10 begin chaieb@26124 11 chaieb@26124 12 text{* Application of polynomial as a function. *} chaieb@26124 13 chaieb@26124 14 fun (in semiring_0) poly :: "'a list => 'a => 'a" where chaieb@26124 15 poly_Nil: "poly [] x = 0" chaieb@26124 16 | poly_Cons: "poly (h#t) x = h + x * poly t x" chaieb@26124 17 chaieb@26124 18 chaieb@26124 19 subsection{*Arithmetic Operations on Polynomials*} chaieb@26124 20 chaieb@26124 21 text{*addition*} chaieb@26124 22 chaieb@26124 23 fun (in semiring_0) padd :: "'a list \ 'a list \ 'a list" (infixl "+++" 65) chaieb@26124 24 where chaieb@26124 25 padd_Nil: "[] +++ l2 = l2" chaieb@26124 26 | padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t chaieb@26124 27 else (h + hd l2)#(t +++ tl l2))" chaieb@26124 28 chaieb@26124 29 text{*Multiplication by a constant*} chaieb@26124 30 fun (in semiring_0) cmult :: "'a \ 'a list \ 'a list" (infixl "%*" 70) where chaieb@26124 31 cmult_Nil: "c %* [] = []" chaieb@26124 32 | cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)" chaieb@26124 33 chaieb@26124 34 text{*Multiplication by a polynomial*} chaieb@26124 35 fun (in semiring_0) pmult :: "'a list \ 'a list \ 'a list" (infixl "***" 70) chaieb@26124 36 where chaieb@26124 37 pmult_Nil: "[] *** l2 = []" chaieb@26124 38 | pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2 chaieb@26124 39 else (h %* l2) +++ ((0) # (t *** l2)))" chaieb@26124 40 chaieb@26124 41 text{*Repeated multiplication by a polynomial*} chaieb@26124 42 fun (in semiring_0) mulexp :: "nat \ 'a list \ 'a list \ 'a list" where chaieb@26124 43 mulexp_zero: "mulexp 0 p q = q" chaieb@26124 44 | mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q" chaieb@26124 45 chaieb@26124 46 text{*Exponential*} chaieb@26124 47 fun (in semiring_1) pexp :: "'a list \ nat \ 'a list" (infixl "%^" 80) where chaieb@26124 48 pexp_0: "p %^ 0 = [1]" chaieb@26124 49 | pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)" chaieb@26124 50 chaieb@26124 51 text{*Quotient related value of dividing a polynomial by x + a*} chaieb@26124 52 (* Useful for divisor properties in inductive proofs *) chaieb@26124 53 fun (in field) "pquot" :: "'a list \ 'a \ 'a list" where chaieb@26124 54 pquot_Nil: "pquot [] a= []" chaieb@26124 55 | pquot_Cons: "pquot (h#t) a = (if t = [] then [h] chaieb@26124 56 else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))" chaieb@26124 57 chaieb@26124 58 text{*normalization of polynomials (remove extra 0 coeff)*} chaieb@26124 59 fun (in semiring_0) pnormalize :: "'a list \ 'a list" where chaieb@26124 60 pnormalize_Nil: "pnormalize [] = []" chaieb@26124 61 | pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = []) chaieb@26124 62 then (if (h = 0) then [] else [h]) chaieb@26124 63 else (h#(pnormalize p)))" chaieb@26124 64 chaieb@26124 65 definition (in semiring_0) "pnormal p = ((pnormalize p = p) \ p \ [])" chaieb@26124 66 definition (in semiring_0) "nonconstant p = (pnormal p \ (\x. p \ [x]))" chaieb@26124 67 text{*Other definitions*} chaieb@26124 68 chaieb@26124 69 definition (in ring_1) chaieb@26124 70 poly_minus :: "'a list => 'a list" ("-- _" [80] 80) where chaieb@26124 71 "-- p = (- 1) %* p" chaieb@26124 72 chaieb@26124 73 definition (in semiring_0) chaieb@26124 74 divides :: "'a list \ 'a list \ bool" (infixl "divides" 70) where chaieb@26124 75 "p1 divides p2 = (\q. poly p2 = poly(p1 *** q))" chaieb@26124 76 chaieb@26124 77 --{*order of a polynomial*} chaieb@26124 78 definition (in ring_1) order :: "'a => 'a list => nat" where chaieb@26124 79 "order a p = (SOME n. ([-a, 1] %^ n) divides p & chaieb@26124 80 ~ (([-a, 1] %^ (Suc n)) divides p))" chaieb@26124 81 chaieb@26124 82 --{*degree of a polynomial*} chaieb@26124 83 definition (in semiring_0) degree :: "'a list => nat" where chaieb@26124 84 "degree p = length (pnormalize p) - 1" chaieb@26124 85 chaieb@26124 86 --{*squarefree polynomials --- NB with respect to real roots only.*} chaieb@26124 87 definition (in ring_1) chaieb@26124 88 rsquarefree :: "'a list => bool" where chaieb@26124 89 "rsquarefree p = (poly p \ poly [] & chaieb@26124 90 (\a. (order a p = 0) | (order a p = 1)))" chaieb@26124 91 chaieb@26124 92 context semiring_0 chaieb@26124 93 begin chaieb@26124 94 chaieb@26124 95 lemma padd_Nil2[simp]: "p +++ [] = p" chaieb@26124 96 by (induct p) auto chaieb@26124 97 chaieb@26124 98 lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)" chaieb@26124 99 by auto chaieb@26124 100 chaieb@26124 101 lemma pminus_Nil[simp]: "-- [] = []" chaieb@26124 102 by (simp add: poly_minus_def) chaieb@26124 103 chaieb@26124 104 lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" by simp chaieb@26124 105 end chaieb@26124 106 chaieb@26124 107 lemma (in semiring_1) poly_ident_mult[simp]: "1 %* t = t" by (induct "t", auto) chaieb@26124 108 chaieb@26124 109 lemma (in semiring_0) poly_simple_add_Cons[simp]: "[a] +++ ((0)#t) = (a#t)" chaieb@26124 110 by simp chaieb@26124 111 chaieb@26124 112 text{*Handy general properties*} chaieb@26124 113 chaieb@26124 114 lemma (in comm_semiring_0) padd_commut: "b +++ a = a +++ b" chaieb@26124 115 proof(induct b arbitrary: a) chaieb@26124 116 case Nil thus ?case by auto chaieb@26124 117 next chaieb@26124 118 case (Cons b bs a) thus ?case by (cases a, simp_all add: add_commute) chaieb@26124 119 qed chaieb@26124 120 chaieb@26124 121 lemma (in comm_semiring_0) padd_assoc: "\b c. (a +++ b) +++ c = a +++ (b +++ c)" chaieb@26124 122 apply (induct a arbitrary: b c) chaieb@26124 123 apply (simp, clarify) chaieb@26124 124 apply (case_tac b, simp_all add: add_ac) chaieb@26124 125 done chaieb@26124 126 chaieb@26124 127 lemma (in semiring_0) poly_cmult_distr: "a %* ( p +++ q) = (a %* p +++ a %* q)" chaieb@26124 128 apply (induct p arbitrary: q,simp) chaieb@26124 129 apply (case_tac q, simp_all add: right_distrib) chaieb@26124 130 done chaieb@26124 131 chaieb@26124 132 lemma (in ring_1) pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)" chaieb@26124 133 apply (induct "t", simp) chaieb@26124 134 apply (auto simp add: mult_zero_left poly_ident_mult padd_commut) chaieb@26124 135 apply (case_tac t, auto) chaieb@26124 136 done chaieb@26124 137 chaieb@26124 138 text{*properties of evaluation of polynomials.*} chaieb@26124 139 chaieb@26124 140 lemma (in semiring_0) poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x" chaieb@26124 141 proof(induct p1 arbitrary: p2) chaieb@26124 142 case Nil thus ?case by simp chaieb@26124 143 next chaieb@26124 144 case (Cons a as p2) thus ?case chaieb@26124 145 by (cases p2, simp_all add: add_ac right_distrib) chaieb@26124 146 qed chaieb@26124 147 chaieb@26124 148 lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x" chaieb@26124 149 apply (induct "p") chaieb@26124 150 apply (case_tac [2] "x=zero") chaieb@26124 151 apply (auto simp add: right_distrib mult_ac) chaieb@26124 152 done chaieb@26124 153 chaieb@26124 154 lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c*poly p x" chaieb@26124 155 by (induct p, auto simp add: right_distrib mult_ac) chaieb@26124 156 chaieb@26124 157 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)" chaieb@26124 158 apply (simp add: poly_minus_def) chaieb@26124 159 apply (auto simp add: poly_cmult minus_mult_left[symmetric]) chaieb@26124 160 done chaieb@26124 161 chaieb@26124 162 lemma (in comm_semiring_0) poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x" chaieb@26124 163 proof(induct p1 arbitrary: p2) chaieb@26124 164 case Nil thus ?case by simp chaieb@26124 165 next chaieb@26124 166 case (Cons a as p2) chaieb@26124 167 thus ?case by (cases as, chaieb@26124 168 simp_all add: poly_cmult poly_add left_distrib right_distrib mult_ac) chaieb@26124 169 qed chaieb@26124 170 chaieb@26124 171 class recpower_semiring = semiring + recpower chaieb@26124 172 class recpower_semiring_1 = semiring_1 + recpower chaieb@26124 173 class recpower_semiring_0 = semiring_0 + recpower chaieb@26124 174 class recpower_ring = ring + recpower chaieb@26124 175 class recpower_ring_1 = ring_1 + recpower chaieb@26124 176 subclass (in recpower_ring_1) recpower_ring by unfold_locales chaieb@26124 177 subclass (in recpower_ring_1) recpower_ring by unfold_locales chaieb@26124 178 class recpower_comm_semiring_1 = recpower + comm_semiring_1 chaieb@26124 179 class recpower_comm_ring_1 = recpower + comm_ring_1 chaieb@26124 180 subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales chaieb@26124 181 class recpower_idom = recpower + idom chaieb@26124 182 subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales chaieb@26124 183 class idom_char_0 = idom + ring_char_0 chaieb@26124 184 class recpower_idom_char_0 = recpower + idom_char_0 chaieb@26124 185 subclass (in recpower_idom_char_0) recpower_idom by unfold_locales chaieb@26124 186 chaieb@26124 187 lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n" chaieb@26124 188 apply (induct "n") chaieb@26124 189 apply (auto simp add: poly_cmult poly_mult power_Suc) chaieb@26124 190 done chaieb@26124 191 chaieb@26124 192 text{*More Polynomial Evaluation Lemmas*} chaieb@26124 193 chaieb@26124 194 lemma (in semiring_0) poly_add_rzero[simp]: "poly (a +++ []) x = poly a x" chaieb@26124 195 by simp chaieb@26124 196 chaieb@26124 197 lemma (in comm_semiring_0) poly_mult_assoc: "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x" chaieb@26124 198 by (simp add: poly_mult mult_assoc) chaieb@26124 199 chaieb@26124 200 lemma (in semiring_0) poly_mult_Nil2[simp]: "poly (p *** []) x = 0" chaieb@26124 201 by (induct "p", auto) chaieb@26124 202 chaieb@26124 203 lemma (in comm_semiring_1) poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x" chaieb@26124 204 apply (induct "n") chaieb@26124 205 apply (auto simp add: poly_mult mult_assoc) chaieb@26124 206 done chaieb@26124 207 chaieb@26124 208 subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides chaieb@26124 209 @{term "p(x)"} *} chaieb@26124 210 chaieb@26124 211 lemma (in comm_ring_1) lemma_poly_linear_rem: "\h. \q r. h#t = [r] +++ [-a, 1] *** q" chaieb@26124 212 proof(induct t) chaieb@26124 213 case Nil chaieb@26124 214 {fix h have "[h] = [h] +++ [- a, 1] *** []" by simp} chaieb@26124 215 thus ?case by blast chaieb@26124 216 next chaieb@26124 217 case (Cons x xs) chaieb@26124 218 {fix h chaieb@26124 219 from Cons.hyps[rule_format, of x] chaieb@26124 220 obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast chaieb@26124 221 have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)" chaieb@26124 222 using qr by(cases q, simp_all add: ring_simps diff_def[symmetric] chaieb@26124 223 minus_mult_left[symmetric] right_minus) chaieb@26124 224 hence "\q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast} chaieb@26124 225 thus ?case by blast chaieb@26124 226 qed chaieb@26124 227 chaieb@26124 228 lemma (in comm_ring_1) poly_linear_rem: "\q r. h#t = [r] +++ [-a, 1] *** q" chaieb@26124 229 by (cut_tac t = t and a = a in lemma_poly_linear_rem, auto) chaieb@26124 230 chaieb@26124 231 chaieb@26124 232 lemma (in comm_ring_1) poly_linear_divides: "(poly p a = 0) = ((p = []) | (\q. p = [-a, 1] *** q))" chaieb@26124 233 proof- chaieb@26124 234 {assume p: "p = []" hence ?thesis by simp} chaieb@26124 235 moreover chaieb@26124 236 {fix x xs assume p: "p = x#xs" chaieb@26124 237 {fix q assume "p = [-a, 1] *** q" hence "poly p a = 0" chaieb@26124 238 by (simp add: poly_add poly_cmult minus_mult_left[symmetric])} chaieb@26124 239 moreover chaieb@26124 240 {assume p0: "poly p a = 0" chaieb@26124 241 from poly_linear_rem[of x xs a] obtain q r chaieb@26124 242 where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast chaieb@26124 243 have "r = 0" using p0 by (simp only: p qr poly_mult poly_add) simp chaieb@26124 244 hence "\q. p = [- a, 1] *** q" using p qr apply - apply (rule exI[where x=q])apply auto apply (cases q) apply auto done} chaieb@26124 245 ultimately have ?thesis using p by blast} chaieb@26124 246 ultimately show ?thesis by (cases p, auto) chaieb@26124 247 qed chaieb@26124 248 chaieb@26124 249 lemma (in semiring_0) lemma_poly_length_mult[simp]: "\h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)" chaieb@26124 250 by (induct "p", auto) chaieb@26124 251 chaieb@26124 252 lemma (in semiring_0) lemma_poly_length_mult2[simp]: "\h k. length (k %* p +++ (h # p)) = Suc (length p)" chaieb@26124 253 by (induct "p", auto) chaieb@26124 254 chaieb@26124 255 lemma (in ring_1) poly_length_mult[simp]: "length([-a,1] *** q) = Suc (length q)" chaieb@26124 256 by auto chaieb@26124 257 chaieb@26124 258 subsection{*Polynomial length*} chaieb@26124 259 chaieb@26124 260 lemma (in semiring_0) poly_cmult_length[simp]: "length (a %* p) = length p" chaieb@26124 261 by (induct "p", auto) chaieb@26124 262 chaieb@26124 263 lemma (in semiring_0) poly_add_length: "length (p1 +++ p2) = max (length p1) (length p2)" chaieb@26124 264 apply (induct p1 arbitrary: p2, simp_all) chaieb@26124 265 apply arith chaieb@26124 266 done chaieb@26124 267 chaieb@26124 268 lemma (in semiring_0) poly_root_mult_length[simp]: "length([a,b] *** p) = Suc (length p)" chaieb@26124 269 by (simp add: poly_add_length) chaieb@26124 270 chaieb@26124 271 lemma (in idom) poly_mult_not_eq_poly_Nil[simp]: chaieb@26124 272 "poly (p *** q) x \ poly [] x \ poly p x \ poly [] x \ poly q x \ poly [] x" chaieb@26124 273 by (auto simp add: poly_mult) chaieb@26124 274 chaieb@26124 275 lemma (in idom) poly_mult_eq_zero_disj: "poly (p *** q) x = 0 \ poly p x = 0 \ poly q x = 0" chaieb@26124 276 by (auto simp add: poly_mult) chaieb@26124 277 chaieb@26124 278 text{*Normalisation Properties*} chaieb@26124 279 chaieb@26124 280 lemma (in semiring_0) poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)" chaieb@26124 281 by (induct "p", auto) chaieb@26124 282 chaieb@26124 283 text{*A nontrivial polynomial of degree n has no more than n roots*} chaieb@26124 284 lemma (in idom) poly_roots_index_lemma: chaieb@26124 285 assumes p: "poly p x \ poly [] x" and n: "length p = n" chaieb@26124 286 shows "\i. \x. poly p x = 0 \ (\m\n. x = i m)" chaieb@26124 287 using p n chaieb@26124 288 proof(induct n arbitrary: p x) chaieb@26124 289 case 0 thus ?case by simp chaieb@26124 290 next chaieb@26124 291 case (Suc n p x) chaieb@26124 292 {assume C: "\i. \x. poly p x = 0 \ (\m\Suc n. x \ i m)" chaieb@26124 293 from Suc.prems have p0: "poly p x \ 0" "p\ []" by auto chaieb@26124 294 from p0(1)[unfolded poly_linear_divides[of p x]] chaieb@26124 295 have "\q. p \ [- x, 1] *** q" by blast chaieb@26124 296 from C obtain a where a: "poly p a = 0" by blast chaieb@26124 297 from a[unfolded poly_linear_divides[of p a]] p0(2) chaieb@26124 298 obtain q where q: "p = [-a, 1] *** q" by blast chaieb@26124 299 have lg: "length q = n" using q Suc.prems(2) by simp chaieb@26124 300 from q p0 have qx: "poly q x \ poly [] x" chaieb@26124 301 by (auto simp add: poly_mult poly_add poly_cmult) chaieb@26124 302 from Suc.hyps[OF qx lg] obtain i where chaieb@26124 303 i: "\x. poly q x = 0 \ (\m\n. x = i m)" by blast chaieb@26124 304 let ?i = "\m. if m = Suc n then a else i m" chaieb@26124 305 from C[of ?i] obtain y where y: "poly p y = 0" "\m\ Suc n. y \ ?i m" chaieb@26124 306 by blast chaieb@26124 307 from y have "y = a \ poly q y = 0" chaieb@26124 308 by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: ring_simps) chaieb@26124 309 with i[rule_format, of y] y(1) y(2) have False apply auto chaieb@26124 310 apply (erule_tac x="m" in allE) chaieb@26124 311 apply auto chaieb@26124 312 done} chaieb@26124 313 thus ?case by blast chaieb@26124 314 qed chaieb@26124 315 chaieb@26124 316 chaieb@26124 317 lemma (in idom) poly_roots_index_length: "poly p x \ poly [] x ==> chaieb@26124 318 \i. \x. (poly p x = 0) --> (\n. n \ length p & x = i n)" chaieb@26124 319 by (blast intro: poly_roots_index_lemma) chaieb@26124 320 chaieb@26124 321 lemma (in idom) poly_roots_finite_lemma: "poly p x \ poly [] x ==> chaieb@26124 322 \N i. \x. (poly p x = 0) --> (\n. (n::nat) < N & x = i n)" chaieb@26124 323 apply (drule poly_roots_index_length, safe) chaieb@26124 324 apply (rule_tac x = "Suc (length p)" in exI) chaieb@26124 325 apply (rule_tac x = i in exI) chaieb@26124 326 apply (simp add: less_Suc_eq_le) chaieb@26124 327 done chaieb@26124 328 chaieb@26124 329 chaieb@26124 330 lemma (in idom) idom_finite_lemma: chaieb@26124 331 assumes P: "\x. P x --> (\n. n < length j & x = j!n)" chaieb@26124 332 shows "finite {x. P x}" chaieb@26124 333 proof- chaieb@26124 334 let ?M = "{x. P x}" chaieb@26124 335 let ?N = "set j" chaieb@26124 336 have "?M \ ?N" using P by auto chaieb@26124 337 thus ?thesis using finite_subset by auto chaieb@26124 338 qed chaieb@26124 339 chaieb@26124 340 chaieb@26124 341 lemma (in idom) poly_roots_finite_lemma: "poly p x \ poly [] x ==> chaieb@26124 342 \i. \x. (poly p x = 0) --> x \ set i" chaieb@26124 343 apply (drule poly_roots_index_length, safe) chaieb@26124 344 apply (rule_tac x="map (\n. i n) [0 ..< Suc (length p)]" in exI) chaieb@26124 345 apply (auto simp add: image_iff) chaieb@26124 346 apply (erule_tac x="x" in allE, clarsimp) chaieb@26124 347 by (case_tac "n=length p", auto simp add: order_le_less) chaieb@26124 348 chaieb@26124 349 lemma UNIV_nat_infinite: "\ finite (UNIV :: nat set)" chaieb@26124 350 unfolding finite_conv_nat_seg_image chaieb@26124 351 proof(auto simp add: expand_set_eq image_iff) chaieb@26124 352 fix n::nat and f:: "nat \ nat" chaieb@26124 353 let ?N = "{i. i < n}" chaieb@26124 354 let ?fN = "f ` ?N" chaieb@26124 355 let ?y = "Max ?fN + 1" chaieb@26124 356 from nat_seg_image_imp_finite[of "?fN" "f" n] chaieb@26124 357 have thfN: "finite ?fN" by simp chaieb@26124 358 {assume "n =0" hence "\x. \xa f xa" by auto} chaieb@26124 359 moreover chaieb@26124 360 {assume nz: "n \ 0" chaieb@26124 361 hence thne: "?fN \ {}" by (auto simp add: neq0_conv) chaieb@26124 362 have "\x\ ?fN. Max ?fN \ x" using nz Max_ge_iff[OF thfN thne] by auto chaieb@26124 363 hence "\x\ ?fN. ?y > x" by auto chaieb@26124 364 hence "?y \ ?fN" by auto chaieb@26124 365 hence "\x. \xa f xa" by auto } chaieb@26124 366 ultimately show "\x. \xa f xa" by blast chaieb@26124 367 qed chaieb@26124 368 chaieb@26124 369 lemma (in ring_char_0) UNIV_ring_char_0_infinte: chaieb@26124 370 "\ (finite (UNIV:: 'a set))" chaieb@26124 371 proof chaieb@26124 372 assume F: "finite (UNIV :: 'a set)" chaieb@26124 373 have th0: "of_nat ` UNIV \ UNIV" by simp chaieb@26124 374 from finite_subset[OF th0] have th: "finite (of_nat ` UNIV :: 'a set)" . chaieb@26124 375 have th': "inj_on (of_nat::nat \ 'a) (UNIV)" chaieb@26124 376 unfolding inj_on_def by auto chaieb@26124 377 from finite_imageD[OF th th'] UNIV_nat_infinite chaieb@26124 378 show False by blast chaieb@26124 379 qed chaieb@26124 380 chaieb@26124 381 lemma (in idom_char_0) poly_roots_finite: "(poly p \ poly []) = chaieb@26124 382 finite {x. poly p x = 0}" chaieb@26124 383 proof chaieb@26124 384 assume H: "poly p \ poly []" chaieb@26124 385 show "finite {x. poly p x = (0::'a)}" chaieb@26124 386 using H chaieb@26124 387 apply - chaieb@26124 388 apply (erule contrapos_np, rule ext) chaieb@26124 389 apply (rule ccontr) chaieb@26124 390 apply (clarify dest!: poly_roots_finite_lemma) chaieb@26124 391 using finite_subset chaieb@26124 392 proof- chaieb@26124 393 fix x i chaieb@26124 394 assume F: "\ finite {x. poly p x = (0\'a)}" chaieb@26124 395 and P: "\x. poly p x = (0\'a) \ x \ set i" chaieb@26124 396 let ?M= "{x. poly p x = (0\'a)}" chaieb@26124 397 from P have "?M \ set i" by auto chaieb@26124 398 with finite_subset F show False by auto chaieb@26124 399 qed chaieb@26124 400 next chaieb@26124 401 assume F: "finite {x. poly p x = (0\'a)}" chaieb@26124 402 show "poly p \ poly []" using F UNIV_ring_char_0_infinte by auto chaieb@26124 403 qed chaieb@26124 404 chaieb@26124 405 text{*Entirety and Cancellation for polynomials*} chaieb@26124 406 chaieb@26124 407 lemma (in idom_char_0) poly_entire_lemma: "\poly p \ poly [] ; poly q \ poly [] \ chaieb@26124 408 \ poly (p *** q) \ poly []" chaieb@26124 409 by (auto simp add: poly_roots_finite poly_mult Collect_disj_eq) chaieb@26124 410 chaieb@26124 411 lemma (in idom_char_0) poly_entire: "poly (p *** q) = poly [] \(poly p = poly []) | (poly q = poly [])" chaieb@26124 412 apply (auto intro: ext dest: fun_cong simp add: poly_entire_lemma poly_mult) chaieb@26124 413 apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst]) chaieb@26124 414 done chaieb@26124 415 chaieb@26124 416 lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \ poly []) = ((poly p \ poly []) & (poly q \ poly []))" chaieb@26124 417 by (simp add: poly_entire) chaieb@26124 418 chaieb@26124 419 lemma fun_eq: " (f = g) = (\x. f x = g x)" chaieb@26124 420 by (auto intro!: ext) chaieb@26124 421 chaieb@26124 422 lemma (in comm_ring_1) poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)" chaieb@26124 423 by (auto simp add: ring_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric]) chaieb@26124 424 chaieb@26124 425 lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))" chaieb@26124 426 by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric]) chaieb@26124 427 chaieb@26124 428 subclass (in idom_char_0) comm_ring_1 by unfold_locales chaieb@26124 429 lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)" chaieb@26124 430 proof- chaieb@26124 431 have "poly (p *** q) = poly (p *** r) \ poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff) chaieb@26124 432 also have "\ \ poly p = poly [] | poly q = poly r" chaieb@26124 433 by (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff) chaieb@26124 434 finally show ?thesis . chaieb@26124 435 qed chaieb@26124 436 chaieb@26124 437 lemma (in recpower_idom) poly_exp_eq_zero[simp]: chaieb@26124 438 "(poly (p %^ n) = poly []) = (poly p = poly [] & n \ 0)" chaieb@26124 439 apply (simp only: fun_eq add: all_simps [symmetric]) chaieb@26124 440 apply (rule arg_cong [where f = All]) chaieb@26124 441 apply (rule ext) chaieb@26124 442 apply (induct_tac "n") chaieb@26124 443 apply (simp add: poly_exp) chaieb@26124 444 using zero_neq_one apply blast chaieb@26124 445 apply (auto simp add: poly_exp poly_mult) chaieb@26124 446 done chaieb@26124 447 chaieb@26124 448 lemma (in semiring_1) one_neq_zero[simp]: "1 \ 0" using zero_neq_one by blast chaieb@26124 449 lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \ poly []" chaieb@26124 450 apply (simp add: fun_eq) chaieb@26124 451 apply (rule_tac x = "minus one a" in exI) chaieb@26124 452 apply (unfold diff_minus) chaieb@26124 453 apply (subst add_commute) chaieb@26124 454 apply (subst add_assoc) chaieb@26124 455 apply simp chaieb@26124 456 done chaieb@26124 457 chaieb@26124 458 lemma (in recpower_idom) poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \ poly [])" chaieb@26124 459 by auto chaieb@26124 460 chaieb@26124 461 text{*A more constructive notion of polynomials being trivial*} chaieb@26124 462 chaieb@26124 463 lemma (in idom_char_0) poly_zero_lemma': "poly (h # t) = poly [] ==> h = 0 & poly t = poly []" chaieb@26124 464 apply(simp add: fun_eq) chaieb@26124 465 apply (case_tac "h = zero") chaieb@26124 466 apply (drule_tac [2] x = zero in spec, auto) chaieb@26124 467 apply (cases "poly t = poly []", simp) chaieb@26124 468 proof- chaieb@26124 469 fix x chaieb@26124 470 assume H: "\x. x = (0\'a) \ poly t x = (0\'a)" and pnz: "poly t \ poly []" chaieb@26124 471 let ?S = "{x. poly t x = 0}" chaieb@26124 472 from H have "\x. x \0 \ poly t x = 0" by blast chaieb@26124 473 hence th: "?S \ UNIV - {0}" by auto chaieb@26124 474 from poly_roots_finite pnz have th': "finite ?S" by blast chaieb@26124 475 from finite_subset[OF th th'] UNIV_ring_char_0_infinte chaieb@26124 476 show "poly t x = (0\'a)" by simp chaieb@26124 477 qed chaieb@26124 478 chaieb@26124 479 lemma (in idom_char_0) poly_zero: "(poly p = poly []) = list_all (%c. c = 0) p" chaieb@26124 480 apply (induct "p", simp) chaieb@26124 481 apply (rule iffI) chaieb@26124 482 apply (drule poly_zero_lemma', auto) chaieb@26124 483 done chaieb@26124 484 chaieb@26124 485 lemma (in idom_char_0) poly_0: "list_all (\c. c = 0) p \ poly p x = 0" chaieb@26124 486 unfolding poly_zero[symmetric] by simp chaieb@26124 487 chaieb@26124 488 chaieb@26124 489 chaieb@26124 490 text{*Basics of divisibility.*} chaieb@26124 491 chaieb@26124 492 lemma (in idom) poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)" chaieb@26124 493 apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric]) chaieb@26124 494 apply (drule_tac x = "uminus a" in spec) chaieb@26124 495 apply (simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric]) chaieb@26124 496 apply (cases "p = []") chaieb@26124 497 apply (rule exI[where x="[]"]) chaieb@26124 498 apply simp chaieb@26124 499 apply (cases "q = []") chaieb@26124 500 apply (erule allE[where x="[]"], simp) chaieb@26124 501 chaieb@26124 502 apply clarsimp chaieb@26124 503 apply (cases "\q\'a list. p = a %* q +++ ((0\'a) # q)") chaieb@26124 504 apply (clarsimp simp add: poly_add poly_cmult) chaieb@26124 505 apply (rule_tac x="qa" in exI) chaieb@26124 506 apply (simp add: left_distrib [symmetric]) chaieb@26124 507 apply clarsimp chaieb@26124 508 chaieb@26124 509 apply (auto simp add: right_minus poly_linear_divides poly_add poly_cmult left_distrib [symmetric]) chaieb@26124 510 apply (rule_tac x = "pmult qa q" in exI) chaieb@26124 511 apply (rule_tac [2] x = "pmult p qa" in exI) chaieb@26124 512 apply (auto simp add: poly_add poly_mult poly_cmult mult_ac) chaieb@26124 513 done chaieb@26124 514 chaieb@26124 515 lemma (in comm_semiring_1) poly_divides_refl[simp]: "p divides p" chaieb@26124 516 apply (simp add: divides_def) chaieb@26124 517 apply (rule_tac x = "[one]" in exI) chaieb@26124 518 apply (auto simp add: poly_mult fun_eq) chaieb@26124 519 done chaieb@26124 520 chaieb@26124 521 lemma (in comm_semiring_1) poly_divides_trans: "[| p divides q; q divides r |] ==> p divides r" chaieb@26124 522 apply (simp add: divides_def, safe) chaieb@26124 523 apply (rule_tac x = "pmult qa qaa" in exI) chaieb@26124 524 apply (auto simp add: poly_mult fun_eq mult_assoc) chaieb@26124 525 done chaieb@26124 526 chaieb@26124 527 chaieb@26124 528 lemma (in recpower_comm_semiring_1) poly_divides_exp: "m \ n ==> (p %^ m) divides (p %^ n)" chaieb@26124 529 apply (auto simp add: le_iff_add) chaieb@26124 530 apply (induct_tac k) chaieb@26124 531 apply (rule_tac [2] poly_divides_trans) chaieb@26124 532 apply (auto simp add: divides_def) chaieb@26124 533 apply (rule_tac x = p in exI) chaieb@26124 534 apply (auto simp add: poly_mult fun_eq mult_ac) chaieb@26124 535 done chaieb@26124 536 chaieb@26124 537 lemma (in recpower_comm_semiring_1) poly_exp_divides: "[| (p %^ n) divides q; m\n |] ==> (p %^ m) divides q" chaieb@26124 538 by (blast intro: poly_divides_exp poly_divides_trans) chaieb@26124 539 chaieb@26124 540 lemma (in comm_semiring_0) poly_divides_add: chaieb@26124 541 "[| p divides q; p divides r |] ==> p divides (q +++ r)" chaieb@26124 542 apply (simp add: divides_def, auto) chaieb@26124 543 apply (rule_tac x = "padd qa qaa" in exI) chaieb@26124 544 apply (auto simp add: poly_add fun_eq poly_mult right_distrib) chaieb@26124 545 done chaieb@26124 546 chaieb@26124 547 lemma (in comm_ring_1) poly_divides_diff: chaieb@26124 548 "[| p divides q; p divides (q +++ r) |] ==> p divides r" chaieb@26124 549 apply (simp add: divides_def, auto) chaieb@26124 550 apply (rule_tac x = "padd qaa (poly_minus qa)" in exI) chaieb@26124 551 apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib compare_rls add_ac) chaieb@26124 552 done chaieb@26124 553 chaieb@26124 554 lemma (in comm_ring_1) poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q" chaieb@26124 555 apply (erule poly_divides_diff) chaieb@26124 556 apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac) chaieb@26124 557 done chaieb@26124 558 chaieb@26124 559 lemma (in semiring_0) poly_divides_zero: "poly p = poly [] ==> q divides p" chaieb@26124 560 apply (simp add: divides_def) chaieb@26124 561 apply (rule exI[where x="[]"]) chaieb@26124 562 apply (auto simp add: fun_eq poly_mult) chaieb@26124 563 done chaieb@26124 564 chaieb@26124 565 lemma (in semiring_0) poly_divides_zero2[simp]: "q divides []" chaieb@26124 566 apply (simp add: divides_def) chaieb@26124 567 apply (rule_tac x = "[]" in exI) chaieb@26124 568 apply (auto simp add: fun_eq) chaieb@26124 569 done chaieb@26124 570 chaieb@26124 571 text{*At last, we can consider the order of a root.*} chaieb@26124 572 chaieb@26124 573 lemma (in idom_char_0) poly_order_exists_lemma: chaieb@26124 574 assumes lp: "length p = d" and p: "poly p \ poly []" chaieb@26124 575 shows "\n q. p = mulexp n [-a, 1] q \ poly q a \ 0" chaieb@26124 576 using lp p chaieb@26124 577 proof(induct d arbitrary: p) chaieb@26124 578 case 0 thus ?case by simp chaieb@26124 579 next chaieb@26124 580 case (Suc n p) chaieb@26124 581 {assume p0: "poly p a = 0" chaieb@26124 582 from Suc.prems have h: "length p = Suc n" "poly p \ poly []" by blast chaieb@26124 583 hence pN: "p \ []" by - (rule ccontr, simp) chaieb@26124 584 from p0[unfolded poly_linear_divides] pN obtain q where chaieb@26124 585 q: "p = [-a, 1] *** q" by blast chaieb@26124 586 from q h p0 have qh: "length q = n" "poly q \ poly []" chaieb@26124 587 apply - chaieb@26124 588 apply simp chaieb@26124 589 apply (simp only: fun_eq) chaieb@26124 590 apply (rule ccontr) chaieb@26124 591 apply (simp add: fun_eq poly_add poly_cmult minus_mult_left[symmetric]) chaieb@26124 592 done chaieb@26124 593 from Suc.hyps[OF qh] obtain m r where chaieb@26124 594 mr: "q = mulexp m [-a,1] r" "poly r a \ 0" by blast chaieb@26124 595 from mr q have "p = mulexp (Suc m) [-a,1] r \ poly r a \ 0" by simp chaieb@26124 596 hence ?case by blast} chaieb@26124 597 moreover chaieb@26124 598 {assume p0: "poly p a \ 0" chaieb@26124 599 hence ?case using Suc.prems apply simp by (rule exI[where x="0::nat"], simp)} chaieb@26124 600 ultimately show ?case by blast chaieb@26124 601 qed chaieb@26124 602 chaieb@26124 603 chaieb@26124 604 lemma (in recpower_comm_semiring_1) poly_mulexp: "poly (mulexp n p q) x = (poly p x) ^ n * poly q x" chaieb@26124 605 by(induct n, auto simp add: poly_mult power_Suc mult_ac) chaieb@26124 606 chaieb@26124 607 lemma (in comm_semiring_1) divides_left_mult: chaieb@26124 608 assumes d:"(p***q) divides r" shows "p divides r \ q divides r" chaieb@26124 609 proof- chaieb@26124 610 from d obtain t where r:"poly r = poly (p***q *** t)" chaieb@26124 611 unfolding divides_def by blast chaieb@26124 612 hence "poly r = poly (p *** (q *** t))" chaieb@26124 613 "poly r = poly (q *** (p***t))" by(auto simp add: fun_eq poly_mult mult_ac) chaieb@26124 614 thus ?thesis unfolding divides_def by blast chaieb@26124 615 qed chaieb@26124 616 chaieb@26124 617 chaieb@26124 618 chaieb@26124 619 (* FIXME: Tidy up *) chaieb@26124 620 chaieb@26124 621 lemma (in recpower_semiring_1) chaieb@26124 622 zero_power_iff: "0 ^ n = (if n = 0 then 1 else 0)" chaieb@26124 623 by (induct n, simp_all add: power_Suc) chaieb@26124 624 chaieb@26124 625 lemma (in recpower_idom_char_0) poly_order_exists: chaieb@26124 626 assumes lp: "length p = d" and p0: "poly p \ poly []" chaieb@26124 627 shows "\n. ([-a, 1] %^ n) divides p & ~(([-a, 1] %^ (Suc n)) divides p)" chaieb@26124 628 proof- chaieb@26124 629 let ?poly = poly chaieb@26124 630 let ?mulexp = mulexp chaieb@26124 631 let ?pexp = pexp chaieb@26124 632 from lp p0 chaieb@26124 633 show ?thesis chaieb@26124 634 apply - chaieb@26124 635 apply (drule poly_order_exists_lemma [where a=a], assumption, clarify) chaieb@26124 636 apply (rule_tac x = n in exI, safe) chaieb@26124 637 apply (unfold divides_def) chaieb@26124 638 apply (rule_tac x = q in exI) chaieb@26124 639 apply (induct_tac "n", simp) chaieb@26124 640 apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac) chaieb@26124 641 apply safe chaieb@26124 642 apply (subgoal_tac "?poly (?mulexp n [uminus a, one] q) \ ?poly (pmult (?pexp [uminus a, one] (Suc n)) qa)") chaieb@26124 643 apply simp chaieb@26124 644 apply (induct_tac "n") chaieb@26124 645 apply (simp del: pmult_Cons pexp_Suc) chaieb@26124 646 apply (erule_tac Q = "?poly q a = zero" in contrapos_np) chaieb@26124 647 apply (simp add: poly_add poly_cmult minus_mult_left[symmetric]) chaieb@26124 648 apply (rule pexp_Suc [THEN ssubst]) chaieb@26124 649 apply (rule ccontr) chaieb@26124 650 apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc) chaieb@26124 651 done chaieb@26124 652 qed chaieb@26124 653 chaieb@26124 654 chaieb@26124 655 lemma (in semiring_1) poly_one_divides[simp]: "[1] divides p" chaieb@26124 656 by (simp add: divides_def, auto) chaieb@26124 657 chaieb@26124 658 lemma (in recpower_idom_char_0) poly_order: "poly p \ poly [] chaieb@26124 659 ==> EX! n. ([-a, 1] %^ n) divides p & chaieb@26124 660 ~(([-a, 1] %^ (Suc n)) divides p)" chaieb@26124 661 apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc) chaieb@26124 662 apply (cut_tac x = y and y = n in less_linear) chaieb@26124 663 apply (drule_tac m = n in poly_exp_divides) chaieb@26124 664 apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides] chaieb@26124 665 simp del: pmult_Cons pexp_Suc) chaieb@26124 666 done chaieb@26124 667 chaieb@26124 668 text{*Order*} chaieb@26124 669 chaieb@26124 670 lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n" chaieb@26124 671 by (blast intro: someI2) chaieb@26124 672 chaieb@26124 673 lemma (in recpower_idom_char_0) order: chaieb@26124 674 "(([-a, 1] %^ n) divides p & chaieb@26124 675 ~(([-a, 1] %^ (Suc n)) divides p)) = chaieb@26124 676 ((n = order a p) & ~(poly p = poly []))" chaieb@26124 677 apply (unfold order_def) chaieb@26124 678 apply (rule iffI) chaieb@26124 679 apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order) chaieb@26124 680 apply (blast intro!: poly_order [THEN [2] some1_equalityD]) chaieb@26124 681 done chaieb@26124 682 chaieb@26124 683 lemma (in recpower_idom_char_0) order2: "[| poly p \ poly [] |] chaieb@26124 684 ==> ([-a, 1] %^ (order a p)) divides p & chaieb@26124 685 ~(([-a, 1] %^ (Suc(order a p))) divides p)" chaieb@26124 686 by (simp add: order del: pexp_Suc) chaieb@26124 687 chaieb@26124 688 lemma (in recpower_idom_char_0) order_unique: "[| poly p \ poly []; ([-a, 1] %^ n) divides p; chaieb@26124 689 ~(([-a, 1] %^ (Suc n)) divides p) chaieb@26124 690 |] ==> (n = order a p)" chaieb@26124 691 by (insert order [of a n p], auto) chaieb@26124 692 chaieb@26124 693 lemma (in recpower_idom_char_0) order_unique_lemma: "(poly p \ poly [] & ([-a, 1] %^ n) divides p & chaieb@26124 694 ~(([-a, 1] %^ (Suc n)) divides p)) chaieb@26124 695 ==> (n = order a p)" chaieb@26124 696 by (blast intro: order_unique) chaieb@26124 697 chaieb@26124 698 lemma (in ring_1) order_poly: "poly p = poly q ==> order a p = order a q" chaieb@26124 699 by (auto simp add: fun_eq divides_def poly_mult order_def) chaieb@26124 700 chaieb@26124 701 lemma (in semiring_1) pexp_one[simp]: "p %^ (Suc 0) = p" chaieb@26124 702 apply (induct "p") chaieb@26124 703 apply (auto simp add: numeral_1_eq_1) chaieb@26124 704 done chaieb@26124 705 chaieb@26124 706 lemma (in comm_ring_1) lemma_order_root: chaieb@26124 707 " 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p chaieb@26124 708 \ poly p a = 0" chaieb@26124 709 apply (induct n arbitrary: a p, blast) chaieb@26124 710 apply (auto simp add: divides_def poly_mult simp del: pmult_Cons) chaieb@26124 711 done chaieb@26124 712 chaieb@26124 713 lemma (in recpower_idom_char_0) order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \ 0)" chaieb@26124 714 proof- chaieb@26124 715 let ?poly = poly chaieb@26124 716 show ?thesis chaieb@26124 717 apply (case_tac "?poly p = ?poly []", auto) chaieb@26124 718 apply (simp add: poly_linear_divides del: pmult_Cons, safe) chaieb@26124 719 apply (drule_tac [!] a = a in order2) chaieb@26124 720 apply (rule ccontr) chaieb@26124 721 apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast) chaieb@26124 722 using neq0_conv chaieb@26124 723 apply (blast intro: lemma_order_root) chaieb@26124 724 done chaieb@26124 725 qed chaieb@26124 726 chaieb@26124 727 lemma (in recpower_idom_char_0) order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \ order a p)" chaieb@26124 728 proof- chaieb@26124 729 let ?poly = poly chaieb@26124 730 show ?thesis chaieb@26124 731 apply (case_tac "?poly p = ?poly []", auto) chaieb@26124 732 apply (simp add: divides_def fun_eq poly_mult) chaieb@26124 733 apply (rule_tac x = "[]" in exI) chaieb@26124 734 apply (auto dest!: order2 [where a=a] chaieb@26124 735 intro: poly_exp_divides simp del: pexp_Suc) chaieb@26124 736 done chaieb@26124 737 qed chaieb@26124 738 chaieb@26124 739 lemma (in recpower_idom_char_0) order_decomp: chaieb@26124 740 "poly p \ poly [] chaieb@26124 741 ==> \q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) & chaieb@26124 742 ~([-a, 1] divides q)" chaieb@26124 743 apply (unfold divides_def) chaieb@26124 744 apply (drule order2 [where a = a]) chaieb@26124 745 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe) chaieb@26124 746 apply (rule_tac x = q in exI, safe) chaieb@26124 747 apply (drule_tac x = qa in spec) chaieb@26124 748 apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons) chaieb@26124 749 done chaieb@26124 750 chaieb@26124 751 text{*Important composition properties of orders.*} chaieb@26124 752 lemma order_mult: "poly (p *** q) \ poly [] chaieb@26124 753 ==> order a (p *** q) = order a p + order (a::'a::{recpower_idom_char_0}) q" chaieb@26124 754 apply (cut_tac a = a and p = "p *** q" and n = "order a p + order a q" in order) chaieb@26124 755 apply (auto simp add: poly_entire simp del: pmult_Cons) chaieb@26124 756 apply (drule_tac a = a in order2)+ chaieb@26124 757 apply safe chaieb@26124 758 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) chaieb@26124 759 apply (rule_tac x = "qa *** qaa" in exI) chaieb@26124 760 apply (simp add: poly_mult mult_ac del: pmult_Cons) chaieb@26124 761 apply (drule_tac a = a in order_decomp)+ chaieb@26124 762 apply safe chaieb@26124 763 apply (subgoal_tac "[-a,1] divides (qa *** qaa) ") chaieb@26124 764 apply (simp add: poly_primes del: pmult_Cons) chaieb@26124 765 apply (auto simp add: divides_def simp del: pmult_Cons) chaieb@26124 766 apply (rule_tac x = qb in exI) chaieb@26124 767 apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))") chaieb@26124 768 apply (drule poly_mult_left_cancel [THEN iffD1], force) chaieb@26124 769 apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ") chaieb@26124 770 apply (drule poly_mult_left_cancel [THEN iffD1], force) chaieb@26124 771 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) chaieb@26124 772 done chaieb@26124 773 chaieb@26124 774 lemma (in recpower_idom_char_0) order_mult: chaieb@26124 775 assumes pq0: "poly (p *** q) \ poly []" chaieb@26124 776 shows "order a (p *** q) = order a p + order a q" chaieb@26124 777 proof- chaieb@26124 778 let ?order = order chaieb@26124 779 let ?divides = "op divides" chaieb@26124 780 let ?poly = poly chaieb@26124 781 from pq0 chaieb@26124 782 show ?thesis chaieb@26124 783 apply (cut_tac a = a and p = "pmult p q" and n = "?order a p + ?order a q" in order) chaieb@26124 784 apply (auto simp add: poly_entire simp del: pmult_Cons) chaieb@26124 785 apply (drule_tac a = a in order2)+ chaieb@26124 786 apply safe chaieb@26124 787 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe) chaieb@26124 788 apply (rule_tac x = "pmult qa qaa" in exI) chaieb@26124 789 apply (simp add: poly_mult mult_ac del: pmult_Cons) chaieb@26124 790 apply (drule_tac a = a in order_decomp)+ chaieb@26124 791 apply safe chaieb@26124 792 apply (subgoal_tac "?divides [uminus a,one ] (pmult qa qaa) ") chaieb@26124 793 apply (simp add: poly_primes del: pmult_Cons) chaieb@26124 794 apply (auto simp add: divides_def simp del: pmult_Cons) chaieb@26124 795 apply (rule_tac x = qb in exI) chaieb@26124 796 apply (subgoal_tac "?poly (pmult (pexp [uminus a, one] (?order a p)) (pmult qa qaa)) = ?poly (pmult (pexp [uminus a, one] (?order a p)) (pmult [uminus a, one] qb))") chaieb@26124 797 apply (drule poly_mult_left_cancel [THEN iffD1], force) chaieb@26124 798 apply (subgoal_tac "?poly (pmult (pexp [uminus a, one ] (order a q)) (pmult (pexp [uminus a, one] (order a p)) (pmult qa qaa))) = ?poly (pmult (pexp [uminus a, one] (order a q)) (pmult (pexp [uminus a, one] (order a p)) (pmult [uminus a, one] qb))) ") chaieb@26124 799 apply (drule poly_mult_left_cancel [THEN iffD1], force) chaieb@26124 800 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons) chaieb@26124 801 done chaieb@26124 802 qed chaieb@26124 803 chaieb@26124 804 lemma (in recpower_idom_char_0) order_root2: "poly p \ poly [] ==> (poly p a = 0) = (order a p \ 0)" chaieb@26124 805 by (rule order_root [THEN ssubst], auto) chaieb@26124 806 chaieb@26124 807 lemma (in semiring_1) pmult_one[simp]: "[1] *** p = p" by auto chaieb@26124 808 chaieb@26124 809 lemma (in semiring_0) poly_Nil_zero: "poly [] = poly [0]" chaieb@26124 810 by (simp add: fun_eq) chaieb@26124 811 chaieb@26124 812 lemma (in recpower_idom_char_0) rsquarefree_decomp: chaieb@26124 813 "[| rsquarefree p; poly p a = 0 |] chaieb@26124 814 ==> \q. (poly p = poly ([-a, 1] *** q)) & poly q a \ 0" chaieb@26124 815 apply (simp add: rsquarefree_def, safe) chaieb@26124 816 apply (frule_tac a = a in order_decomp) chaieb@26124 817 apply (drule_tac x = a in spec) chaieb@26124 818 apply (drule_tac a = a in order_root2 [symmetric]) chaieb@26124 819 apply (auto simp del: pmult_Cons) chaieb@26124 820 apply (rule_tac x = q in exI, safe) chaieb@26124 821 apply (simp add: poly_mult fun_eq) chaieb@26124 822 apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1]) chaieb@26124 823 apply (simp add: divides_def del: pmult_Cons, safe) chaieb@26124 824 apply (drule_tac x = "[]" in spec) chaieb@26124 825 apply (auto simp add: fun_eq) chaieb@26124 826 done chaieb@26124 827 chaieb@26124 828 chaieb@26124 829 text{*Normalization of a polynomial.*} chaieb@26124 830 chaieb@26124 831 lemma (in semiring_0) poly_normalize[simp]: "poly (pnormalize p) = poly p" chaieb@26124 832 apply (induct "p") chaieb@26124 833 apply (auto simp add: fun_eq) chaieb@26124 834 done chaieb@26124 835 chaieb@26124 836 text{*The degree of a polynomial.*} chaieb@26124 837 chaieb@26124 838 lemma (in semiring_0) lemma_degree_zero: chaieb@26124 839 "list_all (%c. c = 0) p \ pnormalize p = []" chaieb@26124 840 by (induct "p", auto) chaieb@26124 841 chaieb@26124 842 lemma (in idom_char_0) degree_zero: chaieb@26124 843 assumes pN: "poly p = poly []" shows"degree p = 0" chaieb@26124 844 proof- chaieb@26124 845 let ?pn = pnormalize chaieb@26124 846 from pN chaieb@26124 847 show ?thesis chaieb@26124 848 apply (simp add: degree_def) chaieb@26124 849 apply (case_tac "?pn p = []") chaieb@26124 850 apply (auto simp add: poly_zero lemma_degree_zero ) chaieb@26124 851 done chaieb@26124 852 qed chaieb@26124 853 chaieb@26124 854 lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \ x \ 0" by simp chaieb@26124 855 lemma (in semiring_0) pnormalize_pair: "y \ 0 \ (pnormalize [x, y] = [x, y])" by simp chaieb@26124 856 lemma (in semiring_0) pnormal_cons: "pnormal p \ pnormal (c#p)" chaieb@26124 857 unfolding pnormal_def by simp chaieb@26124 858 lemma (in semiring_0) pnormal_tail: "p\[] \ pnormal (c#p) \ pnormal p" chaieb@26124 859 unfolding pnormal_def chaieb@26124 860 apply (cases "pnormalize p = []", auto) chaieb@26124 861 by (cases "c = 0", auto) chaieb@26124 862 chaieb@26124 863 chaieb@26124 864 lemma (in semiring_0) pnormal_last_nonzero: "pnormal p ==> last p \ 0" chaieb@26124 865 proof(induct p) chaieb@26124 866 case Nil thus ?case by (simp add: pnormal_def) chaieb@26124 867 next chaieb@26124 868 case (Cons a as) thus ?case chaieb@26124 869 apply (simp add: pnormal_def) chaieb@26124 870 apply (cases "pnormalize as = []", simp_all) chaieb@26124 871 apply (cases "as = []", simp_all) chaieb@26124 872 apply (cases "a=0", simp_all) chaieb@26124 873 apply (cases "a=0", simp_all) chaieb@26124 874 done chaieb@26124 875 qed chaieb@26124 876 chaieb@26124 877 lemma (in semiring_0) pnormal_length: "pnormal p \ 0 < length p" chaieb@26124 878 unfolding pnormal_def length_greater_0_conv by blast chaieb@26124 879 chaieb@26124 880 lemma (in semiring_0) pnormal_last_length: "\0 < length p ; last p \ 0\ \ pnormal p" chaieb@26124 881 apply (induct p, auto) chaieb@26124 882 apply (case_tac "p = []", auto) chaieb@26124 883 apply (simp add: pnormal_def) chaieb@26124 884 by (rule pnormal_cons, auto) chaieb@26124 885 chaieb@26124 886 lemma (in semiring_0) pnormal_id: "pnormal p \ (0 < length p \ last p \ 0)" chaieb@26124 887 using pnormal_last_length pnormal_length pnormal_last_nonzero by blast chaieb@26124 888 chaieb@26124 889 lemma (in idom_char_0) poly_Cons_eq: "poly (c#cs) = poly (d#ds) \ c=d \ poly cs = poly ds" (is "?lhs \ ?rhs") chaieb@26124 890 proof chaieb@26124 891 assume eq: ?lhs chaieb@26124 892 hence "\x. poly ((c#cs) +++ -- (d#ds)) x = 0" chaieb@26124 893 by (simp only: poly_minus poly_add ring_simps) simp chaieb@26124 894 hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by - (rule ext, simp) chaieb@26124 895 hence "c = d \ list_all (\x. x=0) ((cs +++ -- ds))" chaieb@26124 896 unfolding poly_zero by (simp add: poly_minus_def ring_simps minus_mult_left[symmetric]) chaieb@26124 897 hence "c = d \ (\x. poly (cs +++ -- ds) x = 0)" chaieb@26124 898 unfolding poly_zero[symmetric] by simp chaieb@26124 899 thus ?rhs apply (simp add: poly_minus poly_add ring_simps) apply (rule ext, simp) done chaieb@26124 900 next chaieb@26124 901 assume ?rhs then show ?lhs by - (rule ext,simp) chaieb@26124 902 qed chaieb@26124 903 chaieb@26124 904 lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \ pnormalize p = pnormalize q" chaieb@26124 905 proof(induct q arbitrary: p) chaieb@26124 906 case Nil thus ?case by (simp only: poly_zero lemma_degree_zero) simp chaieb@26124 907 next chaieb@26124 908 case (Cons c cs p) chaieb@26124 909 thus ?case chaieb@26124 910 proof(induct p) chaieb@26124 911 case Nil chaieb@26124 912 hence "poly [] = poly (c#cs)" by blast chaieb@26124 913 then have "poly (c#cs) = poly [] " by simp chaieb@26124 914 thus ?case by (simp only: poly_zero lemma_degree_zero) simp chaieb@26124 915 next chaieb@26124 916 case (Cons d ds) chaieb@26124 917 hence eq: "poly (d # ds) = poly (c # cs)" by blast chaieb@26124 918 hence eq': "\x. poly (d # ds) x = poly (c # cs) x" by simp chaieb@26124 919 hence "poly (d # ds) 0 = poly (c # cs) 0" by blast chaieb@26124 920 hence dc: "d = c" by auto chaieb@26124 921 with eq have "poly ds = poly cs" chaieb@26124 922 unfolding poly_Cons_eq by simp chaieb@26124 923 with Cons.prems have "pnormalize ds = pnormalize cs" by blast chaieb@26124 924 with dc show ?case by simp chaieb@26124 925 qed chaieb@26124 926 qed chaieb@26124 927 chaieb@26124 928 lemma (in idom_char_0) degree_unique: assumes pq: "poly p = poly q" chaieb@26124 929 shows "degree p = degree q" chaieb@26124 930 using pnormalize_unique[OF pq] unfolding degree_def by simp chaieb@26124 931 chaieb@26124 932 lemma (in semiring_0) pnormalize_length: "length (pnormalize p) \ length p" by (induct p, auto) chaieb@26124 933 chaieb@26124 934 lemma (in semiring_0) last_linear_mul_lemma: chaieb@26124 935 "last ((a %* p) +++ (x#(b %* p))) = (if p=[] then x else b*last p)" chaieb@26124 936 chaieb@26124 937 apply (induct p arbitrary: a x b, auto) chaieb@26124 938 apply (subgoal_tac "padd (cmult aa p) (times b a # cmult b p) \ []", simp) chaieb@26124 939 apply (induct_tac p, auto) chaieb@26124 940 done chaieb@26124 941 chaieb@26124 942 lemma (in semiring_1) last_linear_mul: assumes p:"p\[]" shows "last ([a,1] *** p) = last p" chaieb@26124 943 proof- chaieb@26124 944 from p obtain c cs where cs: "p = c#cs" by (cases p, auto) chaieb@26124 945 from cs have eq:"[a,1] *** p = (a %* (c#cs)) +++ (0#(1 %* (c#cs)))" chaieb@26124 946 by (simp add: poly_cmult_distr) chaieb@26124 947 show ?thesis using cs chaieb@26124 948 unfolding eq last_linear_mul_lemma by simp chaieb@26124 949 qed chaieb@26124 950 chaieb@26124 951 lemma (in semiring_0) pnormalize_eq: "last p \ 0 \ pnormalize p = p" chaieb@26124 952 apply (induct p, auto) chaieb@26124 953 apply (case_tac p, auto)+ chaieb@26124 954 done chaieb@26124 955 chaieb@26124 956 lemma (in semiring_0) last_pnormalize: "pnormalize p \ [] \ last (pnormalize p) \ 0" chaieb@26124 957 by (induct p, auto) chaieb@26124 958 chaieb@26124 959 lemma (in semiring_0) pnormal_degree: "last p \ 0 \ degree p = length p - 1" chaieb@26124 960 using pnormalize_eq[of p] unfolding degree_def by simp chaieb@26124 961 chaieb@26124 962 lemma (in semiring_0) poly_Nil: "poly [] = (\x. 0)" by (rule ext, simp) chaieb@26124 963 chaieb@26124 964 lemma (in idom_char_0) linear_mul_degree: assumes p: "poly p \ poly []" chaieb@26124 965 shows "degree ([a,1] *** p) = degree p + 1" chaieb@26124 966 proof- chaieb@26124 967 from p have pnz: "pnormalize p \ []" chaieb@26124 968 unfolding poly_zero lemma_degree_zero . chaieb@26124 969 chaieb@26124 970 from last_linear_mul[OF pnz, of a] last_pnormalize[OF pnz] chaieb@26124 971 have l0: "last ([a, 1] *** pnormalize p) \ 0" by simp chaieb@26124 972 from last_pnormalize[OF pnz] last_linear_mul[OF pnz, of a] chaieb@26124 973 pnormal_degree[OF l0] pnormal_degree[OF last_pnormalize[OF pnz]] pnz chaieb@26124 974 chaieb@26124 975 chaieb@26124 976 have th: "degree ([a,1] *** pnormalize p) = degree (pnormalize p) + 1" chaieb@26124 977 by (auto simp add: poly_length_mult) chaieb@26124 978 chaieb@26124 979 have eqs: "poly ([a,1] *** pnormalize p) = poly ([a,1] *** p)" chaieb@26124 980 by (rule ext) (simp add: poly_mult poly_add poly_cmult) chaieb@26124 981 from degree_unique[OF eqs] th chaieb@26124 982 show ?thesis by (simp add: degree_unique[OF poly_normalize]) chaieb@26124 983 qed chaieb@26124 984 chaieb@26124 985 lemma (in idom_char_0) poly_entire_lemma: chaieb@26124 986 assumes p0: "poly p \ poly []" and q0: "poly q \ poly []" chaieb@26124 987 shows "poly (p***q) \ poly []" chaieb@26124 988 proof- chaieb@26124 989 let ?S = "\p. {x. poly p x = 0}" chaieb@26124 990 have "?S (p *** q) = ?S p \ ?S q" by (auto simp add: poly_mult) chaieb@26124 991 with p0 q0 show ?thesis unfolding poly_roots_finite by auto chaieb@26124 992 qed chaieb@26124 993 chaieb@26124 994 lemma (in idom_char_0) poly_entire: chaieb@26124 995 "poly (p *** q) = poly [] \ poly p = poly [] \ poly q = poly []" chaieb@26124 996 using poly_entire_lemma[of p q] chaieb@26124 997 by auto (rule ext, simp add: poly_mult)+ chaieb@26124 998 chaieb@26124 999 lemma (in idom_char_0) linear_pow_mul_degree: chaieb@26124 1000 "degree([a,1] %^n *** p) = (if poly p = poly [] then 0 else degree p + n)" chaieb@26124 1001 proof(induct n arbitrary: a p) chaieb@26124 1002 case (0 a p) chaieb@26124 1003 {assume p: "poly p = poly []" chaieb@26124 1004 hence ?case using degree_unique[OF p] by (simp add: degree_def)} chaieb@26124 1005 moreover chaieb@26124 1006 {assume p: "poly p \ poly []" hence ?case by (auto simp add: poly_Nil) } chaieb@26124 1007 ultimately show ?case by blast chaieb@26124 1008 next chaieb@26124 1009 case (Suc n a p) chaieb@26124 1010 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1] %^ n *** ([a,1] *** p))" chaieb@26124 1011 apply (rule ext, simp add: poly_mult poly_add poly_cmult) chaieb@26124 1012 by (simp add: mult_ac add_ac right_distrib) chaieb@26124 1013 note deq = degree_unique[OF eq] chaieb@26124 1014 {assume p: "poly p = poly []" chaieb@26124 1015 with eq have eq': "poly ([a,1] %^(Suc n) *** p) = poly []" chaieb@26124 1016 by - (rule ext,simp add: poly_mult poly_cmult poly_add) chaieb@26124 1017 from degree_unique[OF eq'] p have ?case by (simp add: degree_def)} chaieb@26124 1018 moreover chaieb@26124 1019 {assume p: "poly p \ poly []" chaieb@26124 1020 from p have ap: "poly ([a,1] *** p) \ poly []" chaieb@26124 1021 using poly_mult_not_eq_poly_Nil unfolding poly_entire by auto chaieb@26124 1022 have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1]%^n *** ([a,1] *** p))" chaieb@26124 1023 by (rule ext, simp add: poly_mult poly_add poly_exp poly_cmult mult_ac add_ac right_distrib) chaieb@26124 1024 from ap have ap': "(poly ([a,1] *** p) = poly []) = False" by blast chaieb@26124 1025 have th0: "degree ([a,1]%^n *** ([a,1] *** p)) = degree ([a,1] *** p) + n" chaieb@26124 1026 apply (simp only: Suc.hyps[of a "pmult [a,one] p"] ap') chaieb@26124 1027 by simp chaieb@26124 1028 chaieb@26124 1029 from degree_unique[OF eq] ap p th0 linear_mul_degree[OF p, of a] chaieb@26124 1030 have ?case by (auto simp del: poly.simps)} chaieb@26124 1031 ultimately show ?case by blast chaieb@26124 1032 qed chaieb@26124 1033 chaieb@26124 1034 lemma (in recpower_idom_char_0) order_degree: chaieb@26124 1035 assumes p0: "poly p \ poly []" chaieb@26124 1036 shows "order a p \ degree p" chaieb@26124 1037 proof- chaieb@26124 1038 from order2[OF p0, unfolded divides_def] chaieb@26124 1039 obtain q where q: "poly p = poly ([- a, 1]%^ (order a p) *** q)" by blast chaieb@26124 1040 {assume "poly q = poly []" chaieb@26124 1041 with q p0 have False by (simp add: poly_mult poly_entire)} chaieb@26124 1042 with degree_unique[OF q, unfolded linear_pow_mul_degree] chaieb@26124 1043 show ?thesis by auto chaieb@26124 1044 qed chaieb@26124 1045 chaieb@26124 1046 text{*Tidier versions of finiteness of roots.*} chaieb@26124 1047 chaieb@26124 1048 lemma (in idom_char_0) poly_roots_finite_set: "poly p \ poly [] ==> finite {x. poly p x = 0}" chaieb@26124 1049 unfolding poly_roots_finite . chaieb@26124 1050 chaieb@26124 1051 text{*bound for polynomial.*} chaieb@26124 1052 chaieb@26124 1053 lemma poly_mono: "abs(x) \ k ==> abs(poly p (x::'a::{ordered_idom})) \ poly (map abs p) k" chaieb@26124 1054 apply (induct "p", auto) chaieb@26124 1055 apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans) chaieb@26124 1056 apply (rule abs_triangle_ineq) chaieb@26124 1057 apply (auto intro!: mult_mono simp add: abs_mult) chaieb@26124 1058 done chaieb@26124 1059 chaieb@26124 1060 lemma (in semiring_0) poly_Sing: "poly [c] x = c" by simp chaieb@26124 1061 chaieb@26124 1062 end