1.1 --- a/src/HOL/MacLaurin.thy Fri Aug 19 08:40:15 2011 -0700
1.2 +++ b/src/HOL/MacLaurin.thy Fri Aug 19 10:46:54 2011 -0700
1.3 @@ -430,6 +430,7 @@
1.4 apply safe
1.5 apply (simp (no_asm))
1.6 apply (simp (no_asm) add: sin_expansion_lemma)
1.7 +apply (force intro!: DERIV_intros)
1.8 apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
1.9 apply (cases n, simp, simp)
1.10 apply (rule ccontr, simp)
1.11 @@ -458,6 +459,7 @@
1.12 apply safe
1.13 apply simp
1.14 apply (simp (no_asm) add: sin_expansion_lemma)
1.15 +apply (force intro!: DERIV_intros)
1.16 apply (erule ssubst)
1.17 apply (rule_tac x = t in exI, simp)
1.18 apply (rule setsum_cong[OF refl])
1.19 @@ -474,6 +476,7 @@
1.20 apply safe
1.21 apply simp
1.22 apply (simp (no_asm) add: sin_expansion_lemma)
1.23 +apply (force intro!: DERIV_intros)
1.24 apply (erule ssubst)
1.25 apply (rule_tac x = t in exI, simp)
1.26 apply (rule setsum_cong[OF refl])
2.1 --- a/src/HOL/Transcendental.thy Fri Aug 19 08:40:15 2011 -0700
2.2 +++ b/src/HOL/Transcendental.thy Fri Aug 19 10:46:54 2011 -0700
2.3 @@ -803,9 +803,8 @@
2.4
2.5 subsection {* Exponential Function *}
2.6
2.7 -definition
2.8 - exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
2.9 - "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
2.10 +definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
2.11 + "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
2.12
2.13 lemma summable_exp_generic:
2.14 fixes x :: "'a::{real_normed_algebra_1,banach}"
2.15 @@ -863,14 +862,10 @@
2.16 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
2.17 by (simp add: diffs_def)
2.18
2.19 -lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
2.20 -by (auto simp add: exp_def)
2.21 -
2.22 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
2.23 -apply (simp add: exp_def)
2.24 -apply (subst lemma_exp_ext)
2.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)")
2.26 -apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs)
2.27 +unfolding exp_def scaleR_conv_of_real
2.28 +apply (rule DERIV_cong)
2.29 +apply (rule termdiffs [where K="of_real (1 + norm x)"])
2.30 apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
2.31 apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
2.32 apply (simp del: of_real_add)
2.33 @@ -1083,120 +1078,93 @@
2.34
2.35 subsection {* Natural Logarithm *}
2.36
2.37 -definition
2.38 - ln :: "real => real" where
2.39 +definition ln :: "real \<Rightarrow> real" where
2.40 "ln x = (THE u. exp u = x)"
2.41
2.42 lemma ln_exp [simp]: "ln (exp x) = x"
2.43 -by (simp add: ln_def)
2.44 + by (simp add: ln_def)
2.45
2.46 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
2.47 -by (auto dest: exp_total)
2.48 + by (auto dest: exp_total)
2.49
2.50 lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
2.51 -apply (rule iffI)
2.52 -apply (erule subst, rule exp_gt_zero)
2.53 -apply (erule exp_ln)
2.54 -done
2.55 + by (metis exp_gt_zero exp_ln)
2.56
2.57 lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
2.58 -by (erule subst, rule ln_exp)
2.59 + by (erule subst, rule ln_exp)
2.60
2.61 lemma ln_one [simp]: "ln 1 = 0"
2.62 -by (rule ln_unique, simp)
2.63 + by (rule ln_unique, simp)
2.64
2.65 lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y"
2.66 -by (rule ln_unique, simp add: exp_add)
2.67 + by (rule ln_unique, simp add: exp_add)
2.68
2.69 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
2.70 -by (rule ln_unique, simp add: exp_minus)
2.71 + by (rule ln_unique, simp add: exp_minus)
2.72
2.73 lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y"
2.74 -by (rule ln_unique, simp add: exp_diff)
2.75 + by (rule ln_unique, simp add: exp_diff)
2.76
2.77 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
2.78 -by (rule ln_unique, simp add: exp_real_of_nat_mult)
2.79 + by (rule ln_unique, simp add: exp_real_of_nat_mult)
2.80
2.81 lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
2.82 -by (subst exp_less_cancel_iff [symmetric], simp)
2.83 + by (subst exp_less_cancel_iff [symmetric], simp)
2.84
2.85 lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
2.86 -by (simp add: linorder_not_less [symmetric])
2.87 + by (simp add: linorder_not_less [symmetric])
2.88
2.89 lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
2.90 -by (simp add: order_eq_iff)
2.91 + by (simp add: order_eq_iff)
2.92
2.93 lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
2.94 -apply (rule exp_le_cancel_iff [THEN iffD1])
2.95 -apply (simp add: exp_ge_add_one_self_aux)
2.96 -done
2.97 + apply (rule exp_le_cancel_iff [THEN iffD1])
2.98 + apply (simp add: exp_ge_add_one_self_aux)
2.99 + done
2.100
2.101 lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
2.102 -by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
2.103 -
2.104 -lemma ln_ge_zero [simp]:
2.105 - assumes x: "1 \<le> x" shows "0 \<le> ln x"
2.106 -proof -
2.107 - have "0 < x" using x by arith
2.108 - hence "exp 0 \<le> exp (ln x)"
2.109 - by (simp add: x)
2.110 - thus ?thesis by (simp only: exp_le_cancel_iff)
2.111 -qed
2.112 -
2.113 -lemma ln_ge_zero_imp_ge_one:
2.114 - assumes ln: "0 \<le> ln x"
2.115 - and x: "0 < x"
2.116 - shows "1 \<le> x"
2.117 -proof -
2.118 - from ln have "ln 1 \<le> ln x" by simp
2.119 - thus ?thesis by (simp add: x del: ln_one)
2.120 -qed
2.121 -
2.122 -lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
2.123 -by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
2.124 -
2.125 -lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
2.126 -by (insert ln_ge_zero_iff [of x], arith)
2.127 -
2.128 -lemma ln_gt_zero:
2.129 - assumes x: "1 < x" shows "0 < ln x"
2.130 -proof -
2.131 - have "0 < x" using x by arith
2.132 - hence "exp 0 < exp (ln x)" by (simp add: x)
2.133 - thus ?thesis by (simp only: exp_less_cancel_iff)
2.134 -qed
2.135 -
2.136 -lemma ln_gt_zero_imp_gt_one:
2.137 - assumes ln: "0 < ln x"
2.138 - and x: "0 < x"
2.139 - shows "1 < x"
2.140 -proof -
2.141 - from ln have "ln 1 < ln x" by simp
2.142 - thus ?thesis by (simp add: x del: ln_one)
2.143 -qed
2.144 -
2.145 -lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
2.146 -by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
2.147 -
2.148 -lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
2.149 -by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
2.150 -
2.151 -lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
2.152 -by simp
2.153 + by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
2.154 +
2.155 +lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
2.156 + using ln_le_cancel_iff [of 1 x] by simp
2.157 +
2.158 +lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x"
2.159 + using ln_le_cancel_iff [of 1 x] by simp
2.160 +
2.161 +lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)"
2.162 + using ln_le_cancel_iff [of 1 x] by simp
2.163 +
2.164 +lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)"
2.165 + using ln_less_cancel_iff [of x 1] by simp
2.166 +
2.167 +lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
2.168 + using ln_less_cancel_iff [of 1 x] by simp
2.169 +
2.170 +lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x"
2.171 + using ln_less_cancel_iff [of 1 x] by simp
2.172 +
2.173 +lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)"
2.174 + using ln_less_cancel_iff [of 1 x] by simp
2.175 +
2.176 +lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)"
2.177 + using ln_inj_iff [of x 1] by simp
2.178 +
2.179 +lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
2.180 + by simp
2.181
2.182 lemma exp_ln_eq: "exp u = x ==> ln x = u"
2.183 -by auto
2.184 + by (rule ln_unique) (* TODO: delete *)
2.185
2.186 lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
2.187 -apply (subgoal_tac "isCont ln (exp (ln x))", simp)
2.188 -apply (rule isCont_inverse_function [where f=exp], simp_all)
2.189 -done
2.190 + apply (subgoal_tac "isCont ln (exp (ln x))", simp)
2.191 + apply (rule isCont_inverse_function [where f=exp], simp_all)
2.192 + done
2.193
2.194 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
2.195 -apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
2.196 -apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
2.197 -apply (simp_all add: abs_if isCont_ln)
2.198 -done
2.199 + apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
2.200 + apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
2.201 + apply (simp_all add: abs_if isCont_ln)
2.202 + done
2.203
2.204 lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
2.205 by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
2.206 @@ -1236,35 +1204,27 @@
2.207
2.208 subsection {* Sine and Cosine *}
2.209
2.210 -definition
2.211 - sin_coeff :: "nat \<Rightarrow> real" where
2.212 +definition sin_coeff :: "nat \<Rightarrow> real" where
2.213 "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
2.214
2.215 -definition
2.216 - cos_coeff :: "nat \<Rightarrow> real" where
2.217 +definition cos_coeff :: "nat \<Rightarrow> real" where
2.218 "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
2.219
2.220 -definition
2.221 - sin :: "real => real" where
2.222 - "sin x = (\<Sum>n. sin_coeff n * x ^ n)"
2.223 -
2.224 -definition
2.225 - cos :: "real => real" where
2.226 - "cos x = (\<Sum>n. cos_coeff n * x ^ n)"
2.227 +definition sin :: "real \<Rightarrow> real" where
2.228 + "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
2.229 +
2.230 +definition cos :: "real \<Rightarrow> real" where
2.231 + "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
2.232
2.233 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
2.234 unfolding sin_coeff_def
2.235 -apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
2.236 -apply (rule_tac [2] summable_exp)
2.237 -apply (rule_tac x = 0 in exI)
2.238 +apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
2.239 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
2.240 done
2.241
2.242 lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
2.243 unfolding cos_coeff_def
2.244 -apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
2.245 -apply (rule_tac [2] summable_exp)
2.246 -apply (rule_tac x = 0 in exI)
2.247 +apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
2.248 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
2.249 done
2.250
2.251 @@ -1297,22 +1257,15 @@
2.252 lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
2.253 by (auto intro!: sums_unique sums_minus sin_converges)
2.254
2.255 -lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
2.256 - by (auto simp add: sin_def)
2.257 -
2.258 -lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
2.259 - by (auto simp add: cos_def)
2.260 -
2.261 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
2.262 -apply (simp add: cos_def)
2.263 -apply (subst lemma_sin_ext)
2.264 +unfolding sin_def cos_def
2.265 apply (auto simp add: sin_fdiffs2 [symmetric])
2.266 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
2.267 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
2.268 done
2.269
2.270 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
2.271 -apply (subst lemma_cos_ext)
2.272 +unfolding cos_def
2.273 apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
2.274 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
2.275 apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
2.276 @@ -1339,196 +1292,122 @@
2.277 lemma cos_zero [simp]: "cos 0 = 1"
2.278 unfolding cos_def cos_coeff_def by (simp add: powser_zero)
2.279
2.280 -lemma DERIV_sin_sin_mult [simp]:
2.281 - "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
2.282 -by (rule DERIV_mult, auto)
2.283 -
2.284 -lemma DERIV_sin_sin_mult2 [simp]:
2.285 - "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
2.286 -apply (cut_tac x = x in DERIV_sin_sin_mult)
2.287 -apply (auto simp add: mult_assoc)
2.288 -done
2.289 -
2.290 -lemma DERIV_sin_realpow2 [simp]:
2.291 - "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
2.292 -by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
2.293 -
2.294 -lemma DERIV_sin_realpow2a [simp]:
2.295 - "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
2.296 -by (auto simp add: numeral_2_eq_2)
2.297 -
2.298 -lemma DERIV_cos_cos_mult [simp]:
2.299 - "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
2.300 -by (rule DERIV_mult, auto)
2.301 -
2.302 -lemma DERIV_cos_cos_mult2 [simp]:
2.303 - "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
2.304 -apply (cut_tac x = x in DERIV_cos_cos_mult)
2.305 -apply (auto simp add: mult_ac)
2.306 -done
2.307 -
2.308 -lemma DERIV_cos_realpow2 [simp]:
2.309 - "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
2.310 -by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
2.311 -
2.312 -lemma DERIV_cos_realpow2a [simp]:
2.313 - "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
2.314 -by (auto simp add: numeral_2_eq_2)
2.315 -
2.316 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
2.317 -by auto
2.318 -
2.319 -lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
2.320 - by (auto intro!: DERIV_intros)
2.321 -
2.322 -(* most useful *)
2.323 -lemma DERIV_cos_cos_mult3 [simp]:
2.324 - "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
2.325 - by (auto intro!: DERIV_intros)
2.326 -
2.327 -lemma DERIV_sin_circle_all:
2.328 - "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
2.329 - (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
2.330 - by (auto intro!: DERIV_intros)
2.331 -
2.332 -lemma DERIV_sin_circle_all_zero [simp]:
2.333 - "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
2.334 -by (cut_tac DERIV_sin_circle_all, auto)
2.335 -
2.336 -lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
2.337 -apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
2.338 -apply (auto simp add: numeral_2_eq_2)
2.339 -done
2.340 -
2.341 -lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
2.342 -apply (subst add_commute)
2.343 -apply (rule sin_cos_squared_add)
2.344 -done
2.345 + by (rule DERIV_cong) (* TODO: delete *)
2.346 +
2.347 +lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
2.348 +proof -
2.349 + have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
2.350 + by (auto intro!: DERIV_intros)
2.351 + hence "(sin x)\<twosuperior> + (cos x)\<twosuperior> = (sin 0)\<twosuperior> + (cos 0)\<twosuperior>"
2.352 + by (rule DERIV_isconst_all)
2.353 + thus "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1" by simp
2.354 +qed
2.355 +
2.356 +lemma sin_cos_squared_add2 [simp]: "(cos x)\<twosuperior> + (sin x)\<twosuperior> = 1"
2.357 + by (subst add_commute, rule sin_cos_squared_add)
2.358
2.359 lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
2.360 -apply (cut_tac x = x in sin_cos_squared_add2)
2.361 -apply (simp add: power2_eq_square)
2.362 -done
2.363 + using sin_cos_squared_add2 [unfolded power2_eq_square] .
2.364
2.365 lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
2.366 -apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
2.367 -apply simp
2.368 -done
2.369 + unfolding eq_diff_eq by (rule sin_cos_squared_add)
2.370
2.371 lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
2.372 -apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
2.373 -apply simp
2.374 -done
2.375 + unfolding eq_diff_eq by (rule sin_cos_squared_add2)
2.376
2.377 lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
2.378 -by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
2.379 + by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
2.380
2.381 lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
2.382 -apply (insert abs_sin_le_one [of x])
2.383 -apply (simp add: abs_le_iff del: abs_sin_le_one)
2.384 -done
2.385 + using abs_sin_le_one [of x] unfolding abs_le_iff by simp
2.386
2.387 lemma sin_le_one [simp]: "sin x \<le> 1"
2.388 -apply (insert abs_sin_le_one [of x])
2.389 -apply (simp add: abs_le_iff del: abs_sin_le_one)
2.390 -done
2.391 + using abs_sin_le_one [of x] unfolding abs_le_iff by simp
2.392
2.393 lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
2.394 -by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
2.395 + by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
2.396
2.397 lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
2.398 -apply (insert abs_cos_le_one [of x])
2.399 -apply (simp add: abs_le_iff del: abs_cos_le_one)
2.400 -done
2.401 + using abs_cos_le_one [of x] unfolding abs_le_iff by simp
2.402
2.403 lemma cos_le_one [simp]: "cos x \<le> 1"
2.404 -apply (insert abs_cos_le_one [of x])
2.405 -apply (simp add: abs_le_iff del: abs_cos_le_one)
2.406 -done
2.407 + using abs_cos_le_one [of x] unfolding abs_le_iff by simp
2.408
2.409 lemma DERIV_fun_pow: "DERIV g x :> m ==>
2.410 DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
2.411 unfolding One_nat_def
2.412 -apply (rule lemma_DERIV_subst)
2.413 +apply (rule DERIV_cong)
2.414 apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
2.415 apply (rule DERIV_pow, auto)
2.416 done
2.417
2.418 lemma DERIV_fun_exp:
2.419 "DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
2.420 -apply (rule lemma_DERIV_subst)
2.421 +apply (rule DERIV_cong)
2.422 apply (rule_tac f = exp in DERIV_chain2)
2.423 apply (rule DERIV_exp, auto)
2.424 done
2.425
2.426 lemma DERIV_fun_sin:
2.427 "DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
2.428 -apply (rule lemma_DERIV_subst)
2.429 +apply (rule DERIV_cong)
2.430 apply (rule_tac f = sin in DERIV_chain2)
2.431 apply (rule DERIV_sin, auto)
2.432 done
2.433
2.434 lemma DERIV_fun_cos:
2.435 "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
2.436 -apply (rule lemma_DERIV_subst)
2.437 +apply (rule DERIV_cong)
2.438 apply (rule_tac f = cos in DERIV_chain2)
2.439 apply (rule DERIV_cos, auto)
2.440 done
2.441
2.442 -(* lemma *)
2.443 -lemma lemma_DERIV_sin_cos_add:
2.444 - "\<forall>x.
2.445 - DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
2.446 - (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
2.447 - by (auto intro!: DERIV_intros simp add: algebra_simps)
2.448 -
2.449 -lemma sin_cos_add [simp]:
2.450 +lemma sin_cos_add_lemma:
2.451 "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
2.452 (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
2.453 -apply (cut_tac y = 0 and x = x and y7 = y
2.454 - in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
2.455 -apply (auto simp add: numeral_2_eq_2)
2.456 -done
2.457 + (is "?f x = 0")
2.458 +proof -
2.459 + have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
2.460 + by (auto intro!: DERIV_intros simp add: algebra_simps)
2.461 + hence "?f x = ?f 0"
2.462 + by (rule DERIV_isconst_all)
2.463 + thus ?thesis by simp
2.464 +qed
2.465
2.466 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
2.467 -apply (cut_tac x = x and y = y in sin_cos_add)
2.468 -apply (simp del: sin_cos_add)
2.469 -done
2.470 + using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
2.471
2.472 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
2.473 -apply (cut_tac x = x and y = y in sin_cos_add)
2.474 -apply (simp del: sin_cos_add)
2.475 -done
2.476 -
2.477 -lemma lemma_DERIV_sin_cos_minus:
2.478 - "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
2.479 - by (auto intro!: DERIV_intros simp add: algebra_simps)
2.480 -
2.481 -
2.482 -lemma sin_cos_minus:
2.483 - "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
2.484 -apply (cut_tac y = 0 and x = x
2.485 - in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
2.486 -apply simp
2.487 -done
2.488 + using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
2.489 +
2.490 +lemma sin_cos_minus_lemma:
2.491 + "(sin(-x) + sin(x))\<twosuperior> + (cos(-x) - cos(x))\<twosuperior> = 0" (is "?f x = 0")
2.492 +proof -
2.493 + have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
2.494 + by (auto intro!: DERIV_intros simp add: algebra_simps)
2.495 + hence "?f x = ?f 0"
2.496 + by (rule DERIV_isconst_all)
2.497 + thus ?thesis by simp
2.498 +qed
2.499
2.500 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
2.501 - using sin_cos_minus [where x=x] by simp
2.502 + using sin_cos_minus_lemma [where x=x] by simp
2.503
2.504 lemma cos_minus [simp]: "cos (-x) = cos(x)"
2.505 - using sin_cos_minus [where x=x] by simp
2.506 + using sin_cos_minus_lemma [where x=x] by simp
2.507
2.508 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
2.509 -by (simp add: diff_minus sin_add)
2.510 + by (simp add: diff_minus sin_add)
2.511
2.512 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
2.513 -by (simp add: sin_diff mult_commute)
2.514 + by (simp add: sin_diff mult_commute)
2.515
2.516 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
2.517 -by (simp add: diff_minus cos_add)
2.518 + by (simp add: diff_minus cos_add)
2.519
2.520 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
2.521 -by (simp add: cos_diff mult_commute)
2.522 + by (simp add: cos_diff mult_commute)
2.523
2.524 lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
2.525 using sin_add [where x=x and y=x] by simp
2.526 @@ -1540,8 +1419,7 @@
2.527
2.528 subsection {* The Constant Pi *}
2.529
2.530 -definition
2.531 - pi :: "real" where
2.532 +definition pi :: "real" where
2.533 "pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
2.534
2.535 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
2.536 @@ -2429,7 +2307,7 @@
2.537 lemma DERIV_arcsin:
2.538 "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
2.539 apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
2.540 -apply (rule lemma_DERIV_subst [OF DERIV_sin])
2.541 +apply (rule DERIV_cong [OF DERIV_sin])
2.542 apply (simp add: cos_arcsin)
2.543 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
2.544 apply (rule power_strict_mono, simp, simp, simp)
2.545 @@ -2442,7 +2320,7 @@
2.546 lemma DERIV_arccos:
2.547 "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<twosuperior>))"
2.548 apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
2.549 -apply (rule lemma_DERIV_subst [OF DERIV_cos])
2.550 +apply (rule DERIV_cong [OF DERIV_cos])
2.551 apply (simp add: sin_arccos)
2.552 apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
2.553 apply (rule power_strict_mono, simp, simp, simp)
2.554 @@ -2454,7 +2332,7 @@
2.555
2.556 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<twosuperior>)"
2.557 apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
2.558 -apply (rule lemma_DERIV_subst [OF DERIV_tan])
2.559 +apply (rule DERIV_cong [OF DERIV_tan])
2.560 apply (rule cos_arctan_not_zero)
2.561 apply (simp add: power_inverse tan_sec [symmetric])
2.562 apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp)
2.563 @@ -2543,8 +2421,8 @@
2.564 lemma tan_60: "tan (pi / 3) = sqrt 3"
2.565 unfolding tan_def by (simp add: sin_60 cos_60)
2.566
2.567 -lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
2.568 - by (auto intro!: DERIV_intros)
2.569 +lemma DERIV_sin_add: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
2.570 + by (auto intro!: DERIV_intros) (* TODO: delete *)
2.571
2.572 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
2.573 proof -