# HG changeset patch
# User huffman
# Date 1230135405 28800
# Node ID c23b2d1086121578ac56ca32b359ae86b8b50a8d
# Parent  562f95f06244ec04a3009a8bcea1e5c085f7a351
move theorems about limits from Transcendental.thy to Deriv.thy

diff -r 562f95f06244 -r c23b2d108612 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Dec 24 08:06:27 2008 -0800
+++ b/src/HOL/Deriv.thy	Wed Dec 24 08:16:45 2008 -0800
@@ -1722,4 +1722,60 @@
 apply (simp add: poly_entire del: pmult_Cons)
 done
 
+
+subsection {* Theorems about Limits *}
+
+(* need to rename second isCont_inverse *)
+
+lemma isCont_inv_fun:
+  fixes f g :: "real \<Rightarrow> real"
+  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
+         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
+      ==> isCont g (f x)"
+by (rule isCont_inverse_function)
+
+lemma isCont_inv_fun_inv:
+  fixes f g :: "real \<Rightarrow> real"
+  shows "[| 0 < d;  
+         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
+         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
+       ==> \<exists>e. 0 < e &  
+             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
+apply (drule isCont_inj_range)
+prefer 2 apply (assumption, assumption, auto)
+apply (rule_tac x = e in exI, auto)
+apply (rotate_tac 2)
+apply (drule_tac x = y in spec, auto)
+done
+
+
+text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
+lemma LIM_fun_gt_zero:
+     "[| f -- c --> (l::real); 0 < l |]  
+         ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
+apply (auto simp add: LIM_def)
+apply (drule_tac x = "l/2" in spec, safe, force)
+apply (rule_tac x = s in exI)
+apply (auto simp only: abs_less_iff)
+done
+
+lemma LIM_fun_less_zero:
+     "[| f -- c --> (l::real); l < 0 |]  
+      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
+apply (auto simp add: LIM_def)
+apply (drule_tac x = "-l/2" in spec, safe, force)
+apply (rule_tac x = s in exI)
+apply (auto simp only: abs_less_iff)
+done
+
+
+lemma LIM_fun_not_zero:
+     "[| f -- c --> (l::real); l \<noteq> 0 |] 
+      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
+apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
+apply (drule LIM_fun_less_zero)
+apply (drule_tac [3] LIM_fun_gt_zero)
+apply force+
+done
+
 end
diff -r 562f95f06244 -r c23b2d108612 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Dec 24 08:06:27 2008 -0800
+++ b/src/HOL/Transcendental.thy	Wed Dec 24 08:16:45 2008 -0800
@@ -2163,60 +2163,4 @@
 apply (erule polar_ex2)
 done
 
-
-subsection {* Theorems about Limits *}
-
-(* need to rename second isCont_inverse *)
-
-lemma isCont_inv_fun:
-  fixes f g :: "real \<Rightarrow> real"
-  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
-      ==> isCont g (f x)"
-by (rule isCont_inverse_function)
-
-lemma isCont_inv_fun_inv:
-  fixes f g :: "real \<Rightarrow> real"
-  shows "[| 0 < d;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
-       ==> \<exists>e. 0 < e &  
-             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
-apply (drule isCont_inj_range)
-prefer 2 apply (assumption, assumption, auto)
-apply (rule_tac x = e in exI, auto)
-apply (rotate_tac 2)
-apply (drule_tac x = y in spec, auto)
-done
-
-
-text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
-lemma LIM_fun_gt_zero:
-     "[| f -- c --> (l::real); 0 < l |]  
-         ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
-apply (auto simp add: LIM_def)
-apply (drule_tac x = "l/2" in spec, safe, force)
-apply (rule_tac x = s in exI)
-apply (auto simp only: abs_less_iff)
-done
-
-lemma LIM_fun_less_zero:
-     "[| f -- c --> (l::real); l < 0 |]  
-      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
-apply (auto simp add: LIM_def)
-apply (drule_tac x = "-l/2" in spec, safe, force)
-apply (rule_tac x = s in exI)
-apply (auto simp only: abs_less_iff)
-done
-
-
-lemma LIM_fun_not_zero:
-     "[| f -- c --> (l::real); l \<noteq> 0 |] 
-      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
-apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
-apply (drule LIM_fun_less_zero)
-apply (drule_tac [3] LIM_fun_gt_zero)
-apply force+
-done
-  
 end