merged

--- a/src/HOL/Deriv.thy	Mon Jul 16 17:50:07 2018 +0200
+++ b/src/HOL/Deriv.thy	Mon Jul 16 23:33:38 2018 +0100
@@ -1086,7 +1086,7 @@
 
 text \<open>Caratheodory formulation of derivative at a point\<close>
 
-lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
+lemma CARAT_DERIV:
   "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
   (is "?lhs = ?rhs")
 proof
@@ -1103,8 +1103,6 @@
   qed
 next
   assume ?rhs
-  then obtain g where "(\<forall>z. f z - f x = g z * (z - x))" and "isCont g x" and "g x = l"
-    by blast
   then show ?lhs
     by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
 qed

--- a/src/HOL/Divides.thy	Mon Jul 16 17:50:07 2018 +0200
+++ b/src/HOL/Divides.thy	Mon Jul 16 23:33:38 2018 +0100
@@ -607,7 +607,7 @@
   shows "a div b < 0"
 proof -
   have "a div b \<le> - 1 div b"
-    using Divides.zdiv_mono1 assms by auto
+    using zdiv_mono1 assms by auto
   also have "... \<le> -1"
     by (simp add: assms(2) div_eq_minus1)
   finally show ?thesis 

--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Jul 16 17:50:07 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Jul 16 23:33:38 2018 +0100
@@ -39,34 +39,26 @@
 
 lemma Infinitesimal_of_hypreal:
   "x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal"
-  apply (rule InfinitesimalI2)
-  apply (drule (1) InfinitesimalD2)
-  apply (simp add: hnorm_of_hypreal)
-  done
+  by (metis Infinitesimal_of_hypreal_iff of_hypreal_def)
 
 lemma of_hypreal_eq_0_iff: "\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)"
   by transfer (rule of_real_eq_0_iff)
 
-lemma NSDeriv_unique: "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
-  apply (subgoal_tac "( *f* of_real) \<epsilon> \<in> Infinitesimal - {0::'a star}")
-   apply (simp only: nsderiv_def)
-   apply (drule (1) bspec)+
-   apply (drule (1) approx_trans3)
-   apply simp
-  apply (simp add: Infinitesimal_of_hypreal)
-  apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
-  done
+lemma NSDeriv_unique:
+  assumes "NSDERIV f x :> D" "NSDERIV f x :> E"
+  shows "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
+proof -
+  have "\<exists>s. (s::'a star) \<in> Infinitesimal - {0}"
+    by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal hypreal_epsilon_not_zero singletonD)
+  with assms show ?thesis
+    by (meson approx_trans3 nsderiv_def star_of_approx_iff)
+qed
 
 text \<open>First \<open>NSDERIV\<close> in terms of \<open>NSLIM\<close>.\<close>
 
 text \<open>First equivalence.\<close>
 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"
-  apply (auto simp add: nsderiv_def NSLIM_def)
-   apply (drule_tac x = xa in bspec)
-    apply (rule_tac [3] ccontr)
-    apply (drule_tac [3] x = h in spec)
-    apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
-  done
+  by (auto simp add: nsderiv_def NSLIM_def starfun_lambda_cancel mem_infmal_iff)
 
 text \<open>Second equivalence.\<close>
 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"
@@ -78,63 +70,39 @@
     (\<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)"
   by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
 
-(* FIXME delete *)
-lemma hypreal_not_eq_minus_iff: "x \<noteq> a \<longleftrightarrow> x - a \<noteq> (0::'a::ab_group_add)"
-  by auto
-
 lemma NSDERIVD5:
-  "(NSDERIV f x :> D) \<Longrightarrow>
-   (\<forall>u. u \<approx> hypreal_of_real x \<longrightarrow>
-     ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))"
-  apply (auto simp add: NSDERIV_iff2)
+  "\<lbrakk>NSDERIV f x :> D; u \<approx> hypreal_of_real x\<rbrakk> \<Longrightarrow>
+     ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x)"
+  unfolding NSDERIV_iff2
   apply (case_tac "u = hypreal_of_real x", auto)
-  apply (drule_tac x = u in spec, auto)
-  apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
-   apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
-   apply (subgoal_tac [2] "( *f* (\<lambda>z. z - x)) u \<noteq> (0::hypreal) ")
-    apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
-      Infinitesimal_subset_HFinite [THEN subsetD])
-  done
+  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)
 
 lemma NSDERIVD4:
-  "(NSDERIV f x :> D) \<Longrightarrow>
-    (\<forall>h \<in> Infinitesimal.
-      ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h)"
-  apply (auto simp add: nsderiv_def)
-  apply (case_tac "h = 0")
-   apply auto
-  apply (drule_tac x = h in bspec)
-   apply (drule_tac [2] c = h in approx_mult1)
-    apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
-  done
-
-lemma NSDERIVD3:
-  "(NSDERIV f x :> D) \<Longrightarrow>
-    \<forall>h \<in> Infinitesimal - {0}.
-      (( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) \<approx> hypreal_of_real D * h"
-  apply (auto simp add: nsderiv_def)
-  apply (rule ccontr, drule_tac x = h in bspec)
-   apply (drule_tac [2] c = h in approx_mult1)
-    apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
-  done
+  "\<lbrakk>NSDERIV f x :> D; h \<in> Infinitesimal\<rbrakk>
+    \<Longrightarrow> ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h"
+  apply (clarsimp simp add: nsderiv_def)
+  apply (case_tac "h = 0", simp)
+  by (meson DiffI Infinitesimal_approx Infinitesimal_ratio Infinitesimal_star_of_mult2 approx_star_of_HFinite singletonD)
 
 text \<open>Differentiability implies continuity nice and simple "algebraic" proof.\<close>
-lemma NSDERIV_isNSCont: "NSDERIV f x :> D \<Longrightarrow> isNSCont f x"
-  apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
-  apply (drule approx_minus_iff [THEN iffD1])
-  apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
-  apply (drule_tac x = "xa - star_of x" in bspec)
-   prefer 2 apply (simp add: add.assoc [symmetric])
-   apply (auto simp add: mem_infmal_iff [symmetric] add.commute)
-  apply (drule_tac c = "xa - star_of x" in approx_mult1)
-   apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
-  apply (drule_tac x3=D in
-      HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult, THEN mem_infmal_iff [THEN iffD1]])
-  apply (auto simp add: mult.commute intro: approx_trans approx_minus_iff [THEN iffD2])
-  done
+lemma NSDERIV_isNSCont: 
+  assumes "NSDERIV f x :> D" shows "isNSCont f x"
+  unfolding isNSCont_NSLIM_iff NSLIM_def
+proof clarify
+  fix x'
+  assume "x' \<noteq> star_of x" "x' \<approx> star_of x"
+  then have m0: "x' - star_of x \<in> Infinitesimal - {0}"
+    using bex_Infinitesimal_iff by auto
+  then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<approx> star_of D"
+    by (metis \<open>x' \<approx> star_of x\<close> add_diff_cancel_left' assms bex_Infinitesimal_iff2 nsderiv_def)
+  then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<in> HFinite"
+    by (metis approx_star_of_HFinite)  
+  then show "( *f* f) x' \<approx> star_of (f x)"
+    by (metis (no_types) Diff_iff Infinitesimal_ratio m0 bex_Infinitesimal_iff insert_iff)
+qed
 
 text \<open>Differentiation rules for combinations of functions
-  follow from clear, straightforard, algebraic manipulations.\<close>
+  follow from clear, straightforward, algebraic manipulations.\<close>
 
 text \<open>Constant function.\<close>
 
@@ -145,53 +113,34 @@
 text \<open>Sum of functions- proved easily.\<close>
 
 lemma NSDERIV_add:
-  "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x + g x) x :> Da + Db"
-  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
-  apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
-  apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
-   apply (auto simp add: ac_simps algebra_simps)
-  done
-
-text \<open>Product of functions - Proof is trivial but tedious
-  and long due to rearrangement of terms.\<close>
+  assumes "NSDERIV f x :> Da" "NSDERIV g x :> Db"
+  shows "NSDERIV (\<lambda>x. f x + g x) x :> Da + Db"
+proof -
+  have "((\<lambda>x. f x + g x) has_field_derivative Da + Db) (at x)"
+    using assms DERIV_NS_iff NSDERIV_NSLIM_iff field_differentiable_add by blast
+  then show ?thesis
+    by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff)
+qed
 
-lemma lemma_nsderiv1: "(a * b) - (c * d) = (b * (a - c)) + (c * (b - d))"
-  for a b c d :: "'a::comm_ring star"
-  by (simp add: right_diff_distrib ac_simps)
-
-lemma lemma_nsderiv2: "(x - y) / z = star_of D + yb \<Longrightarrow> z \<noteq> 0 \<Longrightarrow>
-  z \<in> Infinitesimal \<Longrightarrow> yb \<in> Infinitesimal \<Longrightarrow> x - y \<approx> 0"
-  for x y z :: "'a::real_normed_field star"
-  apply (simp add: nonzero_divide_eq_eq)
-  apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
-      simp add: mult.assoc mem_infmal_iff [symmetric])
-  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
-  done
+text \<open>Product of functions - Proof is simple.\<close>
 
 lemma NSDERIV_mult:
-  "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow>
-    NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)"
-  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
-  apply (auto dest!: spec simp add: starfun_lambda_cancel lemma_nsderiv1)
-  apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
-  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
-  apply (auto simp add: times_divide_eq_right [symmetric]
-      simp del: times_divide_eq_right times_divide_eq_left)
-  apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
-  apply (drule_tac approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
-  apply (auto intro!: approx_add_mono1 simp: distrib_right distrib_left mult.commute add.assoc)
-  apply (rule_tac b1 = "star_of Db * star_of (f x)" in add.commute [THEN subst])
-  apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
-      Infinitesimal_add Infinitesimal_mult Infinitesimal_star_of_mult Infinitesimal_star_of_mult2
-      simp add: add.assoc [symmetric])
-  done
+  assumes "NSDERIV g x :> Db" "NSDERIV f x :> Da"
+  shows "NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)"
+proof -
+  have "(f has_field_derivative Da) (at x)" "(g has_field_derivative Db) (at x)"
+    using assms by (simp_all add: DERIV_NS_iff NSDERIV_NSLIM_iff)
+  then have "((\<lambda>a. f a * g a) has_field_derivative Da * g x + Db * f x) (at x)"
+    using DERIV_mult by blast
+  then show ?thesis
+    by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff)
+qed
 
 text \<open>Multiplying by a constant.\<close>
 lemma NSDERIV_cmult: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. c * f x) x :> c * D"
-  apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
-      minus_mult_right right_diff_distrib [symmetric])
-  apply (erule NSLIM_const [THEN NSLIM_mult])
-  done
+  unfolding times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
+      minus_mult_right right_diff_distrib [symmetric]
+  by (erule NSLIM_const [THEN NSLIM_mult])
 
 text \<open>Negation of function.\<close>
 lemma NSDERIV_minus: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. - f x) x :> - D"
@@ -227,22 +176,15 @@
 subsection \<open>Lemmas\<close>
 
 lemma NSDERIV_zero:
-  "NSDERIV g x :> D \<Longrightarrow> ( *f* g) (star_of x + xa) = star_of (g x) \<Longrightarrow>
-    xa \<in> Infinitesimal \<Longrightarrow> xa \<noteq> 0 \<Longrightarrow> D = 0"
-  apply (simp add: nsderiv_def)
-  apply (drule bspec)
-   apply auto
-  done
+  "\<lbrakk>NSDERIV g x :> D; ( *f* g) (star_of x + y) = star_of (g x); y \<in> Infinitesimal; y \<noteq> 0\<rbrakk>
+    \<Longrightarrow> D = 0"
+  by (force simp add: nsderiv_def)
 
 text \<open>Can be proved differently using \<open>NSLIM_isCont_iff\<close>.\<close>
 lemma NSDERIV_approx:
   "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
     ( *f* f) (star_of x + h) - star_of (f x) \<approx> 0"
-  apply (simp add: nsderiv_def)
-  apply (simp add: mem_infmal_iff [symmetric])
-  apply (rule Infinitesimal_ratio)
-    apply (rule_tac [3] approx_star_of_HFinite, auto)
-  done
+  by (meson DiffI Infinitesimal_ratio approx_star_of_HFinite mem_infmal_iff nsderiv_def singletonD)
 
 text \<open>From one version of differentiability
 
@@ -251,13 +193,13 @@
           \<open>x - a\<close>
 \<close>
 
-lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
-         ( *f* g) (star_of(x) + xa) \<noteq> star_of (g x);
-         ( *f* g) (star_of(x) + xa) \<approx> star_of (g x)
-      |] ==> (( *f* f) (( *f* g) (star_of(x) + xa))
-                   - star_of (f (g x)))
-              / (( *f* g) (star_of(x) + xa) - star_of (g x))
-             \<approx> star_of(Da)"
+lemma NSDERIVD1: 
+    "\<lbrakk>NSDERIV f (g x) :> Da;
+     ( *f* g) (star_of x + y) \<noteq> star_of (g x);
+     ( *f* g) (star_of x + y) \<approx> star_of (g x)\<rbrakk>
+    \<Longrightarrow> (( *f* f) (( *f* g) (star_of x + y)) -
+         star_of (f (g x))) / (( *f* g) (star_of x + y) - star_of (g x)) \<approx>
+        star_of Da"
   by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
 
 text \<open>From other version of differentiability
@@ -267,37 +209,15 @@
              \<open>h\<close>
 \<close>
 
-lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |]
-      ==> (( *f* g) (star_of(x) + xa) - star_of(g x)) / xa
+lemma NSDERIVD2: "[| NSDERIV g x :> Db; y \<in> Infinitesimal; y \<noteq> 0 |]
+      ==> (( *f* g) (star_of(x) + y) - star_of(g x)) / y
           \<approx> star_of(Db)"
   by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)
 
-lemma lemma_chain: "z \<noteq> 0 \<Longrightarrow> x * y = (x * inverse z) * (z * y)"
-  for x y z :: "'a::real_normed_field star"
-proof -
-  assume z: "z \<noteq> 0"
-  have "x * y = x * (inverse z * z) * y" by (simp add: z)
-  then show ?thesis by (simp add: mult.assoc)
-qed
-
 text \<open>This proof uses both definitions of differentiability.\<close>
 lemma NSDERIV_chain:
   "NSDERIV f (g x) :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (f \<circ> g) x :> Da * Db"
-  apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff [symmetric])
-  apply clarify
-  apply (frule_tac f = g in NSDERIV_approx)
-    apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
-  apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
-   apply (drule_tac g = g in NSDERIV_zero)
-      apply (auto simp add: divide_inverse)
-  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
-      in lemma_chain [THEN ssubst])
-   apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
-  apply (rule approx_mult_star_of)
-   apply (simp_all add: divide_inverse [symmetric])
-   apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
-  apply (blast intro: NSDERIVD2)
-  done
+  using DERIV_NS_iff DERIV_chain NSDERIV_NSLIM_iff by blast
 
 text \<open>Differentiation of natural number powers.\<close>
 lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1"
@@ -321,20 +241,17 @@
       by (rule Infinitesimal_HFinite_mult) simp
     with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx>
       inverse (- (star_of x * star_of x))"
-      apply -
-      apply (rule inverse_add_Infinitesimal_approx2)
-      apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
-        simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
-      done
+    proof -
+      have "- (h * star_of x) + - (star_of x * star_of x) \<approx> - (star_of x * star_of x)"
+        using \<open>h * star_of x \<in> Infinitesimal\<close> assms bex_Infinitesimal_iff by fastforce
+      then show ?thesis
+        by (metis assms mult_eq_0_iff neg_equal_0_iff_equal star_of_approx_inverse star_of_minus star_of_mult)
+    qed
     moreover from not_0 \<open>h \<noteq> 0\<close> assms
-    have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
-      (inverse (star_of x + h) - inverse (star_of x)) / h"
-      apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
-          nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
-      apply (subst nonzero_inverse_minus_eq [symmetric])
-      using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
-      apply (simp add: field_simps)
-      done
+    have "inverse (- (h * star_of x) + - (star_of x * star_of x)) 
+          = (inverse (star_of x + h) - inverse (star_of x)) / h"
+      by (simp add: division_ring_inverse_diff inverse_mult_distrib [symmetric]
+          inverse_minus_eq [symmetric] algebra_simps)
     ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
       - (inverse (star_of x) * inverse (star_of x))"
       using assms by simp
@@ -372,7 +289,7 @@
 
 lemma CARAT_NSDERIV:
   "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"
-  by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV mult.commute)
+  by (simp add: CARAT_DERIV NSDERIV_DERIV_iff isNSCont_isCont_iff)
 
 lemma hypreal_eq_minus_iff3: "x = y + z \<longleftrightarrow> x + - z = y"
   for x y z :: hypreal
@@ -414,30 +331,23 @@
 
 text \<open>The Increment theorem -- Keisler p. 65.\<close>
 lemma increment_thm:
-  "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
-    \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
-  apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
-  apply (drule bspec, auto)
-  apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
-  apply (frule_tac b1 = "hypreal_of_real D + y" in mult_right_cancel [THEN iffD2])
-   apply (erule_tac [2]
-      V = "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y"
-      in thin_rl)
-   apply assumption
-  apply (simp add: times_divide_eq_right [symmetric])
-  apply (auto simp add: distrib_right)
-  done
-
-lemma increment_thm2:
-  "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
-    \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
-  by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
+  assumes "NSDERIV f x :> D" "h \<in> Infinitesimal" "h \<noteq> 0"
+  shows "\<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
+proof -
+  have inc: "increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)"
+    using assms(1) incrementI2 by auto
+  have "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h \<approx> hypreal_of_real D"
+    by (simp add: NSDERIVD2 assms)
+  then obtain y where "y \<in> Infinitesimal" 
+    "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real D + y"
+    by (metis bex_Infinitesimal_iff2)
+  then have "increment f x h / h = hypreal_of_real D + y"
+    by (metis inc) 
+  then show ?thesis
+    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)
+qed
 
 lemma increment_approx_zero: "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow> increment f x h \<approx> 0"
-  apply (drule increment_thm2)
-    apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
-      simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
-  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
-  done
+  by (simp add: NSDERIV_approx incrementI2 mem_infmal_iff)
 
 end

--- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Jul 16 17:50:07 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Jul 16 23:33:38 2018 +0100
@@ -117,10 +117,7 @@
 
 lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \<approx> sumhr (0, N, f) \<Longrightarrow> \<bar>sumhr (M, N, f)\<bar> \<approx> 0"
   using linorder_less_linear [where x = M and y = N]
-  apply auto
-  apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
-  apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
-  done
+  by (metis (no_types, lifting) abs_zero approx_hrabs approx_minus_iff approx_refl approx_sym sumhr_eq_bounds sumhr_less_bounds_zero sumhr_split_diff)
 
 
 subsection \<open>Infinite sums: Standard and NS theorems\<close>
@@ -153,26 +150,16 @@
       summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
       NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
   apply (cut_tac x = M and y = N in linorder_less_linear)
-  apply auto
-   apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
-   apply (rule_tac [2] approx_minus_iff [THEN iffD2])
-   apply (auto dest: approx_hrabs_zero_cancel simp: sumhr_split_diff atLeast0LessThan[symmetric])
-  done
+  by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym sumhr_split_diff)
 
 text \<open>Terms of a convergent series tend to zero.\<close>
 lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
-  apply (drule bspec)
-   apply auto
-  apply (drule_tac x = "N + 1 " in bspec)
-   apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
-  done
+  by (metis HNatInfinite_add_one approx_hrabs_zero_cancel sumhr_Suc)
 
 text \<open>Nonstandard comparison test.\<close>
 lemma NSsummable_comparison_test: "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable f"
-  apply (fold summable_NSsummable_iff)
-  apply (rule summable_comparison_test, simp, assumption)
-  done
+  by (metis real_norm_def summable_NSsummable_iff summable_comparison_test)
 
 lemma NSsummable_rabs_comparison_test:
   "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable (\<lambda>k. \<bar>f k\<bar>)"