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