src/HOL/Library/Poly_Deriv.thy
author eberlm
Mon Jan 11 16:38:39 2016 +0100 (2016-01-11)
changeset 62128 3201ddb00097
parent 62072 bf3d9f113474
child 62175 8ffc4d0e652d
permissions -rw-r--r--
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
     1 (*  Title:      HOL/Library/Poly_Deriv.thy
     2     Author:     Amine Chaieb
     3     Author:     Brian Huffman
     4 *)
     5 
     6 section\<open>Polynomials and Differentiation\<close>
     7 
     8 theory Poly_Deriv
     9 imports Deriv Polynomial
    10 begin
    11 
    12 subsection \<open>Derivatives of univariate polynomials\<close>
    13 
    14 function pderiv :: "('a :: semidom) poly \<Rightarrow> 'a poly"
    15 where
    16   [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
    17   by (auto intro: pCons_cases)
    18 
    19 termination pderiv
    20   by (relation "measure degree") simp_all
    21 
    22 lemma pderiv_0 [simp]:
    23   "pderiv 0 = 0"
    24   using pderiv.simps [of 0 0] by simp
    25 
    26 lemma pderiv_pCons:
    27   "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
    28   by (simp add: pderiv.simps)
    29 
    30 lemma pderiv_1 [simp]: "pderiv 1 = 0" 
    31   unfolding one_poly_def by (simp add: pderiv_pCons)
    32 
    33 lemma pderiv_of_nat  [simp]: "pderiv (of_nat n) = 0"
    34   and pderiv_numeral [simp]: "pderiv (numeral m) = 0"
    35   by (simp_all add: of_nat_poly numeral_poly pderiv_pCons)
    36 
    37 lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
    38   by (induct p arbitrary: n) 
    39      (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
    40 
    41 fun pderiv_coeffs_code :: "('a :: semidom) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    42   "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
    43 | "pderiv_coeffs_code f [] = []"
    44 
    45 definition pderiv_coeffs :: "('a :: semidom) list \<Rightarrow> 'a list" where
    46   "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
    47 
    48 (* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *)
    49 lemma pderiv_coeffs_code: 
    50   "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * (nth_default 0 xs n)"
    51 proof (induct xs arbitrary: f n)
    52   case (Cons x xs f n)
    53   show ?case 
    54   proof (cases n)
    55     case 0
    56     thus ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0", auto simp: cCons_def)
    57   next
    58     case (Suc m) note n = this
    59     show ?thesis 
    60     proof (cases "pderiv_coeffs_code (f + 1) xs = [] \<and> f * x = 0")
    61       case False
    62       hence "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 
    63                nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" 
    64         by (auto simp: cCons_def n)
    65       also have "\<dots> = (f + of_nat n) * (nth_default 0 xs m)" 
    66         unfolding Cons by (simp add: n add_ac)
    67       finally show ?thesis by (simp add: n)
    68     next
    69       case True
    70       {
    71         fix g 
    72         have "pderiv_coeffs_code g xs = [] \<Longrightarrow> g + of_nat m = 0 \<or> nth_default 0 xs m = 0"
    73         proof (induct xs arbitrary: g m)
    74           case (Cons x xs g)
    75           from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []"
    76                             and g: "(g = 0 \<or> x = 0)"
    77             by (auto simp: cCons_def split: if_splits)
    78           note IH = Cons(1)[OF empty]
    79           from IH[of m] IH[of "m - 1"] g
    80           show ?case by (cases m, auto simp: field_simps)
    81         qed simp
    82       } note empty = this
    83       from True have "nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0"
    84         by (auto simp: cCons_def n)
    85       moreover have "(f + of_nat n) * nth_default 0 (x # xs) n = 0" using True
    86         by (simp add: n, insert empty[of "f+1"], auto simp: field_simps)
    87       ultimately show ?thesis by simp
    88     qed
    89   qed
    90 qed simp
    91 
    92 lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda> i. f (Suc i)) [0 ..< n]"
    93   by (induct n arbitrary: f, auto)
    94 
    95 lemma coeffs_pderiv_code [code abstract]:
    96   "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def
    97 proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
    98   case (1 n)
    99   have id: "coeff p (Suc n) = nth_default 0 (map (\<lambda>i. coeff p (Suc i)) [0..<degree p]) n"
   100     by (cases "n < degree p", auto simp: nth_default_def coeff_eq_0)
   101   show ?case unfolding coeffs_def map_upt_Suc by (auto simp: id)
   102 next
   103   case 2
   104   obtain n xs where id: "tl (coeffs p) = xs" "(1 :: 'a) = n" by auto
   105   from 2 show ?case
   106     unfolding id by (induct xs arbitrary: n, auto simp: cCons_def)
   107 qed
   108 
   109 context
   110   assumes "SORT_CONSTRAINT('a::{semidom, semiring_char_0})"
   111 begin
   112 
   113 lemma pderiv_eq_0_iff: 
   114   "pderiv (p :: 'a poly) = 0 \<longleftrightarrow> degree p = 0"
   115   apply (rule iffI)
   116   apply (cases p, simp)
   117   apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc)
   118   apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0)
   119   done
   120 
   121 lemma degree_pderiv: "degree (pderiv (p :: 'a poly)) = degree p - 1"
   122   apply (rule order_antisym [OF degree_le])
   123   apply (simp add: coeff_pderiv coeff_eq_0)
   124   apply (cases "degree p", simp)
   125   apply (rule le_degree)
   126   apply (simp add: coeff_pderiv del: of_nat_Suc)
   127   apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
   128   done
   129 
   130 lemma not_dvd_pderiv: 
   131   assumes "degree (p :: 'a poly) \<noteq> 0"
   132   shows "\<not> p dvd pderiv p"
   133 proof
   134   assume dvd: "p dvd pderiv p"
   135   then obtain q where p: "pderiv p = p * q" unfolding dvd_def by auto
   136   from dvd have le: "degree p \<le> degree (pderiv p)"
   137     by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff)
   138   from this[unfolded degree_pderiv] assms show False by auto
   139 qed
   140 
   141 lemma dvd_pderiv_iff [simp]: "(p :: 'a poly) dvd pderiv p \<longleftrightarrow> degree p = 0"
   142   using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric])
   143 
   144 end
   145 
   146 lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
   147 by (simp add: pderiv_pCons)
   148 
   149 lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
   150 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
   151 
   152 lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p"
   153 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
   154 
   155 lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
   156 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
   157 
   158 lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)"
   159 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
   160 
   161 lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
   162 by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
   163 
   164 lemma pderiv_power_Suc:
   165   "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p"
   166 apply (induct n)
   167 apply simp
   168 apply (subst power_Suc)
   169 apply (subst pderiv_mult)
   170 apply (erule ssubst)
   171 apply (simp only: of_nat_Suc smult_add_left smult_1_left)
   172 apply (simp add: algebra_simps)
   173 done
   174 
   175 lemma pderiv_setprod: "pderiv (setprod f (as)) = 
   176   (\<Sum>a \<in> as. setprod f (as - {a}) * pderiv (f a))"
   177 proof (induct as rule: infinite_finite_induct)
   178   case (insert a as)
   179   hence id: "setprod f (insert a as) = f a * setprod f as" 
   180     "\<And> g. setsum g (insert a as) = g a + setsum g as"
   181     "insert a as - {a} = as"
   182     by auto
   183   {
   184     fix b
   185     assume "b \<in> as"
   186     hence id2: "insert a as - {b} = insert a (as - {b})" using `a \<notin> as` by auto
   187     have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
   188       unfolding id2
   189       by (subst setprod.insert, insert insert, auto)
   190   } note id2 = this
   191   show ?case
   192     unfolding id pderiv_mult insert(3) setsum_right_distrib
   193     by (auto simp add: ac_simps id2 intro!: setsum.cong)
   194 qed auto
   195 
   196 lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
   197 by (rule DERIV_cong, rule DERIV_pow, simp)
   198 declare DERIV_pow2 [simp] DERIV_pow [simp]
   199 
   200 lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: 'a::real_normed_field) x :> D"
   201 by (rule DERIV_cong, rule DERIV_add, auto)
   202 
   203 lemma poly_DERIV [simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
   204   by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons)
   205 
   206 lemma continuous_on_poly [continuous_intros]: 
   207   fixes p :: "'a :: {real_normed_field} poly"
   208   assumes "continuous_on A f"
   209   shows   "continuous_on A (\<lambda>x. poly p (f x))"
   210 proof -
   211   have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))" 
   212     by (intro continuous_intros assms)
   213   also have "\<dots> = (\<lambda>x. poly p (f x))" by (intro ext) (simp add: poly_altdef mult_ac)
   214   finally show ?thesis .
   215 qed
   216 
   217 text\<open>Consequences of the derivative theorem above\<close>
   218 
   219 lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)"
   220 apply (simp add: real_differentiable_def)
   221 apply (blast intro: poly_DERIV)
   222 done
   223 
   224 lemma poly_isCont[simp]: "isCont (%x. poly p x) (x::real)"
   225 by (rule poly_DERIV [THEN DERIV_isCont])
   226 
   227 lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |]
   228       ==> \<exists>x. a < x & x < b & (poly p x = 0)"
   229 using IVT_objl [of "poly p" a 0 b]
   230 by (auto simp add: order_le_less)
   231 
   232 lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |]
   233       ==> \<exists>x. a < x & x < b & (poly p x = 0)"
   234 by (insert poly_IVT_pos [where p = "- p" ]) simp
   235 
   236 lemma poly_IVT:
   237   fixes p::"real poly"
   238   assumes "a<b" and "poly p a * poly p b < 0"
   239   shows "\<exists>x>a. x < b \<and> poly p x = 0"
   240 by (metis assms(1) assms(2) less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos)
   241 
   242 lemma poly_MVT: "(a::real) < b ==>
   243      \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
   244 using MVT [of a b "poly p"]
   245 apply auto
   246 apply (rule_tac x = z in exI)
   247 apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
   248 done
   249 
   250 lemma poly_MVT':
   251   assumes "{min a b..max a b} \<subseteq> A"
   252   shows   "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) (x::real)"
   253 proof (cases a b rule: linorder_cases)
   254   case less
   255   from poly_MVT[OF less, of p] guess x by (elim exE conjE)
   256   thus ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
   257 
   258 next
   259   case greater
   260   from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
   261   thus ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
   262 qed (insert assms, auto)
   263 
   264 lemma poly_pinfty_gt_lc:
   265   fixes p:: "real poly"
   266   assumes  "lead_coeff p > 0" 
   267   shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p" using assms
   268 proof (induct p)
   269   case 0
   270   thus ?case by auto
   271 next
   272   case (pCons a p)
   273   have "\<lbrakk>a\<noteq>0;p=0\<rbrakk> \<Longrightarrow> ?case" by auto
   274   moreover have "p\<noteq>0 \<Longrightarrow> ?case"
   275     proof -
   276       assume "p\<noteq>0"
   277       then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
   278       have gt_0:"lead_coeff p >0" using pCons(3) \<open>p\<noteq>0\<close> by auto
   279       def n\<equiv>"max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
   280       show ?thesis 
   281         proof (rule_tac x=n in exI,rule,rule) 
   282           fix x assume "n \<le> x"
   283           hence "lead_coeff p \<le> poly p x" 
   284             using gte_lcoeff unfolding n_def by auto
   285           hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
   286             by (intro frac_le,auto)
   287           hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using \<open>n\<le>x\<close>[unfolded n_def] by auto
   288           thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
   289             using \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x>0\<close> \<open>p\<noteq>0\<close>
   290             by (auto simp add:field_simps)
   291         qed
   292     qed
   293   ultimately show ?case by fastforce
   294 qed
   295 
   296 
   297 subsection \<open>Algebraic numbers\<close>
   298 
   299 text \<open>
   300   Algebraic numbers can be defined in two equivalent ways: all real numbers that are 
   301   roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry 
   302   uses the rational definition, but we need the integer definition.
   303 
   304   The equivalence is obvious since any rational polynomial can be multiplied with the 
   305   LCM of its coefficients, yielding an integer polynomial with the same roots.
   306 \<close>
   307 subsection \<open>Algebraic numbers\<close>
   308 
   309 definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool" where
   310   "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
   311 
   312 lemma algebraicI:
   313   assumes "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
   314   shows   "algebraic x"
   315   using assms unfolding algebraic_def by blast
   316   
   317 lemma algebraicE:
   318   assumes "algebraic x"
   319   obtains p where "\<And>i. coeff p i \<in> \<int>" "p \<noteq> 0" "poly p x = 0"
   320   using assms unfolding algebraic_def by blast
   321 
   322 lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
   323   using quotient_of_denom_pos[OF surjective_pairing] .
   324   
   325 lemma of_int_div_in_Ints: 
   326   "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: ring_div set)"
   327 proof (cases "of_int b = (0 :: 'a)")
   328   assume "b dvd a" "of_int b \<noteq> (0::'a)"
   329   then obtain c where "a = b * c" by (elim dvdE)
   330   with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
   331 qed auto
   332 
   333 lemma of_int_divide_in_Ints: 
   334   "b dvd a \<Longrightarrow> of_int a / of_int b \<in> (\<int> :: 'a :: field set)"
   335 proof (cases "of_int b = (0 :: 'a)")
   336   assume "b dvd a" "of_int b \<noteq> (0::'a)"
   337   then obtain c where "a = b * c" by (elim dvdE)
   338   with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
   339 qed auto
   340 
   341 lemma algebraic_altdef:
   342   fixes p :: "'a :: field_char_0 poly"
   343   shows "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)"
   344 proof safe
   345   fix p assume rat: "\<forall>i. coeff p i \<in> \<rat>" and root: "poly p x = 0" and nz: "p \<noteq> 0"
   346   def cs \<equiv> "coeffs p"
   347   from rat have "\<forall>c\<in>range (coeff p). \<exists>c'. c = of_rat c'" unfolding Rats_def by blast
   348   then obtain f where f: "\<And>i. coeff p i = of_rat (f (coeff p i))" 
   349     by (subst (asm) bchoice_iff) blast
   350   def cs' \<equiv> "map (quotient_of \<circ> f) (coeffs p)"
   351   def d \<equiv> "Lcm (set (map snd cs'))"
   352   def p' \<equiv> "smult (of_int d) p"
   353   
   354   have "\<forall>n. coeff p' n \<in> \<int>"
   355   proof
   356     fix n :: nat
   357     show "coeff p' n \<in> \<int>"
   358     proof (cases "n \<le> degree p")
   359       case True
   360       def c \<equiv> "coeff p n"
   361       def a \<equiv> "fst (quotient_of (f (coeff p n)))" and b \<equiv> "snd (quotient_of (f (coeff p n)))"
   362       have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp
   363       have "coeff p' n = of_int d * coeff p n" by (simp add: p'_def)
   364       also have "coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def
   365         by (subst quotient_of_div [of "f (coeff p n)", symmetric])
   366            (simp_all add: f [symmetric])
   367       also have "of_int d * \<dots> = of_rat (of_int (a*d) / of_int b)"
   368         by (simp add: of_rat_mult of_rat_divide)
   369       also from nz True have "b \<in> snd ` set cs'" unfolding cs'_def
   370         by (force simp: o_def b_def coeffs_def simp del: upt_Suc)
   371       hence "b dvd (a * d)" unfolding d_def by simp
   372       hence "of_int (a * d) / of_int b \<in> (\<int> :: rat set)"
   373         by (rule of_int_divide_in_Ints)
   374       hence "of_rat (of_int (a * d) / of_int b) \<in> \<int>" by (elim Ints_cases) auto
   375       finally show ?thesis .
   376     qed (auto simp: p'_def not_le coeff_eq_0)
   377   qed
   378   
   379   moreover have "set (map snd cs') \<subseteq> {0<..}"
   380     unfolding cs'_def using quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) 
   381   hence "d \<noteq> 0" unfolding d_def by (induction cs') simp_all
   382   with nz have "p' \<noteq> 0" by (simp add: p'_def)
   383   moreover from root have "poly p' x = 0" by (simp add: p'_def)
   384   ultimately show "algebraic x" unfolding algebraic_def by blast
   385 next
   386 
   387   assume "algebraic x"
   388   then obtain p where p: "\<And>i. coeff p i \<in> \<int>" "poly p x = 0" "p \<noteq> 0" 
   389     by (force simp: algebraic_def)
   390   moreover have "coeff p i \<in> \<int> \<Longrightarrow> coeff p i \<in> \<rat>" for i by (elim Ints_cases) simp
   391   ultimately show  "(\<exists>p. (\<forall>i. coeff p i \<in> \<rat>) \<and> p \<noteq> 0 \<and> poly p x = 0)" by auto
   392 qed
   393 
   394 
   395 text\<open>Lemmas for Derivatives\<close>
   396 
   397 lemma order_unique_lemma:
   398   fixes p :: "'a::idom poly"
   399   assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
   400   shows "n = order a p"
   401 unfolding Polynomial.order_def
   402 apply (rule Least_equality [symmetric])
   403 apply (fact assms)
   404 apply (rule classical)
   405 apply (erule notE)
   406 unfolding not_less_eq_eq
   407 using assms(1) apply (rule power_le_dvd)
   408 apply assumption
   409 done
   410 
   411 lemma lemma_order_pderiv1:
   412   "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
   413     smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
   414 apply (simp only: pderiv_mult pderiv_power_Suc)
   415 apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
   416 done
   417 
   418 lemma lemma_order_pderiv:
   419   fixes p :: "'a :: field_char_0 poly"
   420   assumes n: "0 < n" 
   421       and pd: "pderiv p \<noteq> 0" 
   422       and pe: "p = [:- a, 1:] ^ n * q" 
   423       and nd: "~ [:- a, 1:] dvd q"
   424     shows "n = Suc (order a (pderiv p))"
   425 using n 
   426 proof -
   427   have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
   428     using assms by auto
   429   obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
   430     using assms by (cases n) auto
   431   have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
   432     by (auto simp del: of_nat_Suc simp: dvd_add_right_iff dvd_smult_iff)
   433   have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))" 
   434   proof (rule order_unique_lemma)
   435     show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
   436       apply (subst lemma_order_pderiv1)
   437       apply (rule dvd_add)
   438       apply (metis dvdI dvd_mult2 power_Suc2)
   439       apply (metis dvd_smult dvd_triv_right)
   440       done
   441   next
   442     show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
   443      apply (subst lemma_order_pderiv1)
   444      by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
   445   qed
   446   then show ?thesis
   447     by (metis \<open>n = Suc n'\<close> pe)
   448 qed
   449 
   450 lemma order_decomp:
   451   assumes "p \<noteq> 0"
   452   shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
   453 proof -
   454   from assms have A: "[:- a, 1:] ^ order a p dvd p"
   455     and B: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order)
   456   from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" ..
   457   with B have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
   458     by simp
   459   then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
   460     by simp
   461   then have D: "\<not> [:- a, 1:] dvd q"
   462     using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
   463     by auto
   464   from C D show ?thesis by blast
   465 qed
   466 
   467 lemma order_pderiv:
   468   "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk> \<Longrightarrow>
   469      (order a p = Suc (order a (pderiv p)))"
   470 apply (case_tac "p = 0", simp)
   471 apply (drule_tac a = a and p = p in order_decomp)
   472 using neq0_conv
   473 apply (blast intro: lemma_order_pderiv)
   474 done
   475 
   476 lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q"
   477 proof -
   478   def i \<equiv> "order a p"
   479   def j \<equiv> "order a q"
   480   def t \<equiv> "[:-a, 1:]"
   481   have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0"
   482     unfolding t_def by (simp add: dvd_iff_poly_eq_0)
   483   assume "p * q \<noteq> 0"
   484   then show "order a (p * q) = i + j"
   485     apply clarsimp
   486     apply (drule order [where a=a and p=p, folded i_def t_def])
   487     apply (drule order [where a=a and p=q, folded j_def t_def])
   488     apply clarify
   489     apply (erule dvdE)+
   490     apply (rule order_unique_lemma [symmetric], fold t_def)
   491     apply (simp_all add: power_add t_dvd_iff)
   492     done
   493 qed
   494 
   495 lemma order_smult:
   496   assumes "c \<noteq> 0" 
   497   shows "order x (smult c p) = order x p"
   498 proof (cases "p = 0")
   499   case False
   500   have "smult c p = [:c:] * p" by simp
   501   also from assms False have "order x \<dots> = order x [:c:] + order x p" 
   502     by (subst order_mult) simp_all
   503   also from assms have "order x [:c:] = 0" by (intro order_0I) auto
   504   finally show ?thesis by simp
   505 qed simp
   506 
   507 (* Next two lemmas contributed by Wenda Li *)
   508 lemma order_1_eq_0 [simp]:"order x 1 = 0" 
   509   by (metis order_root poly_1 zero_neq_one)
   510 
   511 lemma order_power_n_n: "order a ([:-a,1:]^n)=n" 
   512 proof (induct n) (*might be proved more concisely using nat_less_induct*)
   513   case 0
   514   thus ?case by (metis order_root poly_1 power_0 zero_neq_one)
   515 next 
   516   case (Suc n)
   517   have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]" 
   518     by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral 
   519       one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
   520   moreover have "order a [:-a,1:]=1" unfolding order_def
   521     proof (rule Least_equality,rule ccontr)
   522       assume  "\<not> \<not> [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
   523       hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp
   524       hence "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:] )" 
   525         by (rule dvd_imp_degree_le,auto) 
   526       thus False by auto
   527     next
   528       fix y assume asm:"\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
   529       show "1 \<le> y" 
   530         proof (rule ccontr)
   531           assume "\<not> 1 \<le> y"
   532           hence "y=0" by auto
   533           hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
   534           thus False using asm by auto
   535         qed
   536     qed
   537   ultimately show ?case using Suc by auto
   538 qed
   539 
   540 text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>
   541 
   542 lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
   543 apply (cases "p = 0", auto)
   544 apply (drule order_2 [where a=a and p=p])
   545 apply (metis not_less_eq_eq power_le_dvd)
   546 apply (erule power_le_dvd [OF order_1])
   547 done
   548 
   549 lemma poly_squarefree_decomp_order:
   550   assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
   551   and p: "p = q * d"
   552   and p': "pderiv p = e * d"
   553   and d: "d = r * p + s * pderiv p"
   554   shows "order a q = (if order a p = 0 then 0 else 1)"
   555 proof (rule classical)
   556   assume 1: "order a q \<noteq> (if order a p = 0 then 0 else 1)"
   557   from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
   558   with p have "order a p = order a q + order a d"
   559     by (simp add: order_mult)
   560   with 1 have "order a p \<noteq> 0" by (auto split: if_splits)
   561   have "order a (pderiv p) = order a e + order a d"
   562     using \<open>pderiv p \<noteq> 0\<close> \<open>pderiv p = e * d\<close> by (simp add: order_mult)
   563   have "order a p = Suc (order a (pderiv p))"
   564     using \<open>pderiv p \<noteq> 0\<close> \<open>order a p \<noteq> 0\<close> by (rule order_pderiv)
   565   have "d \<noteq> 0" using \<open>p \<noteq> 0\<close> \<open>p = q * d\<close> by simp
   566   have "([:-a, 1:] ^ (order a (pderiv p))) dvd d"
   567     apply (simp add: d)
   568     apply (rule dvd_add)
   569     apply (rule dvd_mult)
   570     apply (simp add: order_divides \<open>p \<noteq> 0\<close>
   571            \<open>order a p = Suc (order a (pderiv p))\<close>)
   572     apply (rule dvd_mult)
   573     apply (simp add: order_divides)
   574     done
   575   then have "order a (pderiv p) \<le> order a d"
   576     using \<open>d \<noteq> 0\<close> by (simp add: order_divides)
   577   show ?thesis
   578     using \<open>order a p = order a q + order a d\<close>
   579     using \<open>order a (pderiv p) = order a e + order a d\<close>
   580     using \<open>order a p = Suc (order a (pderiv p))\<close>
   581     using \<open>order a (pderiv p) \<le> order a d\<close>
   582     by auto
   583 qed
   584 
   585 lemma poly_squarefree_decomp_order2: 
   586      "\<lbrakk>pderiv p \<noteq> (0 :: 'a :: field_char_0 poly);
   587        p = q * d;
   588        pderiv p = e * d;
   589        d = r * p + s * pderiv p
   590       \<rbrakk> \<Longrightarrow> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
   591 by (blast intro: poly_squarefree_decomp_order)
   592 
   593 lemma order_pderiv2: 
   594   "\<lbrakk>pderiv p \<noteq> 0; order a (p :: 'a :: field_char_0 poly) \<noteq> 0\<rbrakk>
   595       \<Longrightarrow> (order a (pderiv p) = n) = (order a p = Suc n)"
   596 by (auto dest: order_pderiv)
   597 
   598 definition
   599   rsquarefree :: "'a::idom poly => bool" where
   600   "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
   601 
   602 lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
   603 apply (simp add: pderiv_eq_0_iff)
   604 apply (case_tac p, auto split: if_splits)
   605 done
   606 
   607 lemma rsquarefree_roots:
   608   fixes p :: "'a :: field_char_0 poly"
   609   shows "rsquarefree p = (\<forall>a. \<not>(poly p a = 0 \<and> poly (pderiv p) a = 0))"
   610 apply (simp add: rsquarefree_def)
   611 apply (case_tac "p = 0", simp, simp)
   612 apply (case_tac "pderiv p = 0")
   613 apply simp
   614 apply (drule pderiv_iszero, clarsimp)
   615 apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
   616 apply (force simp add: order_root order_pderiv2)
   617 done
   618 
   619 lemma poly_squarefree_decomp:
   620   assumes "pderiv (p :: 'a :: field_char_0 poly) \<noteq> 0"
   621     and "p = q * d"
   622     and "pderiv p = e * d"
   623     and "d = r * p + s * pderiv p"
   624   shows "rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
   625 proof -
   626   from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto
   627   with \<open>p = q * d\<close> have "q \<noteq> 0" by simp
   628   have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
   629     using assms by (rule poly_squarefree_decomp_order2)
   630   with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> show ?thesis
   631     by (simp add: rsquarefree_def order_root)
   632 qed
   633 
   634 end