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