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