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