merged default tip
authorpaulson
Mon Jul 16 23:33:38 2018 +0100 (14 hours ago)
changeset 686455e15795788d3
parent 68643 3db6c9338ec1
parent 68644 242d298526a3
merged
     1.1 --- a/src/HOL/Deriv.thy	Mon Jul 16 17:50:07 2018 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Mon Jul 16 23:33:38 2018 +0100
     1.3 @@ -1086,7 +1086,7 @@
     1.4  
     1.5  text \<open>Caratheodory formulation of derivative at a point\<close>
     1.6  
     1.7 -lemma CARAT_DERIV: (*FIXME: SUPERSEDED BY THE ONE IN Deriv.thy. But still used by NSA/HDeriv.thy*)
     1.8 +lemma CARAT_DERIV:
     1.9    "(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)"
    1.10    (is "?lhs = ?rhs")
    1.11  proof
    1.12 @@ -1103,8 +1103,6 @@
    1.13    qed
    1.14  next
    1.15    assume ?rhs
    1.16 -  then obtain g where "(\<forall>z. f z - f x = g z * (z - x))" and "isCont g x" and "g x = l"
    1.17 -    by blast
    1.18    then show ?lhs
    1.19      by (auto simp add: isCont_iff DERIV_def cong: LIM_cong)
    1.20  qed
     2.1 --- a/src/HOL/Divides.thy	Mon Jul 16 17:50:07 2018 +0200
     2.2 +++ b/src/HOL/Divides.thy	Mon Jul 16 23:33:38 2018 +0100
     2.3 @@ -607,7 +607,7 @@
     2.4    shows "a div b < 0"
     2.5  proof -
     2.6    have "a div b \<le> - 1 div b"
     2.7 -    using Divides.zdiv_mono1 assms by auto
     2.8 +    using zdiv_mono1 assms by auto
     2.9    also have "... \<le> -1"
    2.10      by (simp add: assms(2) div_eq_minus1)
    2.11    finally show ?thesis 
     3.1 --- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Jul 16 17:50:07 2018 +0200
     3.2 +++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Jul 16 23:33:38 2018 +0100
     3.3 @@ -39,34 +39,26 @@
     3.4  
     3.5  lemma Infinitesimal_of_hypreal:
     3.6    "x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal"
     3.7 -  apply (rule InfinitesimalI2)
     3.8 -  apply (drule (1) InfinitesimalD2)
     3.9 -  apply (simp add: hnorm_of_hypreal)
    3.10 -  done
    3.11 +  by (metis Infinitesimal_of_hypreal_iff of_hypreal_def)
    3.12  
    3.13  lemma of_hypreal_eq_0_iff: "\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)"
    3.14    by transfer (rule of_real_eq_0_iff)
    3.15  
    3.16 -lemma NSDeriv_unique: "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
    3.17 -  apply (subgoal_tac "( *f* of_real) \<epsilon> \<in> Infinitesimal - {0::'a star}")
    3.18 -   apply (simp only: nsderiv_def)
    3.19 -   apply (drule (1) bspec)+
    3.20 -   apply (drule (1) approx_trans3)
    3.21 -   apply simp
    3.22 -  apply (simp add: Infinitesimal_of_hypreal)
    3.23 -  apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
    3.24 -  done
    3.25 +lemma NSDeriv_unique:
    3.26 +  assumes "NSDERIV f x :> D" "NSDERIV f x :> E"
    3.27 +  shows "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
    3.28 +proof -
    3.29 +  have "\<exists>s. (s::'a star) \<in> Infinitesimal - {0}"
    3.30 +    by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal hypreal_epsilon_not_zero singletonD)
    3.31 +  with assms show ?thesis
    3.32 +    by (meson approx_trans3 nsderiv_def star_of_approx_iff)
    3.33 +qed
    3.34  
    3.35  text \<open>First \<open>NSDERIV\<close> in terms of \<open>NSLIM\<close>.\<close>
    3.36  
    3.37  text \<open>First equivalence.\<close>
    3.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"
    3.39 -  apply (auto simp add: nsderiv_def NSLIM_def)
    3.40 -   apply (drule_tac x = xa in bspec)
    3.41 -    apply (rule_tac [3] ccontr)
    3.42 -    apply (drule_tac [3] x = h in spec)
    3.43 -    apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
    3.44 -  done
    3.45 +  by (auto simp add: nsderiv_def NSLIM_def starfun_lambda_cancel mem_infmal_iff)
    3.46  
    3.47  text \<open>Second equivalence.\<close>
    3.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"
    3.49 @@ -78,63 +70,39 @@
    3.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)"
    3.51    by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
    3.52  
    3.53 -(* FIXME delete *)
    3.54 -lemma hypreal_not_eq_minus_iff: "x \<noteq> a \<longleftrightarrow> x - a \<noteq> (0::'a::ab_group_add)"
    3.55 -  by auto
    3.56 -
    3.57  lemma NSDERIVD5:
    3.58 -  "(NSDERIV f x :> D) \<Longrightarrow>
    3.59 -   (\<forall>u. u \<approx> hypreal_of_real x \<longrightarrow>
    3.60 -     ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))"
    3.61 -  apply (auto simp add: NSDERIV_iff2)
    3.62 +  "\<lbrakk>NSDERIV f x :> D; u \<approx> hypreal_of_real x\<rbrakk> \<Longrightarrow>
    3.63 +     ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x)"
    3.64 +  unfolding NSDERIV_iff2
    3.65    apply (case_tac "u = hypreal_of_real x", auto)
    3.66 -  apply (drule_tac x = u in spec, auto)
    3.67 -  apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
    3.68 -   apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
    3.69 -   apply (subgoal_tac [2] "( *f* (\<lambda>z. z - x)) u \<noteq> (0::hypreal) ")
    3.70 -    apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
    3.71 -      Infinitesimal_subset_HFinite [THEN subsetD])
    3.72 -  done
    3.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)
    3.74  
    3.75  lemma NSDERIVD4:
    3.76 -  "(NSDERIV f x :> D) \<Longrightarrow>
    3.77 -    (\<forall>h \<in> Infinitesimal.
    3.78 -      ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h)"
    3.79 -  apply (auto simp add: nsderiv_def)
    3.80 -  apply (case_tac "h = 0")
    3.81 -   apply auto
    3.82 -  apply (drule_tac x = h in bspec)
    3.83 -   apply (drule_tac [2] c = h in approx_mult1)
    3.84 -    apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
    3.85 -  done
    3.86 -
    3.87 -lemma NSDERIVD3:
    3.88 -  "(NSDERIV f x :> D) \<Longrightarrow>
    3.89 -    \<forall>h \<in> Infinitesimal - {0}.
    3.90 -      (( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) \<approx> hypreal_of_real D * h"
    3.91 -  apply (auto simp add: nsderiv_def)
    3.92 -  apply (rule ccontr, drule_tac x = h in bspec)
    3.93 -   apply (drule_tac [2] c = h in approx_mult1)
    3.94 -    apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
    3.95 -  done
    3.96 +  "\<lbrakk>NSDERIV f x :> D; h \<in> Infinitesimal\<rbrakk>
    3.97 +    \<Longrightarrow> ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h"
    3.98 +  apply (clarsimp simp add: nsderiv_def)
    3.99 +  apply (case_tac "h = 0", simp)
   3.100 +  by (meson DiffI Infinitesimal_approx Infinitesimal_ratio Infinitesimal_star_of_mult2 approx_star_of_HFinite singletonD)
   3.101  
   3.102  text \<open>Differentiability implies continuity nice and simple "algebraic" proof.\<close>
   3.103 -lemma NSDERIV_isNSCont: "NSDERIV f x :> D \<Longrightarrow> isNSCont f x"
   3.104 -  apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
   3.105 -  apply (drule approx_minus_iff [THEN iffD1])
   3.106 -  apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
   3.107 -  apply (drule_tac x = "xa - star_of x" in bspec)
   3.108 -   prefer 2 apply (simp add: add.assoc [symmetric])
   3.109 -   apply (auto simp add: mem_infmal_iff [symmetric] add.commute)
   3.110 -  apply (drule_tac c = "xa - star_of x" in approx_mult1)
   3.111 -   apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
   3.112 -  apply (drule_tac x3=D in
   3.113 -      HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult, THEN mem_infmal_iff [THEN iffD1]])
   3.114 -  apply (auto simp add: mult.commute intro: approx_trans approx_minus_iff [THEN iffD2])
   3.115 -  done
   3.116 +lemma NSDERIV_isNSCont: 
   3.117 +  assumes "NSDERIV f x :> D" shows "isNSCont f x"
   3.118 +  unfolding isNSCont_NSLIM_iff NSLIM_def
   3.119 +proof clarify
   3.120 +  fix x'
   3.121 +  assume "x' \<noteq> star_of x" "x' \<approx> star_of x"
   3.122 +  then have m0: "x' - star_of x \<in> Infinitesimal - {0}"
   3.123 +    using bex_Infinitesimal_iff by auto
   3.124 +  then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<approx> star_of D"
   3.125 +    by (metis \<open>x' \<approx> star_of x\<close> add_diff_cancel_left' assms bex_Infinitesimal_iff2 nsderiv_def)
   3.126 +  then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<in> HFinite"
   3.127 +    by (metis approx_star_of_HFinite)  
   3.128 +  then show "( *f* f) x' \<approx> star_of (f x)"
   3.129 +    by (metis (no_types) Diff_iff Infinitesimal_ratio m0 bex_Infinitesimal_iff insert_iff)
   3.130 +qed
   3.131  
   3.132  text \<open>Differentiation rules for combinations of functions
   3.133 -  follow from clear, straightforard, algebraic manipulations.\<close>
   3.134 +  follow from clear, straightforward, algebraic manipulations.\<close>
   3.135  
   3.136  text \<open>Constant function.\<close>
   3.137  
   3.138 @@ -145,53 +113,34 @@
   3.139  text \<open>Sum of functions- proved easily.\<close>
   3.140  
   3.141  lemma NSDERIV_add:
   3.142 -  "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x + g x) x :> Da + Db"
   3.143 -  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   3.144 -  apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
   3.145 -  apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
   3.146 -   apply (auto simp add: ac_simps algebra_simps)
   3.147 -  done
   3.148 +  assumes "NSDERIV f x :> Da" "NSDERIV g x :> Db"
   3.149 +  shows "NSDERIV (\<lambda>x. f x + g x) x :> Da + Db"
   3.150 +proof -
   3.151 +  have "((\<lambda>x. f x + g x) has_field_derivative Da + Db) (at x)"
   3.152 +    using assms DERIV_NS_iff NSDERIV_NSLIM_iff field_differentiable_add by blast
   3.153 +  then show ?thesis
   3.154 +    by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff)
   3.155 +qed
   3.156  
   3.157 -text \<open>Product of functions - Proof is trivial but tedious
   3.158 -  and long due to rearrangement of terms.\<close>
   3.159 -
   3.160 -lemma lemma_nsderiv1: "(a * b) - (c * d) = (b * (a - c)) + (c * (b - d))"
   3.161 -  for a b c d :: "'a::comm_ring star"
   3.162 -  by (simp add: right_diff_distrib ac_simps)
   3.163 -
   3.164 -lemma lemma_nsderiv2: "(x - y) / z = star_of D + yb \<Longrightarrow> z \<noteq> 0 \<Longrightarrow>
   3.165 -  z \<in> Infinitesimal \<Longrightarrow> yb \<in> Infinitesimal \<Longrightarrow> x - y \<approx> 0"
   3.166 -  for x y z :: "'a::real_normed_field star"
   3.167 -  apply (simp add: nonzero_divide_eq_eq)
   3.168 -  apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
   3.169 -      simp add: mult.assoc mem_infmal_iff [symmetric])
   3.170 -  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   3.171 -  done
   3.172 +text \<open>Product of functions - Proof is simple.\<close>
   3.173  
   3.174  lemma NSDERIV_mult:
   3.175 -  "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow>
   3.176 -    NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)"
   3.177 -  apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   3.178 -  apply (auto dest!: spec simp add: starfun_lambda_cancel lemma_nsderiv1)
   3.179 -  apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
   3.180 -  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   3.181 -  apply (auto simp add: times_divide_eq_right [symmetric]
   3.182 -      simp del: times_divide_eq_right times_divide_eq_left)
   3.183 -  apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
   3.184 -  apply (drule_tac approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
   3.185 -  apply (auto intro!: approx_add_mono1 simp: distrib_right distrib_left mult.commute add.assoc)
   3.186 -  apply (rule_tac b1 = "star_of Db * star_of (f x)" in add.commute [THEN subst])
   3.187 -  apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
   3.188 -      Infinitesimal_add Infinitesimal_mult Infinitesimal_star_of_mult Infinitesimal_star_of_mult2
   3.189 -      simp add: add.assoc [symmetric])
   3.190 -  done
   3.191 +  assumes "NSDERIV g x :> Db" "NSDERIV f x :> Da"
   3.192 +  shows "NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)"
   3.193 +proof -
   3.194 +  have "(f has_field_derivative Da) (at x)" "(g has_field_derivative Db) (at x)"
   3.195 +    using assms by (simp_all add: DERIV_NS_iff NSDERIV_NSLIM_iff)
   3.196 +  then have "((\<lambda>a. f a * g a) has_field_derivative Da * g x + Db * f x) (at x)"
   3.197 +    using DERIV_mult by blast
   3.198 +  then show ?thesis
   3.199 +    by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff)
   3.200 +qed
   3.201  
   3.202  text \<open>Multiplying by a constant.\<close>
   3.203  lemma NSDERIV_cmult: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. c * f x) x :> c * D"
   3.204 -  apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
   3.205 -      minus_mult_right right_diff_distrib [symmetric])
   3.206 -  apply (erule NSLIM_const [THEN NSLIM_mult])
   3.207 -  done
   3.208 +  unfolding times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
   3.209 +      minus_mult_right right_diff_distrib [symmetric]
   3.210 +  by (erule NSLIM_const [THEN NSLIM_mult])
   3.211  
   3.212  text \<open>Negation of function.\<close>
   3.213  lemma NSDERIV_minus: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. - f x) x :> - D"
   3.214 @@ -227,22 +176,15 @@
   3.215  subsection \<open>Lemmas\<close>
   3.216  
   3.217  lemma NSDERIV_zero:
   3.218 -  "NSDERIV g x :> D \<Longrightarrow> ( *f* g) (star_of x + xa) = star_of (g x) \<Longrightarrow>
   3.219 -    xa \<in> Infinitesimal \<Longrightarrow> xa \<noteq> 0 \<Longrightarrow> D = 0"
   3.220 -  apply (simp add: nsderiv_def)
   3.221 -  apply (drule bspec)
   3.222 -   apply auto
   3.223 -  done
   3.224 +  "\<lbrakk>NSDERIV g x :> D; ( *f* g) (star_of x + y) = star_of (g x); y \<in> Infinitesimal; y \<noteq> 0\<rbrakk>
   3.225 +    \<Longrightarrow> D = 0"
   3.226 +  by (force simp add: nsderiv_def)
   3.227  
   3.228  text \<open>Can be proved differently using \<open>NSLIM_isCont_iff\<close>.\<close>
   3.229  lemma NSDERIV_approx:
   3.230    "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
   3.231      ( *f* f) (star_of x + h) - star_of (f x) \<approx> 0"
   3.232 -  apply (simp add: nsderiv_def)
   3.233 -  apply (simp add: mem_infmal_iff [symmetric])
   3.234 -  apply (rule Infinitesimal_ratio)
   3.235 -    apply (rule_tac [3] approx_star_of_HFinite, auto)
   3.236 -  done
   3.237 +  by (meson DiffI Infinitesimal_ratio approx_star_of_HFinite mem_infmal_iff nsderiv_def singletonD)
   3.238  
   3.239  text \<open>From one version of differentiability
   3.240  
   3.241 @@ -251,13 +193,13 @@
   3.242            \<open>x - a\<close>
   3.243  \<close>
   3.244  
   3.245 -lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
   3.246 -         ( *f* g) (star_of(x) + xa) \<noteq> star_of (g x);
   3.247 -         ( *f* g) (star_of(x) + xa) \<approx> star_of (g x)
   3.248 -      |] ==> (( *f* f) (( *f* g) (star_of(x) + xa))
   3.249 -                   - star_of (f (g x)))
   3.250 -              / (( *f* g) (star_of(x) + xa) - star_of (g x))
   3.251 -             \<approx> star_of(Da)"
   3.252 +lemma NSDERIVD1: 
   3.253 +    "\<lbrakk>NSDERIV f (g x) :> Da;
   3.254 +     ( *f* g) (star_of x + y) \<noteq> star_of (g x);
   3.255 +     ( *f* g) (star_of x + y) \<approx> star_of (g x)\<rbrakk>
   3.256 +    \<Longrightarrow> (( *f* f) (( *f* g) (star_of x + y)) -
   3.257 +         star_of (f (g x))) / (( *f* g) (star_of x + y) - star_of (g x)) \<approx>
   3.258 +        star_of Da"
   3.259    by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
   3.260  
   3.261  text \<open>From other version of differentiability
   3.262 @@ -267,37 +209,15 @@
   3.263               \<open>h\<close>
   3.264  \<close>
   3.265  
   3.266 -lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |]
   3.267 -      ==> (( *f* g) (star_of(x) + xa) - star_of(g x)) / xa
   3.268 +lemma NSDERIVD2: "[| NSDERIV g x :> Db; y \<in> Infinitesimal; y \<noteq> 0 |]
   3.269 +      ==> (( *f* g) (star_of(x) + y) - star_of(g x)) / y
   3.270            \<approx> star_of(Db)"
   3.271    by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)
   3.272  
   3.273 -lemma lemma_chain: "z \<noteq> 0 \<Longrightarrow> x * y = (x * inverse z) * (z * y)"
   3.274 -  for x y z :: "'a::real_normed_field star"
   3.275 -proof -
   3.276 -  assume z: "z \<noteq> 0"
   3.277 -  have "x * y = x * (inverse z * z) * y" by (simp add: z)
   3.278 -  then show ?thesis by (simp add: mult.assoc)
   3.279 -qed
   3.280 -
   3.281  text \<open>This proof uses both definitions of differentiability.\<close>
   3.282  lemma NSDERIV_chain:
   3.283    "NSDERIV f (g x) :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (f \<circ> g) x :> Da * Db"
   3.284 -  apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff [symmetric])
   3.285 -  apply clarify
   3.286 -  apply (frule_tac f = g in NSDERIV_approx)
   3.287 -    apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
   3.288 -  apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
   3.289 -   apply (drule_tac g = g in NSDERIV_zero)
   3.290 -      apply (auto simp add: divide_inverse)
   3.291 -  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
   3.292 -      in lemma_chain [THEN ssubst])
   3.293 -   apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
   3.294 -  apply (rule approx_mult_star_of)
   3.295 -   apply (simp_all add: divide_inverse [symmetric])
   3.296 -   apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
   3.297 -  apply (blast intro: NSDERIVD2)
   3.298 -  done
   3.299 +  using DERIV_NS_iff DERIV_chain NSDERIV_NSLIM_iff by blast
   3.300  
   3.301  text \<open>Differentiation of natural number powers.\<close>
   3.302  lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1"
   3.303 @@ -321,20 +241,17 @@
   3.304        by (rule Infinitesimal_HFinite_mult) simp
   3.305      with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx>
   3.306        inverse (- (star_of x * star_of x))"
   3.307 -      apply -
   3.308 -      apply (rule inverse_add_Infinitesimal_approx2)
   3.309 -      apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
   3.310 -        simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
   3.311 -      done
   3.312 +    proof -
   3.313 +      have "- (h * star_of x) + - (star_of x * star_of x) \<approx> - (star_of x * star_of x)"
   3.314 +        using \<open>h * star_of x \<in> Infinitesimal\<close> assms bex_Infinitesimal_iff by fastforce
   3.315 +      then show ?thesis
   3.316 +        by (metis assms mult_eq_0_iff neg_equal_0_iff_equal star_of_approx_inverse star_of_minus star_of_mult)
   3.317 +    qed
   3.318      moreover from not_0 \<open>h \<noteq> 0\<close> assms
   3.319 -    have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
   3.320 -      (inverse (star_of x + h) - inverse (star_of x)) / h"
   3.321 -      apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
   3.322 -          nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
   3.323 -      apply (subst nonzero_inverse_minus_eq [symmetric])
   3.324 -      using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
   3.325 -      apply (simp add: field_simps)
   3.326 -      done
   3.327 +    have "inverse (- (h * star_of x) + - (star_of x * star_of x)) 
   3.328 +          = (inverse (star_of x + h) - inverse (star_of x)) / h"
   3.329 +      by (simp add: division_ring_inverse_diff inverse_mult_distrib [symmetric]
   3.330 +          inverse_minus_eq [symmetric] algebra_simps)
   3.331      ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
   3.332        - (inverse (star_of x) * inverse (star_of x))"
   3.333        using assms by simp
   3.334 @@ -372,7 +289,7 @@
   3.335  
   3.336  lemma CARAT_NSDERIV:
   3.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"
   3.338 -  by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV mult.commute)
   3.339 +  by (simp add: CARAT_DERIV NSDERIV_DERIV_iff isNSCont_isCont_iff)
   3.340  
   3.341  lemma hypreal_eq_minus_iff3: "x = y + z \<longleftrightarrow> x + - z = y"
   3.342    for x y z :: hypreal
   3.343 @@ -414,30 +331,23 @@
   3.344  
   3.345  text \<open>The Increment theorem -- Keisler p. 65.\<close>
   3.346  lemma increment_thm:
   3.347 -  "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
   3.348 -    \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
   3.349 -  apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
   3.350 -  apply (drule bspec, auto)
   3.351 -  apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
   3.352 -  apply (frule_tac b1 = "hypreal_of_real D + y" in mult_right_cancel [THEN iffD2])
   3.353 -   apply (erule_tac [2]
   3.354 -      V = "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y"
   3.355 -      in thin_rl)
   3.356 -   apply assumption
   3.357 -  apply (simp add: times_divide_eq_right [symmetric])
   3.358 -  apply (auto simp add: distrib_right)
   3.359 -  done
   3.360 -
   3.361 -lemma increment_thm2:
   3.362 -  "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
   3.363 -    \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
   3.364 -  by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
   3.365 +  assumes "NSDERIV f x :> D" "h \<in> Infinitesimal" "h \<noteq> 0"
   3.366 +  shows "\<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
   3.367 +proof -
   3.368 +  have inc: "increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)"
   3.369 +    using assms(1) incrementI2 by auto
   3.370 +  have "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h \<approx> hypreal_of_real D"
   3.371 +    by (simp add: NSDERIVD2 assms)
   3.372 +  then obtain y where "y \<in> Infinitesimal" 
   3.373 +    "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real D + y"
   3.374 +    by (metis bex_Infinitesimal_iff2)
   3.375 +  then have "increment f x h / h = hypreal_of_real D + y"
   3.376 +    by (metis inc) 
   3.377 +  then show ?thesis
   3.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)
   3.379 +qed
   3.380  
   3.381  lemma increment_approx_zero: "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow> increment f x h \<approx> 0"
   3.382 -  apply (drule increment_thm2)
   3.383 -    apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
   3.384 -      simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
   3.385 -  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   3.386 -  done
   3.387 +  by (simp add: NSDERIV_approx incrementI2 mem_infmal_iff)
   3.388  
   3.389  end
     4.1 --- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Jul 16 17:50:07 2018 +0200
     4.2 +++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Mon Jul 16 23:33:38 2018 +0100
     4.3 @@ -117,10 +117,7 @@
     4.4  
     4.5  lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \<approx> sumhr (0, N, f) \<Longrightarrow> \<bar>sumhr (M, N, f)\<bar> \<approx> 0"
     4.6    using linorder_less_linear [where x = M and y = N]
     4.7 -  apply auto
     4.8 -  apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
     4.9 -  apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
    4.10 -  done
    4.11 +  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)
    4.12  
    4.13  
    4.14  subsection \<open>Infinite sums: Standard and NS theorems\<close>
    4.15 @@ -153,26 +150,16 @@
    4.16        summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
    4.17        NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
    4.18    apply (cut_tac x = M and y = N in linorder_less_linear)
    4.19 -  apply auto
    4.20 -   apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
    4.21 -   apply (rule_tac [2] approx_minus_iff [THEN iffD2])
    4.22 -   apply (auto dest: approx_hrabs_zero_cancel simp: sumhr_split_diff atLeast0LessThan[symmetric])
    4.23 -  done
    4.24 +  by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym sumhr_split_diff)
    4.25  
    4.26  text \<open>Terms of a convergent series tend to zero.\<close>
    4.27  lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
    4.28    apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
    4.29 -  apply (drule bspec)
    4.30 -   apply auto
    4.31 -  apply (drule_tac x = "N + 1 " in bspec)
    4.32 -   apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
    4.33 -  done
    4.34 +  by (metis HNatInfinite_add_one approx_hrabs_zero_cancel sumhr_Suc)
    4.35  
    4.36  text \<open>Nonstandard comparison test.\<close>
    4.37  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"
    4.38 -  apply (fold summable_NSsummable_iff)
    4.39 -  apply (rule summable_comparison_test, simp, assumption)
    4.40 -  done
    4.41 +  by (metis real_norm_def summable_NSsummable_iff summable_comparison_test)
    4.42  
    4.43  lemma NSsummable_rabs_comparison_test:
    4.44    "\<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>)"