remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
authorhuffman
Fri Aug 19 18:06:27 2011 -0700 (2011-08-19)
changeset 44317b7e9fa025f15
parent 44316 84b6f7a6cea4
child 44318 425c1f8f9487
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
src/HOL/Deriv.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Deriv.thy	Fri Aug 19 17:59:19 2011 -0700
     1.2 +++ b/src/HOL/Deriv.thy	Fri Aug 19 18:06:27 2011 -0700
     1.3 @@ -304,9 +304,6 @@
     1.4         ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
     1.5  by (drule (2) DERIV_divide) (simp add: mult_commute)
     1.6  
     1.7 -lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
     1.8 -by auto
     1.9 -
    1.10  text {* @{text "DERIV_intros"} *}
    1.11  ML {*
    1.12  structure Deriv_Intros = Named_Thms
     2.1 --- a/src/HOL/Library/Poly_Deriv.thy	Fri Aug 19 17:59:19 2011 -0700
     2.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Fri Aug 19 18:06:27 2011 -0700
     2.3 @@ -78,11 +78,11 @@
     2.4  by (simp add: DERIV_cmult mult_commute [of _ c])
     2.5  
     2.6  lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
     2.7 -by (rule lemma_DERIV_subst, rule DERIV_pow, simp)
     2.8 +by (rule DERIV_cong, rule DERIV_pow, simp)
     2.9  declare DERIV_pow2 [simp] DERIV_pow [simp]
    2.10  
    2.11  lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: 'a::real_normed_field) x :> D"
    2.12 -by (rule lemma_DERIV_subst, rule DERIV_add, auto)
    2.13 +by (rule DERIV_cong, rule DERIV_add, auto)
    2.14  
    2.15  lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
    2.16    by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
     3.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 17:59:19 2011 -0700
     3.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 18:06:27 2011 -0700
     3.3 @@ -1166,7 +1166,7 @@
     3.4  
     3.5  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
     3.6    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
     3.7 -  apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
     3.8 +  apply (erule DERIV_cong [OF DERIV_exp exp_ln])
     3.9    apply (simp_all add: abs_if isCont_ln)
    3.10    done
    3.11  
    3.12 @@ -1309,9 +1309,6 @@
    3.13  lemma cos_zero [simp]: "cos 0 = 1"
    3.14    unfolding cos_def cos_coeff_def by (simp add: powser_zero)
    3.15  
    3.16 -lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
    3.17 -  by (rule DERIV_cong) (* TODO: delete *)
    3.18 -
    3.19  lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
    3.20  proof -
    3.21    have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"