# HG changeset patch
# User huffman
# Date 1163704790 -3600
# Node ID 700ae58d2273106a7ef22eca483700ccd12c0c73
# Parent  11996e938dfe5759e9fec6084ce35e7716a4436d
add lemmas LIM_zero_iff, LIM_norm_zero_iff

diff -r 11996e938dfe -r 700ae58d2273 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Nov 16 17:06:24 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Nov 16 20:19:50 2006 +0100
@@ -133,6 +133,9 @@
 lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
 by (simp add: LIM_def)
 
+lemma LIM_zero_iff: "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
+by (simp add: LIM_def)
+
 lemma LIM_imp_LIM:
   assumes f: "f -- a --> l"
   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
@@ -152,6 +155,9 @@
 lemma LIM_norm_zero_cancel: "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
 by (erule LIM_imp_LIM, simp)
 
+lemma LIM_norm_zero_iff: "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
+by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero])
+
 lemma LIM_const_not_eq:
   fixes a :: "'a::real_normed_div_algebra"
   shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
@@ -216,7 +222,7 @@
 
 lemma LIM_cong:
   "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
-   \<Longrightarrow> (f -- a --> l) = (g -- b --> m)"
+   \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
 by (simp add: LIM_def)
 
 lemma LIM_equal2: