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