1.1 --- a/src/HOL/Transcendental.thy Fri Aug 19 08:40:15 2011 -0700
1.2 +++ b/src/HOL/Transcendental.thy Fri Aug 19 10:46:54 2011 -0700
1.3 @@ -803,9 +803,8 @@
1.4
1.5 subsection {* Exponential Function *}
1.6
1.7 -definition
1.8 - exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
1.9 - "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
1.10 +definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
1.11 + "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
1.12
1.13 lemma summable_exp_generic:
1.14 fixes x :: "'a::{real_normed_algebra_1,banach}"
1.15 @@ -863,14 +862,10 @@
1.16 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
1.17 by (simp add: diffs_def)
1.18
1.19 -lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
1.20 -by (auto simp add: exp_def)
1.21 -
1.22 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
1.23 -apply (simp add: exp_def)
1.24 -apply (subst lemma_exp_ext)
1.25 -apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)")
1.26 -apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs)
1.27 +unfolding exp_def scaleR_conv_of_real
1.28 +apply (rule DERIV_cong)
1.29 +apply (rule termdiffs [where K="of_real (1 + norm x)"])
1.30 apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
1.31 apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
1.32 apply (simp del: of_real_add)
1.33 @@ -1083,120 +1078,93 @@
1.34
1.35 subsection {* Natural Logarithm *}
1.36
1.37 -definition
1.38 - ln :: "real => real" where
1.39 +definition ln :: "real \<Rightarrow> real" where
1.40 "ln x = (THE u. exp u = x)"
1.41
1.42 lemma ln_exp [simp]: "ln (exp x) = x"
1.43 -by (simp add: ln_def)
1.44 + by (simp add: ln_def)
1.45
1.46 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
1.47 -by (auto dest: exp_total)
1.48 + by (auto dest: exp_total)
1.49
1.50 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
1.51 -apply (rule iffI)
1.52 -apply (erule subst, rule exp_gt_zero)
1.53 -apply (erule exp_ln)
1.54 -done
1.55 + by (metis exp_gt_zero exp_ln)
1.56
1.57 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
1.58 -by (erule subst, rule ln_exp)
1.59 + by (erule subst, rule ln_exp)
1.60
1.61 lemma ln_one [simp]: "ln 1 = 0"
1.62 -by (rule ln_unique, simp)
1.63 + by (rule ln_unique, simp)
1.64
1.65 lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y"
1.66 -by (rule ln_unique, simp add: exp_add)
1.67 + by (rule ln_unique, simp add: exp_add)
1.68
1.69 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
1.70 -by (rule ln_unique, simp add: exp_minus)
1.71 + by (rule ln_unique, simp add: exp_minus)
1.72
1.73 lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y"
1.74 -by (rule ln_unique, simp add: exp_diff)
1.75 + by (rule ln_unique, simp add: exp_diff)
1.76
1.77 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
1.78 -by (rule ln_unique, simp add: exp_real_of_nat_mult)
1.79 + by (rule ln_unique, simp add: exp_real_of_nat_mult)
1.80
1.81 lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
1.82 -by (subst exp_less_cancel_iff [symmetric], simp)
1.83 + by (subst exp_less_cancel_iff [symmetric], simp)
1.84
1.85 lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
1.86 -by (simp add: linorder_not_less [symmetric])
1.87 + by (simp add: linorder_not_less [symmetric])
1.88
1.89 lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
1.90 -by (simp add: order_eq_iff)
1.91 + by (simp add: order_eq_iff)
1.92
1.93 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
1.94 -apply (rule exp_le_cancel_iff [THEN iffD1])
1.95 -apply (simp add: exp_ge_add_one_self_aux)
1.96 -done
1.97 + apply (rule exp_le_cancel_iff [THEN iffD1])
1.98 + apply (simp add: exp_ge_add_one_self_aux)
1.99 + done
1.100
1.101 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
1.102 -by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
1.103 -
1.104 -lemma ln_ge_zero [simp]:
1.105 - assumes x: "1 \<le> x" shows "0 \<le> ln x"
1.106 -proof -
1.107 - have "0 < x" using x by arith
1.108 - hence "exp 0 \<le> exp (ln x)"
1.109 - by (simp add: x)
1.110 - thus ?thesis by (simp only: exp_le_cancel_iff)
1.111 -qed
1.112 -
1.113 -lemma ln_ge_zero_imp_ge_one:
1.114 - assumes ln: "0 \<le> ln x"
1.115 - and x: "0 < x"
1.116 - shows "1 \<le> x"
1.117 -proof -
1.118 - from ln have "ln 1 \<le> ln x" by simp
1.119 - thus ?thesis by (simp add: x del: ln_one)
1.120 -qed
1.121 -
1.122 -lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
1.123 -by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
1.124 -
1.125 -lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
1.126 -by (insert ln_ge_zero_iff [of x], arith)
1.127 -
1.128 -lemma ln_gt_zero:
1.129 - assumes x: "1 < x" shows "0 < ln x"
1.130 -proof -
1.131 - have "0 < x" using x by arith
1.132 - hence "exp 0 < exp (ln x)" by (simp add: x)
1.133 - thus ?thesis by (simp only: exp_less_cancel_iff)
1.134 -qed
1.135 -
1.136 -lemma ln_gt_zero_imp_gt_one:
1.137 - assumes ln: "0 < ln x"
1.138 - and x: "0 < x"
1.139 - shows "1 < x"
1.140 -proof -
1.141 - from ln have "ln 1 < ln x" by simp
1.142 - thus ?thesis by (simp add: x del: ln_one)
1.143 -qed
1.144 -
1.145 -lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
1.146 -by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
1.147 -
1.148 -lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
1.149 -by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
1.150 -
1.151 -lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
1.152 -by simp
1.153 + by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
1.154 +
1.155 +lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
1.156 + using ln_le_cancel_iff [of 1 x] by simp
1.157 +
1.158 +lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x"
1.159 + using ln_le_cancel_iff [of 1 x] by simp
1.160 +
1.161 +lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)"
1.162 + using ln_le_cancel_iff [of 1 x] by simp
1.163 +
1.164 +lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)"
1.165 + using ln_less_cancel_iff [of x 1] by simp
1.166 +
1.167 +lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
1.168 + using ln_less_cancel_iff [of 1 x] by simp
1.169 +
1.170 +lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x"
1.171 + using ln_less_cancel_iff [of 1 x] by simp
1.172 +
1.173 +lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)"
1.174 + using ln_less_cancel_iff [of 1 x] by simp
1.175 +
1.176 +lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)"
1.177 + using ln_inj_iff [of x 1] by simp
1.178 +
1.179 +lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
1.180 + by simp
1.181
1.182 lemma exp_ln_eq: "exp u = x ==> ln x = u"
1.183 -by auto
1.184 + by (rule ln_unique) (* TODO: delete *)
1.185
1.186 lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
1.187 -apply (subgoal_tac "isCont ln (exp (ln x))", simp)
1.188 -apply (rule isCont_inverse_function [where f=exp], simp_all)
1.189 -done
1.190 + apply (subgoal_tac "isCont ln (exp (ln x))", simp)
1.191 + apply (rule isCont_inverse_function [where f=exp], simp_all)
1.192 + done
1.193
1.194 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
1.195 -apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
1.196 -apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
1.197 -apply (simp_all add: abs_if isCont_ln)
1.198 -done
1.199 + apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
1.200 + apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
1.201 + apply (simp_all add: abs_if isCont_ln)
1.202 + done
1.203
1.204 lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
1.205 by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
1.206 @@ -1236,35 +1204,27 @@
1.207
1.208 subsection {* Sine and Cosine *}
1.209
1.210 -definition
1.211 - sin_coeff :: "nat \<Rightarrow> real" where
1.212 +definition sin_coeff :: "nat \<Rightarrow> real" where
1.213 "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
1.214
1.215 -definition
1.216 - cos_coeff :: "nat \<Rightarrow> real" where
1.217 +definition cos_coeff :: "nat \<Rightarrow> real" where
1.218 "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
1.219
1.220 -definition
1.221 - sin :: "real => real" where
1.222 - "sin x = (\<Sum>n. sin_coeff n * x ^ n)"
1.223 -
1.224 -definition
1.225 - cos :: "real => real" where
1.226 - "cos x = (\<Sum>n. cos_coeff n * x ^ n)"
1.227 +definition sin :: "real \<Rightarrow> real" where
1.228 + "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
1.229 +
1.230 +definition cos :: "real \<Rightarrow> real" where
1.231 + "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
1.232
1.233 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
1.234 unfolding sin_coeff_def
1.235 -apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
1.236 -apply (rule_tac [2] summable_exp)
1.237 -apply (rule_tac x = 0 in exI)
1.238 +apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
1.239 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.240 done
1.241
1.242 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
1.243 unfolding cos_coeff_def
1.244 -apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
1.245 -apply (rule_tac [2] summable_exp)
1.246 -apply (rule_tac x = 0 in exI)
1.247 +apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
1.248 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
1.249 done
1.250
1.251 @@ -1297,22 +1257,15 @@
1.252 lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
1.253 by (auto intro!: sums_unique sums_minus sin_converges)
1.254
1.255 -lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
1.256 - by (auto simp add: sin_def)
1.257 -
1.258 -lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
1.259 - by (auto simp add: cos_def)
1.260 -
1.261 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
1.262 -apply (simp add: cos_def)
1.263 -apply (subst lemma_sin_ext)
1.264 +unfolding sin_def cos_def
1.265 apply (auto simp add: sin_fdiffs2 [symmetric])
1.266 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
1.267 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
1.268 done
1.269
1.270 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
1.271 -apply (subst lemma_cos_ext)
1.272 +unfolding cos_def
1.273 apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
1.274 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
1.275 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
1.276 @@ -1339,196 +1292,122 @@
1.277 lemma cos_zero [simp]: "cos 0 = 1"
1.278 unfolding cos_def cos_coeff_def by (simp add: powser_zero)
1.279
1.280 -lemma DERIV_sin_sin_mult [simp]:
1.281 - "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
1.282 -by (rule DERIV_mult, auto)
1.283 -
1.284 -lemma DERIV_sin_sin_mult2 [simp]:
1.285 - "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
1.286 -apply (cut_tac x = x in DERIV_sin_sin_mult)
1.287 -apply (auto simp add: mult_assoc)
1.288 -done
1.289 -
1.290 -lemma DERIV_sin_realpow2 [simp]:
1.291 - "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
1.292 -by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
1.293 -
1.294 -lemma DERIV_sin_realpow2a [simp]:
1.295 - "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
1.296 -by (auto simp add: numeral_2_eq_2)
1.297 -
1.298 -lemma DERIV_cos_cos_mult [simp]:
1.299 - "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
1.300 -by (rule DERIV_mult, auto)
1.301 -
1.302 -lemma DERIV_cos_cos_mult2 [simp]:
1.303 - "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
1.304 -apply (cut_tac x = x in DERIV_cos_cos_mult)
1.305 -apply (auto simp add: mult_ac)
1.306 -done
1.307 -
1.308 -lemma DERIV_cos_realpow2 [simp]:
1.309 - "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
1.310 -by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
1.311 -
1.312 -lemma DERIV_cos_realpow2a [simp]:
1.313 - "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
1.314 -by (auto simp add: numeral_2_eq_2)
1.315 -
1.316 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
1.317 -by auto
1.318 -
1.319 -lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
1.320 - by (auto intro!: DERIV_intros)
1.321 -
1.322 -(* most useful *)
1.323 -lemma DERIV_cos_cos_mult3 [simp]:
1.324 - "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
1.325 - by (auto intro!: DERIV_intros)
1.326 -
1.327 -lemma DERIV_sin_circle_all:
1.328 - "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
1.329 - (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
1.330 - by (auto intro!: DERIV_intros)
1.331 -
1.332 -lemma DERIV_sin_circle_all_zero [simp]:
1.333 - "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
1.334 -by (cut_tac DERIV_sin_circle_all, auto)
1.335 -
1.336 -lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
1.337 -apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
1.338 -apply (auto simp add: numeral_2_eq_2)
1.339 -done
1.340 -
1.341 -lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
1.342 -apply (subst add_commute)
1.343 -apply (rule sin_cos_squared_add)
1.344 -done
1.345 + by (rule DERIV_cong) (* TODO: delete *)
1.346 +
1.347 +lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
1.348 +proof -
1.349 + have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
1.350 + by (auto intro!: DERIV_intros)
1.351 + hence "(sin x)\<twosuperior> + (cos x)\<twosuperior> = (sin 0)\<twosuperior> + (cos 0)\<twosuperior>"
1.352 + by (rule DERIV_isconst_all)
1.353 + thus "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1" by simp
1.354 +qed
1.355 +
1.356 +lemma sin_cos_squared_add2 [simp]: "(cos x)\<twosuperior> + (sin x)\<twosuperior> = 1"
1.357 + by (subst add_commute, rule sin_cos_squared_add)
1.358
1.359 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
1.360 -apply (cut_tac x = x in sin_cos_squared_add2)
1.361 -apply (simp add: power2_eq_square)
1.362 -done
1.363 + using sin_cos_squared_add2 [unfolded power2_eq_square] .
1.364
1.365 lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
1.366 -apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
1.367 -apply simp
1.368 -done
1.369 + unfolding eq_diff_eq by (rule sin_cos_squared_add)
1.370
1.371 lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
1.372 -apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
1.373 -apply simp
1.374 -done
1.375 + unfolding eq_diff_eq by (rule sin_cos_squared_add2)
1.376
1.377 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
1.378 -by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
1.379 + by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
1.380
1.381 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
1.382 -apply (insert abs_sin_le_one [of x])
1.383 -apply (simp add: abs_le_iff del: abs_sin_le_one)
1.384 -done
1.385 + using abs_sin_le_one [of x] unfolding abs_le_iff by simp
1.386
1.387 lemma sin_le_one [simp]: "sin x \<le> 1"
1.388 -apply (insert abs_sin_le_one [of x])
1.389 -apply (simp add: abs_le_iff del: abs_sin_le_one)
1.390 -done
1.391 + using abs_sin_le_one [of x] unfolding abs_le_iff by simp
1.392
1.393 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
1.394 -by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
1.395 + by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
1.396
1.397 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
1.398 -apply (insert abs_cos_le_one [of x])
1.399 -apply (simp add: abs_le_iff del: abs_cos_le_one)
1.400 -done
1.401 + using abs_cos_le_one [of x] unfolding abs_le_iff by simp
1.402
1.403 lemma cos_le_one [simp]: "cos x \<le> 1"
1.404 -apply (insert abs_cos_le_one [of x])
1.405 -apply (simp add: abs_le_iff del: abs_cos_le_one)
1.406 -done
1.407 + using abs_cos_le_one [of x] unfolding abs_le_iff by simp
1.408
1.409 lemma DERIV_fun_pow: "DERIV g x :> m ==>
1.410 DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
1.411 unfolding One_nat_def
1.412 -apply (rule lemma_DERIV_subst)
1.413 +apply (rule DERIV_cong)
1.414 apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
1.415 apply (rule DERIV_pow, auto)
1.416 done
1.417
1.418 lemma DERIV_fun_exp:
1.419 "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
1.420 -apply (rule lemma_DERIV_subst)
1.421 +apply (rule DERIV_cong)
1.422 apply (rule_tac f = exp in DERIV_chain2)
1.423 apply (rule DERIV_exp, auto)
1.424 done
1.425
1.426 lemma DERIV_fun_sin:
1.427 "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
1.428 -apply (rule lemma_DERIV_subst)
1.429 +apply (rule DERIV_cong)
1.430 apply (rule_tac f = sin in DERIV_chain2)
1.431 apply (rule DERIV_sin, auto)
1.432 done
1.433
1.434 lemma DERIV_fun_cos:
1.435 "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
1.436 -apply (rule lemma_DERIV_subst)
1.437 +apply (rule DERIV_cong)
1.438 apply (rule_tac f = cos in DERIV_chain2)
1.439 apply (rule DERIV_cos, auto)
1.440 done
1.441
1.442 -(* lemma *)
1.443 -lemma lemma_DERIV_sin_cos_add:
1.444 - "\<forall>x.
1.445 - DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.446 - (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
1.447 - by (auto intro!: DERIV_intros simp add: algebra_simps)
1.448 -
1.449 -lemma sin_cos_add [simp]:
1.450 +lemma sin_cos_add_lemma:
1.451 "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
1.452 (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
1.453 -apply (cut_tac y = 0 and x = x and y7 = y
1.454 - in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
1.455 -apply (auto simp add: numeral_2_eq_2)
1.456 -done
1.457 + (is "?f x = 0")
1.458 +proof -
1.459 + have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
1.460 + by (auto intro!: DERIV_intros simp add: algebra_simps)
1.461 + hence "?f x = ?f 0"
1.462 + by (rule DERIV_isconst_all)
1.463 + thus ?thesis by simp
1.464 +qed
1.465
1.466 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
1.467 -apply (cut_tac x = x and y = y in sin_cos_add)
1.468 -apply (simp del: sin_cos_add)
1.469 -done
1.470 + using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
1.471
1.472 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
1.473 -apply (cut_tac x = x and y = y in sin_cos_add)
1.474 -apply (simp del: sin_cos_add)
1.475 -done
1.476 -
1.477 -lemma lemma_DERIV_sin_cos_minus:
1.478 - "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
1.479 - by (auto intro!: DERIV_intros simp add: algebra_simps)
1.480 -
1.481 -
1.482 -lemma sin_cos_minus:
1.483 - "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
1.484 -apply (cut_tac y = 0 and x = x
1.485 - in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
1.486 -apply simp
1.487 -done
1.488 + using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
1.489 +
1.490 +lemma sin_cos_minus_lemma:
1.491 + "(sin(-x) + sin(x))\<twosuperior> + (cos(-x) - cos(x))\<twosuperior> = 0" (is "?f x = 0")
1.492 +proof -
1.493 + have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
1.494 + by (auto intro!: DERIV_intros simp add: algebra_simps)
1.495 + hence "?f x = ?f 0"
1.496 + by (rule DERIV_isconst_all)
1.497 + thus ?thesis by simp
1.498 +qed
1.499
1.500 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
1.501 - using sin_cos_minus [where x=x] by simp
1.502 + using sin_cos_minus_lemma [where x=x] by simp
1.503
1.504 lemma cos_minus [simp]: "cos (-x) = cos(x)"
1.505 - using sin_cos_minus [where x=x] by simp
1.506 + using sin_cos_minus_lemma [where x=x] by simp
1.507
1.508 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
1.509 -by (simp add: diff_minus sin_add)
1.510 + by (simp add: diff_minus sin_add)
1.511
1.512 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
1.513 -by (simp add: sin_diff mult_commute)
1.514 + by (simp add: sin_diff mult_commute)
1.515
1.516 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
1.517 -by (simp add: diff_minus cos_add)
1.518 + by (simp add: diff_minus cos_add)
1.519
1.520 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
1.521 -by (simp add: cos_diff mult_commute)
1.522 + by (simp add: cos_diff mult_commute)
1.523
1.524 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
1.525 using sin_add [where x=x and y=x] by simp
1.526 @@ -1540,8 +1419,7 @@
1.527
1.528 subsection {* The Constant Pi *}
1.529
1.530 -definition
1.531 - pi :: "real" where
1.532 +definition pi :: "real" where
1.533 "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
1.534
1.535 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
1.536 @@ -2429,7 +2307,7 @@
1.537 lemma DERIV_arcsin:
1.538 "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
1.539 apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
1.540 -apply (rule lemma_DERIV_subst [OF DERIV_sin])
1.541 +apply (rule DERIV_cong [OF DERIV_sin])
1.542 apply (simp add: cos_arcsin)
1.543 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
1.544 apply (rule power_strict_mono, simp, simp, simp)
1.545 @@ -2442,7 +2320,7 @@
1.546 lemma DERIV_arccos:
1.547 "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<twosuperior>))"
1.548 apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
1.549 -apply (rule lemma_DERIV_subst [OF DERIV_cos])
1.550 +apply (rule DERIV_cong [OF DERIV_cos])
1.551 apply (simp add: sin_arccos)
1.552 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
1.553 apply (rule power_strict_mono, simp, simp, simp)
1.554 @@ -2454,7 +2332,7 @@
1.555
1.556 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<twosuperior>)"
1.557 apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
1.558 -apply (rule lemma_DERIV_subst [OF DERIV_tan])
1.559 +apply (rule DERIV_cong [OF DERIV_tan])
1.560 apply (rule cos_arctan_not_zero)
1.561 apply (simp add: power_inverse tan_sec [symmetric])
1.562 apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp)
1.563 @@ -2543,8 +2421,8 @@
1.564 lemma tan_60: "tan (pi / 3) = sqrt 3"
1.565 unfolding tan_def by (simp add: sin_60 cos_60)
1.566
1.567 -lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
1.568 - by (auto intro!: DERIV_intros)
1.569 +lemma DERIV_sin_add: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
1.570 + by (auto intro!: DERIV_intros) (* TODO: delete *)
1.571
1.572 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
1.573 proof -