src/HOL/Nonstandard_Analysis/HDeriv.thy
 changeset 68644 242d298526a3 parent 67399 eab6ce8368fa child 69064 5840724b1d71
```     1.1 --- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Jul 15 21:58:50 2018 +0100
1.2 +++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Jul 16 23:33:28 2018 +0100
1.3 @@ -39,34 +39,26 @@
1.4
1.5  lemma Infinitesimal_of_hypreal:
1.6    "x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal"
1.7 -  apply (rule InfinitesimalI2)
1.8 -  apply (drule (1) InfinitesimalD2)
1.9 -  apply (simp add: hnorm_of_hypreal)
1.10 -  done
1.11 +  by (metis Infinitesimal_of_hypreal_iff of_hypreal_def)
1.12
1.13  lemma of_hypreal_eq_0_iff: "\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)"
1.14    by transfer (rule of_real_eq_0_iff)
1.15
1.16 -lemma NSDeriv_unique: "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
1.17 -  apply (subgoal_tac "( *f* of_real) \<epsilon> \<in> Infinitesimal - {0::'a star}")
1.18 -   apply (simp only: nsderiv_def)
1.19 -   apply (drule (1) bspec)+
1.20 -   apply (drule (1) approx_trans3)
1.21 -   apply simp
1.22 -  apply (simp add: Infinitesimal_of_hypreal)
1.23 -  apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
1.24 -  done
1.25 +lemma NSDeriv_unique:
1.26 +  assumes "NSDERIV f x :> D" "NSDERIV f x :> E"
1.27 +  shows "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
1.28 +proof -
1.29 +  have "\<exists>s. (s::'a star) \<in> Infinitesimal - {0}"
1.30 +    by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal hypreal_epsilon_not_zero singletonD)
1.31 +  with assms show ?thesis
1.32 +    by (meson approx_trans3 nsderiv_def star_of_approx_iff)
1.33 +qed
1.34
1.35  text \<open>First \<open>NSDERIV\<close> in terms of \<open>NSLIM\<close>.\<close>
1.36
1.37  text \<open>First equivalence.\<close>
1.38  lemma NSDERIV_NSLIM_iff: "(NSDERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
1.39 -  apply (auto simp add: nsderiv_def NSLIM_def)
1.40 -   apply (drule_tac x = xa in bspec)
1.41 -    apply (rule_tac [3] ccontr)
1.42 -    apply (drule_tac [3] x = h in spec)
1.43 -    apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
1.44 -  done
1.45 +  by (auto simp add: nsderiv_def NSLIM_def starfun_lambda_cancel mem_infmal_iff)
1.46
1.47  text \<open>Second equivalence.\<close>
1.48  lemma NSDERIV_NSLIM_iff2: "(NSDERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D"
1.49 @@ -78,63 +70,39 @@
1.50      (\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow> ( *f* (\<lambda>z. (f z - f x) / (z - x))) w \<approx> star_of D)"
1.51    by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
1.52
1.53 -(* FIXME delete *)
1.54 -lemma hypreal_not_eq_minus_iff: "x \<noteq> a \<longleftrightarrow> x - a \<noteq> (0::'a::ab_group_add)"
1.55 -  by auto
1.56 -
1.57  lemma NSDERIVD5:
1.58 -  "(NSDERIV f x :> D) \<Longrightarrow>
1.59 -   (\<forall>u. u \<approx> hypreal_of_real x \<longrightarrow>
1.60 -     ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))"
1.61 -  apply (auto simp add: NSDERIV_iff2)
1.62 +  "\<lbrakk>NSDERIV f x :> D; u \<approx> hypreal_of_real x\<rbrakk> \<Longrightarrow>
1.63 +     ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x)"
1.64 +  unfolding NSDERIV_iff2
1.65    apply (case_tac "u = hypreal_of_real x", auto)
1.66 -  apply (drule_tac x = u in spec, auto)
1.67 -  apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
1.68 -   apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
1.69 -   apply (subgoal_tac [2] "( *f* (\<lambda>z. z - x)) u \<noteq> (0::hypreal) ")
1.70 -    apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
1.71 -      Infinitesimal_subset_HFinite [THEN subsetD])
1.72 -  done
1.73 +  by (metis (mono_tags, lifting) HFinite_star_of Infinitesimal_ratio approx_def approx_minus_iff approx_mult_subst approx_star_of_HFinite approx_sym mult_zero_right right_minus_eq)
1.74
1.75  lemma NSDERIVD4:
1.76 -  "(NSDERIV f x :> D) \<Longrightarrow>
1.77 -    (\<forall>h \<in> Infinitesimal.
1.78 -      ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h)"
1.79 -  apply (auto simp add: nsderiv_def)
1.80 -  apply (case_tac "h = 0")
1.81 -   apply auto
1.82 -  apply (drule_tac x = h in bspec)
1.83 -   apply (drule_tac [2] c = h in approx_mult1)
1.84 -    apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
1.85 -  done
1.86 -
1.87 -lemma NSDERIVD3:
1.88 -  "(NSDERIV f x :> D) \<Longrightarrow>
1.89 -    \<forall>h \<in> Infinitesimal - {0}.
1.90 -      (( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) \<approx> hypreal_of_real D * h"
1.91 -  apply (auto simp add: nsderiv_def)
1.92 -  apply (rule ccontr, drule_tac x = h in bspec)
1.93 -   apply (drule_tac [2] c = h in approx_mult1)
1.94 -    apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
1.95 -  done
1.96 +  "\<lbrakk>NSDERIV f x :> D; h \<in> Infinitesimal\<rbrakk>
1.97 +    \<Longrightarrow> ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h"
1.98 +  apply (clarsimp simp add: nsderiv_def)
1.99 +  apply (case_tac "h = 0", simp)
1.100 +  by (meson DiffI Infinitesimal_approx Infinitesimal_ratio Infinitesimal_star_of_mult2 approx_star_of_HFinite singletonD)
1.101
1.102  text \<open>Differentiability implies continuity nice and simple "algebraic" proof.\<close>
1.103 -lemma NSDERIV_isNSCont: "NSDERIV f x :> D \<Longrightarrow> isNSCont f x"
1.104 -  apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
1.105 -  apply (drule approx_minus_iff [THEN iffD1])
1.106 -  apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
1.107 -  apply (drule_tac x = "xa - star_of x" in bspec)
1.110 -  apply (drule_tac c = "xa - star_of x" in approx_mult1)
1.111 -   apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
1.112 -  apply (drule_tac x3=D in
1.113 -      HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult, THEN mem_infmal_iff [THEN iffD1]])
1.114 -  apply (auto simp add: mult.commute intro: approx_trans approx_minus_iff [THEN iffD2])
1.115 -  done
1.116 +lemma NSDERIV_isNSCont:
1.117 +  assumes "NSDERIV f x :> D" shows "isNSCont f x"
1.118 +  unfolding isNSCont_NSLIM_iff NSLIM_def
1.119 +proof clarify
1.120 +  fix x'
1.121 +  assume "x' \<noteq> star_of x" "x' \<approx> star_of x"
1.122 +  then have m0: "x' - star_of x \<in> Infinitesimal - {0}"
1.123 +    using bex_Infinitesimal_iff by auto
1.124 +  then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<approx> star_of D"
1.125 +    by (metis \<open>x' \<approx> star_of x\<close> add_diff_cancel_left' assms bex_Infinitesimal_iff2 nsderiv_def)
1.126 +  then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<in> HFinite"
1.127 +    by (metis approx_star_of_HFinite)
1.128 +  then show "( *f* f) x' \<approx> star_of (f x)"
1.129 +    by (metis (no_types) Diff_iff Infinitesimal_ratio m0 bex_Infinitesimal_iff insert_iff)
1.130 +qed
1.131
1.132  text \<open>Differentiation rules for combinations of functions
1.133 -  follow from clear, straightforard, algebraic manipulations.\<close>
1.134 +  follow from clear, straightforward, algebraic manipulations.\<close>
1.135
1.136  text \<open>Constant function.\<close>
1.137
1.138 @@ -145,53 +113,34 @@
1.139  text \<open>Sum of functions- proved easily.\<close>
1.140
1.142 -  "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x + g x) x :> Da + Db"
1.143 -  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
1.145 -  apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
1.146 -   apply (auto simp add: ac_simps algebra_simps)
1.147 -  done
1.148 -
1.149 -text \<open>Product of functions - Proof is trivial but tedious
1.150 -  and long due to rearrangement of terms.\<close>
1.151 +  assumes "NSDERIV f x :> Da" "NSDERIV g x :> Db"
1.152 +  shows "NSDERIV (\<lambda>x. f x + g x) x :> Da + Db"
1.153 +proof -
1.154 +  have "((\<lambda>x. f x + g x) has_field_derivative Da + Db) (at x)"
1.155 +    using assms DERIV_NS_iff NSDERIV_NSLIM_iff field_differentiable_add by blast
1.156 +  then show ?thesis
1.157 +    by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff)
1.158 +qed
1.159
1.160 -lemma lemma_nsderiv1: "(a * b) - (c * d) = (b * (a - c)) + (c * (b - d))"
1.161 -  for a b c d :: "'a::comm_ring star"
1.162 -  by (simp add: right_diff_distrib ac_simps)
1.163 -
1.164 -lemma lemma_nsderiv2: "(x - y) / z = star_of D + yb \<Longrightarrow> z \<noteq> 0 \<Longrightarrow>
1.165 -  z \<in> Infinitesimal \<Longrightarrow> yb \<in> Infinitesimal \<Longrightarrow> x - y \<approx> 0"
1.166 -  for x y z :: "'a::real_normed_field star"
1.167 -  apply (simp add: nonzero_divide_eq_eq)
1.168 -  apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
1.169 -      simp add: mult.assoc mem_infmal_iff [symmetric])
1.170 -  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
1.171 -  done
1.172 +text \<open>Product of functions - Proof is simple.\<close>
1.173
1.174  lemma NSDERIV_mult:
1.175 -  "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow>
1.176 -    NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)"
1.177 -  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
1.178 -  apply (auto dest!: spec simp add: starfun_lambda_cancel lemma_nsderiv1)
1.180 -  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
1.181 -  apply (auto simp add: times_divide_eq_right [symmetric]
1.182 -      simp del: times_divide_eq_right times_divide_eq_left)
1.183 -  apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
1.184 -  apply (drule_tac approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
1.186 -  apply (rule_tac b1 = "star_of Db * star_of (f x)" in add.commute [THEN subst])
1.187 -  apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
1.188 -      Infinitesimal_add Infinitesimal_mult Infinitesimal_star_of_mult Infinitesimal_star_of_mult2
1.190 -  done
1.191 +  assumes "NSDERIV g x :> Db" "NSDERIV f x :> Da"
1.192 +  shows "NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)"
1.193 +proof -
1.194 +  have "(f has_field_derivative Da) (at x)" "(g has_field_derivative Db) (at x)"
1.195 +    using assms by (simp_all add: DERIV_NS_iff NSDERIV_NSLIM_iff)
1.196 +  then have "((\<lambda>a. f a * g a) has_field_derivative Da * g x + Db * f x) (at x)"
1.197 +    using DERIV_mult by blast
1.198 +  then show ?thesis
1.199 +    by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff)
1.200 +qed
1.201
1.202  text \<open>Multiplying by a constant.\<close>
1.203  lemma NSDERIV_cmult: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. c * f x) x :> c * D"
1.204 -  apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
1.205 -      minus_mult_right right_diff_distrib [symmetric])
1.206 -  apply (erule NSLIM_const [THEN NSLIM_mult])
1.207 -  done
1.208 +  unfolding times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
1.209 +      minus_mult_right right_diff_distrib [symmetric]
1.210 +  by (erule NSLIM_const [THEN NSLIM_mult])
1.211
1.212  text \<open>Negation of function.\<close>
1.213  lemma NSDERIV_minus: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. - f x) x :> - D"
1.214 @@ -227,22 +176,15 @@
1.215  subsection \<open>Lemmas\<close>
1.216
1.217  lemma NSDERIV_zero:
1.218 -  "NSDERIV g x :> D \<Longrightarrow> ( *f* g) (star_of x + xa) = star_of (g x) \<Longrightarrow>
1.219 -    xa \<in> Infinitesimal \<Longrightarrow> xa \<noteq> 0 \<Longrightarrow> D = 0"
1.220 -  apply (simp add: nsderiv_def)
1.221 -  apply (drule bspec)
1.222 -   apply auto
1.223 -  done
1.224 +  "\<lbrakk>NSDERIV g x :> D; ( *f* g) (star_of x + y) = star_of (g x); y \<in> Infinitesimal; y \<noteq> 0\<rbrakk>
1.225 +    \<Longrightarrow> D = 0"
1.226 +  by (force simp add: nsderiv_def)
1.227
1.228  text \<open>Can be proved differently using \<open>NSLIM_isCont_iff\<close>.\<close>
1.229  lemma NSDERIV_approx:
1.230    "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
1.231      ( *f* f) (star_of x + h) - star_of (f x) \<approx> 0"
1.232 -  apply (simp add: nsderiv_def)
1.233 -  apply (simp add: mem_infmal_iff [symmetric])
1.234 -  apply (rule Infinitesimal_ratio)
1.235 -    apply (rule_tac [3] approx_star_of_HFinite, auto)
1.236 -  done
1.237 +  by (meson DiffI Infinitesimal_ratio approx_star_of_HFinite mem_infmal_iff nsderiv_def singletonD)
1.238
1.239  text \<open>From one version of differentiability
1.240
1.241 @@ -251,13 +193,13 @@
1.242            \<open>x - a\<close>
1.243  \<close>
1.244
1.245 -lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
1.246 -         ( *f* g) (star_of(x) + xa) \<noteq> star_of (g x);
1.247 -         ( *f* g) (star_of(x) + xa) \<approx> star_of (g x)
1.248 -      |] ==> (( *f* f) (( *f* g) (star_of(x) + xa))
1.249 -                   - star_of (f (g x)))
1.250 -              / (( *f* g) (star_of(x) + xa) - star_of (g x))
1.251 -             \<approx> star_of(Da)"
1.252 +lemma NSDERIVD1:
1.253 +    "\<lbrakk>NSDERIV f (g x) :> Da;
1.254 +     ( *f* g) (star_of x + y) \<noteq> star_of (g x);
1.255 +     ( *f* g) (star_of x + y) \<approx> star_of (g x)\<rbrakk>
1.256 +    \<Longrightarrow> (( *f* f) (( *f* g) (star_of x + y)) -
1.257 +         star_of (f (g x))) / (( *f* g) (star_of x + y) - star_of (g x)) \<approx>
1.258 +        star_of Da"
1.259    by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
1.260
1.261  text \<open>From other version of differentiability
1.262 @@ -267,37 +209,15 @@
1.263               \<open>h\<close>
1.264  \<close>
1.265
1.266 -lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |]
1.267 -      ==> (( *f* g) (star_of(x) + xa) - star_of(g x)) / xa
1.268 +lemma NSDERIVD2: "[| NSDERIV g x :> Db; y \<in> Infinitesimal; y \<noteq> 0 |]
1.269 +      ==> (( *f* g) (star_of(x) + y) - star_of(g x)) / y
1.270            \<approx> star_of(Db)"
1.271    by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)
1.272
1.273 -lemma lemma_chain: "z \<noteq> 0 \<Longrightarrow> x * y = (x * inverse z) * (z * y)"
1.274 -  for x y z :: "'a::real_normed_field star"
1.275 -proof -
1.276 -  assume z: "z \<noteq> 0"
1.277 -  have "x * y = x * (inverse z * z) * y" by (simp add: z)
1.278 -  then show ?thesis by (simp add: mult.assoc)
1.279 -qed
1.280 -
1.281  text \<open>This proof uses both definitions of differentiability.\<close>
1.282  lemma NSDERIV_chain:
1.283    "NSDERIV f (g x) :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (f \<circ> g) x :> Da * Db"
1.284 -  apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff [symmetric])
1.285 -  apply clarify
1.286 -  apply (frule_tac f = g in NSDERIV_approx)
1.287 -    apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
1.288 -  apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
1.289 -   apply (drule_tac g = g in NSDERIV_zero)
1.290 -      apply (auto simp add: divide_inverse)
1.291 -  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
1.292 -      in lemma_chain [THEN ssubst])
1.293 -   apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
1.294 -  apply (rule approx_mult_star_of)
1.295 -   apply (simp_all add: divide_inverse [symmetric])
1.296 -   apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
1.297 -  apply (blast intro: NSDERIVD2)
1.298 -  done
1.299 +  using DERIV_NS_iff DERIV_chain NSDERIV_NSLIM_iff by blast
1.300
1.301  text \<open>Differentiation of natural number powers.\<close>
1.302  lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1"
1.303 @@ -321,20 +241,17 @@
1.304        by (rule Infinitesimal_HFinite_mult) simp
1.305      with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx>
1.306        inverse (- (star_of x * star_of x))"
1.307 -      apply -
1.309 -      apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
1.310 -        simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
1.311 -      done
1.312 +    proof -
1.313 +      have "- (h * star_of x) + - (star_of x * star_of x) \<approx> - (star_of x * star_of x)"
1.314 +        using \<open>h * star_of x \<in> Infinitesimal\<close> assms bex_Infinitesimal_iff by fastforce
1.315 +      then show ?thesis
1.316 +        by (metis assms mult_eq_0_iff neg_equal_0_iff_equal star_of_approx_inverse star_of_minus star_of_mult)
1.317 +    qed
1.318      moreover from not_0 \<open>h \<noteq> 0\<close> assms
1.319 -    have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
1.320 -      (inverse (star_of x + h) - inverse (star_of x)) / h"
1.321 -      apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
1.322 -          nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
1.323 -      apply (subst nonzero_inverse_minus_eq [symmetric])
1.324 -      using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
1.325 -      apply (simp add: field_simps)
1.326 -      done
1.327 +    have "inverse (- (h * star_of x) + - (star_of x * star_of x))
1.328 +          = (inverse (star_of x + h) - inverse (star_of x)) / h"
1.329 +      by (simp add: division_ring_inverse_diff inverse_mult_distrib [symmetric]
1.330 +          inverse_minus_eq [symmetric] algebra_simps)
1.331      ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
1.332        - (inverse (star_of x) * inverse (star_of x))"
1.333        using assms by simp
1.334 @@ -372,7 +289,7 @@
1.335
1.336  lemma CARAT_NSDERIV:
1.337    "NSDERIV f x :> l \<Longrightarrow> \<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isNSCont g x \<and> g x = l"
1.338 -  by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV mult.commute)
1.339 +  by (simp add: CARAT_DERIV NSDERIV_DERIV_iff isNSCont_isCont_iff)
1.340
1.341  lemma hypreal_eq_minus_iff3: "x = y + z \<longleftrightarrow> x + - z = y"
1.342    for x y z :: hypreal
1.343 @@ -414,30 +331,23 @@
1.344
1.345  text \<open>The Increment theorem -- Keisler p. 65.\<close>
1.346  lemma increment_thm:
1.347 -  "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
1.348 -    \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
1.349 -  apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
1.350 -  apply (drule bspec, auto)
1.351 -  apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
1.352 -  apply (frule_tac b1 = "hypreal_of_real D + y" in mult_right_cancel [THEN iffD2])
1.353 -   apply (erule_tac [2]
1.354 -      V = "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y"
1.355 -      in thin_rl)
1.356 -   apply assumption
1.357 -  apply (simp add: times_divide_eq_right [symmetric])
1.358 -  apply (auto simp add: distrib_right)
1.359 -  done
1.360 -
1.361 -lemma increment_thm2:
1.362 -  "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
1.363 -    \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
1.364 -  by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
1.365 +  assumes "NSDERIV f x :> D" "h \<in> Infinitesimal" "h \<noteq> 0"
1.366 +  shows "\<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
1.367 +proof -
1.368 +  have inc: "increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)"
1.369 +    using assms(1) incrementI2 by auto
1.370 +  have "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h \<approx> hypreal_of_real D"
1.371 +    by (simp add: NSDERIVD2 assms)
1.372 +  then obtain y where "y \<in> Infinitesimal"
1.373 +    "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real D + y"
1.374 +    by (metis bex_Infinitesimal_iff2)
1.375 +  then have "increment f x h / h = hypreal_of_real D + y"
1.376 +    by (metis inc)
1.377 +  then show ?thesis
1.378 +    by (metis (no_types) \<open>y \<in> Infinitesimal\<close> \<open>h \<noteq> 0\<close> distrib_right mult.commute nonzero_mult_div_cancel_left times_divide_eq_right)
1.379 +qed
1.380
1.381  lemma increment_approx_zero: "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow> increment f x h \<approx> 0"
1.382 -  apply (drule increment_thm2)
1.383 -    apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
1.384 -      simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
1.385 -  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
1.386 -  done
1.387 +  by (simp add: NSDERIV_approx incrementI2 mem_infmal_iff)
1.388
1.389  end
```