src/HOL/Transcendental.thy
 changeset 44317 b7e9fa025f15 parent 44316 84b6f7a6cea4 child 44318 425c1f8f9487
equal inserted replaced
44316:84b6f7a6cea4 44317:b7e9fa025f15
1164   apply (rule isCont_inverse_function [where f=exp], simp_all)
1164   apply (rule isCont_inverse_function [where f=exp], simp_all)
1165   done
1165   done
1166
1166
1167 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
1167 lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
1168   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
1168   apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
1169   apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
1169   apply (erule DERIV_cong [OF DERIV_exp exp_ln])
1170   apply (simp_all add: abs_if isCont_ln)
1170   apply (simp_all add: abs_if isCont_ln)
1171   done
1171   done
1172
1172
1173 lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
1173 lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
1174   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
1174   by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
1306 lemma sin_zero [simp]: "sin 0 = 0"
1306 lemma sin_zero [simp]: "sin 0 = 0"
1307   unfolding sin_def sin_coeff_def by (simp add: powser_zero)
1307   unfolding sin_def sin_coeff_def by (simp add: powser_zero)
1308
1308
1309 lemma cos_zero [simp]: "cos 0 = 1"
1309 lemma cos_zero [simp]: "cos 0 = 1"
1310   unfolding cos_def cos_coeff_def by (simp add: powser_zero)
1310   unfolding cos_def cos_coeff_def by (simp add: powser_zero)
1314
1311
1315 lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
1312 lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
1316 proof -
1313 proof -
1317   have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
1314   have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
1318     by (auto intro!: DERIV_intros)
1315     by (auto intro!: DERIV_intros)