# HG changeset patch
# User huffman
# Date 1163027956 -3600
# Node ID b7f090c5057de1f25ee398efd5ea4c117627dd03
# Parent  47195501ecf7054b2a7278d8608610d81443c3aa
added LIM_norm and related lemmas

diff -r 47195501ecf7 -r b7f090c5057d src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Wed Nov 08 23:11:13 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Nov 09 00:19:16 2006 +0100
@@ -107,6 +107,10 @@
   qed
 qed
 
+lemma LIM_add_zero:
+  "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
+by (drule (1) LIM_add, simp)
+
 lemma minus_diff_minus:
   fixes a b :: "'a::ab_group_add"
   shows "(- a) - (- b) = - (a - b)"
@@ -129,6 +133,25 @@
 lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> 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)"
+  shows "g -- a --> m"
+apply (rule LIM_I, drule LIM_D [OF f], safe)
+apply (rule_tac x="s" in exI, safe)
+apply (drule_tac x="x" in spec, safe)
+apply (erule (1) order_le_less_trans [OF le])
+done
+
+lemma LIM_norm: "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
+by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3)
+
+lemma LIM_norm_zero: "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
+by (drule LIM_norm, simp)
+
+lemma LIM_norm_zero_cancel: "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
+by (erule LIM_imp_LIM, simp)
+
 lemma LIM_const_not_eq:
   fixes a :: "'a::real_normed_div_algebra"
   shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"