src/HOL/Hyperreal/Lim.thy
 changeset 14477 cc61fd03e589 parent 14387 e96d5c42c4b0 child 15003 6145dd7538d7
```     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Fri Mar 19 10:50:06 2004 +0100
1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Fri Mar 19 10:51:03 2004 +0100
1.3 @@ -1,66 +1,67 @@
1.4  (*  Title       : Lim.thy
1.5 +    ID          : \$Id\$
1.6      Author      : Jacques D. Fleuriot
1.7      Copyright   : 1998  University of Cambridge
1.8 -    Description : Theory of limits, continuity and
1.9 -                  differentiation of real=>real functions
1.10 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.11  *)
1.12
1.13 -Lim = SEQ + RealDef +
1.15
1.16 -(*-----------------------------------------------------------------------
1.17 -    Limits, continuity and differentiation: standard and NS definitions
1.18 - -----------------------------------------------------------------------*)
1.19 +theory Lim = SEQ + RealDef:
1.20 +
1.21 +text{*Standard and Nonstandard Definitions*}
1.22
1.23  constdefs
1.24 -  LIM :: [real=>real,real,real] => bool
1.25 +  LIM :: "[real=>real,real,real] => bool"
1.26  				("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
1.27    "f -- a --> L ==
1.28 -     ALL r. 0 < r -->
1.29 -	     (EX s. 0 < s & (ALL x. (x ~= a & (abs(x + -a) < s)
1.30 -			  --> abs(f x + -L) < r)))"
1.31 +     \<forall>r. 0 < r -->
1.32 +	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (\<bar>x + -a\<bar> < s)
1.33 +			  --> \<bar>f x + -L\<bar> < r)))"
1.34
1.35 -  NSLIM :: [real=>real,real,real] => bool
1.36 +  NSLIM :: "[real=>real,real,real] => bool"
1.37  			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
1.38 -  "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a &
1.39 +  "f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a &
1.40  		      x @= hypreal_of_real a -->
1.41 -		      ( *f* f) x @= hypreal_of_real L))"
1.42 +		      ( *f* f) x @= hypreal_of_real L))"
1.43
1.44 -  isCont :: [real=>real,real] => bool
1.45 -  "isCont f a == (f -- a --> (f a))"
1.46 +  isCont :: "[real=>real,real] => bool"
1.47 +  "isCont f a == (f -- a --> (f a))"
1.48
1.49    (* NS definition dispenses with limit notions *)
1.50 -  isNSCont :: [real=>real,real] => bool
1.51 -  "isNSCont f a == (ALL y. y @= hypreal_of_real a -->
1.52 +  isNSCont :: "[real=>real,real] => bool"
1.53 +  "isNSCont f a == (\<forall>y. y @= hypreal_of_real a -->
1.54  			   ( *f* f) y @= hypreal_of_real (f a))"
1.55
1.56    (* differentiation: D is derivative of function f at x *)
1.57 -  deriv:: [real=>real,real,real] => bool
1.58 +  deriv:: "[real=>real,real,real] => bool"
1.59  			    ("(DERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
1.60 -  "DERIV f x :> D == ((%h. (f(x + h) + -f(x))/h) -- 0 --> D)"
1.61 +  "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
1.62
1.63 -  nsderiv :: [real=>real,real,real] => bool
1.64 +  nsderiv :: "[real=>real,real,real] => bool"
1.65  			    ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
1.66 -  "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}.
1.67 -			(( *f* f)(hypreal_of_real x + h) +
1.68 +  "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
1.69 +			(( *f* f)(hypreal_of_real x + h) +
1.70  			 - hypreal_of_real (f x))/h @= hypreal_of_real D)"
1.71
1.72 -  differentiable :: [real=>real,real] => bool   (infixl 60)
1.73 -  "f differentiable x == (EX D. DERIV f x :> D)"
1.74 +  differentiable :: "[real=>real,real] => bool"   (infixl "differentiable" 60)
1.75 +  "f differentiable x == (\<exists>D. DERIV f x :> D)"
1.76
1.77 -  NSdifferentiable :: [real=>real,real] => bool   (infixl 60)
1.78 -  "f NSdifferentiable x == (EX D. NSDERIV f x :> D)"
1.79 +  NSdifferentiable :: "[real=>real,real] => bool"
1.80 +                       (infixl "NSdifferentiable" 60)
1.81 +  "f NSdifferentiable x == (\<exists>D. NSDERIV f x :> D)"
1.82
1.83 -  increment :: [real=>real,real,hypreal] => hypreal
1.84 -  "increment f x h == (@inc. f NSdifferentiable x &
1.85 +  increment :: "[real=>real,real,hypreal] => hypreal"
1.86 +  "increment f x h == (@inc. f NSdifferentiable x &
1.87  		       inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
1.88
1.89 -  isUCont :: (real=>real) => bool
1.90 -  "isUCont f ==  (ALL r. 0 < r -->
1.91 -		      (EX s. 0 < s & (ALL x y. abs(x + -y) < s
1.92 -			    --> abs(f x + -f y) < r)))"
1.93 +  isUCont :: "(real=>real) => bool"
1.94 +  "isUCont f ==  (\<forall>r. 0 < r -->
1.95 +		      (\<exists>s. 0 < s & (\<forall>x y. \<bar>x + -y\<bar> < s
1.96 +			    --> \<bar>f x + -f y\<bar> < r)))"
1.97
1.98 -  isNSUCont :: (real=>real) => bool
1.99 -  "isNSUCont f == (ALL x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
1.100 +  isNSUCont :: "(real=>real) => bool"
1.101 +  "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
1.102
1.103
1.104  (*Used in the proof of the Bolzano theorem*)
1.105 @@ -72,8 +73,2258 @@
1.106    "Bolzano_bisect P a b (Suc n) =
1.107        (let (x,y) = Bolzano_bisect P a b n
1.108         in if P(x, (x+y)/2) then ((x+y)/2, y)
1.109 -                            else (x, (x+y)/2) )"
1.110 -
1.111 +                            else (x, (x+y)/2))"
1.112 +
1.113 +
1.114 +
1.115 +section{*Some Purely Standard Proofs*}
1.116 +
1.117 +lemma LIM_eq:
1.118 +     "f -- a --> L =
1.119 +     (\<forall>r. 0<r --> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))"
1.120 +by (simp add: LIM_def diff_minus)
1.121 +
1.122 +lemma LIM_D:
1.123 +     "[| f -- a --> L; 0<r |]
1.124 +      ==> \<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)"
1.126 +
1.127 +lemma LIM_const: "(%x. k) -- x --> k"
1.129 +declare LIM_const [simp]
1.130 +
1.132 +  assumes f: "f -- a --> L" and g: "g -- a --> M"
1.133 +  shows "(%x. f x + g(x)) -- a --> (L + M)"
1.134 +proof (simp add: LIM_eq, clarify)
1.135 +  fix r :: real
1.136 +  assume r: "0<r"
1.137 +  from LIM_D [OF f half_gt_zero [OF r]]
1.138 +  obtain fs
1.139 +    where fs:    "0 < fs"
1.140 +      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x - L\<bar> < r/2"
1.141 +  by blast
1.142 +  from LIM_D [OF g half_gt_zero [OF r]]
1.143 +  obtain gs
1.144 +    where gs:    "0 < gs"
1.145 +      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x - M\<bar> < r/2"
1.146 +  by blast
1.147 +  show "\<exists>s. 0 < s \<and>
1.148 +            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>f x + g x - (L + M)\<bar> < r)"
1.149 +  proof (intro exI conjI strip)
1.150 +    show "0 < min fs gs"  by (simp add: fs gs)
1.151 +    fix x :: real
1.152 +    assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
1.153 +    with fs_lt gs_lt
1.154 +    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by (auto simp add: fs_lt)
1.155 +    hence "\<bar>f x - L\<bar> + \<bar>g x - M\<bar> < r" by arith
1.156 +    thus "\<bar>f x + g x - (L + M)\<bar> < r"
1.157 +      by (blast intro: abs_diff_triangle_ineq order_le_less_trans)
1.158 +  qed
1.159 +qed
1.160 +
1.161 +lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
1.163 +apply (subgoal_tac "\<forall>x. \<bar>- f x + L\<bar> = \<bar>f x - L\<bar>")
1.165 +done
1.166 +
1.168 +    "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
1.169 +by (blast dest: LIM_add LIM_minus)
1.170 +
1.171 +lemma LIM_diff:
1.172 +    "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
1.174 +
1.175 +
1.176 +lemma LIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
1.177 +proof (simp add: linorder_neq_iff LIM_eq, elim disjE)
1.178 +  assume k: "k < L"
1.179 +  show "\<exists>r. 0 < r \<and>
1.180 +        (\<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)"
1.181 +  proof (intro exI conjI strip)
1.182 +    show "0 < L-k" by (simp add: k)
1.183 +    fix s :: real
1.184 +    assume s: "0<s"
1.185 +    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
1.186 +     next
1.187 +      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
1.188 +     next
1.189 +      from s show "~ \<bar>k-L\<bar> < L-k" by (simp add: abs_if) }
1.190 +  qed
1.191 +next
1.192 +  assume k: "L < k"
1.193 +  show "\<exists>r. 0 < r \<and>
1.194 +        (\<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)"
1.195 +  proof (intro exI conjI strip)
1.196 +    show "0 < k-L" by (simp add: k)
1.197 +    fix s :: real
1.198 +    assume s: "0<s"
1.199 +    { from s show "s/2 + a < a \<or> a < s/2 + a" by arith
1.200 +     next
1.201 +      from s show "\<bar>s / 2 + a - a\<bar> < s" by (simp add: abs_if)
1.202 +     next
1.203 +      from s show "~ \<bar>k-L\<bar> < k-L" by (simp add: abs_if) }
1.204 +  qed
1.205 +qed
1.206 +
1.207 +lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L"
1.208 +apply (rule ccontr)
1.209 +apply (blast dest: LIM_const_not_eq)
1.210 +done
1.211 +
1.212 +lemma LIM_unique: "[| f -- a --> L; f -- a --> M |] ==> L = M"
1.213 +apply (drule LIM_diff, assumption)
1.214 +apply (auto dest!: LIM_const_eq)
1.215 +done
1.216 +
1.217 +lemma LIM_mult_zero:
1.218 +  assumes f: "f -- a --> 0" and g: "g -- a --> 0"
1.219 +  shows "(%x. f(x) * g(x)) -- a --> 0"
1.220 +proof (simp add: LIM_eq, clarify)
1.221 +  fix r :: real
1.222 +  assume r: "0<r"
1.223 +  from LIM_D [OF f zero_less_one]
1.224 +  obtain fs
1.225 +    where fs:    "0 < fs"
1.226 +      and fs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < fs --> \<bar>f x\<bar> < 1"
1.227 +  by auto
1.228 +  from LIM_D [OF g r]
1.229 +  obtain gs
1.230 +    where gs:    "0 < gs"
1.231 +      and gs_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < gs --> \<bar>g x\<bar> < r"
1.232 +  by auto
1.233 +  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)"
1.234 +  proof (intro exI conjI strip)
1.235 +    show "0 < min fs gs"  by (simp add: fs gs)
1.236 +    fix x :: real
1.237 +    assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
1.238 +    with fs_lt gs_lt
1.239 +    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by (auto simp add: fs_lt)
1.240 +    hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
1.241 +    thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
1.242 +  qed
1.243 +qed
1.244 +
1.245 +lemma LIM_self: "(%x. x) -- a --> a"
1.246 +by (auto simp add: LIM_def)
1.247 +
1.248 +text{*Limits are equal for functions equal except at limit point*}
1.249 +lemma LIM_equal:
1.250 +     "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
1.252 +
1.253 +text{*Two uses in Hyperreal/Transcendental.ML*}
1.254 +lemma LIM_trans:
1.255 +     "[| (%x. f(x) + -g(x)) -- a --> 0;  g -- a --> l |] ==> f -- a --> l"
1.258 +done
1.259 +
1.260 +
1.261 +subsection{*Relationships Between Standard and Nonstandard Concepts*}
1.262 +
1.263 +text{*Standard and NS definitions of Limit*} (*NEEDS STRUCTURING*)
1.264 +lemma LIM_NSLIM:
1.265 +      "f -- x --> L ==> f -- x --NS> L"
1.266 +apply (simp add: LIM_def NSLIM_def approx_def)
1.267 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
1.268 +apply (rule_tac z = xa in eq_Abs_hypreal)
1.270 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, clarify)
1.271 +apply (drule_tac x = u in spec, clarify)
1.272 +apply (drule_tac x = s in spec, clarify)
1.273 +apply (subgoal_tac "\<forall>n::nat. (xa n) \<noteq> x & abs ((xa n) + - x) < s --> abs (f (xa n) + - L) < u")
1.274 +prefer 2 apply blast
1.275 +apply (drule FreeUltrafilterNat_all, ultra)
1.276 +done
1.277 +
1.278 +(*---------------------------------------------------------------------
1.279 +    Limit: NS definition ==> standard definition
1.280 + ---------------------------------------------------------------------*)
1.281 +
1.282 +lemma lemma_LIM: "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
1.283 +         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
1.284 +      ==> \<forall>n::nat. \<exists>xa.  xa \<noteq> x &
1.285 +              \<bar>xa + -x\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f xa + -L\<bar>"
1.286 +apply clarify
1.287 +apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
1.288 +done
1.289 +
1.290 +lemma lemma_skolemize_LIM2:
1.291 +     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
1.292 +         \<bar>xa + - x\<bar> < s  & r \<le> \<bar>f xa + -L\<bar>)
1.293 +      ==> \<exists>X. \<forall>n::nat. X n \<noteq> x &
1.294 +                \<bar>X n + -x\<bar> < inverse(real(Suc n)) & r \<le> abs(f (X n) + -L)"
1.295 +apply (drule lemma_LIM)
1.296 +apply (drule choice, blast)
1.297 +done
1.298 +
1.299 +lemma lemma_simp: "\<forall>n. X n \<noteq> x &
1.300 +          \<bar>X n + - x\<bar> < inverse (real(Suc n)) &
1.301 +          r \<le> abs (f (X n) + - L) ==>
1.302 +          \<forall>n. \<bar>X n + - x\<bar> < inverse (real(Suc n))"
1.303 +by auto
1.304 +
1.305 +
1.306 +(*-------------------
1.307 +    NSLIM => LIM
1.308 + -------------------*)
1.309 +
1.310 +lemma NSLIM_LIM: "f -- x --NS> L ==> f -- x --> L"
1.311 +apply (simp add: LIM_def NSLIM_def approx_def)
1.312 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, clarify)
1.313 +apply (rule ccontr, simp)
1.315 +apply (drule lemma_skolemize_LIM2, safe)
1.316 +apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
1.318 +apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
1.320 +apply (drule spec, drule mp, assumption)
1.321 +apply (drule FreeUltrafilterNat_all, ultra)
1.322 +done
1.323 +
1.324 +
1.325 +(**** Key result ****)
1.326 +lemma LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
1.327 +by (blast intro: LIM_NSLIM NSLIM_LIM)
1.328 +
1.329 +(*-------------------------------------------------------------------*)
1.330 +(*   Proving properties of limits using nonstandard definition and   *)
1.331 +(*   hence, the properties hold for standard limits as well          *)
1.332 +(*-------------------------------------------------------------------*)
1.333 +(*------------------------------------------------
1.334 +      NSLIM_mult and hence (trivially) LIM_mult
1.335 + ------------------------------------------------*)
1.336 +
1.337 +lemma NSLIM_mult:
1.338 +     "[| f -- x --NS> l; g -- x --NS> m |]
1.339 +      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
1.341 +apply (auto intro!: approx_mult_HFinite)
1.342 +done
1.343 +
1.344 +lemma LIM_mult2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) * g(x)) -- x --> (l * m)"
1.345 +by (simp add: LIM_NSLIM_iff NSLIM_mult)
1.346 +
1.347 +(*----------------------------------------------
1.349 +      Note the much shorter proof
1.350 + ----------------------------------------------*)
1.352 +     "[| f -- x --NS> l; g -- x --NS> m |]
1.353 +      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
1.356 +done
1.357 +
1.358 +lemma LIM_add2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
1.360 +
1.361 +
1.362 +lemma NSLIM_const: "(%x. k) -- x --NS> k"
1.364 +
1.365 +declare NSLIM_const [simp]
1.366 +
1.367 +lemma LIM_const2: "(%x. k) -- x --> k"
1.369 +
1.370 +
1.371 +lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
1.373 +
1.374 +lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
1.375 +by (simp add: LIM_NSLIM_iff NSLIM_minus)
1.376 +
1.377 +
1.378 +lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
1.379 +by (blast dest: NSLIM_add NSLIM_minus)
1.380 +
1.381 +lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
1.383 +
1.384 +
1.385 +lemma NSLIM_inverse:
1.386 +     "[| f -- a --NS> L;  L \<noteq> 0 |]
1.387 +      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
1.388 +apply (simp add: NSLIM_def, clarify)
1.389 +apply (drule spec)
1.390 +apply (auto simp add: hypreal_of_real_approx_inverse)
1.391 +done
1.392 +
1.393 +lemma LIM_inverse: "[| f -- a --> L; L \<noteq> 0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)"
1.394 +by (simp add: LIM_NSLIM_iff NSLIM_inverse)
1.395 +
1.396 +
1.397 +lemma NSLIM_zero:
1.398 +  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
1.399 +proof -;
1.400 +  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
1.401 +    by (rule NSLIM_add_minus [OF f NSLIM_const])
1.402 +  thus ?thesis by simp
1.403 +qed
1.404 +
1.405 +lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"
1.406 +by (simp add: LIM_NSLIM_iff NSLIM_zero)
1.407 +
1.408 +lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
1.409 +apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
1.411 +done
1.412 +
1.413 +lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l"
1.414 +apply (drule_tac g = "%x. l" and M = l in LIM_add)
1.416 +done
1.417 +
1.418 +
1.419 +
1.420 +lemma NSLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)"
1.422 +apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
1.423 +apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
1.425 +done
1.426 +
1.427 +lemma NSLIM_const_not_eq: "k \<noteq> L ==> ~ ((%x. k) -- x --NS> L)"
1.429 +apply (rule_tac x = "hypreal_of_real x + epsilon" in exI)
1.430 +apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
1.432 +done
1.433 +
1.434 +lemma NSLIM_const_eq: "(%x. k) -- x --NS> L ==> k = L"
1.435 +apply (rule ccontr)
1.436 +apply (blast dest: NSLIM_const_not_eq)
1.437 +done
1.438 +
1.439 +(* can actually be proved more easily by unfolding def! *)
1.440 +lemma NSLIM_unique: "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M"
1.441 +apply (drule NSLIM_minus)
1.443 +apply (auto dest!: NSLIM_const_eq [symmetric])
1.444 +done
1.445 +
1.446 +lemma LIM_unique2: "[| f -- x --> L; f -- x --> M |] ==> L = M"
1.447 +by (simp add: LIM_NSLIM_iff NSLIM_unique)
1.448 +
1.449 +
1.450 +lemma NSLIM_mult_zero: "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
1.451 +by (drule NSLIM_mult, auto)
1.452 +
1.453 +(* we can use the corresponding thm LIM_mult2 *)
1.454 +(* for standard definition of limit           *)
1.455 +
1.456 +lemma LIM_mult_zero2: "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0"
1.457 +by (drule LIM_mult2, auto)
1.458 +
1.459 +
1.460 +lemma NSLIM_self: "(%x. x) -- a --NS> a"
1.462 +
1.463 +
1.464 +(*-----------------------------------------------------------------------------
1.465 +   Derivatives and Continuity - NS and Standard properties
1.466 + -----------------------------------------------------------------------------*)
1.467 +text{*Continuity*}
1.468 +
1.469 +lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
1.471 +
1.472 +lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
1.473 +by (simp add: isNSCont_def NSLIM_def)
1.474 +
1.475 +lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
1.476 +apply (simp add: isNSCont_def NSLIM_def, auto)
1.477 +apply (rule_tac Q = "y = hypreal_of_real a" in excluded_middle [THEN disjE], auto)
1.478 +done
1.479 +
1.480 +(*-----------------------------------------------------
1.481 +    NS continuity can be defined using NS Limit in
1.482 +    similar fashion to standard def of continuity
1.483 + -----------------------------------------------------*)
1.484 +lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
1.485 +by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
1.486 +
1.487 +(*----------------------------------------------
1.488 +  Hence, NS continuity can be given
1.489 +  in terms of standard limit
1.490 + ---------------------------------------------*)
1.491 +lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
1.492 +by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
1.493 +
1.494 +(*-----------------------------------------------
1.495 +  Moreover, it's trivial now that NS continuity
1.496 +  is equivalent to standard continuity
1.497 + -----------------------------------------------*)
1.498 +lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
1.500 +apply (rule isNSCont_LIM_iff)
1.501 +done
1.502 +
1.503 +(*----------------------------------------
1.504 +  Standard continuity ==> NS continuity
1.505 + ----------------------------------------*)
1.506 +lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
1.507 +by (erule isNSCont_isCont_iff [THEN iffD2])
1.508 +
1.509 +(*----------------------------------------
1.510 +  NS continuity ==> Standard continuity
1.511 + ----------------------------------------*)
1.512 +lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
1.513 +by (erule isNSCont_isCont_iff [THEN iffD1])
1.514 +
1.515 +text{*Alternative definition of continuity*}
1.516 +(* Prove equivalence between NS limits - *)
1.517 +(* seems easier than using standard def  *)
1.518 +lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
1.519 +apply (simp add: NSLIM_def, auto)
1.520 +apply (drule_tac x = "hypreal_of_real a + x" in spec)
1.521 +apply (drule_tac [2] x = "-hypreal_of_real a + x" in spec, safe, simp)
1.522 +apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
1.523 +apply (rule_tac [4] approx_minus_iff2 [THEN iffD1])
1.525 +apply (rule_tac [2] z = x in eq_Abs_hypreal)
1.526 +apply (rule_tac [4] z = x in eq_Abs_hypreal)
1.528 +done
1.529 +
1.530 +lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
1.531 +by (rule NSLIM_h_iff)
1.532 +
1.533 +lemma LIM_isCont_iff: "(f -- a --> f a) = ((%h. f(a + h)) -- 0 --> f(a))"
1.534 +by (simp add: LIM_NSLIM_iff NSLIM_isCont_iff)
1.535 +
1.536 +lemma isCont_iff: "(isCont f x) = ((%h. f(x + h)) -- 0 --> f(x))"
1.537 +by (simp add: isCont_def LIM_isCont_iff)
1.538 +
1.539 +(*--------------------------------------------------------------------------
1.540 +   Immediate application of nonstandard criterion for continuity can offer
1.541 +   very simple proofs of some standard property of continuous functions
1.542 + --------------------------------------------------------------------------*)
1.543 +text{*sum continuous*}
1.544 +lemma isCont_add: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a"
1.546 +
1.547 +text{*mult continuous*}
1.548 +lemma isCont_mult: "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
1.549 +by (auto intro!: starfun_mult_HFinite_approx
1.550 +            simp del: starfun_mult [symmetric]
1.551 +            simp add: isNSCont_isCont_iff [symmetric] isNSCont_def)
1.552 +
1.553 +(*-------------------------------------------
1.554 +     composition of continuous functions
1.555 +     Note very short straightforard proof!
1.556 + ------------------------------------------*)
1.557 +lemma isCont_o: "[| isCont f a; isCont g (f a) |] ==> isCont (g o f) a"
1.558 +by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_def starfun_o [symmetric])
1.559 +
1.560 +lemma isCont_o2: "[| isCont f a; isCont g (f a) |] ==> isCont (%x. g (f x)) a"
1.561 +by (auto dest: isCont_o simp add: o_def)
1.562 +
1.563 +lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
1.565 +
1.566 +lemma isCont_minus: "isCont f a ==> isCont (%x. - f x) a"
1.567 +by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus)
1.568 +
1.569 +lemma isCont_inverse:
1.570 +      "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
1.572 +apply (blast intro: LIM_inverse)
1.573 +done
1.574 +
1.575 +lemma isNSCont_inverse: "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
1.576 +by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
1.577 +
1.578 +lemma isCont_diff:
1.579 +      "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a"
1.581 +apply (auto intro: isCont_add isCont_minus)
1.582 +done
1.583 +
1.584 +lemma isCont_const: "isCont (%x. k) a"
1.586 +declare isCont_const [simp]
1.587 +
1.588 +lemma isNSCont_const: "isNSCont (%x. k) a"
1.590 +declare isNSCont_const [simp]
1.591 +
1.592 +lemma isNSCont_rabs: "isNSCont abs a"
1.594 +apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs)
1.595 +done
1.596 +declare isNSCont_rabs [simp]
1.597 +
1.598 +lemma isCont_rabs: "isCont abs a"
1.599 +by (auto simp add: isNSCont_isCont_iff [symmetric])
1.600 +declare isCont_rabs [simp]
1.601 +
1.602 +(****************************************************************
1.603 +(%* Leave as commented until I add topology theory or remove? *%)
1.604 +(%*------------------------------------------------------------
1.605 +  Elementary topology proof for a characterisation of
1.606 +  continuity now: a function f is continuous if and only
1.607 +  if the inverse image, {x. f(x) \<in> A}, of any open set A
1.608 +  is always an open set
1.609 + ------------------------------------------------------------*%)
1.610 +Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
1.611 +               ==> isNSopen {x. f x \<in> A}"
1.612 +by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
1.613 +by (dtac (mem_monad_approx RS approx_sym);
1.614 +by (dres_inst_tac [("x","a")] spec 1);
1.615 +by (dtac isNSContD 1 THEN assume_tac 1)
1.616 +by (dtac bspec 1 THEN assume_tac 1)
1.617 +by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
1.618 +by (blast_tac (claset() addIs [starfun_mem_starset]);
1.619 +qed "isNSCont_isNSopen";
1.620 +
1.621 +Goalw [isNSCont_def]
1.622 +          "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \
1.623 +\              ==> isNSCont f x";
1.624 +by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
1.625 +     (approx_minus_iff RS iffD2)],simpset() addsimps
1.626 +      [Infinitesimal_def,SReal_iff]));
1.627 +by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
1.628 +by (etac (isNSopen_open_interval RSN (2,impE));
1.629 +by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
1.630 +by (dres_inst_tac [("x","x")] spec 1);
1.633 +qed "isNSopen_isNSCont";
1.634 +
1.635 +Goal "(\<forall>x. isNSCont f x) = \
1.636 +\     (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
1.637 +by (blast_tac (claset() addIs [isNSCont_isNSopen,
1.638 +    isNSopen_isNSCont]);
1.639 +qed "isNSCont_isNSopen_iff";
1.640 +
1.641 +(%*------- Standard version of same theorem --------*%)
1.642 +Goal "(\<forall>x. isCont f x) = \
1.643 +\         (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})";
1.644 +by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
1.645 +              simpset() addsimps [isNSopen_isopen_iff RS sym,
1.646 +              isNSCont_isCont_iff RS sym]));
1.647 +qed "isCont_isopen_iff";
1.648 +*******************************************************************)
1.649 +
1.650 +text{*Uniform continuity*}
1.651 +lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
1.653 +
1.654 +lemma isUCont_isCont: "isUCont f ==> isCont f x"
1.655 +by (simp add: isUCont_def isCont_def LIM_def, meson)
1.656 +
1.657 +lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
1.658 +apply (simp add: isNSUCont_def isUCont_def approx_def)
1.659 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
1.660 +apply (rule_tac z = x in eq_Abs_hypreal)
1.661 +apply (rule_tac z = y in eq_Abs_hypreal)
1.663 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
1.664 +apply (drule_tac x = u in spec, clarify)
1.665 +apply (drule_tac x = s in spec, clarify)
1.666 +apply (subgoal_tac "\<forall>n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u")
1.667 +prefer 2 apply blast
1.668 +apply (erule_tac V = "\<forall>x y. \<bar>x + - y\<bar> < s --> \<bar>f x + - f y\<bar> < u" in thin_rl)
1.669 +apply (drule FreeUltrafilterNat_all, ultra)
1.670 +done
1.671 +
1.672 +lemma lemma_LIMu: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>)
1.673 +      ==> \<forall>n::nat. \<exists>z y.
1.674 +               \<bar>z + -y\<bar> < inverse(real(Suc n)) &
1.675 +               r \<le> \<bar>f z + -f y\<bar>"
1.676 +apply clarify
1.677 +apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
1.678 +done
1.679 +
1.680 +lemma lemma_skolemize_LIM2u: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>)
1.681 +      ==> \<exists>X Y. \<forall>n::nat.
1.682 +               abs(X n + -(Y n)) < inverse(real(Suc n)) &
1.683 +               r \<le> abs(f (X n) + -f (Y n))"
1.684 +apply (drule lemma_LIMu)
1.685 +apply (drule choice, safe)
1.686 +apply (drule choice, blast)
1.687 +done
1.688 +
1.689 +lemma lemma_simpu: "\<forall>n. \<bar>X n + -Y n\<bar> < inverse (real(Suc n)) &
1.690 +          r \<le> abs (f (X n) + - f(Y n)) ==>
1.691 +          \<forall>n. \<bar>X n + - Y n\<bar> < inverse (real(Suc n))"
1.692 +apply auto
1.693 +done
1.694 +
1.695 +lemma isNSUCont_isUCont:
1.696 +     "isNSUCont f ==> isUCont f"
1.697 +apply (simp add: isNSUCont_def isUCont_def approx_def)
1.698 +apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
1.699 +apply (rule ccontr, simp)
1.701 +apply (drule lemma_skolemize_LIM2u, safe)
1.702 +apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
1.703 +apply (drule_tac x = "Abs_hypreal (hyprel``{Y}) " in spec)
1.705 +apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
1.707 +apply (rotate_tac 2)
1.708 +apply (drule_tac x = r in spec, clarify)
1.709 +apply (drule FreeUltrafilterNat_all, ultra)
1.710 +done
1.711 +
1.712 +text{*Derivatives*}
1.713 +lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)"
1.715 +
1.716 +lemma DERIV_NS_iff:
1.717 +      "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"
1.718 +by (simp add: deriv_def LIM_NSLIM_iff)
1.719 +
1.720 +lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D"
1.722 +
1.723 +lemma NS_DERIV_D: "DERIV f x :> D ==>
1.724 +           (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D"
1.725 +by (simp add: deriv_def LIM_NSLIM_iff)
1.726 +
1.727 +subsubsection{*Uniqueness*}
1.728 +
1.729 +lemma DERIV_unique:
1.730 +      "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"
1.732 +apply (blast intro: LIM_unique)
1.733 +done
1.734 +
1.735 +lemma NSDeriv_unique:
1.736 +     "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"
1.738 +apply (cut_tac Infinitesimal_epsilon hypreal_epsilon_not_zero)
1.739 +apply (auto dest!: bspec [where x=epsilon]
1.740 +            intro!: inj_hypreal_of_real [THEN injD]
1.741 +            dest: approx_trans3)
1.742 +done
1.743 +
1.744 +subsubsection{*Differentiable*}
1.745 +
1.746 +lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
1.748 +
1.749 +lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
1.750 +by (force simp add: differentiable_def)
1.751 +
1.752 +lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
1.754 +
1.755 +lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
1.756 +by (force simp add: NSdifferentiable_def)
1.757 +
1.758 +subsubsection{*Alternative definition for differentiability*}
1.759 +
1.760 +lemma LIM_I:
1.761 +     "(!!r. 0<r ==> (\<exists>s. 0 < s & (\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>f x - L\<bar> < r)))
1.762 +      ==> f -- a --> L"
1.764 +
1.765 +lemma DERIV_LIM_iff:
1.766 +     "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
1.767 +      ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
1.768 +proof (intro iffI LIM_I)
1.769 +  fix r::real
1.770 +  assume r: "0<r"
1.771 +  assume "(\<lambda>h. (f (a + h) - f a) / h) -- 0 --> D"
1.772 +  from LIM_D [OF this r]
1.773 +  obtain s
1.774 +    where s:    "0 < s"
1.775 +      and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r"
1.776 +  by auto
1.777 +  show "\<exists>s. 0 < s \<and>
1.778 +            (\<forall>x. x \<noteq> a \<and> \<bar>x-a\<bar> < s \<longrightarrow> \<bar>(f x - f a) / (x-a) - D\<bar> < r)"
1.779 +  proof (intro exI conjI strip)
1.780 +    show "0 < s"  by (rule s)
1.781 +  next
1.782 +    fix x::real
1.783 +    assume "x \<noteq> a \<and> \<bar>x-a\<bar> < s"
1.784 +    with s_lt [THEN spec [where x="x-a"]]
1.785 +    show "\<bar>(f x - f a) / (x-a) - D\<bar> < r" by auto
1.786 +  qed
1.787 +next
1.788 +  fix r::real
1.789 +  assume r: "0<r"
1.790 +  assume "(\<lambda>x. (f x - f a) / (x-a)) -- a --> D"
1.791 +  from LIM_D [OF this r]
1.792 +  obtain s
1.793 +    where s:    "0 < s"
1.794 +      and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r"
1.795 +  by auto
1.796 +  show "\<exists>s. 0 < s \<and>
1.797 +            (\<forall>x. x \<noteq> 0 & \<bar>x - 0\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r)"
1.798 +  proof (intro exI conjI strip)
1.799 +    show "0 < s"  by (rule s)
1.800 +  next
1.801 +    fix x::real
1.802 +    assume "x \<noteq> 0 \<and> \<bar>x - 0\<bar> < s"
1.803 +    with s_lt [THEN spec [where x="x+a"]]
1.804 +    show "\<bar>(f (a + x) - f a) / x - D\<bar> < r" by (auto simp add: add_ac)
1.805 +  qed
1.806 +qed
1.807 +
1.808 +lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)"
1.809 +by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
1.810 +
1.811 +
1.812 +subsection{*Equivalence of NS and standard definitions of differentiation*}
1.813 +
1.814 +text{*First NSDERIV in terms of NSLIM*}
1.815 +
1.816 +(*--- first equivalence ---*)
1.817 +lemma NSDERIV_NSLIM_iff:
1.818 +      "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)"
1.819 +apply (simp add: nsderiv_def NSLIM_def, auto)
1.820 +apply (drule_tac x = xa in bspec)
1.821 +apply (rule_tac [3] ccontr)
1.822 +apply (drule_tac [3] x = h in spec)
1.823 +apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
1.824 +done
1.825 +
1.826 +(*--- second equivalence ---*)
1.827 +lemma NSDERIV_NSLIM_iff2:
1.828 +     "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
1.829 +by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff  diff_minus [symmetric]
1.830 +              LIM_NSLIM_iff [symmetric])
1.831 +
1.832 +(* while we're at it! *)
1.833 +lemma NSDERIV_iff2:
1.834 +     "(NSDERIV f x :> D) =
1.835 +      (\<forall>w.
1.836 +        w \<noteq> hypreal_of_real x & w \<approx> hypreal_of_real x -->
1.837 +        ( *f* (%z. (f z - f x) / (z-x))) w \<approx> hypreal_of_real D)"
1.838 +by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
1.839 +
1.840 +(*FIXME DELETE*)
1.841 +lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))"
1.842 +by (auto dest: hypreal_eq_minus_iff [THEN iffD2])
1.843 +
1.844 +lemma NSDERIVD5:
1.845 +  "(NSDERIV f x :> D) ==>
1.846 +   (\<forall>u. u \<approx> hypreal_of_real x -->
1.847 +     ( *f* (%z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x))"
1.848 +apply (auto simp add: NSDERIV_iff2)
1.849 +apply (case_tac "u = hypreal_of_real x", auto)
1.850 +apply (drule_tac x = u in spec, auto)
1.851 +apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
1.852 +apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
1.853 +apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
1.854 +apply (auto simp add: diff_minus
1.855 +	       approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
1.856 +		     Infinitesimal_subset_HFinite [THEN subsetD])
1.857 +done
1.858 +
1.859 +lemma NSDERIVD4:
1.860 +     "(NSDERIV f x :> D) ==>
1.861 +      (\<forall>h \<in> Infinitesimal.
1.862 +               (( *f* f)(hypreal_of_real x + h) -
1.863 +                 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
1.864 +apply (auto simp add: nsderiv_def)
1.865 +apply (case_tac "h = (0::hypreal) ")
1.866 +apply (auto simp add: diff_minus)
1.867 +apply (drule_tac x = h in bspec)
1.868 +apply (drule_tac [2] c = h in approx_mult1)
1.869 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
1.871 +done
1.872 +
1.873 +lemma NSDERIVD3:
1.874 +     "(NSDERIV f x :> D) ==>
1.875 +      (\<forall>h \<in> Infinitesimal - {0}.
1.876 +               (( *f* f)(hypreal_of_real x + h) -
1.877 +                 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
1.878 +apply (auto simp add: nsderiv_def)
1.879 +apply (rule ccontr, drule_tac x = h in bspec)
1.880 +apply (drule_tac [2] c = h in approx_mult1)
1.881 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
1.882 +            simp add: mult_assoc diff_minus)
1.883 +done
1.884 +
1.885 +text{*Now equivalence between NSDERIV and DERIV*}
1.886 +lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
1.887 +by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
1.888 +
1.889 +(*---------------------------------------------------
1.890 +         Differentiability implies continuity
1.891 +         nice and simple "algebraic" proof
1.892 + --------------------------------------------------*)
1.893 +lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x"
1.894 +apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
1.895 +apply (drule approx_minus_iff [THEN iffD1])
1.896 +apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
1.897 +apply (drule_tac x = "-hypreal_of_real x + xa" in bspec)
1.900 +apply (drule_tac c = "xa + -hypreal_of_real x" in approx_mult1)
1.901 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
1.903 +apply (drule_tac x3=D in
1.904 +           HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
1.905 +             THEN mem_infmal_iff [THEN iffD1]])
1.906 +apply (auto simp add: mult_commute
1.907 +            intro: approx_trans approx_minus_iff [THEN iffD2])
1.908 +done
1.909 +
1.910 +text{*Now Sandard proof*}
1.911 +lemma DERIV_isCont: "DERIV f x :> D ==> isCont f x"
1.912 +by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric]
1.913 +              NSDERIV_isNSCont)
1.914 +
1.915 +
1.916 +(*----------------------------------------------------------------------------
1.917 +      Differentiation rules for combinations of functions
1.918 +      follow from clear, straightforard, algebraic
1.919 +      manipulations
1.920 + ----------------------------------------------------------------------------*)
1.921 +text{*Constant function*}
1.922 +
1.923 +(* use simple constant nslimit theorem *)
1.924 +lemma NSDERIV_const: "(NSDERIV (%x. k) x :> 0)"
1.926 +declare NSDERIV_const [simp]
1.927 +
1.928 +lemma DERIV_const: "(DERIV (%x. k) x :> 0)"
1.929 +by (simp add: NSDERIV_DERIV_iff [symmetric])
1.930 +declare DERIV_const [simp]
1.931 +
1.932 +(*-----------------------------------------------------
1.933 +    Sum of functions- proved easily
1.934 + ----------------------------------------------------*)
1.935 +
1.936 +
1.937 +lemma NSDERIV_add: "[| NSDERIV f x :> Da;  NSDERIV g x :> Db |]
1.938 +      ==> NSDERIV (%x. f x + g x) x :> Da + Db"
1.939 +apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
1.941 +apply (drule_tac b = "hypreal_of_real Da" and d = "hypreal_of_real Db" in approx_add)
1.943 +done
1.944 +
1.945 +(* Standard theorem *)
1.946 +lemma DERIV_add: "[| DERIV f x :> Da; DERIV g x :> Db |]
1.947 +      ==> DERIV (%x. f x + g x) x :> Da + Db"
1.949 +done
1.950 +
1.951 +(*-----------------------------------------------------
1.952 +  Product of functions - Proof is trivial but tedious
1.953 +  and long due to rearrangement of terms
1.954 + ----------------------------------------------------*)
1.955 +
1.956 +lemma lemma_nsderiv1: "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))"
1.958 +
1.959 +lemma lemma_nsderiv2: "[| (x + y) / z = hypreal_of_real D + yb; z \<noteq> 0;
1.960 +         z \<in> Infinitesimal; yb \<in> Infinitesimal |]
1.961 +      ==> x + y \<approx> 0"
1.962 +apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption)
1.963 +apply (erule_tac V = " (x + y) / z = hypreal_of_real D + yb" in thin_rl)
1.964 +apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
1.965 +            simp add: hypreal_mult_assoc mem_infmal_iff [symmetric])
1.966 +apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
1.967 +done
1.968 +
1.969 +
1.970 +lemma NSDERIV_mult: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
1.971 +      ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
1.972 +apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
1.973 +apply (auto dest!: spec
1.974 +	    simp add: starfun_lambda_cancel lemma_nsderiv1)
1.976 +apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
1.977 +apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
1.978 +apply (drule_tac D = Db in lemma_nsderiv2)
1.979 +apply (drule_tac [4]
1.980 +     approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
1.983 +apply (rule_tac b1 = "hypreal_of_real Db * hypreal_of_real (f x)"
1.984 +         in add_commute [THEN subst])
1.985 +apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
1.987 +                    Infinitesimal_hypreal_of_real_mult
1.988 +                    Infinitesimal_hypreal_of_real_mult2
1.990 +done
1.991 +
1.992 +lemma DERIV_mult:
1.993 +     "[| DERIV f x :> Da; DERIV g x :> Db |]
1.994 +      ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
1.995 +by (simp add: NSDERIV_mult NSDERIV_DERIV_iff [symmetric])
1.996 +
1.997 +text{*Multiplying by a constant*}
1.998 +lemma NSDERIV_cmult: "NSDERIV f x :> D
1.999 +      ==> NSDERIV (%x. c * f x) x :> c*D"
1.1000 +apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
1.1001 +                  minus_mult_right right_distrib [symmetric])
1.1002 +apply (erule NSLIM_const [THEN NSLIM_mult])
1.1003 +done
1.1004 +
1.1005 +(* let's do the standard proof though theorem *)
1.1006 +(* LIM_mult2 follows from a NS proof          *)
1.1007 +
1.1008 +lemma DERIV_cmult:
1.1009 +      "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
1.1010 +apply (simp only: deriv_def times_divide_eq_right [symmetric]
1.1011 +                  NSDERIV_NSLIM_iff minus_mult_right right_distrib [symmetric])
1.1012 +apply (erule LIM_const [THEN LIM_mult2])
1.1013 +done
1.1014 +
1.1015 +text{*Negation of function*}
1.1016 +lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
1.1018 +  assume "(\<lambda>h. (f (x + h) + - f x) / h) -- 0 --NS> D"
1.1019 +  hence deriv: "(\<lambda>h. - ((f(x+h) + - f x) / h)) -- 0 --NS> - D"
1.1020 +    by (rule NSLIM_minus)
1.1021 +  have "\<forall>h. - ((f (x + h) + - f x) / h) = (- f (x + h) + f x) / h"
1.1022 +    by (simp add: minus_divide_left)
1.1023 +  with deriv
1.1024 +  show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
1.1025 +qed
1.1026 +
1.1027 +
1.1028 +lemma DERIV_minus: "DERIV f x :> D ==> DERIV (%x. -(f x)) x :> -D"
1.1029 +by (simp add: NSDERIV_minus NSDERIV_DERIV_iff [symmetric])
1.1030 +
1.1031 +text{*Subtraction*}
1.1032 +lemma NSDERIV_add_minus: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + -g x) x :> Da + -Db"
1.1033 +by (blast dest: NSDERIV_add NSDERIV_minus)
1.1034 +
1.1035 +lemma DERIV_add_minus: "[| DERIV f x :> Da; DERIV g x :> Db |] ==> DERIV (%x. f x + -g x) x :> Da + -Db"
1.1036 +by (blast dest: DERIV_add DERIV_minus)
1.1037 +
1.1038 +lemma NSDERIV_diff:
1.1039 +     "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
1.1040 +      ==> NSDERIV (%x. f x - g x) x :> Da-Db"
1.1043 +done
1.1044 +
1.1045 +lemma DERIV_diff:
1.1046 +     "[| DERIV f x :> Da; DERIV g x :> Db |]
1.1047 +       ==> DERIV (%x. f x - g x) x :> Da-Db"
1.1050 +done
1.1051 +
1.1052 +(*---------------------------------------------------------------
1.1053 +                     (NS) Increment
1.1054 + ---------------------------------------------------------------*)
1.1055 +lemma incrementI:
1.1056 +      "f NSdifferentiable x ==>
1.1057 +      increment f x h = ( *f* f) (hypreal_of_real(x) + h) +
1.1058 +      -hypreal_of_real (f x)"
1.1060 +
1.1061 +lemma incrementI2: "NSDERIV f x :> D ==>
1.1062 +     increment f x h = ( *f* f) (hypreal_of_real(x) + h) +
1.1063 +     -hypreal_of_real (f x)"
1.1064 +apply (erule NSdifferentiableI [THEN incrementI])
1.1065 +done
1.1066 +
1.1067 +(* The Increment theorem -- Keisler p. 65 *)
1.1068 +lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
1.1069 +      ==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h"
1.1070 +apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
1.1071 +apply (drule bspec, auto)
1.1072 +apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
1.1073 +apply (frule_tac b1 = "hypreal_of_real (D) + y"
1.1074 +        in hypreal_mult_right_cancel [THEN iffD2])
1.1075 +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)
1.1076 +apply assumption
1.1077 +apply (simp add: times_divide_eq_right [symmetric] del: times_divide_eq_right)
1.1078 +apply (auto simp add: left_distrib)
1.1079 +done
1.1080 +
1.1081 +lemma increment_thm2:
1.1082 +     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
1.1083 +      ==> \<exists>e \<in> Infinitesimal. increment f x h =
1.1084 +              hypreal_of_real(D)*h + e*h"
1.1085 +by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)
1.1086 +
1.1087 +
1.1088 +lemma increment_approx_zero: "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
1.1089 +      ==> increment f x h \<approx> 0"
1.1090 +apply (drule increment_thm2,
1.1091 +       auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric])
1.1092 +apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
1.1093 +done
1.1094 +
1.1095 +text{*  Similarly to the above, the chain rule admits an entirely
1.1096 +   straightforward derivation. Compare this with Harrison's
1.1097 +   HOL proof of the chain rule, which proved to be trickier and
1.1098 +   required an alternative characterisation of differentiability-
1.1099 +   the so-called Carathedory derivative. Our main problem is
1.1100 +   manipulation of terms.*}
1.1101 +
1.1102 +
1.1103 +(* lemmas *)
1.1104 +lemma NSDERIV_zero:
1.1105 +      "[| NSDERIV g x :> D;
1.1106 +               ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);
1.1107 +               xa \<in> Infinitesimal;
1.1108 +               xa \<noteq> 0
1.1109 +            |] ==> D = 0"
1.1111 +apply (drule bspec, auto)
1.1112 +done
1.1113 +
1.1114 +(* can be proved differently using NSLIM_isCont_iff *)
1.1115 +lemma NSDERIV_approx:
1.1116 +     "[| NSDERIV f x :> D;  h \<in> Infinitesimal;  h \<noteq> 0 |]
1.1117 +      ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \<approx> 0"
1.1119 +apply (simp add: mem_infmal_iff [symmetric])
1.1120 +apply (rule Infinitesimal_ratio)
1.1121 +apply (rule_tac [3] approx_hypreal_of_real_HFinite, auto)
1.1122 +done
1.1123 +
1.1124 +(*---------------------------------------------------------------
1.1125 +   from one version of differentiability
1.1126 +
1.1127 +                f(x) - f(a)
1.1128 +              --------------- \<approx> Db
1.1129 +                  x - a
1.1130 + ---------------------------------------------------------------*)
1.1131 +lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
1.1132 +         ( *f* g) (hypreal_of_real(x) + xa) \<noteq> hypreal_of_real (g x);
1.1133 +         ( *f* g) (hypreal_of_real(x) + xa) \<approx> hypreal_of_real (g x)
1.1134 +      |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa))
1.1135 +                   + - hypreal_of_real (f (g x)))
1.1136 +              / (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x))
1.1137 +             \<approx> hypreal_of_real(Da)"
1.1138 +by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric])
1.1139 +
1.1140 +(*--------------------------------------------------------------
1.1141 +   from other version of differentiability
1.1142 +
1.1143 +                f(x + h) - f(x)
1.1144 +               ----------------- \<approx> Db
1.1145 +                       h
1.1146 + --------------------------------------------------------------*)
1.1147 +lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 |]
1.1148 +      ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa
1.1149 +          \<approx> hypreal_of_real(Db)"
1.1150 +by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)
1.1151 +
1.1152 +lemma lemma_chain: "(z::hypreal) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
1.1153 +by auto
1.1154 +
1.1155 +(*------------------------------------------------------
1.1156 +  This proof uses both definitions of differentiability.
1.1157 + ------------------------------------------------------*)
1.1158 +lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |]
1.1159 +      ==> NSDERIV (f o g) x :> Da * Db"
1.1160 +apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def
1.1161 +                mem_infmal_iff [symmetric])
1.1162 +apply clarify
1.1163 +apply (frule_tac f = g in NSDERIV_approx)
1.1164 +apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
1.1165 +apply (case_tac "( *f* g) (hypreal_of_real (x) + xa) = hypreal_of_real (g x) ")
1.1166 +apply (drule_tac g = g in NSDERIV_zero)
1.1167 +apply (auto simp add: divide_inverse)
1.1168 +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])
1.1169 +apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
1.1170 +apply (rule approx_mult_hypreal_of_real)
1.1171 +apply (simp_all add: divide_inverse [symmetric])
1.1172 +apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
1.1173 +apply (blast intro: NSDERIVD2)
1.1174 +done
1.1175 +
1.1176 +(* standard version *)
1.1177 +lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
1.1178 +by (simp add: NSDERIV_DERIV_iff [symmetric] NSDERIV_chain)
1.1179 +
1.1180 +lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
1.1181 +by (auto dest: DERIV_chain simp add: o_def)
1.1182 +
1.1183 +text{*Differentiation of natural number powers*}
1.1184 +lemma NSDERIV_Id: "NSDERIV (%x. x) x :> 1"
1.1185 +by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def starfun_Id)
1.1186 +declare NSDERIV_Id [simp]
1.1187 +
1.1188 +(*derivative of the identity function*)
1.1189 +lemma DERIV_Id: "DERIV (%x. x) x :> 1"
1.1190 +by (simp add: NSDERIV_DERIV_iff [symmetric])
1.1191 +declare DERIV_Id [simp]
1.1192 +
1.1193 +lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard]
1.1194 +
1.1195 +(*derivative of linear multiplication*)
1.1196 +lemma DERIV_cmult_Id: "DERIV (op * c) x :> c"
1.1197 +by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp)
1.1198 +declare DERIV_cmult_Id [simp]
1.1199 +
1.1200 +lemma NSDERIV_cmult_Id: "NSDERIV (op * c) x :> c"
1.1202 +declare NSDERIV_cmult_Id [simp]
1.1203 +
1.1204 +lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
1.1205 +apply (induct_tac "n")
1.1206 +apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
1.1207 +apply (auto simp add: real_of_nat_Suc left_distrib)
1.1208 +apply (case_tac "0 < n")
1.1209 +apply (drule_tac x = x in realpow_minus_mult)
1.1211 +done
1.1212 +
1.1213 +(* NS version *)
1.1214 +lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
1.1215 +by (simp add: NSDERIV_DERIV_iff DERIV_pow)
1.1216 +
1.1217 +(*---------------------------------------------------------------
1.1218 +                    Power of -1
1.1219 + ---------------------------------------------------------------*)
1.1220 +
1.1221 +(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
1.1222 +lemma NSDERIV_inverse:
1.1223 +     "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"
1.1225 +apply (rule ballI, simp, clarify)
1.1228 +apply (auto simp add: starfun_inverse_inverse realpow_two
1.1229 +        simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])
1.1231 +              inverse_minus_eq [symmetric] add_ac mult_ac
1.1232 +            del: inverse_mult_distrib inverse_minus_eq
1.1233 +                 minus_mult_left [symmetric] minus_mult_right [symmetric])
1.1234 +apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
1.1235 +            del: minus_mult_left [symmetric] minus_mult_right [symmetric])
1.1236 +apply (rule_tac y = " inverse (- hypreal_of_real x * hypreal_of_real x) " in approx_trans)
1.1238 +apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
1.1239 +            simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
1.1240 +apply (rule Infinitesimal_HFinite_mult2, auto)
1.1241 +done
1.1242 +
1.1243 +
1.1244 +
1.1245 +
1.1246 +lemma DERIV_inverse: "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
1.1247 +by (simp add: NSDERIV_inverse NSDERIV_DERIV_iff [symmetric] del: realpow_Suc)
1.1248 +
1.1249 +text{*Derivative of inverse*}
1.1250 +lemma DERIV_inverse_fun: "[| DERIV f x :> d; f(x) \<noteq> 0 |]
1.1251 +      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
1.1252 +apply (simp only: mult_commute [of d] minus_mult_left power_inverse)
1.1253 +apply (fold o_def)
1.1254 +apply (blast intro!: DERIV_chain DERIV_inverse)
1.1255 +done
1.1256 +
1.1257 +lemma NSDERIV_inverse_fun: "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
1.1258 +      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
1.1259 +by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: realpow_Suc)
1.1260 +
1.1261 +text{*Derivative of quotient*}
1.1262 +lemma DERIV_quotient: "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
1.1263 +       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"
1.1264 +apply (drule_tac f = g in DERIV_inverse_fun)
1.1265 +apply (drule_tac [2] DERIV_mult)
1.1266 +apply (assumption+)
1.1267 +apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
1.1268 +                 mult_ac
1.1269 +     del: realpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
1.1270 +done
1.1271 +
1.1272 +lemma NSDERIV_quotient: "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
1.1273 +       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
1.1274 +                            + -(e*f(x))) / (g(x) ^ Suc (Suc 0))"
1.1275 +by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
1.1276 +
1.1277 +(* ------------------------------------------------------------------------ *)
1.1278 +(* Caratheodory formulation of derivative at a point: standard proof        *)
1.1279 +(* ------------------------------------------------------------------------ *)
1.1280 +
1.1281 +lemma CARAT_DERIV:
1.1282 +     "(DERIV f x :> l) =
1.1283 +      (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
1.1284 +      (is "?lhs = ?rhs")
1.1285 +proof
1.1286 +  assume der: "DERIV f x :> l"
1.1287 +  show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
1.1288 +  proof (intro exI conjI)
1.1289 +    let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
1.1290 +    show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
1.1291 +    show "isCont ?g x" using der
1.1292 +      by (simp add: isCont_iff DERIV_iff diff_minus
1.1293 +               cong: LIM_equal [rule_format])
1.1294 +    show "?g x = l" by simp
1.1295 +  qed
1.1296 +next
1.1297 +  assume "?rhs"
1.1298 +  then obtain g where
1.1299 +    "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
1.1300 +  thus "(DERIV f x :> l)"
1.1301 +     by (auto simp add: isCont_iff DERIV_iff diff_minus
1.1302 +               cong: LIM_equal [rule_format])
1.1303 +qed
1.1304 +
1.1305 +
1.1306 +lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>
1.1307 +      \<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isNSCont g x & g x = l"
1.1308 +by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV)
1.1309 +
1.1310 +lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))"
1.1311 +by auto
1.1312 +
1.1313 +lemma CARAT_DERIVD:
1.1314 +  assumes all: "\<forall>z. f z - f x = g z * (z-x)"
1.1315 +      and nsc: "isNSCont g x"
1.1316 +  shows "NSDERIV f x :> g x"
1.1317 +proof -
1.1318 +  from nsc
1.1319 +  have "\<forall>w. w \<noteq> hypreal_of_real x \<and> w \<approx> hypreal_of_real x \<longrightarrow>
1.1320 +         ( *f* g) w * (w - hypreal_of_real x) / (w - hypreal_of_real x) \<approx>
1.1321 +         hypreal_of_real (g x)"
1.1322 +    by (simp add: diff_minus isNSCont_def)
1.1323 +  thus ?thesis using all
1.1324 +    by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
1.1325 +qed
1.1326 +
1.1327 +(*--------------------------------------------------------------------------*)
1.1328 +(* Lemmas about nested intervals and proof by bisection (cf.Harrison)       *)
1.1329 +(* All considerably tidied by lcp                                           *)
1.1330 +(*--------------------------------------------------------------------------*)
1.1331 +
1.1332 +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)"
1.1333 +apply (induct_tac "no")
1.1334 +apply (auto intro: order_trans)
1.1335 +done
1.1336 +
1.1337 +lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
1.1338 +         \<forall>n. g(Suc n) \<le> g(n);
1.1339 +         \<forall>n. f(n) \<le> g(n) |]
1.1340 +      ==> Bseq f"
1.1341 +apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
1.1342 +apply (induct_tac "n")
1.1343 +apply (auto intro: order_trans)
1.1344 +apply (rule_tac y = "g (Suc na) " in order_trans)
1.1345 +apply (induct_tac [2] "na")
1.1346 +apply (auto intro: order_trans)
1.1347 +done
1.1348 +
1.1349 +lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
1.1350 +         \<forall>n. g(Suc n) \<le> g(n);
1.1351 +         \<forall>n. f(n) \<le> g(n) |]
1.1352 +      ==> Bseq g"
1.1353 +apply (subst Bseq_minus_iff [symmetric])
1.1354 +apply (rule_tac g = "%x. - (f x) " in f_inc_g_dec_Beq_f)
1.1355 +apply auto
1.1356 +done
1.1357 +
1.1358 +lemma f_inc_imp_le_lim: "[| \<forall>n. f n \<le> f (Suc n);  convergent f |] ==> f n \<le> lim f"
1.1359 +apply (rule linorder_not_less [THEN iffD1])
1.1360 +apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
1.1361 +apply (drule real_less_sum_gt_zero)
1.1362 +apply (drule_tac x = "f n + - lim f" in spec, safe)
1.1363 +apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
1.1364 +apply (subgoal_tac "lim f \<le> f (no + n) ")
1.1365 +apply (induct_tac [2] "no")
1.1366 +apply (auto intro: order_trans simp add: diff_minus real_abs_def)
1.1367 +apply (drule_tac no=no and m=n in lemma_f_mono_add)
1.1369 +done
1.1370 +
1.1371 +lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)"
1.1372 +apply (rule LIMSEQ_minus [THEN limI])
1.1374 +done
1.1375 +
1.1376 +lemma g_dec_imp_lim_le: "[| \<forall>n. g(Suc n) \<le> g(n);  convergent g |] ==> lim g \<le> g n"
1.1377 +apply (subgoal_tac "- (g n) \<le> - (lim g) ")
1.1378 +apply (cut_tac [2] f = "%x. - (g x) " in f_inc_imp_le_lim)
1.1379 +apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
1.1380 +done
1.1381 +
1.1382 +lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
1.1383 +         \<forall>n. g(Suc n) \<le> g(n);
1.1384 +         \<forall>n. f(n) \<le> g(n) |]
1.1385 +      ==> \<exists>l m. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
1.1386 +                            ((\<forall>n. m \<le> g(n)) & g ----> m)"
1.1387 +apply (subgoal_tac "monoseq f & monoseq g")
1.1388 +prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
1.1389 +apply (subgoal_tac "Bseq f & Bseq g")
1.1390 +prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g)
1.1391 +apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff)
1.1392 +apply (rule_tac x = "lim f" in exI)
1.1393 +apply (rule_tac x = "lim g" in exI)
1.1394 +apply (auto intro: LIMSEQ_le)
1.1395 +apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff)
1.1396 +done
1.1397 +
1.1398 +lemma lemma_nest_unique: "[| \<forall>n. f(n) \<le> f(Suc n);
1.1399 +         \<forall>n. g(Suc n) \<le> g(n);
1.1400 +         \<forall>n. f(n) \<le> g(n);
1.1401 +         (%n. f(n) - g(n)) ----> 0 |]
1.1402 +      ==> \<exists>l. ((\<forall>n. f(n) \<le> l) & f ----> l) &
1.1403 +                ((\<forall>n. l \<le> g(n)) & g ----> l)"
1.1404 +apply (drule lemma_nest, auto)
1.1405 +apply (subgoal_tac "l = m")
1.1406 +apply (drule_tac [2] X = f in LIMSEQ_diff)
1.1407 +apply (auto intro: LIMSEQ_unique)
1.1408 +done
1.1409 +
1.1410 +text{*The universal quantifiers below are required for the declaration
1.1411 +  of @{text Bolzano_nest_unique} below.*}
1.1412 +
1.1413 +lemma Bolzano_bisect_le:
1.1414 + "a \<le> b ==> \<forall>n. fst (Bolzano_bisect P a b n) \<le> snd (Bolzano_bisect P a b n)"
1.1415 +apply (rule allI)
1.1416 +apply (induct_tac "n")
1.1417 +apply (auto simp add: Let_def split_def)
1.1418 +done
1.1419 +
1.1420 +lemma Bolzano_bisect_fst_le_Suc: "a \<le> b ==>
1.1421 +   \<forall>n. fst(Bolzano_bisect P a b n) \<le> fst (Bolzano_bisect P a b (Suc n))"
1.1422 +apply (rule allI)
1.1423 +apply (induct_tac "n")
1.1424 +apply (auto simp add: Bolzano_bisect_le Let_def split_def)
1.1425 +done
1.1426 +
1.1427 +lemma Bolzano_bisect_Suc_le_snd: "a \<le> b ==>
1.1428 +   \<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
1.1429 +apply (rule allI)
1.1430 +apply (induct_tac "n")
1.1431 +apply (auto simp add: Bolzano_bisect_le Let_def split_def)
1.1432 +done
1.1433 +
1.1434 +lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
1.1435 +apply auto
1.1436 +apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
1.1437 +apply auto
1.1438 +done
1.1439 +
1.1440 +lemma Bolzano_bisect_diff:
1.1441 +     "a \<le> b ==>
1.1442 +      snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) =
1.1443 +      (b-a) / (2 ^ n)"
1.1444 +apply (induct_tac "n")
1.1447 +done
1.1448 +
1.1449 +lemmas Bolzano_nest_unique =
1.1450 +    lemma_nest_unique
1.1451 +    [OF Bolzano_bisect_fst_le_Suc Bolzano_bisect_Suc_le_snd Bolzano_bisect_le]
1.1452 +
1.1453 +
1.1454 +lemma not_P_Bolzano_bisect:
1.1455 +  assumes P:    "!!a b c. [| P(a,b); P(b,c); a \<le> b; b \<le> c|] ==> P(a,c)"
1.1456 +      and notP: "~ P(a,b)"
1.1457 +      and le:   "a \<le> b"
1.1458 +  shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
1.1459 +proof (induct n)
1.1460 +  case 0 thus ?case by simp
1.1461 + next
1.1462 +  case (Suc n)
1.1463 +  thus ?case
1.1464 + by (auto simp del: surjective_pairing [symmetric]
1.1465 +             simp add: Let_def split_def Bolzano_bisect_le [OF le]
1.1466 +     P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"])
1.1467 +qed
1.1468 +
1.1469 +(*Now we re-package P_prem as a formula*)
1.1470 +lemma not_P_Bolzano_bisect':
1.1471 +     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
1.1472 +         ~ P(a,b);  a \<le> b |] ==>
1.1473 +      \<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
1.1474 +by (blast elim!: not_P_Bolzano_bisect [THEN [2] rev_notE])
1.1475 +
1.1476 +
1.1477 +
1.1478 +lemma lemma_BOLZANO:
1.1479 +     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
1.1480 +         \<forall>x. \<exists>d::real. 0 < d &
1.1481 +                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
1.1482 +         a \<le> b |]
1.1483 +      ==> P(a,b)"
1.1484 +apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+)
1.1485 +apply (rule LIMSEQ_minus_cancel)
1.1486 +apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
1.1487 +apply (rule ccontr)
1.1488 +apply (drule not_P_Bolzano_bisect', assumption+)
1.1489 +apply (rename_tac "l")
1.1490 +apply (drule_tac x = l in spec, clarify)
1.1492 +apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
1.1493 +apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
1.1494 +apply (drule real_less_half_sum, auto)
1.1495 +apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec)
1.1496 +apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec)
1.1497 +apply safe
1.1498 +apply (simp_all (no_asm_simp))
1.1499 +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)
1.1500 +apply (simp (no_asm_simp) add: abs_if)
1.1501 +apply (rule real_sum_of_halves [THEN subst])
1.1503 +apply (simp_all add: diff_minus [symmetric])
1.1504 +done
1.1505 +
1.1506 +
1.1507 +lemma lemma_BOLZANO2: "((\<forall>a b c. (a \<le> b & b \<le> c & P(a,b) & P(b,c)) --> P(a,c)) &
1.1508 +       (\<forall>x. \<exists>d::real. 0 < d &
1.1509 +                (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b))))
1.1510 +      --> (\<forall>a b. a \<le> b --> P(a,b))"
1.1511 +apply clarify
1.1512 +apply (blast intro: lemma_BOLZANO)
1.1513 +done
1.1514 +
1.1515 +
1.1516 +subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
1.1517 +
1.1518 +lemma IVT: "[| f(a) \<le> y; y \<le> f(b);
1.1519 +         a \<le> b;
1.1520 +         (\<forall>x. a \<le> x & x \<le> b --> isCont f x) |]
1.1521 +      ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
1.1522 +apply (rule contrapos_pp, assumption)
1.1523 +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)
1.1524 +apply safe
1.1525 +apply simp_all
1.1526 +apply (simp add: isCont_iff LIM_def)
1.1527 +apply (rule ccontr)
1.1528 +apply (subgoal_tac "a \<le> x & x \<le> b")
1.1529 + prefer 2
1.1530 + apply simp
1.1531 + apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
1.1532 +apply (drule_tac x = x in spec)+
1.1533 +apply simp
1.1534 +apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar> " in spec)
1.1535 +apply safe
1.1536 +apply simp
1.1537 +apply (drule_tac x = s in spec, clarify)
1.1538 +apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe)
1.1539 +apply (drule_tac x = "ba-x" in spec)
1.1541 +apply (drule_tac x = "aa-x" in spec)
1.1542 +apply (case_tac "x \<le> aa", simp_all)
1.1543 +apply (drule_tac x = x and y = aa in order_antisym)
1.1544 +apply (assumption, simp)
1.1545 +done
1.1546 +
1.1547 +lemma IVT2: "[| f(b) \<le> y; y \<le> f(a);
1.1548 +         a \<le> b;
1.1549 +         (\<forall>x. a \<le> x & x \<le> b --> isCont f x)
1.1550 +      |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
1.1551 +apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
1.1552 +apply (drule IVT [where f = "%x. - f x"], assumption)
1.1553 +apply (auto intro: isCont_minus)
1.1554 +done
1.1555 +
1.1556 +(*HOL style here: object-level formulations*)
1.1557 +lemma IVT_objl: "(f(a) \<le> y & y \<le> f(b) & a \<le> b &
1.1558 +      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
1.1559 +      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
1.1560 +apply (blast intro: IVT)
1.1561 +done
1.1562 +
1.1563 +lemma IVT2_objl: "(f(b) \<le> y & y \<le> f(a) & a \<le> b &
1.1564 +      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
1.1565 +      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
1.1566 +apply (blast intro: IVT2)
1.1567 +done
1.1568 +
1.1569 +(*---------------------------------------------------------------------------*)
1.1570 +(* By bisection, function continuous on closed interval is bounded above     *)
1.1571 +(*---------------------------------------------------------------------------*)
1.1572 +
1.1573 +
1.1574 +lemma isCont_bounded:
1.1575 +     "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
1.1576 +      ==> \<exists>M. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
1.1577 +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)
1.1578 +apply safe
1.1579 +apply simp_all
1.1580 +apply (rename_tac x xa ya M Ma)
1.1581 +apply (cut_tac x = M and y = Ma in linorder_linear, safe)
1.1582 +apply (rule_tac x = Ma in exI, clarify)
1.1583 +apply (cut_tac x = xb and y = xa in linorder_linear, force)
1.1584 +apply (rule_tac x = M in exI, clarify)
1.1585 +apply (cut_tac x = xb and y = xa in linorder_linear, force)
1.1586 +apply (case_tac "a \<le> x & x \<le> b")
1.1587 +apply (rule_tac [2] x = 1 in exI)
1.1588 +prefer 2 apply force
1.1589 +apply (simp add: LIM_def isCont_iff)
1.1590 +apply (drule_tac x = x in spec, auto)
1.1591 +apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
1.1592 +apply (drule_tac x = 1 in spec, auto)
1.1593 +apply (rule_tac x = s in exI, clarify)
1.1594 +apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
1.1595 +apply (drule_tac x = "xa-x" in spec)
1.1596 +apply (auto simp add: abs_ge_self, arith+)
1.1597 +done
1.1598 +
1.1599 +(*----------------------------------------------------------------------------*)
1.1600 +(* Refine the above to existence of least upper bound                         *)
1.1601 +(*----------------------------------------------------------------------------*)
1.1602 +
1.1603 +lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) -->
1.1604 +      (\<exists>t. isLub UNIV S t)"
1.1605 +apply (blast intro: reals_complete)
1.1606 +done
1.1607 +
1.1608 +lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
1.1609 +         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
1.1610 +                   (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
1.1611 +apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x) " in lemma_reals_complete)
1.1612 +apply auto
1.1613 +apply (drule isCont_bounded, assumption)
1.1614 +apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
1.1615 +apply (rule exI, auto)
1.1616 +apply (auto dest!: spec simp add: linorder_not_less)
1.1617 +done
1.1618 +
1.1619 +(*----------------------------------------------------------------------------*)
1.1620 +(* Now show that it attains its upper bound                                   *)
1.1621 +(*----------------------------------------------------------------------------*)
1.1622 +
1.1623 +lemma isCont_eq_Ub:
1.1624 +  assumes le: "a \<le> b"
1.1625 +      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
1.1626 +  shows "\<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
1.1627 +             (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
1.1628 +proof -
1.1629 +  from isCont_has_Ub [OF le con]
1.1630 +  obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
1.1631 +             and M2: "!!N. N<M ==> \<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x"  by blast
1.1632 +  show ?thesis
1.1633 +  proof (intro exI, intro conjI)
1.1634 +    show " \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" by (rule M1)
1.1635 +    show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M"
1.1636 +    proof (rule ccontr)
1.1637 +      assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
1.1638 +      with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
1.1639 +        by (auto simp add: linorder_not_le [symmetric] intro: order_antisym)
1.1640 +      hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
1.1641 +        by (auto simp add: isCont_inverse isCont_diff con)
1.1642 +      from isCont_bounded [OF le this]
1.1643 +      obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
1.1644 +      have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
1.1645 +        by (simp add: M3)
1.1646 +      have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k
1.1647 +        by (auto intro: order_le_less_trans [of _ k])
1.1648 +      with Minv
1.1649 +      have "!!x. a \<le> x & x \<le> b --> inverse(k+1) < inverse(inverse(M - f x))"
1.1650 +        by (intro strip less_imp_inverse_less, simp_all)
1.1651 +      hence invlt: "!!x. a \<le> x & x \<le> b --> inverse(k+1) < M - f x"
1.1652 +        by simp
1.1653 +      have "M - inverse (k+1) < M" using k [of a] Minv [of a] le
1.1654 +        by (simp, arith)
1.1655 +      from M2 [OF this]
1.1656 +      obtain x where ax: "a \<le> x & x \<le> b & M - inverse(k+1) < f x" ..
1.1657 +      thus False using invlt [of x] by force
1.1658 +    qed
1.1659 +  qed
1.1660 +qed
1.1661 +
1.1662 +
1.1663 +
1.1664 +(*----------------------------------------------------------------------------*)
1.1665 +(* Same theorem for lower bound                                               *)
1.1666 +(*----------------------------------------------------------------------------*)
1.1667 +
1.1668 +lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
1.1669 +         ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
1.1670 +                   (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
1.1671 +apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
1.1672 +prefer 2 apply (blast intro: isCont_minus)
1.1673 +apply (drule_tac f = " (%x. - (f x))" in isCont_eq_Ub)
1.1674 +apply safe
1.1675 +apply auto
1.1676 +done
1.1677 +
1.1678 +
1.1679 +(* ------------------------------------------------------------------------- *)
1.1680 +(* Another version.                                                          *)
1.1681 +(* ------------------------------------------------------------------------- *)
1.1682 +
1.1683 +lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
1.1684 +      ==> \<exists>L M. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
1.1685 +          (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))"
1.1686 +apply (frule isCont_eq_Lb)
1.1687 +apply (frule_tac [2] isCont_eq_Ub)
1.1688 +apply (assumption+, safe)
1.1689 +apply (rule_tac x = "f x" in exI)
1.1690 +apply (rule_tac x = "f xa" in exI, simp, safe)
1.1691 +apply (cut_tac x = x and y = xa in linorder_linear, safe)
1.1692 +apply (cut_tac f = f and a = x and b = xa and y = y in IVT_objl)
1.1693 +apply (cut_tac [2] f = f and a = xa and b = x and y = y in IVT2_objl, safe)
1.1694 +apply (rule_tac [2] x = xb in exI)
1.1695 +apply (rule_tac [4] x = xb in exI, simp_all)
1.1696 +done
1.1697 +
1.1698 +(*----------------------------------------------------------------------------*)
1.1699 +(* If f'(x) > 0 then x is locally strictly increasing at the right            *)
1.1700 +(*----------------------------------------------------------------------------*)
1.1701 +
1.1702 +lemma DERIV_left_inc:
1.1703 +    "[| DERIV f x :> l;  0 < l |]
1.1704 +     ==> \<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
1.1705 +apply (simp add: deriv_def LIM_def)
1.1706 +apply (drule spec, auto)
1.1707 +apply (rule_tac x = s in exI, auto)
1.1708 +apply (subgoal_tac "0 < l*h")
1.1709 + prefer 2 apply (simp add: zero_less_mult_iff)
1.1710 +apply (drule_tac x = h in spec)
1.1711 +apply (simp add: real_abs_def pos_le_divide_eq pos_less_divide_eq
1.1713 +done
1.1714 +
1.1715 +lemma DERIV_left_dec:
1.1716 +  assumes der: "DERIV f x :> l"
1.1717 +      and l:   "l < 0"
1.1718 +  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x-h))"
1.1719 +proof -
1.1720 +  from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
1.1721 +  have "\<exists>s. 0 < s \<and>
1.1722 +              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
1.1723 +    by (simp add: diff_minus)
1.1724 +  then obtain s
1.1725 +        where s:   "0 < s"
1.1726 +          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
1.1727 +    by auto
1.1728 +  thus ?thesis
1.1729 +  proof (intro exI conjI strip)
1.1730 +    show "0<s" .
1.1731 +    fix h::real
1.1732 +    assume "0 < h \<and> h < s"
1.1733 +    with all [of "-h"] show "f x < f (x-h)"
1.1734 +    proof (simp add: real_abs_def pos_less_divide_eq diff_minus [symmetric]
1.1736 +      assume "~ l \<le> - ((f (x-h) - f x) / h)" and h: "0 < h"
1.1737 +      with l
1.1738 +      have "0 < (f (x-h) - f x) / h" by arith
1.1739 +      thus "f x < f (x-h)"
1.1740 +	by (simp add: pos_less_divide_eq h)
1.1741 +    qed
1.1742 +  qed
1.1743 +qed
1.1744 +
1.1745 +lemma DERIV_local_max:
1.1746 +  assumes der: "DERIV f x :> l"
1.1747 +      and d:   "0 < d"
1.1748 +      and le:  "\<forall>y. \<bar>x-y\<bar> < d --> f(y) \<le> f(x)"
1.1749 +  shows "l = 0"
1.1750 +proof (cases rule: linorder_cases [of l 0])
1.1751 +  case equal show ?thesis .
1.1752 +next
1.1753 +  case less
1.1754 +  from DERIV_left_dec [OF der less]
1.1755 +  obtain d' where d': "0 < d'"
1.1756 +             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x-h)" by blast
1.1757 +  from real_lbound_gt_zero [OF d d']
1.1758 +  obtain e where "0 < e \<and> e < d \<and> e < d'" ..
1.1759 +  with lt le [THEN spec [where x="x-e"]]
1.1760 +  show ?thesis by (auto simp add: abs_if)
1.1761 +next
1.1762 +  case greater
1.1763 +  from DERIV_left_inc [OF der greater]
1.1764 +  obtain d' where d': "0 < d'"
1.1765 +             and lt: "\<forall>h. 0 < h \<and> h < d' \<longrightarrow> f x < f (x + h)" by blast
1.1766 +  from real_lbound_gt_zero [OF d d']
1.1767 +  obtain e where "0 < e \<and> e < d \<and> e < d'" ..
1.1768 +  with lt le [THEN spec [where x="x+e"]]
1.1769 +  show ?thesis by (auto simp add: abs_if)
1.1770 +qed
1.1771 +
1.1772 +
1.1773 +text{*Similar theorem for a local minimum*}
1.1774 +lemma DERIV_local_min:
1.1775 +     "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) \<le> f(y) |] ==> l = 0"
1.1776 +by (drule DERIV_minus [THEN DERIV_local_max], auto)
1.1777 +
1.1778 +
1.1779 +text{*In particular, if a function is locally flat*}
1.1780 +lemma DERIV_local_const:
1.1781 +     "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
1.1782 +by (auto dest!: DERIV_local_max)
1.1783 +
1.1784 +text{*Lemma about introducing open ball in open interval*}
1.1785 +lemma lemma_interval_lt:
1.1786 +     "[| a < x;  x < b |]
1.1787 +      ==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>x-y\<bar> < d --> a < y & y < b)"
1.1789 +apply (insert linorder_linear [of "x-a" "b-x"], safe)
1.1790 +apply (rule_tac x = "x-a" in exI)
1.1791 +apply (rule_tac [2] x = "b-x" in exI, auto)
1.1792 +done
1.1793 +
1.1794 +lemma lemma_interval: "[| a < x;  x < b |] ==>
1.1795 +        \<exists>d::real. 0 < d &  (\<forall>y. \<bar>x-y\<bar> < d --> a \<le> y & y \<le> b)"
1.1796 +apply (drule lemma_interval_lt, auto)
1.1797 +apply (auto intro!: exI)
1.1798 +done
1.1799 +
1.1800 +text{*Rolle's Theorem.
1.1801 +   If @{term f} is defined and continuous on the closed interval
1.1802 +   @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"},
1.1803 +   and @{term "f(a) = f(b)"},
1.1804 +   then there exists @{text "x0 \<in> (a,b)"} such that @{term "f'(x0) = 0"}*}
1.1805 +theorem Rolle:
1.1806 +  assumes lt: "a < b"
1.1807 +      and eq: "f(a) = f(b)"
1.1808 +      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
1.1809 +      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
1.1810 +  shows "\<exists>z. a < z & z < b & DERIV f z :> 0"
1.1811 +proof -
1.1812 +  have le: "a \<le> b" using lt by simp
1.1813 +  from isCont_eq_Ub [OF le con]
1.1814 +  obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x"
1.1815 +             and alex: "a \<le> x" and xleb: "x \<le> b"
1.1816 +    by blast
1.1817 +  from isCont_eq_Lb [OF le con]
1.1818 +  obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z"
1.1819 +              and alex': "a \<le> x'" and x'leb: "x' \<le> b"
1.1820 +    by blast
1.1821 +  show ?thesis
1.1822 +  proof cases
1.1823 +    assume axb: "a < x & x < b"
1.1824 +        --{*@{term f} attains its maximum within the interval*}
1.1825 +    hence ax: "a<x" and xb: "x<b" by auto
1.1826 +    from lemma_interval [OF ax xb]
1.1827 +    obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
1.1828 +      by blast
1.1829 +    hence bound': "\<forall>y. \<bar>x-y\<bar> < d \<longrightarrow> f y \<le> f x" using x_max
1.1830 +      by blast
1.1831 +    from differentiableD [OF dif [OF axb]]
1.1832 +    obtain l where der: "DERIV f x :> l" ..
1.1833 +    have "l=0" by (rule DERIV_local_max [OF der d bound'])
1.1834 +        --{*the derivative at a local maximum is zero*}
1.1835 +    thus ?thesis using ax xb der by auto
1.1836 +  next
1.1837 +    assume notaxb: "~ (a < x & x < b)"
1.1838 +    hence xeqab: "x=a | x=b" using alex xleb by arith
1.1839 +    hence fb_eq_fx: "f b = f x" by (auto simp add: eq)
1.1840 +    show ?thesis
1.1841 +    proof cases
1.1842 +      assume ax'b: "a < x' & x' < b"
1.1843 +        --{*@{term f} attains its minimum within the interval*}
1.1844 +      hence ax': "a<x'" and x'b: "x'<b" by auto
1.1845 +      from lemma_interval [OF ax' x'b]
1.1846 +      obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
1.1847 +	by blast
1.1848 +      hence bound': "\<forall>y. \<bar>x'-y\<bar> < d \<longrightarrow> f x' \<le> f y" using x'_min
1.1849 +	by blast
1.1850 +      from differentiableD [OF dif [OF ax'b]]
1.1851 +      obtain l where der: "DERIV f x' :> l" ..
1.1852 +      have "l=0" by (rule DERIV_local_min [OF der d bound'])
1.1853 +        --{*the derivative at a local minimum is zero*}
1.1854 +      thus ?thesis using ax' x'b der by auto
1.1855 +    next
1.1856 +      assume notax'b: "~ (a < x' & x' < b)"
1.1857 +        --{*@{term f} is constant througout the interval*}
1.1858 +      hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith
1.1859 +      hence fb_eq_fx': "f b = f x'" by (auto simp add: eq)
1.1860 +      from dense [OF lt]
1.1861 +      obtain r where ar: "a < r" and rb: "r < b" by blast
1.1862 +      from lemma_interval [OF ar rb]
1.1863 +      obtain d where d: "0<d" and bound: "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b"
1.1864 +	by blast
1.1865 +      have eq_fb: "\<forall>z. a \<le> z --> z \<le> b --> f z = f b"
1.1866 +      proof (clarify)
1.1867 +        fix z::real
1.1868 +        assume az: "a \<le> z" and zb: "z \<le> b"
1.1869 +        show "f z = f b"
1.1870 +        proof (rule order_antisym)
1.1871 +          show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb)
1.1872 +          show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb)
1.1873 +        qed
1.1874 +      qed
1.1875 +      have bound': "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> f r = f y"
1.1876 +      proof (intro strip)
1.1877 +        fix y::real
1.1878 +        assume lt: "\<bar>r-y\<bar> < d"
1.1879 +        hence "f y = f b" by (simp add: eq_fb bound)
1.1880 +        thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le)
1.1881 +      qed
1.1882 +      from differentiableD [OF dif [OF conjI [OF ar rb]]]
1.1883 +      obtain l where der: "DERIV f r :> l" ..
1.1884 +      have "l=0" by (rule DERIV_local_const [OF der d bound'])
1.1885 +        --{*the derivative of a constant function is zero*}
1.1886 +      thus ?thesis using ar rb der by auto
1.1887 +    qed
1.1888 +  qed
1.1889 +qed
1.1890 +
1.1891 +
1.1892 +subsection{*Mean Value Theorem*}
1.1893 +
1.1894 +lemma lemma_MVT:
1.1895 +     "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
1.1896 +proof cases
1.1897 +  assume "a=b" thus ?thesis by simp
1.1898 +next
1.1899 +  assume "a\<noteq>b"
1.1900 +  hence ba: "b-a \<noteq> 0" by arith
1.1901 +  show ?thesis
1.1902 +    by (rule real_mult_left_cancel [OF ba, THEN iffD1],
1.1904 +qed
1.1905 +
1.1906 +theorem MVT:
1.1907 +  assumes lt:  "a < b"
1.1908 +      and con: "\<forall>x. a \<le> x & x \<le> b --> isCont f x"
1.1909 +      and dif [rule_format]: "\<forall>x. a < x & x < b --> f differentiable x"
1.1910 +  shows "\<exists>l z. a < z & z < b & DERIV f z :> l &
1.1911 +                   (f(b) - f(a) = (b-a) * l)"
1.1912 +proof -
1.1913 +  let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
1.1914 +  have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
1.1915 +    by (fast intro: isCont_diff isCont_const isCont_mult isCont_Id)
1.1916 +  have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
1.1917 +  proof (clarify)
1.1918 +    fix x::real
1.1919 +    assume ax: "a < x" and xb: "x < b"
1.1920 +    from differentiableD [OF dif [OF conjI [OF ax xb]]]
1.1921 +    obtain l where der: "DERIV f x :> l" ..
1.1922 +    show "?F differentiable x"
1.1923 +      by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"],
1.1924 +          blast intro: DERIV_diff DERIV_cmult_Id der)
1.1925 +  qed
1.1926 +  from Rolle [where f = ?F, OF lt lemma_MVT contF difF]
1.1927 +  obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0"
1.1928 +    by blast
1.1929 +  have "DERIV (%x. ((f b - f a)/(b-a)) * x) z :> (f b - f a)/(b-a)"
1.1930 +    by (rule DERIV_cmult_Id)
1.1931 +  hence derF: "DERIV (\<lambda>x. ?F x + (f b - f a) / (b - a) * x) z
1.1932 +                   :> 0 + (f b - f a) / (b - a)"
1.1933 +    by (rule DERIV_add [OF der])
1.1934 +  show ?thesis
1.1935 +  proof (intro exI conjI)
1.1936 +    show "a < z" .
1.1937 +    show "z < b" .
1.1938 +    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by simp
1.1939 +    show "DERIV f z :> ((f b - f a)/(b-a))"  using derF by simp
1.1940 +  qed
1.1941 +qed
1.1942 +
1.1943 +
1.1944 +text{*A function is constant if its derivative is 0 over an interval.*}
1.1945 +
1.1946 +lemma DERIV_isconst_end: "[| a < b;
1.1947 +         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
1.1948 +         \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
1.1949 +        ==> (f b = f a)"
1.1950 +apply (drule MVT, assumption)
1.1951 +apply (blast intro: differentiableI)
1.1952 +apply (auto dest!: DERIV_unique simp add: diff_eq_eq)
1.1953 +done
1.1954 +
1.1955 +lemma DERIV_isconst1: "[| a < b;
1.1956 +         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
1.1957 +         \<forall>x. a < x & x < b --> DERIV f x :> 0 |]
1.1958 +        ==> \<forall>x. a \<le> x & x \<le> b --> f x = f a"
1.1959 +apply safe
1.1960 +apply (drule_tac x = a in order_le_imp_less_or_eq, safe)
1.1961 +apply (drule_tac b = x in DERIV_isconst_end, auto)
1.1962 +done
1.1963 +
1.1964 +lemma DERIV_isconst2: "[| a < b;
1.1965 +         \<forall>x. a \<le> x & x \<le> b --> isCont f x;
1.1966 +         \<forall>x. a < x & x < b --> DERIV f x :> 0;
1.1967 +         a \<le> x; x \<le> b |]
1.1968 +        ==> f x = f a"
1.1969 +apply (blast dest: DERIV_isconst1)
1.1970 +done
1.1971 +
1.1972 +lemma DERIV_isconst_all: "\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)"
1.1973 +apply (rule linorder_cases [of x y])
1.1974 +apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+
1.1975 +done
1.1976 +
1.1977 +lemma DERIV_const_ratio_const:
1.1978 +     "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k"
1.1979 +apply (rule linorder_cases [of a b], auto)
1.1980 +apply (drule_tac [!] f = f in MVT)
1.1981 +apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
1.1982 +apply (auto dest: DERIV_unique simp add: left_distrib diff_minus)
1.1983 +done
1.1984 +
1.1985 +lemma DERIV_const_ratio_const2:
1.1986 +     "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
1.1987 +apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
1.1988 +apply (auto dest!: DERIV_const_ratio_const simp add: real_mult_assoc)
1.1989 +done
1.1990 +
1.1991 +lemma real_average_minus_first: "((a + b) /2 - a) = (b-a)/(2::real)"
1.1992 +by auto
1.1993 +declare real_average_minus_first [simp]
1.1994 +
1.1995 +lemma real_average_minus_second: "((b + a)/2 - a) = (b-a)/(2::real)"
1.1996 +by auto
1.1997 +declare real_average_minus_second [simp]
1.1998 +
1.1999 +text{*Gallileo's "trick": average velocity = av. of end velocities*}
1.2000 +
1.2001 +lemma DERIV_const_average:
1.2002 +  assumes neq: "a \<noteq> (b::real)"
1.2003 +      and der: "\<forall>x. DERIV v x :> k"
1.2004 +  shows "v ((a + b)/2) = (v a + v b)/2"
1.2005 +proof (cases rule: linorder_cases [of a b])
1.2006 +  case equal with neq show ?thesis by simp
1.2007 +next
1.2008 +  case less
1.2009 +  have "(v b - v a) / (b - a) = k"
1.2010 +    by (rule DERIV_const_ratio_const2 [OF neq der])
1.2011 +  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp
1.2012 +  moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k"
1.2013 +    by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
1.2014 +  ultimately show ?thesis using neq by force
1.2015 +next
1.2016 +  case greater
1.2017 +  have "(v b - v a) / (b - a) = k"
1.2018 +    by (rule DERIV_const_ratio_const2 [OF neq der])
1.2019 +  hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp
1.2020 +  moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k"
1.2021 +    by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq)
1.2022 +  ultimately show ?thesis using neq by (force simp add: add_commute)
1.2023 +qed
1.2024 +
1.2025 +
1.2026 +text{*Dull lemma: an continuous injection on an interval must have a
1.2027 +strict maximum at an end point, not in the middle.*}
1.2028 +
1.2029 +lemma lemma_isCont_inj:
1.2030 +  assumes d: "0 < d"
1.2031 +      and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
1.2032 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
1.2033 +  shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
1.2034 +proof (rule ccontr)
1.2035 +  assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
1.2036 +  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
1.2037 +  show False
1.2038 +  proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
1.2039 +    case le
1.2040 +    from d cont all [of "x+d"]
1.2041 +    have flef: "f(x+d) \<le> f x"
1.2042 +     and xlex: "x - d \<le> x"
1.2043 +     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
1.2044 +       by (auto simp add: abs_if)
1.2045 +    from IVT [OF le flef xlex cont']
1.2046 +    obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
1.2047 +    moreover
1.2048 +    hence "g(f x') = g (f(x+d))" by simp
1.2049 +    ultimately show False using d inj [of x'] inj [of "x+d"]
1.2050 +      by (simp add: abs_le_interval_iff)
1.2051 +  next
1.2052 +    case ge
1.2053 +    from d cont all [of "x-d"]
1.2054 +    have flef: "f(x-d) \<le> f x"
1.2055 +     and xlex: "x \<le> x+d"
1.2056 +     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
1.2057 +       by (auto simp add: abs_if)
1.2058 +    from IVT2 [OF ge flef xlex cont']
1.2059 +    obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
1.2060 +    moreover
1.2061 +    hence "g(f x') = g (f(x-d))" by simp
1.2062 +    ultimately show False using d inj [of x'] inj [of "x-d"]
1.2063 +      by (simp add: abs_le_interval_iff)
1.2064 +  qed
1.2065 +qed
1.2066 +
1.2067 +
1.2068 +text{*Similar version for lower bound.*}
1.2069 +
1.2070 +lemma lemma_isCont_inj2:
1.2071 +     "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
1.2072 +        \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
1.2073 +      ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
1.2074 +apply (insert lemma_isCont_inj
1.2075 +          [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
1.2076 +apply (simp add: isCont_minus linorder_not_le)
1.2077 +done
1.2078 +
1.2079 +text{*Show there's an interval surrounding @{term "f(x)"} in
1.2080 +@{text "f[[x - d, x + d]]"} .*}
1.2081 +
1.2082 +lemma isCont_inj_range:
1.2083 +  assumes d: "0 < d"
1.2084 +      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
1.2085 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
1.2086 +  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))"
1.2087 +proof -
1.2088 +  have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
1.2089 +    by (auto simp add: abs_le_interval_iff)
1.2090 +  from isCont_Lb_Ub [OF this]
1.2091 +  obtain L M
1.2092 +  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"
1.2093 +    and all2 [rule_format]:
1.2094 +           "\<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)"
1.2095 +    by auto
1.2096 +  with d have "L \<le> f x & f x \<le> M" by simp
1.2097 +  moreover have "L \<noteq> f x"
1.2098 +  proof -
1.2099 +    from lemma_isCont_inj2 [OF d inj cont]
1.2100 +    obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x"  by auto
1.2101 +    thus ?thesis using all1 [of u] by arith
1.2102 +  qed
1.2103 +  moreover have "f x \<noteq> M"
1.2104 +  proof -
1.2105 +    from lemma_isCont_inj [OF d inj cont]
1.2106 +    obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u"  by auto
1.2107 +    thus ?thesis using all1 [of u] by arith
1.2108 +  qed
1.2109 +  ultimately have "L < f x & f x < M" by arith
1.2110 +  hence "0 < f x - L" "0 < M - f x" by arith+
1.2111 +  from real_lbound_gt_zero [OF this]
1.2112 +  obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
1.2113 +  thus ?thesis
1.2114 +  proof (intro exI conjI)
1.2115 +    show "0<e" .
1.2116 +    show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
1.2117 +    proof (intro strip)
1.2118 +      fix y::real
1.2119 +      assume "\<bar>y - f x\<bar> \<le> e"
1.2120 +      with e have "L \<le> y \<and> y \<le> M" by arith
1.2121 +      from all2 [OF this]
1.2122 +      obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
1.2123 +      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
1.2124 +        by (force simp add: abs_le_interval_iff)
1.2125 +    qed
1.2126 +  qed
1.2127 +qed
1.2128 +
1.2129 +
1.2130 +text{*Continuity of inverse function*}
1.2131 +
1.2132 +lemma isCont_inverse_function:
1.2133 +  assumes d: "0 < d"
1.2134 +      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
1.2135 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
1.2136 +  shows "isCont g (f x)"
1.2137 +proof (simp add: isCont_iff LIM_eq)
1.2138 +  show "\<forall>r. 0 < r \<longrightarrow>
1.2139 +         (\<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))"
1.2140 +  proof (intro strip)
1.2141 +    fix r::real
1.2142 +    assume r: "0<r"
1.2143 +    from real_lbound_gt_zero [OF r d]
1.2144 +    obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
1.2145 +    with inj cont
1.2146 +    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
1.2147 +                  "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
1.2148 +    from isCont_inj_range [OF e this]
1.2149 +    obtain e' where e': "0 < e'"
1.2150 +        and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
1.2151 +          by blast
1.2152 +    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)"
1.2153 +    proof (intro exI conjI)
1.2154 +      show "0<e'" .
1.2155 +      show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
1.2156 +      proof (intro strip)
1.2157 +        fix z::real
1.2158 +        assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
1.2159 +        with e e_lt e_simps all [rule_format, of "f x + z"]
1.2160 +        show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
1.2161 +      qed
1.2162 +    qed
1.2163 +  qed
1.2164 +qed
1.2165 +
1.2166 +ML
1.2167 +{*
1.2168 +val LIM_def = thm"LIM_def";
1.2169 +val NSLIM_def = thm"NSLIM_def";
1.2170 +val isCont_def = thm"isCont_def";
1.2171 +val isNSCont_def = thm"isNSCont_def";
1.2172 +val deriv_def = thm"deriv_def";
1.2173 +val nsderiv_def = thm"nsderiv_def";
1.2174 +val differentiable_def = thm"differentiable_def";
1.2175 +val NSdifferentiable_def = thm"NSdifferentiable_def";
1.2176 +val increment_def = thm"increment_def";
1.2177 +val isUCont_def = thm"isUCont_def";
1.2178 +val isNSUCont_def = thm"isNSUCont_def";
1.2179 +
1.2180 +val half_gt_zero_iff = thm "half_gt_zero_iff";
1.2181 +val half_gt_zero = thms "half_gt_zero";
1.2182 +val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
1.2183 +val LIM_eq = thm "LIM_eq";
1.2184 +val LIM_D = thm "LIM_D";
1.2185 +val LIM_const = thm "LIM_const";
1.2187 +val LIM_minus = thm "LIM_minus";
1.2189 +val LIM_diff = thm "LIM_diff";
1.2190 +val LIM_const_not_eq = thm "LIM_const_not_eq";
1.2191 +val LIM_const_eq = thm "LIM_const_eq";
1.2192 +val LIM_unique = thm "LIM_unique";
1.2193 +val LIM_mult_zero = thm "LIM_mult_zero";
1.2194 +val LIM_self = thm "LIM_self";
1.2195 +val LIM_equal = thm "LIM_equal";
1.2196 +val LIM_trans = thm "LIM_trans";
1.2197 +val LIM_NSLIM = thm "LIM_NSLIM";
1.2198 +val NSLIM_LIM = thm "NSLIM_LIM";
1.2199 +val LIM_NSLIM_iff = thm "LIM_NSLIM_iff";
1.2200 +val NSLIM_mult = thm "NSLIM_mult";
1.2201 +val LIM_mult2 = thm "LIM_mult2";
1.2204 +val NSLIM_const = thm "NSLIM_const";
1.2205 +val LIM_const2 = thm "LIM_const2";
1.2206 +val NSLIM_minus = thm "NSLIM_minus";
1.2207 +val LIM_minus2 = thm "LIM_minus2";
1.2210 +val NSLIM_inverse = thm "NSLIM_inverse";
1.2211 +val LIM_inverse = thm "LIM_inverse";
1.2212 +val NSLIM_zero = thm "NSLIM_zero";
1.2213 +val LIM_zero2 = thm "LIM_zero2";
1.2214 +val NSLIM_zero_cancel = thm "NSLIM_zero_cancel";
1.2215 +val LIM_zero_cancel = thm "LIM_zero_cancel";
1.2216 +val NSLIM_not_zero = thm "NSLIM_not_zero";
1.2217 +val NSLIM_const_not_eq = thm "NSLIM_const_not_eq";
1.2218 +val NSLIM_const_eq = thm "NSLIM_const_eq";
1.2219 +val NSLIM_unique = thm "NSLIM_unique";
1.2220 +val LIM_unique2 = thm "LIM_unique2";
1.2221 +val NSLIM_mult_zero = thm "NSLIM_mult_zero";
1.2222 +val LIM_mult_zero2 = thm "LIM_mult_zero2";
1.2223 +val NSLIM_self = thm "NSLIM_self";
1.2224 +val isNSContD = thm "isNSContD";
1.2225 +val isNSCont_NSLIM = thm "isNSCont_NSLIM";
1.2226 +val NSLIM_isNSCont = thm "NSLIM_isNSCont";
1.2227 +val isNSCont_NSLIM_iff = thm "isNSCont_NSLIM_iff";
1.2228 +val isNSCont_LIM_iff = thm "isNSCont_LIM_iff";
1.2229 +val isNSCont_isCont_iff = thm "isNSCont_isCont_iff";
1.2230 +val isCont_isNSCont = thm "isCont_isNSCont";
1.2231 +val isNSCont_isCont = thm "isNSCont_isCont";
1.2232 +val NSLIM_h_iff = thm "NSLIM_h_iff";
1.2233 +val NSLIM_isCont_iff = thm "NSLIM_isCont_iff";
1.2234 +val LIM_isCont_iff = thm "LIM_isCont_iff";
1.2235 +val isCont_iff = thm "isCont_iff";
1.2237 +val isCont_mult = thm "isCont_mult";
1.2238 +val isCont_o = thm "isCont_o";
1.2239 +val isCont_o2 = thm "isCont_o2";
1.2240 +val isNSCont_minus = thm "isNSCont_minus";
1.2241 +val isCont_minus = thm "isCont_minus";
1.2242 +val isCont_inverse = thm "isCont_inverse";
1.2243 +val isNSCont_inverse = thm "isNSCont_inverse";
1.2244 +val isCont_diff = thm "isCont_diff";
1.2245 +val isCont_const = thm "isCont_const";
1.2246 +val isNSCont_const = thm "isNSCont_const";
1.2247 +val isNSCont_rabs = thm "isNSCont_rabs";
1.2248 +val isCont_rabs = thm "isCont_rabs";
1.2249 +val isNSUContD = thm "isNSUContD";
1.2250 +val isUCont_isCont = thm "isUCont_isCont";
1.2251 +val isUCont_isNSUCont = thm "isUCont_isNSUCont";
1.2252 +val isNSUCont_isUCont = thm "isNSUCont_isUCont";
1.2253 +val DERIV_iff = thm "DERIV_iff";
1.2254 +val DERIV_NS_iff = thm "DERIV_NS_iff";
1.2255 +val DERIV_D = thm "DERIV_D";
1.2256 +val NS_DERIV_D = thm "NS_DERIV_D";
1.2257 +val DERIV_unique = thm "DERIV_unique";
1.2258 +val NSDeriv_unique = thm "NSDeriv_unique";
1.2259 +val differentiableD = thm "differentiableD";
1.2260 +val differentiableI = thm "differentiableI";
1.2261 +val NSdifferentiableD = thm "NSdifferentiableD";
1.2262 +val NSdifferentiableI = thm "NSdifferentiableI";
1.2263 +val LIM_I = thm "LIM_I";
1.2264 +val DERIV_LIM_iff = thm "DERIV_LIM_iff";
1.2265 +val DERIV_iff2 = thm "DERIV_iff2";
1.2266 +val NSDERIV_NSLIM_iff = thm "NSDERIV_NSLIM_iff";
1.2267 +val NSDERIV_NSLIM_iff2 = thm "NSDERIV_NSLIM_iff2";
1.2268 +val NSDERIV_iff2 = thm "NSDERIV_iff2";
1.2269 +val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff";
1.2270 +val NSDERIVD5 = thm "NSDERIVD5";
1.2271 +val NSDERIVD4 = thm "NSDERIVD4";
1.2272 +val NSDERIVD3 = thm "NSDERIVD3";
1.2273 +val NSDERIV_DERIV_iff = thm "NSDERIV_DERIV_iff";
1.2274 +val NSDERIV_isNSCont = thm "NSDERIV_isNSCont";
1.2275 +val DERIV_isCont = thm "DERIV_isCont";
1.2276 +val NSDERIV_const = thm "NSDERIV_const";
1.2277 +val DERIV_const = thm "DERIV_const";
1.2280 +val NSDERIV_mult = thm "NSDERIV_mult";
1.2281 +val DERIV_mult = thm "DERIV_mult";
1.2282 +val NSDERIV_cmult = thm "NSDERIV_cmult";
1.2283 +val DERIV_cmult = thm "DERIV_cmult";
1.2284 +val NSDERIV_minus = thm "NSDERIV_minus";
1.2285 +val DERIV_minus = thm "DERIV_minus";
1.2288 +val NSDERIV_diff = thm "NSDERIV_diff";
1.2289 +val DERIV_diff = thm "DERIV_diff";
1.2290 +val incrementI = thm "incrementI";
1.2291 +val incrementI2 = thm "incrementI2";
1.2292 +val increment_thm = thm "increment_thm";
1.2293 +val increment_thm2 = thm "increment_thm2";
1.2294 +val increment_approx_zero = thm "increment_approx_zero";
1.2295 +val NSDERIV_zero = thm "NSDERIV_zero";
1.2296 +val NSDERIV_approx = thm "NSDERIV_approx";
1.2297 +val NSDERIVD1 = thm "NSDERIVD1";
1.2298 +val NSDERIVD2 = thm "NSDERIVD2";
1.2299 +val NSDERIV_chain = thm "NSDERIV_chain";
1.2300 +val DERIV_chain = thm "DERIV_chain";
1.2301 +val DERIV_chain2 = thm "DERIV_chain2";
1.2302 +val NSDERIV_Id = thm "NSDERIV_Id";
1.2303 +val DERIV_Id = thm "DERIV_Id";
1.2304 +val isCont_Id = thms "isCont_Id";
1.2305 +val DERIV_cmult_Id = thm "DERIV_cmult_Id";
1.2306 +val NSDERIV_cmult_Id = thm "NSDERIV_cmult_Id";
1.2307 +val DERIV_pow = thm "DERIV_pow";
1.2308 +val NSDERIV_pow = thm "NSDERIV_pow";
1.2309 +val NSDERIV_inverse = thm "NSDERIV_inverse";
1.2310 +val DERIV_inverse = thm "DERIV_inverse";
1.2311 +val DERIV_inverse_fun = thm "DERIV_inverse_fun";
1.2312 +val NSDERIV_inverse_fun = thm "NSDERIV_inverse_fun";
1.2313 +val DERIV_quotient = thm "DERIV_quotient";
1.2314 +val NSDERIV_quotient = thm "NSDERIV_quotient";
1.2315 +val CARAT_DERIV = thm "CARAT_DERIV";
1.2316 +val CARAT_NSDERIV = thm "CARAT_NSDERIV";
1.2317 +val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3";
1.2318 +val starfun_if_eq = thm "starfun_if_eq";
1.2319 +val CARAT_DERIVD = thm "CARAT_DERIVD";
1.2320 +val f_inc_g_dec_Beq_f = thm "f_inc_g_dec_Beq_f";
1.2321 +val f_inc_g_dec_Beq_g = thm "f_inc_g_dec_Beq_g";
1.2322 +val f_inc_imp_le_lim = thm "f_inc_imp_le_lim";
1.2323 +val lim_uminus = thm "lim_uminus";
1.2324 +val g_dec_imp_lim_le = thm "g_dec_imp_lim_le";
1.2325 +val Bolzano_bisect_le = thm "Bolzano_bisect_le";
1.2326 +val Bolzano_bisect_fst_le_Suc = thm "Bolzano_bisect_fst_le_Suc";
1.2327 +val Bolzano_bisect_Suc_le_snd = thm "Bolzano_bisect_Suc_le_snd";
1.2328 +val eq_divide_2_times_iff = thm "eq_divide_2_times_iff";
1.2329 +val Bolzano_bisect_diff = thm "Bolzano_bisect_diff";
1.2330 +val Bolzano_nest_unique = thms "Bolzano_nest_unique";
1.2331 +val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
1.2332 +val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
1.2333 +val lemma_BOLZANO2 = thm "lemma_BOLZANO2";
1.2334 +val IVT = thm "IVT";
1.2335 +val IVT2 = thm "IVT2";
1.2336 +val IVT_objl = thm "IVT_objl";
1.2337 +val IVT2_objl = thm "IVT2_objl";
1.2338 +val isCont_bounded = thm "isCont_bounded";
1.2339 +val isCont_has_Ub = thm "isCont_has_Ub";
1.2340 +val isCont_eq_Ub = thm "isCont_eq_Ub";
1.2341 +val isCont_eq_Lb = thm "isCont_eq_Lb";
1.2342 +val isCont_Lb_Ub = thm "isCont_Lb_Ub";
1.2343 +val DERIV_left_inc = thm "DERIV_left_inc";
1.2344 +val DERIV_left_dec = thm "DERIV_left_dec";
1.2345 +val DERIV_local_max = thm "DERIV_local_max";
1.2346 +val DERIV_local_min = thm "DERIV_local_min";
1.2347 +val DERIV_local_const = thm "DERIV_local_const";
1.2348 +val Rolle = thm "Rolle";
1.2349 +val MVT = thm "MVT";
1.2350 +val DERIV_isconst_end = thm "DERIV_isconst_end";
1.2351 +val DERIV_isconst1 = thm "DERIV_isconst1";
1.2352 +val DERIV_isconst2 = thm "DERIV_isconst2";
1.2353 +val DERIV_isconst_all = thm "DERIV_isconst_all";
1.2354 +val DERIV_const_ratio_const = thm "DERIV_const_ratio_const";
1.2355 +val DERIV_const_ratio_const2 = thm "DERIV_const_ratio_const2";
1.2356 +val real_average_minus_first = thm "real_average_minus_first";
1.2357 +val real_average_minus_second = thm "real_average_minus_second";
1.2358 +val DERIV_const_average = thm "DERIV_const_average";
1.2359 +val isCont_inj_range = thm "isCont_inj_range";
1.2360 +val isCont_inverse_function = thm "isCont_inverse_function";
1.2361 +*}
1.2362 +
1.2363
1.2364  end
1.2365
```