# HG changeset patch
# User huffman
# Date 1179623930 -7200
# Node ID d329182b59660db453f0f779e12b4e3b7a1f9fef
# Parent  761f37e0ccc5095723e18625623006cd8deab039
add lemmas LIM_compose2, isCont_LIM_compose2

diff -r 761f37e0ccc5 -r d329182b5966 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Sat May 19 19:35:31 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sun May 20 03:18:50 2007 +0200
@@ -238,6 +238,37 @@
   qed
 qed
 
+lemma LIM_compose2:
+  assumes f: "f -- a --> b"
+  assumes g: "g -- b --> c"
+  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
+  shows "(\<lambda>x. g (f x)) -- a --> c"
+proof (rule LIM_I)
+  fix r :: real
+  assume r: "0 < r"
+  obtain s where s: "0 < s"
+    and less_r: "\<And>y. \<lbrakk>y \<noteq> b; norm (y - b) < s\<rbrakk> \<Longrightarrow> norm (g y - c) < r"
+    using LIM_D [OF g r] by fast
+  obtain t where t: "0 < t"
+    and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - b) < s"
+    using LIM_D [OF f s] by fast
+  obtain d where d: "0 < d"
+    and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
+    using inj by fast
+
+  show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - c) < r"
+  proof (safe intro!: exI)
+    show "0 < min d t" using d t by simp
+  next
+    fix x
+    assume "x \<noteq> a" and "norm (x - a) < min d t"
+    hence "f x \<noteq> b" and "norm (f x - b) < s"
+      using neq_b less_s by simp_all
+    thus "norm (g (f x) - c) < r"
+      by (rule less_r)
+  qed
+qed
+
 lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
 unfolding o_def by (rule LIM_compose)
 
@@ -468,6 +499,13 @@
   "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
   unfolding isCont_def by (rule LIM_compose)
 
+lemma isCont_LIM_compose2:
+  assumes f [unfolded isCont_def]: "isCont f a"
+  assumes g: "g -- f a --> l"
+  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
+  shows "(\<lambda>x. g (f x)) -- a --> l"
+by (rule LIM_compose2 [OF f g inj])
+
 lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
   unfolding isCont_def by (rule LIM_compose)