src/HOL/Hyperreal/Poly.thy
 author wenzelm Thu Apr 26 14:24:08 2007 +0200 (2007-04-26) changeset 22808 a7daa74e2980 parent 21404 eb85850d3eb7 child 22983 3314057c3b57 permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
```     1 (*  Title:       Poly.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:      Jacques D. Fleuriot
```
```     4     Copyright:   2000 University of Edinburgh
```
```     5
```
```     6     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
```
```     7 *)
```
```     8
```
```     9 header{*Univariate Real Polynomials*}
```
```    10
```
```    11 theory Poly
```
```    12 imports Ln
```
```    13 begin
```
```    14
```
```    15 text{*Application of polynomial as a real function.*}
```
```    16
```
```    17 consts poly :: "real list => real => real"
```
```    18 primrec
```
```    19   poly_Nil:  "poly [] x = 0"
```
```    20   poly_Cons: "poly (h#t) x = h + x * poly t x"
```
```    21
```
```    22
```
```    23 subsection{*Arithmetic Operations on Polynomials*}
```
```    24
```
```    25 text{*addition*}
```
```    26 consts padd :: "[real list, real list] => real list"  (infixl "+++" 65)
```
```    27 primrec
```
```    28   padd_Nil:  "[] +++ l2 = l2"
```
```    29   padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
```
```    30                             else (h + hd l2)#(t +++ tl l2))"
```
```    31
```
```    32 text{*Multiplication by a constant*}
```
```    33 consts cmult :: "[real, real list] => real list"  (infixl "%*" 70)
```
```    34 primrec
```
```    35    cmult_Nil:  "c %* [] = []"
```
```    36    cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
```
```    37
```
```    38 text{*Multiplication by a polynomial*}
```
```    39 consts pmult :: "[real list, real list] => real list"  (infixl "***" 70)
```
```    40 primrec
```
```    41    pmult_Nil:  "[] *** l2 = []"
```
```    42    pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
```
```    43                               else (h %* l2) +++ ((0) # (t *** l2)))"
```
```    44
```
```    45 text{*Repeated multiplication by a polynomial*}
```
```    46 consts mulexp :: "[nat, real list, real list] => real list"
```
```    47 primrec
```
```    48    mulexp_zero:  "mulexp 0 p q = q"
```
```    49    mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
```
```    50
```
```    51
```
```    52 text{*Exponential*}
```
```    53 consts pexp :: "[real list, nat] => real list"  (infixl "%^" 80)
```
```    54 primrec
```
```    55    pexp_0:   "p %^ 0 = [1]"
```
```    56    pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
```
```    57
```
```    58 text{*Quotient related value of dividing a polynomial by x + a*}
```
```    59 (* Useful for divisor properties in inductive proofs *)
```
```    60 consts "pquot" :: "[real list, real] => real list"
```
```    61 primrec
```
```    62    pquot_Nil:  "pquot [] a= []"
```
```    63    pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
```
```    64                    else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
```
```    65
```
```    66 text{*Differentiation of polynomials (needs an auxiliary function).*}
```
```    67 consts pderiv_aux :: "nat => real list => real list"
```
```    68 primrec
```
```    69    pderiv_aux_Nil:  "pderiv_aux n [] = []"
```
```    70    pderiv_aux_Cons: "pderiv_aux n (h#t) =
```
```    71                      (real n * h)#(pderiv_aux (Suc n) t)"
```
```    72
```
```    73 text{*normalization of polynomials (remove extra 0 coeff)*}
```
```    74 consts pnormalize :: "real list => real list"
```
```    75 primrec
```
```    76    pnormalize_Nil:  "pnormalize [] = []"
```
```    77    pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
```
```    78                                      then (if (h = 0) then [] else [h])
```
```    79                                      else (h#(pnormalize p)))"
```
```    80
```
```    81
```
```    82 text{*Other definitions*}
```
```    83
```
```    84 definition
```
```    85   poly_minus :: "real list => real list"      ("-- _" [80] 80) where
```
```    86   "-- p = (- 1) %* p"
```
```    87
```
```    88 definition
```
```    89   pderiv :: "real list => real list" where
```
```    90   "pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))"
```
```    91
```
```    92 definition
```
```    93   divides :: "[real list,real list] => bool"  (infixl "divides" 70) where
```
```    94   "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
```
```    95
```
```    96 definition
```
```    97   order :: "real => real list => nat" where
```
```    98     --{*order of a polynomial*}
```
```    99   "order a p = (SOME n. ([-a, 1] %^ n) divides p &
```
```   100                       ~ (([-a, 1] %^ (Suc n)) divides p))"
```
```   101
```
```   102 definition
```
```   103   degree :: "real list => nat" where
```
```   104      --{*degree of a polynomial*}
```
```   105   "degree p = length (pnormalize p)"
```
```   106
```
```   107 definition
```
```   108   rsquarefree :: "real list => bool" where
```
```   109      --{*squarefree polynomials --- NB with respect to real roots only.*}
```
```   110   "rsquarefree p = (poly p \<noteq> poly [] &
```
```   111                      (\<forall>a. (order a p = 0) | (order a p = 1)))"
```
```   112
```
```   113
```
```   114
```
```   115 lemma padd_Nil2: "p +++ [] = p"
```
```   116 by (induct p) auto
```
```   117 declare padd_Nil2 [simp]
```
```   118
```
```   119 lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
```
```   120 by auto
```
```   121
```
```   122 lemma pminus_Nil: "-- [] = []"
```
```   123 by (simp add: poly_minus_def)
```
```   124 declare pminus_Nil [simp]
```
```   125
```
```   126 lemma pmult_singleton: "[h1] *** p1 = h1 %* p1"
```
```   127 by simp
```
```   128
```
```   129 lemma poly_ident_mult: "1 %* t = t"
```
```   130 by (induct "t", auto)
```
```   131 declare poly_ident_mult [simp]
```
```   132
```
```   133 lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)"
```
```   134 by simp
```
```   135 declare poly_simple_add_Cons [simp]
```
```   136
```
```   137 text{*Handy general properties*}
```
```   138
```
```   139 lemma padd_commut: "b +++ a = a +++ b"
```
```   140 apply (subgoal_tac "\<forall>a. b +++ a = a +++ b")
```
```   141 apply (induct_tac [2] "b", auto)
```
```   142 apply (rule padd_Cons [THEN ssubst])
```
```   143 apply (case_tac "aa", auto)
```
```   144 done
```
```   145
```
```   146 lemma padd_assoc [rule_format]: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
```
```   147 apply (induct "a", simp, clarify)
```
```   148 apply (case_tac b, simp_all)
```
```   149 done
```
```   150
```
```   151 lemma poly_cmult_distr [rule_format]:
```
```   152      "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
```
```   153 apply (induct "p", simp, clarify)
```
```   154 apply (case_tac "q")
```
```   155 apply (simp_all add: right_distrib)
```
```   156 done
```
```   157
```
```   158 lemma pmult_by_x: "[0, 1] *** t = ((0)#t)"
```
```   159 apply (induct "t", simp)
```
```   160 apply (auto simp add: poly_ident_mult padd_commut)
```
```   161 done
```
```   162 declare pmult_by_x [simp]
```
```   163
```
```   164
```
```   165 text{*properties of evaluation of polynomials.*}
```
```   166
```
```   167 lemma poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x"
```
```   168 apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
```
```   169 apply (induct_tac [2] "p1", auto)
```
```   170 apply (case_tac "p2")
```
```   171 apply (auto simp add: right_distrib)
```
```   172 done
```
```   173
```
```   174 lemma poly_cmult: "poly (c %* p) x = c * poly p x"
```
```   175 apply (induct "p")
```
```   176 apply (case_tac [2] "x=0")
```
```   177 apply (auto simp add: right_distrib mult_ac)
```
```   178 done
```
```   179
```
```   180 lemma poly_minus: "poly (-- p) x = - (poly p x)"
```
```   181 apply (simp add: poly_minus_def)
```
```   182 apply (auto simp add: poly_cmult)
```
```   183 done
```
```   184
```
```   185 lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
```
```   186 apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x")
```
```   187 apply (simp (no_asm_simp))
```
```   188 apply (induct "p1")
```
```   189 apply (auto simp add: poly_cmult)
```
```   190 apply (case_tac p1)
```
```   191 apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
```
```   192 done
```
```   193
```
```   194 lemma poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
```
```   195 apply (induct "n")
```
```   196 apply (auto simp add: poly_cmult poly_mult)
```
```   197 done
```
```   198
```
```   199 text{*More Polynomial Evaluation Lemmas*}
```
```   200
```
```   201 lemma poly_add_rzero: "poly (a +++ []) x = poly a x"
```
```   202 by simp
```
```   203 declare poly_add_rzero [simp]
```
```   204
```
```   205 lemma poly_mult_assoc: "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x"
```
```   206 by (simp add: poly_mult real_mult_assoc)
```
```   207
```
```   208 lemma poly_mult_Nil2: "poly (p *** []) x = 0"
```
```   209 by (induct "p", auto)
```
```   210 declare poly_mult_Nil2 [simp]
```
```   211
```
```   212 lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x"
```
```   213 apply (induct "n")
```
```   214 apply (auto simp add: poly_mult real_mult_assoc)
```
```   215 done
```
```   216
```
```   217 text{*The derivative*}
```
```   218
```
```   219 lemma pderiv_Nil: "pderiv [] = []"
```
```   220
```
```   221 apply (simp add: pderiv_def)
```
```   222 done
```
```   223 declare pderiv_Nil [simp]
```
```   224
```
```   225 lemma pderiv_singleton: "pderiv [c] = []"
```
```   226 by (simp add: pderiv_def)
```
```   227 declare pderiv_singleton [simp]
```
```   228
```
```   229 lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t"
```
```   230 by (simp add: pderiv_def)
```
```   231
```
```   232 lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
```
```   233 by (simp add: DERIV_cmult mult_commute [of _ c])
```
```   234
```
```   235 lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
```
```   236 by (rule lemma_DERIV_subst, rule DERIV_pow, simp)
```
```   237 declare DERIV_pow2 [simp] DERIV_pow [simp]
```
```   238
```
```   239 lemma lemma_DERIV_poly1: "\<forall>n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
```
```   240         x ^ n * poly (pderiv_aux (Suc n) p) x "
```
```   241 apply (induct "p")
```
```   242 apply (auto intro!: DERIV_add DERIV_cmult2
```
```   243             simp add: pderiv_def right_distrib real_mult_assoc [symmetric]
```
```   244             simp del: realpow_Suc)
```
```   245 apply (subst mult_commute)
```
```   246 apply (simp del: realpow_Suc)
```
```   247 apply (simp add: mult_commute realpow_Suc [symmetric] del: realpow_Suc)
```
```   248 done
```
```   249
```
```   250 lemma lemma_DERIV_poly: "DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
```
```   251         x ^ n * poly (pderiv_aux (Suc n) p) x "
```
```   252 by (simp add: lemma_DERIV_poly1 del: realpow_Suc)
```
```   253
```
```   254 lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: real) x :> D"
```
```   255 by (rule lemma_DERIV_subst, rule DERIV_add, auto)
```
```   256
```
```   257 lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
```
```   258 apply (induct "p")
```
```   259 apply (auto simp add: pderiv_Cons)
```
```   260 apply (rule DERIV_add_const)
```
```   261 apply (rule lemma_DERIV_subst)
```
```   262 apply (rule lemma_DERIV_poly [where n=0, simplified], simp)
```
```   263 done
```
```   264 declare poly_DERIV [simp]
```
```   265
```
```   266
```
```   267 text{* Consequences of the derivative theorem above*}
```
```   268
```
```   269 lemma poly_differentiable: "(%x. poly p x) differentiable x"
```
```   270
```
```   271 apply (simp add: differentiable_def)
```
```   272 apply (blast intro: poly_DERIV)
```
```   273 done
```
```   274 declare poly_differentiable [simp]
```
```   275
```
```   276 lemma poly_isCont: "isCont (%x. poly p x) x"
```
```   277 by (rule poly_DERIV [THEN DERIV_isCont])
```
```   278 declare poly_isCont [simp]
```
```   279
```
```   280 lemma poly_IVT_pos: "[| a < b; poly p a < 0; 0 < poly p b |]
```
```   281       ==> \<exists>x. a < x & x < b & (poly p x = 0)"
```
```   282 apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl)
```
```   283 apply (auto simp add: order_le_less)
```
```   284 done
```
```   285
```
```   286 lemma poly_IVT_neg: "[| a < b; 0 < poly p a; poly p b < 0 |]
```
```   287       ==> \<exists>x. a < x & x < b & (poly p x = 0)"
```
```   288 apply (insert poly_IVT_pos [where p = "-- p" ])
```
```   289 apply (simp add: poly_minus neg_less_0_iff_less)
```
```   290 done
```
```   291
```
```   292 lemma poly_MVT: "a < b ==>
```
```   293      \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
```
```   294 apply (drule_tac f = "poly p" in MVT, auto)
```
```   295 apply (rule_tac x = z in exI)
```
```   296 apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique])
```
```   297 done
```
```   298
```
```   299
```
```   300 text{*Lemmas for Derivatives*}
```
```   301
```
```   302 lemma lemma_poly_pderiv_aux_add: "\<forall>p2 n. poly (pderiv_aux n (p1 +++ p2)) x =
```
```   303                 poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
```
```   304 apply (induct "p1", simp, clarify)
```
```   305 apply (case_tac "p2")
```
```   306 apply (auto simp add: right_distrib)
```
```   307 done
```
```   308
```
```   309 lemma poly_pderiv_aux_add: "poly (pderiv_aux n (p1 +++ p2)) x =
```
```   310       poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
```
```   311 apply (simp add: lemma_poly_pderiv_aux_add)
```
```   312 done
```
```   313
```
```   314 lemma lemma_poly_pderiv_aux_cmult: "\<forall>n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
```
```   315 apply (induct "p")
```
```   316 apply (auto simp add: poly_cmult mult_ac)
```
```   317 done
```
```   318
```
```   319 lemma poly_pderiv_aux_cmult: "poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
```
```   320 by (simp add: lemma_poly_pderiv_aux_cmult)
```
```   321
```
```   322 lemma poly_pderiv_aux_minus:
```
```   323    "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x"
```
```   324 apply (simp add: poly_minus_def poly_pderiv_aux_cmult)
```
```   325 done
```
```   326
```
```   327 lemma lemma_poly_pderiv_aux_mult1: "\<forall>n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
```
```   328 apply (induct "p")
```
```   329 apply (auto simp add: real_of_nat_Suc left_distrib)
```
```   330 done
```
```   331
```
```   332 lemma lemma_poly_pderiv_aux_mult: "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
```
```   333 by (simp add: lemma_poly_pderiv_aux_mult1)
```
```   334
```
```   335 lemma lemma_poly_pderiv_add: "\<forall>q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
```
```   336 apply (induct "p", simp, clarify)
```
```   337 apply (case_tac "q")
```
```   338 apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def)
```
```   339 done
```
```   340
```
```   341 lemma poly_pderiv_add: "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
```
```   342 by (simp add: lemma_poly_pderiv_add)
```
```   343
```
```   344 lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x"
```
```   345 apply (induct "p")
```
```   346 apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def)
```
```   347 done
```
```   348
```
```   349 lemma poly_pderiv_minus: "poly (pderiv (--p)) x = poly (--(pderiv p)) x"
```
```   350 by (simp add: poly_minus_def poly_pderiv_cmult)
```
```   351
```
```   352 lemma lemma_poly_mult_pderiv:
```
```   353    "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x"
```
```   354 apply (simp add: pderiv_def)
```
```   355 apply (induct "t")
```
```   356 apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult)
```
```   357 done
```
```   358
```
```   359 lemma poly_pderiv_mult: "\<forall>q. poly (pderiv (p *** q)) x =
```
```   360       poly (p *** (pderiv q) +++ q *** (pderiv p)) x"
```
```   361 apply (induct "p")
```
```   362 apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult)
```
```   363 apply (rule lemma_poly_mult_pderiv [THEN ssubst])
```
```   364 apply (rule lemma_poly_mult_pderiv [THEN ssubst])
```
```   365 apply (rule poly_add [THEN ssubst])
```
```   366 apply (rule poly_add [THEN ssubst])
```
```   367 apply (simp (no_asm_simp) add: poly_mult right_distrib add_ac mult_ac)
```
```   368 done
```
```   369
```
```   370 lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x =
```
```   371          poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x"
```
```   372 apply (induct "n")
```
```   373 apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult
```
```   374                       real_of_nat_zero poly_mult real_of_nat_Suc
```
```   375                       right_distrib left_distrib mult_ac)
```
```   376 done
```
```   377
```
```   378 lemma poly_pderiv_exp_prime: "poly (pderiv ([-a, 1] %^ (Suc n))) x =
```
```   379       poly (real (Suc n) %* ([-a, 1] %^ n)) x"
```
```   380 apply (simp add: poly_pderiv_exp poly_mult del: pexp_Suc)
```
```   381 apply (simp add: poly_cmult pderiv_def)
```
```   382 done
```
```   383
```
```   384 subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides
```
```   385  @{term "p(x)"} *}
```
```   386
```
```   387 lemma lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
```
```   388 apply (induct "t", safe)
```
```   389 apply (rule_tac x = "[]" in exI)
```
```   390 apply (rule_tac x = h in exI, simp)
```
```   391 apply (drule_tac x = aa in spec, safe)
```
```   392 apply (rule_tac x = "r#q" in exI)
```
```   393 apply (rule_tac x = "a*r + h" in exI)
```
```   394 apply (case_tac "q", auto)
```
```   395 done
```
```   396
```
```   397 lemma poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q"
```
```   398 by (cut_tac t = t and a = a in lemma_poly_linear_rem, auto)
```
```   399
```
```   400
```
```   401 lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))"
```
```   402 apply (auto simp add: poly_add poly_cmult right_distrib)
```
```   403 apply (case_tac "p", simp)
```
```   404 apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
```
```   405 apply (case_tac "q", auto)
```
```   406 apply (drule_tac x = "[]" in spec, simp)
```
```   407 apply (auto simp add: poly_add poly_cmult real_add_assoc)
```
```   408 apply (drule_tac x = "aa#lista" in spec, auto)
```
```   409 done
```
```   410
```
```   411 lemma lemma_poly_length_mult: "\<forall>h k a. length (k %* p +++  (h # (a %* p))) = Suc (length p)"
```
```   412 by (induct "p", auto)
```
```   413 declare lemma_poly_length_mult [simp]
```
```   414
```
```   415 lemma lemma_poly_length_mult2: "\<forall>h k. length (k %* p +++  (h # p)) = Suc (length p)"
```
```   416 by (induct "p", auto)
```
```   417 declare lemma_poly_length_mult2 [simp]
```
```   418
```
```   419 lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)"
```
```   420 by auto
```
```   421 declare poly_length_mult [simp]
```
```   422
```
```   423
```
```   424 subsection{*Polynomial length*}
```
```   425
```
```   426 lemma poly_cmult_length: "length (a %* p) = length p"
```
```   427 by (induct "p", auto)
```
```   428 declare poly_cmult_length [simp]
```
```   429
```
```   430 lemma poly_add_length [rule_format]:
```
```   431      "\<forall>p2. length (p1 +++ p2) =
```
```   432              (if (length p1 < length p2) then length p2 else length p1)"
```
```   433 apply (induct "p1", simp_all)
```
```   434 apply arith
```
```   435 done
```
```   436
```
```   437 lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
```
```   438 by (simp add: poly_cmult_length poly_add_length)
```
```   439 declare poly_root_mult_length [simp]
```
```   440
```
```   441 lemma poly_mult_not_eq_poly_Nil: "(poly (p *** q) x \<noteq> poly [] x) =
```
```   442       (poly p x \<noteq> poly [] x & poly q x \<noteq> poly [] x)"
```
```   443 apply (auto simp add: poly_mult)
```
```   444 done
```
```   445 declare poly_mult_not_eq_poly_Nil [simp]
```
```   446
```
```   447 lemma poly_mult_eq_zero_disj: "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)"
```
```   448 by (auto simp add: poly_mult)
```
```   449
```
```   450 text{*Normalisation Properties*}
```
```   451
```
```   452 lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)"
```
```   453 by (induct "p", auto)
```
```   454
```
```   455 text{*A nontrivial polynomial of degree n has no more than n roots*}
```
```   456
```
```   457 lemma poly_roots_index_lemma [rule_format]:
```
```   458    "\<forall>p x. poly p x \<noteq> poly [] x & length p = n
```
```   459     --> (\<exists>i. \<forall>x. (poly p x = (0::real)) --> (\<exists>m. (m \<le> n & x = i m)))"
```
```   460 apply (induct "n", safe)
```
```   461 apply (rule ccontr)
```
```   462 apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
```
```   463 apply (drule poly_linear_divides [THEN iffD1], safe)
```
```   464 apply (drule_tac x = q in spec)
```
```   465 apply (drule_tac x = x in spec)
```
```   466 apply (simp del: poly_Nil pmult_Cons)
```
```   467 apply (erule exE)
```
```   468 apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
```
```   469 apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
```
```   470 apply (drule_tac x = "Suc (length q)" in spec)
```
```   471 apply simp
```
```   472 apply (drule_tac x = xa in spec, safe)
```
```   473 apply (drule_tac x = m in spec, simp, blast)
```
```   474 done
```
```   475 lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
```
```   476
```
```   477 lemma poly_roots_index_length: "poly p x \<noteq> poly [] x ==>
```
```   478       \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)"
```
```   479 by (blast intro: poly_roots_index_lemma2)
```
```   480
```
```   481 lemma poly_roots_finite_lemma: "poly p x \<noteq> poly [] x ==>
```
```   482       \<exists>N i. \<forall>x. (poly p x = 0) --> (\<exists>n. (n::nat) < N & x = i n)"
```
```   483 apply (drule poly_roots_index_length, safe)
```
```   484 apply (rule_tac x = "Suc (length p)" in exI)
```
```   485 apply (rule_tac x = i in exI)
```
```   486 apply (simp add: less_Suc_eq_le)
```
```   487 done
```
```   488
```
```   489 (* annoying proof *)
```
```   490 lemma real_finite_lemma [rule_format (no_asm)]:
```
```   491      "\<forall>P. (\<forall>x. P x --> (\<exists>n. n < N & x = (j::nat=>real) n))
```
```   492       --> (\<exists>a. \<forall>x. P x --> x < a)"
```
```   493 apply (induct "N", simp, safe)
```
```   494 apply (drule_tac x = "%z. P z & (z \<noteq> j N)" in spec)
```
```   495 apply (auto simp add: less_Suc_eq)
```
```   496 apply (rename_tac N P a)
```
```   497 apply (rule_tac x = "abs a + abs (j N) + 1" in exI)
```
```   498 apply safe
```
```   499 apply (drule_tac x = x in spec, safe)
```
```   500 apply (drule_tac x = "j n" in spec, arith+)
```
```   501 done
```
```   502
```
```   503 lemma poly_roots_finite: "(poly p \<noteq> poly []) =
```
```   504       (\<exists>N j. \<forall>x. poly p x = 0 --> (\<exists>n. (n::nat) < N & x = j n))"
```
```   505 apply safe
```
```   506 apply (erule contrapos_np, rule ext)
```
```   507 apply (rule ccontr)
```
```   508 apply (clarify dest!: poly_roots_finite_lemma)
```
```   509 apply (clarify dest!: real_finite_lemma)
```
```   510 apply (drule_tac x = a in fun_cong, auto)
```
```   511 done
```
```   512
```
```   513 text{*Entirety and Cancellation for polynomials*}
```
```   514
```
```   515 lemma poly_entire_lemma: "[| poly p \<noteq> poly [] ; poly q \<noteq> poly [] |]
```
```   516       ==>  poly (p *** q) \<noteq> poly []"
```
```   517 apply (auto simp add: poly_roots_finite)
```
```   518 apply (rule_tac x = "N + Na" in exI)
```
```   519 apply (rule_tac x = "%n. if n < N then j n else ja (n - N)" in exI)
```
```   520 apply (auto simp add: poly_mult_eq_zero_disj, force)
```
```   521 done
```
```   522
```
```   523 lemma poly_entire: "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))"
```
```   524 apply (auto intro: ext dest: fun_cong simp add: poly_entire_lemma poly_mult)
```
```   525 apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst])
```
```   526 done
```
```   527
```
```   528 lemma poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
```
```   529 by (simp add: poly_entire)
```
```   530
```
```   531 lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)"
```
```   532 by (auto intro!: ext)
```
```   533
```
```   534 lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
```
```   535 by (auto simp add: poly_add poly_minus_def fun_eq poly_cmult)
```
```   536
```
```   537 lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
```
```   538 by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)
```
```   539
```
```   540 lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
```
```   541 apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
```
```   542 apply (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
```
```   543 done
```
```   544
```
```   545 lemma real_mult_zero_disj_iff: "(x * y = 0) = (x = (0::real) | y = 0)"
```
```   546 by simp
```
```   547
```
```   548 lemma poly_exp_eq_zero:
```
```   549      "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
```
```   550 apply (simp only: fun_eq add: all_simps [symmetric])
```
```   551 apply (rule arg_cong [where f = All])
```
```   552 apply (rule ext)
```
```   553 apply (induct_tac "n")
```
```   554 apply (auto simp add: poly_mult real_mult_zero_disj_iff)
```
```   555 done
```
```   556 declare poly_exp_eq_zero [simp]
```
```   557
```
```   558 lemma poly_prime_eq_zero: "poly [a,1] \<noteq> poly []"
```
```   559 apply (simp add: fun_eq)
```
```   560 apply (rule_tac x = "1 - a" in exI, simp)
```
```   561 done
```
```   562 declare poly_prime_eq_zero [simp]
```
```   563
```
```   564 lemma poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
```
```   565 by auto
```
```   566 declare poly_exp_prime_eq_zero [simp]
```
```   567
```
```   568 text{*A more constructive notion of polynomials being trivial*}
```
```   569
```
```   570 lemma poly_zero_lemma: "poly (h # t) = poly [] ==> h = 0 & poly t = poly []"
```
```   571 apply (simp add: fun_eq)
```
```   572 apply (case_tac "h = 0")
```
```   573 apply (drule_tac [2] x = 0 in spec, auto)
```
```   574 apply (case_tac "poly t = poly []", simp)
```
```   575 apply (auto simp add: poly_roots_finite real_mult_zero_disj_iff)
```
```   576 apply (drule real_finite_lemma, safe)
```
```   577 apply (drule_tac x = "abs a + 1" in spec)+
```
```   578 apply arith
```
```   579 done
```
```   580
```
```   581
```
```   582 lemma poly_zero: "(poly p = poly []) = list_all (%c. c = 0) p"
```
```   583 apply (induct "p", simp)
```
```   584 apply (rule iffI)
```
```   585 apply (drule poly_zero_lemma, auto)
```
```   586 done
```
```   587
```
```   588 declare real_mult_zero_disj_iff [simp]
```
```   589
```
```   590 lemma pderiv_aux_iszero [rule_format, simp]:
```
```   591     "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
```
```   592 by (induct "p", auto)
```
```   593
```
```   594 lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
```
```   595       ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
```
```   596       list_all (%c. c = 0) p)"
```
```   597 apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force)
```
```   598 apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst])
```
```   599 apply (simp (no_asm_simp) del: pderiv_aux_iszero)
```
```   600 done
```
```   601
```
```   602 lemma pderiv_iszero [rule_format]:
```
```   603      "poly (pderiv p) = poly [] --> (\<exists>h. poly p = poly [h])"
```
```   604 apply (simp add: poly_zero)
```
```   605 apply (induct "p", force)
```
```   606 apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
```
```   607 apply (auto simp add: poly_zero [symmetric])
```
```   608 done
```
```   609
```
```   610 lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])"
```
```   611 apply (simp add: poly_zero)
```
```   612 apply (induct "p", force)
```
```   613 apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
```
```   614 done
```
```   615
```
```   616 lemma pderiv_zero: "poly p = poly [] ==> (poly (pderiv p) = poly [])"
```
```   617 by (blast elim: pderiv_zero_obj [THEN impE])
```
```   618 declare pderiv_zero [simp]
```
```   619
```
```   620 lemma poly_pderiv_welldef: "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))"
```
```   621 apply (cut_tac p = "p +++ --q" in pderiv_zero_obj)
```
```   622 apply (simp add: fun_eq poly_add poly_minus poly_pderiv_add poly_pderiv_minus del: pderiv_zero)
```
```   623 done
```
```   624
```
```   625 text{*Basics of divisibility.*}
```
```   626
```
```   627 lemma poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
```
```   628 apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
```
```   629 apply (drule_tac x = "-a" in spec)
```
```   630 apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
```
```   631 apply (rule_tac x = "qa *** q" in exI)
```
```   632 apply (rule_tac [2] x = "p *** qa" in exI)
```
```   633 apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
```
```   634 done
```
```   635
```
```   636 lemma poly_divides_refl: "p divides p"
```
```   637 apply (simp add: divides_def)
```
```   638 apply (rule_tac x = "[1]" in exI)
```
```   639 apply (auto simp add: poly_mult fun_eq)
```
```   640 done
```
```   641 declare poly_divides_refl [simp]
```
```   642
```
```   643 lemma poly_divides_trans: "[| p divides q; q divides r |] ==> p divides r"
```
```   644 apply (simp add: divides_def, safe)
```
```   645 apply (rule_tac x = "qa *** qaa" in exI)
```
```   646 apply (auto simp add: poly_mult fun_eq real_mult_assoc)
```
```   647 done
```
```   648
```
```   649 lemma poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
```
```   650 apply (auto simp add: le_iff_add)
```
```   651 apply (induct_tac k)
```
```   652 apply (rule_tac [2] poly_divides_trans)
```
```   653 apply (auto simp add: divides_def)
```
```   654 apply (rule_tac x = p in exI)
```
```   655 apply (auto simp add: poly_mult fun_eq mult_ac)
```
```   656 done
```
```   657
```
```   658 lemma poly_exp_divides: "[| (p %^ n) divides q;  m\<le>n |] ==> (p %^ m) divides q"
```
```   659 by (blast intro: poly_divides_exp poly_divides_trans)
```
```   660
```
```   661 lemma poly_divides_add:
```
```   662    "[| p divides q; p divides r |] ==> p divides (q +++ r)"
```
```   663 apply (simp add: divides_def, auto)
```
```   664 apply (rule_tac x = "qa +++ qaa" in exI)
```
```   665 apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
```
```   666 done
```
```   667
```
```   668 lemma poly_divides_diff:
```
```   669    "[| p divides q; p divides (q +++ r) |] ==> p divides r"
```
```   670 apply (simp add: divides_def, auto)
```
```   671 apply (rule_tac x = "qaa +++ -- qa" in exI)
```
```   672 apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib compare_rls add_ac)
```
```   673 done
```
```   674
```
```   675 lemma poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q"
```
```   676 apply (erule poly_divides_diff)
```
```   677 apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
```
```   678 done
```
```   679
```
```   680 lemma poly_divides_zero: "poly p = poly [] ==> q divides p"
```
```   681 apply (simp add: divides_def)
```
```   682 apply (auto simp add: fun_eq poly_mult)
```
```   683 done
```
```   684
```
```   685 lemma poly_divides_zero2: "q divides []"
```
```   686 apply (simp add: divides_def)
```
```   687 apply (rule_tac x = "[]" in exI)
```
```   688 apply (auto simp add: fun_eq)
```
```   689 done
```
```   690 declare poly_divides_zero2 [simp]
```
```   691
```
```   692 text{*At last, we can consider the order of a root.*}
```
```   693
```
```   694
```
```   695 lemma poly_order_exists_lemma [rule_format]:
```
```   696      "\<forall>p. length p = d --> poly p \<noteq> poly []
```
```   697              --> (\<exists>n q. p = mulexp n [-a, 1] q & poly q a \<noteq> 0)"
```
```   698 apply (induct "d")
```
```   699 apply (simp add: fun_eq, safe)
```
```   700 apply (case_tac "poly p a = 0")
```
```   701 apply (drule_tac poly_linear_divides [THEN iffD1], safe)
```
```   702 apply (drule_tac x = q in spec)
```
```   703 apply (drule_tac poly_entire_neg [THEN iffD1], safe, force, blast)
```
```   704 apply (rule_tac x = "Suc n" in exI)
```
```   705 apply (rule_tac x = qa in exI)
```
```   706 apply (simp del: pmult_Cons)
```
```   707 apply (rule_tac x = 0 in exI, force)
```
```   708 done
```
```   709
```
```   710 (* FIXME: Tidy up *)
```
```   711 lemma poly_order_exists:
```
```   712      "[| length p = d; poly p \<noteq> poly [] |]
```
```   713       ==> \<exists>n. ([-a, 1] %^ n) divides p &
```
```   714                 ~(([-a, 1] %^ (Suc n)) divides p)"
```
```   715 apply (drule poly_order_exists_lemma [where a=a], assumption, clarify)
```
```   716 apply (rule_tac x = n in exI, safe)
```
```   717 apply (unfold divides_def)
```
```   718 apply (rule_tac x = q in exI)
```
```   719 apply (induct_tac "n", simp)
```
```   720 apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
```
```   721 apply safe
```
```   722 apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)")
```
```   723 apply simp
```
```   724 apply (induct_tac "n")
```
```   725 apply (simp del: pmult_Cons pexp_Suc)
```
```   726 apply (erule_tac Q = "poly q a = 0" in contrapos_np)
```
```   727 apply (simp add: poly_add poly_cmult)
```
```   728 apply (rule pexp_Suc [THEN ssubst])
```
```   729 apply (rule ccontr)
```
```   730 apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
```
```   731 done
```
```   732
```
```   733 lemma poly_one_divides: "[1] divides p"
```
```   734 by (simp add: divides_def, auto)
```
```   735 declare poly_one_divides [simp]
```
```   736
```
```   737 lemma poly_order: "poly p \<noteq> poly []
```
```   738       ==> EX! n. ([-a, 1] %^ n) divides p &
```
```   739                  ~(([-a, 1] %^ (Suc n)) divides p)"
```
```   740 apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
```
```   741 apply (cut_tac m = y and n = n in less_linear)
```
```   742 apply (drule_tac m = n in poly_exp_divides)
```
```   743 apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
```
```   744             simp del: pmult_Cons pexp_Suc)
```
```   745 done
```
```   746
```
```   747 text{*Order*}
```
```   748
```
```   749 lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
```
```   750 by (blast intro: someI2)
```
```   751
```
```   752 lemma order:
```
```   753       "(([-a, 1] %^ n) divides p &
```
```   754         ~(([-a, 1] %^ (Suc n)) divides p)) =
```
```   755         ((n = order a p) & ~(poly p = poly []))"
```
```   756 apply (unfold order_def)
```
```   757 apply (rule iffI)
```
```   758 apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order)
```
```   759 apply (blast intro!: poly_order [THEN [2] some1_equalityD])
```
```   760 done
```
```   761
```
```   762 lemma order2: "[| poly p \<noteq> poly [] |]
```
```   763       ==> ([-a, 1] %^ (order a p)) divides p &
```
```   764               ~(([-a, 1] %^ (Suc(order a p))) divides p)"
```
```   765 by (simp add: order del: pexp_Suc)
```
```   766
```
```   767 lemma order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
```
```   768          ~(([-a, 1] %^ (Suc n)) divides p)
```
```   769       |] ==> (n = order a p)"
```
```   770 by (insert order [of a n p], auto)
```
```   771
```
```   772 lemma order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
```
```   773          ~(([-a, 1] %^ (Suc n)) divides p))
```
```   774       ==> (n = order a p)"
```
```   775 by (blast intro: order_unique)
```
```   776
```
```   777 lemma order_poly: "poly p = poly q ==> order a p = order a q"
```
```   778 by (auto simp add: fun_eq divides_def poly_mult order_def)
```
```   779
```
```   780 lemma pexp_one: "p %^ (Suc 0) = p"
```
```   781 apply (induct "p")
```
```   782 apply (auto simp add: numeral_1_eq_1)
```
```   783 done
```
```   784 declare pexp_one [simp]
```
```   785
```
```   786 lemma lemma_order_root [rule_format]:
```
```   787      "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
```
```   788              --> poly p a = 0"
```
```   789 apply (induct "n", blast)
```
```   790 apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
```
```   791 done
```
```   792
```
```   793 lemma order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
```
```   794 apply (case_tac "poly p = poly []", auto)
```
```   795 apply (simp add: poly_linear_divides del: pmult_Cons, safe)
```
```   796 apply (drule_tac [!] a = a in order2)
```
```   797 apply (rule ccontr)
```
```   798 apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
```
```   799 apply (blast intro: lemma_order_root)
```
```   800 done
```
```   801
```
```   802 lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
```
```   803 apply (case_tac "poly p = poly []", auto)
```
```   804 apply (simp add: divides_def fun_eq poly_mult)
```
```   805 apply (rule_tac x = "[]" in exI)
```
```   806 apply (auto dest!: order2 [where a=a]
```
```   807 	    intro: poly_exp_divides simp del: pexp_Suc)
```
```   808 done
```
```   809
```
```   810 lemma order_decomp:
```
```   811      "poly p \<noteq> poly []
```
```   812       ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
```
```   813                 ~([-a, 1] divides q)"
```
```   814 apply (unfold divides_def)
```
```   815 apply (drule order2 [where a = a])
```
```   816 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
```
```   817 apply (rule_tac x = q in exI, safe)
```
```   818 apply (drule_tac x = qa in spec)
```
```   819 apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
```
```   820 done
```
```   821
```
```   822 text{*Important composition properties of orders.*}
```
```   823
```
```   824 lemma order_mult: "poly (p *** q) \<noteq> poly []
```
```   825       ==> order a (p *** q) = order a p + order a q"
```
```   826 apply (cut_tac a = a and p = "p***q" and n = "order a p + order a q" in order)
```
```   827 apply (auto simp add: poly_entire simp del: pmult_Cons)
```
```   828 apply (drule_tac a = a in order2)+
```
```   829 apply safe
```
```   830 apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
```
```   831 apply (rule_tac x = "qa *** qaa" in exI)
```
```   832 apply (simp add: poly_mult mult_ac del: pmult_Cons)
```
```   833 apply (drule_tac a = a in order_decomp)+
```
```   834 apply safe
```
```   835 apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
```
```   836 apply (simp add: poly_primes del: pmult_Cons)
```
```   837 apply (auto simp add: divides_def simp del: pmult_Cons)
```
```   838 apply (rule_tac x = qb in exI)
```
```   839 apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
```
```   840 apply (drule poly_mult_left_cancel [THEN iffD1], force)
```
```   841 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))) ")
```
```   842 apply (drule poly_mult_left_cancel [THEN iffD1], force)
```
```   843 apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
```
```   844 done
```
```   845
```
```   846 (* FIXME: too too long! *)
```
```   847 lemma lemma_order_pderiv [rule_format]:
```
```   848      "\<forall>p q a. 0 < n &
```
```   849        poly (pderiv p) \<noteq> poly [] &
```
```   850        poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
```
```   851        --> n = Suc (order a (pderiv p))"
```
```   852 apply (induct "n", safe)
```
```   853 apply (rule order_unique_lemma, rule conjI, assumption)
```
```   854 apply (subgoal_tac "\<forall>r. r divides (pderiv p) = r divides (pderiv ([-a, 1] %^ Suc n *** q))")
```
```   855 apply (drule_tac [2] poly_pderiv_welldef)
```
```   856  prefer 2 apply (simp add: divides_def del: pmult_Cons pexp_Suc)
```
```   857 apply (simp del: pmult_Cons pexp_Suc)
```
```   858 apply (rule conjI)
```
```   859 apply (simp add: divides_def fun_eq del: pmult_Cons pexp_Suc)
```
```   860 apply (rule_tac x = "[-a, 1] *** (pderiv q) +++ real (Suc n) %* q" in exI)
```
```   861 apply (simp add: poly_pderiv_mult poly_pderiv_exp_prime poly_add poly_mult poly_cmult right_distrib mult_ac del: pmult_Cons pexp_Suc)
```
```   862 apply (simp add: poly_mult right_distrib left_distrib mult_ac del: pmult_Cons)
```
```   863 apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl)
```
```   864 apply (unfold divides_def)
```
```   865 apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc)
```
```   866 apply (rule contrapos_np, assumption)
```
```   867 apply (rotate_tac 3, erule contrapos_np)
```
```   868 apply (simp del: pmult_Cons pexp_Suc, safe)
```
```   869 apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI)
```
```   870 apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
```
```   871 apply (drule poly_mult_left_cancel [THEN iffD1], simp)
```
```   872 apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left field_mult_cancel_left, safe)
```
```   873 apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1])
```
```   874 apply (simp (no_asm))
```
```   875 apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) =
```
```   876           (poly qa xa + - poly (pderiv q) xa) *
```
```   877           (poly ([- a, 1] %^ n) xa *
```
```   878            ((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))")
```
```   879 apply (simp only: mult_ac)
```
```   880 apply (rotate_tac 2)
```
```   881 apply (drule_tac x = xa in spec)
```
```   882 apply (simp add: left_distrib mult_ac del: pmult_Cons)
```
```   883 done
```
```   884
```
```   885 lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
```
```   886       ==> (order a p = Suc (order a (pderiv p)))"
```
```   887 apply (case_tac "poly p = poly []")
```
```   888 apply (auto dest: pderiv_zero)
```
```   889 apply (drule_tac a = a and p = p in order_decomp)
```
```   890 apply (blast intro: lemma_order_pderiv)
```
```   891 done
```
```   892
```
```   893 text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
```
```   894 (* `a la Harrison*}
```
```   895
```
```   896 lemma poly_squarefree_decomp_order: "[| poly (pderiv p) \<noteq> poly [];
```
```   897          poly p = poly (q *** d);
```
```   898          poly (pderiv p) = poly (e *** d);
```
```   899          poly d = poly (r *** p +++ s *** pderiv p)
```
```   900       |] ==> order a q = (if order a p = 0 then 0 else 1)"
```
```   901 apply (subgoal_tac "order a p = order a q + order a d")
```
```   902 apply (rule_tac [2] s = "order a (q *** d)" in trans)
```
```   903 prefer 2 apply (blast intro: order_poly)
```
```   904 apply (rule_tac [2] order_mult)
```
```   905  prefer 2 apply force
```
```   906 apply (case_tac "order a p = 0", simp)
```
```   907 apply (subgoal_tac "order a (pderiv p) = order a e + order a d")
```
```   908 apply (rule_tac [2] s = "order a (e *** d)" in trans)
```
```   909 prefer 2 apply (blast intro: order_poly)
```
```   910 apply (rule_tac [2] order_mult)
```
```   911  prefer 2 apply force
```
```   912 apply (case_tac "poly p = poly []")
```
```   913 apply (drule_tac p = p in pderiv_zero, simp)
```
```   914 apply (drule order_pderiv, assumption)
```
```   915 apply (subgoal_tac "order a (pderiv p) \<le> order a d")
```
```   916 apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides d")
```
```   917  prefer 2 apply (simp add: poly_entire order_divides)
```
```   918 apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides p & ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p) ")
```
```   919  prefer 3 apply (simp add: order_divides)
```
```   920  prefer 2 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
```
```   921 apply (rule_tac x = "r *** qa +++ s *** qaa" in exI)
```
```   922 apply (simp add: fun_eq poly_add poly_mult left_distrib right_distrib mult_ac del: pexp_Suc pmult_Cons, auto)
```
```   923 done
```
```   924
```
```   925
```
```   926 lemma poly_squarefree_decomp_order2: "[| poly (pderiv p) \<noteq> poly [];
```
```   927          poly p = poly (q *** d);
```
```   928          poly (pderiv p) = poly (e *** d);
```
```   929          poly d = poly (r *** p +++ s *** pderiv p)
```
```   930       |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
```
```   931 apply (blast intro: poly_squarefree_decomp_order)
```
```   932 done
```
```   933
```
```   934 lemma order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
```
```   935 by (rule order_root [THEN ssubst], auto)
```
```   936
```
```   937 lemma order_pderiv2: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
```
```   938       ==> (order a (pderiv p) = n) = (order a p = Suc n)"
```
```   939 apply (auto dest: order_pderiv)
```
```   940 done
```
```   941
```
```   942 lemma rsquarefree_roots:
```
```   943   "rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))"
```
```   944 apply (simp add: rsquarefree_def)
```
```   945 apply (case_tac "poly p = poly []", simp, simp)
```
```   946 apply (case_tac "poly (pderiv p) = poly []")
```
```   947 apply simp
```
```   948 apply (drule pderiv_iszero, clarify)
```
```   949 apply (subgoal_tac "\<forall>a. order a p = order a [h]")
```
```   950 apply (simp add: fun_eq)
```
```   951 apply (rule allI)
```
```   952 apply (cut_tac p = "[h]" and a = a in order_root)
```
```   953 apply (simp add: fun_eq)
```
```   954 apply (blast intro: order_poly)
```
```   955 apply (auto simp add: order_root order_pderiv2)
```
```   956 apply (drule spec, auto)
```
```   957 done
```
```   958
```
```   959 lemma pmult_one: "[1] *** p = p"
```
```   960 by auto
```
```   961 declare pmult_one [simp]
```
```   962
```
```   963 lemma poly_Nil_zero: "poly [] = poly [0]"
```
```   964 by (simp add: fun_eq)
```
```   965
```
```   966 lemma rsquarefree_decomp:
```
```   967      "[| rsquarefree p; poly p a = 0 |]
```
```   968       ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
```
```   969 apply (simp add: rsquarefree_def, safe)
```
```   970 apply (frule_tac a = a in order_decomp)
```
```   971 apply (drule_tac x = a in spec)
```
```   972 apply (drule_tac a = a in order_root2 [symmetric])
```
```   973 apply (auto simp del: pmult_Cons)
```
```   974 apply (rule_tac x = q in exI, safe)
```
```   975 apply (simp add: poly_mult fun_eq)
```
```   976 apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1])
```
```   977 apply (simp add: divides_def del: pmult_Cons, safe)
```
```   978 apply (drule_tac x = "[]" in spec)
```
```   979 apply (auto simp add: fun_eq)
```
```   980 done
```
```   981
```
```   982 lemma poly_squarefree_decomp: "[| poly (pderiv p) \<noteq> poly [];
```
```   983          poly p = poly (q *** d);
```
```   984          poly (pderiv p) = poly (e *** d);
```
```   985          poly d = poly (r *** p +++ s *** pderiv p)
```
```   986       |] ==> rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
```
```   987 apply (frule poly_squarefree_decomp_order2, assumption+)
```
```   988 apply (case_tac "poly p = poly []")
```
```   989 apply (blast dest: pderiv_zero)
```
```   990 apply (simp (no_asm) add: rsquarefree_def order_root del: pmult_Cons)
```
```   991 apply (simp add: poly_entire del: pmult_Cons)
```
```   992 done
```
```   993
```
```   994
```
```   995 text{*Normalization of a polynomial.*}
```
```   996
```
```   997 lemma poly_normalize: "poly (pnormalize p) = poly p"
```
```   998 apply (induct "p")
```
```   999 apply (auto simp add: fun_eq)
```
```  1000 done
```
```  1001 declare poly_normalize [simp]
```
```  1002
```
```  1003
```
```  1004 text{*The degree of a polynomial.*}
```
```  1005
```
```  1006 lemma lemma_degree_zero [rule_format]:
```
```  1007      "list_all (%c. c = 0) p -->  pnormalize p = []"
```
```  1008 by (induct "p", auto)
```
```  1009
```
```  1010 lemma degree_zero: "poly p = poly [] ==> degree p = 0"
```
```  1011 apply (simp add: degree_def)
```
```  1012 apply (case_tac "pnormalize p = []")
```
```  1013 apply (auto dest: lemma_degree_zero simp add: poly_zero)
```
```  1014 done
```
```  1015
```
```  1016 text{*Tidier versions of finiteness of roots.*}
```
```  1017
```
```  1018 lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x. poly p x = 0}"
```
```  1019 apply (auto simp add: poly_roots_finite)
```
```  1020 apply (rule_tac B = "{x::real. \<exists>n. (n::nat) < N & (x = j n) }" in finite_subset)
```
```  1021 apply (induct_tac [2] "N", auto)
```
```  1022 apply (subgoal_tac "{x::real. \<exists>na. na < Suc n & (x = j na) } = { (j n) } Un {x. \<exists>na. na < n & (x = j na) }")
```
```  1023 apply (auto simp add: less_Suc_eq)
```
```  1024 done
```
```  1025
```
```  1026 text{*bound for polynomial.*}
```
```  1027
```
```  1028 lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k"
```
```  1029 apply (induct "p", auto)
```
```  1030 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
```
```  1031 apply (rule abs_triangle_ineq)
```
```  1032 apply (auto intro!: mult_mono simp add: abs_mult)
```
```  1033 done
```
```  1034
```
```  1035 end
```