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