src/HOL/Multivariate_Analysis/Derivative.thy
 changeset 51478 270b21f3ae0a parent 51363 d4d00c804645 child 51641 cd05e9fcc63d
```     1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 22 10:41:43 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Mar 22 10:41:43 2013 +0100
1.3 @@ -576,10 +576,6 @@
1.4    unfolding FDERIV_conv_has_derivative [symmetric]
1.5    by (rule FDERIV_unique)
1.6
1.7 -lemma continuous_isCont: "isCont f x = continuous (at x) f"
1.8 -  unfolding isCont_def LIM_def
1.9 -  unfolding continuous_at Lim_at unfolding dist_nz by auto
1.10 -
1.11  lemma frechet_derivative_unique_within_closed_interval:
1.12    fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
1.13    assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" "x \<in> {a..b}" (is "x\<in>?I")
1.14 @@ -783,15 +779,12 @@
1.15    shows "\<exists>x\<in>{a<..<b}. (f b - f a = (f' x) (b - a))"
1.16  proof-
1.17    have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
1.18 -    apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
1.19 -    defer
1.20 -    apply(rule continuous_on_intros assms(2))+
1.21 -  proof
1.22 +  proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
1.23      fix x assume x:"x \<in> {a<..<b}"
1.24      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
1.25        by (intro has_derivative_intros assms(3)[rule_format,OF x]
1.26          mult_right_has_derivative)
1.27 -  qed(insert assms(1), auto simp add:field_simps)
1.28 +  qed (insert assms(1,2), auto intro!: continuous_on_intros simp: field_simps)
1.29    then guess x ..
1.30    thus ?thesis apply(rule_tac x=x in bexI)
1.31      apply(drule fun_cong[of _ _ "b - a"]) by auto
```