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.10  apply (auto simp add: add_commute)
    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)"