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
```