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