author huffman Wed, 31 Aug 2011 07:51:55 -0700 changeset 44627 134c06282ae6 parent 44626 a40b713232c8 child 44628 bd17b7543af1
convert to Isar-style proof
 src/HOL/Limits.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Limits.thy	Wed Aug 31 13:22:50 2011 +0200
+++ b/src/HOL/Limits.thy	Wed Aug 31 07:51:55 2011 -0700
@@ -916,21 +916,6 @@
thus ?thesis by (rule BfunI)
qed

-lemma tendsto_inverse_lemma:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "\<lbrakk>(f ---> a) F; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) F\<rbrakk>
-         \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) F"
-  apply (subst tendsto_Zfun_iff)
-  apply (rule Zfun_ssubst)
-  apply (erule eventually_elim1)
-  apply (erule (1) inverse_diff_inverse)
-  apply (rule Zfun_minus)
-  apply (rule Zfun_mult_left)
-  apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult])
-  apply (erule (1) Bfun_inverse)
-  done
-
lemma tendsto_inverse [tendsto_intros]:
fixes a :: "'a::real_normed_div_algebra"
assumes f: "(f ---> a) F"
@@ -942,8 +927,15 @@
by (rule tendstoD)
then have "eventually (\<lambda>x. f x \<noteq> 0) F"
unfolding dist_norm by (auto elim!: eventually_elim1)
-  with f a show ?thesis
-    by (rule tendsto_inverse_lemma)
+  with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
+    - (inverse (f x) * (f x - a) * inverse a)) F"
+    by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
+  moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
+    by (intro Zfun_minus Zfun_mult_left
+      bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
+      Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
+  ultimately show ?thesis
+    unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
qed

lemma tendsto_divide [tendsto_intros]:```