tidy up of Derivative
authorpaulson <lp15@cam.ac.uk>
Sun May 20 18:37:34 2018 +0100 (12 months ago)
changeset 682390764ee22a4d1
parent 68223 88dd06301dd3
child 68240 fa63bde6d659
tidy up of Derivative
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat May 19 20:42:34 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun May 20 18:37:34 2018 +0100
     1.3 @@ -1154,7 +1154,7 @@
     1.4            vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
     1.5        apply (rule vector_derivative_at_within_ivl
     1.6                    [OF has_vector_derivative_transform_within_open
     1.7 -                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and s = "{0<..<1}-s"]])
     1.8 +                      [where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]])
     1.9        using s g assms x
    1.10        apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
    1.11                          vector_derivative_within_interior vector_derivative_works [symmetric])
    1.12 @@ -4453,7 +4453,7 @@
    1.13      case True then show ?thesis
    1.14        apply (simp add: continuous_within)
    1.15        apply (rule Lim_transform_away_within [of _ "z+1" _ "\<lambda>w::complex. (f w - f z)/(w - z)"])
    1.16 -      using has_field_derivative_at_within DERIV_within_iff f'
    1.17 +      using has_field_derivative_at_within has_field_derivative_iff f'
    1.18        apply (fastforce simp add:)+
    1.19        done
    1.20    next
    1.21 @@ -5554,7 +5554,7 @@
    1.22      apply (rule w)
    1.23      done
    1.24    show ?thes2
    1.25 -    apply (simp add: DERIV_within_iff del: power_Suc)
    1.26 +    apply (simp add: has_field_derivative_iff del: power_Suc)
    1.27      apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
    1.28      apply (simp add: \<open>k \<noteq> 0\<close> **)
    1.29      done
     2.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 19 20:42:34 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun May 20 18:37:34 2018 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4  lemma has_derivative_mult_right:
     2.5    fixes c:: "'a :: real_normed_algebra"
     2.6    shows "((( * ) c) has_derivative (( * ) c)) F"
     2.7 -by (rule has_derivative_mult_right [OF has_derivative_id])
     2.8 +by (rule has_derivative_mult_right [OF has_derivative_ident])
     2.9  
    2.10  lemma has_derivative_of_real[derivative_intros, simp]:
    2.11    "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
    2.12 @@ -382,7 +382,7 @@
    2.13  lemma holomorphic_on_Un [holomorphic_intros]:
    2.14    assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
    2.15    shows   "f holomorphic_on (A \<union> B)"
    2.16 -  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A] 
    2.17 +  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A]
    2.18                               at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
    2.19  
    2.20  lemma holomorphic_on_If_Un [holomorphic_intros]:
    2.21 @@ -839,10 +839,10 @@
    2.22    show ?thesis
    2.23      unfolding has_field_derivative_def
    2.24    proof (rule has_derivative_sequence [OF cvs _ _ x])
    2.25 -  show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    2.26 -    by (rule tf)
    2.27 -  next show "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
    2.28 -    by (blast intro: **)
    2.29 +    show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    2.30 +      by (rule tf)
    2.31 +  next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
    2.32 +      unfolding eventually_sequentially by (blast intro: **)
    2.33    qed (metis has_field_derivative_def df)
    2.34  qed
    2.35  
    2.36 @@ -882,8 +882,8 @@
    2.37        by (metis df has_field_derivative_def mult_commute_abs)
    2.38    next show " ((\<lambda>n. f n x) sums l)"
    2.39      by (rule sf)
    2.40 -  next show "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
    2.41 -    by (blast intro: **)
    2.42 +  next show "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
    2.43 +      unfolding eventually_sequentially by (blast intro: **)
    2.44    qed
    2.45  qed
    2.46  
    2.47 @@ -922,10 +922,8 @@
    2.48        and "x \<in> s"  "y \<in> s"
    2.49      shows "norm(f x - f y) \<le> B * norm(x - y)"
    2.50    apply (rule differentiable_bound [OF cvs])
    2.51 -  apply (rule ballI, erule df [unfolded has_field_derivative_def])
    2.52 -  apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn)
    2.53 -  apply fact
    2.54 -  apply fact
    2.55 +  apply (erule df [unfolded has_field_derivative_def])
    2.56 +  apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
    2.57    done
    2.58  
    2.59  subsection\<open>Inverse function theorem for complex derivatives\<close>
     3.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sat May 19 20:42:34 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sun May 20 18:37:34 2018 +0100
     3.3 @@ -864,7 +864,7 @@
     3.4    proof -
     3.5      define h where [abs_def]: "h z = (z - \<xi>)^2 * f z" for z
     3.6      have h0: "(h has_field_derivative 0) (at \<xi>)"
     3.7 -      apply (simp add: h_def Derivative.DERIV_within_iff)
     3.8 +      apply (simp add: h_def has_field_derivative_iff)
     3.9        apply (rule Lim_transform_within [OF that, of 1])
    3.10        apply (auto simp: divide_simps power2_eq_square)
    3.11        done
    3.12 @@ -879,7 +879,7 @@
    3.13          case False
    3.14          then have "f field_differentiable at z within S"
    3.15            using holomorphic_onD [OF holf, of z] \<open>z \<in> S\<close>
    3.16 -          unfolding field_differentiable_def DERIV_within_iff
    3.17 +          unfolding field_differentiable_def has_field_derivative_iff
    3.18            by (force intro: exI [where x="dist \<xi> z"] elim: Lim_transform_within_set [unfolded eventually_at])
    3.19          then show ?thesis
    3.20            by (simp add: h_def power2_eq_square derivative_intros)
    3.21 @@ -1719,7 +1719,7 @@
    3.22    have "cnj \<circ> f \<circ> cnj field_differentiable at x within S \<inter> {z. Im z < 0}"
    3.23          if "x \<in> S" "Im x < 0" "f field_differentiable at (cnj x) within S \<inter> {z. 0 < Im z}" for x
    3.24      using that
    3.25 -    apply (simp add: field_differentiable_def Derivative.DERIV_within_iff Lim_within dist_norm, clarify)
    3.26 +    apply (simp add: field_differentiable_def has_field_derivative_iff Lim_within dist_norm, clarify)
    3.27      apply (rule_tac x="cnj f'" in exI)
    3.28      apply (elim all_forward ex_forward conj_forward imp_forward asm_rl, clarify)
    3.29      apply (drule_tac x="cnj xa" in bspec)
     4.1 --- a/src/HOL/Analysis/Derivative.thy	Sat May 19 20:42:34 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Derivative.thy	Sun May 20 18:37:34 2018 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4  (*  Title:      HOL/Analysis/Derivative.thy
     4.5      Author:     John Harrison
     4.6 -    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light)
     4.7 +    Author:     Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP
     4.8  *)
     4.9  
    4.10  section \<open>Multivariate calculus in Euclidean space\<close>
    4.11 @@ -15,18 +15,6 @@
    4.12  
    4.13  subsection \<open>Derivatives\<close>
    4.14  
    4.15 -subsubsection \<open>Combining theorems\<close>
    4.16 -
    4.17 -lemmas has_derivative_id = has_derivative_ident
    4.18 -lemmas has_derivative_neg = has_derivative_minus
    4.19 -lemmas has_derivative_sub = has_derivative_diff
    4.20 -lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
    4.21 -lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
    4.22 -lemmas inner_right_has_derivative = has_derivative_inner_right
    4.23 -lemmas inner_left_has_derivative = has_derivative_inner_left
    4.24 -lemmas mult_right_has_derivative = has_derivative_mult_right
    4.25 -lemmas mult_left_has_derivative = has_derivative_mult_left
    4.26 -
    4.27  lemma has_derivative_add_const:
    4.28    "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
    4.29    by (intro derivative_eq_intros) auto
    4.30 @@ -34,20 +22,6 @@
    4.31  
    4.32  subsection \<open>Derivative with composed bilinear function\<close>
    4.33  
    4.34 -lemma has_derivative_bilinear_within:
    4.35 -  assumes "(f has_derivative f') (at x within s)"
    4.36 -    and "(g has_derivative g') (at x within s)"
    4.37 -    and "bounded_bilinear h"
    4.38 -  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
    4.39 -  using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
    4.40 -
    4.41 -lemma has_derivative_bilinear_at:
    4.42 -  assumes "(f has_derivative f') (at x)"
    4.43 -    and "(g has_derivative g') (at x)"
    4.44 -    and "bounded_bilinear h"
    4.45 -  shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
    4.46 -  using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
    4.47 -
    4.48  text \<open>More explicit epsilon-delta forms.\<close>
    4.49  
    4.50  lemma has_derivative_within':
    4.51 @@ -56,15 +30,14 @@
    4.52      (\<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
    4.53        norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
    4.54    unfolding has_derivative_within Lim_within dist_norm
    4.55 -  unfolding diff_0_right
    4.56    by (simp add: diff_diff_eq)
    4.57  
    4.58  lemma has_derivative_at':
    4.59 -  "(f has_derivative f') (at x) \<longleftrightarrow> bounded_linear f' \<and>
    4.60 -    (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
    4.61 -      norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
    4.62 -  using has_derivative_within' [of f f' x UNIV]
    4.63 -  by simp
    4.64 +  "(f has_derivative f') (at x) 
    4.65 +   \<longleftrightarrow> bounded_linear f' \<and>
    4.66 +       (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
    4.67 +        norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
    4.68 +  using has_derivative_within' [of f f' x UNIV] by simp
    4.69  
    4.70  lemma has_derivative_at_withinI:
    4.71    "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
    4.72 @@ -80,7 +53,7 @@
    4.73    fixes f :: "real \<Rightarrow> real"
    4.74      and y :: "real"
    4.75    shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
    4.76 -    ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
    4.77 +         ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
    4.78  proof -
    4.79    have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
    4.80      ((\<lambda>t. (f t - f x) / (t - x) - y) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I))"
    4.81 @@ -95,8 +68,6 @@
    4.82  
    4.83  subsubsection \<open>Caratheodory characterization\<close>
    4.84  
    4.85 -lemmas DERIV_within_iff = has_field_derivative_iff
    4.86 -
    4.87  lemma DERIV_caratheodory_within:
    4.88    "(f has_field_derivative l) (at x within S) \<longleftrightarrow>
    4.89     (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within S) g \<and> g x = l)"
    4.90 @@ -108,7 +79,7 @@
    4.91      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
    4.92      show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
    4.93      show "continuous (at x within S) ?g" using \<open>?lhs\<close>
    4.94 -      by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
    4.95 +      by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
    4.96      show "?g x = l" by simp
    4.97    qed
    4.98  next
    4.99 @@ -116,7 +87,7 @@
   4.100    then obtain g where
   4.101      "(\<forall>z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast
   4.102    thus ?lhs
   4.103 -    by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
   4.104 +    by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
   4.105  qed
   4.106  
   4.107  subsection \<open>Differentiability\<close>
   4.108 @@ -173,7 +144,7 @@
   4.109  lemma differentiable_on_mult [simp, derivative_intros]:
   4.110    fixes f :: "'M::real_normed_vector \<Rightarrow> 'a::real_normed_algebra"
   4.111    shows "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) differentiable_on S"
   4.112 -  apply (simp add: differentiable_on_def differentiable_def)
   4.113 +  unfolding differentiable_on_def differentiable_def
   4.114    using differentiable_def differentiable_mult by blast
   4.115  
   4.116  lemma differentiable_on_compose:
   4.117 @@ -211,9 +182,9 @@
   4.118    by (blast intro: differentiable_scaleR)
   4.119  
   4.120  lemma has_derivative_sqnorm_at [derivative_intros, simp]:
   4.121 -   "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
   4.122 -using has_derivative_bilinear_at [of id id a id id "(\<bullet>)"]
   4.123 -by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
   4.124 +  "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
   4.125 +  using bounded_bilinear.FDERIV  [of "(\<bullet>)" id id a _ id id]
   4.126 +  by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
   4.127  
   4.128  lemma differentiable_sqnorm_at [derivative_intros, simp]:
   4.129    fixes a :: "'a :: {real_normed_vector,real_inner}"
   4.130 @@ -378,29 +349,24 @@
   4.131  
   4.132  lemma frechet_derivative_unique_within:
   4.133    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   4.134 -  assumes "(f has_derivative f') (at x within S)"
   4.135 -    and "(f has_derivative f'') (at x within S)"
   4.136 -    and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S"
   4.137 +  assumes 1: "(f has_derivative f') (at x within S)"
   4.138 +    and 2: "(f has_derivative f'') (at x within S)"
   4.139 +    and S: "\<And>i e. \<lbrakk>i\<in>Basis; e>0\<rbrakk> \<Longrightarrow> \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S"
   4.140    shows "f' = f''"
   4.141  proof -
   4.142    note as = assms(1,2)[unfolded has_derivative_def]
   4.143    then interpret f': bounded_linear f' by auto
   4.144    from as interpret f'': bounded_linear f'' by auto
   4.145    have "x islimpt S" unfolding islimpt_approachable
   4.146 -  proof (rule, rule)
   4.147 +  proof (intro allI impI)
   4.148      fix e :: real
   4.149      assume "e > 0"
   4.150      obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S"
   4.151        using assms(3) SOME_Basis \<open>e>0\<close> by blast
   4.152      then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
   4.153 -      apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
   4.154 -      unfolding dist_norm
   4.155 -      apply (auto simp: SOME_Basis nonzero_Basis)
   4.156 -      done
   4.157 -  qed
   4.158 +      by (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI) (auto simp: dist_norm SOME_Basis nonzero_Basis)  qed
   4.159    then have *: "netlimit (at x within S) = x"
   4.160 -    apply (auto intro!: netlimit_within)
   4.161 -    by (metis trivial_limit_within)
   4.162 +    by (simp add: Lim_ident_at trivial_limit_within)
   4.163    show ?thesis
   4.164    proof (rule linear_eq_stdbasis)
   4.165      show "linear f'" "linear f''"
   4.166 @@ -450,81 +416,65 @@
   4.167  
   4.168  lemma frechet_derivative_unique_within_closed_interval:
   4.169    fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   4.170 -  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
   4.171 -    and "x \<in> cbox a b"
   4.172 +  assumes ab: "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
   4.173 +    and x: "x \<in> cbox a b"
   4.174      and "(f has_derivative f' ) (at x within cbox a b)"
   4.175      and "(f has_derivative f'') (at x within cbox a b)"
   4.176    shows "f' = f''"
   4.177 -  apply(rule frechet_derivative_unique_within)
   4.178 -  apply(rule assms(3,4))+
   4.179 -proof (rule, rule, rule)
   4.180 +proof (rule frechet_derivative_unique_within)
   4.181    fix e :: real
   4.182    fix i :: 'a
   4.183    assume "e > 0" and i: "i \<in> Basis"
   4.184    then show "\<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> cbox a b"
   4.185    proof (cases "x\<bullet>i = a\<bullet>i")
   4.186      case True
   4.187 -    then show ?thesis
   4.188 -      apply (rule_tac x="(min (b\<bullet>i - a\<bullet>i)  e) / 2" in exI)
   4.189 -      using assms(1)[THEN bspec[where x=i]] and \<open>e>0\<close> and assms(2)
   4.190 -      unfolding mem_box
   4.191 -      using i
   4.192 -      apply (auto simp add: field_simps inner_simps inner_Basis)
   4.193 -      done
   4.194 +    with ab[of i] \<open>e>0\<close> x i show ?thesis
   4.195 +      by (rule_tac x="(min (b\<bullet>i - a\<bullet>i) e) / 2" in exI)
   4.196 +         (auto simp add: mem_box field_simps inner_simps inner_Basis)
   4.197    next
   4.198 -    note * = assms(2)[unfolded mem_box, THEN bspec, OF i]
   4.199      case False
   4.200      moreover have "a \<bullet> i < x \<bullet> i"
   4.201 -      using False * by auto
   4.202 +      using False i mem_box(2) x by force
   4.203      moreover {
   4.204        have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> a\<bullet>i *2 + x\<bullet>i - a\<bullet>i"
   4.205          by auto
   4.206        also have "\<dots> = a\<bullet>i + x\<bullet>i"
   4.207          by auto
   4.208        also have "\<dots> \<le> 2 * (x\<bullet>i)"
   4.209 -        using * by auto
   4.210 +        using \<open>a \<bullet> i < x \<bullet> i\<close> by auto
   4.211        finally have "a \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e \<le> x \<bullet> i * 2"
   4.212          by auto
   4.213      }
   4.214      moreover have "min (x \<bullet> i - a \<bullet> i) e \<ge> 0"
   4.215 -      using * and \<open>e>0\<close> by auto
   4.216 +      by (simp add: \<open>0 < e\<close> \<open>a \<bullet> i < x \<bullet> i\<close> less_eq_real_def)
   4.217      then have "x \<bullet> i * 2 \<le> b \<bullet> i * 2 + min (x \<bullet> i - a \<bullet> i) e"
   4.218 -      using * by auto
   4.219 +      using i mem_box(2) x by force
   4.220      ultimately show ?thesis
   4.221 -      apply (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
   4.222 -      using assms(1)[THEN bspec, OF i] and \<open>e>0\<close> and assms(2)
   4.223 -      unfolding mem_box
   4.224 -      using i
   4.225 -      apply (auto simp add: field_simps inner_simps inner_Basis)
   4.226 -      done
   4.227 +    using ab[of i] \<open>e>0\<close> x i 
   4.228 +      by (rule_tac x="- (min (x\<bullet>i - a\<bullet>i) e) / 2" in exI)
   4.229 +         (auto simp add: mem_box field_simps inner_simps inner_Basis)
   4.230    qed
   4.231 -qed
   4.232 +qed (use assms in auto)
   4.233  
   4.234  lemma frechet_derivative_unique_within_open_interval:
   4.235    fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   4.236 -  assumes "x \<in> box a b"
   4.237 -    and "(f has_derivative f' ) (at x within box a b)"
   4.238 -    and "(f has_derivative f'') (at x within box a b)"
   4.239 +  assumes x: "x \<in> box a b"
   4.240 +    and f: "(f has_derivative f' ) (at x within box a b)" "(f has_derivative f'') (at x within box a b)"
   4.241    shows "f' = f''"
   4.242  proof -
   4.243 -  from assms(1) have *: "at x within box a b = at x"
   4.244 -    by (metis at_within_interior interior_open open_box)
   4.245 -  from assms(2,3) [unfolded *] show "f' = f''"
   4.246 -    by (rule has_derivative_unique)
   4.247 +  have "at x within box a b = at x"
   4.248 +    by (metis x at_within_interior interior_open open_box)
   4.249 +  with f show "f' = f''"
   4.250 +    by (simp add: has_derivative_unique)
   4.251  qed
   4.252  
   4.253  lemma frechet_derivative_at:
   4.254    "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
   4.255 -  apply (rule has_derivative_unique[of f])
   4.256 -  apply assumption
   4.257 -  unfolding frechet_derivative_works[symmetric]
   4.258 -  using differentiable_def
   4.259 -  apply auto
   4.260 -  done
   4.261 +  using differentiable_def frechet_derivative_works has_derivative_unique by blast
   4.262  
   4.263  lemma frechet_derivative_within_cbox:
   4.264    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   4.265 -  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
   4.266 +  assumes "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
   4.267      and "x \<in> cbox a b"
   4.268      and "(f has_derivative f') (at x within cbox a b)"
   4.269    shows "frechet_derivative f (at x within cbox a b) = f'"
   4.270 @@ -547,7 +497,7 @@
   4.271      using deriv by (rule has_derivative_bounded_linear)
   4.272    show "f' h = 0"
   4.273    proof (cases "h = 0")
   4.274 -    assume "h \<noteq> 0"
   4.275 +    case False
   4.276      from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
   4.277        unfolding eventually_at by (force simp: dist_commute)
   4.278      have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
   4.279 @@ -561,7 +511,7 @@
   4.280        using \<open>h \<noteq> 0\<close> by (auto simp add: d2 dist_norm pos_less_divide_eq)
   4.281      ultimately show "f' h = 0"
   4.282        by (rule DERIV_local_min)
   4.283 -  qed (simp add: f'.zero)
   4.284 +  qed simp
   4.285  qed
   4.286  
   4.287  lemma has_derivative_local_max:
   4.288 @@ -574,21 +524,21 @@
   4.289  
   4.290  lemma differential_zero_maxmin:
   4.291    fixes f::"'a::real_normed_vector \<Rightarrow> real"
   4.292 -  assumes "x \<in> s"
   4.293 -    and "open s"
   4.294 +  assumes "x \<in> S"
   4.295 +    and "open S"
   4.296      and deriv: "(f has_derivative f') (at x)"
   4.297 -    and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
   4.298 +    and mono: "(\<forall>y\<in>S. f y \<le> f x) \<or> (\<forall>y\<in>S. f x \<le> f y)"
   4.299    shows "f' = (\<lambda>v. 0)"
   4.300    using mono
   4.301  proof
   4.302 -  assume "\<forall>y\<in>s. f y \<le> f x"
   4.303 -  with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
   4.304 +  assume "\<forall>y\<in>S. f y \<le> f x"
   4.305 +  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f y \<le> f x) (at x)"
   4.306      unfolding eventually_at_topological by auto
   4.307    with deriv show ?thesis
   4.308      by (rule has_derivative_local_max)
   4.309  next
   4.310 -  assume "\<forall>y\<in>s. f x \<le> f y"
   4.311 -  with \<open>x \<in> s\<close> and \<open>open s\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
   4.312 +  assume "\<forall>y\<in>S. f x \<le> f y"
   4.313 +  with \<open>x \<in> S\<close> and \<open>open S\<close> have "eventually (\<lambda>y. f x \<le> f y) (at x)"
   4.314      unfolding eventually_at_topological by auto
   4.315    with deriv show ?thesis
   4.316      by (rule has_derivative_local_min)
   4.317 @@ -613,28 +563,24 @@
   4.318      unfolding fun_eq_iff by simp
   4.319  qed
   4.320  
   4.321 -lemma rolle:
   4.322 +theorem Rolle:
   4.323    fixes f :: "real \<Rightarrow> real"
   4.324    assumes "a < b"
   4.325 -    and "f a = f b"
   4.326 -    and "continuous_on {a .. b} f"
   4.327 -    and "\<forall>x\<in>{a <..< b}. (f has_derivative f' x) (at x)"
   4.328 +    and fab: "f a = f b"
   4.329 +    and contf: "continuous_on {a..b} f"
   4.330 +    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   4.331    shows "\<exists>x\<in>{a <..< b}. f' x = (\<lambda>v. 0)"
   4.332  proof -
   4.333    have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
   4.334    proof -
   4.335 -    have "(a + b) / 2 \<in> {a .. b}"
   4.336 +    have "(a + b) / 2 \<in> {a..b}"
   4.337        using assms(1) by auto
   4.338 -    then have *: "{a .. b} \<noteq> {}"
   4.339 +    then have *: "{a..b} \<noteq> {}"
   4.340        by auto
   4.341 -    obtain d where d:
   4.342 -        "d \<in>cbox a b"
   4.343 -        "\<forall>y\<in>cbox a b. f y \<le> f d"
   4.344 -      using continuous_attains_sup[OF compact_Icc * assms(3)] by auto
   4.345 -    obtain c where c:
   4.346 -        "c \<in> cbox a b"
   4.347 -        "\<forall>y\<in>cbox a b. f c \<le> f y"
   4.348 -      using continuous_attains_inf[OF compact_Icc * assms(3)] by auto
   4.349 +    obtain d where d: "d \<in>cbox a b" "\<forall>y\<in>cbox a b. f y \<le> f d"
   4.350 +      using continuous_attains_sup[OF compact_Icc * contf] by auto
   4.351 +    obtain c where c: "c \<in> cbox a b" "\<forall>y\<in>cbox a b. f c \<le> f y"
   4.352 +      using continuous_attains_inf[OF compact_Icc * contf] by auto
   4.353      show ?thesis
   4.354      proof (cases "d \<in> box a b \<or> c \<in> box a b")
   4.355        case True
   4.356 @@ -644,16 +590,11 @@
   4.357        define e where "e = (a + b) /2"
   4.358        case False
   4.359        then have "f d = f c"
   4.360 -        using d c assms(2) by auto
   4.361 -      then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
   4.362 -        using c d
   4.363 +        using d c fab by auto
   4.364 +      with c d have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
   4.365          by force
   4.366        then show ?thesis
   4.367 -        apply (rule_tac x=e in bexI)
   4.368 -        unfolding e_def
   4.369 -        using assms(1)
   4.370 -        apply auto
   4.371 -        done
   4.372 +        by (rule_tac x=e in bexI) (auto simp: e_def \<open>a < b\<close>)
   4.373      qed
   4.374    qed
   4.375    then obtain x where x: "x \<in> {a <..< b}" "(\<forall>y\<in>{a <..< b}. f x \<le> f y) \<or> (\<forall>y\<in>{a <..< b}. f y \<le> f x)"
   4.376 @@ -673,18 +614,18 @@
   4.377  lemma mvt:
   4.378    fixes f :: "real \<Rightarrow> real"
   4.379    assumes "a < b"
   4.380 -    and "continuous_on {a..b} f"
   4.381 -  assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
   4.382 +    and contf: "continuous_on {a..b} f"
   4.383 +    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   4.384    shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
   4.385  proof -
   4.386    have "\<exists>x\<in>{a <..< b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
   4.387 -  proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
   4.388 +  proof (intro Rolle[OF \<open>a < b\<close>, of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
   4.389      fix x
   4.390 -    assume x: "x \<in> {a <..< b}"
   4.391 +    assume x: "a < x" "x < b"
   4.392      show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
   4.393          (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
   4.394 -      by (intro derivative_intros assms(3)[rule_format,OF x])
   4.395 -  qed (insert assms(1,2), auto intro!: continuous_intros simp: field_simps)
   4.396 +      by (intro derivative_intros derf[OF x])
   4.397 +  qed (use assms in \<open>auto intro!: continuous_intros simp: field_simps\<close>)
   4.398    then obtain x where
   4.399      "x \<in> {a <..< b}"
   4.400      "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
   4.401 @@ -697,50 +638,33 @@
   4.402  lemma mvt_simple:
   4.403    fixes f :: "real \<Rightarrow> real"
   4.404    assumes "a < b"
   4.405 -    and "\<forall>x\<in>{a..b}. (f has_derivative f' x) (at x within {a..b})"
   4.406 +    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   4.407    shows "\<exists>x\<in>{a<..<b}. f b - f a = f' x (b - a)"
   4.408  proof (rule mvt)
   4.409    have "f differentiable_on {a..b}"
   4.410 -    using assms(2) unfolding differentiable_on_def differentiable_def by fast
   4.411 +    by (meson atLeastAtMost_iff derf differentiable_at_imp_differentiable_on differentiable_def)
   4.412    then show "continuous_on {a..b} f"
   4.413      by (rule differentiable_imp_continuous_on)
   4.414 -  show "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
   4.415 -  proof
   4.416 -    fix x
   4.417 -    assume x: "x \<in> {a <..< b}"
   4.418 -    show "(f has_derivative f' x) (at x)"
   4.419 -      unfolding at_within_open[OF x open_greaterThanLessThan,symmetric]
   4.420 -      apply (rule has_derivative_within_subset)
   4.421 -      apply (rule assms(2)[rule_format])
   4.422 -      using x
   4.423 -      apply auto
   4.424 -      done
   4.425 -  qed
   4.426 -qed (rule assms(1))
   4.427 +  show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x
   4.428 +    by (metis derf not_less order.asym that)
   4.429 +qed (rule assms)
   4.430  
   4.431  lemma mvt_very_simple:
   4.432    fixes f :: "real \<Rightarrow> real"
   4.433    assumes "a \<le> b"
   4.434 -    and "\<forall>x\<in>{a .. b}. (f has_derivative f' x) (at x within {a .. b})"
   4.435 -  shows "\<exists>x\<in>{a .. b}. f b - f a = f' x (b - a)"
   4.436 +    and derf: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   4.437 +  shows "\<exists>x\<in>{a..b}. f b - f a = f' x (b - a)"
   4.438  proof (cases "a = b")
   4.439    interpret bounded_linear "f' b"
   4.440      using assms(2) assms(1) by auto
   4.441    case True
   4.442    then show ?thesis
   4.443 -    apply (rule_tac x=a in bexI)
   4.444 -    using assms(2)[THEN bspec[where x=a]]
   4.445 -    unfolding has_derivative_def
   4.446 -    unfolding True
   4.447 -    using zero
   4.448 -    apply auto
   4.449 -    done
   4.450 +    by force
   4.451  next
   4.452    case False
   4.453    then show ?thesis
   4.454 -    using mvt_simple[OF _ assms(2)]
   4.455 -    using assms(1)
   4.456 -    by auto
   4.457 +    using mvt_simple[OF _ derf]
   4.458 +    by (metis \<open>a \<le> b\<close> atLeastAtMost_iff dual_order.order_iff_strict greaterThanLessThan_iff)
   4.459  qed
   4.460  
   4.461  text \<open>A nice generalization (see Havin's proof of 5.19 from Rudin's book).\<close>
   4.462 @@ -748,19 +672,16 @@
   4.463  lemma mvt_general:
   4.464    fixes f :: "real \<Rightarrow> 'a::real_inner"
   4.465    assumes "a < b"
   4.466 -    and "continuous_on {a .. b} f"
   4.467 -    and "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
   4.468 +    and contf: "continuous_on {a..b} f"
   4.469 +    and derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
   4.470    shows "\<exists>x\<in>{a<..<b}. norm (f b - f a) \<le> norm (f' x (b - a))"
   4.471  proof -
   4.472    have "\<exists>x\<in>{a<..<b}. (f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)"
   4.473 -    apply (rule mvt)
   4.474 -    apply (rule assms(1))
   4.475 -    apply (intro continuous_intros assms(2))
   4.476 -    using assms(3)
   4.477 -    apply (fast intro: has_derivative_inner_right)
   4.478 +    apply (rule mvt [OF \<open>a < b\<close>])
   4.479 +    apply (intro continuous_intros contf)
   4.480 +    using derf apply (blast intro: has_derivative_inner_right)
   4.481      done
   4.482 -  then obtain x where x:
   4.483 -    "x \<in> {a<..<b}"
   4.484 +  then obtain x where x: "x \<in> {a<..<b}"
   4.485      "(f b - f a) \<bullet> f b - (f b - f a) \<bullet> f a = (f b - f a) \<bullet> f' x (b - a)" ..
   4.486    show ?thesis
   4.487    proof (cases "f a = f b")
   4.488 @@ -779,21 +700,18 @@
   4.489    next
   4.490      case True
   4.491      then show ?thesis
   4.492 -      using assms(1)
   4.493 -      apply (rule_tac x="(a + b) /2" in bexI)
   4.494 -      apply auto
   4.495 -      done
   4.496 +      using \<open>a < b\<close> by (rule_tac x="(a + b) /2" in bexI) auto
   4.497    qed
   4.498  qed
   4.499  
   4.500  
   4.501  subsection \<open>More general bound theorems\<close>
   4.502  
   4.503 -lemma differentiable_bound_general:
   4.504 +proposition differentiable_bound_general:
   4.505    fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   4.506    assumes "a < b"
   4.507 -    and f_cont: "continuous_on {a .. b} f"
   4.508 -    and phi_cont: "continuous_on {a .. b} \<phi>"
   4.509 +    and f_cont: "continuous_on {a..b} f"
   4.510 +    and phi_cont: "continuous_on {a..b} \<phi>"
   4.511      and f': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
   4.512      and phi': "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (\<phi> has_vector_derivative \<phi>' x) (at x)"
   4.513      and bnd: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> norm (f' x) \<le> \<phi>' x"
   4.514 @@ -813,7 +731,7 @@
   4.515      with \<open>e > 0\<close> have "e2 > 0" by simp
   4.516      let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
   4.517      define A where "A = {x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
   4.518 -    have A_subset: "A \<subseteq> {a .. b}" by (auto simp: A_def)
   4.519 +    have A_subset: "A \<subseteq> {a..b}" by (auto simp: A_def)
   4.520      {
   4.521        fix x2
   4.522        assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
   4.523 @@ -828,7 +746,7 @@
   4.524            "((\<lambda>x1. norm (f x1 - f a)) \<longlongrightarrow> norm (f x2 - f a)) (at x2 within {a <..<x2})"
   4.525            using a
   4.526            by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
   4.527 -            intro: tendsto_within_subset[where S="{a .. b}"])
   4.528 +            intro: tendsto_within_subset[where S="{a..b}"])
   4.529          moreover
   4.530          have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
   4.531            by (auto simp: eventually_at_filter)
   4.532 @@ -860,85 +778,11 @@
   4.533        using y_all_le \<open>a \<le> y\<close> \<open>y \<le> b\<close>
   4.534        by (auto simp: A_def)
   4.535      hence "A = {a .. y}"
   4.536 -      using A_subset
   4.537 -      by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
   4.538 +      using A_subset by (auto simp: subset_iff y_def cSup_upper intro: A_ivl)
   4.539      from le_cont[OF \<open>a \<le> y\<close> \<open>y \<le> b\<close> y_all_le] have le_y: "?le y" .
   4.540 -    {
   4.541 -      assume "a \<noteq> y" with \<open>a \<le> y\<close> have "a < y" by simp
   4.542 -      have "y = b"
   4.543 -      proof (rule ccontr)
   4.544 -        assume "y \<noteq> b"
   4.545 -        hence "y < b" using \<open>y \<le> b\<close> by simp
   4.546 -        let ?F = "at y within {y..<b}"
   4.547 -        from f' phi'
   4.548 -        have "(f has_vector_derivative f' y) ?F"
   4.549 -          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
   4.550 -          using \<open>a < y\<close> \<open>y < b\<close>
   4.551 -          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
   4.552 -            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
   4.553 -        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
   4.554 -            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
   4.555 -          using \<open>e2 > 0\<close>
   4.556 -          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
   4.557 -        moreover
   4.558 -        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
   4.559 -          by (auto simp: eventually_at_filter)
   4.560 -        ultimately
   4.561 -        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
   4.562 -          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
   4.563 -        proof eventually_elim
   4.564 -          case (elim x1)
   4.565 -          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
   4.566 -          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   4.567 -            by (simp add: ac_simps)
   4.568 -          also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
   4.569 -          also
   4.570 -          from elim have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
   4.571 -            by (simp add: ac_simps)
   4.572 -          finally
   4.573 -          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   4.574 -            by (auto simp: mult_right_mono)
   4.575 -          thus ?case by (simp add: e2_def)
   4.576 -        qed
   4.577 -        moreover have "?le' y" by simp
   4.578 -        ultimately obtain S
   4.579 -        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
   4.580 -          unfolding eventually_at_topological
   4.581 -          by metis
   4.582 -        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
   4.583 -          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
   4.584 -        define d' where "d' = min ((y + b)/2) (y + (d/2))"
   4.585 -        have "d' \<in> A"
   4.586 -          unfolding A_def
   4.587 -        proof safe
   4.588 -          show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
   4.589 -          show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
   4.590 -          fix x1
   4.591 -          assume x1: "x1 \<in> {a..<d'}"
   4.592 -          {
   4.593 -            assume "x1 < y"
   4.594 -            hence "?le x1"
   4.595 -              using \<open>x1 \<in> {a..<d'}\<close> y_all_le by auto
   4.596 -          } moreover {
   4.597 -            assume "x1 \<ge> y"
   4.598 -            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
   4.599 -              by (auto simp: d'_def dist_real_def intro!: d)
   4.600 -            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
   4.601 -              by (rule order_trans[OF _ norm_triangle_ineq]) simp
   4.602 -            also note S(3)[OF x1']
   4.603 -            also note le_y
   4.604 -            finally have "?le x1"
   4.605 -              using \<open>x1 \<ge> y\<close> by (auto simp: algebra_simps)
   4.606 -          } ultimately show "?le x1" by arith
   4.607 -        qed
   4.608 -        hence "d' \<le> y"
   4.609 -          unfolding y_def
   4.610 -          by (rule cSup_upper) simp
   4.611 -        thus False using \<open>d > 0\<close> \<open>y < b\<close>
   4.612 -          by (simp add: d'_def min_def split: if_split_asm)
   4.613 -      qed
   4.614 -    } moreover {
   4.615 -      assume "a = y"
   4.616 +    have "y = b"
   4.617 +    proof (cases "a = y")
   4.618 +      case True
   4.619        with \<open>a < b\<close> have "y < b" by simp
   4.620        with \<open>a = y\<close> f_cont phi_cont \<open>e2 > 0\<close>
   4.621        have 1: "\<forall>\<^sub>F x in at y within {y..b}. dist (f x) (f y) < e2"
   4.622 @@ -966,8 +810,7 @@
   4.623          finally show "?le x1" .
   4.624        qed
   4.625        from this[unfolded eventually_at_topological] \<open>?le y\<close>
   4.626 -      obtain S
   4.627 -      where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
   4.628 +      obtain S where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
   4.629          by metis
   4.630        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
   4.631          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
   4.632 @@ -987,81 +830,140 @@
   4.633        hence "d' \<le> y"
   4.634          unfolding y_def
   4.635          by (rule cSup_upper) simp
   4.636 -      hence "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
   4.637 +      then show "y = b" using \<open>d > 0\<close> \<open>y < b\<close>
   4.638          by (simp add: d'_def)
   4.639 -    } ultimately have "y = b"
   4.640 -      by auto
   4.641 +    next
   4.642 +      case False
   4.643 +      with \<open>a \<le> y\<close> have "a < y" by simp
   4.644 +      show "y = b"
   4.645 +      proof (rule ccontr)
   4.646 +        assume "y \<noteq> b"
   4.647 +        hence "y < b" using \<open>y \<le> b\<close> by simp
   4.648 +        let ?F = "at y within {y..<b}"
   4.649 +        from f' phi'
   4.650 +        have "(f has_vector_derivative f' y) ?F"
   4.651 +          and "(\<phi> has_vector_derivative \<phi>' y) ?F"
   4.652 +          using \<open>a < y\<close> \<open>y < b\<close>
   4.653 +          by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def
   4.654 +            intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"])
   4.655 +        hence "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>"
   4.656 +            "\<forall>\<^sub>F x1 in ?F. norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>"
   4.657 +          using \<open>e2 > 0\<close>
   4.658 +          by (auto simp: has_derivative_within_alt2 has_vector_derivative_def)
   4.659 +        moreover
   4.660 +        have "\<forall>\<^sub>F x1 in ?F. y \<le> x1" "\<forall>\<^sub>F x1 in ?F. x1 < b"
   4.661 +          by (auto simp: eventually_at_filter)
   4.662 +        ultimately
   4.663 +        have "\<forall>\<^sub>F x1 in ?F. norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>"
   4.664 +          (is "\<forall>\<^sub>F x1 in ?F. ?le' x1")
   4.665 +        proof eventually_elim
   4.666 +          case (elim x1)
   4.667 +          from norm_triangle_ineq2[THEN order_trans, OF elim(1)]
   4.668 +          have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   4.669 +            by (simp add: ac_simps)
   4.670 +          also have "norm (f' y) \<le> \<phi>' y" using bnd \<open>a < y\<close> \<open>y < b\<close> by simp
   4.671 +          also have "\<phi>' y * \<bar>x1 - y\<bar> \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar>"
   4.672 +            using elim by (simp add: ac_simps)
   4.673 +          finally
   4.674 +          have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
   4.675 +            by (auto simp: mult_right_mono)
   4.676 +          thus ?case by (simp add: e2_def)
   4.677 +        qed
   4.678 +        moreover have "?le' y" by simp
   4.679 +        ultimately obtain S
   4.680 +        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..<b} \<Longrightarrow> ?le' x"
   4.681 +          unfolding eventually_at_topological
   4.682 +          by metis
   4.683 +        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
   4.684 +          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
   4.685 +        define d' where "d' = min ((y + b)/2) (y + (d/2))"
   4.686 +        have "d' \<in> A"
   4.687 +          unfolding A_def
   4.688 +        proof safe
   4.689 +          show "a \<le> d'" using \<open>a < y\<close> \<open>0 < d\<close> \<open>y < b\<close> by (simp add: d'_def)
   4.690 +          show "d' \<le> b" using \<open>y < b\<close> by (simp add: d'_def min_def)
   4.691 +          fix x1
   4.692 +          assume x1: "x1 \<in> {a..<d'}"
   4.693 +          show "?le x1"
   4.694 +          proof (cases "x1 < y")
   4.695 +            case True
   4.696 +            then show ?thesis
   4.697 +              using \<open>y \<in> A\<close> local.leI x1 by auto
   4.698 +          next
   4.699 +            case False
   4.700 +            hence x1': "x1 \<in> S" "x1 \<in> {y..<b}" using x1
   4.701 +              by (auto simp: d'_def dist_real_def intro!: d)
   4.702 +            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
   4.703 +              by (rule order_trans[OF _ norm_triangle_ineq]) simp
   4.704 +            also note S(3)[OF x1']
   4.705 +            also note le_y
   4.706 +            finally show "?le x1"
   4.707 +              using False by (auto simp: algebra_simps)
   4.708 +          qed
   4.709 +        qed
   4.710 +        hence "d' \<le> y"
   4.711 +          unfolding y_def by (rule cSup_upper) simp
   4.712 +        thus False using \<open>d > 0\<close> \<open>y < b\<close>
   4.713 +          by (simp add: d'_def min_def split: if_split_asm)
   4.714 +      qed
   4.715 +    qed
   4.716      with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
   4.717        by (simp add: algebra_simps)
   4.718    } note * = this
   4.719 -  {
   4.720 +  show ?thesis
   4.721 +  proof (rule field_le_epsilon)
   4.722      fix e::real assume "e > 0"
   4.723 -    hence "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
   4.724 +    then show "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
   4.725        using *[of "e / (b - a + 1)"] \<open>a < b\<close> by simp
   4.726 -  } thus ?thesis
   4.727 -    by (rule field_le_epsilon)
   4.728 +  qed
   4.729  qed
   4.730  
   4.731  lemma differentiable_bound:
   4.732    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   4.733 -  assumes "convex s"
   4.734 -    and "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)"
   4.735 -    and "\<forall>x\<in>s. onorm (f' x) \<le> B"
   4.736 -    and x: "x \<in> s"
   4.737 -    and y: "y \<in> s"
   4.738 +  assumes "convex S"
   4.739 +    and derf: "\<And>x. x\<in>S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
   4.740 +    and B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x) \<le> B"
   4.741 +    and x: "x \<in> S"
   4.742 +    and y: "y \<in> S"
   4.743    shows "norm (f x - f y) \<le> B * norm (x - y)"
   4.744  proof -
   4.745    let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
   4.746    let ?\<phi> = "\<lambda>h. h * B * norm (x - y)"
   4.747 -  have *: "\<And>u. u\<in>{0..1} \<Longrightarrow> x + u *\<^sub>R (y - x) \<in> s"
   4.748 -    using assms(1)[unfolded convex_alt,rule_format,OF x y]
   4.749 -    unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
   4.750 -    by (auto simp add: algebra_simps)
   4.751 -  have 0: "continuous_on (?p ` {0..1}) f"
   4.752 -    using *
   4.753 +  have *: "x + u *\<^sub>R (y - x) \<in> S" if "u \<in> {0..1}" for u
   4.754 +  proof -
   4.755 +    have "u *\<^sub>R y = u *\<^sub>R (y - x) + u *\<^sub>R x"
   4.756 +      by (simp add: scale_right_diff_distrib)
   4.757 +    then show "x + u *\<^sub>R (y - x) \<in> S"
   4.758 +      using that \<open>convex S\<close> unfolding convex_alt by (metis (no_types) atLeastAtMost_iff linordered_field_class.sign_simps(2) pth_c(3) scaleR_collapse x y)
   4.759 +  qed
   4.760 +  have "\<And>z. z \<in> (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1} \<Longrightarrow>
   4.761 +          (f has_derivative f' z) (at z within (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1})"
   4.762 +    by (auto intro: * has_derivative_within_subset [OF derf])
   4.763 +  then have "continuous_on (?p ` {0..1}) f"
   4.764      unfolding continuous_on_eq_continuous_within
   4.765 -    apply -
   4.766 -    apply rule
   4.767 -    apply (rule differentiable_imp_continuous_within)
   4.768 -    unfolding differentiable_def
   4.769 -    apply (rule_tac x="f' xa" in exI)
   4.770 -    apply (rule has_derivative_within_subset)
   4.771 -    apply (rule assms(2)[rule_format])
   4.772 -    apply auto
   4.773 -    done
   4.774 -  from * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
   4.775 -    by (intro continuous_intros 0)+
   4.776 +    by (meson has_derivative_continuous)
   4.777 +  with * have 1: "continuous_on {0 .. 1} (f \<circ> ?p)"
   4.778 +    by (intro continuous_intros)+
   4.779    {
   4.780      fix u::real assume u: "u \<in>{0 <..< 1}"
   4.781      let ?u = "?p u"
   4.782      interpret linear "(f' ?u)"
   4.783 -      using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
   4.784 +      using u by (auto intro!: has_derivative_linear derf *)
   4.785      have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
   4.786 -      apply (rule diff_chain_within)
   4.787 -      apply (rule derivative_intros)+
   4.788 -      apply (rule has_derivative_within_subset)
   4.789 -      apply (rule assms(2)[rule_format])
   4.790 -      using u *
   4.791 -      apply auto
   4.792 -      done
   4.793 +      by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto)
   4.794      hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
   4.795        by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
   4.796          scaleR has_vector_derivative_def o_def)
   4.797    } note 2 = this
   4.798 -  {
   4.799 -    have "continuous_on {0..1} ?\<phi>"
   4.800 -      by (rule continuous_intros)+
   4.801 -  } note 3 = this
   4.802 -  {
   4.803 -    fix u::real assume u: "u \<in>{0 <..< 1}"
   4.804 -    have "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)"
   4.805 -      by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
   4.806 -  } note 4 = this
   4.807 +  have 3: "continuous_on {0..1} ?\<phi>"
   4.808 +    by (rule continuous_intros)+
   4.809 +  have 4: "(?\<phi> has_vector_derivative B * norm (x - y)) (at u)" for u
   4.810 +    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
   4.811    {
   4.812      fix u::real assume u: "u \<in>{0 <..< 1}"
   4.813      let ?u = "?p u"
   4.814      interpret bounded_linear "(f' ?u)"
   4.815 -      using u by (auto intro!: has_derivative_bounded_linear assms(2)[rule_format] *)
   4.816 +      using u by (auto intro!: has_derivative_bounded_linear derf *)
   4.817      have "norm (f' ?u (y - x)) \<le> onorm (f' ?u) * norm (y - x)"
   4.818        by (rule onorm) (rule bounded_linear)
   4.819      also have "onorm (f' ?u) \<le> B"
   4.820 @@ -1083,7 +985,7 @@
   4.821    fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   4.822    assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R a \<in> G"
   4.823    assumes f': "\<And>x. x \<in> G \<Longrightarrow> (f has_derivative f' x) (at x within G)"
   4.824 -  assumes B: "\<forall>x\<in>{0..1}. onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
   4.825 +  assumes B: "\<And>x. x \<in> {0..1} \<Longrightarrow> onorm (f' (x0 + x *\<^sub>R a)) \<le> B"
   4.826    shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
   4.827  proof -
   4.828    let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
   4.829 @@ -1095,14 +997,14 @@
   4.830    ultimately show ?thesis
   4.831      using has_derivative_subset[OF f' \<open>?G \<subseteq> G\<close>] B
   4.832        differentiable_bound[of "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}" f f' B "x0 + a" x0]
   4.833 -    by (auto simp: ac_simps)
   4.834 +    by (force simp: ac_simps)
   4.835  qed
   4.836  
   4.837  lemma differentiable_bound_linearization:
   4.838    fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   4.839 -  assumes "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
   4.840 +  assumes S: "\<And>t. t \<in> {0..1} \<Longrightarrow> a + t *\<^sub>R (b - a) \<in> S"
   4.841    assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
   4.842 -  assumes B: "\<forall>x\<in>S. onorm (f' x - f' x0) \<le> B"
   4.843 +  assumes B: "\<And>x. x \<in> S \<Longrightarrow> onorm (f' x - f' x0) \<le> B"
   4.844    assumes "x0 \<in> S"
   4.845    shows "norm (f b - f a - f' x0 (b - a)) \<le> norm (b - a) * B"
   4.846  proof -
   4.847 @@ -1111,9 +1013,9 @@
   4.848      unfolding g_def using assms
   4.849      by (auto intro!: derivative_eq_intros
   4.850        bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f'])
   4.851 -  from B have B: "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
   4.852 -     using assms by (auto simp: fun_diff_def)
   4.853 -  from differentiable_bound_segment[OF assms(1) g B] \<open>x0 \<in> S\<close>
   4.854 +  from B have "\<forall>x\<in>{0..1}. onorm (\<lambda>i. f' (a + x *\<^sub>R (b - a)) i - f' x0 i) \<le> B"
   4.855 +    using assms by (auto simp: fun_diff_def)
   4.856 +  with differentiable_bound_segment[OF S g] \<open>x0 \<in> S\<close>
   4.857    show ?thesis
   4.858      by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
   4.859  qed
   4.860 @@ -1122,7 +1024,7 @@
   4.861    fixes f::"real \<Rightarrow> 'b::real_normed_vector"
   4.862    assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
   4.863    assumes "closed_segment a b \<subseteq> S"
   4.864 -  assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
   4.865 +  assumes B: "\<And>x. x \<in> S \<Longrightarrow> norm (f' x - f' x0) \<le> B"
   4.866    assumes "x0 \<in> S"
   4.867    shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
   4.868    using assms
   4.869 @@ -1346,20 +1248,14 @@
   4.870      and "x \<in> S"
   4.871      and fx: "f x \<in> interior (f ` S)"
   4.872      and "continuous_on S f"
   4.873 -    and "\<And>y. y \<in> S \<Longrightarrow> g (f y) = y"
   4.874 +    and gf: "\<And>y. y \<in> S \<Longrightarrow> g (f y) = y"
   4.875      and "(f has_derivative f') (at x)"
   4.876      and "bounded_linear g'"
   4.877      and "g' \<circ> f' = id"
   4.878    shows "(g has_derivative g') (at (f x))"
   4.879  proof -
   4.880 -  {
   4.881 -    fix y
   4.882 -    assume "y \<in> interior (f ` S)"
   4.883 -    then obtain x where "x \<in> S" and *: "y = f x"
   4.884 -      by (meson imageE interior_subset subsetCE)
   4.885 -    have "f (g y) = y"
   4.886 -      unfolding * and assms(5)[rule_format,OF \<open>x\<in>S\<close>] ..
   4.887 -  } note * = this
   4.888 +  have *: "\<And>y. y \<in> interior (f ` S) \<Longrightarrow> f (g y) = y"
   4.889 +    by (metis gf image_iff interior_subset subsetCE)
   4.890    show ?thesis
   4.891      apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"])
   4.892      apply (rule continuous_on_interior[OF _ fx])
   4.893 @@ -1386,8 +1282,8 @@
   4.894    show ?thesis
   4.895      unfolding *
   4.896      apply (rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
   4.897 -    apply (rule continuous_intros assms)+
   4.898 -    using assms(4-6)
   4.899 +    apply (intro continuous_intros)
   4.900 +    using assms
   4.901      apply auto
   4.902      done
   4.903  qed
   4.904 @@ -1411,34 +1307,28 @@
   4.905  lemma sussmann_open_mapping:
   4.906    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
   4.907    assumes "open S"
   4.908 -    and "continuous_on S f"
   4.909 +    and contf: "continuous_on S f"
   4.910      and "x \<in> S"
   4.911 -    and "(f has_derivative f') (at x)"
   4.912 +    and derf: "(f has_derivative f') (at x)"
   4.913      and "bounded_linear g'" "f' \<circ> g' = id"
   4.914      and "T \<subseteq> S"
   4.915 -    and "x \<in> interior T"
   4.916 +    and x: "x \<in> interior T"
   4.917    shows "f x \<in> interior (f ` T)"
   4.918  proof -
   4.919    interpret f': bounded_linear f'
   4.920 -    using assms
   4.921 -    unfolding has_derivative_def
   4.922 -    by auto
   4.923 +    using assms unfolding has_derivative_def by auto
   4.924    interpret g': bounded_linear g'
   4.925 -    using assms
   4.926 -    by auto
   4.927 +    using assms by auto
   4.928    obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
   4.929      using bounded_linear.pos_bounded[OF assms(5)] by blast
   4.930    hence *: "1 / (2 * B) > 0" by auto
   4.931    obtain e0 where e0:
   4.932        "0 < e0"
   4.933        "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
   4.934 -    using assms(4)
   4.935 -    unfolding has_derivative_at_alt
   4.936 +    using derf unfolding has_derivative_at_alt
   4.937      using * by blast
   4.938    obtain e1 where e1: "0 < e1" "cball x e1 \<subseteq> T"
   4.939 -    using assms(8)
   4.940 -    unfolding mem_interior_cball
   4.941 -    by blast
   4.942 +    using mem_interior_cball x by blast
   4.943    have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
   4.944    obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
   4.945      using real_lbound_gt_zero[OF *] by blast
   4.946 @@ -1449,83 +1339,59 @@
   4.947        have "dist x z = norm (g' (f x) - g' y)"
   4.948          unfolding as(2) and dist_norm by auto
   4.949        also have "\<dots> \<le> norm (f x - y) * B"
   4.950 -        unfolding g'.diff[symmetric]
   4.951 -        using B
   4.952 -        by auto
   4.953 +        by (metis B(2) g'.diff)
   4.954        also have "\<dots> \<le> e * B"
   4.955 -        using as(1)[unfolded mem_cball dist_norm]
   4.956 -        using B
   4.957 -        by auto
   4.958 +        by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1))
   4.959        also have "\<dots> \<le> e1"
   4.960 -        using e
   4.961 -        unfolding less_divide_eq
   4.962 -        using B
   4.963 -        by auto
   4.964 +        using B(1) e(3) pos_less_divide_eq by fastforce
   4.965        finally have "z \<in> cball x e1"
   4.966 -        unfolding mem_cball
   4.967          by force
   4.968        then show "z \<in> S"
   4.969          using e1 assms(7) by auto
   4.970      qed
   4.971      show "continuous_on (cball (f x) e) (\<lambda>y. f (x + g' (y - f x)))"
   4.972        unfolding g'.diff
   4.973 -      apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
   4.974 -       apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
   4.975 -      apply (rule continuous_on_subset[OF assms(2)])
   4.976 -      using z
   4.977 -      by blast
   4.978 +    proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f])
   4.979 +      show "continuous_on ((\<lambda>y. x + (g' y - g' (f x))) ` cball (f x) e) f"
   4.980 +        by (rule continuous_on_subset[OF contf]) (use z in blast)
   4.981 +      show "continuous_on (cball (f x) e) (\<lambda>y. x + (g' y - g' (f x)))"
   4.982 +        by (intro continuous_intros linear_continuous_on[OF \<open>bounded_linear g'\<close>])
   4.983 +    qed
   4.984    next
   4.985      fix y z
   4.986 -    assume as: "y \<in> cball (f x) (e / 2)" "z \<in> cball (f x) e"
   4.987 +    assume y: "y \<in> cball (f x) (e / 2)" and z: "z \<in> cball (f x) e"
   4.988      have "norm (g' (z - f x)) \<le> norm (z - f x) * B"
   4.989        using B by auto
   4.990      also have "\<dots> \<le> e * B"
   4.991 -      apply (rule mult_right_mono)
   4.992 -      using as(2)[unfolded mem_cball dist_norm] and B
   4.993 -      unfolding norm_minus_commute
   4.994 -       apply auto
   4.995 -      done
   4.996 +      by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1)
   4.997      also have "\<dots> < e0"
   4.998 -      using e and B
   4.999 -      unfolding less_divide_eq
  4.1000 -      by auto
  4.1001 +      using B(1) e(2) pos_less_divide_eq by blast
  4.1002      finally have *: "norm (x + g' (z - f x) - x) < e0"
  4.1003        by auto
  4.1004      have **: "f x + f' (x + g' (z - f x) - x) = z"
  4.1005        using assms(6)[unfolded o_def id_def,THEN cong]
  4.1006        by auto
  4.1007      have "norm (f x - (y + (z - f (x + g' (z - f x))))) \<le>
  4.1008 -        norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
  4.1009 +          norm (f (x + g' (z - f x)) - z) + norm (f x - y)"
  4.1010        using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"]
  4.1011        by (auto simp add: algebra_simps)
  4.1012      also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)"
  4.1013        using e0(2)[rule_format, OF *]
  4.1014        by (simp only: algebra_simps **) auto
  4.1015      also have "\<dots> \<le> 1 / (B * 2) * norm (g' (z - f x)) + e/2"
  4.1016 -      using as(1)[unfolded mem_cball dist_norm]
  4.1017 -      by auto
  4.1018 +      using y by (auto simp: dist_norm)
  4.1019      also have "\<dots> \<le> 1 / (B * 2) * B * norm (z - f x) + e/2"
  4.1020 -      using * and B
  4.1021 -      by (auto simp add: field_simps)
  4.1022 +      using * B by (auto simp add: field_simps)
  4.1023      also have "\<dots> \<le> 1 / 2 * norm (z - f x) + e/2"
  4.1024        by auto
  4.1025      also have "\<dots> \<le> e/2 + e/2"
  4.1026 -      apply (rule add_right_mono)
  4.1027 -      using as(2)[unfolded mem_cball dist_norm]
  4.1028 -      unfolding norm_minus_commute
  4.1029 -      apply auto
  4.1030 -      done
  4.1031 +      using B(1) \<open>norm (z - f x) * B \<le> e * B\<close> by auto
  4.1032      finally show "y + (z - f (x + g' (z - f x))) \<in> cball (f x) e"
  4.1033 -      unfolding mem_cball dist_norm
  4.1034 -      by auto
  4.1035 +      by (auto simp: dist_norm)
  4.1036    qed (use e that in auto) 
  4.1037    show ?thesis
  4.1038      unfolding mem_interior
  4.1039 -    apply (rule_tac x="e/2" in exI)
  4.1040 -    apply rule
  4.1041 -    apply (rule divide_pos_pos)
  4.1042 -    prefer 3
  4.1043 -  proof
  4.1044 +  proof (intro exI conjI subsetI)
  4.1045      fix y
  4.1046      assume "y \<in> ball (f x) (e / 2)"
  4.1047      then have *: "y \<in> cball (f x) (e / 2)"
  4.1048 @@ -1536,23 +1402,14 @@
  4.1049        using B
  4.1050        by (auto simp add: field_simps)
  4.1051      also have "\<dots> \<le> e * B"
  4.1052 -      apply (rule mult_right_mono)
  4.1053 -      using z(1)
  4.1054 -      unfolding mem_cball dist_norm norm_minus_commute
  4.1055 -      using B
  4.1056 -      apply auto
  4.1057 -      done
  4.1058 +      by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1))
  4.1059      also have "\<dots> \<le> e1"
  4.1060        using e B unfolding less_divide_eq by auto
  4.1061      finally have "x + g'(z - f x) \<in> T"
  4.1062 -      apply -
  4.1063 -      apply (rule e1(2)[unfolded subset_eq,rule_format])
  4.1064 -      unfolding mem_cball dist_norm
  4.1065 -      apply auto
  4.1066 -      done
  4.1067 +      by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq)
  4.1068      then show "y \<in> f ` T"
  4.1069        using z by auto
  4.1070 -  qed (insert e, auto)
  4.1071 +  qed (use e in auto)
  4.1072  qed
  4.1073  
  4.1074  text \<open>Hence the following eccentric variant of the inverse function theorem.
  4.1075 @@ -1562,30 +1419,25 @@
  4.1076  
  4.1077  lemma has_derivative_inverse_strong:
  4.1078    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  4.1079 -  assumes "open s"
  4.1080 -    and "x \<in> s"
  4.1081 -    and "continuous_on s f"
  4.1082 -    and "\<forall>x\<in>s. g (f x) = x"
  4.1083 -    and "(f has_derivative f') (at x)"
  4.1084 -    and "f' \<circ> g' = id"
  4.1085 +  assumes "open S"
  4.1086 +    and "x \<in> S"
  4.1087 +    and contf: "continuous_on S f"
  4.1088 +    and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
  4.1089 +    and derf: "(f has_derivative f') (at x)"
  4.1090 +    and id: "f' \<circ> g' = id"
  4.1091    shows "(g has_derivative g') (at (f x))"
  4.1092  proof -
  4.1093    have linf: "bounded_linear f'"
  4.1094 -    using assms(5) unfolding has_derivative_def by auto
  4.1095 +    using derf unfolding has_derivative_def by auto
  4.1096    then have ling: "bounded_linear g'"
  4.1097      unfolding linear_conv_bounded_linear[symmetric]
  4.1098 -    apply -
  4.1099 -    apply (rule right_inverse_linear)
  4.1100 -    using assms(6)
  4.1101 -    apply auto
  4.1102 -    done
  4.1103 +    using id right_inverse_linear by blast
  4.1104    moreover have "g' \<circ> f' = id"
  4.1105 -    using assms(6) linf ling
  4.1106 +    using id linf ling
  4.1107      unfolding linear_conv_bounded_linear[symmetric]
  4.1108      using linear_inverse_left
  4.1109      by auto
  4.1110 -  moreover have *:"\<forall>t\<subseteq>s. x \<in> interior t \<longrightarrow> f x \<in> interior (f ` t)"
  4.1111 -    apply clarify
  4.1112 +  moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
  4.1113      apply (rule sussmann_open_mapping)
  4.1114      apply (rule assms ling)+
  4.1115      apply auto
  4.1116 @@ -1595,44 +1447,30 @@
  4.1117    proof (rule, rule)
  4.1118      fix e :: real
  4.1119      assume "e > 0"
  4.1120 -    then have "f x \<in> interior (f ` (ball x e \<inter> s))"
  4.1121 -      using *[rule_format,of "ball x e \<inter> s"] \<open>x \<in> s\<close>
  4.1122 +    then have "f x \<in> interior (f ` (ball x e \<inter> S))"
  4.1123 +      using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
  4.1124        by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
  4.1125 -    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> s)"
  4.1126 +    then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
  4.1127        unfolding mem_interior by blast
  4.1128      show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
  4.1129 -      apply (rule_tac x=d in exI)
  4.1130 -      apply rule
  4.1131 -      apply (rule d(1))
  4.1132 -      apply rule
  4.1133 -      apply rule
  4.1134 -    proof -
  4.1135 +    proof (intro exI allI impI conjI)
  4.1136        fix y
  4.1137        assume "0 < dist y (f x) \<and> dist y (f x) < d"
  4.1138 -      then have "g y \<in> g ` f ` (ball x e \<inter> s)"
  4.1139 -        using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
  4.1140 -        by (auto simp add: dist_commute)
  4.1141 -      then have "g y \<in> ball x e \<inter> s"
  4.1142 -        using assms(4) by auto
  4.1143 +      then have "g y \<in> g ` f ` (ball x e \<inter> S)"
  4.1144 +        by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
  4.1145        then show "dist (g y) (g (f x)) < e"
  4.1146 -        using assms(4)[rule_format,OF \<open>x \<in> s\<close>]
  4.1147 -        by (auto simp add: dist_commute)
  4.1148 -    qed
  4.1149 +        using gf[OF \<open>x \<in> S\<close>]
  4.1150 +        by (simp add: assms(4) dist_commute image_iff)
  4.1151 +    qed (use d in auto)
  4.1152    qed
  4.1153 -  moreover have "f x \<in> interior (f ` s)"
  4.1154 +  moreover have "f x \<in> interior (f ` S)"
  4.1155      apply (rule sussmann_open_mapping)
  4.1156      apply (rule assms ling)+
  4.1157 -    using interior_open[OF assms(1)] and \<open>x \<in> s\<close>
  4.1158 +    using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
  4.1159      apply auto
  4.1160      done
  4.1161 -  moreover have "f (g y) = y" if "y \<in> interior (f ` s)" for y
  4.1162 -  proof -
  4.1163 -    from that have "y \<in> f ` s"
  4.1164 -      using interior_subset by auto
  4.1165 -    then obtain z where "z \<in> s" "y = f z" unfolding image_iff ..
  4.1166 -    then show ?thesis
  4.1167 -      using assms(4) by auto
  4.1168 -  qed
  4.1169 +  moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
  4.1170 +    by (metis gf imageE interiorE set_mp that)
  4.1171    ultimately show ?thesis using assms
  4.1172      by (metis has_derivative_inverse_basic_x open_interior)
  4.1173  qed
  4.1174 @@ -1641,10 +1479,10 @@
  4.1175  
  4.1176  lemma has_derivative_inverse_strong_x:
  4.1177    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
  4.1178 -  assumes "open s"
  4.1179 -    and "g y \<in> s"
  4.1180 -    and "continuous_on s f"
  4.1181 -    and "\<forall>x\<in>s. g (f x) = x"
  4.1182 +  assumes "open S"
  4.1183 +    and "g y \<in> S"
  4.1184 +    and "continuous_on S f"
  4.1185 +    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
  4.1186      and "(f has_derivative f') (at (g y))"
  4.1187      and "f' \<circ> g' = id"
  4.1188      and "f (g y) = y"
  4.1189 @@ -1657,21 +1495,18 @@
  4.1190  
  4.1191  lemma has_derivative_inverse_on:
  4.1192    fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
  4.1193 -  assumes "open s"
  4.1194 -    and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
  4.1195 -    and "\<forall>x\<in>s. g (f x) = x"
  4.1196 +  assumes "open S"
  4.1197 +    and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
  4.1198 +    and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
  4.1199      and "f' x \<circ> g' x = id"
  4.1200 -    and "x \<in> s"
  4.1201 +    and "x \<in> S"
  4.1202    shows "(g has_derivative g'(x)) (at (f x))"
  4.1203 -  apply (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
  4.1204 -  apply (rule assms)+
  4.1205 -  unfolding continuous_on_eq_continuous_at[OF assms(1)]
  4.1206 -  apply rule
  4.1207 -  apply (rule differentiable_imp_continuous_within)
  4.1208 -  unfolding differentiable_def
  4.1209 -  using assms
  4.1210 -  apply auto
  4.1211 -  done
  4.1212 +proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
  4.1213 +  show "continuous_on S f"
  4.1214 +  unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
  4.1215 +  using derf has_derivative_continuous by blast
  4.1216 +qed (use assms in auto)
  4.1217 +
  4.1218  
  4.1219  text \<open>Invertible derivative continous at a point implies local
  4.1220  injectivity. It's only for this we need continuity of the derivative,
  4.1221 @@ -1681,13 +1516,13 @@
  4.1222  
  4.1223  proposition has_derivative_locally_injective:
  4.1224    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  4.1225 -  assumes "a \<in> s"
  4.1226 -      and "open s"
  4.1227 +  assumes "a \<in> S"
  4.1228 +      and "open S"
  4.1229        and bling: "bounded_linear g'"
  4.1230        and "g' \<circ> f' a = id"
  4.1231 -      and derf: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
  4.1232 +      and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x)"
  4.1233        and "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
  4.1234 -  obtains r where "r > 0" "ball a r \<subseteq> s" "inj_on f (ball a r)"
  4.1235 +  obtains r where "r > 0" "ball a r \<subseteq> S" "inj_on f (ball a r)"
  4.1236  proof -
  4.1237    interpret bounded_linear g'
  4.1238      using assms by auto
  4.1239 @@ -1704,21 +1539,17 @@
  4.1240        "0 < d1"
  4.1241        "\<And>x. dist a x < d1 \<Longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < k"
  4.1242      using assms(6) * by blast
  4.1243 -  from \<open>open s\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
  4.1244 -    using \<open>a\<in>s\<close> ..
  4.1245 -  obtain d2 where "d2 > 0" "ball a d2 \<subseteq> s"
  4.1246 -    using assms(2,1) ..
  4.1247 -  obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> s"
  4.1248 -    using assms(2)
  4.1249 -    unfolding open_contains_ball
  4.1250 -    using \<open>a\<in>s\<close> by blast
  4.1251 +  from \<open>open S\<close> obtain d2 where "d2 > 0" "ball a d2 \<subseteq> S"
  4.1252 +    using \<open>a\<in>S\<close> ..
  4.1253 +  obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> S"
  4.1254 +    using \<open>0 < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by blast
  4.1255    obtain d where d: "0 < d" "d < d1" "d < d2"
  4.1256      using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
  4.1257    show ?thesis
  4.1258    proof
  4.1259      show "0 < d" by (fact d)
  4.1260 -    show "ball a d \<subseteq> s"
  4.1261 -      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> s\<close> by auto
  4.1262 +    show "ball a d \<subseteq> S"
  4.1263 +      using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by auto
  4.1264      show "inj_on f (ball a d)"
  4.1265      unfolding inj_on_def
  4.1266      proof (intro strip)
  4.1267 @@ -1726,55 +1557,36 @@
  4.1268        assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y"
  4.1269        define ph where [abs_def]: "ph w = w - g' (f w - f x)" for w
  4.1270        have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
  4.1271 -        unfolding ph_def o_def
  4.1272 -        unfolding diff
  4.1273 -        using f'g'
  4.1274 -        by (auto simp: algebra_simps)
  4.1275 +        unfolding ph_def o_def  by (simp add: diff f'g')
  4.1276        have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)"
  4.1277 -        apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
  4.1278 -        apply (rule_tac[!] ballI)
  4.1279 -      proof -
  4.1280 +      proof (rule differentiable_bound[OF convex_ball _ _ as(1-2)])
  4.1281          fix u
  4.1282          assume u: "u \<in> ball a d"
  4.1283 -        then have "u \<in> s"
  4.1284 +        then have "u \<in> S"
  4.1285            using d d2 by auto
  4.1286          have *: "(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)"
  4.1287            unfolding o_def and diff
  4.1288            using f'g' by auto
  4.1289          have blin: "bounded_linear (f' a)"
  4.1290 -          using \<open>a \<in> s\<close> derf by blast
  4.1291 +          using \<open>a \<in> S\<close> derf by blast
  4.1292          show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
  4.1293            unfolding ph' * comp_def
  4.1294 -          by (rule \<open>u \<in> s\<close> derivative_eq_intros has_derivative_at_withinI [OF derf] bounded_linear.has_derivative [OF blin]  bounded_linear.has_derivative [OF bling] |simp)+
  4.1295 +          by (rule \<open>u \<in> S\<close> derivative_eq_intros has_derivative_at_withinI [OF derf] bounded_linear.has_derivative [OF blin]  bounded_linear.has_derivative [OF bling] |simp)+
  4.1296          have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
  4.1297 -          apply (rule_tac[!] bounded_linear_sub)
  4.1298 -          apply (rule_tac[!] has_derivative_bounded_linear)
  4.1299 -          using assms(5) \<open>u \<in> s\<close> \<open>a \<in> s\<close>
  4.1300 -          apply auto
  4.1301 -          done
  4.1302 -        have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
  4.1303 -          unfolding *
  4.1304 -          apply (rule onorm_compose)
  4.1305 -          apply (rule assms(3) **)+
  4.1306 -          done
  4.1307 +          using \<open>u \<in> S\<close> blin bounded_linear_sub derf by auto
  4.1308 +        then have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)"
  4.1309 +          by (simp add: "*" bounded_linear_axioms onorm_compose)
  4.1310          also have "\<dots> \<le> onorm g' * k"
  4.1311            apply (rule mult_left_mono)
  4.1312            using d1(2)[of u]
  4.1313 -          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
  4.1314 -          using d and u and onorm_pos_le[OF assms(3)]
  4.1315 -          apply (auto simp: algebra_simps)
  4.1316 +          using onorm_neg[where f="\<lambda>x. f' u x - f' a x"] d u onorm_pos_le[OF bling] apply (auto simp: algebra_simps)
  4.1317            done
  4.1318          also have "\<dots> \<le> 1 / 2"
  4.1319            unfolding k_def by auto
  4.1320          finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" .
  4.1321        qed
  4.1322        moreover have "norm (ph y - ph x) = norm (y - x)"
  4.1323 -        apply (rule arg_cong[where f=norm])
  4.1324 -        unfolding ph_def
  4.1325 -        using diff
  4.1326 -        unfolding as
  4.1327 -        apply auto
  4.1328 -        done
  4.1329 +        by (simp add: as(3) ph_def)
  4.1330        ultimately show "x = y"
  4.1331          unfolding norm_minus_commute by auto
  4.1332      qed
  4.1333 @@ -1786,32 +1598,28 @@
  4.1334  
  4.1335  lemma has_derivative_sequence_lipschitz_lemma:
  4.1336    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  4.1337 -  assumes "convex s"
  4.1338 -    and "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
  4.1339 -    and "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1340 +  assumes "convex S"
  4.1341 +    and derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
  4.1342 +    and nle: "\<And>n x h. \<lbrakk>n\<ge>N; x \<in> S\<rbrakk> \<Longrightarrow> norm (f' n x h - g' x h) \<le> e * norm h"
  4.1343      and "0 \<le> e"
  4.1344 -  shows "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
  4.1345 -proof rule+
  4.1346 +  shows "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
  4.1347 +proof clarify
  4.1348    fix m n x y
  4.1349 -  assume as: "N \<le> m" "N \<le> n" "x \<in> s" "y \<in> s"
  4.1350 +  assume as: "N \<le> m" "N \<le> n" "x \<in> S" "y \<in> S"
  4.1351    show "norm ((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm (x - y)"
  4.1352 -    apply (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)])
  4.1353 -    apply (rule_tac[!] ballI)
  4.1354 -  proof -
  4.1355 +  proof (rule differentiable_bound[where f'="\<lambda>x h. f' m x h - f' n x h", OF \<open>convex S\<close> _ _ as(3-4)])
  4.1356      fix x
  4.1357 -    assume "x \<in> s"
  4.1358 -    show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
  4.1359 -      by (rule derivative_intros assms(2)[rule_format] \<open>x\<in>s\<close>)+
  4.1360 +    assume "x \<in> S"
  4.1361 +    show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within S)"
  4.1362 +      by (rule derivative_intros derf \<open>x\<in>S\<close>)+
  4.1363      show "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e"
  4.1364      proof (rule onorm_bound)
  4.1365        fix h
  4.1366        have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
  4.1367          using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"]
  4.1368 -        unfolding norm_minus_commute
  4.1369 -        by (auto simp add: algebra_simps)
  4.1370 +        by (auto simp add: algebra_simps norm_minus_commute)
  4.1371        also have "\<dots> \<le> e * norm h + e * norm h"
  4.1372 -        using assms(3)[rule_format,OF \<open>N \<le> m\<close> \<open>x \<in> s\<close>, of h]
  4.1373 -        using assms(3)[rule_format,OF \<open>N \<le> n\<close> \<open>x \<in> s\<close>, of h]
  4.1374 +        using nle[OF \<open>N \<le> m\<close> \<open>x \<in> S\<close>, of h] nle[OF \<open>N \<le> n\<close> \<open>x \<in> S\<close>, of h]
  4.1375          by (auto simp add: field_simps)
  4.1376        finally show "norm (f' m x h - f' n x h) \<le> 2 * e * norm h"
  4.1377          by auto
  4.1378 @@ -1823,18 +1631,20 @@
  4.1379    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  4.1380    assumes "convex S"
  4.1381      and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
  4.1382 -    and "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1383 +    and nle: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1384      and "e > 0"
  4.1385    shows "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S.
  4.1386      norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
  4.1387  proof -
  4.1388 -  have *: "2 * (1/2* e) = e" "1/2 * e >0"
  4.1389 -    using \<open>e>0\<close> by auto
  4.1390 -  obtain N where "\<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
  4.1391 -    using assms(3) *(2) by blast
  4.1392 +  have *: "2 * (e/2) = e"
  4.1393 +    using \<open>e > 0\<close> by auto
  4.1394 +  obtain N where "\<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> (e/2) * norm h"
  4.1395 +    using nle \<open>e > 0\<close>
  4.1396 +    unfolding eventually_sequentially
  4.1397 +    by (metis less_divide_eq_numeral1(1) mult_zero_left)
  4.1398    then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
  4.1399      apply (rule_tac x=N in exI)
  4.1400 -    apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
  4.1401 +    apply (rule has_derivative_sequence_lipschitz_lemma[where e="e/2", unfolded *])
  4.1402      using assms \<open>e > 0\<close>
  4.1403      apply auto
  4.1404      done
  4.1405 @@ -1843,60 +1653,51 @@
  4.1406  lemma has_derivative_sequence:
  4.1407    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
  4.1408    assumes "convex S"
  4.1409 -    and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
  4.1410 -    and "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1411 +    and derf: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
  4.1412 +    and nle: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1413      and "x0 \<in> S"
  4.1414 -    and "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
  4.1415 -  shows "\<exists>g. \<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g'(x)) (at x within S)"
  4.1416 +    and lim: "((\<lambda>n. f n x0) \<longlongrightarrow> l) sequentially"
  4.1417 +  shows "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) \<longlonglongrightarrow> g x \<and> (g has_derivative g'(x)) (at x within S)"
  4.1418  proof -
  4.1419    have lem1: "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S.
  4.1420        norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
  4.1421      using assms(1,2,3) by (rule has_derivative_sequence_Lipschitz)
  4.1422    have "\<exists>g. \<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
  4.1423 -    apply (rule bchoice)
  4.1424 -    unfolding convergent_eq_Cauchy
  4.1425 -  proof
  4.1426 +  proof (intro ballI bchoice)
  4.1427      fix x
  4.1428      assume "x \<in> S"
  4.1429 -    show "Cauchy (\<lambda>n. f n x)"
  4.1430 +    show "\<exists>y. (\<lambda>n. f n x) \<longlonglongrightarrow> y"
  4.1431 +    unfolding convergent_eq_Cauchy
  4.1432      proof (cases "x = x0")
  4.1433        case True
  4.1434 -      then show ?thesis
  4.1435 -        using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
  4.1436 +      then show "Cauchy (\<lambda>n. f n x)"
  4.1437 +        using LIMSEQ_imp_Cauchy[OF lim] by auto
  4.1438      next
  4.1439        case False
  4.1440 -      show ?thesis
  4.1441 +      show "Cauchy (\<lambda>n. f n x)"
  4.1442          unfolding Cauchy_def
  4.1443        proof (intro allI impI)
  4.1444          fix e :: real
  4.1445          assume "e > 0"
  4.1446          hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
  4.1447          obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2"
  4.1448 -          using LIMSEQ_imp_Cauchy[OF assms(5)]
  4.1449 -          unfolding Cauchy_def
  4.1450 -          using *(1) by blast
  4.1451 +          using LIMSEQ_imp_Cauchy[OF lim] * unfolding Cauchy_def by blast
  4.1452          obtain N where N:
  4.1453            "\<forall>m\<ge>N. \<forall>n\<ge>N.
  4.1454 -            \<forall>xa\<in>S. \<forall>y\<in>S. norm (f m xa - f n xa - (f m y - f n y)) \<le>
  4.1455 -              e / 2 / norm (x - x0) * norm (xa - y)"
  4.1456 +            \<forall>u\<in>S. \<forall>y\<in>S. norm (f m u - f n u - (f m y - f n y)) \<le>
  4.1457 +              e / 2 / norm (x - x0) * norm (u - y)"
  4.1458          using lem1 *(2) by blast
  4.1459          show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
  4.1460          proof (intro exI allI impI)
  4.1461            fix m n
  4.1462            assume as: "max M N \<le>m" "max M N\<le>n"
  4.1463 -          have "dist (f m x) (f n x) \<le>
  4.1464 -              norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
  4.1465 +          have "dist (f m x) (f n x) \<le> norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
  4.1466              unfolding dist_norm
  4.1467              by (rule norm_triangle_sub)
  4.1468            also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2"
  4.1469 -            using N[rule_format,OF _ _ \<open>x\<in>S\<close> \<open>x0\<in>S\<close>, of m n] and as and False
  4.1470 -            by auto
  4.1471 +            using N \<open>x\<in>S\<close> \<open>x0\<in>S\<close> as False by fastforce
  4.1472            also have "\<dots> < e / 2 + e / 2"
  4.1473 -            apply (rule add_strict_right_mono)
  4.1474 -            using as and M[rule_format]
  4.1475 -            unfolding dist_norm
  4.1476 -            apply auto
  4.1477 -            done
  4.1478 +            by (rule add_strict_right_mono) (use as M in \<open>auto simp: dist_norm\<close>)
  4.1479            finally show "dist (f m x) (f n x) < e"
  4.1480              by auto
  4.1481          qed
  4.1482 @@ -1904,16 +1705,13 @@
  4.1483      qed
  4.1484    qed
  4.1485    then obtain g where g: "\<forall>x\<in>S. (\<lambda>n. f n x) \<longlonglongrightarrow> g x" ..
  4.1486 -  have lem2: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)"
  4.1487 -  proof (rule, rule)
  4.1488 -    fix e :: real
  4.1489 -    assume *: "e > 0"
  4.1490 +  have lem2: "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm ((f n x - f n y) - (g x - g y)) \<le> e * norm (x - y)" if "e > 0" for e
  4.1491 +  proof -
  4.1492      obtain N where
  4.1493        N: "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
  4.1494 -      using lem1 * by blast
  4.1495 +      using lem1 \<open>e > 0\<close> by blast
  4.1496      show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>y\<in>S. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
  4.1497 -      apply (rule_tac x=N in exI)
  4.1498 -    proof rule+
  4.1499 +    proof (intro exI ballI allI impI)
  4.1500        fix n x y
  4.1501        assume as: "N \<le> n" "x \<in> S" "y \<in> S"
  4.1502        have "((\<lambda>m. norm (f n x - f n y - (f m x - f m y))) \<longlongrightarrow> norm (f n x - f n y - (g x - g y))) sequentially"
  4.1503 @@ -1924,8 +1722,7 @@
  4.1504          fix m
  4.1505          assume "N \<le> m"
  4.1506          then show "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
  4.1507 -          using N[rule_format, of n m x y] and as
  4.1508 -          by (auto simp add: algebra_simps)
  4.1509 +          using N as by (auto simp add: algebra_simps)
  4.1510        qed
  4.1511        ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
  4.1512          by (simp add: tendsto_upperbound)
  4.1513 @@ -1933,31 +1730,28 @@
  4.1514    qed
  4.1515    have "\<forall>x\<in>S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within S)"
  4.1516      unfolding has_derivative_within_alt2
  4.1517 -  proof (intro ballI conjI)
  4.1518 +  proof (intro ballI conjI allI impI)
  4.1519      fix x
  4.1520      assume "x \<in> S"
  4.1521 -    then show "((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
  4.1522 +    then show "(\<lambda>n. f n x) \<longlonglongrightarrow> g x"
  4.1523        by (simp add: g)
  4.1524 -    have lem3: "\<forall>u. ((\<lambda>n. f' n x u) \<longlongrightarrow> g' x u) sequentially"
  4.1525 +    have tog': "(\<lambda>n. f' n x u) \<longlonglongrightarrow> g' x u" for u
  4.1526        unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm
  4.1527      proof (intro allI impI)
  4.1528 -      fix u
  4.1529        fix e :: real
  4.1530        assume "e > 0"
  4.1531        show "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e) sequentially"
  4.1532        proof (cases "u = 0")
  4.1533          case True
  4.1534          have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
  4.1535 -          using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> S\<close>
  4.1536 -          by (fast elim: eventually_mono)
  4.1537 +          using nle \<open>0 < e\<close> \<open>x \<in> S\<close> by (fast elim: eventually_mono)
  4.1538          then show ?thesis
  4.1539 -          using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_mono)
  4.1540 +          using \<open>u = 0\<close> \<open>0 < e\<close> by (auto elim: eventually_mono)
  4.1541        next
  4.1542          case False
  4.1543          with \<open>0 < e\<close> have "0 < e / norm u" by simp
  4.1544          then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
  4.1545 -          using assms(3)[folded eventually_sequentially] and \<open>x \<in> S\<close>
  4.1546 -          by (fast elim: eventually_mono)
  4.1547 +          using nle \<open>x \<in> S\<close> by (fast elim: eventually_mono)
  4.1548          then show ?thesis
  4.1549            using \<open>u \<noteq> 0\<close> by simp
  4.1550        qed
  4.1551 @@ -1968,23 +1762,20 @@
  4.1552        fix c :: real
  4.1553        note lin = assms(2)[rule_format,OF \<open>x\<in>S\<close>,THEN has_derivative_bounded_linear]
  4.1554        show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
  4.1555 -        apply (rule tendsto_unique[OF trivial_limit_sequentially])
  4.1556 -        apply (rule lem3[rule_format])
  4.1557 +        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
  4.1558          unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
  4.1559 -        apply (intro tendsto_intros)
  4.1560 -        apply (rule lem3[rule_format])
  4.1561 +        apply (intro tendsto_intros tog')
  4.1562          done
  4.1563        show "g' x (y + z) = g' x y + g' x z"
  4.1564 -        apply (rule tendsto_unique[OF trivial_limit_sequentially])
  4.1565 -        apply (rule lem3[rule_format])
  4.1566 +        apply (rule tendsto_unique[OF trivial_limit_sequentially tog'])
  4.1567          unfolding lin[THEN bounded_linear.linear, THEN linear_add]
  4.1568          apply (rule tendsto_add)
  4.1569 -        apply (rule lem3[rule_format])+
  4.1570 +        apply (rule tog')+
  4.1571          done
  4.1572        obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
  4.1573 -        using assms(3) \<open>x \<in> S\<close> by (fast intro: zero_less_one)
  4.1574 +        using nle \<open>x \<in> S\<close> unfolding eventually_sequentially by (fast intro: zero_less_one)
  4.1575        have "bounded_linear (f' N x)"
  4.1576 -        using assms(2) \<open>x \<in> S\<close> by fast
  4.1577 +        using derf \<open>x \<in> S\<close> by fast
  4.1578        from bounded_linear.bounded [OF this]
  4.1579        obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
  4.1580        {
  4.1581 @@ -2000,20 +1791,19 @@
  4.1582        }
  4.1583        then show "\<exists>K. \<forall>h. norm (g' x h) \<le> norm h * K" by fast
  4.1584      qed
  4.1585 -    show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within S)"
  4.1586 -    proof (rule, rule)
  4.1587 -      fix e :: real
  4.1588 -      assume "e > 0"
  4.1589 -      then have *: "e / 3 > 0"
  4.1590 -        by auto
  4.1591 +    show "eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within S)"
  4.1592 +      if "e > 0" for e
  4.1593 +    proof -
  4.1594 +      have *: "e / 3 > 0"
  4.1595 +        using that by auto
  4.1596        obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
  4.1597 -        using assms(3) * by blast
  4.1598 +        using nle * unfolding eventually_sequentially by blast
  4.1599        obtain N2 where
  4.1600 -          N2: "\<forall>n\<ge>N2. \<forall>x\<in>S. \<forall>y\<in>S. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
  4.1601 +          N2[rule_format]: "\<forall>n\<ge>N2. \<forall>x\<in>S. \<forall>y\<in>S. norm (f n x - f n y - (g x - g y)) \<le> e / 3 * norm (x - y)"
  4.1602          using lem2 * by blast
  4.1603        let ?N = "max N1 N2"
  4.1604        have "eventually (\<lambda>y. norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)) (at x within S)"
  4.1605 -        using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> S\<close> and * by fast
  4.1606 +        using derf[unfolded has_derivative_within_alt2] and \<open>x \<in> S\<close> and * by fast
  4.1607        moreover have "eventually (\<lambda>y. y \<in> S) (at x within S)"
  4.1608          unfolding eventually_at by (fast intro: zero_less_one)
  4.1609        ultimately show "\<forall>\<^sub>F y in at x within S. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
  4.1610 @@ -2022,7 +1812,7 @@
  4.1611          assume "y \<in> S"
  4.1612          assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)"
  4.1613          moreover have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e / 3 * norm (y - x)"
  4.1614 -          using N2[rule_format, OF _ \<open>y \<in> S\<close> \<open>x \<in> S\<close>]
  4.1615 +          using N2[OF _ \<open>y \<in> S\<close> \<open>x \<in> S\<close>]
  4.1616            by (simp add: norm_minus_commute)
  4.1617          ultimately have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)"
  4.1618            using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"]
  4.1619 @@ -2045,7 +1835,8 @@
  4.1620    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
  4.1621    assumes "convex S"
  4.1622      and der: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
  4.1623 -    and no: "\<And>e. e > 0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1624 +    and no: "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially.
  4.1625 +       \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1626    shows "\<exists>g. \<forall>x\<in>S. (g has_derivative g' x) (at x within S)"
  4.1627  proof (cases "S = {}")
  4.1628    case False
  4.1629 @@ -2058,7 +1849,7 @@
  4.1630      apply (rule has_derivative_sequence [OF \<open>convex S\<close> _ no, of "\<lambda>n x. f n x + (f 0 a - f n a)"])
  4.1631         apply (metis assms(2) has_derivative_add_const)
  4.1632      using \<open>a \<in> S\<close> 
  4.1633 -    apply auto
  4.1634 +      apply auto
  4.1635      done
  4.1636  qed auto
  4.1637  
  4.1638 @@ -2087,14 +1878,14 @@
  4.1639      assume "e > 0"
  4.1640      obtain N where N: "inverse (real (Suc N)) < e"
  4.1641        using reals_Archimedean[OF \<open>e>0\<close>] ..
  4.1642 -    show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1643 +    show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S.  \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
  4.1644 +        unfolding eventually_sequentially
  4.1645      proof (intro exI allI ballI impI)
  4.1646        fix n x h
  4.1647        assume n: "N \<le> n" and x: "x \<in> S"
  4.1648        have *: "inverse (real (Suc n)) \<le> e"
  4.1649          apply (rule order_trans[OF _ N[THEN less_imp_le]])
  4.1650 -        using n
  4.1651 -        apply (auto simp add: field_simps)
  4.1652 +        using n apply (auto simp add: field_simps)
  4.1653          done
  4.1654        show "norm (f' n x h - g' x h) \<le> e * norm h"
  4.1655          by (meson "*" mult_right_mono norm_ge_zero order.trans x f')
  4.1656 @@ -2109,7 +1900,7 @@
  4.1657    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::banach"
  4.1658    assumes "convex S"
  4.1659      and "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_derivative (f' n x)) (at x within S)"
  4.1660 -    and "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm (sum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
  4.1661 +    and "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. norm (sum (\<lambda>i. f' i x h) {..<n} - g' x h) \<le> e * norm h"
  4.1662      and "x \<in> S"
  4.1663      and "(\<lambda>n. f n x) sums l"
  4.1664    shows "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums (g x) \<and> (g has_derivative g' x) (at x within S)"
  4.1665 @@ -2130,7 +1921,9 @@
  4.1666    shows   "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)"
  4.1667  unfolding has_field_derivative_def
  4.1668  proof (rule has_derivative_series)
  4.1669 -  show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" if "e > 0" for e
  4.1670 +  show "\<forall>\<^sub>F n in sequentially.
  4.1671 +       \<forall>x\<in>S. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" if "e > 0" for e
  4.1672 +    unfolding eventually_sequentially
  4.1673    proof -
  4.1674      from that assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> S \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
  4.1675        unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
  4.1676 @@ -2217,17 +2010,17 @@
  4.1677    shows "f' = f''"
  4.1678  proof -
  4.1679    have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
  4.1680 -  proof (rule frechet_derivative_unique_within)
  4.1681 -    show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> S"
  4.1682 -    proof clarsimp
  4.1683 -      fix e :: real assume "0 < e"
  4.1684 -      with islimpt_approachable_real[of x S] not_bot
  4.1685 +  proof (rule frechet_derivative_unique_within, simp_all)
  4.1686 +    show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S" if "0 < e"  for e
  4.1687 +    proof -
  4.1688 +      from that
  4.1689        obtain x' where "x' \<in> S" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
  4.1690 +        using islimpt_approachable_real[of x S] not_bot
  4.1691          by (auto simp add: trivial_limit_within)
  4.1692 -      then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> S"
  4.1693 -        by (intro exI[of _ "x' - x"]) auto
  4.1694 +      then show ?thesis
  4.1695 +        using eq_iff_diff_eq_0 by fastforce
  4.1696      qed
  4.1697 -  qed (insert f' f'', auto simp: has_vector_derivative_def)
  4.1698 +  qed (use f' f'' in \<open>auto simp: has_vector_derivative_def\<close>)
  4.1699    then show ?thesis
  4.1700      unfolding fun_eq_iff by (metis scaleR_one)
  4.1701  qed
  4.1702 @@ -2416,59 +2209,59 @@
  4.1703  
  4.1704  lemma vector_derivative_within_closed_interval:
  4.1705    fixes f::"real \<Rightarrow> 'a::euclidean_space"
  4.1706 -  assumes "a < b" and "x \<in> {a .. b}"
  4.1707 -  assumes "(f has_vector_derivative f') (at x within {a .. b})"
  4.1708 -  shows "vector_derivative f (at x within {a .. b}) = f'"
  4.1709 +  assumes "a < b" and "x \<in> {a..b}"
  4.1710 +  assumes "(f has_vector_derivative f') (at x within {a..b})"
  4.1711 +  shows "vector_derivative f (at x within {a..b}) = f'"
  4.1712    using assms vector_derivative_within_cbox
  4.1713    by fastforce
  4.1714  
  4.1715  lemma has_vector_derivative_within_subset:
  4.1716 -  "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
  4.1717 +  "(f has_vector_derivative f') (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f has_vector_derivative f') (at x within T)"
  4.1718    by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
  4.1719  
  4.1720  lemma has_vector_derivative_at_within:
  4.1721 -  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
  4.1722 +  "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within S)"
  4.1723    unfolding has_vector_derivative_def
  4.1724    by (rule has_derivative_at_withinI)
  4.1725  
  4.1726  lemma has_vector_derivative_weaken:
  4.1727 -  fixes x D and f g s t
  4.1728 -  assumes f: "(f has_vector_derivative D) (at x within t)"
  4.1729 -    and "x \<in> s" "s \<subseteq> t"
  4.1730 -    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
  4.1731 -  shows "(g has_vector_derivative D) (at x within s)"
  4.1732 +  fixes x D and f g S T
  4.1733 +  assumes f: "(f has_vector_derivative D) (at x within T)"
  4.1734 +    and "x \<in> S" "S \<subseteq> T"
  4.1735 +    and "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  4.1736 +  shows "(g has_vector_derivative D) (at x within S)"
  4.1737  proof -
  4.1738 -  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
  4.1739 +  have "(f has_vector_derivative D) (at x within S) \<longleftrightarrow> (g has_vector_derivative D) (at x within S)"
  4.1740      unfolding has_vector_derivative_def has_derivative_iff_norm
  4.1741      using assms by (intro conj_cong Lim_cong_within refl) auto
  4.1742    then show ?thesis
  4.1743 -    using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
  4.1744 +    using has_vector_derivative_within_subset[OF f \<open>S \<subseteq> T\<close>] by simp
  4.1745  qed
  4.1746  
  4.1747  lemma has_vector_derivative_transform_within:
  4.1748 -  assumes "(f has_vector_derivative f') (at x within s)"
  4.1749 +  assumes "(f has_vector_derivative f') (at x within S)"
  4.1750      and "0 < d"
  4.1751 -    and "x \<in> s"
  4.1752 -    and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
  4.1753 -    shows "(g has_vector_derivative f') (at x within s)"
  4.1754 +    and "x \<in> S"
  4.1755 +    and "\<And>x'. \<lbrakk>x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
  4.1756 +    shows "(g has_vector_derivative f') (at x within S)"
  4.1757    using assms
  4.1758    unfolding has_vector_derivative_def
  4.1759    by (rule has_derivative_transform_within)
  4.1760  
  4.1761  lemma has_vector_derivative_transform_within_open:
  4.1762    assumes "(f has_vector_derivative f') (at x)"
  4.1763 -    and "open s"
  4.1764 -    and "x \<in> s"
  4.1765 -    and "\<And>y. y\<in>s \<Longrightarrow> f y = g y"
  4.1766 +    and "open S"
  4.1767 +    and "x \<in> S"
  4.1768 +    and "\<And>y. y\<in>S \<Longrightarrow> f y = g y"
  4.1769    shows "(g has_vector_derivative f') (at x)"
  4.1770    using assms
  4.1771    unfolding has_vector_derivative_def
  4.1772    by (rule has_derivative_transform_within_open)
  4.1773  
  4.1774  lemma has_vector_derivative_transform:
  4.1775 -  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
  4.1776 -  assumes f': "(f has_vector_derivative f') (at x within s)"
  4.1777 -  shows "(g has_vector_derivative f') (at x within s)"
  4.1778 +  assumes "x \<in> S" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
  4.1779 +  assumes f': "(f has_vector_derivative f') (at x within S)"
  4.1780 +  shows "(g has_vector_derivative f') (at x within S)"
  4.1781    using assms
  4.1782    unfolding has_vector_derivative_def
  4.1783    by (rule has_derivative_transform)
  4.1784 @@ -2477,23 +2270,13 @@
  4.1785    assumes "(f has_vector_derivative f') (at x)"
  4.1786      and "(g has_vector_derivative g') (at (f x))"
  4.1787    shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x)"
  4.1788 -  using assms(2)
  4.1789 -  unfolding has_vector_derivative_def
  4.1790 -  apply -
  4.1791 -  apply (drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
  4.1792 -  apply (simp only: o_def real_scaleR_def scaleR_scaleR)
  4.1793 -  done
  4.1794 +  using assms has_vector_derivative_at_within has_vector_derivative_def vector_derivative_diff_chain_within by blast
  4.1795  
  4.1796  lemma vector_diff_chain_within:
  4.1797    assumes "(f has_vector_derivative f') (at x within s)"
  4.1798      and "(g has_vector_derivative g') (at (f x) within f ` s)"
  4.1799    shows "((g \<circ> f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)"
  4.1800 -  using assms(2)
  4.1801 -  unfolding has_vector_derivative_def
  4.1802 -  apply -
  4.1803 -  apply (drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
  4.1804 -  apply (simp only: o_def real_scaleR_def scaleR_scaleR)
  4.1805 -  done
  4.1806 +  using assms has_vector_derivative_def vector_derivative_diff_chain_within by blast
  4.1807  
  4.1808  lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
  4.1809    by (simp add: vector_derivative_at)
  4.1810 @@ -2518,11 +2301,11 @@
  4.1811   by (auto simp: o_def mult.commute has_vector_derivative_def)
  4.1812  
  4.1813  lemma vector_derivative_chain_within: 
  4.1814 -  assumes "at x within s \<noteq> bot" "f differentiable (at x within s)" 
  4.1815 -    "(g has_derivative g') (at (f x) within f ` s)" 
  4.1816 -  shows "vector_derivative (g \<circ> f) (at x within s) =
  4.1817 -        g' (vector_derivative f (at x within s)) "
  4.1818 -  apply (rule vector_derivative_within [OF \<open>at x within s \<noteq> bot\<close>])
  4.1819 +  assumes "at x within S \<noteq> bot" "f differentiable (at x within S)" 
  4.1820 +    "(g has_derivative g') (at (f x) within f ` S)" 
  4.1821 +  shows "vector_derivative (g \<circ> f) (at x within S) =
  4.1822 +        g' (vector_derivative f (at x within S)) "
  4.1823 +  apply (rule vector_derivative_within [OF \<open>at x within S \<noteq> bot\<close>])
  4.1824    apply (rule vector_derivative_diff_chain_within)
  4.1825    using assms(2-3) vector_derivative_works
  4.1826    by auto
  4.1827 @@ -2543,26 +2326,22 @@
  4.1828  by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
  4.1829  
  4.1830  lemma field_differentiable_imp_continuous_at:
  4.1831 -    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
  4.1832 +    "f field_differentiable (at x within S) \<Longrightarrow> continuous (at x within S) f"
  4.1833    by (metis DERIV_continuous field_differentiable_def)
  4.1834  
  4.1835  lemma field_differentiable_within_subset:
  4.1836 -    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
  4.1837 -     \<Longrightarrow> f field_differentiable (at x within t)"
  4.1838 +    "\<lbrakk>f field_differentiable (at x within S); T \<subseteq> S\<rbrakk> \<Longrightarrow> f field_differentiable (at x within T)"
  4.1839    by (metis DERIV_subset field_differentiable_def)
  4.1840  
  4.1841  lemma field_differentiable_at_within:
  4.1842      "\<lbrakk>f field_differentiable (at x)\<rbrakk>
  4.1843 -     \<Longrightarrow> f field_differentiable (at x within s)"
  4.1844 +     \<Longrightarrow> f field_differentiable (at x within S)"
  4.1845    unfolding field_differentiable_def
  4.1846    by (metis DERIV_subset top_greatest)
  4.1847  
  4.1848  lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F"
  4.1849 -proof -
  4.1850 -  show ?thesis
  4.1851 -    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
  4.1852 -    by (force intro: has_derivative_mult_right)
  4.1853 -qed
  4.1854 +  unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
  4.1855 +  by (force intro: has_derivative_mult_right)
  4.1856  
  4.1857  lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
  4.1858    unfolding field_differentiable_def has_field_derivative_def
  4.1859 @@ -2602,45 +2381,45 @@
  4.1860    by (metis field_differentiable_diff)
  4.1861  
  4.1862  lemma field_differentiable_inverse [derivative_intros]:
  4.1863 -  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
  4.1864 -  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
  4.1865 +  assumes "f field_differentiable (at a within S)" "f a \<noteq> 0"
  4.1866 +  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within S)"
  4.1867    using assms unfolding field_differentiable_def
  4.1868    by (metis DERIV_inverse_fun)
  4.1869  
  4.1870  lemma field_differentiable_mult [derivative_intros]:
  4.1871 -  assumes "f field_differentiable (at a within s)"
  4.1872 -          "g field_differentiable (at a within s)"
  4.1873 -    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
  4.1874 +  assumes "f field_differentiable (at a within S)"
  4.1875 +          "g field_differentiable (at a within S)"
  4.1876 +    shows "(\<lambda>z. f z * g z) field_differentiable (at a within S)"
  4.1877    using assms unfolding field_differentiable_def
  4.1878 -  by (metis DERIV_mult [of f _ a s g])
  4.1879 +  by (metis DERIV_mult [of f _ a S g])
  4.1880  
  4.1881  lemma field_differentiable_divide [derivative_intros]:
  4.1882 -  assumes "f field_differentiable (at a within s)"
  4.1883 -          "g field_differentiable (at a within s)"
  4.1884 +  assumes "f field_differentiable (at a within S)"
  4.1885 +          "g field_differentiable (at a within S)"
  4.1886            "g a \<noteq> 0"
  4.1887 -    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
  4.1888 +    shows "(\<lambda>z. f z / g z) field_differentiable (at a within S)"
  4.1889    using assms unfolding field_differentiable_def
  4.1890 -  by (metis DERIV_divide [of f _ a s g])
  4.1891 +  by (metis DERIV_divide [of f _ a S g])
  4.1892  
  4.1893  lemma field_differentiable_power [derivative_intros]:
  4.1894 -  assumes "f field_differentiable (at a within s)"
  4.1895 -    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
  4.1896 +  assumes "f field_differentiable (at a within S)"
  4.1897 +    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within S)"
  4.1898    using assms unfolding field_differentiable_def
  4.1899    by (metis DERIV_power)
  4.1900  
  4.1901  lemma field_differentiable_transform_within:
  4.1902    "0 < d \<Longrightarrow>
  4.1903 -        x \<in> s \<Longrightarrow>
  4.1904 -        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
  4.1905 -        f field_differentiable (at x within s)
  4.1906 -        \<Longrightarrow> g field_differentiable (at x within s)"
  4.1907 +        x \<in> S \<Longrightarrow>
  4.1908 +        (\<And>x'. x' \<in> S \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
  4.1909 +        f field_differentiable (at x within S)
  4.1910 +        \<Longrightarrow> g field_differentiable (at x within S)"
  4.1911    unfolding field_differentiable_def has_field_derivative_def
  4.1912    by (blast intro: has_derivative_transform_within)
  4.1913  
  4.1914  lemma field_differentiable_compose_within:
  4.1915 -  assumes "f field_differentiable (at a within s)"
  4.1916 -          "g field_differentiable (at (f a) within f`s)"
  4.1917 -    shows "(g o f) field_differentiable (at a within s)"
  4.1918 +  assumes "f field_differentiable (at a within S)"
  4.1919 +          "g field_differentiable (at (f a) within f`S)"
  4.1920 +    shows "(g o f) field_differentiable (at a within S)"
  4.1921    using assms unfolding field_differentiable_def
  4.1922    by (metis DERIV_image_chain)
  4.1923  
  4.1924 @@ -2650,7 +2429,7 @@
  4.1925  by (metis field_differentiable_at_within field_differentiable_compose_within)
  4.1926  
  4.1927  lemma field_differentiable_within_open:
  4.1928 -     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
  4.1929 +     "\<lbrakk>a \<in> S; open S\<rbrakk> \<Longrightarrow> f field_differentiable at a within S \<longleftrightarrow>
  4.1930                            f field_differentiable at a"
  4.1931    unfolding field_differentiable_def
  4.1932    by (metis at_within_open)
  4.1933 @@ -2692,9 +2471,7 @@
  4.1934      unfolding *
  4.1935      by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros)
  4.1936  
  4.1937 -  moreover
  4.1938 -
  4.1939 -  have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
  4.1940 +  moreover have "\<forall>\<^sub>F x in at t within T. x \<noteq> t"
  4.1941      by (simp add: eventually_at_filter)
  4.1942    then have "\<forall>\<^sub>F x in at t within T. ((x - t) / \<bar>x - t\<bar>) *\<^sub>R ((\<Sum>n. ?e n x) - A) =
  4.1943      (exp ((x - t) *\<^sub>R A) - 1 - (x - t) *\<^sub>R A) /\<^sub>R norm (x - t)"
  4.1944 @@ -2721,9 +2498,7 @@
  4.1945        by (simp add: divide_simps)
  4.1946    qed
  4.1947  
  4.1948 -  ultimately
  4.1949 -
  4.1950 -  have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
  4.1951 +  ultimately have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
  4.1952      by (rule Lim_transform_eventually[rotated])
  4.1953    from tendsto_mult_right_zero[OF this, where c="exp (t *\<^sub>R A)"]
  4.1954    show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
  4.1955 @@ -2756,7 +2531,7 @@
  4.1956    also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_Int_closure_subset) auto
  4.1957    finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
  4.1958    moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
  4.1959 -    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  4.1960 +    unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  4.1961    moreover from eventually_at_right_real[OF xc]
  4.1962      have "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
  4.1963    proof eventually_elim
  4.1964 @@ -2778,7 +2553,7 @@
  4.1965    also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_Int_closure_subset) auto
  4.1966    finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
  4.1967    moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) \<longlongrightarrow> f') (at c within ?A')"
  4.1968 -    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  4.1969 +    unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  4.1970    moreover from eventually_at_left_real[OF xc]
  4.1971      have "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
  4.1972    proof eventually_elim
  4.1973 @@ -2816,8 +2591,7 @@
  4.1974  
  4.1975  lemma eventually_at_Pair_within_TimesI2:
  4.1976    fixes x::"'a::metric_space"
  4.1977 -  assumes "\<forall>\<^sub>F y' in at y within Y. P y'"
  4.1978 -  assumes "P y"
  4.1979 +  assumes "\<forall>\<^sub>F y' in at y within Y. P y'" "P y"
  4.1980    shows "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. P y'"
  4.1981  proof -
  4.1982    from assms[unfolded eventually_at_topological]
  4.1983 @@ -2907,12 +2681,12 @@
  4.1984        have "\<dots> \<subseteq> ball y d \<inter> Y"
  4.1985          using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
  4.1986          by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
  4.1987 -          (auto simp: dist_commute mem_ball)
  4.1988 +          (auto simp: dist_commute)
  4.1989        finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
  4.1990      } note seg = this
  4.1991  
  4.1992 -    have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
  4.1993 -      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: mem_ball dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
  4.1994 +    have "\<And>x. x \<in> ball y d \<inter> Y \<Longrightarrow> onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
  4.1995 +      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
  4.1996      with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
  4.1997      show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
  4.1998        by (rule differentiable_bound_linearization[where S="?S"])
  4.1999 @@ -2923,10 +2697,10 @@
  4.2000    from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
  4.2001    have "\<forall>\<^sub>F x' in at x within X. ?le x'"
  4.2002      by eventually_elim
  4.2003 -       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
  4.2004 +       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
  4.2005    then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
  4.2006      by (rule eventually_at_Pair_within_TimesI1)
  4.2007 -       (simp add: blinfun.bilinear_simps fx.zero)
  4.2008 +       (simp add: blinfun.bilinear_simps)
  4.2009    moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
  4.2010      unfolding norm_eq_zero right_minus_eq
  4.2011      by (auto simp: eventually_at intro!: zero_less_one)
  4.2012 @@ -2996,11 +2770,11 @@
  4.2013  subsection \<open>Differentiable case distinction\<close>
  4.2014  
  4.2015  lemma has_derivative_within_If_eq:
  4.2016 -  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
  4.2017 +  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within S) =
  4.2018      (bounded_linear f' \<and>
  4.2019       ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
  4.2020             else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
  4.2021 -      \<longlongrightarrow> 0) (at x within s))"
  4.2022 +      \<longlongrightarrow> 0) (at x within S))"
  4.2023    (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
  4.2024  proof -
  4.2025    have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
  4.2026 @@ -3011,41 +2785,41 @@
  4.2027  qed
  4.2028  
  4.2029  lemma has_derivative_If_within_closures:
  4.2030 -  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
  4.2031 -    (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
  4.2032 -  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
  4.2033 -    (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
  4.2034 -  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
  4.2035 -  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
  4.2036 -  assumes x_in: "x \<in> s \<union> t"
  4.2037 -  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
  4.2038 -      (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
  4.2039 +  assumes f': "x \<in> S \<union> (closure S \<inter> closure T) \<Longrightarrow>
  4.2040 +    (f has_derivative f' x) (at x within S \<union> (closure S \<inter> closure T))"
  4.2041 +  assumes g': "x \<in> T \<union> (closure S \<inter> closure T) \<Longrightarrow>
  4.2042 +    (g has_derivative g' x) (at x within T \<union> (closure S \<inter> closure T))"
  4.2043 +  assumes connect: "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f x = g x"
  4.2044 +  assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
  4.2045 +  assumes x_in: "x \<in> S \<union> T"
  4.2046 +  shows "((\<lambda>x. if x \<in> S then f x else g x) has_derivative
  4.2047 +      (if x \<in> S then f' x else g' x)) (at x within (S \<union> T))"
  4.2048  proof -
  4.2049 -  from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
  4.2050 +  from f' x_in interpret f': bounded_linear "if x \<in> S then f' x else (\<lambda>x. 0)"
  4.2051      by (auto simp add: has_derivative_within)
  4.2052 -  from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
  4.2053 +  from g' interpret g': bounded_linear "if x \<in> T then g' x else (\<lambda>x. 0)"
  4.2054      by (auto simp add: has_derivative_within)
  4.2055 -  have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
  4.2056 +  have bl: "bounded_linear (if x \<in> S then f' x else g' x)"
  4.2057      using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
  4.2058      by (unfold_locales; force)
  4.2059    show ?thesis
  4.2060 -    using f' g' closure_subset[of t] closure_subset[of s]
  4.2061 +    using f' g' closure_subset[of T] closure_subset[of S]
  4.2062      unfolding has_derivative_within_If_eq
  4.2063      by (intro conjI bl tendsto_If_within_closures x_in)
  4.2064        (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
  4.2065  qed
  4.2066  
  4.2067  lemma has_vector_derivative_If_within_closures:
  4.2068 -  assumes x_in: "x \<in> s \<union> t"
  4.2069 -  assumes "u = s \<union> t"
  4.2070 -  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
  4.2071 -    (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
  4.2072 -  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
  4.2073 -    (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
  4.2074 -  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
  4.2075 -  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
  4.2076 -  shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
  4.2077 -    (if x \<in> s then f' x else g' x)) (at x within u)"
  4.2078 +  assumes x_in: "x \<in> S \<union> T"
  4.2079 +  assumes "u = S \<union> T"
  4.2080 +  assumes f': "x \<in> S \<union> (closure S \<inter> closure T) \<Longrightarrow>
  4.2081 +    (f has_vector_derivative f' x) (at x within S \<union> (closure S \<inter> closure T))"
  4.2082 +  assumes g': "x \<in> T \<union> (closure S \<inter> closure T) \<Longrightarrow>
  4.2083 +    (g has_vector_derivative g' x) (at x within T \<union> (closure S \<inter> closure T))"
  4.2084 +  assumes connect: "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f x = g x"
  4.2085 +  assumes connect': "x \<in> closure S \<Longrightarrow> x \<in> closure T \<Longrightarrow> f' x = g' x"
  4.2086 +  shows "((\<lambda>x. if x \<in> S then f x else g x) has_vector_derivative
  4.2087 +    (if x \<in> S then f' x else g' x)) (at x within u)"
  4.2088    unfolding has_vector_derivative_def assms
  4.2089    using x_in
  4.2090    apply (intro has_derivative_If_within_closures[where
     5.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat May 19 20:42:34 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun May 20 18:37:34 2018 +0100
     5.3 @@ -5089,9 +5089,9 @@
     5.4              using B' [of a b] B' [of c d] norm_triangle_half_r by blast
     5.5          qed
     5.6        qed (use \<open>B > 0\<close> in auto)}
     5.7 -  then show ?thesis
     5.8 -    by force
     5.9 -qed
    5.10 +    then show ?thesis
    5.11 +      by force
    5.12 +  qed
    5.13    finally show ?thesis .
    5.14  qed
    5.15  
    5.16 @@ -6496,7 +6496,7 @@
    5.17            unfolding has_vector_derivative_def[symmetric]
    5.18            using that \<open>x \<in> X0\<close>
    5.19            by (intro has_derivative_within_subset[OF fx]) auto
    5.20 -        have "\<forall>x \<in> X0 \<inter> U. onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
    5.21 +        have "\<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
    5.22            using fx_bound t
    5.23            by (auto simp add: norm_blinfun_def fun_diff_def blinfun.bilinear_simps[symmetric])
    5.24          from differentiable_bound_linearization[OF seg deriv this] X0
     6.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sat May 19 20:42:34 2018 +0200
     6.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun May 20 18:37:34 2018 +0100
     6.3 @@ -250,8 +250,8 @@
     6.4  lemma homeomorphic_closed_intervals_real:
     6.5    fixes a::real and b and c::real and d
     6.6    assumes "a<b" and "c<d"
     6.7 -    shows "{a..b} homeomorphic {c..d}"
     6.8 -by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
     6.9 +  shows "{a..b} homeomorphic {c..d}"
    6.10 +  using assms by (auto intro: homeomorphic_convex_compact)
    6.11  
    6.12  no_notation
    6.13    eucl_less (infix "<e" 50)