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