move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
authorhoelzl
Tue Mar 26 12:21:00 2013 +0100 (2013-03-26)
changeset 515292d2f59e6055a
parent 51528 66c3a7589de7
child 51530 609914f0934a
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
src/HOL/Deriv.thy
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Mar 26 12:20:59 2013 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Tue Mar 26 12:21:00 2013 +0100
     1.3 @@ -422,178 +422,6 @@
     1.4    apply (simp add: assms)
     1.5    done
     1.6  
     1.7 -
     1.8 -subsection {* Nested Intervals and Bisection *}
     1.9 -
    1.10 -lemma nested_sequence_unique:
    1.11 -  assumes "\<forall>n. f n \<le> f (Suc n)" "\<forall>n. g (Suc n) \<le> g n" "\<forall>n. f n \<le> g n" "(\<lambda>n. f n - g n) ----> 0"
    1.12 -  shows "\<exists>l::real. ((\<forall>n. f n \<le> l) \<and> f ----> l) \<and> ((\<forall>n. l \<le> g n) \<and> g ----> l)"
    1.13 -proof -
    1.14 -  have "incseq f" unfolding incseq_Suc_iff by fact
    1.15 -  have "decseq g" unfolding decseq_Suc_iff by fact
    1.16 -
    1.17 -  { fix n
    1.18 -    from `decseq g` have "g n \<le> g 0" by (rule decseqD) simp
    1.19 -    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f n \<le> g 0" by auto }
    1.20 -  then obtain u where "f ----> u" "\<forall>i. f i \<le> u"
    1.21 -    using incseq_convergent[OF `incseq f`] by auto
    1.22 -  moreover
    1.23 -  { fix n
    1.24 -    from `incseq f` have "f 0 \<le> f n" by (rule incseqD) simp
    1.25 -    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f 0 \<le> g n" by simp }
    1.26 -  then obtain l where "g ----> l" "\<forall>i. l \<le> g i"
    1.27 -    using decseq_convergent[OF `decseq g`] by auto
    1.28 -  moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]]
    1.29 -  ultimately show ?thesis by auto
    1.30 -qed
    1.31 -
    1.32 -lemma Bolzano[consumes 1, case_names trans local]:
    1.33 -  fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
    1.34 -  assumes [arith]: "a \<le> b"
    1.35 -  assumes trans: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
    1.36 -  assumes local: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<exists>d>0. \<forall>a b. a \<le> x \<and> x \<le> b \<and> b - a < d \<longrightarrow> P a b"
    1.37 -  shows "P a b"
    1.38 -proof -
    1.39 -  def bisect \<equiv> "nat_rec (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))"
    1.40 -  def l \<equiv> "\<lambda>n. fst (bisect n)" and u \<equiv> "\<lambda>n. snd (bisect n)"
    1.41 -  have l[simp]: "l 0 = a" "\<And>n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)"
    1.42 -    and u[simp]: "u 0 = b" "\<And>n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)"
    1.43 -    by (simp_all add: l_def u_def bisect_def split: prod.split)
    1.44 -
    1.45 -  { fix n have "l n \<le> u n" by (induct n) auto } note this[simp]
    1.46 -
    1.47 -  have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l ----> x) \<and> ((\<forall>n. x \<le> u n) \<and> u ----> x)"
    1.48 -  proof (safe intro!: nested_sequence_unique)
    1.49 -    fix n show "l n \<le> l (Suc n)" "u (Suc n) \<le> u n" by (induct n) auto
    1.50 -  next
    1.51 -    { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) }
    1.52 -    then show "(\<lambda>n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero)
    1.53 -  qed fact
    1.54 -  then obtain x where x: "\<And>n. l n \<le> x" "\<And>n. x \<le> u n" and "l ----> x" "u ----> x" by auto
    1.55 -  obtain d where "0 < d" and d: "\<And>a b. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> b - a < d \<Longrightarrow> P a b"
    1.56 -    using `l 0 \<le> x` `x \<le> u 0` local[of x] by auto
    1.57 -
    1.58 -  show "P a b"
    1.59 -  proof (rule ccontr)
    1.60 -    assume "\<not> P a b" 
    1.61 -    { fix n have "\<not> P (l n) (u n)"
    1.62 -      proof (induct n)
    1.63 -        case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto
    1.64 -      qed (simp add: `\<not> P a b`) }
    1.65 -    moreover
    1.66 -    { have "eventually (\<lambda>n. x - d / 2 < l n) sequentially"
    1.67 -        using `0 < d` `l ----> x` by (intro order_tendstoD[of _ x]) auto
    1.68 -      moreover have "eventually (\<lambda>n. u n < x + d / 2) sequentially"
    1.69 -        using `0 < d` `u ----> x` by (intro order_tendstoD[of _ x]) auto
    1.70 -      ultimately have "eventually (\<lambda>n. P (l n) (u n)) sequentially"
    1.71 -      proof eventually_elim
    1.72 -        fix n assume "x - d / 2 < l n" "u n < x + d / 2"
    1.73 -        from add_strict_mono[OF this] have "u n - l n < d" by simp
    1.74 -        with x show "P (l n) (u n)" by (rule d)
    1.75 -      qed }
    1.76 -    ultimately show False by simp
    1.77 -  qed
    1.78 -qed
    1.79 -
    1.80 -(*HOL style here: object-level formulations*)
    1.81 -lemma IVT_objl: "(f(a::real) \<le> (y::real) & y \<le> f(b) & a \<le> b &
    1.82 -      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
    1.83 -      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
    1.84 -apply (blast intro: IVT)
    1.85 -done
    1.86 -
    1.87 -lemma IVT2_objl: "(f(b::real) \<le> (y::real) & y \<le> f(a) & a \<le> b &
    1.88 -      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
    1.89 -      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
    1.90 -apply (blast intro: IVT2)
    1.91 -done
    1.92 -
    1.93 -
    1.94 -lemma compact_Icc[simp, intro]: "compact {a .. b::real}"
    1.95 -proof (cases "a \<le> b", rule compactI)
    1.96 -  fix C assume C: "a \<le> b" "\<forall>t\<in>C. open t" "{a..b} \<subseteq> \<Union>C"
    1.97 -  def T == "{a .. b}"
    1.98 -  from C(1,3) show "\<exists>C'\<subseteq>C. finite C' \<and> {a..b} \<subseteq> \<Union>C'"
    1.99 -  proof (induct rule: Bolzano)
   1.100 -    case (trans a b c)
   1.101 -    then have *: "{a .. c} = {a .. b} \<union> {b .. c}" by auto
   1.102 -    from trans obtain C1 C2 where "C1\<subseteq>C \<and> finite C1 \<and> {a..b} \<subseteq> \<Union>C1" "C2\<subseteq>C \<and> finite C2 \<and> {b..c} \<subseteq> \<Union>C2"
   1.103 -      by (auto simp: *)
   1.104 -    with trans show ?case
   1.105 -      unfolding * by (intro exI[of _ "C1 \<union> C2"]) auto
   1.106 -  next
   1.107 -    case (local x)
   1.108 -    then have "x \<in> \<Union>C" using C by auto
   1.109 -    with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
   1.110 -    then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
   1.111 -      by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
   1.112 -    with `c \<in> C` show ?case
   1.113 -      by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
   1.114 -  qed
   1.115 -qed simp
   1.116 -
   1.117 -subsection {* Boundedness of continuous functions *}
   1.118 -
   1.119 -text{*By bisection, function continuous on closed interval is bounded above*}
   1.120 -
   1.121 -lemma isCont_eq_Ub:
   1.122 -  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   1.123 -  shows "a \<le> b \<Longrightarrow> \<forall>x::real. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
   1.124 -    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
   1.125 -  using continuous_attains_sup[of "{a .. b}" f]
   1.126 -  apply (simp add: continuous_at_imp_continuous_on Ball_def)
   1.127 -  apply safe
   1.128 -  apply (rule_tac x="f x" in exI)
   1.129 -  apply auto
   1.130 -  done
   1.131 -
   1.132 -lemma isCont_eq_Lb:
   1.133 -  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   1.134 -  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
   1.135 -    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> M \<le> f x) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
   1.136 -  using continuous_attains_inf[of "{a .. b}" f]
   1.137 -  apply (simp add: continuous_at_imp_continuous_on Ball_def)
   1.138 -  apply safe
   1.139 -  apply (rule_tac x="f x" in exI)
   1.140 -  apply auto
   1.141 -  done
   1.142 -
   1.143 -lemma isCont_bounded:
   1.144 -  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   1.145 -  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> \<exists>M. \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
   1.146 -  using isCont_eq_Ub[of a b f] by auto
   1.147 -
   1.148 -lemma isCont_has_Ub:
   1.149 -  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   1.150 -  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
   1.151 -    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<forall>N. N < M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x))"
   1.152 -  using isCont_eq_Ub[of a b f] by auto
   1.153 -
   1.154 -text{*Refine the above to existence of least upper bound*}
   1.155 -
   1.156 -lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) -->
   1.157 -      (\<exists>t. isLub UNIV S t)"
   1.158 -by (blast intro: reals_complete)
   1.159 -
   1.160 -
   1.161 -text{*Another version.*}
   1.162 -
   1.163 -lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
   1.164 -      ==> \<exists>L M::real. (\<forall>x::real. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
   1.165 -          (\<forall>y. L \<le> y & y \<le> M --> (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))"
   1.166 -apply (frule isCont_eq_Lb)
   1.167 -apply (frule_tac [2] isCont_eq_Ub)
   1.168 -apply (assumption+, safe)
   1.169 -apply (rule_tac x = "f x" in exI)
   1.170 -apply (rule_tac x = "f xa" in exI, simp, safe)
   1.171 -apply (cut_tac x = x and y = xa in linorder_linear, safe)
   1.172 -apply (cut_tac f = f and a = x and b = xa and y = y in IVT_objl)
   1.173 -apply (cut_tac [2] f = f and a = xa and b = x and y = y in IVT2_objl, safe)
   1.174 -apply (rule_tac [2] x = xb in exI)
   1.175 -apply (rule_tac [4] x = xb in exI, simp_all)
   1.176 -done
   1.177 -
   1.178 -
   1.179  subsection {* Local extrema *}
   1.180  
   1.181  text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
   1.182 @@ -658,7 +486,6 @@
   1.183    qed
   1.184  qed
   1.185  
   1.186 -
   1.187  lemma DERIV_pos_inc_left:
   1.188    fixes f :: "real => real"
   1.189    shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
   1.190 @@ -1081,47 +908,6 @@
   1.191      by simp
   1.192  qed
   1.193  
   1.194 -text{*Continuity of inverse function*}
   1.195 -
   1.196 -lemma isCont_inverse_function:
   1.197 -  fixes f g :: "real \<Rightarrow> real"
   1.198 -  assumes d: "0 < d"
   1.199 -      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
   1.200 -      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
   1.201 -  shows "isCont g (f x)"
   1.202 -proof -
   1.203 -  let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}"
   1.204 -
   1.205 -  have f: "continuous_on ?D f"
   1.206 -    using cont by (intro continuous_at_imp_continuous_on ballI) auto
   1.207 -  then have g: "continuous_on (f`?D) g"
   1.208 -    using inj by (intro continuous_on_inv) auto
   1.209 -
   1.210 -  from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D"
   1.211 -    by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
   1.212 -  with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
   1.213 -    by (rule continuous_on_subset)
   1.214 -  moreover
   1.215 -  have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)"
   1.216 -    using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
   1.217 -  then have "f x \<in> {min ?A ?B <..< max ?A ?B}"
   1.218 -    by auto
   1.219 -  ultimately
   1.220 -  show ?thesis
   1.221 -    by (simp add: continuous_on_eq_continuous_at)
   1.222 -qed
   1.223 -
   1.224 -lemma isCont_inverse_function2:
   1.225 -  fixes f g :: "real \<Rightarrow> real" shows
   1.226 -  "\<lbrakk>a < x; x < b;
   1.227 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
   1.228 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
   1.229 -   \<Longrightarrow> isCont g (f x)"
   1.230 -apply (rule isCont_inverse_function
   1.231 -       [where f=f and d="min (x - a) (b - x)"])
   1.232 -apply (simp_all add: abs_le_iff)
   1.233 -done
   1.234 -
   1.235  text {* Derivative of inverse function *}
   1.236  
   1.237  lemma DERIV_inverse_function:
   1.238 @@ -1228,44 +1014,6 @@
   1.239    with g'cdef f'cdef cint show ?thesis by auto
   1.240  qed
   1.241  
   1.242 -
   1.243 -subsection {* Theorems about Limits *}
   1.244 -
   1.245 -(* need to rename second isCont_inverse *)
   1.246 -
   1.247 -lemma isCont_inv_fun:
   1.248 -  fixes f g :: "real \<Rightarrow> real"
   1.249 -  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
   1.250 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
   1.251 -      ==> isCont g (f x)"
   1.252 -by (rule isCont_inverse_function)
   1.253 -
   1.254 -text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
   1.255 -lemma LIM_fun_gt_zero:
   1.256 -     "[| f -- c --> (l::real); 0 < l |]  
   1.257 -         ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
   1.258 -apply (drule (1) LIM_D, clarify)
   1.259 -apply (rule_tac x = s in exI)
   1.260 -apply (simp add: abs_less_iff)
   1.261 -done
   1.262 -
   1.263 -lemma LIM_fun_less_zero:
   1.264 -     "[| f -- c --> (l::real); l < 0 |]  
   1.265 -      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
   1.266 -apply (drule LIM_D [where r="-l"], simp, clarify)
   1.267 -apply (rule_tac x = s in exI)
   1.268 -apply (simp add: abs_less_iff)
   1.269 -done
   1.270 -
   1.271 -lemma LIM_fun_not_zero:
   1.272 -     "[| f -- c --> (l::real); l \<noteq> 0 |] 
   1.273 -      ==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
   1.274 -apply (rule linorder_cases [of l 0])
   1.275 -apply (drule (1) LIM_fun_less_zero, force)
   1.276 -apply simp
   1.277 -apply (drule (1) LIM_fun_gt_zero, force)
   1.278 -done
   1.279 -
   1.280  lemma GMVT':
   1.281    fixes f g :: "real \<Rightarrow> real"
   1.282    assumes "a < b"
   1.283 @@ -1284,6 +1032,9 @@
   1.284      by auto
   1.285  qed
   1.286  
   1.287 +
   1.288 +subsection {* L'Hopitals rule *}
   1.289 +
   1.290  lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
   1.291      DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
   1.292    unfolding DERIV_iff2
     2.1 --- a/src/HOL/Limits.thy	Tue Mar 26 12:20:59 2013 +0100
     2.2 +++ b/src/HOL/Limits.thy	Tue Mar 26 12:21:00 2013 +0100
     2.3 @@ -705,6 +705,7 @@
     2.4    qed
     2.5  qed force
     2.6  
     2.7 +
     2.8  subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
     2.9  
    2.10  text {*
    2.11 @@ -1648,5 +1649,234 @@
    2.12      using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
    2.13  qed simp
    2.14  
    2.15 +
    2.16 +subsection {* Nested Intervals and Bisection -- Needed for Compactness *}
    2.17 +
    2.18 +lemma nested_sequence_unique:
    2.19 +  assumes "\<forall>n. f n \<le> f (Suc n)" "\<forall>n. g (Suc n) \<le> g n" "\<forall>n. f n \<le> g n" "(\<lambda>n. f n - g n) ----> 0"
    2.20 +  shows "\<exists>l::real. ((\<forall>n. f n \<le> l) \<and> f ----> l) \<and> ((\<forall>n. l \<le> g n) \<and> g ----> l)"
    2.21 +proof -
    2.22 +  have "incseq f" unfolding incseq_Suc_iff by fact
    2.23 +  have "decseq g" unfolding decseq_Suc_iff by fact
    2.24 +
    2.25 +  { fix n
    2.26 +    from `decseq g` have "g n \<le> g 0" by (rule decseqD) simp
    2.27 +    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f n \<le> g 0" by auto }
    2.28 +  then obtain u where "f ----> u" "\<forall>i. f i \<le> u"
    2.29 +    using incseq_convergent[OF `incseq f`] by auto
    2.30 +  moreover
    2.31 +  { fix n
    2.32 +    from `incseq f` have "f 0 \<le> f n" by (rule incseqD) simp
    2.33 +    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f 0 \<le> g n" by simp }
    2.34 +  then obtain l where "g ----> l" "\<forall>i. l \<le> g i"
    2.35 +    using decseq_convergent[OF `decseq g`] by auto
    2.36 +  moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]]
    2.37 +  ultimately show ?thesis by auto
    2.38 +qed
    2.39 +
    2.40 +lemma Bolzano[consumes 1, case_names trans local]:
    2.41 +  fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
    2.42 +  assumes [arith]: "a \<le> b"
    2.43 +  assumes trans: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
    2.44 +  assumes local: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<exists>d>0. \<forall>a b. a \<le> x \<and> x \<le> b \<and> b - a < d \<longrightarrow> P a b"
    2.45 +  shows "P a b"
    2.46 +proof -
    2.47 +  def bisect \<equiv> "nat_rec (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))"
    2.48 +  def l \<equiv> "\<lambda>n. fst (bisect n)" and u \<equiv> "\<lambda>n. snd (bisect n)"
    2.49 +  have l[simp]: "l 0 = a" "\<And>n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)"
    2.50 +    and u[simp]: "u 0 = b" "\<And>n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)"
    2.51 +    by (simp_all add: l_def u_def bisect_def split: prod.split)
    2.52 +
    2.53 +  { fix n have "l n \<le> u n" by (induct n) auto } note this[simp]
    2.54 +
    2.55 +  have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l ----> x) \<and> ((\<forall>n. x \<le> u n) \<and> u ----> x)"
    2.56 +  proof (safe intro!: nested_sequence_unique)
    2.57 +    fix n show "l n \<le> l (Suc n)" "u (Suc n) \<le> u n" by (induct n) auto
    2.58 +  next
    2.59 +    { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) }
    2.60 +    then show "(\<lambda>n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero)
    2.61 +  qed fact
    2.62 +  then obtain x where x: "\<And>n. l n \<le> x" "\<And>n. x \<le> u n" and "l ----> x" "u ----> x" by auto
    2.63 +  obtain d where "0 < d" and d: "\<And>a b. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> b - a < d \<Longrightarrow> P a b"
    2.64 +    using `l 0 \<le> x` `x \<le> u 0` local[of x] by auto
    2.65 +
    2.66 +  show "P a b"
    2.67 +  proof (rule ccontr)
    2.68 +    assume "\<not> P a b" 
    2.69 +    { fix n have "\<not> P (l n) (u n)"
    2.70 +      proof (induct n)
    2.71 +        case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto
    2.72 +      qed (simp add: `\<not> P a b`) }
    2.73 +    moreover
    2.74 +    { have "eventually (\<lambda>n. x - d / 2 < l n) sequentially"
    2.75 +        using `0 < d` `l ----> x` by (intro order_tendstoD[of _ x]) auto
    2.76 +      moreover have "eventually (\<lambda>n. u n < x + d / 2) sequentially"
    2.77 +        using `0 < d` `u ----> x` by (intro order_tendstoD[of _ x]) auto
    2.78 +      ultimately have "eventually (\<lambda>n. P (l n) (u n)) sequentially"
    2.79 +      proof eventually_elim
    2.80 +        fix n assume "x - d / 2 < l n" "u n < x + d / 2"
    2.81 +        from add_strict_mono[OF this] have "u n - l n < d" by simp
    2.82 +        with x show "P (l n) (u n)" by (rule d)
    2.83 +      qed }
    2.84 +    ultimately show False by simp
    2.85 +  qed
    2.86 +qed
    2.87 +
    2.88 +lemma compact_Icc[simp, intro]: "compact {a .. b::real}"
    2.89 +proof (cases "a \<le> b", rule compactI)
    2.90 +  fix C assume C: "a \<le> b" "\<forall>t\<in>C. open t" "{a..b} \<subseteq> \<Union>C"
    2.91 +  def T == "{a .. b}"
    2.92 +  from C(1,3) show "\<exists>C'\<subseteq>C. finite C' \<and> {a..b} \<subseteq> \<Union>C'"
    2.93 +  proof (induct rule: Bolzano)
    2.94 +    case (trans a b c)
    2.95 +    then have *: "{a .. c} = {a .. b} \<union> {b .. c}" by auto
    2.96 +    from trans obtain C1 C2 where "C1\<subseteq>C \<and> finite C1 \<and> {a..b} \<subseteq> \<Union>C1" "C2\<subseteq>C \<and> finite C2 \<and> {b..c} \<subseteq> \<Union>C2"
    2.97 +      by (auto simp: *)
    2.98 +    with trans show ?case
    2.99 +      unfolding * by (intro exI[of _ "C1 \<union> C2"]) auto
   2.100 +  next
   2.101 +    case (local x)
   2.102 +    then have "x \<in> \<Union>C" using C by auto
   2.103 +    with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
   2.104 +    then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
   2.105 +      by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
   2.106 +    with `c \<in> C` show ?case
   2.107 +      by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
   2.108 +  qed
   2.109 +qed simp
   2.110 +
   2.111 +
   2.112 +subsection {* Boundedness of continuous functions *}
   2.113 +
   2.114 +text{*By bisection, function continuous on closed interval is bounded above*}
   2.115 +
   2.116 +lemma isCont_eq_Ub:
   2.117 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   2.118 +  shows "a \<le> b \<Longrightarrow> \<forall>x::real. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
   2.119 +    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
   2.120 +  using continuous_attains_sup[of "{a .. b}" f]
   2.121 +  by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def)
   2.122 +
   2.123 +lemma isCont_eq_Lb:
   2.124 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   2.125 +  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
   2.126 +    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> M \<le> f x) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
   2.127 +  using continuous_attains_inf[of "{a .. b}" f]
   2.128 +  by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def)
   2.129 +
   2.130 +lemma isCont_bounded:
   2.131 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   2.132 +  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> \<exists>M. \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
   2.133 +  using isCont_eq_Ub[of a b f] by auto
   2.134 +
   2.135 +lemma isCont_has_Ub:
   2.136 +  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   2.137 +  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
   2.138 +    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<forall>N. N < M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x))"
   2.139 +  using isCont_eq_Ub[of a b f] by auto
   2.140 +
   2.141 +(*HOL style here: object-level formulations*)
   2.142 +lemma IVT_objl: "(f(a::real) \<le> (y::real) & y \<le> f(b) & a \<le> b &
   2.143 +      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
   2.144 +      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
   2.145 +  by (blast intro: IVT)
   2.146 +
   2.147 +lemma IVT2_objl: "(f(b::real) \<le> (y::real) & y \<le> f(a) & a \<le> b &
   2.148 +      (\<forall>x. a \<le> x & x \<le> b --> isCont f x))
   2.149 +      --> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)"
   2.150 +  by (blast intro: IVT2)
   2.151 +
   2.152 +lemma isCont_Lb_Ub:
   2.153 +  fixes f :: "real \<Rightarrow> real"
   2.154 +  assumes "a \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
   2.155 +  shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and> 
   2.156 +               (\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> (f x = y)))"
   2.157 +proof -
   2.158 +  obtain M where M: "a \<le> M" "M \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> f M"
   2.159 +    using isCont_eq_Ub[OF assms] by auto
   2.160 +  obtain L where L: "a \<le> L" "L \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f L \<le> f x"
   2.161 +    using isCont_eq_Lb[OF assms] by auto
   2.162 +  show ?thesis
   2.163 +    using IVT[of f L _ M] IVT2[of f L _ M] M L assms
   2.164 +    apply (rule_tac x="f L" in exI)
   2.165 +    apply (rule_tac x="f M" in exI)
   2.166 +    apply (cases "L \<le> M")
   2.167 +    apply (simp, metis order_trans)
   2.168 +    apply (simp, metis order_trans)
   2.169 +    done
   2.170 +qed
   2.171 +
   2.172 +
   2.173 +text{*Continuity of inverse function*}
   2.174 +
   2.175 +lemma isCont_inverse_function:
   2.176 +  fixes f g :: "real \<Rightarrow> real"
   2.177 +  assumes d: "0 < d"
   2.178 +      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
   2.179 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
   2.180 +  shows "isCont g (f x)"
   2.181 +proof -
   2.182 +  let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}"
   2.183 +
   2.184 +  have f: "continuous_on ?D f"
   2.185 +    using cont by (intro continuous_at_imp_continuous_on ballI) auto
   2.186 +  then have g: "continuous_on (f`?D) g"
   2.187 +    using inj by (intro continuous_on_inv) auto
   2.188 +
   2.189 +  from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D"
   2.190 +    by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
   2.191 +  with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
   2.192 +    by (rule continuous_on_subset)
   2.193 +  moreover
   2.194 +  have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)"
   2.195 +    using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
   2.196 +  then have "f x \<in> {min ?A ?B <..< max ?A ?B}"
   2.197 +    by auto
   2.198 +  ultimately
   2.199 +  show ?thesis
   2.200 +    by (simp add: continuous_on_eq_continuous_at)
   2.201 +qed
   2.202 +
   2.203 +lemma isCont_inverse_function2:
   2.204 +  fixes f g :: "real \<Rightarrow> real" shows
   2.205 +  "\<lbrakk>a < x; x < b;
   2.206 +    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
   2.207 +    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
   2.208 +   \<Longrightarrow> isCont g (f x)"
   2.209 +apply (rule isCont_inverse_function
   2.210 +       [where f=f and d="min (x - a) (b - x)"])
   2.211 +apply (simp_all add: abs_le_iff)
   2.212 +done
   2.213 +
   2.214 +(* need to rename second isCont_inverse *)
   2.215 +
   2.216 +lemma isCont_inv_fun:
   2.217 +  fixes f g :: "real \<Rightarrow> real"
   2.218 +  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
   2.219 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
   2.220 +      ==> isCont g (f x)"
   2.221 +by (rule isCont_inverse_function)
   2.222 +
   2.223 +text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
   2.224 +lemma LIM_fun_gt_zero:
   2.225 +  fixes f :: "real \<Rightarrow> real"
   2.226 +  shows "f -- c --> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"
   2.227 +apply (drule (1) LIM_D, clarify)
   2.228 +apply (rule_tac x = s in exI)
   2.229 +apply (simp add: abs_less_iff)
   2.230 +done
   2.231 +
   2.232 +lemma LIM_fun_less_zero:
   2.233 +  fixes f :: "real \<Rightarrow> real"
   2.234 +  shows "f -- c --> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x < 0)"
   2.235 +apply (drule LIM_D [where r="-l"], simp, clarify)
   2.236 +apply (rule_tac x = s in exI)
   2.237 +apply (simp add: abs_less_iff)
   2.238 +done
   2.239 +
   2.240 +lemma LIM_fun_not_zero:
   2.241 +  fixes f :: "real \<Rightarrow> real"
   2.242 +  shows "f -- c --> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)"
   2.243 +  using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
   2.244  end
   2.245