author  wenzelm 
Mon, 28 Dec 2015 01:28:28 +0100  
changeset 61945  1135b8de26c3 
parent 60867  86e7560e07d0 
child 62065  1546a042e87b 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Poly_Deriv.thy 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

2 
Author: Amine Chaieb 
41959  3 
Author: Brian Huffman 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

4 
*) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

5 

60500  6 
section\<open>Polynomials and Differentiation\<close> 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

7 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

8 
theory Poly_Deriv 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

9 
imports Deriv Polynomial 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

10 
begin 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

11 

60500  12 
subsection \<open>Derivatives of univariate polynomials\<close> 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

13 

52380  14 
function pderiv :: "'a::real_normed_field 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 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

21 

52380  22 
lemma pderiv_0 [simp]: 
23 
"pderiv 0 = 0" 

24 
using pderiv.simps [of 0 0] by simp 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

25 

52380  26 
lemma pderiv_pCons: 
27 
"pderiv (pCons a p) = p + pCons 0 (pderiv p)" 

28 
by (simp add: pderiv.simps) 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

29 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

30 
lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)" 
56383  31 
by (induct p arbitrary: n) 
32 
(auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split) 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

33 

52380  34 
primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list" 
35 
where 

36 
"pderiv_coeffs [] = []" 

37 
 "pderiv_coeffs (x # xs) = plus_coeffs xs (cCons 0 (pderiv_coeffs xs))" 

38 

39 
lemma coeffs_pderiv [code abstract]: 

40 
"coeffs (pderiv p) = pderiv_coeffs (coeffs p)" 

41 
by (rule sym, induct p) (simp_all add: pderiv_pCons coeffs_plus_eq_plus_coeffs cCons_def) 

42 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

43 
lemma pderiv_eq_0_iff: "pderiv p = 0 \<longleftrightarrow> degree p = 0" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

44 
apply (rule iffI) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

45 
apply (cases p, simp) 
52380  46 
apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc) 
47 
apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0) 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

48 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

49 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

50 
lemma degree_pderiv: "degree (pderiv p) = degree p  1" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

51 
apply (rule order_antisym [OF degree_le]) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

52 
apply (simp add: coeff_pderiv coeff_eq_0) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

53 
apply (cases "degree p", simp) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

54 
apply (rule le_degree) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

55 
apply (simp add: coeff_pderiv del: of_nat_Suc) 
56383  56 
apply (metis degree_0 leading_coeff_0_iff nat.distinct(1)) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

57 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

58 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

59 
lemma pderiv_singleton [simp]: "pderiv [:a:] = 0" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

60 
by (simp add: pderiv_pCons) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

61 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

62 
lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q" 
52380  63 
by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

64 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

65 
lemma pderiv_minus: "pderiv ( p) =  pderiv p" 
52380  66 
by (rule poly_eqI, simp add: coeff_pderiv) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

67 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

68 
lemma pderiv_diff: "pderiv (p  q) = pderiv p  pderiv q" 
52380  69 
by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

70 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

71 
lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)" 
52380  72 
by (rule poly_eqI, simp add: coeff_pderiv algebra_simps) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

73 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

74 
lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p" 
56383  75 
by (induct p) (auto simp: pderiv_add pderiv_smult pderiv_pCons algebra_simps) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

76 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

77 
lemma pderiv_power_Suc: 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

78 
"pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

79 
apply (induct n) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

80 
apply simp 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

81 
apply (subst power_Suc) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

82 
apply (subst pderiv_mult) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

83 
apply (erule ssubst) 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44317
diff
changeset

84 
apply (simp only: of_nat_Suc smult_add_left smult_1_left) 
56383  85 
apply (simp add: algebra_simps) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

86 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

87 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

88 
lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)" 
44317
b7e9fa025f15
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
huffman
parents:
41959
diff
changeset

89 
by (rule DERIV_cong, rule DERIV_pow, simp) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

90 
declare DERIV_pow2 [simp] DERIV_pow [simp] 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

91 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

92 
lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: 'a::real_normed_field) x :> D" 
44317
b7e9fa025f15
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
huffman
parents:
41959
diff
changeset

93 
by (rule DERIV_cong, rule DERIV_add, auto) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

94 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

95 
lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56217
diff
changeset

96 
by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

97 

60500  98 
text\<open>Consequences of the derivative theorem above\<close> 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

99 

56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
52380
diff
changeset

100 
lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)" 
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
52380
diff
changeset

101 
apply (simp add: real_differentiable_def) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

102 
apply (blast intro: poly_DERIV) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

103 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

104 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

105 
lemma poly_isCont[simp]: "isCont (%x. poly p x) (x::real)" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

106 
by (rule poly_DERIV [THEN DERIV_isCont]) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

107 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

108 
lemma poly_IVT_pos: "[ a < b; poly p (a::real) < 0; 0 < poly p b ] 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

109 
==> \<exists>x. a < x & x < b & (poly p x = 0)" 
56383  110 
using IVT_objl [of "poly p" a 0 b] 
111 
by (auto simp add: order_le_less) 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

112 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

113 
lemma poly_IVT_neg: "[ (a::real) < b; 0 < poly p a; poly p b < 0 ] 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

114 
==> \<exists>x. a < x & x < b & (poly p x = 0)" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

115 
by (insert poly_IVT_pos [where p = " p" ]) simp 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

116 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

117 
lemma poly_MVT: "(a::real) < b ==> 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

118 
\<exists>x. a < x & x < b & (poly p b  poly p a = (b  a) * poly (pderiv p) x)" 
56383  119 
using MVT [of a b "poly p"] 
120 
apply auto 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

121 
apply (rule_tac x = z in exI) 
56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
56181
diff
changeset

122 
apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique]) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

123 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

124 

60500  125 
text\<open>Lemmas for Derivatives\<close> 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

126 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

127 
lemma order_unique_lemma: 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

128 
fixes p :: "'a::idom poly" 
56383  129 
assumes "[:a, 1:] ^ n dvd p" "\<not> [:a, 1:] ^ Suc n dvd p" 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

130 
shows "n = order a p" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

131 
unfolding Polynomial.order_def 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

132 
apply (rule Least_equality [symmetric]) 
58199
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
56383
diff
changeset

133 
apply (fact assms) 
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
56383
diff
changeset

134 
apply (rule classical) 
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
56383
diff
changeset

135 
apply (erule notE) 
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
56383
diff
changeset

136 
unfolding not_less_eq_eq 
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
56383
diff
changeset

137 
using assms(1) apply (rule power_le_dvd) 
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
56383
diff
changeset

138 
apply assumption 
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
56383
diff
changeset

139 
done 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

140 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

141 
lemma lemma_order_pderiv1: 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

142 
"pderiv ([: a, 1:] ^ Suc n * q) = [: a, 1:] ^ Suc n * pderiv q + 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

143 
smult (of_nat (Suc n)) (q * [: a, 1:] ^ n)" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

144 
apply (simp only: pderiv_mult pderiv_power_Suc) 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
29985
diff
changeset

145 
apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

146 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

147 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

148 
lemma dvd_add_cancel1: 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

149 
fixes a b c :: "'a::comm_ring_1" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

150 
shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c" 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
31881
diff
changeset

151 
by (drule (1) Rings.dvd_diff, simp) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

152 

56383  153 
lemma lemma_order_pderiv: 
154 
assumes n: "0 < n" 

155 
and pd: "pderiv p \<noteq> 0" 

156 
and pe: "p = [: a, 1:] ^ n * q" 

157 
and nd: "~ [: a, 1:] dvd q" 

158 
shows "n = Suc (order a (pderiv p))" 

159 
using n 

160 
proof  

161 
have "pderiv ([: a, 1:] ^ n * q) \<noteq> 0" 

162 
using assms by auto 

163 
obtain n' where "n = Suc n'" "0 < Suc n'" "pderiv ([: a, 1:] ^ Suc n' * q) \<noteq> 0" 

164 
using assms by (cases n) auto 

165 
then have *: "!!k l. k dvd k * pderiv q + smult (of_nat (Suc n')) l \<Longrightarrow> k dvd l" 

166 
by (metis dvd_add_cancel1 dvd_smult_iff dvd_triv_left of_nat_eq_0_iff old.nat.distinct(2)) 

167 
have "n' = order a (pderiv ([: a, 1:] ^ Suc n' * q))" 

168 
proof (rule order_unique_lemma) 

169 
show "[: a, 1:] ^ n' dvd pderiv ([: a, 1:] ^ Suc n' * q)" 

170 
apply (subst lemma_order_pderiv1) 

171 
apply (rule dvd_add) 

172 
apply (metis dvdI dvd_mult2 power_Suc2) 

173 
apply (metis dvd_smult dvd_triv_right) 

174 
done 

175 
next 

176 
show "\<not> [: a, 1:] ^ Suc n' dvd pderiv ([: a, 1:] ^ Suc n' * q)" 

177 
apply (subst lemma_order_pderiv1) 

60867  178 
by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one) 
56383  179 
qed 
180 
then show ?thesis 

60500  181 
by (metis \<open>n = Suc n'\<close> pe) 
56383  182 
qed 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

183 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

184 
lemma order_decomp: 
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

185 
assumes "p \<noteq> 0" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

186 
shows "\<exists>q. p = [: a, 1:] ^ order a p * q \<and> \<not> [: a, 1:] dvd q" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

187 
proof  
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

188 
from assms have A: "[: a, 1:] ^ order a p dvd p" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

189 
and B: "\<not> [: a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

190 
from A obtain q where C: "p = [: a, 1:] ^ order a p * q" .. 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

191 
with B have "\<not> [: a, 1:] ^ Suc (order a p) dvd [: a, 1:] ^ order a p * q" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

192 
by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

193 
then have "\<not> [: a, 1:] ^ order a p * [: a, 1:] dvd [: a, 1:] ^ order a p * q" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

194 
by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

195 
then have D: "\<not> [: a, 1:] dvd q" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

196 
using idom_class.dvd_mult_cancel_left [of "[: a, 1:] ^ order a p" "[: a, 1:]" q] 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

197 
by auto 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

198 
from C D show ?thesis by blast 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60500
diff
changeset

199 
qed 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

200 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

201 
lemma order_pderiv: "[ pderiv p \<noteq> 0; order a p \<noteq> 0 ] 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

202 
==> (order a p = Suc (order a (pderiv p)))" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

203 
apply (case_tac "p = 0", simp) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

204 
apply (drule_tac a = a and p = p in order_decomp) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

205 
using neq0_conv 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

206 
apply (blast intro: lemma_order_pderiv) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

207 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

208 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

209 
lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

210 
proof  
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

211 
def i \<equiv> "order a p" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

212 
def j \<equiv> "order a q" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

213 
def t \<equiv> "[:a, 1:]" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

214 
have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

215 
unfolding t_def by (simp add: dvd_iff_poly_eq_0) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

216 
assume "p * q \<noteq> 0" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

217 
then show "order a (p * q) = i + j" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

218 
apply clarsimp 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

219 
apply (drule order [where a=a and p=p, folded i_def t_def]) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

220 
apply (drule order [where a=a and p=q, folded j_def t_def]) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

221 
apply clarify 
56383  222 
apply (erule dvdE)+ 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

223 
apply (rule order_unique_lemma [symmetric], fold t_def) 
56383  224 
apply (simp_all add: power_add t_dvd_iff) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

225 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

226 
qed 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

227 

60500  228 
text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close> 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

229 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

230 
lemma order_divides: "[:a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

231 
apply (cases "p = 0", auto) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

232 
apply (drule order_2 [where a=a and p=p]) 
56383  233 
apply (metis not_less_eq_eq power_le_dvd) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

234 
apply (erule power_le_dvd [OF order_1]) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

235 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

236 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

237 
lemma poly_squarefree_decomp_order: 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

238 
assumes "pderiv p \<noteq> 0" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

239 
and p: "p = q * d" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

240 
and p': "pderiv p = e * d" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

241 
and d: "d = r * p + s * pderiv p" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

242 
shows "order a q = (if order a p = 0 then 0 else 1)" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

243 
proof (rule classical) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

244 
assume 1: "order a q \<noteq> (if order a p = 0 then 0 else 1)" 
60500  245 
from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

246 
with p have "order a p = order a q + order a d" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

247 
by (simp add: order_mult) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

248 
with 1 have "order a p \<noteq> 0" by (auto split: if_splits) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

249 
have "order a (pderiv p) = order a e + order a d" 
60500  250 
using \<open>pderiv p \<noteq> 0\<close> \<open>pderiv p = e * d\<close> by (simp add: order_mult) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

251 
have "order a p = Suc (order a (pderiv p))" 
60500  252 
using \<open>pderiv p \<noteq> 0\<close> \<open>order a p \<noteq> 0\<close> by (rule order_pderiv) 
253 
have "d \<noteq> 0" using \<open>p \<noteq> 0\<close> \<open>p = q * d\<close> by simp 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

254 
have "([:a, 1:] ^ (order a (pderiv p))) dvd d" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

255 
apply (simp add: d) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

256 
apply (rule dvd_add) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

257 
apply (rule dvd_mult) 
60500  258 
apply (simp add: order_divides \<open>p \<noteq> 0\<close> 
259 
\<open>order a p = Suc (order a (pderiv p))\<close>) 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

260 
apply (rule dvd_mult) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

261 
apply (simp add: order_divides) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

262 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

263 
then have "order a (pderiv p) \<le> order a d" 
60500  264 
using \<open>d \<noteq> 0\<close> by (simp add: order_divides) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

265 
show ?thesis 
60500  266 
using \<open>order a p = order a q + order a d\<close> 
267 
using \<open>order a (pderiv p) = order a e + order a d\<close> 

268 
using \<open>order a p = Suc (order a (pderiv p))\<close> 

269 
using \<open>order a (pderiv p) \<le> order a d\<close> 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

270 
by auto 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

271 
qed 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

272 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

273 
lemma poly_squarefree_decomp_order2: "[ pderiv p \<noteq> 0; 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

274 
p = q * d; 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

275 
pderiv p = e * d; 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

276 
d = r * p + s * pderiv p 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

277 
] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)" 
56383  278 
by (blast intro: poly_squarefree_decomp_order) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

279 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

280 
lemma order_pderiv2: "[ pderiv p \<noteq> 0; order a p \<noteq> 0 ] 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

281 
==> (order a (pderiv p) = n) = (order a p = Suc n)" 
56383  282 
by (auto dest: order_pderiv) 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

283 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

284 
definition 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

285 
rsquarefree :: "'a::idom poly => bool" where 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

286 
"rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0)  (order a p = 1)))" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

287 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

288 
lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h:]" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

289 
apply (simp add: pderiv_eq_0_iff) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

290 
apply (case_tac p, auto split: if_splits) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

291 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

292 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

293 
lemma rsquarefree_roots: 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

294 
"rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

295 
apply (simp add: rsquarefree_def) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

296 
apply (case_tac "p = 0", simp, simp) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

297 
apply (case_tac "pderiv p = 0") 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

298 
apply simp 
56383  299 
apply (drule pderiv_iszero, clarsimp) 
300 
apply (metis coeff_0 coeff_pCons_0 degree_pCons_0 le0 le_antisym order_degree) 

301 
apply (force simp add: order_root order_pderiv2) 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

302 
done 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

303 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

304 
lemma poly_squarefree_decomp: 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

305 
assumes "pderiv p \<noteq> 0" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

306 
and "p = q * d" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

307 
and "pderiv p = e * d" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

308 
and "d = r * p + s * pderiv p" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

309 
shows "rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

310 
proof  
60500  311 
from \<open>pderiv p \<noteq> 0\<close> have "p \<noteq> 0" by auto 
312 
with \<open>p = q * d\<close> have "q \<noteq> 0" by simp 

29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

313 
have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)" 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

314 
using assms by (rule poly_squarefree_decomp_order2) 
60500  315 
with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> show ?thesis 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

316 
by (simp add: rsquarefree_def order_root) 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

317 
qed 
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

318 

57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
diff
changeset

319 
end 