src/HOL/Lim.thy
changeset 31355 3d18766ddc4b
parent 31353 14a58e2ca374
child 31392 69570155ddf8
     1.1 --- a/src/HOL/Lim.thy	Mon Jun 01 08:04:19 2009 -0700
     1.2 +++ b/src/HOL/Lim.thy	Mon Jun 01 10:36:42 2009 -0700
     1.3 @@ -413,67 +413,16 @@
     1.4  
     1.5  subsubsection {* Derived theorems about @{term LIM} *}
     1.6  
     1.7 -lemma LIM_inverse_lemma:
     1.8 -  fixes x :: "'a::real_normed_div_algebra"
     1.9 -  assumes r: "0 < r"
    1.10 -  assumes x: "norm (x - 1) < min (1/2) (r/2)"
    1.11 -  shows "norm (inverse x - 1) < r"
    1.12 -proof -
    1.13 -  from r have r2: "0 < r/2" by simp
    1.14 -  from x have 0: "x \<noteq> 0" by clarsimp
    1.15 -  from x have x': "norm (1 - x) < min (1/2) (r/2)"
    1.16 -    by (simp only: norm_minus_commute)
    1.17 -  hence less1: "norm (1 - x) < r/2" by simp
    1.18 -  have "norm (1::'a) - norm x \<le> norm (1 - x)" by (rule norm_triangle_ineq2)
    1.19 -  also from x' have "norm (1 - x) < 1/2" by simp
    1.20 -  finally have "1/2 < norm x" by simp
    1.21 -  hence "inverse (norm x) < inverse (1/2)"
    1.22 -    by (rule less_imp_inverse_less, simp)
    1.23 -  hence less2: "norm (inverse x) < 2"
    1.24 -    by (simp add: nonzero_norm_inverse 0)
    1.25 -  from less1 less2 r2 norm_ge_zero
    1.26 -  have "norm (1 - x) * norm (inverse x) < (r/2) * 2"
    1.27 -    by (rule mult_strict_mono)
    1.28 -  thus "norm (inverse x - 1) < r"
    1.29 -    by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0)
    1.30 -qed
    1.31 +lemma LIM_inverse:
    1.32 +  fixes L :: "'a::real_normed_div_algebra"
    1.33 +  shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
    1.34 +unfolding LIM_conv_tendsto
    1.35 +by (rule tendsto_inverse)
    1.36  
    1.37  lemma LIM_inverse_fun:
    1.38    assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
    1.39    shows "inverse -- a --> inverse a"
    1.40 -proof (rule LIM_equal2)
    1.41 -  from a show "0 < norm a" by simp
    1.42 -next
    1.43 -  fix x assume "norm (x - a) < norm a"
    1.44 -  hence "x \<noteq> 0" by auto
    1.45 -  with a show "inverse x = inverse (inverse a * x) * inverse a"
    1.46 -    by (simp add: nonzero_inverse_mult_distrib
    1.47 -                  nonzero_imp_inverse_nonzero
    1.48 -                  nonzero_inverse_inverse_eq mult_assoc)
    1.49 -next
    1.50 -  have 1: "inverse -- 1 --> inverse (1::'a)"
    1.51 -    apply (rule LIM_I)
    1.52 -    apply (rule_tac x="min (1/2) (r/2)" in exI)
    1.53 -    apply (simp add: LIM_inverse_lemma)
    1.54 -    done
    1.55 -  have "(\<lambda>x. inverse a * x) -- a --> inverse a * a"
    1.56 -    by (intro LIM_mult LIM_ident LIM_const)
    1.57 -  hence "(\<lambda>x. inverse a * x) -- a --> 1"
    1.58 -    by (simp add: a)
    1.59 -  with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1"
    1.60 -    by (rule LIM_compose)
    1.61 -  hence "(\<lambda>x. inverse (inverse a * x)) -- a --> 1"
    1.62 -    by simp
    1.63 -  hence "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> 1 * inverse a"
    1.64 -    by (intro LIM_mult LIM_const)
    1.65 -  thus "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> inverse a"
    1.66 -    by simp
    1.67 -qed
    1.68 -
    1.69 -lemma LIM_inverse:
    1.70 -  fixes L :: "'a::real_normed_div_algebra"
    1.71 -  shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
    1.72 -by (rule LIM_inverse_fun [THEN LIM_compose])
    1.73 +by (rule LIM_inverse [OF LIM_ident a])
    1.74  
    1.75  lemma LIM_sgn:
    1.76    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"