# HG changeset patch
# User huffman
# Date 1234499801 28800
# Node ID 379e43e513c21e3ee8967161603d646e86fd3de2
# Parent  74c183927054d1625735e503ee7a202f7ab162de
add lemmas about sgn

diff -r 74c183927054 -r 379e43e513c2 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Fri Feb 13 08:00:46 2009 +1100
+++ b/src/HOL/Lim.thy	Thu Feb 12 20:36:41 2009 -0800
@@ -452,6 +452,11 @@
   shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
 by (rule LIM_inverse_fun [THEN LIM_compose])
 
+lemma LIM_sgn:
+  "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
+unfolding sgn_div_norm
+by (simp add: LIM_scaleR LIM_inverse LIM_norm)
+
 
 subsection {* Continuity *}
 
@@ -529,6 +534,10 @@
   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   unfolding isCont_def by (rule LIM_power)
 
+lemma isCont_sgn:
+  "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
+  unfolding isCont_def by (rule LIM_sgn)
+
 lemma isCont_abs [simp]: "isCont abs (a::real)"
 by (rule isCont_rabs [OF isCont_ident])