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