convert to Isar-style proof
authorhuffman
Wed Aug 31 07:51:55 2011 -0700 (2011-08-31)
changeset 44627134c06282ae6
parent 44626 a40b713232c8
child 44628 bd17b7543af1
convert to Isar-style proof
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Limits.thy	Wed Aug 31 13:22:50 2011 +0200
     1.2 +++ b/src/HOL/Limits.thy	Wed Aug 31 07:51:55 2011 -0700
     1.3 @@ -916,21 +916,6 @@
     1.4    thus ?thesis by (rule BfunI)
     1.5  qed
     1.6  
     1.7 -lemma tendsto_inverse_lemma:
     1.8 -  fixes a :: "'a::real_normed_div_algebra"
     1.9 -  shows "\<lbrakk>(f ---> a) F; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) F\<rbrakk>
    1.10 -         \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) F"
    1.11 -  apply (subst tendsto_Zfun_iff)
    1.12 -  apply (rule Zfun_ssubst)
    1.13 -  apply (erule eventually_elim1)
    1.14 -  apply (erule (1) inverse_diff_inverse)
    1.15 -  apply (rule Zfun_minus)
    1.16 -  apply (rule Zfun_mult_left)
    1.17 -  apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
    1.18 -  apply (erule (1) Bfun_inverse)
    1.19 -  apply (simp add: tendsto_Zfun_iff)
    1.20 -  done
    1.21 -
    1.22  lemma tendsto_inverse [tendsto_intros]:
    1.23    fixes a :: "'a::real_normed_div_algebra"
    1.24    assumes f: "(f ---> a) F"
    1.25 @@ -942,8 +927,15 @@
    1.26      by (rule tendstoD)
    1.27    then have "eventually (\<lambda>x. f x \<noteq> 0) F"
    1.28      unfolding dist_norm by (auto elim!: eventually_elim1)
    1.29 -  with f a show ?thesis
    1.30 -    by (rule tendsto_inverse_lemma)
    1.31 +  with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
    1.32 +    - (inverse (f x) * (f x - a) * inverse a)) F"
    1.33 +    by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
    1.34 +  moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
    1.35 +    by (intro Zfun_minus Zfun_mult_left
    1.36 +      bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
    1.37 +      Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
    1.38 +  ultimately show ?thesis
    1.39 +    unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
    1.40  qed
    1.41  
    1.42  lemma tendsto_divide [tendsto_intros]: