1.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Feb 06 17:18:01 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 06 17:57:21 2013 +0100
     1.3 @@ -11,6 +11,13 @@
     1.4  imports "~~/src/HOL/Complex_Main" Extended_Nat
     1.5  begin
     1.6  
     1.7 +text {*
     1.8 +
     1.9 +For more lemmas about the extended real numbers go to
    1.10 +  @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
    1.11 +
    1.12 +*}
    1.13 +
    1.14  lemma LIMSEQ_SUP:
    1.15    fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
    1.16    assumes "incseq X"
    1.17 @@ -22,24 +29,37 @@
    1.18  lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
    1.19    by (cases P) (simp_all add: eventually_False)
    1.20  
    1.21 -lemma (in complete_lattice) Inf_le_Sup:
    1.22 -  assumes "A \<noteq> {}" shows "Inf A \<le> Sup A"
    1.23 -proof -
    1.24 -  from `A \<noteq> {}` obtain x where "x \<in> A" by auto
    1.25 -  then show ?thesis
    1.26 -    by (metis Sup_upper2 Inf_lower)
    1.27 -qed
    1.28 -
    1.29 -lemma (in complete_lattice) INF_le_SUP:
    1.30 -  "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
    1.31 +lemma (in complete_lattice) Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
    1.32 +  by (metis Sup_upper2 Inf_lower ex_in_conv)
    1.33 +
    1.34 +lemma (in complete_lattice) INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
    1.35    unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
    1.36  
    1.37 -text {*
    1.38 -
    1.39 -For more lemmas about the extended real numbers go to
    1.40 -  @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
    1.41 -
    1.42 -*}
    1.43 +lemma (in complete_linorder) le_Sup_iff:
    1.44 +  "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
    1.45 +proof safe
    1.46 +  fix y assume "x \<le> Sup A" "y < x"
    1.47 +  then have "y < Sup A" by auto
    1.48 +  then show "\<exists>a\<in>A. y < a"
    1.49 +    unfolding less_Sup_iff .
    1.50 +qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper)
    1.51 +
    1.52 +lemma (in complete_linorder) le_SUP_iff:
    1.53 +  "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
    1.54 +  unfolding le_Sup_iff SUP_def by simp
    1.55 +
    1.56 +lemma (in complete_linorder) Inf_le_iff:
    1.57 +  "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
    1.58 +proof safe
    1.59 +  fix y assume "x \<ge> Inf A" "y > x"
    1.60 +  then have "y > Inf A" by auto
    1.61 +  then show "\<exists>a\<in>A. y > a"
    1.62 +    unfolding Inf_less_iff .
    1.63 +qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower)
    1.64 +
    1.65 +lemma (in complete_linorder) le_INF_iff:
    1.66 +  "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
    1.67 +  unfolding Inf_le_iff INF_def by simp
    1.68  
    1.69  lemma (in complete_lattice) Sup_eqI:
    1.70    assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
    1.71 @@ -1429,8 +1449,7 @@
    1.72  
    1.73  lemma ereal_le_Sup:
    1.74    fixes x :: ereal
    1.75 -  shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))"
    1.76 -(is "?lhs <-> ?rhs")
    1.77 +  shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs")
    1.78  proof-
    1.79  { assume "?rhs"
    1.80    { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
    1.81 @@ -1994,18 +2013,13 @@
    1.82  qed
    1.83  
    1.84  lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
    1.85 -  unfolding tendsto_def
    1.86 -proof safe
    1.87 -  fix S :: "ereal set" assume "open S" "\<infinity> \<in> S"
    1.88 -  from open_PInfty[OF this] guess B .. note B = this
    1.89 -  moreover
    1.90 -  assume "\<forall>r::real. eventually (\<lambda>z. r < f z) F"
    1.91 -  then have "eventually (\<lambda>z. f z \<in> {B <..}) F" by auto
    1.92 -  ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
    1.93 -next
    1.94 -  fix x assume "\<forall>S. open S \<longrightarrow> \<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
    1.95 -  from this[rule_format, of "{ereal x <..}"]
    1.96 -  show "eventually (\<lambda>y. ereal x < f y) F" by auto
    1.97 +proof -
    1.98 +  { fix l :: ereal assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
    1.99 +    from this[THEN spec, of "real l"]
   1.100 +    have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
   1.101 +      by (cases l) (auto elim: eventually_elim1) }
   1.102 +  then show ?thesis
   1.103 +    by (auto simp: order_tendsto_iff)
   1.104  qed
   1.105  
   1.106  lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
   1.107 @@ -2209,7 +2223,6 @@
   1.108    "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
   1.109    by (metis sup_ereal_def sup_least)
   1.110  
   1.111 -
   1.112  lemma ereal_LimI_finite:
   1.113    fixes x :: ereal
   1.114    assumes "\<bar>x\<bar> \<noteq> \<infinity>"
   1.115 @@ -2403,25 +2416,142 @@
   1.116    shows "Limsup F X \<le> C"
   1.117    using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
   1.118  
   1.119 +lemma le_Liminf_iff:
   1.120 +  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   1.121 +  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   1.122 +proof -
   1.123 +  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
   1.124 +    then have "eventually (\<lambda>x. y < X x) F"
   1.125 +      by (auto elim!: eventually_elim1 dest: less_INF_D) }
   1.126 +  moreover
   1.127 +  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
   1.128 +    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
   1.129 +    proof cases
   1.130 +      assume "\<exists>z. y < z \<and> z < C"
   1.131 +      then guess z ..
   1.132 +      moreover then have "z \<le> INFI {x. z < X x} X"
   1.133 +        by (auto intro!: INF_greatest)
   1.134 +      ultimately show ?thesis
   1.135 +        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   1.136 +    next
   1.137 +      assume "\<not> (\<exists>z. y < z \<and> z < C)"
   1.138 +      then have "C \<le> INFI {x. y < X x} X"
   1.139 +        by (intro INF_greatest) auto
   1.140 +      with `y < C` show ?thesis
   1.141 +        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
   1.142 +    qed }
   1.143 +  ultimately show ?thesis
   1.144 +    unfolding Liminf_def le_SUP_iff by auto
   1.145 +qed
   1.146 +
   1.147 +lemma lim_imp_Liminf:
   1.148 +  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
   1.149 +  assumes ntriv: "\<not> trivial_limit F"
   1.150 +  assumes lim: "(f ---> f0) F"
   1.151 +  shows "Liminf F f = f0"
   1.152 +proof (intro Liminf_eqI)
   1.153 +  fix P assume P: "eventually P F"
   1.154 +  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
   1.155 +    by eventually_elim (auto intro!: INF_lower)
   1.156 +  then show "INFI (Collect P) f \<le> f0"
   1.157 +    by (rule tendsto_le[OF ntriv lim tendsto_const])
   1.158 +next
   1.159 +  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
   1.160 +  show "f0 \<le> y"
   1.161 +  proof cases
   1.162 +    assume "\<exists>z. y < z \<and> z < f0"
   1.163 +    then guess z ..
   1.164 +    moreover have "z \<le> INFI {x. z < f x} f"
   1.165 +      by (rule INF_greatest) simp
   1.166 +    ultimately show ?thesis
   1.167 +      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   1.168 +  next
   1.169 +    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
   1.170 +    show ?thesis
   1.171 +    proof (rule classical)
   1.172 +      assume "\<not> f0 \<le> y"
   1.173 +      then have "eventually (\<lambda>x. y < f x) F"
   1.174 +        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   1.175 +      then have "eventually (\<lambda>x. f0 \<le> f x) F"
   1.176 +        using discrete by (auto elim!: eventually_elim1)
   1.177 +      then have "INFI {x. f0 \<le> f x} f \<le> y"
   1.178 +        by (rule upper)
   1.179 +      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
   1.180 +        by (intro INF_greatest) simp
   1.181 +      ultimately show "f0 \<le> y" by simp
   1.182 +    qed
   1.183 +  qed
   1.184 +qed
   1.185 +
   1.186 +lemma lim_imp_Limsup:
   1.187 +  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
   1.188 +  assumes ntriv: "\<not> trivial_limit F"
   1.189 +  assumes lim: "(f ---> f0) F"
   1.190 +  shows "Limsup F f = f0"
   1.191 +proof (intro Limsup_eqI)
   1.192 +  fix P assume P: "eventually P F"
   1.193 +  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
   1.194 +    by eventually_elim (auto intro!: SUP_upper)
   1.195 +  then show "f0 \<le> SUPR (Collect P) f"
   1.196 +    by (rule tendsto_le[OF ntriv tendsto_const lim])
   1.197 +next
   1.198 +  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
   1.199 +  show "y \<le> f0"
   1.200 +  proof cases
   1.201 +    assume "\<exists>z. f0 < z \<and> z < y"
   1.202 +    then guess z ..
   1.203 +    moreover have "SUPR {x. f x < z} f \<le> z"
   1.204 +      by (rule SUP_least) simp
   1.205 +    ultimately show ?thesis
   1.206 +      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   1.207 +  next
   1.208 +    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
   1.209 +    show ?thesis
   1.210 +    proof (rule classical)
   1.211 +      assume "\<not> y \<le> f0"
   1.212 +      then have "eventually (\<lambda>x. f x < y) F"
   1.213 +        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   1.214 +      then have "eventually (\<lambda>x. f x \<le> f0) F"
   1.215 +        using discrete by (auto elim!: eventually_elim1 simp: not_less)
   1.216 +      then have "y \<le> SUPR {x. f x \<le> f0} f"
   1.217 +        by (rule lower)
   1.218 +      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
   1.219 +        by (intro SUP_least) simp
   1.220 +      ultimately show "y \<le> f0" by simp
   1.221 +    qed
   1.222 +  qed
   1.223 +qed
   1.224 +
   1.225 +lemma Liminf_eq_Limsup:
   1.226 +  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
   1.227 +  assumes ntriv: "\<not> trivial_limit F"
   1.228 +    and lim: "Liminf F f = f0" "Limsup F f = f0"
   1.229 +  shows "(f ---> f0) F"
   1.230 +proof (rule order_tendstoI)
   1.231 +  fix a assume "f0 < a"
   1.232 +  with assms have "Limsup F f < a" by simp
   1.233 +  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
   1.234 +    unfolding Limsup_def INF_less_iff by auto
   1.235 +  then show "eventually (\<lambda>x. f x < a) F"
   1.236 +    by (auto elim!: eventually_elim1 dest: SUP_lessD)
   1.237 +next
   1.238 +  fix a assume "a < f0"
   1.239 +  with assms have "a < Liminf F f" by simp
   1.240 +  then obtain P where "eventually P F" "a < INFI (Collect P) f"
   1.241 +    unfolding Liminf_def less_SUP_iff by auto
   1.242 +  then show "eventually (\<lambda>x. a < f x) F"
   1.243 +    by (auto elim!: eventually_elim1 dest: less_INF_D)
   1.244 +qed
   1.245 +
   1.246 +lemma tendsto_iff_Liminf_eq_Limsup:
   1.247 +  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
   1.248 +  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
   1.249 +  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
   1.250 +
   1.251  lemma liminf_bounded_iff:
   1.252    fixes x :: "nat \<Rightarrow> ereal"
   1.253    shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
   1.254 -proof safe
   1.255 -  fix B assume "B < C" "C \<le> liminf x"
   1.256 -  then have "B < liminf x" by auto
   1.257 -  then obtain N where "B < (INF m:{N..}. x m)"
   1.258 -    unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
   1.259 -  from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
   1.260 -next
   1.261 -  assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
   1.262 -  { fix B assume "B<C"
   1.263 -    then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
   1.264 -    hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
   1.265 -    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
   1.266 -    finally have "B \<le> liminf x" .
   1.267 -  } then show "?lhs"
   1.268 -    by (metis * leD Liminf_bounded[OF sequentially_bot] linorder_le_less_linear eventually_sequentially)
   1.269 -qed
   1.270 +  unfolding le_Liminf_iff eventually_sequentially ..
   1.271  
   1.272  lemma liminf_subseq_mono:
   1.273    fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   1.274 @@ -2449,56 +2579,6 @@
   1.275    then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
   1.276  qed
   1.277  
   1.278 -lemma lim_imp_Liminf:
   1.279 -  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
   1.280 -  assumes ntriv: "\<not> trivial_limit F"
   1.281 -  assumes lim: "(f ---> f0) F"
   1.282 -  shows "Liminf F f = f0"
   1.283 -proof (rule Liminf_eqI)
   1.284 -  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
   1.285 -  show "f0 \<le> y"
   1.286 -  proof (rule ereal_le_ereal)
   1.287 -    fix B
   1.288 -    assume "B < f0"
   1.289 -    have "B \<le> INFI {x. B < f x} f"
   1.290 -      by (rule INF_greatest) simp
   1.291 -    also have "INFI {x. B < f x} f \<le> y"
   1.292 -      using lim[THEN topological_tendstoD, of "{B <..}"] `B < f0` * by auto
   1.293 -    finally show "B \<le> y" .
   1.294 -  qed
   1.295 -next
   1.296 -  fix P assume P: "eventually P F"
   1.297 -  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
   1.298 -    by eventually_elim (auto intro!: INF_lower)
   1.299 -  then show "INFI (Collect P) f \<le> f0"
   1.300 -    by (rule tendsto_le[OF ntriv lim tendsto_const])
   1.301 -qed
   1.302 -
   1.303 -lemma lim_imp_Limsup:
   1.304 -  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
   1.305 -  assumes ntriv: "\<not> trivial_limit F"
   1.306 -  assumes lim: "(f ---> f0) F"
   1.307 -  shows "Limsup F f = f0"
   1.308 -proof (rule Limsup_eqI)
   1.309 -  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
   1.310 -  show "y \<le> f0"
   1.311 -  proof (rule ereal_ge_ereal, safe)
   1.312 -    fix B
   1.313 -    assume "f0 < B"
   1.314 -    have "y \<le> SUPR {x. f x < B} f"
   1.315 -      using lim[THEN topological_tendstoD, of "{..< B}"] `f0 < B` * by auto
   1.316 -    also have "SUPR {x. f x < B} f \<le> B"
   1.317 -      by (rule SUP_least) simp
   1.318 -    finally show "y \<le> B" .
   1.319 -  qed
   1.320 -next
   1.321 -  fix P assume P: "eventually P F"
   1.322 -  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
   1.323 -    by eventually_elim (auto intro!: SUP_upper)
   1.324 -  then show "f0 \<le> SUPR (Collect P) f"
   1.325 -    by (rule tendsto_le[OF ntriv tendsto_const lim])
   1.326 -qed
   1.327 -
   1.328  definition (in order) mono_set:
   1.329    "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
   1.330  

     2.1 --- a/src/HOL/Limits.thy	Wed Feb 06 17:18:01 2013 +0100
     2.2 +++ b/src/HOL/Limits.thy	Wed Feb 06 17:57:21 2013 +0100
     2.3 @@ -469,12 +469,6 @@
     2.4  apply (erule le_less_trans [OF dist_triangle])
     2.5  done
     2.6  
     2.7 -lemma eventually_nhds_order:
     2.8 -  "eventually P (nhds (a::'a::linorder_topology)) \<longleftrightarrow>
     2.9 -    (\<exists>S. open_interval S \<and> a \<in> S \<and> (\<forall>z\<in>S. P z))"
    2.10 -  (is "_ \<longleftrightarrow> ?rhs")
    2.11 -  unfolding eventually_nhds by (auto dest!: open_orderD dest: open_interval_imp_open)
    2.12 -
    2.13  lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
    2.14    unfolding trivial_limit_def eventually_nhds by simp
    2.15  
    2.16 @@ -838,6 +832,35 @@
    2.17    "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
    2.18    using tendstoI tendstoD by fast
    2.19  
    2.20 +lemma order_tendstoI:
    2.21 +  fixes y :: "_ :: order_topology"
    2.22 +  assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
    2.23 +  assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
    2.24 +  shows "(f ---> y) F"
    2.25 +proof (rule topological_tendstoI)
    2.26 +  fix S assume "open S" "y \<in> S"
    2.27 +  then show "eventually (\<lambda>x. f x \<in> S) F"
    2.28 +    unfolding open_generated_order
    2.29 +  proof induct
    2.30 +    case (UN K)
    2.31 +    then obtain k where "y \<in> k" "k \<in> K" by auto
    2.32 +    with UN(2)[of k] show ?case
    2.33 +      by (auto elim: eventually_elim1)
    2.34 +  qed (insert assms, auto elim: eventually_elim2)
    2.35 +qed
    2.36 +
    2.37 +lemma order_tendstoD:
    2.38 +  fixes y :: "_ :: order_topology"
    2.39 +  assumes y: "(f ---> y) F"
    2.40 +  shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
    2.41 +    and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
    2.42 +  using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto
    2.43 +
    2.44 +lemma order_tendsto_iff: 
    2.45 +  fixes f :: "_ \<Rightarrow> 'a :: order_topology"
    2.46 +  shows "(f ---> x) F \<longleftrightarrow>(\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
    2.47 +  by (metis order_tendstoI order_tendstoD)
    2.48 +
    2.49  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
    2.50    by (simp only: tendsto_iff Zfun_def dist_norm)
    2.51  
    2.52 @@ -908,34 +931,18 @@
    2.53  qed
    2.54  
    2.55  lemma increasing_tendsto:
    2.56 -  fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
    2.57 +  fixes f :: "_ \<Rightarrow> 'a::order_topology"
    2.58    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
    2.59        and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
    2.60    shows "(f ---> l) F"
    2.61 -proof (rule topological_tendstoI)
    2.62 -  fix S assume "open S" "l \<in> S"
    2.63 -  then show "eventually (\<lambda>x. f x \<in> S) F"
    2.64 -  proof (induct rule: open_order_induct)
    2.65 -    case (greaterThanLessThan a b) with en bdd show ?case
    2.66 -      by (auto elim!: eventually_elim2)
    2.67 -  qed (insert en bdd, auto elim!: eventually_elim1)
    2.68 -qed
    2.69 +  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
    2.70  
    2.71  lemma decreasing_tendsto:
    2.72 -  fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
    2.73 +  fixes f :: "_ \<Rightarrow> 'a::order_topology"
    2.74    assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
    2.75        and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
    2.76    shows "(f ---> l) F"
    2.77 -proof (rule topological_tendstoI)
    2.78 -  fix S assume "open S" "l \<in> S"
    2.79 -  then show "eventually (\<lambda>x. f x \<in> S) F"
    2.80 -  proof (induct rule: open_order_induct)
    2.81 -    case (greaterThanLessThan a b)
    2.82 -    with en have "eventually (\<lambda>n. f n < b) F" by auto
    2.83 -    with bdd show ?case
    2.84 -      by eventually_elim (insert greaterThanLessThan, auto)
    2.85 -  qed (insert en bdd, auto elim!: eventually_elim1)
    2.86 -qed
    2.87 +  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
    2.88  
    2.89  subsubsection {* Distance and norms *}
    2.90  
    2.91 @@ -1039,20 +1046,16 @@
    2.92  qed
    2.93  
    2.94  lemma tendsto_sandwich:
    2.95 -  fixes f g h :: "'a \<Rightarrow> 'b::linorder_topology"
    2.96 +  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
    2.97    assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
    2.98    assumes lim: "(f ---> c) net" "(h ---> c) net"
    2.99    shows "(g ---> c) net"
   2.100 -proof (rule topological_tendstoI)
   2.101 -  fix S assume "open S" "c \<in> S"
   2.102 -  from open_orderD[OF this] obtain T where "open_interval T" "c \<in> T" "T \<subseteq> S" by auto
   2.103 -  with lim[THEN topological_tendstoD, of T]
   2.104 -  have "eventually (\<lambda>x. f x \<in> T) net" "eventually (\<lambda>x. h x \<in> T) net"
   2.105 -    by (auto dest: open_interval_imp_open)
   2.106 -  with ev have "eventually (\<lambda>x. g x \<in> T) net"
   2.107 -    by eventually_elim (insert `open_interval T`, auto dest: open_intervalD)
   2.108 -  with `T \<subseteq> S` show "eventually (\<lambda>x. g x \<in> S) net"
   2.109 -    by (auto elim: eventually_elim1)
   2.110 +proof (rule order_tendstoI)
   2.111 +  fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
   2.112 +    using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
   2.113 +next
   2.114 +  fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
   2.115 +    using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
   2.116  qed
   2.117  
   2.118  lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
   2.119 @@ -1129,15 +1132,12 @@
   2.120    shows "y \<le> x"
   2.121  proof (rule ccontr)
   2.122    assume "\<not> y \<le> x"
   2.123 -  then have "x < y" by simp
   2.124 -  from less_separate[OF this] obtain a b where xy: "x \<in> {..<a}" "y \<in> {b <..}" "{..<a} \<inter> {b<..} = {}"
   2.125 -    by auto
   2.126 -  then have less: "\<And>x y. x < a \<Longrightarrow> b < y \<Longrightarrow> x < y"
   2.127 -    by auto
   2.128 -  from x[THEN topological_tendstoD, of "{..<a}"] y[THEN topological_tendstoD, of "{b <..}"] xy
   2.129 -  have "eventually (\<lambda>x. f x \<in> {..<a}) F" "eventually (\<lambda>x. g x \<in> {b <..}) F" by auto
   2.130 +  with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
   2.131 +    by (auto simp: not_le)
   2.132 +  then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
   2.133 +    using x y by (auto intro: order_tendstoD)
   2.134    with ev have "eventually (\<lambda>x. False) F"
   2.135 -    by eventually_elim (auto dest!: less)
   2.136 +    by eventually_elim (insert xy, fastforce)
   2.137    with F show False
   2.138      by (simp add: eventually_False)
   2.139  qed

     3.1 --- a/src/HOL/RealVector.thy	Wed Feb 06 17:18:01 2013 +0100
     3.2 +++ b/src/HOL/RealVector.thy	Wed Feb 06 17:57:21 2013 +0100
     3.3 @@ -559,60 +559,6 @@
     3.4      by (simp add: closed_Int)
     3.5  qed
     3.6  
     3.7 -inductive open_interval :: "'a::order set \<Rightarrow> bool" where
     3.8 -  empty[intro]: "open_interval {}" |
     3.9 -  UNIV[intro]: "open_interval UNIV" |
    3.10 -  greaterThan[intro]: "open_interval {a <..}" |
    3.11 -  lessThan[intro]: "open_interval {..< b}" |
    3.12 -  greaterThanLessThan[intro]: "open_interval {a <..< b}"
    3.13 -hide_fact (open) empty UNIV greaterThan lessThan greaterThanLessThan
    3.14 -
    3.15 -lemma open_intervalD:
    3.16 -  "open_interval S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> S"
    3.17 -  by (cases rule: open_interval.cases) auto
    3.18 -
    3.19 -lemma open_interval_Int[intro]:
    3.20 -  fixes S T :: "'a :: linorder set"
    3.21 -  assumes S: "open_interval S" and T: "open_interval T"
    3.22 -  shows "open_interval (S \<inter> T)"
    3.23 -proof -
    3.24 -  { fix a b :: 'a have "{..<b} \<inter> {a<..} = { a <..} \<inter> {..< b }" by auto } note this[simp]
    3.25 -  { fix a b :: 'a and A have "{a <..} \<inter> ({b <..} \<inter> A) = {max a b <..} \<inter> A" by auto } note this[simp]
    3.26 -  { fix a b :: 'a and A have "{..<b} \<inter> (A \<inter> {..<a}) = A \<inter> {..<min a b}" by auto } note this[simp]
    3.27 -  { fix a b :: 'a have "open_interval ({ a <..} \<inter> {..< b})"
    3.28 -      unfolding greaterThanLessThan_eq[symmetric] by auto } note this[simp]
    3.29 -  show ?thesis
    3.30 -    by (cases rule: open_interval.cases[OF S, case_product open_interval.cases[OF T]])
    3.31 -       (auto simp: greaterThanLessThan_eq lessThan_Int_lessThan greaterThan_Int_greaterThan Int_assoc)
    3.32 -qed
    3.33 -
    3.34 -lemma open_interval_imp_open: "open_interval S \<Longrightarrow> open (S::'a::order_topology set)"
    3.35 -  by (cases S rule: open_interval.cases) auto
    3.36 -
    3.37 -lemma open_orderD:
    3.38 -  "open (S::'a::linorder_topology set) \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>T. open_interval T \<and> T \<subseteq> S \<and> x \<in> T"
    3.39 -  unfolding open_generated_order
    3.40 -proof (induct rule: generate_topology.induct)
    3.41 -  case (UN K) then obtain k where "k \<in> K" "x \<in> k" by auto
    3.42 -  with UN(2)[of k] show ?case by auto
    3.43 -qed auto
    3.44 -
    3.45 -lemma open_order_induct[consumes 2, case_names subset UNIV lessThan greaterThan greaterThanLessThan]:
    3.46 -  fixes S :: "'a::linorder_topology set"
    3.47 -  assumes S: "open S" "x \<in> S"
    3.48 -  assumes subset: "\<And>S T. P S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> P T"
    3.49 -  assumes univ: "P UNIV"
    3.50 -  assumes lt: "\<And>a. x < a \<Longrightarrow> P {..< a}"
    3.51 -  assumes gt: "\<And>a. a < x \<Longrightarrow> P {a <..}"
    3.52 -  assumes lgt: "\<And>a b. a < x \<Longrightarrow> x < b \<Longrightarrow> P {a <..< b}"
    3.53 -  shows "P S"
    3.54 -proof -
    3.55 -  from open_orderD[OF S] obtain T where "open_interval T" "T \<subseteq> S" "x \<in> T"
    3.56 -    by auto
    3.57 -  then show "P S"
    3.58 -    by induct (auto intro: univ subset lt gt lgt)
    3.59 -qed
    3.60 -
    3.61  subsection {* Metric spaces *}
    3.62  
    3.63  class dist =