move theorems about limits from Transcendental.thy to Deriv.thy
authorhuffman
Wed Dec 24 08:16:45 2008 -0800 (2008-12-24)
changeset 29166c23b2d108612
parent 29165 562f95f06244
child 29167 37a952bb9ebc
move theorems about limits from Transcendental.thy to Deriv.thy
src/HOL/Deriv.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Deriv.thy	Wed Dec 24 08:06:27 2008 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Wed Dec 24 08:16:45 2008 -0800
     1.3 @@ -1722,4 +1722,60 @@
     1.4  apply (simp add: poly_entire del: pmult_Cons)
     1.5  done
     1.6  
     1.7 +
     1.8 +subsection {* Theorems about Limits *}
     1.9 +
    1.10 +(* need to rename second isCont_inverse *)
    1.11 +
    1.12 +lemma isCont_inv_fun:
    1.13 +  fixes f g :: "real \<Rightarrow> real"
    1.14 +  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
    1.15 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
    1.16 +      ==> isCont g (f x)"
    1.17 +by (rule isCont_inverse_function)
    1.18 +
    1.19 +lemma isCont_inv_fun_inv:
    1.20 +  fixes f g :: "real \<Rightarrow> real"
    1.21 +  shows "[| 0 < d;  
    1.22 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
    1.23 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
    1.24 +       ==> \<exists>e. 0 < e &  
    1.25 +             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
    1.26 +apply (drule isCont_inj_range)
    1.27 +prefer 2 apply (assumption, assumption, auto)
    1.28 +apply (rule_tac x = e in exI, auto)
    1.29 +apply (rotate_tac 2)
    1.30 +apply (drule_tac x = y in spec, auto)
    1.31 +done
    1.32 +
    1.33 +
    1.34 +text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
    1.35 +lemma LIM_fun_gt_zero:
    1.36 +     "[| f -- c --> (l::real); 0 < l |]  
    1.37 +         ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
    1.38 +apply (auto simp add: LIM_def)
    1.39 +apply (drule_tac x = "l/2" in spec, safe, force)
    1.40 +apply (rule_tac x = s in exI)
    1.41 +apply (auto simp only: abs_less_iff)
    1.42 +done
    1.43 +
    1.44 +lemma LIM_fun_less_zero:
    1.45 +     "[| f -- c --> (l::real); l < 0 |]  
    1.46 +      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
    1.47 +apply (auto simp add: LIM_def)
    1.48 +apply (drule_tac x = "-l/2" in spec, safe, force)
    1.49 +apply (rule_tac x = s in exI)
    1.50 +apply (auto simp only: abs_less_iff)
    1.51 +done
    1.52 +
    1.53 +
    1.54 +lemma LIM_fun_not_zero:
    1.55 +     "[| f -- c --> (l::real); l \<noteq> 0 |] 
    1.56 +      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
    1.57 +apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
    1.58 +apply (drule LIM_fun_less_zero)
    1.59 +apply (drule_tac [3] LIM_fun_gt_zero)
    1.60 +apply force+
    1.61 +done
    1.62 +
    1.63  end
     2.1 --- a/src/HOL/Transcendental.thy	Wed Dec 24 08:06:27 2008 -0800
     2.2 +++ b/src/HOL/Transcendental.thy	Wed Dec 24 08:16:45 2008 -0800
     2.3 @@ -2163,60 +2163,4 @@
     2.4  apply (erule polar_ex2)
     2.5  done
     2.6  
     2.7 -
     2.8 -subsection {* Theorems about Limits *}
     2.9 -
    2.10 -(* need to rename second isCont_inverse *)
    2.11 -
    2.12 -lemma isCont_inv_fun:
    2.13 -  fixes f g :: "real \<Rightarrow> real"
    2.14 -  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
    2.15 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
    2.16 -      ==> isCont g (f x)"
    2.17 -by (rule isCont_inverse_function)
    2.18 -
    2.19 -lemma isCont_inv_fun_inv:
    2.20 -  fixes f g :: "real \<Rightarrow> real"
    2.21 -  shows "[| 0 < d;  
    2.22 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
    2.23 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
    2.24 -       ==> \<exists>e. 0 < e &  
    2.25 -             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
    2.26 -apply (drule isCont_inj_range)
    2.27 -prefer 2 apply (assumption, assumption, auto)
    2.28 -apply (rule_tac x = e in exI, auto)
    2.29 -apply (rotate_tac 2)
    2.30 -apply (drule_tac x = y in spec, auto)
    2.31 -done
    2.32 -
    2.33 -
    2.34 -text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
    2.35 -lemma LIM_fun_gt_zero:
    2.36 -     "[| f -- c --> (l::real); 0 < l |]  
    2.37 -         ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
    2.38 -apply (auto simp add: LIM_def)
    2.39 -apply (drule_tac x = "l/2" in spec, safe, force)
    2.40 -apply (rule_tac x = s in exI)
    2.41 -apply (auto simp only: abs_less_iff)
    2.42 -done
    2.43 -
    2.44 -lemma LIM_fun_less_zero:
    2.45 -     "[| f -- c --> (l::real); l < 0 |]  
    2.46 -      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
    2.47 -apply (auto simp add: LIM_def)
    2.48 -apply (drule_tac x = "-l/2" in spec, safe, force)
    2.49 -apply (rule_tac x = s in exI)
    2.50 -apply (auto simp only: abs_less_iff)
    2.51 -done
    2.52 -
    2.53 -
    2.54 -lemma LIM_fun_not_zero:
    2.55 -     "[| f -- c --> (l::real); l \<noteq> 0 |] 
    2.56 -      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
    2.57 -apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
    2.58 -apply (drule LIM_fun_less_zero)
    2.59 -apply (drule_tac [3] LIM_fun_gt_zero)
    2.60 -apply force+
    2.61 -done
    2.62 -  
    2.63  end