Transcendental.thy: remove several unused lemmas and simplify some proofs
authorhuffman
Fri Aug 19 10:46:54 2011 -0700 (2011-08-19)
changeset 44308d2a6f9af02f4
parent 44307 6a383003d0a9
child 44309 d4decbd67703
child 44310 ba3d031b5dbb
Transcendental.thy: remove several unused lemmas and simplify some proofs
src/HOL/MacLaurin.thy
src/HOL/Transcendental.thy
     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 -