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
```