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.108 -   prefer 2 apply (simp add: add.assoc [symmetric])
   1.109 -   apply (auto simp add: mem_infmal_iff [symmetric] add.commute)
   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.141  lemma NSDERIV_add:
   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.144 -  apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
   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.179 -  apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
   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.185 -  apply (auto intro!: approx_add_mono1 simp: distrib_right distrib_left mult.commute add.assoc)
   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.189 -      simp add: add.assoc [symmetric])
   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.308 -      apply (rule inverse_add_Infinitesimal_approx2)
   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