# HG changeset patch # User hoelzl # Date 1396540568 -7200 # Node ID 0556204bc230587a5f626a46cd3e5a87a4131402 # Parent 9bb2856cc8451400a97afb988865063b2c27b70a merged DERIV_intros, has_derivative_intros into derivative_intros diff -r 9bb2856cc845 -r 0556204bc230 NEWS --- a/NEWS Thu Apr 03 17:16:02 2014 +0200 +++ b/NEWS Thu Apr 03 17:56:08 2014 +0200 @@ -534,6 +534,13 @@ - Renamed FDERIV_... lemmas to has_derivative_... + - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV + + - removed DERIV_intros, has_derivative_eq_intros + + - introduced derivative_intros and deriative_eq_intros which includes now rules for + DERIV, has_derivative and has_vector_derivative. + - Other renamings: differentiable_def ~> real_differentiable_def differentiableE ~> real_differentiableE @@ -541,6 +548,7 @@ field_fderiv_def ~> field_has_derivative_at isDiff_der ~> differentiable_def deriv_fderiv ~> has_field_derivative_def + deriv_def ~> DERIV_def INCOMPATIBILITY. * Include more theorems in continuous_intros. Remove the continuous_on_intros, diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Complex.thy Thu Apr 03 17:56:08 2014 +0200 @@ -374,30 +374,20 @@ lemma bounded_linear_Im: "bounded_linear Im" by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) -lemmas tendsto_Re [tendsto_intros] = - bounded_linear.tendsto [OF bounded_linear_Re] - -lemmas tendsto_Im [tendsto_intros] = - bounded_linear.tendsto [OF bounded_linear_Im] - -lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re] -lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im] lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re] lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im] - -lemma continuous_Re: "continuous_on X Re" - by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re - continuous_on_cong continuous_on_id) - -lemma continuous_Im: "continuous_on X Im" - by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im - continuous_on_cong continuous_on_id) - -lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F" - by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const) - -lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F" - by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const) +lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re] +lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im] +lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re] +lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im] +lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re] +lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im] +lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re] +lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im] +lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re] +lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im] +lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re] +lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im] lemma tendsto_Complex [tendsto_intros]: assumes "(f ---> a) F" and "(g ---> b) F" @@ -445,8 +435,7 @@ qed declare - DERIV_power[where 'a=complex, THEN DERIV_cong, - unfolded of_nat_def[symmetric], DERIV_intros] + DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros] subsection {* The Complex Number $i$ *} @@ -605,11 +594,11 @@ using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1], simp) -lemmas tendsto_cnj [tendsto_intros] = - bounded_linear.tendsto [OF bounded_linear_cnj] - -lemmas isCont_cnj [simp] = - bounded_linear.isCont [OF bounded_linear_cnj] +lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj] +lemmas isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj] +lemmas continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj] +lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj] +lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj] lemma lim_cnj: "((\x. cnj(f x)) ---> cnj l) F \ (f ---> l) F" by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric]) @@ -704,12 +693,6 @@ lemma sums_complex_iff: "f sums x \ ((\x. Re (f x)) sums Re x) \ ((\x. Im (f x)) sums Im x)" unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum .. -lemma sums_Re: "f sums a \ (\x. Re (f x)) sums Re a" - unfolding sums_complex_iff by blast - -lemma sums_Im: "f sums a \ (\x. Im (f x)) sums Im a" - unfolding sums_complex_iff by blast - lemma summable_complex_iff: "summable f \ summable (\x. Re (f x)) \ summable (\x. Im (f x))" unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps) @@ -976,5 +959,4 @@ lemmas complex_Re_Im_cancel_iff = complex_eq_iff lemmas complex_equality = complex_eqI - end diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 03 17:56:08 2014 +0200 @@ -2674,24 +2674,24 @@ proof (induct f arbitrary: x) case (Inverse a) thus ?case - by (auto intro!: DERIV_intros simp add: algebra_simps power2_eq_square) + by (auto intro!: derivative_eq_intros simp add: algebra_simps power2_eq_square) next case (Cos a) thus ?case - by (auto intro!: DERIV_intros + by (auto intro!: derivative_intros simp del: interpret_floatarith.simps(5) simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a]) next case (Power a n) thus ?case - by (cases n) (auto intro!: DERIV_intros simp del: power_Suc) + by (cases n) (auto intro!: derivative_intros simp del: power_Suc) next case (Ln a) - thus ?case by (auto intro!: DERIV_intros simp add: divide_inverse) + thus ?case by (auto intro!: derivative_intros simp add: divide_inverse) next case (Var i) thus ?case using `n < length vs` by auto -qed (auto intro!: DERIV_intros) +qed (auto intro!: derivative_eq_intros) declare approx.simps[simp del] diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Deriv.thy Thu Apr 03 17:56:08 2014 +0200 @@ -29,6 +29,48 @@ most cases @{term s} is either a variable or @{term UNIV}. *} +lemma has_derivative_eq_rhs: "(f has_derivative f') F \ f' = g' \ (f has_derivative g') F" + by simp + +definition + has_field_derivative :: "('a::real_normed_field \ 'a) \ 'a \ 'a filter \ bool" + (infix "(has'_field'_derivative)" 50) +where + "(f has_field_derivative D) F \ (f has_derivative op * D) F" + +lemma DERIV_cong: "(f has_field_derivative X) F \ X = Y \ (f has_field_derivative Y) F" + by simp + +definition + has_vector_derivative :: "(real \ 'b::real_normed_vector) \ 'b \ real filter \ bool" + (infix "has'_vector'_derivative" 50) +where + "(f has_vector_derivative f') net \ (f has_derivative (\x. x *\<^sub>R f')) net" + +lemma has_vector_derivative_eq_rhs: "(f has_vector_derivative X) F \ X = Y \ (f has_vector_derivative Y) F" + by simp + +ML {* + +structure Derivative_Intros = Named_Thms +( + val name = @{binding derivative_intros} + val description = "structural introduction rules for derivatives" +) + +*} + +setup {* + let + val eq_thms = [@{thm has_derivative_eq_rhs}, @{thm DERIV_cong}, @{thm has_vector_derivative_eq_rhs}] + fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms + in + Derivative_Intros.setup #> + Global_Theory.add_thms_dynamic + (@{binding derivative_eq_intros}, map_filter eq_rule o Derivative_Intros.get o Context.proof_of) + end; +*} + text {* The following syntax is only used as a legacy syntax. *} @@ -38,36 +80,16 @@ where "FDERIV f x :> f' \ (f has_derivative f') (at x)" - -lemma has_derivative_eq_rhs: "(f has_derivative f') F \ f' = g' \ (f has_derivative g') F" - by simp - -ML {* - -structure has_derivative_Intros = Named_Thms -( - val name = @{binding has_derivative_intros} - val description = "introduction rules for FDERIV" -) - -*} - -setup {* - has_derivative_Intros.setup #> - Global_Theory.add_thms_dynamic (@{binding has_derivative_eq_intros}, - map_filter (try (fn thm => @{thm has_derivative_eq_rhs} OF [thm])) o has_derivative_Intros.get o Context.proof_of); -*} - lemma has_derivative_bounded_linear: "(f has_derivative f') F \ bounded_linear f'" by (simp add: has_derivative_def) lemma has_derivative_linear: "(f has_derivative f') F \ linear f'" using bounded_linear.linear[OF has_derivative_bounded_linear] . -lemma has_derivative_ident[has_derivative_intros, simp]: "((\x. x) has_derivative (\x. x)) F" +lemma has_derivative_ident[derivative_intros, simp]: "((\x. x) has_derivative (\x. x)) F" by (simp add: has_derivative_def tendsto_const) -lemma has_derivative_const[has_derivative_intros, simp]: "((\x. c) has_derivative (\x. 0)) F" +lemma has_derivative_const[derivative_intros, simp]: "((\x. c) has_derivative (\x. 0)) F" by (simp add: has_derivative_def tendsto_const) lemma (in bounded_linear) bounded_linear: "bounded_linear f" .. @@ -81,19 +103,19 @@ apply (simp add: scaleR diff add zero) done -lemmas has_derivative_scaleR_right [has_derivative_intros] = +lemmas has_derivative_scaleR_right [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_scaleR_right] -lemmas has_derivative_scaleR_left [has_derivative_intros] = +lemmas has_derivative_scaleR_left [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_scaleR_left] -lemmas has_derivative_mult_right [has_derivative_intros] = +lemmas has_derivative_mult_right [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_mult_right] -lemmas has_derivative_mult_left [has_derivative_intros] = +lemmas has_derivative_mult_left [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_mult_left] -lemma has_derivative_add[simp, has_derivative_intros]: +lemma has_derivative_add[simp, derivative_intros]: assumes f: "(f has_derivative f') F" and g: "(g has_derivative g') F" shows "((\x. f x + g x) has_derivative (\x. f' x + g' x)) F" unfolding has_derivative_def @@ -106,7 +128,7 @@ by (simp add: field_simps scaleR_add_right scaleR_diff_right) qed (blast intro: bounded_linear_add f g has_derivative_bounded_linear) -lemma has_derivative_setsum[simp, has_derivative_intros]: +lemma has_derivative_setsum[simp, derivative_intros]: assumes f: "\i. i \ I \ (f i has_derivative f' i) F" shows "((\x. \i\I. f i x) has_derivative (\x. \i\I. f' i x)) F" proof cases @@ -114,10 +136,10 @@ by induct (simp_all add: f) qed simp -lemma has_derivative_minus[simp, has_derivative_intros]: "(f has_derivative f') F \ ((\x. - f x) has_derivative (\x. - f' x)) F" +lemma has_derivative_minus[simp, derivative_intros]: "(f has_derivative f') F \ ((\x. - f x) has_derivative (\x. - f' x)) F" using has_derivative_scaleR_right[of f f' F "-1"] by simp -lemma has_derivative_diff[simp, has_derivative_intros]: +lemma has_derivative_diff[simp, derivative_intros]: "(f has_derivative f') F \ (g has_derivative g') F \ ((\x. f x - g x) has_derivative (\x. f' x - g' x)) F" by (simp only: diff_conv_add_uminus has_derivative_add has_derivative_minus) @@ -320,10 +342,10 @@ qed simp qed -lemmas has_derivative_mult[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult] -lemmas has_derivative_scaleR[simp, has_derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR] +lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult] +lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR] -lemma has_derivative_setprod[simp, has_derivative_intros]: +lemma has_derivative_setprod[simp, derivative_intros]: fixes f :: "'i \ 'a :: real_normed_vector \ 'b :: real_normed_field" assumes f: "\i. i \ I \ (f i has_derivative f' i) (at x within s)" shows "((\x. \i\I. f i x) has_derivative (\y. \i\I. f' i y * (\j\I - {i}. f j x))) (at x within s)" @@ -341,7 +363,7 @@ qed simp qed simp -lemma has_derivative_power[simp, has_derivative_intros]: +lemma has_derivative_power[simp, derivative_intros]: fixes f :: "'a :: real_normed_vector \ 'b :: real_normed_field" assumes f: "(f has_derivative f') (at x within s)" shows "((\x. f x^n) has_derivative (\y. of_nat n * f' y * f x^(n - 1))) (at x within s)" @@ -392,13 +414,13 @@ norm (?inv y - ?inv x) * norm (?inv x)" . qed -lemma has_derivative_inverse[simp, has_derivative_intros]: +lemma has_derivative_inverse[simp, derivative_intros]: fixes f :: "_ \ 'a::real_normed_div_algebra" assumes x: "f x \ 0" and f: "(f has_derivative f') (at x within s)" shows "((\x. inverse (f x)) has_derivative (\h. - (inverse (f x) * f' h * inverse (f x)))) (at x within s)" using has_derivative_compose[OF f has_derivative_inverse', OF x] . -lemma has_derivative_divide[simp, has_derivative_intros]: +lemma has_derivative_divide[simp, derivative_intros]: fixes f :: "_ \ 'a::real_normed_div_algebra" assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" assumes x: "g x \ 0" @@ -409,7 +431,7 @@ text{*Conventional form requires mult-AC laws. Types real and complex only.*} -lemma has_derivative_divide'[has_derivative_intros]: +lemma has_derivative_divide'[derivative_intros]: fixes f :: "_ \ 'a::real_normed_field" assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" and x: "g x \ 0" shows "((\x. f x / g x) has_derivative (\h. (f' h * g x - f x * g' h) / (g x * g x))) (at x within s)" @@ -485,10 +507,10 @@ lemmas differentiable_within_subset = differentiable_subset -lemma differentiable_ident [simp]: "(\x. x) differentiable F" +lemma differentiable_ident [simp, derivative_intros]: "(\x. x) differentiable F" unfolding differentiable_def by (blast intro: has_derivative_ident) -lemma differentiable_const [simp]: "(\z. a) differentiable F" +lemma differentiable_const [simp, derivative_intros]: "(\z. a) differentiable F" unfolding differentiable_def by (blast intro: has_derivative_const) lemma differentiable_in_compose: @@ -499,48 +521,42 @@ "f differentiable (at (g x)) \ g differentiable (at x within s) \ (\x. f (g x)) differentiable (at x within s)" by (blast intro: differentiable_in_compose differentiable_subset) -lemma differentiable_sum [simp]: +lemma differentiable_sum [simp, derivative_intros]: "f differentiable F \ g differentiable F \ (\x. f x + g x) differentiable F" unfolding differentiable_def by (blast intro: has_derivative_add) -lemma differentiable_minus [simp]: +lemma differentiable_minus [simp, derivative_intros]: "f differentiable F \ (\x. - f x) differentiable F" unfolding differentiable_def by (blast intro: has_derivative_minus) -lemma differentiable_diff [simp]: +lemma differentiable_diff [simp, derivative_intros]: "f differentiable F \ g differentiable F \ (\x. f x - g x) differentiable F" unfolding differentiable_def by (blast intro: has_derivative_diff) -lemma differentiable_mult [simp]: +lemma differentiable_mult [simp, derivative_intros]: fixes f g :: "'a :: real_normed_vector \ 'b :: real_normed_algebra" shows "f differentiable (at x within s) \ g differentiable (at x within s) \ (\x. f x * g x) differentiable (at x within s)" unfolding differentiable_def by (blast intro: has_derivative_mult) -lemma differentiable_inverse [simp]: +lemma differentiable_inverse [simp, derivative_intros]: fixes f :: "'a :: real_normed_vector \ 'b :: real_normed_field" shows "f differentiable (at x within s) \ f x \ 0 \ (\x. inverse (f x)) differentiable (at x within s)" unfolding differentiable_def by (blast intro: has_derivative_inverse) -lemma differentiable_divide [simp]: +lemma differentiable_divide [simp, derivative_intros]: fixes f g :: "'a :: real_normed_vector \ 'b :: real_normed_field" shows "f differentiable (at x within s) \ g differentiable (at x within s) \ g x \ 0 \ (\x. f x / g x) differentiable (at x within s)" unfolding divide_inverse using assms by simp -lemma differentiable_power [simp]: +lemma differentiable_power [simp, derivative_intros]: fixes f g :: "'a :: real_normed_vector \ 'b :: real_normed_field" shows "f differentiable (at x within s) \ (\x. f x ^ n) differentiable (at x within s)" unfolding differentiable_def by (blast intro: has_derivative_power) -lemma differentiable_scaleR [simp]: +lemma differentiable_scaleR [simp, derivative_intros]: "f differentiable (at x within s) \ g differentiable (at x within s) \ (\x. f x *\<^sub>R g x) differentiable (at x within s)" unfolding differentiable_def by (blast intro: has_derivative_scaleR) -definition - has_field_derivative :: "('a::real_normed_field \ 'a) \ 'a \ 'a filter \ bool" - (infix "(has'_field'_derivative)" 50) -where - "(f has_field_derivative D) F \ (f has_derivative op * D) F" - lemma has_derivative_imp_has_field_derivative: "(f has_derivative D) F \ (\x. x * D' = D x) \ (f has_field_derivative D') F" unfolding has_field_derivative_def @@ -555,7 +571,7 @@ by (simp add: has_field_derivative_def has_derivative_within_subset) abbreviation (input) - deriv :: "('a::real_normed_field \ 'a) \ 'a \ 'a \ bool" + DERIV :: "('a::real_normed_field \ 'a) \ 'a \ 'a \ bool" ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where "DERIV f x :> D \ (f has_field_derivative D) (at x)" @@ -588,8 +604,7 @@ lemma differentiableI: "(f has_real_derivative D) (at x within s) \ f differentiable (at x within s)" by (force simp add: real_differentiable_def) -lemma deriv_def: - "DERIV f x :> D \ (\h. (f (x + h) - f x) / h) -- 0 --> D" +lemma DERIV_def: "DERIV f x :> D \ (\h. (f (x + h) - f x) / h) -- 0 --> D" apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D]) apply (subst (2) tendsto_norm_zero_iff[symmetric]) apply (rule filterlim_cong) @@ -602,40 +617,36 @@ subsection {* Derivatives *} lemma DERIV_D: "DERIV f x :> D \ (\h. (f (x + h) - f x) / h) -- 0 --> D" - by (simp add: deriv_def) + by (simp add: DERIV_def) -lemma DERIV_const [simp]: "((\x. k) has_field_derivative 0) (at x within s)" +lemma DERIV_const [simp, derivative_intros]: "((\x. k) has_field_derivative 0) F" by (rule has_derivative_imp_has_field_derivative[OF has_derivative_const]) auto -lemma DERIV_ident [simp]: "((\x. x) has_field_derivative 1) (at x within s)" +lemma DERIV_ident [simp, derivative_intros]: "((\x. x) has_field_derivative 1) F" by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto -lemma field_differentiable_add: - assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F" - shows "((\z. f z + g z) has_field_derivative f' + g') F" - apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_add]) - using assms - by (auto simp: has_field_derivative_def field_simps mult_commute_abs) +lemma field_differentiable_add[derivative_intros]: + "(f has_field_derivative f') F \ (g has_field_derivative g') F \ + ((\z. f z + g z) has_field_derivative f' + g') F" + by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add]) + (auto simp: has_field_derivative_def field_simps mult_commute_abs) corollary DERIV_add: "(f has_field_derivative D) (at x within s) \ (g has_field_derivative E) (at x within s) \ ((\x. f x + g x) has_field_derivative D + E) (at x within s)" by (rule field_differentiable_add) -lemma field_differentiable_minus: - assumes "(f has_field_derivative f') F" - shows "((\z. - (f z)) has_field_derivative -f') F" - apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus]) - using assms - by (auto simp: has_field_derivative_def field_simps mult_commute_abs) +lemma field_differentiable_minus[derivative_intros]: + "(f has_field_derivative f') F \ ((\z. - (f z)) has_field_derivative -f') F" + by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus]) + (auto simp: has_field_derivative_def field_simps mult_commute_abs) corollary DERIV_minus: "(f has_field_derivative D) (at x within s) \ ((\x. - f x) has_field_derivative -D) (at x within s)" by (rule field_differentiable_minus) -lemma field_differentiable_diff: - assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F" - shows "((\z. f z - g z) has_field_derivative f' - g') F" -by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus) +lemma field_differentiable_diff[derivative_intros]: + "(f has_field_derivative f') F \ (g has_field_derivative g') F \ ((\z. f z - g z) has_field_derivative f' - g') F" + by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus) corollary DERIV_diff: "(f has_field_derivative D) (at x within s) \ (g has_field_derivative E) (at x within s) \ @@ -658,7 +669,7 @@ by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult]) (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative) -lemma DERIV_mult: +lemma DERIV_mult[derivative_intros]: "(f has_field_derivative Da) (at x within s) \ (g has_field_derivative Db) (at x within s) \ ((\x. f x * g x) has_field_derivative Da * g x + Db * f x) (at x within s)" by (rule has_derivative_imp_has_field_derivative[OF has_derivative_mult]) @@ -672,7 +683,7 @@ lemma DERIV_cmult_right: "(f has_field_derivative D) (at x within s) ==> ((\x. f x * c) has_field_derivative D * c) (at x within s)" - using DERIV_cmult by (force simp add: mult_ac) + using DERIV_cmult by (force simp add: mult_ac) lemma DERIV_cmult_Id [simp]: "(op * c has_field_derivative c) (at x within s)" by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp) @@ -683,15 +694,15 @@ lemma DERIV_unique: "DERIV f x :> D \ DERIV f x :> E \ D = E" - unfolding deriv_def by (rule LIM_unique) + unfolding DERIV_def by (rule LIM_unique) -lemma DERIV_setsum: +lemma DERIV_setsum[derivative_intros]: "(\ n. n \ S \ ((\x. f x n) has_field_derivative (f' x n)) F) \ ((\x. setsum (f x) S) has_field_derivative setsum (f' x) S) F" by (rule has_derivative_imp_has_field_derivative[OF has_derivative_setsum]) (auto simp: setsum_right_distrib mult_commute_abs dest: has_field_derivative_imp_has_derivative) -lemma DERIV_inverse': +lemma DERIV_inverse'[derivative_intros]: "(f has_field_derivative D) (at x within s) \ f x \ 0 \ ((\x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x))) (at x within s)" by (rule has_derivative_imp_has_field_derivative[OF has_derivative_inverse]) @@ -712,7 +723,7 @@ text {* Derivative of quotient *} -lemma DERIV_divide: +lemma DERIV_divide[derivative_intros]: "(f has_field_derivative D) (at x within s) \ (g has_field_derivative E) (at x within s) \ g x \ 0 \ ((\x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)" @@ -731,7 +742,7 @@ by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power]) (auto simp: has_field_derivative_def) -lemma DERIV_power: +lemma DERIV_power[derivative_intros]: "(f has_field_derivative D) (at x within s) \ ((\x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)" by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power]) @@ -778,34 +789,8 @@ shows "DERIV (\x. g(f x)) x :> f' * g'(f x)" by (metis UNIV_I DERIV_chain_s [of UNIV] assms) - -subsubsection {* @{text "DERIV_intros"} *} - -ML {* -structure Deriv_Intros = Named_Thms -( - val name = @{binding DERIV_intros} - val description = "DERIV introduction rules" -) -*} - -setup Deriv_Intros.setup - -lemma DERIV_cong: "(f has_field_derivative X) (at x within s) \ X = Y \ (f has_field_derivative Y) (at x within s)" - by simp - declare - DERIV_const[THEN DERIV_cong, DERIV_intros] - DERIV_ident[THEN DERIV_cong, DERIV_intros] - DERIV_add[THEN DERIV_cong, DERIV_intros] - DERIV_minus[THEN DERIV_cong, DERIV_intros] - DERIV_mult[THEN DERIV_cong, DERIV_intros] - DERIV_diff[THEN DERIV_cong, DERIV_intros] - DERIV_inverse'[THEN DERIV_cong, DERIV_intros] - DERIV_divide[THEN DERIV_cong, DERIV_intros] - DERIV_power[where 'a=real, THEN DERIV_cong, - unfolded real_of_nat_def[symmetric], DERIV_intros] - DERIV_setsum[THEN DERIV_cong, DERIV_intros] + DERIV_power[where 'a=real, unfolded real_of_nat_def[symmetric], derivative_intros] text{*Alternative definition for differentiability*} @@ -821,7 +806,7 @@ done lemma DERIV_iff2: "(DERIV f x :> D) \ (\z. (f z - f x) / (z - x)) --x --> D" - by (simp add: deriv_def DERIV_LIM_iff) + by (simp add: DERIV_def DERIV_LIM_iff) lemma DERIV_cong_ev: "x = y \ eventually (\x. f x = g x) (nhds x) \ u = v \ DERIV f x :> u \ DERIV g y :> v" @@ -836,11 +821,11 @@ lemma DERIV_shift: "(DERIV f (x + z) :> y) \ (DERIV (\x. f (x + z)) x :> y)" - by (simp add: deriv_def field_simps) + by (simp add: DERIV_def field_simps) lemma DERIV_mirror: "(DERIV f (- x) :> y) \ (DERIV (\x. f (- x::real) :: real) x :> - y)" - by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right + by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right tendsto_minus_cancel_left field_simps conj_commute) text {* Caratheodory formulation of derivative at a point *} @@ -855,7 +840,7 @@ let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))" show "\z. f z - f x = ?g z * (z-x)" by simp show "isCont ?g x" using der - by (simp add: isCont_iff deriv_def cong: LIM_equal [rule_format]) + by (simp add: isCont_iff DERIV_def cong: LIM_equal [rule_format]) show "?g x = l" by simp qed next @@ -863,7 +848,7 @@ then obtain g where "(\z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast thus "(DERIV f x :> l)" - by (auto simp add: isCont_iff deriv_def cong: LIM_cong) + by (auto simp add: isCont_iff DERIV_def cong: LIM_cong) qed text {* @@ -1477,7 +1462,7 @@ from cdef have "DERIV ?h c :> l" by auto moreover have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)" - using g'cdef f'cdef by (auto intro!: DERIV_intros) + using g'cdef f'cdef by (auto intro!: derivative_eq_intros) ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique) { diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Library/Inner_Product.thy Thu Apr 03 17:56:08 2014 +0200 @@ -180,7 +180,7 @@ lemmas isCont_inner [simp] = bounded_bilinear.isCont [OF bounded_bilinear_inner] -lemmas has_derivative_inner [has_derivative_intros] = +lemmas has_derivative_inner [derivative_intros] = bounded_bilinear.FDERIV [OF bounded_bilinear_inner] lemmas bounded_linear_inner_left = @@ -189,10 +189,10 @@ lemmas bounded_linear_inner_right = bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner] -lemmas has_derivative_inner_right [has_derivative_intros] = +lemmas has_derivative_inner_right [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_inner_right] -lemmas has_derivative_inner_left [has_derivative_intros] = +lemmas has_derivative_inner_left [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_inner_left] lemma differentiable_inner [simp]: diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Library/Poly_Deriv.thy --- a/src/HOL/Library/Poly_Deriv.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Library/Poly_Deriv.thy Thu Apr 03 17:56:08 2014 +0200 @@ -102,7 +102,7 @@ by (rule DERIV_cong, rule DERIV_add, auto) lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" - by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons) + by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons) text{* Consequences of the derivative theorem above*} diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Library/Product_Vector.thy Thu Apr 03 17:56:08 2014 +0200 @@ -478,7 +478,7 @@ subsubsection {* Frechet derivatives involving pairs *} -lemma has_derivative_Pair [has_derivative_intros]: +lemma has_derivative_Pair [derivative_intros]: assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" shows "((\x. (f x, g x)) has_derivative (\h. (f' h, g' h))) (at x within s)" proof (rule has_derivativeI_sandwich[of 1]) @@ -497,10 +497,10 @@ by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt]) qed simp -lemmas has_derivative_fst [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst] -lemmas has_derivative_snd [has_derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd] +lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst] +lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd] -lemma has_derivative_split [has_derivative_intros]: +lemma has_derivative_split [derivative_intros]: "((\p. f (fst p) (snd p)) has_derivative f') F \ ((\(a, b). f a b) has_derivative f') F" unfolding split_beta' . diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/MacLaurin.thy Thu Apr 03 17:56:08 2014 +0200 @@ -40,7 +40,8 @@ have "DERIV (difg m) t :> diff (Suc m) t - ((\xmt>0. t < - h \ @@ -217,7 +218,7 @@ (\mt\ \ \x\" and diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 03 17:56:08 2014 +0200 @@ -15,7 +15,7 @@ shows "((op * c) has_derivative (op * c)) F" by (rule has_derivative_mult_right [OF has_derivative_id]) -lemma has_derivative_of_real[has_derivative_intros, simp]: +lemma has_derivative_of_real[derivative_intros, simp]: "(f has_derivative f') F \ ((\x. of_real (f x)) has_derivative (\x. of_real (f' x))) F" using bounded_linear.has_derivative[OF bounded_linear_of_real] . @@ -200,14 +200,6 @@ shows "DERIV g a :> f'" by (blast intro: assms DERIV_transform_within) -subsection{*Further useful properties of complex conjugation*} - -lemma continuous_within_cnj: "continuous (at z within s) cnj" -by (metis bounded_linear_cnj linear_continuous_within) - -lemma continuous_on_cnj: "continuous_on s cnj" -by (metis bounded_linear_cnj linear_continuous_on) - subsection {*Some limit theorems about real part of real series etc.*} (*MOVE? But not to Finite_Cartesian_Product*) @@ -521,29 +513,29 @@ "\f complex_differentiable at z; g complex_differentiable at z\ \ deriv (\w. f w + g w) z = deriv f z + deriv g z" unfolding DERIV_deriv_iff_complex_differentiable[symmetric] - by (auto intro!: DERIV_imp_deriv DERIV_intros) + by (auto intro!: DERIV_imp_deriv derivative_intros) lemma complex_derivative_diff: "\f complex_differentiable at z; g complex_differentiable at z\ \ deriv (\w. f w - g w) z = deriv f z - deriv g z" unfolding DERIV_deriv_iff_complex_differentiable[symmetric] - by (auto intro!: DERIV_imp_deriv DERIV_intros) + by (auto intro!: DERIV_imp_deriv derivative_intros) lemma complex_derivative_mult: "\f complex_differentiable at z; g complex_differentiable at z\ \ deriv (\w. f w * g w) z = f z * deriv g z + deriv f z * g z" unfolding DERIV_deriv_iff_complex_differentiable[symmetric] - by (auto intro!: DERIV_imp_deriv DERIV_intros) + by (auto intro!: DERIV_imp_deriv derivative_eq_intros) lemma complex_derivative_cmult: "f complex_differentiable at z \ deriv (\w. c * f w) z = c * deriv f z" unfolding DERIV_deriv_iff_complex_differentiable[symmetric] - by (auto intro!: DERIV_imp_deriv DERIV_intros) + by (auto intro!: DERIV_imp_deriv derivative_eq_intros) lemma complex_derivative_cmult_right: "f complex_differentiable at z \ deriv (\w. f w * c) z = deriv f z * c" unfolding DERIV_deriv_iff_complex_differentiable[symmetric] - by (auto intro!: DERIV_imp_deriv DERIV_intros) + by (auto intro!: DERIV_imp_deriv derivative_eq_intros) lemma complex_derivative_transform_within_open: "\f holomorphic_on s; g holomorphic_on s; open s; z \ s; \w. w \ s \ f w = g w\ @@ -1037,7 +1029,7 @@ then have "((\v. (\i\n. f i v * (z - v)^i / of_nat (fact i))) has_field_derivative f (Suc n) u * (z-u) ^ n / of_nat (fact n)) (at u within s)" - apply (intro DERIV_intros DERIV_power[THEN DERIV_cong]) + apply (intro derivative_eq_intros) apply (blast intro: assms `u \ s`) apply (rule refl)+ apply (auto simp: field_simps) @@ -1083,7 +1075,7 @@ proof - have twz: "\t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)" by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) - note assms[unfolded has_field_derivative_def, has_derivative_intros] + note assms[unfolded has_field_derivative_def, derivative_intros] show ?thesis apply (cut_tac mvt_simple [of 0 1 "Re o f o (\t. (1 - t) *\<^sub>R w + t *\<^sub>R z)" @@ -1091,7 +1083,7 @@ apply auto apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI) apply (auto simp add: open_segment_def twz) [] - apply (intro has_derivative_eq_intros has_derivative_at_within) + apply (intro derivative_eq_intros has_derivative_at_within) apply simp_all apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib) apply (force simp add: twz closed_segment_def) @@ -1136,7 +1128,7 @@ f (Suc n) u * (z - u) ^ n / of_nat (fact n)" . then have "((\u. \i = 0..n. f i u * (z - u) ^ i / of_nat (fact i)) has_field_derivative f (Suc n) u * (z - u) ^ n / of_nat (fact n)) (at u)" - apply (intro DERIV_intros)+ + apply (intro derivative_eq_intros)+ apply (force intro: u assms) apply (rule refl)+ apply (auto simp: mult_ac) diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Apr 03 17:56:08 2014 +0200 @@ -45,7 +45,7 @@ lemma has_derivative_add_const: "(f has_derivative f') net \ ((\x. f x + c) has_derivative f') net" - by (intro has_derivative_eq_intros) auto + by (intro derivative_eq_intros) auto subsection {* Derivative with composed bilinear function. *} @@ -319,14 +319,14 @@ subsection {* The chain rule *} -lemma diff_chain_within[has_derivative_intros]: +lemma diff_chain_within[derivative_intros]: assumes "(f has_derivative f') (at x within s)" and "(g has_derivative g') (at (f x) within (f ` s))" shows "((g \ f) has_derivative (g' \ f'))(at x within s)" using has_derivative_in_compose[OF assms] by (simp add: comp_def) -lemma diff_chain_at[has_derivative_intros]: +lemma diff_chain_at[derivative_intros]: "(f has_derivative f') (at x) \ (g has_derivative g') (at (f x)) \ ((g \ f) has_derivative (g' \ f')) (at x)" using has_derivative_compose[of f f' x UNIV g g'] @@ -544,7 +544,7 @@ from min obtain d where d1: "0 < d" and d2: "\y\ball x d. f x \ f y" unfolding eventually_at by (force simp: dist_commute) have "FDERIV (\r. x + r *\<^sub>R h) 0 :> (\r. r *\<^sub>R h)" - by (intro has_derivative_eq_intros, auto) + by (intro derivative_eq_intros) auto then have "FDERIV (\r. f (x + r *\<^sub>R h)) 0 :> (\k. f' (k *\<^sub>R h))" by (rule has_derivative_compose, simp add: deriv) then have "DERIV (\r. f (x + r *\<^sub>R h)) 0 :> f' h" @@ -677,7 +677,7 @@ assume x: "x \ {a <..< b}" show "((\x. f x - (f b - f a) / (b - a) * x) has_derivative (\xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)" - by (intro has_derivative_intros assms(3)[rule_format,OF x] mult_right_has_derivative) + by (intro derivative_intros assms(3)[rule_format,OF x]) qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps) then obtain x where "x \ {a <..< b}" @@ -815,7 +815,7 @@ let ?u = "x + u *\<^sub>R (y - x)" have "(f \ ?p has_derivative (f' ?u) \ (\u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)" apply (rule diff_chain_within) - apply (rule has_derivative_intros)+ + apply (rule derivative_intros)+ apply (rule has_derivative_within_subset) apply (rule assms(2)[rule_format]) using goal1 * @@ -1538,12 +1538,12 @@ unfolding ph' * apply (simp add: comp_def) apply (rule bounded_linear.has_derivative[OF assms(3)]) - apply (rule has_derivative_intros) + apply (rule derivative_intros) defer apply (rule has_derivative_sub[where g'="\x.0",unfolded diff_0_right]) apply (rule has_derivative_at_within) using assms(5) and `u \ s` `a \ s` - apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\x. x"] has_derivative_bounded_linear) + apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\x. x"] has_derivative_bounded_linear) done have **: "bounded_linear (\x. f' u x - f' a x)" "bounded_linear (\x. f' a x - f' u x)" apply (rule_tac[!] bounded_linear_sub) @@ -1600,7 +1600,7 @@ fix x assume "x \ s" show "((\a. f m a - f n a) has_derivative (\h. f' m x h - f' n x h)) (at x within s)" - by (rule has_derivative_intros assms(2)[rule_format] `x\s`)+ + by (rule derivative_intros assms(2)[rule_format] `x\s`)+ show "onorm (\h. f' m x h - f' n x h) \ 2 * e" proof (rule onorm_bound) fix h @@ -1933,44 +1933,58 @@ apply auto done - text {* Considering derivative @{typ "real \ 'b\real_normed_vector"} as a vector. *} -definition has_vector_derivative :: "(real \ 'b::real_normed_vector) \ 'b \ real filter \ bool" - (infix "has'_vector'_derivative" 50) - where "(f has_vector_derivative f') net \ (f has_derivative (\x. x *\<^sub>R f')) net" - -definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" - -lemma vector_derivative_works: - fixes f :: "real \ 'a::real_normed_vector" - shows "f differentiable net \ (f has_vector_derivative (vector_derivative f net)) net" - (is "?l = ?r") -proof - assume ?l - obtain f' where f': "(f has_derivative f') net" - using `?l` unfolding differentiable_def .. - then interpret bounded_linear f' - by auto - show ?r - unfolding vector_derivative_def has_vector_derivative_def - apply - - apply (rule someI_ex,rule_tac x="f' 1" in exI) - using f' - unfolding scaleR[symmetric] - apply auto - done -next - assume ?r - then show ?l - unfolding vector_derivative_def has_vector_derivative_def differentiable_def - by auto -qed - lemma has_field_derivative_iff_has_vector_derivative: "(f has_field_derivative y) F \ (f has_vector_derivative y) F" unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs .. +lemma has_vector_derivative_const[simp, derivative_intros]: "((\x. c) has_vector_derivative 0) net" + by (auto simp: has_vector_derivative_def) + +lemma has_vector_derivative_id[simp, derivative_intros]: "((\x. x) has_vector_derivative 1) net" + by (auto simp: has_vector_derivative_def) + +lemma has_vector_derivative_neg[derivative_intros]: + "(f has_vector_derivative f') net \ ((\x. - f x) has_vector_derivative (- f')) net" + by (auto simp: has_vector_derivative_def) + +lemma has_vector_derivative_add[derivative_intros]: + "(f has_vector_derivative f') net \ (g has_vector_derivative g') net \ + ((\x. f x + g x) has_vector_derivative (f' + g')) net" + by (auto simp: has_vector_derivative_def scaleR_right_distrib) + +lemma has_vector_derivative_sub[derivative_intros]: + "(f has_vector_derivative f') net \ (g has_vector_derivative g') net \ + ((\x. f x - g x) has_vector_derivative (f' - g')) net" + by (auto simp: has_vector_derivative_def scaleR_diff_right) + +lemma (in bounded_linear) has_vector_derivative: + assumes "(g has_vector_derivative g') (at x within s)" + shows "((\x. f (g x)) has_vector_derivative f g') (at x within s)" + using has_derivative[OF assms[unfolded has_vector_derivative_def]] + by (simp add: has_vector_derivative_def scaleR) + +lemma (in bounded_bilinear) has_vector_derivative: + assumes "(f has_vector_derivative f') (at x within s)" + and "(g has_vector_derivative g') (at x within s)" + shows "((\x. f x ** g x) has_vector_derivative (f x ** g' + f' ** g x)) (at x within s)" + using FDERIV[OF assms(1-2)[unfolded has_vector_derivative_def]] + by (simp add: has_vector_derivative_def scaleR_right scaleR_left scaleR_right_distrib) + +lemma has_vector_derivative_scaleR[derivative_intros]: + "(f has_field_derivative f') (at x within s) \ (g has_vector_derivative g') (at x within s) \ + ((\x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)" + unfolding has_field_derivative_iff_has_vector_derivative + by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR]) + +lemma has_vector_derivative_mult[derivative_intros]: + "(f has_vector_derivative f') (at x within s) \ (g has_vector_derivative g') (at x within s) \ + ((\x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)" + by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult]) + +definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" + lemma vector_derivative_unique_at: assumes "(f has_vector_derivative f') (at x)" and "(f has_vector_derivative f'') (at x)" @@ -1983,6 +1997,20 @@ unfolding fun_eq_iff by auto qed +lemma vector_derivative_works: + "f differentiable net \ (f has_vector_derivative (vector_derivative f net)) net" + (is "?l = ?r") +proof + assume ?l + obtain f' where f': "(f has_derivative f') net" + using `?l` unfolding differentiable_def .. + then interpret bounded_linear f' + by auto + show ?r + unfolding vector_derivative_def has_vector_derivative_def + by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f') +qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def) + lemma vector_derivative_unique_within_closed_interval: assumes "a < b" and "x \ cbox a b" @@ -2028,87 +2056,8 @@ done lemma has_vector_derivative_within_subset: - "(f has_vector_derivative f') (at x within s) \ t \ s \ - (f has_vector_derivative f') (at x within t)" - unfolding has_vector_derivative_def - apply (rule has_derivative_within_subset) - apply auto - done - -lemma has_vector_derivative_const: "((\x. c) has_vector_derivative 0) net" - unfolding has_vector_derivative_def - using has_derivative_const - by auto - -lemma has_vector_derivative_id: "((\x::real. x) has_vector_derivative 1) net" - unfolding has_vector_derivative_def - using has_derivative_id - by auto - -lemma has_vector_derivative_cmul: - "(f has_vector_derivative f') net \ - ((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net" - unfolding has_vector_derivative_def - apply (drule scaleR_right_has_derivative) - apply (auto simp add: algebra_simps) - done - -lemma has_vector_derivative_cmul_eq: - assumes "c \ 0" - shows "(((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \ (f has_vector_derivative f') net)" - apply (rule iffI) - apply (drule has_vector_derivative_cmul[where c="1/c"]) - apply (rule_tac [2] has_vector_derivative_cmul) - using assms - apply auto - done - -lemma has_vector_derivative_neg: - "(f has_vector_derivative f') net \ ((\x. - f x) has_vector_derivative (- f')) net" - unfolding has_vector_derivative_def - apply (drule has_derivative_neg) - apply auto - done - -lemma has_vector_derivative_add: - assumes "(f has_vector_derivative f') net" - and "(g has_vector_derivative g') net" - shows "((\x. f x + g x) has_vector_derivative (f' + g')) net" - using has_derivative_add[OF assms[unfolded has_vector_derivative_def]] - unfolding has_vector_derivative_def - unfolding scaleR_right_distrib - by auto - -lemma has_vector_derivative_sub: - assumes "(f has_vector_derivative f') net" - and "(g has_vector_derivative g') net" - shows "((\x. f x - g x) has_vector_derivative (f' - g')) net" - using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]] - unfolding has_vector_derivative_def scaleR_right_diff_distrib - by auto - -lemma has_vector_derivative_bilinear_within: - assumes "(f has_vector_derivative f') (at x within s)" - and "(g has_vector_derivative g') (at x within s)" - assumes "bounded_bilinear h" - shows "((\x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)" -proof - - interpret bounded_bilinear h - using assms by auto - show ?thesis - using has_derivative_bilinear_within[OF assms(1-2)[unfolded has_vector_derivative_def], of h] - unfolding o_def has_vector_derivative_def - using assms(3) - unfolding scaleR_right scaleR_left scaleR_right_distrib - by auto -qed - -lemma has_vector_derivative_bilinear_at: - assumes "(f has_vector_derivative f') (at x)" - and "(g has_vector_derivative g') (at x)" - assumes "bounded_bilinear h" - shows "((\x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)" - using has_vector_derivative_bilinear_within[OF assms] . + "(f has_vector_derivative f') (at x within s) \ t \ s \ (f has_vector_derivative f') (at x within t)" + by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset) lemma has_vector_derivative_at_within: "(f has_vector_derivative f') (at x) \ (f has_vector_derivative f') (at x within s)" diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Apr 03 17:56:08 2014 +0200 @@ -8793,11 +8793,10 @@ by (auto simp add: algebra_simps) have "(f \ (\t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\x. 0) \ (\z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0 .. 1})" - apply (rule diff_chain_within) - apply (rule has_derivative_add) + apply (intro derivative_eq_intros) + apply simp_all + apply (simp add: field_simps) unfolding scaleR_simps - apply (intro has_derivative_intros) - apply (intro has_derivative_intros) apply (rule has_derivative_within_subset,rule assms(6)[rule_format]) apply (rule *) apply safe diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/NSA/HDeriv.thy --- a/src/HOL/NSA/HDeriv.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/NSA/HDeriv.thy Thu Apr 03 17:56:08 2014 +0200 @@ -34,10 +34,10 @@ lemma DERIV_NS_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)" -by (simp add: deriv_def LIM_NSLIM_iff) +by (simp add: DERIV_def LIM_NSLIM_iff) lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D" -by (simp add: deriv_def LIM_NSLIM_iff) +by (simp add: DERIV_def LIM_NSLIM_iff) lemma hnorm_of_hypreal: "\r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \r\" @@ -377,7 +377,7 @@ text{*Now equivalence between NSDERIV and DERIV*} lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)" -by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff) +by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff) (* NS version *) lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/NthRoot.thy Thu Apr 03 17:56:08 2014 +0200 @@ -326,7 +326,7 @@ qed next show "DERIV (\x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros simp: real_of_nat_def) show "- real n * root n x ^ (n - Suc 0) \ 0" using n x by simp qed (rule isCont_real_root) @@ -471,8 +471,8 @@ using DERIV_real_sqrt_generic by simp declare - DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] - DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] + DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros] + DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros] lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)" apply auto diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Probability/Distributions.thy --- a/src/HOL/Probability/Distributions.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Probability/Distributions.thy Thu Apr 03 17:56:08 2014 +0200 @@ -52,7 +52,7 @@ let ?F = "\x. - exp (- x * l)" have deriv: "\x. DERIV ?F x :> ?f x" "\x. 0 \ l * exp (- x * l)" - by (auto intro!: DERIV_intros simp: zero_le_mult_iff) + by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff) have "emeasure ?D (space ?D) = (\\<^sup>+ x. ereal (?f x) * indicator {0..} x \lborel)" by (auto simp: emeasure_density exponential_density_def @@ -178,12 +178,12 @@ proof (rule integral_FTC_atLeastAtMost) fix x assume "0 \ x" "x \ b" show "DERIV (\x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros) show "isCont (\x. exp (- x) - x * exp (- x)) x " by (intro continuous_intros) qed fact also have "(\x. (exp (-x)) * indicator {0 .. b} x \lborel) = - exp (- b) - - exp (- 0)" - by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros) + by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros) finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)" by (auto simp: field_simps exp_minus inverse_eq_divide) qed @@ -374,7 +374,7 @@ fix x show "DERIV (\x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" using uniform_distributed_params[OF D] - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros) show "isCont (\x. x / Sigma_Algebra.measure lborel {a..b}) x" using uniform_distributed_params[OF D] by (auto intro!: isCont_divide) diff -r 9bb2856cc845 -r 0556204bc230 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Thu Apr 03 17:16:02 2014 +0200 +++ b/src/HOL/Transcendental.thy Thu Apr 03 17:56:08 2014 +0200 @@ -630,7 +630,7 @@ and 3: "summable (\n. (diffs (diffs c)) n * K ^ n)" and 4: "norm x < norm K" shows "DERIV (\x. \n. c n * x ^ n) x :> (\n. (diffs c) n * x ^ n)" - unfolding deriv_def + unfolding DERIV_def proof (rule LIM_zero_cancel) show "(\h. (suminf (\n. c n * (x + h) ^ n) - suminf (\n. c n * x ^ n)) / h - suminf (\n. diffs c n * x ^ n)) -- 0 --> 0" @@ -669,7 +669,7 @@ and "summable L" and L_def: "\n x y. \ x \ { a <..< b} ; y \ { a <..< b} \ \ \f x n - f y n\ \ L n * \x - y\" shows "DERIV (\ x. suminf (f x)) x0 :> (suminf (f' x0))" - unfolding deriv_def + unfolding DERIV_def proof (rule LIM_I) fix r :: real assume "0 < r" hence "0 < r/3" by auto @@ -863,7 +863,7 @@ { fix n show "DERIV (\ x. ?f x n) x0 :> (?f' x0 n)" - by (auto intro!: DERIV_intros simp del: power_Suc) + by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def) } { fix x @@ -978,7 +978,7 @@ apply (simp del: of_real_add) done -declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] +declare DERIV_exp[THEN DERIV_chain2, derivative_intros] lemma isCont_exp: "isCont exp x" by (rule DERIV_exp [THEN DERIV_isCont]) @@ -1315,7 +1315,7 @@ lemma DERIV_ln_divide: "0 < x \ DERIV ln x :> 1 / x" by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse) -declare DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] +declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros] lemma ln_series: assumes "0 < x" and "x < 2" @@ -1356,7 +1356,7 @@ hence "DERIV (\x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto hence "DERIV (\x. suminf (?f (x - 1))) x :> suminf (?f' x)" - unfolding deriv_def repos . + unfolding DERIV_def repos . ultimately have "DERIV (\x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))" by (rule DERIV_diff) thus "DERIV (\x. ln x - suminf (?f (x - 1))) x :> 0" by auto @@ -1621,7 +1621,7 @@ proof - let ?l = "\y. ln y - y + 1" have D: "\x. 0 < x \ DERIV ?l x :> (1 / x - 1)" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros) show ?thesis proof (cases rule: linorder_cases) @@ -1699,9 +1699,9 @@ show ?case proof (rule lhospital_at_top_at_top) show "eventually (\x. DERIV (\x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top" - by eventually_elim (intro DERIV_intros, simp, simp) + by eventually_elim (intro derivative_eq_intros, auto) show "eventually (\x. DERIV exp x :> exp x) at_top" - by eventually_elim (auto intro!: DERIV_intros) + by eventually_elim auto show "eventually (\x. exp x \ 0) at_top" by auto from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"] @@ -1825,12 +1825,12 @@ proof - def lb \ "1 / ln b" moreover have "DERIV (\y. lb * ln y) x :> lb / x" - using `x > 0` by (auto intro!: DERIV_intros) + using `x > 0` by (auto intro!: derivative_eq_intros) ultimately show ?thesis by (simp add: log_def) qed -lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] +lemmas DERIV_log[THEN DERIV_chain2, derivative_intros] lemma powr_log_cancel [simp]: "0 < a \ a \ 1 \ 0 < x \ a powr (log a x) = x" by (simp add: powr_def log_def) @@ -2180,7 +2180,7 @@ summable_minus summable_sin summable_cos) done -declare DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] +declare DERIV_sin[THEN DERIV_chain2, derivative_intros] lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)" unfolding cos_def sin_def @@ -2189,7 +2189,7 @@ summable_minus summable_sin summable_cos suminf_minus) done -declare DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] +declare DERIV_cos[THEN DERIV_chain2, derivative_intros] lemma isCont_sin: "isCont sin x" by (rule DERIV_sin [THEN DERIV_isCont]) @@ -2238,7 +2238,7 @@ lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" proof - have "\x. DERIV (\x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros) hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2" by (rule DERIV_isconst_all) thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp @@ -2276,19 +2276,19 @@ lemma DERIV_fun_pow: "DERIV g x :> m ==> DERIV (\x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros simp: real_of_nat_def) lemma DERIV_fun_exp: "DERIV g x :> m ==> DERIV (\x. exp(g x)) x :> exp(g x) * m" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_intros) lemma DERIV_fun_sin: "DERIV g x :> m ==> DERIV (\x. sin(g x)) x :> cos(g x) * m" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_intros) lemma DERIV_fun_cos: "DERIV g x :> m ==> DERIV (\x. cos(g x)) x :> -sin(g x) * m" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros simp: real_of_nat_def) lemma sin_cos_add_lemma: "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 + @@ -2296,7 +2296,7 @@ (is "?f x = 0") proof - have "\x. DERIV (\x. ?f x) x :> 0" - by (auto intro!: DERIV_intros simp add: algebra_simps) + by (auto intro!: derivative_eq_intros simp add: algebra_simps) hence "?f x = ?f 0" by (rule DERIV_isconst_all) thus ?thesis by simp @@ -2312,7 +2312,7 @@ "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0") proof - have "\x. DERIV (\x. ?f x) x :> 0" - by (auto intro!: DERIV_intros simp add: algebra_simps) + by (auto intro!: derivative_eq_intros simp add: algebra_simps) hence "?f x = ?f 0" by (rule DERIV_isconst_all) thus ?thesis by simp @@ -2859,7 +2859,7 @@ lemma DERIV_tan [simp]: "cos x \ 0 \ DERIV tan x :> inverse ((cos x)\<^sup>2)" unfolding tan_def - by (auto intro!: DERIV_intros, simp add: divide_inverse power2_eq_square) + by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square) lemma isCont_tan: "cos x \ 0 \ isCont tan x" by (rule DERIV_tan [THEN DERIV_isCont]) @@ -3332,9 +3332,9 @@ done declare - DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] - DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] - DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] + DERIV_arcsin[THEN DERIV_chain2, derivative_intros] + DERIV_arccos[THEN DERIV_chain2, derivative_intros] + DERIV_arctan[THEN DERIV_chain2, derivative_intros] lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))" by (rule filterlim_at_bot_at_right[where Q="\x. - pi/2 < x \ x < pi/2" and P="\x. True" and g=arctan]) @@ -3465,7 +3465,7 @@ done lemma DERIV_cos_add [simp]: "DERIV (\x. cos (x + k)) xa :> - sin (xa + k)" - by (auto intro!: DERIV_intros) + by (auto intro!: derivative_eq_intros) lemma sin_zero_abs_cos_one: "sin x = 0 ==> \cos x\ = 1" by (auto simp add: sin_zero_iff even_mult_two_ex)