src/HOL/Hyperreal/Lim.thy
 changeset 15003 6145dd7538d7 parent 14477 cc61fd03e589 child 15077 89840837108e
```     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Thu Jun 24 17:51:28 2004 +0200
1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Thu Jun 24 17:52:02 2004 +0200
1.3 @@ -1328,7 +1328,7 @@
1.4  apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
1.5  apply (subgoal_tac "lim f \<le> f (no + n) ")
1.6  apply (induct_tac [2] "no")
1.7 -apply (auto intro: order_trans simp add: diff_minus real_abs_def)
1.8 +apply (auto intro: order_trans simp add: diff_minus abs_if)
1.9  apply (drule_tac no=no and m=n in lemma_f_mono_add)
1.11  done
1.12 @@ -1660,22 +1660,38 @@
1.13  apply (rule_tac [4] x = xb in exI, simp_all)
1.14  done
1.15
1.16 -(*----------------------------------------------------------------------------*)
1.17 -(* If f'(x) > 0 then x is locally strictly increasing at the right            *)
1.18 -(*----------------------------------------------------------------------------*)
1.19 +
1.20 +subsection{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
1.21
1.22  lemma DERIV_left_inc:
1.23 -    "[| DERIV f x :> l;  0 < l |]
1.24 -     ==> \<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
1.25 -apply (simp add: deriv_def LIM_def)
1.26 -apply (drule spec, auto)
1.27 -apply (rule_tac x = s in exI, auto)
1.28 -apply (subgoal_tac "0 < l*h")
1.29 - prefer 2 apply (simp add: zero_less_mult_iff)
1.30 -apply (drule_tac x = h in spec)
1.31 -apply (simp add: real_abs_def pos_le_divide_eq pos_less_divide_eq
1.32 -            split add: split_if_asm)
1.33 -done
1.34 +  assumes der: "DERIV f x :> l"
1.35 +      and l:   "0 < l"
1.36 +  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
1.37 +proof -
1.38 +  from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
1.39 +  have "\<exists>s. 0 < s \<and>
1.40 +              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
1.41 +    by (simp add: diff_minus)
1.42 +  then obtain s
1.43 +        where s:   "0 < s"
1.44 +          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
1.45 +    by auto
1.46 +  thus ?thesis
1.47 +  proof (intro exI conjI strip)
1.48 +    show "0<s" .
1.49 +    fix h::real
1.50 +    assume "0 < h \<and> h < s"
1.51 +    with all [of h] show "f x < f (x+h)"
1.52 +    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
1.53 +		split add: split_if_asm)
1.54 +      assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
1.55 +      with l
1.56 +      have "0 < (f (x+h) - f x) / h" by arith
1.57 +      thus "f x < f (x+h)"
1.58 +	by (simp add: pos_less_divide_eq h)
1.59 +    qed
1.60 +  qed
1.61 +qed
1.62
1.63  lemma DERIV_left_dec:
1.64    assumes der: "DERIV f x :> l"
1.65 @@ -1696,9 +1712,9 @@
1.66      fix h::real
1.67      assume "0 < h \<and> h < s"
1.68      with all [of "-h"] show "f x < f (x-h)"
1.69 -    proof (simp add: real_abs_def pos_less_divide_eq diff_minus [symmetric]
1.70 +    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
1.71  		split add: split_if_asm)
1.72 -      assume "~ l \<le> - ((f (x-h) - f x) / h)" and h: "0 < h"
1.73 +      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
1.74        with l
1.75        have "0 < (f (x-h) - f x) / h" by arith
1.76        thus "f x < f (x-h)"
```