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