src/HOL/Transcendental.thy
changeset 44317 b7e9fa025f15
parent 44316 84b6f7a6cea4
child 44318 425c1f8f9487
equal deleted 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)
  1311 
       
  1312 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
       
  1313   by (rule DERIV_cong) (* TODO: delete *)
       
  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)