src/HOL/Library/Poly_Deriv.thy
 changeset 56383 8e7052e9fda4 parent 56381 0556204bc230 child 58199 5fbe474b5da8
```     1.1 --- a/src/HOL/Library/Poly_Deriv.thy	Thu Apr 03 17:56:08 2014 +0200
1.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Thu Apr 03 17:26:04 2014 +0100
1.3 @@ -28,9 +28,8 @@
1.5
1.6  lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
1.7 -  apply (induct p arbitrary: n, simp)
1.8 -  apply (simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
1.9 -  done
1.10 +  by (induct p arbitrary: n)
1.11 +     (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
1.12
1.13  primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list"
1.14  where
1.15 @@ -54,8 +53,7 @@
1.16    apply (cases "degree p", simp)
1.17    apply (rule le_degree)
1.18    apply (simp add: coeff_pderiv del: of_nat_Suc)
1.19 -  apply (rule subst, assumption)
1.20 -  apply (rule leading_coeff_neq_0, clarsimp)
1.21 +  apply (metis degree_0 leading_coeff_0_iff nat.distinct(1))
1.22    done
1.23
1.24  lemma pderiv_singleton [simp]: "pderiv [:a:] = 0"
1.25 @@ -74,10 +72,7 @@
1.26  by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
1.27
1.28  lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
1.29 -apply (induct p)
1.30 -apply simp
1.32 -done
1.33 +by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps)
1.34
1.35  lemma pderiv_power_Suc:
1.36    "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p"
1.37 @@ -87,13 +82,9 @@
1.38  apply (subst pderiv_mult)
1.39  apply (erule ssubst)
1.40  apply (simp only: of_nat_Suc smult_add_left smult_1_left)
1.41 -apply (simp add: algebra_simps) (* FIXME *)
1.43  done
1.44
1.45 -
1.46 -lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
1.47 -by (simp add: DERIV_cmult mult_commute [of _ c])
1.48 -
1.49  lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
1.50  by (rule DERIV_cong, rule DERIV_pow, simp)
1.51  declare DERIV_pow2 [simp] DERIV_pow [simp]
1.52 @@ -116,9 +107,8 @@
1.53
1.54  lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |]
1.55        ==> \<exists>x. a < x & x < b & (poly p x = 0)"
1.56 -apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl)
1.57 -apply (auto simp add: order_le_less)
1.58 -done
1.59 +using IVT_objl [of "poly p" a 0 b]
1.60 +by (auto simp add: order_le_less)
1.61
1.62  lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |]
1.63        ==> \<exists>x. a < x & x < b & (poly p x = 0)"
1.64 @@ -126,7 +116,8 @@
1.65
1.66  lemma poly_MVT: "(a::real) < b ==>
1.67       \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
1.68 -apply (drule_tac f = "poly p" in MVT, auto)
1.69 +using MVT [of a b "poly p"]
1.70 +apply auto
1.71  apply (rule_tac x = z in exI)
1.72  apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
1.73  done
1.74 @@ -135,16 +126,12 @@
1.75
1.76  lemma order_unique_lemma:
1.77    fixes p :: "'a::idom poly"
1.78 -  assumes "[:-a, 1:] ^ n dvd p \<and> \<not> [:-a, 1:] ^ Suc n dvd p"
1.79 +  assumes "[:-a, 1:] ^ n dvd p" "\<not> [:-a, 1:] ^ Suc n dvd p"
1.80    shows "n = order a p"
1.81  unfolding Polynomial.order_def
1.82  apply (rule Least_equality [symmetric])
1.83 -apply (rule assms [THEN conjunct2])
1.84 -apply (erule contrapos_np)
1.85 -apply (rule power_le_dvd)
1.86 -apply (rule assms [THEN conjunct1])
1.87 -apply simp
1.88 -done
1.89 +apply (rule assms)
1.90 +by (metis assms not_less_eq_eq power_le_dvd)
1.91
1.92  lemma lemma_order_pderiv1:
1.93    "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
1.94 @@ -158,45 +145,43 @@
1.95    shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
1.96    by (drule (1) Rings.dvd_diff, simp)
1.97
1.98 -lemma lemma_order_pderiv [rule_format]:
1.99 -     "\<forall>p q a. 0 < n &
1.100 -       pderiv p \<noteq> 0 &
1.101 -       p = [:- a, 1:] ^ n * q & ~ [:- a, 1:] dvd q
1.102 -       --> n = Suc (order a (pderiv p))"
1.103 - apply (cases "n", safe, rename_tac n p q a)
1.104 - apply (rule order_unique_lemma)
1.105 - apply (rule conjI)
1.106 -  apply (subst lemma_order_pderiv1)
1.108 -   apply (rule dvd_mult2)
1.109 -   apply (rule le_imp_power_dvd, simp)
1.110 -  apply (rule dvd_smult)
1.111 -  apply (rule dvd_mult)
1.112 -  apply (rule dvd_refl)
1.113 - apply (subst lemma_order_pderiv1)
1.114 - apply (erule contrapos_nn) back
1.115 - apply (subgoal_tac "[:- a, 1:] ^ Suc n dvd q * [:- a, 1:] ^ n")
1.116 -  apply (simp del: mult_pCons_left)
1.118 -  apply (simp del: mult_pCons_left)
1.119 - apply (drule dvd_smult_cancel, simp del: of_nat_Suc)
1.120 - apply assumption
1.121 -done
1.122 +lemma lemma_order_pderiv:
1.123 +  assumes n: "0 < n"
1.124 +      and pd: "pderiv p \<noteq> 0"
1.125 +      and pe: "p = [:- a, 1:] ^ n * q"
1.126 +      and nd: "~ [:- a, 1:] dvd q"
1.127 +    shows "n = Suc (order a (pderiv p))"
1.128 +using n
1.129 +proof -
1.130 +  have "pderiv ([:- a, 1:] ^ n * q) \<noteq> 0"
1.131 +    using assms by auto
1.132 +  obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([:- a, 1:] ^ Suc n' * q) \<noteq> 0"
1.133 +    using assms by (cases n) auto
1.134 +  then have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l"
1.135 +    by (metis dvd_add_cancel1 dvd_smult_iff dvd_triv_left of_nat_eq_0_iff old.nat.distinct(2))
1.136 +  have "n' = order a (pderiv ([:- a, 1:] ^ Suc n' * q))"
1.137 +  proof (rule order_unique_lemma)
1.138 +    show "[:- a, 1:] ^ n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
1.139 +      apply (subst lemma_order_pderiv1)
1.141 +      apply (metis dvdI dvd_mult2 power_Suc2)
1.142 +      apply (metis dvd_smult dvd_triv_right)
1.143 +      done
1.144 +  next
1.145 +    show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
1.146 +     apply (subst lemma_order_pderiv1)
1.147 +     by (metis * nd dvd_mult_cancel_right field_power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
1.148 +  qed
1.149 +  then show ?thesis
1.150 +    by (metis `n = Suc n'` pe)
1.151 +qed
1.152
1.153  lemma order_decomp:
1.154       "p \<noteq> 0
1.155        ==> \<exists>q. p = [:-a, 1:] ^ (order a p) * q &
1.156                  ~([:-a, 1:] dvd q)"
1.157  apply (drule order [where a=a])
1.158 -apply (erule conjE)
1.159 -apply (erule dvdE)
1.160 -apply (rule exI)
1.161 -apply (rule conjI, assumption)
1.162 -apply (erule contrapos_nn)
1.163 -apply (erule ssubst) back
1.164 -apply (subst power_Suc2)
1.165 -apply (erule mult_dvd_mono [OF dvd_refl])
1.166 -done
1.167 +by (metis dvdE dvd_mult_cancel_left power_Suc2)
1.168
1.169  lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
1.170        ==> (order a p = Suc (order a (pderiv p)))"
1.171 @@ -219,9 +204,9 @@
1.172      apply (drule order [where a=a and p=p, folded i_def t_def])
1.173      apply (drule order [where a=a and p=q, folded j_def t_def])
1.174      apply clarify
1.175 +    apply (erule dvdE)+
1.176      apply (rule order_unique_lemma [symmetric], fold t_def)
1.177 -    apply (erule dvdE)+
1.180      done
1.181  qed
1.182
1.183 @@ -230,9 +215,7 @@
1.184  lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
1.185  apply (cases "p = 0", auto)
1.186  apply (drule order_2 [where a=a and p=p])
1.187 -apply (erule contrapos_np)
1.188 -apply (erule power_le_dvd)
1.189 -apply simp
1.190 +apply (metis not_less_eq_eq power_le_dvd)
1.191  apply (erule power_le_dvd [OF order_1])
1.192  done
1.193
1.194 @@ -277,13 +260,11 @@
1.195           pderiv p = e * d;
1.196           d = r * p + s * pderiv p
1.197        |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
1.198 -apply (blast intro: poly_squarefree_decomp_order)
1.199 -done
1.200 +by (blast intro: poly_squarefree_decomp_order)
1.201
1.202  lemma order_pderiv2: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
1.203        ==> (order a (pderiv p) = n) = (order a p = Suc n)"
1.204 -apply (auto dest: order_pderiv)
1.205 -done
1.206 +by (auto dest: order_pderiv)
1.207
1.208  definition
1.209    rsquarefree :: "'a::idom poly => bool" where
1.210 @@ -300,13 +281,9 @@
1.211  apply (case_tac "p = 0", simp, simp)
1.212  apply (case_tac "pderiv p = 0")
1.213  apply simp
1.214 -apply (drule pderiv_iszero, clarify)
1.215 -apply simp
1.216 -apply (rule allI)
1.217 -apply (cut_tac p = "[:h:]" and a = a in order_root)
1.218 -apply simp
1.219 -apply (auto simp add: order_root order_pderiv2)
1.220 -apply (erule_tac x="a" in allE, simp)
1.221 +apply (drule pderiv_iszero, clarsimp)
1.222 +apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree)
1.223 +apply (force simp add: order_root order_pderiv2)
1.224  done
1.225
1.226  lemma poly_squarefree_decomp:
```