src/HOL/Deriv.thy
changeset 31899 1a7ade46061b
parent 31880 6fb86c61747c
child 31902 862ae16a799d
     1.1 --- a/src/HOL/Deriv.thy	Tue Jun 30 22:23:33 2009 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Thu Jul 02 15:37:22 2009 +0200
     1.3 @@ -264,21 +264,23 @@
     1.4      by (simp add: d dfx real_scaleR_def)
     1.5  qed
     1.6  
     1.7 -(* let's do the standard proof though theorem *)
     1.8 -(* LIM_mult2 follows from a NS proof          *)
     1.9 +text {*
    1.10 + Let's do the standard proof, though theorem
    1.11 + @{text "LIM_mult2"} follows from a NS proof
    1.12 +*}
    1.13  
    1.14  lemma DERIV_cmult:
    1.15        "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
    1.16  by (drule DERIV_mult' [OF DERIV_const], simp)
    1.17  
    1.18 -(* standard version *)
    1.19 +text {* Standard version *}
    1.20  lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
    1.21  by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute)
    1.22  
    1.23  lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
    1.24  by (auto dest: DERIV_chain simp add: o_def)
    1.25  
    1.26 -(*derivative of linear multiplication*)
    1.27 +text {* Derivative of linear multiplication *}
    1.28  lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
    1.29  by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
    1.30  
    1.31 @@ -287,21 +289,21 @@
    1.32  apply (simp add: real_scaleR_def real_of_nat_def)
    1.33  done
    1.34  
    1.35 -text{*Power of -1*}
    1.36 +text {* Power of @{text "-1"} *}
    1.37  
    1.38  lemma DERIV_inverse:
    1.39    fixes x :: "'a::{real_normed_field}"
    1.40    shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
    1.41  by (drule DERIV_inverse' [OF DERIV_ident]) simp
    1.42  
    1.43 -text{*Derivative of inverse*}
    1.44 +text {* Derivative of inverse *}
    1.45  lemma DERIV_inverse_fun:
    1.46    fixes x :: "'a::{real_normed_field}"
    1.47    shows "[| DERIV f x :> d; f(x) \<noteq> 0 |]
    1.48        ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
    1.49  by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib)
    1.50  
    1.51 -text{*Derivative of quotient*}
    1.52 +text {* Derivative of quotient *}
    1.53  lemma DERIV_quotient:
    1.54    fixes x :: "'a::{real_normed_field}"
    1.55    shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
    1.56 @@ -311,13 +313,15 @@
    1.57  lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
    1.58  by auto
    1.59  
    1.60 -text {* DERIV_intros *}
    1.61 +text {* @{text "DERIV_intros"} *}
    1.62 +ML {*
    1.63 +structure DerivIntros = NamedThmsFun
    1.64 +(
    1.65 +  val name = "DERIV_intros"
    1.66 +  val description = "DERIV introduction rules"
    1.67 +)
    1.68 +*}
    1.69  
    1.70 -ML{*
    1.71 -structure DerivIntros =
    1.72 -  NamedThmsFun(val name = "DERIV_intros"
    1.73 -               val description = "DERIV introduction rules");
    1.74 -*}
    1.75  setup DerivIntros.setup
    1.76  
    1.77  lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
    1.78 @@ -336,6 +340,7 @@
    1.79                unfolded real_of_nat_def[symmetric], DERIV_intros]
    1.80    DERIV_setsum[THEN DERIV_cong, DERIV_intros]
    1.81  
    1.82 +
    1.83  subsection {* Differentiability predicate *}
    1.84  
    1.85  definition