src/HOL/Nonstandard_Analysis/HDeriv.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64604 2bf8cfc98c4d
child 67399 eab6ce8368fa
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Nonstandard_Analysis/HDeriv.thy
     2     Author:     Jacques D. Fleuriot
     3     Copyright:  1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     6 
     7 section \<open>Differentiation (Nonstandard)\<close>
     8 
     9 theory HDeriv
    10   imports HLim
    11 begin
    12 
    13 text \<open>Nonstandard Definitions.\<close>
    14 
    15 definition nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
    16     ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
    17   where "NSDERIV f x :> D \<longleftrightarrow>
    18     (\<forall>h \<in> Infinitesimal - {0}. (( *f* f)(star_of x + h) - star_of (f x)) / h \<approx> star_of D)"
    19 
    20 definition NSdifferentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
    21     (infixl "NSdifferentiable" 60)
    22   where "f NSdifferentiable x \<longleftrightarrow> (\<exists>D. NSDERIV f x :> D)"
    23 
    24 definition increment :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> hypreal \<Rightarrow> hypreal"
    25   where "increment f x h =
    26     (SOME inc. f NSdifferentiable x \<and> inc = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x))"
    27 
    28 
    29 subsection \<open>Derivatives\<close>
    30 
    31 lemma DERIV_NS_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
    32   by (simp add: DERIV_def LIM_NSLIM_iff)
    33 
    34 lemma NS_DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
    35   by (simp add: DERIV_def LIM_NSLIM_iff)
    36 
    37 lemma hnorm_of_hypreal: "\<And>r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \<bar>r\<bar>"
    38   by transfer (rule norm_of_real)
    39 
    40 lemma Infinitesimal_of_hypreal:
    41   "x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal"
    42   apply (rule InfinitesimalI2)
    43   apply (drule (1) InfinitesimalD2)
    44   apply (simp add: hnorm_of_hypreal)
    45   done
    46 
    47 lemma of_hypreal_eq_0_iff: "\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)"
    48   by transfer (rule of_real_eq_0_iff)
    49 
    50 lemma NSDeriv_unique: "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
    51   apply (subgoal_tac "( *f* of_real) \<epsilon> \<in> Infinitesimal - {0::'a star}")
    52    apply (simp only: nsderiv_def)
    53    apply (drule (1) bspec)+
    54    apply (drule (1) approx_trans3)
    55    apply simp
    56   apply (simp add: Infinitesimal_of_hypreal)
    57   apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
    58   done
    59 
    60 text \<open>First \<open>NSDERIV\<close> in terms of \<open>NSLIM\<close>.\<close>
    61 
    62 text \<open>First equivalence.\<close>
    63 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"
    64   apply (auto simp add: nsderiv_def NSLIM_def)
    65    apply (drule_tac x = xa in bspec)
    66     apply (rule_tac [3] ccontr)
    67     apply (drule_tac [3] x = h in spec)
    68     apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
    69   done
    70 
    71 text \<open>Second equivalence.\<close>
    72 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"
    73   by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
    74 
    75 text \<open>While we're at it!\<close>
    76 lemma NSDERIV_iff2:
    77   "(NSDERIV f x :> D) \<longleftrightarrow>
    78     (\<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)"
    79   by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
    80 
    81 (* FIXME delete *)
    82 lemma hypreal_not_eq_minus_iff: "x \<noteq> a \<longleftrightarrow> x - a \<noteq> (0::'a::ab_group_add)"
    83   by auto
    84 
    85 lemma NSDERIVD5:
    86   "(NSDERIV f x :> D) \<Longrightarrow>
    87    (\<forall>u. u \<approx> hypreal_of_real x \<longrightarrow>
    88      ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))"
    89   apply (auto simp add: NSDERIV_iff2)
    90   apply (case_tac "u = hypreal_of_real x", auto)
    91   apply (drule_tac x = u in spec, auto)
    92   apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
    93    apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
    94    apply (subgoal_tac [2] "( *f* (\<lambda>z. z - x)) u \<noteq> (0::hypreal) ")
    95     apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
    96       Infinitesimal_subset_HFinite [THEN subsetD])
    97   done
    98 
    99 lemma NSDERIVD4:
   100   "(NSDERIV f x :> D) \<Longrightarrow>
   101     (\<forall>h \<in> Infinitesimal.
   102       ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h)"
   103   apply (auto simp add: nsderiv_def)
   104   apply (case_tac "h = 0")
   105    apply auto
   106   apply (drule_tac x = h in bspec)
   107    apply (drule_tac [2] c = h in approx_mult1)
   108     apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
   109   done
   110 
   111 lemma NSDERIVD3:
   112   "(NSDERIV f x :> D) \<Longrightarrow>
   113     \<forall>h \<in> Infinitesimal - {0}.
   114       (( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) \<approx> hypreal_of_real D * h"
   115   apply (auto simp add: nsderiv_def)
   116   apply (rule ccontr, drule_tac x = h in bspec)
   117    apply (drule_tac [2] c = h in approx_mult1)
   118     apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
   119   done
   120 
   121 text \<open>Differentiability implies continuity nice and simple "algebraic" proof.\<close>
   122 lemma NSDERIV_isNSCont: "NSDERIV f x :> D \<Longrightarrow> isNSCont f x"
   123   apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
   124   apply (drule approx_minus_iff [THEN iffD1])
   125   apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
   126   apply (drule_tac x = "xa - star_of x" in bspec)
   127    prefer 2 apply (simp add: add.assoc [symmetric])
   128    apply (auto simp add: mem_infmal_iff [symmetric] add.commute)
   129   apply (drule_tac c = "xa - star_of x" in approx_mult1)
   130    apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
   131   apply (drule_tac x3=D in
   132       HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult, THEN mem_infmal_iff [THEN iffD1]])
   133   apply (auto simp add: mult.commute intro: approx_trans approx_minus_iff [THEN iffD2])
   134   done
   135 
   136 text \<open>Differentiation rules for combinations of functions
   137   follow from clear, straightforard, algebraic manipulations.\<close>
   138 
   139 text \<open>Constant function.\<close>
   140 
   141 (* use simple constant nslimit theorem *)
   142 lemma NSDERIV_const [simp]: "NSDERIV (\<lambda>x. k) x :> 0"
   143   by (simp add: NSDERIV_NSLIM_iff)
   144 
   145 text \<open>Sum of functions- proved easily.\<close>
   146 
   147 lemma NSDERIV_add:
   148   "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x + g x) x :> Da + Db"
   149   apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   150   apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
   151   apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
   152    apply (auto simp add: ac_simps algebra_simps)
   153   done
   154 
   155 text \<open>Product of functions - Proof is trivial but tedious
   156   and long due to rearrangement of terms.\<close>
   157 
   158 lemma lemma_nsderiv1: "(a * b) - (c * d) = (b * (a - c)) + (c * (b - d))"
   159   for a b c d :: "'a::comm_ring star"
   160   by (simp add: right_diff_distrib ac_simps)
   161 
   162 lemma lemma_nsderiv2: "(x - y) / z = star_of D + yb \<Longrightarrow> z \<noteq> 0 \<Longrightarrow>
   163   z \<in> Infinitesimal \<Longrightarrow> yb \<in> Infinitesimal \<Longrightarrow> x - y \<approx> 0"
   164   for x y z :: "'a::real_normed_field star"
   165   apply (simp add: nonzero_divide_eq_eq)
   166   apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
   167       simp add: mult.assoc mem_infmal_iff [symmetric])
   168   apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   169   done
   170 
   171 lemma NSDERIV_mult:
   172   "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow>
   173     NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)"
   174   apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
   175   apply (auto dest!: spec simp add: starfun_lambda_cancel lemma_nsderiv1)
   176   apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
   177   apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   178   apply (auto simp add: times_divide_eq_right [symmetric]
   179       simp del: times_divide_eq_right times_divide_eq_left)
   180   apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
   181   apply (drule_tac approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
   182   apply (auto intro!: approx_add_mono1 simp: distrib_right distrib_left mult.commute add.assoc)
   183   apply (rule_tac b1 = "star_of Db * star_of (f x)" in add.commute [THEN subst])
   184   apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
   185       Infinitesimal_add Infinitesimal_mult Infinitesimal_star_of_mult Infinitesimal_star_of_mult2
   186       simp add: add.assoc [symmetric])
   187   done
   188 
   189 text \<open>Multiplying by a constant.\<close>
   190 lemma NSDERIV_cmult: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. c * f x) x :> c * D"
   191   apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
   192       minus_mult_right right_diff_distrib [symmetric])
   193   apply (erule NSLIM_const [THEN NSLIM_mult])
   194   done
   195 
   196 text \<open>Negation of function.\<close>
   197 lemma NSDERIV_minus: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. - f x) x :> - D"
   198 proof (simp add: NSDERIV_NSLIM_iff)
   199   assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
   200   then have deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D"
   201     by (rule NSLIM_minus)
   202   have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
   203     by (simp add: minus_divide_left)
   204   with deriv have "(\<lambda>h. (- f (x + h) + f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D"
   205     by simp
   206   then show "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D \<Longrightarrow> (\<lambda>h. (f x - f (x + h)) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D"
   207     by simp
   208 qed
   209 
   210 text \<open>Subtraction.\<close>
   211 lemma NSDERIV_add_minus:
   212   "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x + - g x) x :> Da + - Db"
   213   by (blast dest: NSDERIV_add NSDERIV_minus)
   214 
   215 lemma NSDERIV_diff:
   216   "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x - g x) x :> Da - Db"
   217   using NSDERIV_add_minus [of f x Da g Db] by simp
   218 
   219 text \<open>Similarly to the above, the chain rule admits an entirely
   220   straightforward derivation. Compare this with Harrison's
   221   HOL proof of the chain rule, which proved to be trickier and
   222   required an alternative characterisation of differentiability-
   223   the so-called Carathedory derivative. Our main problem is
   224   manipulation of terms.\<close>
   225 
   226 
   227 subsection \<open>Lemmas\<close>
   228 
   229 lemma NSDERIV_zero:
   230   "NSDERIV g x :> D \<Longrightarrow> ( *f* g) (star_of x + xa) = star_of (g x) \<Longrightarrow>
   231     xa \<in> Infinitesimal \<Longrightarrow> xa \<noteq> 0 \<Longrightarrow> D = 0"
   232   apply (simp add: nsderiv_def)
   233   apply (drule bspec)
   234    apply auto
   235   done
   236 
   237 text \<open>Can be proved differently using \<open>NSLIM_isCont_iff\<close>.\<close>
   238 lemma NSDERIV_approx:
   239   "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
   240     ( *f* f) (star_of x + h) - star_of (f x) \<approx> 0"
   241   apply (simp add: nsderiv_def)
   242   apply (simp add: mem_infmal_iff [symmetric])
   243   apply (rule Infinitesimal_ratio)
   244     apply (rule_tac [3] approx_star_of_HFinite, auto)
   245   done
   246 
   247 text \<open>From one version of differentiability
   248 
   249         \<open>f x - f a\<close>
   250       \<open>-------------- \<approx> Db\<close>
   251           \<open>x - a\<close>
   252 \<close>
   253 
   254 lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
   255          ( *f* g) (star_of(x) + xa) \<noteq> star_of (g x);
   256          ( *f* g) (star_of(x) + xa) \<approx> star_of (g x)
   257       |] ==> (( *f* f) (( *f* g) (star_of(x) + xa))
   258                    - star_of (f (g x)))
   259               / (( *f* g) (star_of(x) + xa) - star_of (g x))
   260              \<approx> star_of(Da)"
   261   by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
   262 
   263 text \<open>From other version of differentiability
   264 
   265       \<open>f (x + h) - f x\<close>
   266      \<open>------------------ \<approx> Db\<close>
   267              \<open>h\<close>
   268 \<close>
   269 
   270 lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |]
   271       ==> (( *f* g) (star_of(x) + xa) - star_of(g x)) / xa
   272           \<approx> star_of(Db)"
   273   by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)
   274 
   275 lemma lemma_chain: "z \<noteq> 0 \<Longrightarrow> x * y = (x * inverse z) * (z * y)"
   276   for x y z :: "'a::real_normed_field star"
   277 proof -
   278   assume z: "z \<noteq> 0"
   279   have "x * y = x * (inverse z * z) * y" by (simp add: z)
   280   then show ?thesis by (simp add: mult.assoc)
   281 qed
   282 
   283 text \<open>This proof uses both definitions of differentiability.\<close>
   284 lemma NSDERIV_chain:
   285   "NSDERIV f (g x) :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (f \<circ> g) x :> Da * Db"
   286   apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff [symmetric])
   287   apply clarify
   288   apply (frule_tac f = g in NSDERIV_approx)
   289     apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
   290   apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
   291    apply (drule_tac g = g in NSDERIV_zero)
   292       apply (auto simp add: divide_inverse)
   293   apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
   294       in lemma_chain [THEN ssubst])
   295    apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
   296   apply (rule approx_mult_star_of)
   297    apply (simp_all add: divide_inverse [symmetric])
   298    apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
   299   apply (blast intro: NSDERIVD2)
   300   done
   301 
   302 text \<open>Differentiation of natural number powers.\<close>
   303 lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1"
   304   by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
   305 
   306 lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
   307   using NSDERIV_Id [THEN NSDERIV_cmult] by simp
   308 
   309 lemma NSDERIV_inverse:
   310   fixes x :: "'a::real_normed_field"
   311   assumes "x \<noteq> 0" \<comment> \<open>can't get rid of @{term "x \<noteq> 0"} because it isn't continuous at zero\<close>
   312   shows "NSDERIV (\<lambda>x. inverse x) x :> - (inverse x ^ Suc (Suc 0))"
   313 proof -
   314   {
   315     fix h :: "'a star"
   316     assume h_Inf: "h \<in> Infinitesimal"
   317     from this assms have not_0: "star_of x + h \<noteq> 0"
   318       by (rule Infinitesimal_add_not_zero)
   319     assume "h \<noteq> 0"
   320     from h_Inf have "h * star_of x \<in> Infinitesimal"
   321       by (rule Infinitesimal_HFinite_mult) simp
   322     with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx>
   323       inverse (- (star_of x * star_of x))"
   324       apply -
   325       apply (rule inverse_add_Infinitesimal_approx2)
   326       apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
   327         simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
   328       done
   329     moreover from not_0 \<open>h \<noteq> 0\<close> assms
   330     have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
   331       (inverse (star_of x + h) - inverse (star_of x)) / h"
   332       apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
   333           nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
   334       apply (subst nonzero_inverse_minus_eq [symmetric])
   335       using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
   336       apply (simp add: field_simps)
   337       done
   338     ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
   339       - (inverse (star_of x) * inverse (star_of x))"
   340       using assms by simp
   341   }
   342   then show ?thesis by (simp add: nsderiv_def)
   343 qed
   344 
   345 
   346 subsubsection \<open>Equivalence of NS and Standard definitions\<close>
   347 
   348 lemma divideR_eq_divide: "x /\<^sub>R y = x / y"
   349   by (simp add: divide_inverse mult.commute)
   350 
   351 text \<open>Now equivalence between \<open>NSDERIV\<close> and \<open>DERIV\<close>.\<close>
   352 lemma NSDERIV_DERIV_iff: "NSDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   353   by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
   354 
   355 text \<open>NS version.\<close>
   356 lemma NSDERIV_pow: "NSDERIV (\<lambda>x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
   357   by (simp add: NSDERIV_DERIV_iff DERIV_pow)
   358 
   359 text \<open>Derivative of inverse.\<close>
   360 lemma NSDERIV_inverse_fun:
   361   "NSDERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
   362     NSDERIV (\<lambda>x. inverse (f x)) x :> (- (d * inverse (f x ^ Suc (Suc 0))))"
   363   for x :: "'a::{real_normed_field}"
   364   by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
   365 
   366 text \<open>Derivative of quotient.\<close>
   367 lemma NSDERIV_quotient:
   368   fixes x :: "'a::real_normed_field"
   369   shows "NSDERIV f x :> d \<Longrightarrow> NSDERIV g x :> e \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
   370     NSDERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))"
   371   by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: power_Suc)
   372 
   373 lemma CARAT_NSDERIV:
   374   "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"
   375   by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV mult.commute)
   376 
   377 lemma hypreal_eq_minus_iff3: "x = y + z \<longleftrightarrow> x + - z = y"
   378   for x y z :: hypreal
   379   by auto
   380 
   381 lemma CARAT_DERIVD:
   382   assumes all: "\<forall>z. f z - f x = g z * (z - x)"
   383     and nsc: "isNSCont g x"
   384   shows "NSDERIV f x :> g x"
   385 proof -
   386   from nsc have "\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow>
   387        ( *f* g) w * (w - star_of x) / (w - star_of x) \<approx> star_of (g x)"
   388     by (simp add: isNSCont_def)
   389   with all show ?thesis
   390     by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
   391 qed
   392 
   393 
   394 subsubsection \<open>Differentiability predicate\<close>
   395 
   396 lemma NSdifferentiableD: "f NSdifferentiable x \<Longrightarrow> \<exists>D. NSDERIV f x :> D"
   397   by (simp add: NSdifferentiable_def)
   398 
   399 lemma NSdifferentiableI: "NSDERIV f x :> D \<Longrightarrow> f NSdifferentiable x"
   400   by (force simp add: NSdifferentiable_def)
   401 
   402 
   403 subsection \<open>(NS) Increment\<close>
   404 
   405 lemma incrementI:
   406   "f NSdifferentiable x \<Longrightarrow>
   407     increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)"
   408   by (simp add: increment_def)
   409 
   410 lemma incrementI2:
   411   "NSDERIV f x :> D \<Longrightarrow>
   412     increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)"
   413   by (erule NSdifferentiableI [THEN incrementI])
   414 
   415 text \<open>The Increment theorem -- Keisler p. 65.\<close>
   416 lemma increment_thm:
   417   "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
   418     \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
   419   apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
   420   apply (drule bspec, auto)
   421   apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
   422   apply (frule_tac b1 = "hypreal_of_real D + y" in mult_right_cancel [THEN iffD2])
   423    apply (erule_tac [2]
   424       V = "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y"
   425       in thin_rl)
   426    apply assumption
   427   apply (simp add: times_divide_eq_right [symmetric])
   428   apply (auto simp add: distrib_right)
   429   done
   430 
   431 lemma increment_thm2:
   432   "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow>
   433     \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
   434   by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
   435 
   436 lemma increment_approx_zero: "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow> increment f x h \<approx> 0"
   437   apply (drule increment_thm2)
   438     apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
   439       simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
   440   apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
   441   done
   442 
   443 end