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