src/HOL/Hyperreal/Lim.thy
author huffman
Sat Sep 30 18:04:28 2006 +0200 (2006-09-30)
changeset 20794 02482f9501ac
parent 20793 3b0489715b0e
child 20795 4e3adc66231a
permissions -rw-r--r--
add scaleR lemmas
paulson@10751
     1
(*  Title       : Lim.thy
paulson@14477
     2
    ID          : $Id$
paulson@10751
     3
    Author      : Jacques D. Fleuriot
paulson@10751
     4
    Copyright   : 1998  University of Cambridge
paulson@14477
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
kleing@19023
     6
    GMVT by Benjamin Porter, 2005
paulson@10751
     7
*)
paulson@10751
     8
paulson@14477
     9
header{*Limits, Continuity and Differentiation*}
paulson@10751
    10
nipkow@15131
    11
theory Lim
nipkow@15360
    12
imports SEQ
nipkow@15131
    13
begin
paulson@14477
    14
paulson@14477
    15
text{*Standard and Nonstandard Definitions*}
paulson@10751
    16
wenzelm@19765
    17
definition
huffman@20561
    18
  LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
kleing@19023
    19
        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
wenzelm@19765
    20
  "f -- a --> L =
huffman@20563
    21
     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
huffman@20563
    22
        --> norm (f x - L) < r)"
paulson@10751
    23
huffman@20561
    24
  NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
kleing@19023
    25
            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
huffman@20552
    26
  "f -- a --NS> L =
huffman@20552
    27
    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
paulson@10751
    28
huffman@20561
    29
  isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool"
wenzelm@19765
    30
  "isCont f a = (f -- a --> (f a))"
paulson@10751
    31
huffman@20561
    32
  isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool"
paulson@15228
    33
    --{*NS definition dispenses with limit notions*}
huffman@20552
    34
  "isNSCont f a = (\<forall>y. y @= star_of a -->
huffman@20552
    35
         ( *f* f) y @= star_of (f a))"
paulson@10751
    36
huffman@20793
    37
  deriv :: "[real \<Rightarrow> 'a::real_normed_vector, real, 'a] \<Rightarrow> bool"
paulson@15228
    38
    --{*Differentiation: D is derivative of function f at x*}
kleing@19023
    39
          ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
huffman@20793
    40
  "DERIV f x :> D = ((%h. (f(x + h) - f x) /# h) -- 0 --> D)"
paulson@10751
    41
paulson@14477
    42
  nsderiv :: "[real=>real,real,real] => bool"
kleing@19023
    43
          ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
wenzelm@19765
    44
  "NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal - {0}.
huffman@20563
    45
      (( *f* f)(hypreal_of_real x + h)
kleing@19023
    46
       - hypreal_of_real (f x))/h @= hypreal_of_real D)"
paulson@10751
    47
paulson@14477
    48
  differentiable :: "[real=>real,real] => bool"   (infixl "differentiable" 60)
wenzelm@19765
    49
  "f differentiable x = (\<exists>D. DERIV f x :> D)"
paulson@10751
    50
kleing@19023
    51
  NSdifferentiable :: "[real=>real,real] => bool"
paulson@14477
    52
                       (infixl "NSdifferentiable" 60)
wenzelm@19765
    53
  "f NSdifferentiable x = (\<exists>D. NSDERIV f x :> D)"
paulson@10751
    54
paulson@14477
    55
  increment :: "[real=>real,real,hypreal] => hypreal"
wenzelm@19765
    56
  "increment f x h = (@inc. f NSdifferentiable x &
huffman@20563
    57
           inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
paulson@10751
    58
huffman@20752
    59
  isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool"
huffman@20752
    60
  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
paulson@10751
    61
huffman@20752
    62
  isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool"
wenzelm@19765
    63
  "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
paulson@10751
    64
paulson@10751
    65
paulson@10751
    66
consts
paulson@10751
    67
  Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
paulson@10751
    68
primrec
paulson@10751
    69
  "Bolzano_bisect P a b 0 = (a,b)"
paulson@10751
    70
  "Bolzano_bisect P a b (Suc n) =
paulson@10751
    71
      (let (x,y) = Bolzano_bisect P a b n
wenzelm@11704
    72
       in if P(x, (x+y)/2) then ((x+y)/2, y)
paulson@14477
    73
                            else (x, (x+y)/2))"
paulson@14477
    74
paulson@14477
    75
huffman@20755
    76
subsection {* Limits of Functions *}
paulson@14477
    77
huffman@20755
    78
subsubsection {* Purely standard proofs *}
paulson@14477
    79
paulson@14477
    80
lemma LIM_eq:
paulson@14477
    81
     "f -- a --> L =
huffman@20561
    82
     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
paulson@14477
    83
by (simp add: LIM_def diff_minus)
paulson@14477
    84
huffman@20552
    85
lemma LIM_I:
huffman@20561
    86
     "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
huffman@20552
    87
      ==> f -- a --> L"
huffman@20552
    88
by (simp add: LIM_eq)
huffman@20552
    89
paulson@14477
    90
lemma LIM_D:
paulson@14477
    91
     "[| f -- a --> L; 0<r |]
huffman@20561
    92
      ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
paulson@14477
    93
by (simp add: LIM_eq)
paulson@14477
    94
huffman@20756
    95
lemma LIM_shift: "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
huffman@20756
    96
apply (rule LIM_I)
huffman@20756
    97
apply (drule_tac r="r" in LIM_D, safe)
huffman@20756
    98
apply (rule_tac x="s" in exI, safe)
huffman@20756
    99
apply (drule_tac x="x + k" in spec)
huffman@20756
   100
apply (simp add: compare_rls)
huffman@20756
   101
done
huffman@20756
   102
paulson@15228
   103
lemma LIM_const [simp]: "(%x. k) -- x --> k"
paulson@14477
   104
by (simp add: LIM_def)
paulson@14477
   105
paulson@14477
   106
lemma LIM_add:
huffman@20561
   107
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
paulson@14477
   108
  assumes f: "f -- a --> L" and g: "g -- a --> M"
paulson@14477
   109
  shows "(%x. f x + g(x)) -- a --> (L + M)"
huffman@20552
   110
proof (rule LIM_I)
paulson@14477
   111
  fix r :: real
huffman@20409
   112
  assume r: "0 < r"
paulson@14477
   113
  from LIM_D [OF f half_gt_zero [OF r]]
paulson@14477
   114
  obtain fs
paulson@14477
   115
    where fs:    "0 < fs"
huffman@20561
   116
      and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x - L) < r/2"
paulson@14477
   117
  by blast
paulson@14477
   118
  from LIM_D [OF g half_gt_zero [OF r]]
paulson@14477
   119
  obtain gs
paulson@14477
   120
    where gs:    "0 < gs"
huffman@20561
   121
      and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x - M) < r/2"
paulson@14477
   122
  by blast
huffman@20561
   123
  show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x + g x - (L + M)) < r"
paulson@14477
   124
  proof (intro exI conjI strip)
paulson@14477
   125
    show "0 < min fs gs"  by (simp add: fs gs)
huffman@20561
   126
    fix x :: 'a
huffman@20561
   127
    assume "x \<noteq> a \<and> norm (x-a) < min fs gs"
huffman@20561
   128
    hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp
paulson@14477
   129
    with fs_lt gs_lt
huffman@20552
   130
    have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+
huffman@20552
   131
    hence "norm (f x - L) + norm (g x - M) < r" by arith
huffman@20552
   132
    thus "norm (f x + g x - (L + M)) < r"
huffman@20552
   133
      by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
paulson@14477
   134
  qed
paulson@14477
   135
qed
paulson@14477
   136
huffman@20552
   137
lemma minus_diff_minus:
huffman@20552
   138
  fixes a b :: "'a::ab_group_add"
huffman@20552
   139
  shows "(- a) - (- b) = - (a - b)"
huffman@20552
   140
by simp
huffman@20552
   141
paulson@14477
   142
lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
huffman@20552
   143
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel)
paulson@14477
   144
paulson@14477
   145
lemma LIM_add_minus:
paulson@14477
   146
    "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
huffman@20552
   147
by (intro LIM_add LIM_minus)
paulson@14477
   148
paulson@14477
   149
lemma LIM_diff:
paulson@14477
   150
    "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
huffman@20552
   151
by (simp only: diff_minus LIM_add LIM_minus)
paulson@14477
   152
huffman@20561
   153
lemma LIM_const_not_eq:
huffman@20561
   154
  fixes a :: "'a::real_normed_div_algebra"
huffman@20561
   155
  shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
huffman@20552
   156
apply (simp add: LIM_eq)
huffman@20552
   157
apply (rule_tac x="norm (k - L)" in exI, simp, safe)
huffman@20561
   158
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real)
huffman@20552
   159
done
paulson@14477
   160
huffman@20561
   161
lemma LIM_const_eq:
huffman@20561
   162
  fixes a :: "'a::real_normed_div_algebra"
huffman@20561
   163
  shows "(%x. k) -- a --> L ==> k = L"
paulson@14477
   164
apply (rule ccontr)
kleing@19023
   165
apply (blast dest: LIM_const_not_eq)
paulson@14477
   166
done
paulson@14477
   167
huffman@20561
   168
lemma LIM_unique:
huffman@20561
   169
  fixes a :: "'a::real_normed_div_algebra"
huffman@20561
   170
  shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
kleing@19023
   171
apply (drule LIM_diff, assumption)
paulson@14477
   172
apply (auto dest!: LIM_const_eq)
paulson@14477
   173
done
paulson@14477
   174
paulson@14477
   175
lemma LIM_mult_zero:
huffman@20561
   176
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
paulson@14477
   177
  assumes f: "f -- a --> 0" and g: "g -- a --> 0"
paulson@14477
   178
  shows "(%x. f(x) * g(x)) -- a --> 0"
huffman@20552
   179
proof (rule LIM_I, simp)
paulson@14477
   180
  fix r :: real
paulson@14477
   181
  assume r: "0<r"
paulson@14477
   182
  from LIM_D [OF f zero_less_one]
paulson@14477
   183
  obtain fs
paulson@14477
   184
    where fs:    "0 < fs"
huffman@20561
   185
      and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x) < 1"
paulson@14477
   186
  by auto
paulson@14477
   187
  from LIM_D [OF g r]
paulson@14477
   188
  obtain gs
paulson@14477
   189
    where gs:    "0 < gs"
huffman@20561
   190
      and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x) < r"
paulson@14477
   191
  by auto
huffman@20561
   192
  show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x * g x) < r)"
paulson@14477
   193
  proof (intro exI conjI strip)
paulson@14477
   194
    show "0 < min fs gs"  by (simp add: fs gs)
huffman@20561
   195
    fix x :: 'a
huffman@20561
   196
    assume "x \<noteq> a \<and> norm (x-a) < min fs gs"
huffman@20561
   197
    hence  "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp
paulson@14477
   198
    with fs_lt gs_lt
huffman@20552
   199
    have "norm (f x) < 1" and "norm (g x) < r" by blast+
huffman@20552
   200
    hence "norm (f x) * norm (g x) < 1*r"
huffman@20552
   201
      by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero])
huffman@20552
   202
    thus "norm (f x * g x) < r"
huffman@20552
   203
      by (simp add: order_le_less_trans [OF norm_mult_ineq])
paulson@14477
   204
  qed
paulson@14477
   205
qed
paulson@14477
   206
paulson@14477
   207
lemma LIM_self: "(%x. x) -- a --> a"
paulson@14477
   208
by (auto simp add: LIM_def)
paulson@14477
   209
paulson@14477
   210
text{*Limits are equal for functions equal except at limit point*}
paulson@14477
   211
lemma LIM_equal:
paulson@14477
   212
     "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
paulson@14477
   213
by (simp add: LIM_def)
paulson@14477
   214
paulson@14477
   215
text{*Two uses in Hyperreal/Transcendental.ML*}
paulson@14477
   216
lemma LIM_trans:
paulson@14477
   217
     "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
paulson@14477
   218
apply (drule LIM_add, assumption)
paulson@14477
   219
apply (auto simp add: add_assoc)
paulson@14477
   220
done
paulson@14477
   221
huffman@20755
   222
subsubsection {* Purely nonstandard proofs *}
paulson@14477
   223
huffman@20754
   224
lemma NSLIM_I:
huffman@20754
   225
  "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
huffman@20754
   226
   \<Longrightarrow> f -- a --NS> L"
huffman@20754
   227
by (simp add: NSLIM_def)
paulson@14477
   228
huffman@20754
   229
lemma NSLIM_D:
huffman@20754
   230
  "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
huffman@20754
   231
   \<Longrightarrow> starfun f x \<approx> star_of L"
huffman@20754
   232
by (simp add: NSLIM_def)
paulson@14477
   233
huffman@20755
   234
text{*Proving properties of limits using nonstandard definition.
huffman@20755
   235
      The properties hold for standard limits as well!*}
huffman@20755
   236
huffman@20755
   237
lemma NSLIM_mult:
huffman@20755
   238
  fixes l m :: "'a::real_normed_algebra"
huffman@20755
   239
  shows "[| f -- x --NS> l; g -- x --NS> m |]
huffman@20755
   240
      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
huffman@20755
   241
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
huffman@20755
   242
huffman@20794
   243
lemma starfun_scaleR [simp]:
huffman@20794
   244
  "starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
huffman@20794
   245
by transfer (rule refl)
huffman@20794
   246
huffman@20794
   247
lemma NSLIM_scaleR:
huffman@20794
   248
  "[| f -- x --NS> l; g -- x --NS> m |]
huffman@20794
   249
      ==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)"
huffman@20794
   250
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
huffman@20794
   251
huffman@20755
   252
lemma NSLIM_add:
huffman@20755
   253
     "[| f -- x --NS> l; g -- x --NS> m |]
huffman@20755
   254
      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
huffman@20755
   255
by (auto simp add: NSLIM_def intro!: approx_add)
huffman@20755
   256
huffman@20755
   257
lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
huffman@20755
   258
by (simp add: NSLIM_def)
huffman@20755
   259
huffman@20755
   260
lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
huffman@20755
   261
by (simp add: NSLIM_def)
huffman@20755
   262
huffman@20755
   263
lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
huffman@20755
   264
by (simp only: NSLIM_add NSLIM_minus)
huffman@20755
   265
huffman@20755
   266
lemma NSLIM_inverse:
huffman@20755
   267
  fixes L :: "'a::real_normed_div_algebra"
huffman@20755
   268
  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
huffman@20755
   269
      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
huffman@20755
   270
apply (simp add: NSLIM_def, clarify)
huffman@20755
   271
apply (drule spec)
huffman@20755
   272
apply (auto simp add: star_of_approx_inverse)
huffman@20755
   273
done
huffman@20755
   274
huffman@20755
   275
lemma NSLIM_zero:
huffman@20755
   276
  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
huffman@20755
   277
proof -
huffman@20755
   278
  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
huffman@20755
   279
    by (rule NSLIM_add_minus [OF f NSLIM_const])
huffman@20755
   280
  thus ?thesis by simp
huffman@20755
   281
qed
huffman@20755
   282
huffman@20755
   283
lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
huffman@20755
   284
apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
huffman@20755
   285
apply (auto simp add: diff_minus add_assoc)
huffman@20755
   286
done
huffman@20755
   287
huffman@20755
   288
lemma NSLIM_const_not_eq:
huffman@20755
   289
  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
huffman@20755
   290
  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
huffman@20755
   291
apply (simp add: NSLIM_def)
huffman@20755
   292
apply (rule_tac x="star_of a + epsilon" in exI)
huffman@20755
   293
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
huffman@20755
   294
            simp add: hypreal_epsilon_not_zero)
huffman@20755
   295
done
huffman@20755
   296
huffman@20755
   297
lemma NSLIM_not_zero:
huffman@20755
   298
  fixes a :: real
huffman@20755
   299
  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
huffman@20755
   300
by (rule NSLIM_const_not_eq)
huffman@20755
   301
huffman@20755
   302
lemma NSLIM_const_eq:
huffman@20755
   303
  fixes a :: real
huffman@20755
   304
  shows "(%x. k) -- a --NS> L ==> k = L"
huffman@20755
   305
apply (rule ccontr)
huffman@20755
   306
apply (blast dest: NSLIM_const_not_eq)
huffman@20755
   307
done
huffman@20755
   308
huffman@20755
   309
text{* can actually be proved more easily by unfolding the definition!*}
huffman@20755
   310
lemma NSLIM_unique:
huffman@20755
   311
  fixes a :: real
huffman@20755
   312
  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
huffman@20755
   313
apply (drule NSLIM_minus)
huffman@20755
   314
apply (drule NSLIM_add, assumption)
huffman@20755
   315
apply (auto dest!: NSLIM_const_eq [symmetric])
huffman@20755
   316
apply (simp add: diff_def [symmetric])
huffman@20755
   317
done
huffman@20755
   318
huffman@20755
   319
lemma NSLIM_mult_zero:
huffman@20755
   320
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
huffman@20755
   321
  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
huffman@20755
   322
by (drule NSLIM_mult, auto)
huffman@20755
   323
huffman@20755
   324
lemma NSLIM_self: "(%x. x) -- a --NS> a"
huffman@20755
   325
by (simp add: NSLIM_def)
huffman@20755
   326
huffman@20755
   327
subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
huffman@20755
   328
huffman@20754
   329
lemma LIM_NSLIM:
huffman@20754
   330
  assumes f: "f -- a --> L" shows "f -- a --NS> L"
huffman@20754
   331
proof (rule NSLIM_I)
huffman@20754
   332
  fix x
huffman@20754
   333
  assume neq: "x \<noteq> star_of a"
huffman@20754
   334
  assume approx: "x \<approx> star_of a"
huffman@20754
   335
  have "starfun f x - star_of L \<in> Infinitesimal"
huffman@20754
   336
  proof (rule InfinitesimalI2)
huffman@20754
   337
    fix r::real assume r: "0 < r"
huffman@20754
   338
    from LIM_D [OF f r]
huffman@20754
   339
    obtain s where s: "0 < s" and
huffman@20754
   340
      less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
huffman@20754
   341
      by fast
huffman@20754
   342
    from less_r have less_r':
huffman@20754
   343
       "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
huffman@20754
   344
        \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
huffman@20754
   345
      by transfer
huffman@20754
   346
    from approx have "x - star_of a \<in> Infinitesimal"
huffman@20754
   347
      by (unfold approx_def)
huffman@20754
   348
    hence "hnorm (x - star_of a) < star_of s"
huffman@20754
   349
      using s by (rule InfinitesimalD2)
huffman@20754
   350
    with neq show "hnorm (starfun f x - star_of L) < star_of r"
huffman@20754
   351
      by (rule less_r')
huffman@20754
   352
  qed
huffman@20754
   353
  thus "starfun f x \<approx> star_of L"
huffman@20754
   354
    by (unfold approx_def)
huffman@20754
   355
qed
huffman@20552
   356
huffman@20754
   357
lemma NSLIM_LIM:
huffman@20754
   358
  assumes f: "f -- a --NS> L" shows "f -- a --> L"
huffman@20754
   359
proof (rule LIM_I)
huffman@20754
   360
  fix r::real assume r: "0 < r"
huffman@20754
   361
  have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
huffman@20754
   362
        \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
huffman@20754
   363
  proof (rule exI, safe)
huffman@20754
   364
    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
huffman@20754
   365
  next
huffman@20754
   366
    fix x assume neq: "x \<noteq> star_of a"
huffman@20754
   367
    assume "hnorm (x - star_of a) < epsilon"
huffman@20754
   368
    with Infinitesimal_epsilon
huffman@20754
   369
    have "x - star_of a \<in> Infinitesimal"
huffman@20754
   370
      by (rule hnorm_less_Infinitesimal)
huffman@20754
   371
    hence "x \<approx> star_of a"
huffman@20754
   372
      by (unfold approx_def)
huffman@20754
   373
    with f neq have "starfun f x \<approx> star_of L"
huffman@20754
   374
      by (rule NSLIM_D)
huffman@20754
   375
    hence "starfun f x - star_of L \<in> Infinitesimal"
huffman@20754
   376
      by (unfold approx_def)
huffman@20754
   377
    thus "hnorm (starfun f x - star_of L) < star_of r"
huffman@20754
   378
      using r by (rule InfinitesimalD2)
huffman@20754
   379
  qed
huffman@20754
   380
  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
huffman@20754
   381
    by transfer
huffman@20754
   382
qed
paulson@14477
   383
paulson@15228
   384
theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
paulson@14477
   385
by (blast intro: LIM_NSLIM NSLIM_LIM)
paulson@14477
   386
huffman@20755
   387
subsubsection {* Derived theorems about @{term LIM} *}
paulson@14477
   388
paulson@15228
   389
lemma LIM_mult2:
huffman@20552
   390
  fixes l m :: "'a::real_normed_algebra"
huffman@20552
   391
  shows "[| f -- x --> l; g -- x --> m |]
huffman@20552
   392
      ==> (%x. f(x) * g(x)) -- x --> (l * m)"
paulson@14477
   393
by (simp add: LIM_NSLIM_iff NSLIM_mult)
paulson@14477
   394
huffman@20794
   395
lemma LIM_scaleR:
huffman@20794
   396
  "[| f -- x --> l; g -- x --> m |]
huffman@20794
   397
      ==> (%x. f(x) *# g(x)) -- x --> (l *# m)"
huffman@20794
   398
by (simp add: LIM_NSLIM_iff NSLIM_scaleR)
huffman@20794
   399
paulson@15228
   400
lemma LIM_add2:
paulson@15228
   401
     "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
paulson@14477
   402
by (simp add: LIM_NSLIM_iff NSLIM_add)
paulson@14477
   403
paulson@14477
   404
lemma LIM_const2: "(%x. k) -- x --> k"
paulson@14477
   405
by (simp add: LIM_NSLIM_iff)
paulson@14477
   406
paulson@14477
   407
lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
paulson@14477
   408
by (simp add: LIM_NSLIM_iff NSLIM_minus)
paulson@14477
   409
paulson@14477
   410
lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
paulson@14477
   411
by (simp add: LIM_NSLIM_iff NSLIM_add_minus)
paulson@14477
   412
huffman@20552
   413
lemma LIM_inverse:
huffman@20653
   414
  fixes L :: "'a::real_normed_div_algebra"
huffman@20552
   415
  shows "[| f -- a --> L; L \<noteq> 0 |]
huffman@20552
   416
      ==> (%x. inverse(f(x))) -- a --> (inverse L)"
paulson@14477
   417
by (simp add: LIM_NSLIM_iff NSLIM_inverse)
paulson@14477
   418
paulson@14477
   419
lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"
paulson@14477
   420
by (simp add: LIM_NSLIM_iff NSLIM_zero)
paulson@14477
   421
paulson@14477
   422
lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l"
paulson@14477
   423
apply (drule_tac g = "%x. l" and M = l in LIM_add)
paulson@14477
   424
apply (auto simp add: diff_minus add_assoc)
paulson@14477
   425
done
paulson@14477
   426
huffman@20561
   427
lemma LIM_unique2:
huffman@20561
   428
  fixes a :: real
huffman@20561
   429
  shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
paulson@14477
   430
by (simp add: LIM_NSLIM_iff NSLIM_unique)
paulson@14477
   431
paulson@14477
   432
(* we can use the corresponding thm LIM_mult2 *)
paulson@14477
   433
(* for standard definition of limit           *)
paulson@14477
   434
huffman@20552
   435
lemma LIM_mult_zero2:
huffman@20561
   436
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
huffman@20552
   437
  shows "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
paulson@14477
   438
by (drule LIM_mult2, auto)
paulson@14477
   439
paulson@14477
   440
huffman@20755
   441
subsection {* Continuity *}
paulson@14477
   442
paulson@14477
   443
lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
paulson@14477
   444
by (simp add: isNSCont_def)
paulson@14477
   445
paulson@14477
   446
lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
paulson@14477
   447
by (simp add: isNSCont_def NSLIM_def)
paulson@14477
   448
paulson@14477
   449
lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
paulson@14477
   450
apply (simp add: isNSCont_def NSLIM_def, auto)
huffman@20561
   451
apply (case_tac "y = star_of a", auto)
paulson@14477
   452
done
paulson@14477
   453
paulson@15228
   454
text{*NS continuity can be defined using NS Limit in
paulson@15228
   455
    similar fashion to standard def of continuity*}
paulson@14477
   456
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
paulson@14477
   457
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
paulson@14477
   458
paulson@15228
   459
text{*Hence, NS continuity can be given
paulson@15228
   460
  in terms of standard limit*}
paulson@14477
   461
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
paulson@14477
   462
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
paulson@14477
   463
paulson@15228
   464
text{*Moreover, it's trivial now that NS continuity
paulson@15228
   465
  is equivalent to standard continuity*}
paulson@14477
   466
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
paulson@14477
   467
apply (simp add: isCont_def)
paulson@14477
   468
apply (rule isNSCont_LIM_iff)
paulson@14477
   469
done
paulson@14477
   470
paulson@15228
   471
text{*Standard continuity ==> NS continuity*}
paulson@14477
   472
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
paulson@14477
   473
by (erule isNSCont_isCont_iff [THEN iffD2])
paulson@14477
   474
paulson@15228
   475
text{*NS continuity ==> Standard continuity*}
paulson@14477
   476
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
paulson@14477
   477
by (erule isNSCont_isCont_iff [THEN iffD1])
paulson@14477
   478
paulson@14477
   479
text{*Alternative definition of continuity*}
paulson@14477
   480
(* Prove equivalence between NS limits - *)
paulson@14477
   481
(* seems easier than using standard def  *)
paulson@14477
   482
lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
paulson@14477
   483
apply (simp add: NSLIM_def, auto)
huffman@20561
   484
apply (drule_tac x = "star_of a + x" in spec)
huffman@20561
   485
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
huffman@20561
   486
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
huffman@20561
   487
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
huffman@20561
   488
 prefer 2 apply (simp add: add_commute diff_def [symmetric])
huffman@20561
   489
apply (rule_tac x = x in star_cases)
huffman@17318
   490
apply (rule_tac [2] x = x in star_cases)
huffman@17318
   491
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
paulson@14477
   492
done
paulson@14477
   493
paulson@14477
   494
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
paulson@14477
   495
by (rule NSLIM_h_iff)
paulson@14477
   496
paulson@14477
   497
lemma LIM_isCont_iff: "(f -- a --> f a) = ((%h. f(a + h)) -- 0 --> f(a))"
paulson@14477
   498
by (simp add: LIM_NSLIM_iff NSLIM_isCont_iff)
paulson@14477
   499
paulson@14477
   500
lemma isCont_iff: "(isCont f x) = ((%h. f(x + h)) -- 0 --> f(x))"
paulson@14477
   501
by (simp add: isCont_def LIM_isCont_iff)
paulson@14477
   502
paulson@15228
   503
text{*Immediate application of nonstandard criterion for continuity can offer
paulson@15228
   504
   very simple proofs of some standard property of continuous functions*}
paulson@14477
   505
text{*sum continuous*}
paulson@14477
   506
lemma isCont_add: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a"
paulson@14477
   507
by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
paulson@14477
   508
paulson@14477
   509
text{*mult continuous*}
huffman@20552
   510
lemma isCont_mult:
huffman@20561
   511
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
huffman@20552
   512
  shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
paulson@15228
   513
by (auto intro!: starfun_mult_HFinite_approx
paulson@15228
   514
            simp del: starfun_mult [symmetric]
paulson@14477
   515
            simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
paulson@14477
   516
paulson@15228
   517
text{*composition of continuous functions
paulson@15228
   518
     Note very short straightforard proof!*}
paulson@14477
   519
lemma isCont_o: "[| isCont f a; isCont g (f a) |] ==> isCont (g o f) a"
paulson@14477
   520
by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_def starfun_o [symmetric])
paulson@14477
   521
paulson@14477
   522
lemma isCont_o2: "[| isCont f a; isCont g (f a) |] ==> isCont (%x. g (f x)) a"
paulson@14477
   523
by (auto dest: isCont_o simp add: o_def)
paulson@14477
   524
paulson@14477
   525
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
paulson@14477
   526
by (simp add: isNSCont_def)
paulson@14477
   527
paulson@14477
   528
lemma isCont_minus: "isCont f a ==> isCont (%x. - f x) a"
paulson@14477
   529
by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
paulson@14477
   530
paulson@14477
   531
lemma isCont_inverse:
huffman@20653
   532
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
huffman@20552
   533
  shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
paulson@14477
   534
apply (simp add: isCont_def)
paulson@14477
   535
apply (blast intro: LIM_inverse)
paulson@14477
   536
done
paulson@14477
   537
huffman@20552
   538
lemma isNSCont_inverse:
huffman@20653
   539
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
huffman@20552
   540
  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
paulson@14477
   541
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
paulson@14477
   542
paulson@14477
   543
lemma isCont_diff:
paulson@14477
   544
      "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a"
paulson@14477
   545
apply (simp add: diff_minus)
paulson@14477
   546
apply (auto intro: isCont_add isCont_minus)
paulson@14477
   547
done
paulson@14477
   548
paulson@15228
   549
lemma isCont_const [simp]: "isCont (%x. k) a"
paulson@14477
   550
by (simp add: isCont_def)
paulson@14477
   551
paulson@15228
   552
lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
paulson@14477
   553
by (simp add: isNSCont_def)
paulson@14477
   554
huffman@20561
   555
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
paulson@14477
   556
apply (simp add: isNSCont_def)
paulson@14477
   557
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs)
paulson@14477
   558
done
paulson@14477
   559
huffman@20561
   560
lemma isCont_abs [simp]: "isCont abs (a::real)"
paulson@14477
   561
by (auto simp add: isNSCont_isCont_iff [symmetric])
paulson@15228
   562
paulson@14477
   563
paulson@14477
   564
(****************************************************************
paulson@14477
   565
(%* Leave as commented until I add topology theory or remove? *%)
paulson@14477
   566
(%*------------------------------------------------------------
paulson@14477
   567
  Elementary topology proof for a characterisation of
paulson@14477
   568
  continuity now: a function f is continuous if and only
paulson@14477
   569
  if the inverse image, {x. f(x) \<in> A}, of any open set A
paulson@14477
   570
  is always an open set
paulson@14477
   571
 ------------------------------------------------------------*%)
paulson@14477
   572
Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
paulson@14477
   573
               ==> isNSopen {x. f x \<in> A}"
paulson@14477
   574
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
paulson@14477
   575
by (dtac (mem_monad_approx RS approx_sym);
paulson@14477
   576
by (dres_inst_tac [("x","a")] spec 1);
paulson@14477
   577
by (dtac isNSContD 1 THEN assume_tac 1)
paulson@14477
   578
by (dtac bspec 1 THEN assume_tac 1)
paulson@14477
   579
by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
paulson@14477
   580
by (blast_tac (claset() addIs [starfun_mem_starset]);
paulson@14477
   581
qed "isNSCont_isNSopen";
paulson@14477
   582
paulson@14477
   583
Goalw [isNSCont_def]
paulson@14477
   584
          "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \
paulson@14477
   585
\              ==> isNSCont f x";
paulson@14477
   586
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
paulson@14477
   587
     (approx_minus_iff RS iffD2)],simpset() addsimps
paulson@14477
   588
      [Infinitesimal_def,SReal_iff]));
paulson@14477
   589
by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
paulson@14477
   590
by (etac (isNSopen_open_interval RSN (2,impE));
paulson@14477
   591
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
paulson@14477
   592
by (dres_inst_tac [("x","x")] spec 1);
paulson@14477
   593
by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
paulson@14477
   594
    simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
paulson@14477
   595
qed "isNSopen_isNSCont";
paulson@14477
   596
paulson@14477
   597
Goal "(\<forall>x. isNSCont f x) = \
paulson@14477
   598
\     (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
paulson@14477
   599
by (blast_tac (claset() addIs [isNSCont_isNSopen,
paulson@14477
   600
    isNSopen_isNSCont]);
paulson@14477
   601
qed "isNSCont_isNSopen_iff";
paulson@14477
   602
paulson@14477
   603
(%*------- Standard version of same theorem --------*%)
paulson@14477
   604
Goal "(\<forall>x. isCont f x) = \
paulson@14477
   605
\         (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})";
paulson@14477
   606
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
paulson@14477
   607
              simpset() addsimps [isNSopen_isopen_iff RS sym,
paulson@14477
   608
              isNSCont_isCont_iff RS sym]));
paulson@14477
   609
qed "isCont_isopen_iff";
paulson@14477
   610
*******************************************************************)
paulson@14477
   611
huffman@20755
   612
subsection {* Uniform Continuity *}
huffman@20755
   613
paulson@14477
   614
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
paulson@14477
   615
by (simp add: isNSUCont_def)
paulson@14477
   616
paulson@14477
   617
lemma isUCont_isCont: "isUCont f ==> isCont f x"
paulson@14477
   618
by (simp add: isUCont_def isCont_def LIM_def, meson)
paulson@14477
   619
huffman@20754
   620
lemma isUCont_isNSUCont:
huffman@20754
   621
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
huffman@20754
   622
  assumes f: "isUCont f" shows "isNSUCont f"
huffman@20754
   623
proof (unfold isNSUCont_def, safe)
huffman@20754
   624
  fix x y :: "'a star"
huffman@20754
   625
  assume approx: "x \<approx> y"
huffman@20754
   626
  have "starfun f x - starfun f y \<in> Infinitesimal"
huffman@20754
   627
  proof (rule InfinitesimalI2)
huffman@20754
   628
    fix r::real assume r: "0 < r"
huffman@20754
   629
    with f obtain s where s: "0 < s" and
huffman@20754
   630
      less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
huffman@20754
   631
      by (auto simp add: isUCont_def)
huffman@20754
   632
    from less_r have less_r':
huffman@20754
   633
       "\<And>x y. hnorm (x - y) < star_of s
huffman@20754
   634
        \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
huffman@20754
   635
      by transfer
huffman@20754
   636
    from approx have "x - y \<in> Infinitesimal"
huffman@20754
   637
      by (unfold approx_def)
huffman@20754
   638
    hence "hnorm (x - y) < star_of s"
huffman@20754
   639
      using s by (rule InfinitesimalD2)
huffman@20754
   640
    thus "hnorm (starfun f x - starfun f y) < star_of r"
huffman@20754
   641
      by (rule less_r')
huffman@20754
   642
  qed
huffman@20754
   643
  thus "starfun f x \<approx> starfun f y"
huffman@20754
   644
    by (unfold approx_def)
huffman@20754
   645
qed
paulson@14477
   646
paulson@14477
   647
lemma isNSUCont_isUCont:
huffman@20754
   648
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
huffman@20754
   649
  assumes f: "isNSUCont f" shows "isUCont f"
huffman@20754
   650
proof (unfold isUCont_def, safe)
huffman@20754
   651
  fix r::real assume r: "0 < r"
huffman@20754
   652
  have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
huffman@20754
   653
        \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
huffman@20754
   654
  proof (rule exI, safe)
huffman@20754
   655
    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
huffman@20754
   656
  next
huffman@20754
   657
    fix x y :: "'a star"
huffman@20754
   658
    assume "hnorm (x - y) < epsilon"
huffman@20754
   659
    with Infinitesimal_epsilon
huffman@20754
   660
    have "x - y \<in> Infinitesimal"
huffman@20754
   661
      by (rule hnorm_less_Infinitesimal)
huffman@20754
   662
    hence "x \<approx> y"
huffman@20754
   663
      by (unfold approx_def)
huffman@20754
   664
    with f have "starfun f x \<approx> starfun f y"
huffman@20754
   665
      by (simp add: isNSUCont_def)
huffman@20754
   666
    hence "starfun f x - starfun f y \<in> Infinitesimal"
huffman@20754
   667
      by (unfold approx_def)
huffman@20754
   668
    thus "hnorm (starfun f x - starfun f y) < star_of r"
huffman@20754
   669
      using r by (rule InfinitesimalD2)
huffman@20754
   670
  qed
huffman@20754
   671
  thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
huffman@20754
   672
    by transfer
huffman@20754
   673
qed
paulson@14477
   674
huffman@20755
   675
subsection {* Derivatives *}
huffman@20755
   676
huffman@20756
   677
subsubsection {* Purely standard proofs *}
huffman@20756
   678
huffman@20793
   679
lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/#h) -- 0 --> D)"
paulson@14477
   680
by (simp add: deriv_def)
paulson@14477
   681
huffman@20793
   682
lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/#h) -- 0 --> D"
paulson@14477
   683
by (simp add: deriv_def)
paulson@14477
   684
paulson@14477
   685
lemma DERIV_unique:
paulson@14477
   686
      "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"
paulson@14477
   687
apply (simp add: deriv_def)
paulson@14477
   688
apply (blast intro: LIM_unique)
paulson@14477
   689
done
paulson@14477
   690
huffman@20756
   691
text{*Alternative definition for differentiability*}
huffman@20756
   692
huffman@20756
   693
lemma DERIV_LIM_iff:
huffman@20756
   694
     "((%h::real. (f(a + h) - f(a)) / h) -- 0 --> D) =
huffman@20756
   695
      ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
huffman@20756
   696
apply (rule iffI)
huffman@20756
   697
apply (drule_tac k="- a" in LIM_shift)
huffman@20756
   698
apply (simp add: diff_minus)
huffman@20756
   699
apply (drule_tac k="a" in LIM_shift)
huffman@20756
   700
apply (simp add: add_commute)
huffman@20756
   701
done
huffman@20756
   702
huffman@20793
   703
lemma DERIV_LIM_iff':
huffman@20793
   704
     "((%h::real. (f(a + h) - f(a)) /# h) -- 0 --> D) =
huffman@20793
   705
      ((%x. (f(x)-f(a)) /# (x-a)) -- a --> D)"
huffman@20793
   706
apply (rule iffI)
huffman@20793
   707
apply (drule_tac k="- a" in LIM_shift)
huffman@20793
   708
apply (simp add: diff_minus)
huffman@20793
   709
apply (drule_tac k="a" in LIM_shift)
huffman@20793
   710
apply (simp add: add_commute)
huffman@20793
   711
done
huffman@20793
   712
huffman@20793
   713
lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) /# (z-x)) -- x --> D)"
huffman@20793
   714
by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff')
huffman@20756
   715
huffman@20756
   716
(* ------------------------------------------------------------------------ *)
huffman@20756
   717
(* Caratheodory formulation of derivative at a point: standard proof        *)
huffman@20756
   718
(* ------------------------------------------------------------------------ *)
huffman@20756
   719
huffman@20756
   720
lemma CARAT_DERIV:
huffman@20756
   721
     "(DERIV f x :> l) =
huffman@20793
   722
      (\<exists>g. (\<forall>z. f z - f x = (z-x) *# g z) & isCont g x & g x = l)"
huffman@20756
   723
      (is "?lhs = ?rhs")
huffman@20756
   724
proof
huffman@20756
   725
  assume der: "DERIV f x :> l"
huffman@20793
   726
  show "\<exists>g. (\<forall>z. f z - f x = (z-x) *# g z) \<and> isCont g x \<and> g x = l"
huffman@20756
   727
  proof (intro exI conjI)
huffman@20793
   728
    let ?g = "(%z. if z = x then l else (f z - f x) /# (z-x))"
huffman@20793
   729
    show "\<forall>z. f z - f x = (z-x) *# ?g z" by (simp)
huffman@20756
   730
    show "isCont ?g x" using der
huffman@20756
   731
      by (simp add: isCont_iff DERIV_iff diff_minus
huffman@20756
   732
               cong: LIM_equal [rule_format])
huffman@20756
   733
    show "?g x = l" by simp
huffman@20756
   734
  qed
huffman@20756
   735
next
huffman@20756
   736
  assume "?rhs"
huffman@20756
   737
  then obtain g where
huffman@20793
   738
    "(\<forall>z. f z - f x = (z-x) *# g z)" and "isCont g x" and "g x = l" by blast
huffman@20756
   739
  thus "(DERIV f x :> l)"
huffman@20756
   740
     by (auto simp add: isCont_iff DERIV_iff diff_minus
huffman@20756
   741
               cong: LIM_equal [rule_format])
huffman@20756
   742
qed
huffman@20756
   743
huffman@20756
   744
huffman@20756
   745
huffman@20793
   746
subsubsection {* Nonstandard proofs *}
huffman@20756
   747
huffman@20756
   748
lemma DERIV_NS_iff:
huffman@20793
   749
      "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/#h) -- 0 --NS> D)"
huffman@20756
   750
by (simp add: deriv_def LIM_NSLIM_iff)
huffman@20756
   751
huffman@20793
   752
lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/#h) -- 0 --NS> D"
huffman@20756
   753
by (simp add: deriv_def LIM_NSLIM_iff)
huffman@20756
   754
paulson@14477
   755
lemma NSDeriv_unique:
paulson@14477
   756
     "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"
paulson@14477
   757
apply (simp add: nsderiv_def)
paulson@14477
   758
apply (cut_tac Infinitesimal_epsilon hypreal_epsilon_not_zero)
paulson@15228
   759
apply (auto dest!: bspec [where x=epsilon]
paulson@15228
   760
            intro!: inj_hypreal_of_real [THEN injD]
paulson@14477
   761
            dest: approx_trans3)
paulson@14477
   762
done
paulson@14477
   763
huffman@20755
   764
text {*First NSDERIV in terms of NSLIM*}
paulson@14477
   765
paulson@15228
   766
text{*first equivalence *}
paulson@14477
   767
lemma NSDERIV_NSLIM_iff:
huffman@20563
   768
      "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
paulson@14477
   769
apply (simp add: nsderiv_def NSLIM_def, auto)
paulson@14477
   770
apply (drule_tac x = xa in bspec)
paulson@14477
   771
apply (rule_tac [3] ccontr)
paulson@14477
   772
apply (drule_tac [3] x = h in spec)
paulson@14477
   773
apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
paulson@14477
   774
done
paulson@14477
   775
paulson@15228
   776
text{*second equivalence *}
paulson@14477
   777
lemma NSDERIV_NSLIM_iff2:
paulson@14477
   778
     "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
paulson@15228
   779
by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff  diff_minus [symmetric]
paulson@14477
   780
              LIM_NSLIM_iff [symmetric])
paulson@14477
   781
paulson@14477
   782
(* while we're at it! *)
paulson@14477
   783
lemma NSDERIV_iff2:
paulson@14477
   784
     "(NSDERIV f x :> D) =
paulson@14477
   785
      (\<forall>w.
paulson@14477
   786
        w \<noteq> hypreal_of_real x & w \<approx> hypreal_of_real x -->
paulson@14477
   787
        ( *f* (%z. (f z - f x) / (z-x))) w \<approx> hypreal_of_real D)"
paulson@14477
   788
by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
paulson@14477
   789
paulson@14477
   790
(*FIXME DELETE*)
huffman@20563
   791
lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x - a \<noteq> (0::hypreal))"
paulson@14477
   792
by (auto dest: hypreal_eq_minus_iff [THEN iffD2])
paulson@14477
   793
paulson@14477
   794
lemma NSDERIVD5:
paulson@14477
   795
  "(NSDERIV f x :> D) ==>
paulson@14477
   796
   (\<forall>u. u \<approx> hypreal_of_real x -->
paulson@14477
   797
     ( *f* (%z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))"
paulson@14477
   798
apply (auto simp add: NSDERIV_iff2)
paulson@14477
   799
apply (case_tac "u = hypreal_of_real x", auto)
paulson@14477
   800
apply (drule_tac x = u in spec, auto)
paulson@14477
   801
apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
paulson@14477
   802
apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
paulson@14477
   803
apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
huffman@20563
   804
apply (auto simp add:
kleing@19023
   805
         approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
kleing@19023
   806
         Infinitesimal_subset_HFinite [THEN subsetD])
paulson@14477
   807
done
paulson@14477
   808
paulson@14477
   809
lemma NSDERIVD4:
paulson@14477
   810
     "(NSDERIV f x :> D) ==>
paulson@14477
   811
      (\<forall>h \<in> Infinitesimal.
paulson@14477
   812
               (( *f* f)(hypreal_of_real x + h) -
paulson@14477
   813
                 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
paulson@14477
   814
apply (auto simp add: nsderiv_def)
paulson@14477
   815
apply (case_tac "h = (0::hypreal) ")
paulson@14477
   816
apply (auto simp add: diff_minus)
paulson@14477
   817
apply (drule_tac x = h in bspec)
paulson@14477
   818
apply (drule_tac [2] c = h in approx_mult1)
paulson@14477
   819
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
nipkow@15539
   820
            simp add: diff_minus)
paulson@14477
   821
done
paulson@14477
   822
paulson@14477
   823
lemma NSDERIVD3:
paulson@14477
   824
     "(NSDERIV f x :> D) ==>
paulson@14477
   825
      (\<forall>h \<in> Infinitesimal - {0}.
paulson@14477
   826
               (( *f* f)(hypreal_of_real x + h) -
paulson@14477
   827
                 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
paulson@14477
   828
apply (auto simp add: nsderiv_def)
paulson@14477
   829
apply (rule ccontr, drule_tac x = h in bspec)
paulson@14477
   830
apply (drule_tac [2] c = h in approx_mult1)
paulson@14477
   831
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
nipkow@15539
   832
            simp add: mult_assoc diff_minus)
paulson@14477
   833
done
paulson@14477
   834
paulson@15228
   835
text{*Differentiability implies continuity
paulson@15228
   836
         nice and simple "algebraic" proof*}
paulson@14477
   837
lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x"
paulson@14477
   838
apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
paulson@14477
   839
apply (drule approx_minus_iff [THEN iffD1])
paulson@14477
   840
apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
huffman@20563
   841
apply (drule_tac x = "xa - hypreal_of_real x" in bspec)
paulson@15228
   842
 prefer 2 apply (simp add: add_assoc [symmetric])
paulson@15234
   843
apply (auto simp add: mem_infmal_iff [symmetric] add_commute)
huffman@20563
   844
apply (drule_tac c = "xa - hypreal_of_real x" in approx_mult1)
paulson@14477
   845
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
paulson@14477
   846
            simp add: mult_assoc)
paulson@14477
   847
apply (drule_tac x3=D in
paulson@14477
   848
           HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
paulson@14477
   849
             THEN mem_infmal_iff [THEN iffD1]])
nipkow@15539
   850
apply (auto simp add: mult_commute
paulson@14477
   851
            intro: approx_trans approx_minus_iff [THEN iffD2])
paulson@14477
   852
done
paulson@14477
   853
paulson@15228
   854
text{*Differentiation rules for combinations of functions
paulson@14477
   855
      follow from clear, straightforard, algebraic
paulson@15228
   856
      manipulations*}
paulson@14477
   857
text{*Constant function*}
paulson@14477
   858
paulson@14477
   859
(* use simple constant nslimit theorem *)
paulson@15228
   860
lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)"
paulson@14477
   861
by (simp add: NSDERIV_NSLIM_iff)
paulson@14477
   862
paulson@15228
   863
text{*Sum of functions- proved easily*}
paulson@14477
   864
paulson@14477
   865
lemma NSDERIV_add: "[| NSDERIV f x :> Da;  NSDERIV g x :> Db |]
paulson@14477
   866
      ==> NSDERIV (%x. f x + g x) x :> Da + Db"
paulson@14477
   867
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
huffman@20563
   868
apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
paulson@14477
   869
apply (drule_tac b = "hypreal_of_real Da" and d = "hypreal_of_real Db" in approx_add)
huffman@20563
   870
apply (auto simp add: diff_def add_ac)
paulson@14477
   871
done
paulson@14477
   872
paulson@15228
   873
text{*Product of functions - Proof is trivial but tedious
paulson@15228
   874
  and long due to rearrangement of terms*}
paulson@14477
   875
huffman@20563
   876
lemma lemma_nsderiv1: "((a::hypreal)*b) - (c*d) = (b*(a - c)) + (c*(b - d))"
huffman@20563
   877
by (simp add: right_diff_distrib)
paulson@14477
   878
huffman@20563
   879
lemma lemma_nsderiv2: "[| (x - y) / z = hypreal_of_real D + yb; z \<noteq> 0;
paulson@14477
   880
         z \<in> Infinitesimal; yb \<in> Infinitesimal |]
huffman@20563
   881
      ==> x - y \<approx> 0"
paulson@14477
   882
apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption)
huffman@20563
   883
apply (erule_tac V = "(x - y) / z = hypreal_of_real D + yb" in thin_rl)
paulson@14477
   884
apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
nipkow@15539
   885
            simp add: mult_assoc mem_infmal_iff [symmetric])
paulson@14477
   886
apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
paulson@14477
   887
done
paulson@14477
   888
paulson@14477
   889
lemma NSDERIV_mult: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
paulson@14477
   890
      ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
paulson@14477
   891
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
paulson@14477
   892
apply (auto dest!: spec
kleing@19023
   893
      simp add: starfun_lambda_cancel lemma_nsderiv1)
huffman@20563
   894
apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
paulson@14477
   895
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
paulson@15234
   896
apply (auto simp add: times_divide_eq_right [symmetric]
paulson@15234
   897
            simp del: times_divide_eq)
huffman@20563
   898
apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
huffman@20563
   899
apply (drule_tac
paulson@15228
   900
     approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
paulson@15228
   901
apply (auto intro!: approx_add_mono1
paulson@14477
   902
            simp add: left_distrib right_distrib mult_commute add_assoc)
paulson@15228
   903
apply (rule_tac b1 = "hypreal_of_real Db * hypreal_of_real (f x)"
paulson@14477
   904
         in add_commute [THEN subst])
paulson@15228
   905
apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
paulson@15228
   906
                    Infinitesimal_add Infinitesimal_mult
paulson@15228
   907
                    Infinitesimal_hypreal_of_real_mult
paulson@14477
   908
                    Infinitesimal_hypreal_of_real_mult2
paulson@14477
   909
          simp add: add_assoc [symmetric])
paulson@14477
   910
done
paulson@14477
   911
paulson@14477
   912
text{*Multiplying by a constant*}
paulson@14477
   913
lemma NSDERIV_cmult: "NSDERIV f x :> D
paulson@14477
   914
      ==> NSDERIV (%x. c * f x) x :> c*D"
paulson@15228
   915
apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
huffman@20563
   916
                  minus_mult_right right_diff_distrib [symmetric])
paulson@14477
   917
apply (erule NSLIM_const [THEN NSLIM_mult])
paulson@14477
   918
done
paulson@14477
   919
paulson@14477
   920
text{*Negation of function*}
paulson@14477
   921
lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
paulson@14477
   922
proof (simp add: NSDERIV_NSLIM_iff)
huffman@20563
   923
  assume "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D"
huffman@20563
   924
  hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
paulson@14477
   925
    by (rule NSLIM_minus)
huffman@20563
   926
  have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
paulson@15228
   927
    by (simp add: minus_divide_left)
paulson@14477
   928
  with deriv
paulson@14477
   929
  show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
paulson@14477
   930
qed
paulson@14477
   931
paulson@14477
   932
text{*Subtraction*}
paulson@14477
   933
lemma NSDERIV_add_minus: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + -g x) x :> Da + -Db"
paulson@14477
   934
by (blast dest: NSDERIV_add NSDERIV_minus)
paulson@14477
   935
paulson@14477
   936
lemma NSDERIV_diff:
paulson@14477
   937
     "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
paulson@14477
   938
      ==> NSDERIV (%x. f x - g x) x :> Da-Db"
paulson@14477
   939
apply (simp add: diff_minus)
paulson@14477
   940
apply (blast intro: NSDERIV_add_minus)
paulson@14477
   941
done
paulson@14477
   942
paulson@14477
   943
text{*  Similarly to the above, the chain rule admits an entirely
paulson@14477
   944
   straightforward derivation. Compare this with Harrison's
paulson@14477
   945
   HOL proof of the chain rule, which proved to be trickier and
paulson@14477
   946
   required an alternative characterisation of differentiability-
paulson@14477
   947
   the so-called Carathedory derivative. Our main problem is
paulson@14477
   948
   manipulation of terms.*}
paulson@14477
   949
paulson@14477
   950
paulson@14477
   951
(* lemmas *)
paulson@14477
   952
lemma NSDERIV_zero:
paulson@14477
   953
      "[| NSDERIV g x :> D;
paulson@14477
   954
               ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);
paulson@14477
   955
               xa \<in> Infinitesimal;
paulson@14477
   956
               xa \<noteq> 0
paulson@14477
   957
            |] ==> D = 0"
paulson@14477
   958
apply (simp add: nsderiv_def)
paulson@14477
   959
apply (drule bspec, auto)
paulson@14477
   960
done
paulson@14477
   961
paulson@14477
   962
(* can be proved differently using NSLIM_isCont_iff *)
paulson@14477
   963
lemma NSDERIV_approx:
paulson@14477
   964
     "[| NSDERIV f x :> D;  h \<in> Infinitesimal;  h \<noteq> 0 |]
huffman@20563
   965
      ==> ( *f* f) (hypreal_of_real(x) + h) - hypreal_of_real(f x) \<approx> 0"
paulson@14477
   966
apply (simp add: nsderiv_def)
paulson@14477
   967
apply (simp add: mem_infmal_iff [symmetric])
paulson@14477
   968
apply (rule Infinitesimal_ratio)
paulson@14477
   969
apply (rule_tac [3] approx_hypreal_of_real_HFinite, auto)
paulson@14477
   970
done
paulson@14477
   971
paulson@14477
   972
(*---------------------------------------------------------------
paulson@14477
   973
   from one version of differentiability
paulson@14477
   974
paulson@14477
   975
                f(x) - f(a)
paulson@14477
   976
              --------------- \<approx> Db
paulson@14477
   977
                  x - a
paulson@14477
   978
 ---------------------------------------------------------------*)
paulson@14477
   979
lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
paulson@14477
   980
         ( *f* g) (hypreal_of_real(x) + xa) \<noteq> hypreal_of_real (g x);
paulson@14477
   981
         ( *f* g) (hypreal_of_real(x) + xa) \<approx> hypreal_of_real (g x)
paulson@14477
   982
      |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa))
huffman@20563
   983
                   - hypreal_of_real (f (g x)))
huffman@20563
   984
              / (( *f* g) (hypreal_of_real(x) + xa) - hypreal_of_real (g x))
paulson@14477
   985
             \<approx> hypreal_of_real(Da)"
paulson@14477
   986
by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric])
paulson@14477
   987
paulson@14477
   988
(*--------------------------------------------------------------
paulson@14477
   989
   from other version of differentiability
paulson@14477
   990
paulson@14477
   991
                f(x + h) - f(x)
paulson@14477
   992
               ----------------- \<approx> Db
paulson@14477
   993
                       h
paulson@14477
   994
 --------------------------------------------------------------*)
paulson@14477
   995
lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |]
huffman@20563
   996
      ==> (( *f* g) (hypreal_of_real(x) + xa) - hypreal_of_real(g x)) / xa
paulson@14477
   997
          \<approx> hypreal_of_real(Db)"
paulson@14477
   998
by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)
paulson@14477
   999
paulson@14477
  1000
lemma lemma_chain: "(z::hypreal) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
paulson@14477
  1001
by auto
paulson@14477
  1002
paulson@15228
  1003
text{*This proof uses both definitions of differentiability.*}
paulson@14477
  1004
lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |]
paulson@14477
  1005
      ==> NSDERIV (f o g) x :> Da * Db"
paulson@14477
  1006
apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def
paulson@14477
  1007
                mem_infmal_iff [symmetric])
paulson@14477
  1008
apply clarify
paulson@14477
  1009
apply (frule_tac f = g in NSDERIV_approx)
paulson@14477
  1010
apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
paulson@14477
  1011
apply (case_tac "( *f* g) (hypreal_of_real (x) + xa) = hypreal_of_real (g x) ")
paulson@14477
  1012
apply (drule_tac g = g in NSDERIV_zero)
paulson@14477
  1013
apply (auto simp add: divide_inverse)
huffman@20563
  1014
apply (rule_tac z1 = "( *f* g) (hypreal_of_real (x) + xa) - hypreal_of_real (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst])
paulson@14477
  1015
apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
paulson@14477
  1016
apply (rule approx_mult_hypreal_of_real)
paulson@14477
  1017
apply (simp_all add: divide_inverse [symmetric])
paulson@14477
  1018
apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
paulson@14477
  1019
apply (blast intro: NSDERIVD2)
paulson@14477
  1020
done
paulson@14477
  1021
paulson@14477
  1022
text{*Differentiation of natural number powers*}
paulson@15228
  1023
lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1"
paulson@15228
  1024
by (simp add: NSDERIV_NSLIM_iff NSLIM_def divide_self del: divide_self_if)
paulson@14477
  1025
paulson@15228
  1026
lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
huffman@20756
  1027
by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp)
paulson@14477
  1028
paulson@14477
  1029
(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
paulson@14477
  1030
lemma NSDERIV_inverse:
paulson@14477
  1031
     "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
paulson@14477
  1032
apply (simp add: nsderiv_def)
paulson@15228
  1033
apply (rule ballI, simp, clarify)
huffman@20563
  1034
apply (frule (1) Infinitesimal_add_not_zero)
huffman@20563
  1035
apply (simp add: add_commute)
huffman@20563
  1036
(*apply (auto simp add: starfun_inverse_inverse realpow_two
huffman@20563
  1037
        simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*)
paulson@14477
  1038
apply (simp add: inverse_add inverse_mult_distrib [symmetric]
huffman@20563
  1039
              inverse_minus_eq [symmetric] add_ac mult_ac diff_def
paulson@15228
  1040
            del: inverse_mult_distrib inverse_minus_eq
paulson@14477
  1041
                 minus_mult_left [symmetric] minus_mult_right [symmetric])
paulson@14477
  1042
apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
paulson@14477
  1043
            del: minus_mult_left [symmetric] minus_mult_right [symmetric])
paulson@15234
  1044
apply (rule_tac y = "inverse (- hypreal_of_real x * hypreal_of_real x)" in approx_trans)
paulson@14477
  1045
apply (rule inverse_add_Infinitesimal_approx2)
paulson@15228
  1046
apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
paulson@14477
  1047
            simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
paulson@14477
  1048
apply (rule Infinitesimal_HFinite_mult2, auto)
paulson@14477
  1049
done
paulson@14477
  1050
huffman@20756
  1051
subsubsection {* Equivalence of NS and Standard definitions *}
paulson@14477
  1052
huffman@20793
  1053
lemma divideR_eq_divide [simp]: "x /# y = x / y"
huffman@20793
  1054
by (simp add: real_scaleR_def divide_inverse mult_commute)
huffman@20793
  1055
huffman@20756
  1056
text{*Now equivalence between NSDERIV and DERIV*}
huffman@20756
  1057
lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
huffman@20756
  1058
by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
paulson@14477
  1059
huffman@20756
  1060
text{*Now Standard proof*}
huffman@20793
  1061
lemma DERIV_isCont: "DERIV (f::real=>real) x :> D ==> isCont f x"
huffman@20756
  1062
by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric]
huffman@20756
  1063
              NSDERIV_isNSCont)
huffman@20756
  1064
huffman@20793
  1065
lemma DERIV_const [simp]: "(DERIV (%x. k::real) x :> 0)"
huffman@20756
  1066
by (simp add: NSDERIV_DERIV_iff [symmetric])
huffman@20756
  1067
huffman@20756
  1068
(* Standard theorem *)
huffman@20756
  1069
lemma DERIV_add: "[| DERIV f x :> Da; DERIV g x :> Db |]
huffman@20793
  1070
      ==> DERIV (%x. f x + g x :: real) x :> (Da + Db)"
huffman@20756
  1071
apply (simp add: NSDERIV_add NSDERIV_DERIV_iff [symmetric])
huffman@20756
  1072
done
huffman@20756
  1073
huffman@20756
  1074
lemma DERIV_mult:
huffman@20756
  1075
     "[| DERIV f x :> Da; DERIV g x :> Db |]
huffman@20793
  1076
      ==> DERIV (%x. f x * g x :: real) x :> (Da * g(x)) + (Db * f(x))"
huffman@20756
  1077
by (simp add: NSDERIV_mult NSDERIV_DERIV_iff [symmetric])
huffman@20756
  1078
huffman@20756
  1079
(* let's do the standard proof though theorem *)
huffman@20756
  1080
(* LIM_mult2 follows from a NS proof          *)
huffman@20756
  1081
huffman@20756
  1082
lemma DERIV_cmult:
huffman@20793
  1083
      "DERIV f x :> D ==> DERIV (%x. c * f x :: real) x :> c*D"
huffman@20756
  1084
apply (simp only: deriv_def times_divide_eq_right [symmetric]
huffman@20793
  1085
                  divideR_eq_divide
huffman@20756
  1086
                  NSDERIV_NSLIM_iff minus_mult_right right_diff_distrib [symmetric])
huffman@20756
  1087
apply (erule LIM_const [THEN LIM_mult2])
huffman@20756
  1088
done
huffman@20756
  1089
huffman@20793
  1090
lemma DERIV_minus: "DERIV f x :> D ==> DERIV (%x. -(f x)::real) x :> -D"
huffman@20756
  1091
by (simp add: NSDERIV_minus NSDERIV_DERIV_iff [symmetric])
huffman@20756
  1092
huffman@20793
  1093
lemma DERIV_add_minus: "[| DERIV f x :> Da; DERIV g x :> Db |] ==> DERIV (%x. f x + -g x :: real) x :> Da + -Db"
huffman@20756
  1094
by (blast dest: DERIV_add DERIV_minus)
huffman@20756
  1095
huffman@20756
  1096
lemma DERIV_diff:
huffman@20756
  1097
     "[| DERIV f x :> Da; DERIV g x :> Db |]
huffman@20793
  1098
       ==> DERIV (%x. f x - g x :: real) x :> Da-Db"
huffman@20756
  1099
apply (simp add: diff_minus)
huffman@20756
  1100
apply (blast intro: DERIV_add_minus)
huffman@20756
  1101
done
huffman@20756
  1102
huffman@20756
  1103
(* standard version *)
huffman@20756
  1104
lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
huffman@20756
  1105
by (simp add: NSDERIV_DERIV_iff [symmetric] NSDERIV_chain)
huffman@20756
  1106
huffman@20756
  1107
lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
huffman@20756
  1108
by (auto dest: DERIV_chain simp add: o_def)
huffman@20756
  1109
huffman@20756
  1110
(*derivative of the identity function*)
huffman@20756
  1111
lemma DERIV_Id [simp]: "DERIV (%x. x) x :> 1"
huffman@20756
  1112
by (simp add: NSDERIV_DERIV_iff [symmetric])
huffman@20756
  1113
huffman@20756
  1114
lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard]
huffman@20756
  1115
huffman@20756
  1116
(*derivative of linear multiplication*)
huffman@20756
  1117
lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
huffman@20756
  1118
by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp)
huffman@20756
  1119
huffman@20756
  1120
lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
huffman@20756
  1121
apply (induct "n")
huffman@20756
  1122
apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
huffman@20756
  1123
apply (auto simp add: real_of_nat_Suc left_distrib)
huffman@20756
  1124
apply (case_tac "0 < n")
huffman@20756
  1125
apply (drule_tac x = x in realpow_minus_mult)
huffman@20756
  1126
apply (auto simp add: mult_assoc add_commute)
huffman@20756
  1127
done
huffman@20756
  1128
huffman@20756
  1129
(* NS version *)
huffman@20756
  1130
lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
huffman@20756
  1131
by (simp add: NSDERIV_DERIV_iff DERIV_pow)
huffman@20756
  1132
huffman@20756
  1133
text{*Power of -1*}
paulson@14477
  1134
paulson@14477
  1135
lemma DERIV_inverse: "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
paulson@14477
  1136
by (simp add: NSDERIV_inverse NSDERIV_DERIV_iff [symmetric] del: realpow_Suc)
paulson@14477
  1137
paulson@14477
  1138
text{*Derivative of inverse*}
paulson@14477
  1139
lemma DERIV_inverse_fun: "[| DERIV f x :> d; f(x) \<noteq> 0 |]
huffman@20793
  1140
      ==> DERIV (%x. inverse(f x)::real) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
paulson@14477
  1141
apply (simp only: mult_commute [of d] minus_mult_left power_inverse)
paulson@14477
  1142
apply (fold o_def)
paulson@14477
  1143
apply (blast intro!: DERIV_chain DERIV_inverse)
paulson@14477
  1144
done
paulson@14477
  1145
paulson@14477
  1146
lemma NSDERIV_inverse_fun: "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
paulson@14477
  1147
      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
paulson@14477
  1148
by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: realpow_Suc)
paulson@14477
  1149
paulson@14477
  1150
text{*Derivative of quotient*}
paulson@14477
  1151
lemma DERIV_quotient: "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
huffman@20793
  1152
       ==> DERIV (%y. f(y) / (g y) :: real) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
paulson@14477
  1153
apply (drule_tac f = g in DERIV_inverse_fun)
paulson@14477
  1154
apply (drule_tac [2] DERIV_mult)
paulson@14477
  1155
apply (assumption+)
paulson@14477
  1156
apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
huffman@20563
  1157
                 mult_ac diff_def
paulson@14477
  1158
     del: realpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
paulson@14477
  1159
done
paulson@14477
  1160
paulson@14477
  1161
lemma NSDERIV_quotient: "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
paulson@14477
  1162
       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
huffman@20563
  1163
                            - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
paulson@14477
  1164
by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
paulson@14477
  1165
paulson@14477
  1166
lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>
paulson@14477
  1167
      \<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isNSCont g x & g x = l"
huffman@20793
  1168
by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV
huffman@20793
  1169
                   real_scaleR_def mult_commute)
paulson@14477
  1170
paulson@14477
  1171
lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))"
paulson@14477
  1172
by auto
paulson@14477
  1173
paulson@14477
  1174
lemma CARAT_DERIVD:
paulson@14477
  1175
  assumes all: "\<forall>z. f z - f x = g z * (z-x)"
paulson@14477
  1176
      and nsc: "isNSCont g x"
paulson@14477
  1177
  shows "NSDERIV f x :> g x"
paulson@14477
  1178
proof -
paulson@14477
  1179
  from nsc
paulson@14477
  1180
  have "\<forall>w. w \<noteq> hypreal_of_real x \<and> w \<approx> hypreal_of_real x \<longrightarrow>
paulson@14477
  1181
         ( *f* g) w * (w - hypreal_of_real x) / (w - hypreal_of_real x) \<approx>
paulson@15228
  1182
         hypreal_of_real (g x)"
paulson@14477
  1183
    by (simp add: diff_minus isNSCont_def)
paulson@14477
  1184
  thus ?thesis using all
paulson@15228
  1185
    by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
paulson@14477
  1186
qed
paulson@14477
  1187
huffman@20755
  1188
subsubsection {* Differentiability predicate *}
huffman@20755
  1189
huffman@20755
  1190
lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
huffman@20755
  1191
by (simp add: differentiable_def)
huffman@20755
  1192
huffman@20755
  1193
lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
huffman@20755
  1194
by (force simp add: differentiable_def)
huffman@20755
  1195
huffman@20755
  1196
lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
huffman@20755
  1197
by (simp add: NSdifferentiable_def)
huffman@20755
  1198
huffman@20755
  1199
lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
huffman@20755
  1200
by (force simp add: NSdifferentiable_def)
huffman@20755
  1201
huffman@20755
  1202
lemma differentiable_const: "(\<lambda>z. a) differentiable x"
huffman@20755
  1203
  apply (unfold differentiable_def)
huffman@20755
  1204
  apply (rule_tac x=0 in exI)
huffman@20755
  1205
  apply simp
huffman@20755
  1206
  done
huffman@20755
  1207
huffman@20755
  1208
lemma differentiable_sum:
huffman@20755
  1209
  assumes "f differentiable x"
huffman@20755
  1210
  and "g differentiable x"
huffman@20755
  1211
  shows "(\<lambda>x. f x + g x) differentiable x"
huffman@20755
  1212
proof -
huffman@20755
  1213
  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
huffman@20755
  1214
  then obtain df where "DERIV f x :> df" ..
huffman@20755
  1215
  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
huffman@20755
  1216
  then obtain dg where "DERIV g x :> dg" ..
huffman@20755
  1217
  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
huffman@20755
  1218
  hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
huffman@20755
  1219
  thus ?thesis by (fold differentiable_def)
huffman@20755
  1220
qed
huffman@20755
  1221
huffman@20755
  1222
lemma differentiable_diff:
huffman@20755
  1223
  assumes "f differentiable x"
huffman@20755
  1224
  and "g differentiable x"
huffman@20755
  1225
  shows "(\<lambda>x. f x - g x) differentiable x"
huffman@20755
  1226
proof -
huffman@20755
  1227
  from prems have "f differentiable x" by simp
huffman@20755
  1228
  moreover
huffman@20755
  1229
  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
huffman@20755
  1230
  then obtain dg where "DERIV g x :> dg" ..
huffman@20755
  1231
  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
huffman@20755
  1232
  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
huffman@20755
  1233
  hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
huffman@20755
  1234
  ultimately 
huffman@20755
  1235
  show ?thesis
huffman@20755
  1236
    by (auto simp: real_diff_def dest: differentiable_sum)
huffman@20755
  1237
qed
huffman@20755
  1238
huffman@20755
  1239
lemma differentiable_mult:
huffman@20755
  1240
  assumes "f differentiable x"
huffman@20755
  1241
  and "g differentiable x"
huffman@20755
  1242
  shows "(\<lambda>x. f x * g x) differentiable x"
huffman@20755
  1243
proof -
huffman@20755
  1244
  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
huffman@20755
  1245
  then obtain df where "DERIV f x :> df" ..
huffman@20755
  1246
  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
huffman@20755
  1247
  then obtain dg where "DERIV g x :> dg" ..
huffman@20755
  1248
  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
huffman@20755
  1249
  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
huffman@20755
  1250
  thus ?thesis by (fold differentiable_def)
huffman@20755
  1251
qed
huffman@20755
  1252
huffman@20755
  1253
subsection {*(NS) Increment*}
huffman@20755
  1254
lemma incrementI:
huffman@20755
  1255
      "f NSdifferentiable x ==>
huffman@20755
  1256
      increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
huffman@20755
  1257
      hypreal_of_real (f x)"
huffman@20755
  1258
by (simp add: increment_def)
huffman@20755
  1259
huffman@20755
  1260
lemma incrementI2: "NSDERIV f x :> D ==>
huffman@20755
  1261
     increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
huffman@20755
  1262
     hypreal_of_real (f x)"
huffman@20755
  1263
apply (erule NSdifferentiableI [THEN incrementI])
huffman@20755
  1264
done
huffman@20755
  1265
huffman@20755
  1266
(* The Increment theorem -- Keisler p. 65 *)
huffman@20755
  1267
lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
huffman@20755
  1268
      ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
huffman@20755
  1269
apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
huffman@20755
  1270
apply (drule bspec, auto)
huffman@20755
  1271
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
huffman@20755
  1272
apply (frule_tac b1 = "hypreal_of_real (D) + y"
huffman@20755
  1273
        in hypreal_mult_right_cancel [THEN iffD2])
huffman@20755
  1274
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@20755
  1275
apply assumption
huffman@20755
  1276
apply (simp add: times_divide_eq_right [symmetric])
huffman@20755
  1277
apply (auto simp add: left_distrib)
huffman@20755
  1278
done
huffman@20755
  1279
huffman@20755
  1280
lemma increment_thm2:
huffman@20755
  1281
     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
huffman@20755
  1282
      ==> \<exists>e \<in> Infinitesimal. increment f x h =
huffman@20755
  1283
              hypreal_of_real(D)*h + e*h"
huffman@20755
  1284
by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
huffman@20755
  1285
huffman@20755
  1286
huffman@20755
  1287
lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
huffman@20755
  1288
      ==> increment f x h \<approx> 0"
huffman@20755
  1289
apply (drule increment_thm2,
huffman@20755
  1290
       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
huffman@20755
  1291
apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
huffman@20755
  1292
done
huffman@20755
  1293
huffman@20755
  1294
subsection {* Nested Intervals and Bisection *}
huffman@20755
  1295
paulson@15234
  1296
text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).
paulson@15234
  1297
     All considerably tidied by lcp.*}
paulson@14477
  1298
paulson@14477
  1299
lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) --> f m \<le> f(m + no)"
paulson@15251
  1300
apply (induct "no")
paulson@14477
  1301
apply (auto intro: order_trans)
paulson@14477
  1302
done
paulson@14477
  1303
paulson@14477
  1304
lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
paulson@14477
  1305
         \<forall>n. g(Suc n) \<le> g(n);
paulson@14477
  1306
         \<forall>n. f(n) \<le> g(n) |]
huffman@20552
  1307
      ==> Bseq (f :: nat \<Rightarrow> real)"
paulson@14477
  1308
apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
paulson@14477
  1309
apply (induct_tac "n")
paulson@14477
  1310
apply (auto intro: order_trans)
paulson@15234
  1311
apply (rule_tac y = "g (Suc na)" in order_trans)
paulson@14477
  1312
apply (induct_tac [2] "na")
paulson@14477
  1313
apply (auto intro: order_trans)
paulson@14477
  1314
done
paulson@14477
  1315
paulson@14477
  1316
lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
paulson@14477
  1317
         \<forall>n. g(Suc n) \<le> g(n);
paulson@14477
  1318
         \<forall>n. f(n) \<le> g(n) |]
huffman@20552
  1319
      ==> Bseq (g :: nat \<Rightarrow> real)"
paulson@14477
  1320
apply (subst Bseq_minus_iff [symmetric])
paulson@15234
  1321
apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
paulson@14477
  1322
apply auto
paulson@14477
  1323
done
paulson@14477
  1324
huffman@20693
  1325
lemma f_inc_imp_le_lim:
huffman@20693
  1326
  fixes f :: "nat \<Rightarrow> real"
huffman@20693
  1327
  shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
paulson@14477
  1328
apply (rule linorder_not_less [THEN iffD1])
paulson@14477
  1329
apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
paulson@14477
  1330
apply (drule real_less_sum_gt_zero)
paulson@14477
  1331
apply (drule_tac x = "f n + - lim f" in spec, safe)
paulson@14477
  1332
apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
paulson@14477
  1333
apply (subgoal_tac "lim f \<le> f (no + n) ")
paulson@14477
  1334
apply (drule_tac no=no and m=n in lemma_f_mono_add)
paulson@14477
  1335
apply (auto simp add: add_commute)
webertj@20254
  1336
apply (induct_tac "no")
webertj@20254
  1337
apply simp
webertj@20254
  1338
apply (auto intro: order_trans simp add: diff_minus abs_if)
paulson@14477
  1339
done
paulson@14477
  1340
paulson@14477
  1341
lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)"
paulson@14477
  1342
apply (rule LIMSEQ_minus [THEN limI])
paulson@14477
  1343
apply (simp add: convergent_LIMSEQ_iff)
paulson@14477
  1344
done
paulson@14477
  1345
huffman@20693
  1346
lemma g_dec_imp_lim_le:
huffman@20693
  1347
  fixes g :: "nat \<Rightarrow> real"
huffman@20693
  1348
  shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n"
paulson@14477
  1349
apply (subgoal_tac "- (g n) \<le> - (lim g) ")
paulson@15234
  1350
apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim)
paulson@14477
  1351
apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
paulson@14477
  1352
done
paulson@14477
  1353
paulson@14477
  1354
lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
paulson@14477
  1355
         \<forall>n. g(Suc n) \<le> g(n);
paulson@14477
  1356
         \<forall>n. f(n) \<le> g(n) |]
huffman@20552
  1357
      ==> \<exists>l m :: real. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
paulson@14477
  1358
                            ((\<forall>n. m \<le> g(n)) & g ----> m)"
paulson@14477
  1359
apply (subgoal_tac "monoseq f & monoseq g")
paulson@14477
  1360
prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
paulson@14477
  1361
apply (subgoal_tac "Bseq f & Bseq g")
paulson@14477
  1362
prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g)
paulson@14477
  1363
apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff)
paulson@14477
  1364
apply (rule_tac x = "lim f" in exI)
paulson@14477
  1365
apply (rule_tac x = "lim g" in exI)
paulson@14477
  1366
apply (auto intro: LIMSEQ_le)
paulson@14477
  1367
apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff)
paulson@14477
  1368
done
paulson@14477
  1369
paulson@14477
  1370
lemma lemma_nest_unique: "[| \<forall>n. f(n) \<le> f(Suc n);
paulson@14477
  1371
         \<forall>n. g(Suc n) \<le> g(n);
paulson@14477
  1372
         \<forall>n. f(n) \<le> g(n);
paulson@14477
  1373
         (%n. f(n) - g(n)) ----> 0 |]
huffman@20552
  1374
      ==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f ----> l) &
paulson@14477
  1375
                ((\<forall>n. l \<le> g(n)) & g ----> l)"
paulson@14477
  1376
apply (drule lemma_nest, auto)
paulson@14477
  1377
apply (subgoal_tac "l = m")
paulson@14477
  1378
apply (drule_tac [2] X = f in LIMSEQ_diff)
paulson@14477
  1379
apply (auto intro: LIMSEQ_unique)
paulson@14477
  1380
done
paulson@14477
  1381
paulson@14477
  1382
text{*The universal quantifiers below are required for the declaration
paulson@14477
  1383
  of @{text Bolzano_nest_unique} below.*}
paulson@14477
  1384
paulson@14477
  1385
lemma Bolzano_bisect_le:
paulson@14477
  1386
 "a \<le> b ==> \<forall>n. fst (Bolzano_bisect P a b n) \<le> snd (Bolzano_bisect P a b n)"
paulson@14477
  1387
apply (rule allI)
paulson@14477
  1388
apply (induct_tac "n")
paulson@14477
  1389
apply (auto simp add: Let_def split_def)
paulson@14477
  1390
done
paulson@14477
  1391
paulson@14477
  1392
lemma Bolzano_bisect_fst_le_Suc: "a \<le> b ==>
paulson@14477
  1393
   \<forall>n. fst(Bolzano_bisect P a b n) \<le> fst (Bolzano_bisect P a b (Suc n))"
paulson@14477
  1394
apply (rule allI)
paulson@14477
  1395
apply (induct_tac "n")
paulson@14477
  1396
apply (auto simp add: Bolzano_bisect_le Let_def split_def)
paulson@14477
  1397
done
paulson@14477
  1398
paulson@14477
  1399
lemma Bolzano_bisect_Suc_le_snd: "a \<le> b ==>
paulson@14477
  1400
   \<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
paulson@14477
  1401
apply (rule allI)
paulson@14477
  1402
apply (induct_tac "n")
nipkow@15539
  1403
apply (auto simp add: Bolzano_bisect_le Let_def split_def)
paulson@14477
  1404
done
paulson@14477
  1405
kleing@19023
  1406
lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
nipkow@15539
  1407
apply (auto)
paulson@14477
  1408
apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
nipkow@15539
  1409
apply (simp)
paulson@14477
  1410
done
paulson@14477
  1411
paulson@14477
  1412
lemma Bolzano_bisect_diff:
paulson@14477
  1413
     "a \<le> b ==>
paulson@14477
  1414
      snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) =
paulson@14477
  1415
      (b-a) / (2 ^ n)"
paulson@15251
  1416
apply (induct "n")
paulson@14477
  1417
apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def)
paulson@14477
  1418
done
paulson@14477
  1419
paulson@14477
  1420
lemmas Bolzano_nest_unique =
paulson@14477
  1421
    lemma_nest_unique
paulson@14477
  1422
    [OF Bolzano_bisect_fst_le_Suc Bolzano_bisect_Suc_le_snd Bolzano_bisect_le]
paulson@14477
  1423
paulson@14477
  1424
paulson@14477
  1425
lemma not_P_Bolzano_bisect:
paulson@14477
  1426
  assumes P:    "!!a b c. [| P(a,b); P(b,c); a \<le> b; b \<le> c|] ==> P(a,c)"
paulson@14477
  1427
      and notP: "~ P(a,b)"
paulson@14477
  1428
      and le:   "a \<le> b"
paulson@14477
  1429
  shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
paulson@14477
  1430
proof (induct n)
paulson@14477
  1431
  case 0 thus ?case by simp
paulson@14477
  1432
 next
paulson@14477
  1433
  case (Suc n)
paulson@14477
  1434
  thus ?case
paulson@15228
  1435
 by (auto simp del: surjective_pairing [symmetric]
paulson@15228
  1436
             simp add: Let_def split_def Bolzano_bisect_le [OF le]
paulson@15228
  1437
     P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"])
paulson@14477
  1438
qed
paulson@14477
  1439
paulson@14477
  1440
(*Now we re-package P_prem as a formula*)
paulson@14477
  1441
lemma not_P_Bolzano_bisect':
paulson@14477
  1442
     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
paulson@14477
  1443
         ~ P(a,b);  a \<le> b |] ==>
paulson@14477
  1444
      \<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
paulson@14477
  1445
by (blast elim!: not_P_Bolzano_bisect [THEN [2] rev_notE])
paulson@14477
  1446
paulson@14477
  1447
paulson@14477
  1448
paulson@14477
  1449
lemma lemma_BOLZANO:
paulson@14477
  1450
     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
paulson@14477
  1451
         \<forall>x. \<exists>d::real. 0 < d &
paulson@14477
  1452
                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
paulson@14477
  1453
         a \<le> b |]
paulson@14477
  1454
      ==> P(a,b)"
paulson@14477
  1455
apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+)
paulson@14477
  1456
apply (rule LIMSEQ_minus_cancel)
paulson@14477
  1457
apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
paulson@14477
  1458
apply (rule ccontr)
paulson@14477
  1459
apply (drule not_P_Bolzano_bisect', assumption+)
paulson@14477
  1460
apply (rename_tac "l")
paulson@14477
  1461
apply (drule_tac x = l in spec, clarify)
paulson@14477
  1462
apply (simp add: LIMSEQ_def)
paulson@14477
  1463
apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
paulson@14477
  1464
apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
paulson@15228
  1465
apply (drule real_less_half_sum, auto)
paulson@14477
  1466
apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec)
paulson@14477
  1467
apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec)
paulson@14477
  1468
apply safe
paulson@14477
  1469
apply (simp_all (no_asm_simp))
paulson@15234
  1470
apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l)" in order_le_less_trans)
paulson@14477
  1471
apply (simp (no_asm_simp) add: abs_if)
paulson@14477
  1472
apply (rule real_sum_of_halves [THEN subst])
paulson@14477
  1473
apply (rule add_strict_mono)
paulson@14477
  1474
apply (simp_all add: diff_minus [symmetric])
paulson@14477
  1475
done
paulson@14477
  1476
paulson@14477
  1477
paulson@14477
  1478
lemma lemma_BOLZANO2: "((\<forall>a b c. (a \<le> b & b \<le> c & P(a,b) & P(b,c)) --> P(a,c)) &
paulson@14477
  1479
       (\<forall>x. \<exists>d::real. 0 < d &
paulson@14477
  1480
                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b))))
paulson@14477
  1481
      --> (\<forall>a b. a \<le> b --> P(a,b))"
paulson@14477
  1482
apply clarify
paulson@14477
  1483
apply (blast intro: lemma_BOLZANO)
paulson@14477
  1484
done
paulson@14477
  1485
paulson@14477
  1486
huffman@20755
  1487
subsection {* Intermediate Value Theorem *}
huffman@20755
  1488
huffman@20755
  1489
text {*Prove Contrapositive by Bisection*}
paulson@14477
  1490
huffman@20561
  1491
lemma IVT: "[| f(a::real) \<le> (y::real); y \<le> f(b);
paulson@14477
  1492
         a \<le> b;
paulson@14477
  1493
         (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
paulson@14477
  1494
      ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
paulson@14477
  1495
apply (rule contrapos_pp, assumption)
paulson@14477
  1496
apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2)
paulson@14477
  1497
apply safe
paulson@14477
  1498
apply simp_all
paulson@14477
  1499
apply (simp add: isCont_iff LIM_def)
paulson@14477
  1500
apply (rule ccontr)
paulson@14477
  1501
apply (subgoal_tac "a \<le> x & x \<le> b")
paulson@14477
  1502
 prefer 2
paulson@15228
  1503
 apply simp
paulson@14477
  1504
 apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
paulson@14477
  1505
apply (drule_tac x = x in spec)+
paulson@14477
  1506
apply simp
nipkow@15360
  1507
apply (drule_tac P = "%r. ?P r --> (\<exists>s>0. ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
paulson@14477
  1508
apply safe
paulson@14477
  1509
apply simp
paulson@14477
  1510
apply (drule_tac x = s in spec, clarify)
paulson@14477
  1511
apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe)
paulson@14477
  1512
apply (drule_tac x = "ba-x" in spec)
paulson@14477
  1513
apply (simp_all add: abs_if)
paulson@14477
  1514
apply (drule_tac x = "aa-x" in spec)
paulson@14477
  1515
apply (case_tac "x \<le> aa", simp_all)
paulson@14477
  1516
done
paulson@14477
  1517
huffman@20561
  1518
lemma IVT2: "[| f(b::real) \<le> (y::real); y \<le> f(a);
paulson@14477
  1519
         a \<le> b;
paulson@14477
  1520
         (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
paulson@14477
  1521
      |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
paulson@15228
  1522
apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
paulson@14477
  1523
apply (drule IVT [where f = "%x. - f x"], assumption)
paulson@14477
  1524
apply (auto intro: isCont_minus)
paulson@14477
  1525
done
paulson@14477
  1526
paulson@14477
  1527
(*HOL style here: object-level formulations*)
huffman@20561
  1528
lemma IVT_objl: "(f(a::real) \<le> (y::real) & y \<le> f(b) & a \<le> b &
paulson@14477
  1529
      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
paulson@14477
  1530
      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
paulson@14477
  1531
apply (blast intro: IVT)
paulson@14477
  1532
done
paulson@14477
  1533
huffman@20561
  1534
lemma IVT2_objl: "(f(b::real) \<le> (y::real) & y \<le> f(a) & a \<le> b &
paulson@14477
  1535
      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
paulson@14477
  1536
      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
paulson@14477
  1537
apply (blast intro: IVT2)
paulson@14477
  1538
done
paulson@14477
  1539
huffman@20755
  1540
text{*By bisection, function continuous on closed interval is bounded above*}
paulson@14477
  1541
paulson@14477
  1542
lemma isCont_bounded:
paulson@14477
  1543
     "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
huffman@20561
  1544
      ==> \<exists>M::real. \<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M"
paulson@15234
  1545
apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2)
paulson@14477
  1546
apply safe
paulson@14477
  1547
apply simp_all
paulson@14477
  1548
apply (rename_tac x xa ya M Ma)
paulson@14477
  1549
apply (cut_tac x = M and y = Ma in linorder_linear, safe)
paulson@14477
  1550
apply (rule_tac x = Ma in exI, clarify)
paulson@14477
  1551
apply (cut_tac x = xb and y = xa in linorder_linear, force)
paulson@14477
  1552
apply (rule_tac x = M in exI, clarify)
paulson@14477
  1553
apply (cut_tac x = xb and y = xa in linorder_linear, force)
paulson@14477
  1554
apply (case_tac "a \<le> x & x \<le> b")
paulson@14477
  1555
apply (rule_tac [2] x = 1 in exI)
paulson@14477
  1556
prefer 2 apply force
paulson@14477
  1557
apply (simp add: LIM_def isCont_iff)
paulson@14477
  1558
apply (drule_tac x = x in spec, auto)
paulson@14477
  1559
apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
paulson@14477
  1560
apply (drule_tac x = 1 in spec, auto)
paulson@14477
  1561
apply (rule_tac x = s in exI, clarify)
paulson@14477
  1562
apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
paulson@14477
  1563
apply (drule_tac x = "xa-x" in spec)
webertj@20217
  1564
apply (auto simp add: abs_ge_self)
paulson@14477
  1565
done
paulson@14477
  1566
paulson@15234
  1567
text{*Refine the above to existence of least upper bound*}
paulson@14477
  1568
paulson@14477
  1569
lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) -->
paulson@14477
  1570
      (\<exists>t. isLub UNIV S t)"
paulson@15234
  1571
by (blast intro: reals_complete)
paulson@14477
  1572
paulson@14477
  1573
lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
huffman@20561
  1574
         ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M) &
paulson@14477
  1575
                   (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
kleing@19023
  1576
apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
paulson@15234
  1577
        in lemma_reals_complete)
paulson@14477
  1578
apply auto
paulson@14477
  1579
apply (drule isCont_bounded, assumption)
paulson@14477
  1580
apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
paulson@14477
  1581
apply (rule exI, auto)
paulson@15228
  1582
apply (auto dest!: spec simp add: linorder_not_less)
paulson@14477
  1583
done
paulson@14477
  1584
paulson@15234
  1585
text{*Now show that it attains its upper bound*}
paulson@14477
  1586
paulson@14477
  1587
lemma isCont_eq_Ub:
paulson@14477
  1588
  assumes le: "a \<le> b"
huffman@20561
  1589
      and con: "\<forall>x::real. a \<le> x & x \<le> b --> isCont f x"
huffman@20552
  1590
  shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
paulson@14477
  1591
             (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
paulson@14477
  1592
proof -
paulson@14477
  1593
  from isCont_has_Ub [OF le con]
paulson@14477
  1594
  obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
paulson@14477
  1595
             and M2: "!!N. N<M ==> \<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x"  by blast
paulson@14477
  1596
  show ?thesis
paulson@14477
  1597
  proof (intro exI, intro conjI)
paulson@14477
  1598
    show " \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" by (rule M1)
paulson@15228
  1599
    show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M"
paulson@14477
  1600
    proof (rule ccontr)
paulson@14477
  1601
      assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
paulson@14477
  1602
      with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
nipkow@15195
  1603
        by (fastsimp simp add: linorder_not_le [symmetric])
paulson@14477
  1604
      hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
paulson@14477
  1605
        by (auto simp add: isCont_inverse isCont_diff con)
paulson@14477
  1606
      from isCont_bounded [OF le this]
paulson@14477
  1607
      obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
paulson@14477
  1608
      have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
paulson@15228
  1609
        by (simp add: M3 compare_rls)
paulson@15228
  1610
      have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k
paulson@15228
  1611
        by (auto intro: order_le_less_trans [of _ k])
paulson@15228
  1612
      with Minv
paulson@15228
  1613
      have "!!x. a \<le> x & x \<le> b --> inverse(k+1) < inverse(inverse(M - f x))"
paulson@14477
  1614
        by (intro strip less_imp_inverse_less, simp_all)
paulson@15228
  1615
      hence invlt: "!!x. a \<le> x & x \<le> b --> inverse(k+1) < M - f x"
paulson@14477
  1616
        by simp
paulson@15228
  1617
      have "M - inverse (k+1) < M" using k [of a] Minv [of a] le
paulson@14477
  1618
        by (simp, arith)
paulson@14477
  1619
      from M2 [OF this]
paulson@14477
  1620
      obtain x where ax: "a \<le> x & x \<le> b & M - inverse(k+1) < f x" ..
paulson@14477
  1621
      thus False using invlt [of x] by force
paulson@14477
  1622
    qed
paulson@14477
  1623
  qed
paulson@14477
  1624
qed
paulson@14477
  1625
paulson@14477
  1626
paulson@15234
  1627
text{*Same theorem for lower bound*}
paulson@14477
  1628
paulson@14477
  1629
lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
huffman@20561
  1630
         ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> M \<le> f(x)) &
paulson@14477
  1631
                   (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
paulson@14477
  1632
apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
paulson@14477
  1633
prefer 2 apply (blast intro: isCont_minus)
paulson@15234
  1634
apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub)
paulson@14477
  1635
apply safe
paulson@14477
  1636
apply auto
paulson@14477
  1637
done
paulson@14477
  1638
paulson@14477
  1639
paulson@15234
  1640
text{*Another version.*}
paulson@14477
  1641
paulson@14477
  1642
lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
huffman@20561
  1643
      ==> \<exists>L M::real. (\<forall>x::real. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
paulson@14477
  1644
          (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))"
paulson@14477
  1645
apply (frule isCont_eq_Lb)
paulson@14477
  1646
apply (frule_tac [2] isCont_eq_Ub)
paulson@14477
  1647
apply (assumption+, safe)
paulson@14477
  1648
apply (rule_tac x = "f x" in exI)
paulson@14477
  1649
apply (rule_tac x = "f xa" in exI, simp, safe)
paulson@14477
  1650
apply (cut_tac x = x and y = xa in linorder_linear, safe)
paulson@14477
  1651
apply (cut_tac f = f and a = x and b = xa and y = y in IVT_objl)
paulson@14477
  1652
apply (cut_tac [2] f = f and a = xa and b = x and y = y in IVT2_objl, safe)
paulson@14477
  1653
apply (rule_tac [2] x = xb in exI)
paulson@14477
  1654
apply (rule_tac [4] x = xb in exI, simp_all)
paulson@14477
  1655
done
paulson@14477
  1656
paulson@15003
  1657
huffman@20755
  1658
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
paulson@14477
  1659
paulson@14477
  1660
lemma DERIV_left_inc:
huffman@20793
  1661
  fixes f :: "real => real"
paulson@15003
  1662
  assumes der: "DERIV f x :> l"
paulson@15003
  1663
      and l:   "0 < l"
nipkow@15360
  1664
  shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x + h)"
paulson@15003
  1665
proof -
paulson@15003
  1666
  from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
nipkow@15360
  1667
  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
paulson@15003
  1668
    by (simp add: diff_minus)
paulson@15003
  1669
  then obtain s
paulson@15228
  1670
        where s:   "0 < s"
paulson@15003
  1671
          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
paulson@15003
  1672
    by auto
paulson@15003
  1673
  thus ?thesis
paulson@15003
  1674
  proof (intro exI conjI strip)
paulson@15003
  1675
    show "0<s" .
paulson@15003
  1676
    fix h::real
nipkow@15360
  1677
    assume "0 < h" "h < s"
paulson@15228
  1678
    with all [of h] show "f x < f (x+h)"
paulson@15228
  1679
    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
kleing@19023
  1680
    split add: split_if_asm)
paulson@15228
  1681
      assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
paulson@15228
  1682
      with l
paulson@15003
  1683
      have "0 < (f (x+h) - f x) / h" by arith
paulson@15003
  1684
      thus "f x < f (x+h)"
kleing@19023
  1685
  by (simp add: pos_less_divide_eq h)
paulson@15003
  1686
    qed
paulson@15003
  1687
  qed
paulson@15003
  1688
qed
paulson@14477
  1689
paulson@14477
  1690
lemma DERIV_left_dec:
huffman@20793
  1691
  fixes f :: "real => real"
paulson@14477
  1692
  assumes der: "DERIV f x :> l"
paulson@14477
  1693
      and l:   "l < 0"
nipkow@15360
  1694
  shows "\<exists>d > 0. \<forall>h > 0. h < d --> f(x) < f(x-h)"
paulson@14477
  1695
proof -
paulson@14477
  1696
  from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
nipkow@15360
  1697
  have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
paulson@14477
  1698
    by (simp add: diff_minus)
paulson@14477
  1699
  then obtain s
paulson@15228
  1700
        where s:   "0 < s"
paulson@14477
  1701
          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
paulson@14477
  1702
    by auto
paulson@14477
  1703
  thus ?thesis
paulson@14477
  1704
  proof (intro exI conjI strip)
paulson@14477
  1705
    show "0<s" .
paulson@14477
  1706
    fix h::real
nipkow@15360
  1707
    assume "0 < h" "h < s"
paulson@15228
  1708
    with all [of "-h"] show "f x < f (x-h)"
paulson@15228
  1709
    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
kleing@19023
  1710
    split add: split_if_asm)
paulson@15228
  1711
      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
paulson@15228
  1712
      with l
paulson@14477
  1713
      have "0 < (f (x-h) - f x) / h" by arith
paulson@14477
  1714
      thus "f x < f (x-h)"
kleing@19023
  1715
  by (simp add: pos_less_divide_eq h)
paulson@14477
  1716
    qed
paulson@14477
  1717
  qed
paulson@14477
  1718
qed
paulson@14477
  1719
paulson@15228
  1720
lemma DERIV_local_max:
huffman@20793
  1721
  fixes f :: "real => real"
paulson@14477
  1722
  assumes der: "DERIV f x :> l"
paulson@14477
  1723
      and d:   "0 < d"
paulson@14477
  1724
      and le:  "\<forall>y. \<bar>x-y\<bar> < d --> f(y) \<le> f(x)"
paulson@14477
  1725
  shows "l = 0"
paulson@14477
  1726
proof (cases rule: linorder_cases [of l 0])
paulson@14477
  1727
  case equal show ?thesis .
paulson@14477
  1728
next
paulson@14477
  1729
  case less
paulson@14477
  1730
  from DERIV_left_dec [OF der less]
paulson@14477
  1731
  obtain d' where d': "0 < d'"
nipkow@15360
  1732
             and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x-h)" by blast
paulson@14477
  1733
  from real_lbound_gt_zero [OF d d']
paulson@14477
  1734
  obtain e where "0 < e \<and> e < d \<and> e < d'" ..
paulson@15228
  1735
  with lt le [THEN spec [where x="x-e"]]
paulson@14477
  1736
  show ?thesis by (auto simp add: abs_if)
paulson@14477
  1737
next
paulson@14477
  1738
  case greater
paulson@14477
  1739
  from DERIV_left_inc [OF der greater]
paulson@14477
  1740
  obtain d' where d': "0 < d'"
nipkow@15360
  1741
             and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" by blast
paulson@14477
  1742
  from real_lbound_gt_zero [OF d d']
paulson@14477
  1743
  obtain e where "0 < e \<and> e < d \<and> e < d'" ..
paulson@14477
  1744
  with lt le [THEN spec [where x="x+e"]]
paulson@14477
  1745
  show ?thesis by (auto simp add: abs_if)
paulson@14477
  1746
qed
paulson@14477
  1747
paulson@14477
  1748
paulson@14477
  1749
text{*Similar theorem for a local minimum*}
paulson@14477
  1750
lemma DERIV_local_min:
huffman@20793
  1751
  fixes f :: "real => real"
huffman@20793
  1752
  shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) \<le> f(y) |] ==> l = 0"
paulson@14477
  1753
by (drule DERIV_minus [THEN DERIV_local_max], auto)
paulson@14477
  1754
paulson@14477
  1755
paulson@14477
  1756
text{*In particular, if a function is locally flat*}
paulson@14477
  1757
lemma DERIV_local_const:
huffman@20793
  1758
  fixes f :: "real => real"
huffman@20793
  1759
  shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
paulson@14477
  1760
by (auto dest!: DERIV_local_max)
paulson@14477
  1761
paulson@14477
  1762
text{*Lemma about introducing open ball in open interval*}
paulson@14477
  1763
lemma lemma_interval_lt:
paulson@15228
  1764
     "[| a < x;  x < b |]
paulson@14477
  1765
      ==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a < y & y < b)"
paulson@14477
  1766
apply (simp add: abs_interval_iff)
paulson@14477
  1767
apply (insert linorder_linear [of "x-a" "b-x"], safe)
paulson@14477
  1768
apply (rule_tac x = "x-a" in exI)
paulson@14477
  1769
apply (rule_tac [2] x = "b-x" in exI, auto)
paulson@14477
  1770
done
paulson@14477
  1771
paulson@14477
  1772
lemma lemma_interval: "[| a < x;  x < b |] ==>
paulson@14477
  1773
        \<exists>d::real. 0 < d &  (\<forall>y. \<bar>x-y\<bar> < d --> a \<le> y & y \<le> b)"
paulson@14477
  1774
apply (drule lemma_interval_lt, auto)
paulson@14477
  1775
apply (auto intro!: exI)
paulson@14477
  1776
done
paulson@14477
  1777
paulson@14477
  1778
text{*Rolle's Theorem.
paulson@15228
  1779
   If @{term f} is defined and continuous on the closed interval
paulson@15228
  1780
   @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"},
paulson@14477
  1781
   and @{term "f(a) = f(b)"},
paulson@14477
  1782
   then there exists @{text "x0 \<in> (a,b)"} such that @{term "f'(x0) = 0"}*}
paulson@15228
  1783
theorem Rolle:
paulson@14477
  1784
  assumes lt: "a < b"
paulson@14477
  1785
      and eq: "f(a) = f(b)"
paulson@14477
  1786
      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
paulson@14477
  1787
      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
paulson@14477
  1788
  shows "\<exists>z. a < z & z < b & DERIV f z :> 0"
paulson@14477
  1789
proof -
paulson@14477
  1790
  have le: "a \<le> b" using lt by simp
paulson@14477
  1791
  from isCont_eq_Ub [OF le con]
paulson@15228
  1792
  obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x"
paulson@15228
  1793
             and alex: "a \<le> x" and xleb: "x \<le> b"
paulson@14477
  1794
    by blast
paulson@14477
  1795
  from isCont_eq_Lb [OF le con]
paulson@15228
  1796
  obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z"
paulson@15228
  1797
              and alex': "a \<le> x'" and x'leb: "x' \<le> b"
paulson@14477
  1798
    by blast
paulson@14477
  1799
  show ?thesis
paulson@14477
  1800
  proof cases
paulson@14477
  1801
    assume axb: "a < x & x < b"
paulson@14477
  1802
        --{*@{term f} attains its maximum within the interval*}
paulson@14477
  1803
    hence ax: "a<x" and xb: "x<b" by auto
paulson@14477
  1804
    from lemma_interval [OF ax xb]
paulson@14477
  1805
    obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
paulson@14477
  1806
      by blast
paulson@14477
  1807
    hence bound': "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> f y \<le> f x" using x_max
paulson@14477
  1808
      by blast
paulson@14477
  1809
    from differentiableD [OF dif [OF axb]]
paulson@14477
  1810
    obtain l where der: "DERIV f x :> l" ..
paulson@15228
  1811
    have "l=0" by (rule DERIV_local_max [OF der d bound'])
paulson@14477
  1812
        --{*the derivative at a local maximum is zero*}
paulson@14477
  1813
    thus ?thesis using ax xb der by auto
paulson@14477
  1814
  next
paulson@14477
  1815
    assume notaxb: "~ (a < x & x < b)"
paulson@14477
  1816
    hence xeqab: "x=a | x=b" using alex xleb by arith
paulson@15228
  1817
    hence fb_eq_fx: "f b = f x" by (auto simp add: eq)
paulson@14477
  1818
    show ?thesis
paulson@14477
  1819
    proof cases
paulson@14477
  1820
      assume ax'b: "a < x' & x' < b"
paulson@14477
  1821
        --{*@{term f} attains its minimum within the interval*}
paulson@14477
  1822
      hence ax': "a<x'" and x'b: "x'<b" by auto
paulson@14477
  1823
      from lemma_interval [OF ax' x'b]
paulson@14477
  1824
      obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
kleing@19023
  1825
  by blast
paulson@14477
  1826
      hence bound': "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> f x' \<le> f y" using x'_min
kleing@19023
  1827
  by blast
paulson@14477
  1828
      from differentiableD [OF dif [OF ax'b]]
paulson@14477
  1829
      obtain l where der: "DERIV f x' :> l" ..
paulson@15228
  1830
      have "l=0" by (rule DERIV_local_min [OF der d bound'])
paulson@14477
  1831
        --{*the derivative at a local minimum is zero*}
paulson@14477
  1832
      thus ?thesis using ax' x'b der by auto
paulson@14477
  1833
    next
paulson@14477
  1834
      assume notax'b: "~ (a < x' & x' < b)"
paulson@14477
  1835
        --{*@{term f} is constant througout the interval*}
paulson@14477
  1836
      hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith
paulson@15228
  1837
      hence fb_eq_fx': "f b = f x'" by (auto simp add: eq)
paulson@14477
  1838
      from dense [OF lt]
paulson@14477
  1839
      obtain r where ar: "a < r" and rb: "r < b" by blast
paulson@14477
  1840
      from lemma_interval [OF ar rb]
paulson@14477
  1841
      obtain d where d: "0<d" and bound: "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
kleing@19023
  1842
  by blast
paulson@15228
  1843
      have eq_fb: "\<forall>z. a \<le> z --> z \<le> b --> f z = f b"
paulson@15228
  1844
      proof (clarify)
paulson@14477
  1845
        fix z::real
paulson@14477
  1846
        assume az: "a \<le> z" and zb: "z \<le> b"
paulson@14477
  1847
        show "f z = f b"
paulson@14477
  1848
        proof (rule order_antisym)
nipkow@15195
  1849
          show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb)
nipkow@15195
  1850
          show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb)
paulson@14477
  1851
        qed
paulson@14477
  1852
      qed
paulson@14477
  1853
      have bound': "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> f r = f y"
paulson@14477
  1854
      proof (intro strip)
paulson@14477
  1855
        fix y::real
paulson@14477
  1856
        assume lt: "\<bar>r-y\<bar> < d"
paulson@15228
  1857
        hence "f y = f b" by (simp add: eq_fb bound)
paulson@14477
  1858
        thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le)
paulson@14477
  1859
      qed
paulson@14477
  1860
      from differentiableD [OF dif [OF conjI [OF ar rb]]]
paulson@14477
  1861
      obtain l where der: "DERIV f r :> l" ..
paulson@15228
  1862
      have "l=0" by (rule DERIV_local_const [OF der d bound'])
paulson@14477
  1863
        --{*the derivative of a constant function is zero*}
paulson@14477
  1864
      thus ?thesis using ar rb der by auto
paulson@14477
  1865
    qed
paulson@14477
  1866
  qed
paulson@14477
  1867
qed
paulson@14477
  1868
paulson@14477
  1869
paulson@14477
  1870
subsection{*Mean Value Theorem*}
paulson@14477
  1871
paulson@14477
  1872
lemma lemma_MVT:
paulson@14477
  1873
     "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
paulson@14477
  1874
proof cases
paulson@14477
  1875
  assume "a=b" thus ?thesis by simp
paulson@14477
  1876
next
paulson@15228
  1877
  assume "a\<noteq>b"
paulson@14477
  1878
  hence ba: "b-a \<noteq> 0" by arith
paulson@14477
  1879
  show ?thesis
paulson@14477
  1880
    by (rule real_mult_left_cancel [OF ba, THEN iffD1],
kleing@19023
  1881
        simp add: right_diff_distrib,
paulson@15234
  1882
        simp add: left_diff_distrib)
paulson@14477
  1883
qed
paulson@14477
  1884
paulson@15228
  1885
theorem MVT:
paulson@14477
  1886
  assumes lt:  "a < b"
paulson@14477
  1887
      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
paulson@14477
  1888
      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
paulson@14477
  1889
  shows "\<exists>l z. a < z & z < b & DERIV f z :> l &
paulson@14477
  1890
                   (f(b) - f(a) = (b-a) * l)"
paulson@14477
  1891
proof -
paulson@14477
  1892
  let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
paulson@14477
  1893
  have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
paulson@15228
  1894
    by (fast intro: isCont_diff isCont_const isCont_mult isCont_Id)
paulson@14477
  1895
  have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
paulson@14477
  1896
  proof (clarify)
paulson@14477
  1897
    fix x::real
paulson@14477
  1898
    assume ax: "a < x" and xb: "x < b"
paulson@14477
  1899
    from differentiableD [OF dif [OF conjI [OF ax xb]]]
paulson@14477
  1900
    obtain l where der: "DERIV f x :> l" ..
paulson@14477
  1901
    show "?F differentiable x"
paulson@14477
  1902
      by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"],
paulson@15228
  1903
          blast intro: DERIV_diff DERIV_cmult_Id der)
paulson@15228
  1904
  qed
paulson@14477
  1905
  from Rolle [where f = ?F, OF lt lemma_MVT contF difF]
paulson@15228
  1906
  obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0"
paulson@14477
  1907
    by blast
paulson@14477
  1908
  have "DERIV (%x. ((f b - f a)/(b-a)) * x) z :> (f b - f a)/(b-a)"
paulson@14477
  1909
    by (rule DERIV_cmult_Id)
paulson@15228
  1910
  hence derF: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z
paulson@14477
  1911
                   :> 0 + (f b - f a) / (b - a)"
paulson@14477
  1912
    by (rule DERIV_add [OF der])
paulson@15228
  1913
  show ?thesis
paulson@14477
  1914
  proof (intro exI conjI)
paulson@14477
  1915
    show "a < z" .
paulson@14477
  1916
    show "z < b" .
nipkow@15539
  1917
    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp)
paulson@14477
  1918
    show "DERIV f z :> ((f b - f a)/(b-a))"  using derF by simp
paulson@14477
  1919
  qed
paulson@14477
  1920
qed
paulson@14477
  1921
paulson@14477
  1922
paulson@14477
  1923
text{*A function is constant if its derivative is 0 over an interval.*}
paulson@14477
  1924
huffman@20793
  1925
lemma DERIV_isconst_end:
huffman@20793
  1926
  fixes f :: "real => real"
huffman@20793
  1927
  shows "[| a < b;
paulson@14477
  1928
         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
paulson@14477
  1929
         \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
nipkow@15360
  1930
        ==> f b = f a"
paulson@14477
  1931
apply (drule MVT, assumption)
paulson@14477
  1932
apply (blast intro: differentiableI)
paulson@14477
  1933
apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
paulson@14477
  1934
done
paulson@14477
  1935
huffman@20793
  1936
lemma DERIV_isconst1:
huffman@20793
  1937
  fixes f :: "real => real"
huffman@20793
  1938
  shows "[| a < b;
paulson@14477
  1939
         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
paulson@14477
  1940
         \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
paulson@14477
  1941
        ==> \<forall>x. a \<le> x & x \<le> b --> f x = f a"
paulson@14477
  1942
apply safe
paulson@14477
  1943
apply (drule_tac x = a in order_le_imp_less_or_eq, safe)
paulson@14477
  1944
apply (drule_tac b = x in DERIV_isconst_end, auto)
paulson@14477
  1945
done
paulson@14477
  1946
huffman@20793
  1947
lemma DERIV_isconst2:
huffman@20793
  1948
  fixes f :: "real => real"
huffman@20793
  1949
  shows "[| a < b;
paulson@14477
  1950
         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
paulson@14477
  1951
         \<forall>x. a < x & x < b --> DERIV f x :> 0;
paulson@14477
  1952
         a \<le> x; x \<le> b |]
paulson@14477
  1953
        ==> f x = f a"
paulson@14477
  1954
apply (blast dest: DERIV_isconst1)
paulson@14477
  1955
done
paulson@14477
  1956
huffman@20793
  1957
lemma DERIV_isconst_all:
huffman@20793
  1958
  fixes f :: "real => real"
huffman@20793
  1959
  shows "\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)"
paulson@14477
  1960
apply (rule linorder_cases [of x y])
paulson@14477
  1961
apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+
paulson@14477
  1962
done
paulson@14477
  1963
paulson@14477
  1964
lemma DERIV_const_ratio_const:
paulson@14477
  1965
     "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k"
paulson@14477
  1966
apply (rule linorder_cases [of a b], auto)
paulson@14477
  1967
apply (drule_tac [!] f = f in MVT)
paulson@14477
  1968
apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
paulson@14477
  1969
apply (auto dest: DERIV_unique simp add: left_distrib diff_minus)
paulson@14477
  1970
done
paulson@14477
  1971
paulson@14477
  1972
lemma DERIV_const_ratio_const2:
paulson@14477
  1973
     "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
paulson@14477
  1974
apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
nipkow@15539
  1975
apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc)
paulson@14477
  1976
done
paulson@14477
  1977
paulson@15228
  1978
lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
kleing@19023
  1979
by (simp)
paulson@14477
  1980
paulson@15228
  1981
lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
kleing@19023
  1982
by (simp)
paulson@14477
  1983
paulson@14477
  1984
text{*Gallileo's "trick": average velocity = av. of end velocities*}
paulson@14477
  1985
paulson@14477
  1986
lemma DERIV_const_average:
huffman@20793
  1987
  fixes v :: "real => real"
paulson@14477
  1988
  assumes neq: "a \<noteq> (b::real)"
paulson@14477
  1989
      and der: "\<forall>x. DERIV v x :> k"
paulson@14477
  1990
  shows "v ((a + b)/2) = (v a + v b)/2"
paulson@14477
  1991
proof (cases rule: linorder_cases [of a b])
paulson@14477
  1992
  case equal with neq show ?thesis by simp
paulson@14477
  1993
next
paulson@14477
  1994
  case less
paulson@14477
  1995
  have "(v b - v a) / (b - a) = k"
paulson@14477
  1996
    by (rule DERIV_const_ratio_const2 [OF neq der])
paulson@15228
  1997
  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp
paulson@14477
  1998
  moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k"
paulson@14477
  1999
    by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
paulson@14477
  2000
  ultimately show ?thesis using neq by force
paulson@14477
  2001
next
paulson@14477
  2002
  case greater
paulson@14477
  2003
  have "(v b - v a) / (b - a) = k"
paulson@14477
  2004
    by (rule DERIV_const_ratio_const2 [OF neq der])
paulson@15228
  2005
  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp
paulson@14477
  2006
  moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k"
paulson@14477
  2007
    by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
paulson@15228
  2008
  ultimately show ?thesis using neq by (force simp add: add_commute)
paulson@14477
  2009
qed
paulson@14477
  2010
paulson@14477
  2011
paulson@14477
  2012
text{*Dull lemma: an continuous injection on an interval must have a
paulson@14477
  2013
strict maximum at an end point, not in the middle.*}
paulson@14477
  2014
paulson@14477
  2015
lemma lemma_isCont_inj:
huffman@20552
  2016
  fixes f :: "real \<Rightarrow> real"
paulson@14477
  2017
  assumes d: "0 < d"
paulson@14477
  2018
      and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
paulson@14477
  2019
      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
paulson@14477
  2020
  shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
paulson@14477
  2021
proof (rule ccontr)
paulson@14477
  2022
  assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
paulson@15228
  2023
  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
paulson@14477
  2024
  show False
paulson@14477
  2025
  proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
paulson@14477
  2026
    case le
paulson@14477
  2027
    from d cont all [of "x+d"]
paulson@15228
  2028
    have flef: "f(x+d) \<le> f x"
paulson@15228
  2029
     and xlex: "x - d \<le> x"
paulson@15228
  2030
     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
paulson@14477
  2031
       by (auto simp add: abs_if)
paulson@14477
  2032
    from IVT [OF le flef xlex cont']
paulson@14477
  2033
    obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
paulson@14477
  2034
    moreover
paulson@14477
  2035
    hence "g(f x') = g (f(x+d))" by simp
paulson@14477
  2036
    ultimately show False using d inj [of x'] inj [of "x+d"]
paulson@14477
  2037
      by (simp add: abs_le_interval_iff)
paulson@14477
  2038
  next
paulson@14477
  2039
    case ge
paulson@14477
  2040
    from d cont all [of "x-d"]
paulson@15228
  2041
    have flef: "f(x-d) \<le> f x"
paulson@15228
  2042
     and xlex: "x \<le> x+d"
paulson@15228
  2043
     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
paulson@14477
  2044
       by (auto simp add: abs_if)
paulson@14477
  2045
    from IVT2 [OF ge flef xlex cont']
paulson@14477
  2046
    obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
paulson@14477
  2047
    moreover
paulson@14477
  2048
    hence "g(f x') = g (f(x-d))" by simp
paulson@14477
  2049
    ultimately show False using d inj [of x'] inj [of "x-d"]
paulson@14477
  2050
      by (simp add: abs_le_interval_iff)
paulson@14477
  2051
  qed
paulson@14477
  2052
qed
paulson@14477
  2053
paulson@14477
  2054
paulson@14477
  2055
text{*Similar version for lower bound.*}
paulson@14477
  2056
paulson@14477
  2057
lemma lemma_isCont_inj2:
huffman@20552
  2058
  fixes f g :: "real \<Rightarrow> real"
huffman@20552
  2059
  shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
paulson@14477
  2060
        \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
paulson@14477
  2061
      ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
paulson@14477
  2062
apply (insert lemma_isCont_inj
paulson@14477
  2063
          [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
paulson@15228
  2064
apply (simp add: isCont_minus linorder_not_le)
paulson@14477
  2065
done
paulson@14477
  2066
paulson@15228
  2067
text{*Show there's an interval surrounding @{term "f(x)"} in
paulson@14477
  2068
@{text "f[[x - d, x + d]]"} .*}
paulson@14477
  2069
paulson@15228
  2070
lemma isCont_inj_range:
huffman@20552
  2071
  fixes f :: "real \<Rightarrow> real"
paulson@14477
  2072
  assumes d: "0 < d"
paulson@14477
  2073
      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
paulson@14477
  2074
      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
nipkow@15360
  2075
  shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
paulson@14477
  2076
proof -
paulson@14477
  2077
  have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
paulson@14477
  2078
    by (auto simp add: abs_le_interval_iff)
paulson@14477
  2079
  from isCont_Lb_Ub [OF this]
paulson@15228
  2080
  obtain L M
paulson@14477
  2081
  where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
paulson@14477
  2082
    and all2 [rule_format]:
paulson@14477
  2083
           "\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>z. x-d \<le> z \<and> z \<le> x+d \<and> f z = y)"
paulson@14477
  2084
    by auto
paulson@14477
  2085
  with d have "L \<le> f x & f x \<le> M" by simp
paulson@14477
  2086
  moreover have "L \<noteq> f x"
paulson@14477
  2087
  proof -
paulson@14477
  2088
    from lemma_isCont_inj2 [OF d inj cont]
paulson@14477
  2089
    obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x"  by auto
paulson@14477
  2090
    thus ?thesis using all1 [of u] by arith
paulson@14477
  2091
  qed
paulson@14477
  2092
  moreover have "f x \<noteq> M"
paulson@14477
  2093
  proof -
paulson@14477
  2094
    from lemma_isCont_inj [OF d inj cont]
paulson@14477
  2095
    obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u"  by auto
paulson@14477
  2096
    thus ?thesis using all1 [of u] by arith
paulson@14477
  2097
  qed
paulson@14477
  2098
  ultimately have "L < f x & f x < M" by arith
paulson@14477
  2099
  hence "0 < f x - L" "0 < M - f x" by arith+
paulson@14477
  2100
  from real_lbound_gt_zero [OF this]
paulson@14477
  2101
  obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
paulson@14477
  2102
  thus ?thesis
paulson@14477
  2103
  proof (intro exI conjI)
paulson@14477
  2104
    show "0<e" .
paulson@14477
  2105
    show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
paulson@14477
  2106
    proof (intro strip)
paulson@14477
  2107
      fix y::real
paulson@14477
  2108
      assume "\<bar>y - f x\<bar> \<le> e"
paulson@14477
  2109
      with e have "L \<le> y \<and> y \<le> M" by arith
paulson@14477
  2110
      from all2 [OF this]
paulson@14477
  2111
      obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
paulson@15228
  2112
      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
paulson@14477
  2113
        by (force simp add: abs_le_interval_iff)
paulson@14477
  2114
    qed
paulson@14477
  2115
  qed
paulson@14477
  2116
qed
paulson@14477
  2117
paulson@14477
  2118
paulson@14477
  2119
text{*Continuity of inverse function*}
paulson@14477
  2120
paulson@14477
  2121
lemma isCont_inverse_function:
huffman@20561
  2122
  fixes f g :: "real \<Rightarrow> real"
paulson@14477
  2123
  assumes d: "0 < d"
paulson@14477
  2124
      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
paulson@14477
  2125
      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
paulson@14477
  2126
  shows "isCont g (f x)"
paulson@14477
  2127
proof (simp add: isCont_iff LIM_eq)
paulson@14477
  2128
  show "\<forall>r. 0 < r \<longrightarrow>
nipkow@15360
  2129
         (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
paulson@14477
  2130
  proof (intro strip)
paulson@14477
  2131
    fix r::real
paulson@14477
  2132
    assume r: "0<r"
paulson@14477
  2133
    from real_lbound_gt_zero [OF r d]
paulson@14477
  2134
    obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
paulson@14477
  2135
    with inj cont
paulson@15228
  2136
    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
paulson@14477
  2137
                  "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
paulson@14477
  2138
    from isCont_inj_range [OF e this]
paulson@15228
  2139
    obtain e' where e': "0 < e'"
paulson@14477
  2140
        and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
paulson@14477
  2141
          by blast
nipkow@15360
  2142
    show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
paulson@14477
  2143
    proof (intro exI conjI)
paulson@14477
  2144
      show "0<e'" .
paulson@14477
  2145
      show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
paulson@14477
  2146
      proof (intro strip)
paulson@14477
  2147
        fix z::real
paulson@14477
  2148
        assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
paulson@14477
  2149
        with e e_lt e_simps all [rule_format, of "f x + z"]
paulson@14477
  2150
        show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
paulson@14477
  2151
      qed
paulson@14477
  2152
    qed
paulson@14477
  2153
  qed
paulson@15228
  2154
qed
paulson@14477
  2155
kleing@19023
  2156
theorem GMVT:
kleing@19023
  2157
  assumes alb: "a < b"
kleing@19023
  2158
  and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
kleing@19023
  2159
  and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
kleing@19023
  2160
  and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
kleing@19023
  2161
  and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
kleing@19023
  2162
  shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
kleing@19023
  2163
proof -
kleing@19023
  2164
  let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
kleing@19023
  2165
  from prems have "a < b" by simp
kleing@19023
  2166
  moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
kleing@19023
  2167
  proof -
kleing@19023
  2168
    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
kleing@19023
  2169
    with gc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (f b - f a) * g x) x"
kleing@19023
  2170
      by (auto intro: isCont_mult)
kleing@19023
  2171
    moreover
kleing@19023
  2172
    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. g b - g a) x" by simp
kleing@19023
  2173
    with fc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (g b - g a) * f x) x"
kleing@19023
  2174
      by (auto intro: isCont_mult)
kleing@19023
  2175
    ultimately show ?thesis
kleing@19023
  2176
      by (fastsimp intro: isCont_diff)
kleing@19023
  2177
  qed
kleing@19023
  2178
  moreover
kleing@19023
  2179
  have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
kleing@19023
  2180
  proof -
kleing@19023
  2181
    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by (simp add: differentiable_const)
kleing@19023
  2182
    with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult)
kleing@19023
  2183
    moreover
kleing@19023
  2184
    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by (simp add: differentiable_const)
kleing@19023
  2185
    with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult)
kleing@19023
  2186
    ultimately show ?thesis by (simp add: differentiable_diff)
kleing@19023
  2187
  qed
kleing@19023
  2188
  ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
kleing@19023
  2189
  then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
kleing@19023
  2190
  then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
kleing@19023
  2191
kleing@19023
  2192
  from cdef have cint: "a < c \<and> c < b" by auto
kleing@19023
  2193
  with gd have "g differentiable c" by simp
kleing@19023
  2194
  hence "\<exists>D. DERIV g c :> D" by (rule differentiableD)
kleing@19023
  2195
  then obtain g'c where g'cdef: "DERIV g c :> g'c" ..
kleing@19023
  2196
kleing@19023
  2197
  from cdef have "a < c \<and> c < b" by auto
kleing@19023
  2198
  with fd have "f differentiable c" by simp
kleing@19023
  2199
  hence "\<exists>D. DERIV f c :> D" by (rule differentiableD)
kleing@19023
  2200
  then obtain f'c where f'cdef: "DERIV f c :> f'c" ..
kleing@19023
  2201
kleing@19023
  2202
  from cdef have "DERIV ?h c :> l" by auto
kleing@19023
  2203
  moreover
kleing@19023
  2204
  {
kleing@19023
  2205
    from g'cdef have "DERIV (\<lambda>x. (f b - f a) * g x) c :> g'c * (f b - f a)"
kleing@19023
  2206
      apply (insert DERIV_const [where k="f b - f a"])
kleing@19023
  2207
      apply (drule meta_spec [of _ c])
kleing@19023
  2208
      apply (drule DERIV_mult [where f="(\<lambda>x. f b - f a)" and g=g])
kleing@19023
  2209
      by simp_all
kleing@19023
  2210
    moreover from f'cdef have "DERIV (\<lambda>x. (g b - g a) * f x) c :> f'c * (g b - g a)"
kleing@19023
  2211
      apply (insert DERIV_const [where k="g b - g a"])
kleing@19023
  2212
      apply (drule meta_spec [of _ c])
kleing@19023
  2213
      apply (drule DERIV_mult [where f="(\<lambda>x. g b - g a)" and g=f])
kleing@19023
  2214
      by simp_all
kleing@19023
  2215
    ultimately have "DERIV ?h c :>  g'c * (f b - f a) - f'c * (g b - g a)"
kleing@19023
  2216
      by (simp add: DERIV_diff)
kleing@19023
  2217
  }
kleing@19023
  2218
  ultimately have leq: "l =  g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique)
kleing@19023
  2219
kleing@19023
  2220
  {
kleing@19023
  2221
    from cdef have "?h b - ?h a = (b - a) * l" by auto
kleing@19023
  2222
    also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
kleing@19023
  2223
    finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
kleing@19023
  2224
  }
kleing@19023
  2225
  moreover
kleing@19023
  2226
  {
kleing@19023
  2227
    have "?h b - ?h a =
kleing@19023
  2228
         ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) -
kleing@19023
  2229
          ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))"
kleing@19023
  2230
      by (simp add: mult_ac add_ac real_diff_mult_distrib)
kleing@19023
  2231
    hence "?h b - ?h a = 0" by auto
kleing@19023
  2232
  }
kleing@19023
  2233
  ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
kleing@19023
  2234
  with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp
kleing@19023
  2235
  hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp
kleing@19023
  2236
  hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac)
kleing@19023
  2237
kleing@19023
  2238
  with g'cdef f'cdef cint show ?thesis by auto
kleing@19023
  2239
qed
kleing@19023
  2240
kleing@19023
  2241
kleing@19023
  2242
lemma LIMSEQ_SEQ_conv1:
huffman@20561
  2243
  fixes a :: real
kleing@19023
  2244
  assumes "X -- a --> L"
kleing@19023
  2245
  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
kleing@19023
  2246
proof -
kleing@19023
  2247
  {
huffman@20563
  2248
    from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r" by (unfold LIM_def)
kleing@19023
  2249
    
kleing@19023
  2250
    fix S
kleing@19023
  2251
    assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a"
kleing@19023
  2252
    then have "S ----> a" by auto
huffman@20563
  2253
    then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n - a) < r))" by (unfold LIMSEQ_def)
kleing@19023
  2254
    {
kleing@19023
  2255
      fix r
huffman@20563
  2256
      from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp
kleing@19023
  2257
      {
kleing@19023
  2258
        assume rgz: "0 < r"
kleing@19023
  2259
huffman@20563
  2260
        from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r" by simp 
huffman@20563
  2261
        then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x - a\<bar> < s \<longrightarrow> norm (X x - L) < r)" by auto
huffman@20563
  2262
        then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x - a\<bar> < s \<longrightarrow> norm (X x - L) < r" by auto
kleing@19023
  2263
        {
kleing@19023
  2264
          fix n
huffman@20563
  2265
          from aux have "S n \<noteq> a \<and> \<bar>S n - a\<bar> < s \<longrightarrow> norm (X (S n) - L) < r" by simp
huffman@20563
  2266
          with as have imp2: "\<bar>S n - a\<bar> < s --> norm (X (S n) - L) < r" by auto
kleing@19023
  2267
        }
huffman@20563
  2268
        hence "\<forall>n. \<bar>S n - a\<bar> < s --> norm (X (S n) - L) < r" ..
kleing@19023
  2269
        moreover
huffman@20563
  2270
        from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n - a\<bar> < s" by auto  
huffman@20563
  2271
        then obtain no where "\<forall>n. no \<le> n --> \<bar>S n - a\<bar> < s" by auto
huffman@20563
  2272
        ultimately have "\<forall>n. no \<le> n \<longrightarrow> norm (X (S n) - L) < r" by simp
huffman@20563
  2273
        hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> norm (X (S n) - L) < r" by auto
kleing@19023
  2274
      }
kleing@19023
  2275
    }
huffman@20563
  2276
    hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X (S n) - L) < r))" by simp
kleing@19023
  2277
    hence "(\<lambda>n. X (S n)) ----> L" by (fold LIMSEQ_def)
kleing@19023
  2278
  }
kleing@19023
  2279
  thus ?thesis by simp
kleing@19023
  2280
qed
kleing@19023
  2281
webertj@20432
  2282
ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
webertj@20217
  2283
kleing@19023
  2284
lemma LIMSEQ_SEQ_conv2:
huffman@20561
  2285
  fixes a :: real
kleing@19023
  2286
  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
kleing@19023
  2287
  shows "X -- a --> L"
kleing@19023
  2288
proof (rule ccontr)
kleing@19023
  2289
  assume "\<not> (X -- a --> L)"
huffman@20563
  2290
  hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r)" by (unfold LIM_def)
huffman@20563
  2291
  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp
huffman@20563
  2292
  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" by (simp add: linorder_not_less)
huffman@20563
  2293
  then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r))" by auto
kleing@19023
  2294
huffman@20563
  2295
  let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
kleing@19023
  2296
  have "?F ----> a"
kleing@19023
  2297
  proof -
kleing@19023
  2298
    {
kleing@19023
  2299
      fix e::real
kleing@19023
  2300
      assume "0 < e"
kleing@19023
  2301
        (* choose no such that inverse (real (Suc n)) < e *)
kleing@19023
  2302
      have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
kleing@19023
  2303
      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
kleing@19023
  2304
      {
kleing@19023
  2305
        fix n
kleing@19023
  2306
        assume mlen: "m \<le> n"
kleing@19023
  2307
        then have
kleing@19023
  2308
          "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
kleing@19023
  2309
          by auto
kleing@19023
  2310
        moreover have
huffman@20563
  2311
          "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
kleing@19023
  2312
        proof -
kleing@19023
  2313
          from rdef have
huffman@20563
  2314
            "\<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
kleing@19023
  2315
            by simp
kleing@19023
  2316
          hence
huffman@20563
  2317
            "(?F n)\<noteq>a \<and> \<bar>(?F n) - a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) - L) \<ge> r"
kleing@19023
  2318
            by (simp add: some_eq_ex [symmetric])
kleing@19023
  2319
          thus ?thesis by simp
kleing@19023
  2320
        qed
kleing@19023
  2321
        moreover from nodef have
kleing@19023
  2322
          "inverse (real (Suc m)) < e" .
huffman@20563
  2323
        ultimately have "\<bar>?F n - a\<bar> < e" by arith
kleing@19023
  2324
      }
huffman@20563
  2325
      then have "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e" by auto
kleing@19023
  2326
    }
kleing@19023
  2327
    thus ?thesis by (unfold LIMSEQ_def, simp)
kleing@19023
  2328
  qed
kleing@19023
  2329
  
kleing@19023
  2330
  moreover have "\<forall>n. ?F n \<noteq> a"
kleing@19023
  2331
  proof -
kleing@19023
  2332
    {
kleing@19023
  2333
      fix n
kleing@19023
  2334
      from rdef have
huffman@20563
  2335
        "\<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
kleing@19023
  2336
        by simp
kleing@19023
  2337
      hence "?F n \<noteq> a" by (simp add: some_eq_ex [symmetric])
kleing@19023
  2338
    }
kleing@19023
  2339
    thus ?thesis ..
kleing@19023
  2340
  qed
kleing@19023
  2341
  moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
kleing@19023
  2342
  ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
kleing@19023
  2343
  
kleing@19023
  2344
  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
kleing@19023
  2345
  proof -
kleing@19023
  2346
    {
kleing@19023
  2347
      fix no::nat
kleing@19023
  2348
      obtain n where "n = no + 1" by simp
kleing@19023
  2349
      then have nolen: "no \<le> n" by simp
kleing@19023
  2350
        (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
huffman@20563
  2351
      from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" ..
kleing@19023
  2352
huffman@20563
  2353
      then have "\<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r" by simp
kleing@19023
  2354
      
huffman@20563
  2355
      hence "norm (X (?F n) - L) \<ge> r" by (simp add: some_eq_ex [symmetric])
huffman@20563
  2356
      with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by auto
kleing@19023
  2357
    }
huffman@20563
  2358
    then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
huffman@20563
  2359
    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
kleing@19023
  2360
    thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
kleing@19023
  2361
  qed
kleing@19023
  2362
  ultimately show False by simp
kleing@19023
  2363
qed
kleing@19023
  2364
webertj@20432
  2365
ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
kleing@19023
  2366
kleing@19023
  2367
lemma LIMSEQ_SEQ_conv:
huffman@20561
  2368
  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
huffman@20561
  2369
   (X -- a --> L)"
kleing@19023
  2370
proof
kleing@19023
  2371
  assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
kleing@19023
  2372
  show "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
kleing@19023
  2373
next
kleing@19023
  2374
  assume "(X -- a --> L)"
kleing@19023
  2375
  show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
kleing@19023
  2376
qed
kleing@19023
  2377
kleing@19023
  2378
lemma real_sqz:
kleing@19023
  2379
  fixes a::real
kleing@19023
  2380
  assumes "a < c"
kleing@19023
  2381
  shows "\<exists>b. a < b \<and> b < c"
huffman@20563
  2382
by (rule dense)
kleing@19023
  2383
kleing@19023
  2384
lemma LIM_offset:
kleing@19023
  2385
  assumes "(\<lambda>x. f x) -- a --> L"
kleing@19023
  2386
  shows "(\<lambda>x. f (x+c)) -- (a-c) --> L"
kleing@19023
  2387
proof -
kleing@19023
  2388
  have "f -- a --> L" .
kleing@19023
  2389
  hence
huffman@20563
  2390
    fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (f x - L) < r"
kleing@19023
  2391
    by (unfold LIM_def)
kleing@19023
  2392
  {
kleing@19023
  2393
    fix r::real
kleing@19023
  2394
    assume rgz: "0 < r"
huffman@20563
  2395
    with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> norm (x - a) < s --> norm (f x - L) < r" by simp
huffman@20563
  2396
    then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r" by auto
huffman@20563
  2397
    from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> norm ((x+c) - a) < s \<longrightarrow> norm (f (x+c) - L) < r" by auto
kleing@19023
  2398
    {
huffman@20561
  2399
      fix x
huffman@20563
  2400
      from ax2 have nt: "(x+c)\<noteq>a \<and> norm ((x+c) - a) < s \<longrightarrow> norm (f (x+c) - L) < r" ..
kleing@19023
  2401
      moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto
huffman@20563
  2402
      moreover have "((x+c) - a) = (x - (a-c))" by simp
huffman@20563
  2403
      ultimately have "x\<noteq>(a-c) \<and> norm (x - (a-c)) < s \<longrightarrow> norm (f (x+c) - L) < r" by simp
kleing@19023
  2404
    }
huffman@20563
  2405
    then have "\<forall>x. x\<noteq>(a-c) \<and> norm (x - (a-c)) < s \<longrightarrow> norm (f (x+c) - L) < r" ..
huffman@20563
  2406
    with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> norm (x - (a-c)) < s \<longrightarrow> norm (f (x+c) - L) < r" by auto
kleing@19023
  2407
  }
kleing@19023
  2408
  then have
huffman@20563
  2409
    "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & norm (x - (a-c)) < s --> norm (f (x+c) - L) < r" by simp
kleing@19023
  2410
  thus ?thesis by (fold LIM_def)
kleing@19023
  2411
qed
kleing@19023
  2412
paulson@10751
  2413
end