# HG changeset patch
# User hoelzl
# Date 1360169841 -3600
# Node ID 78de6c7e8a583c65075f90a05086f5a62eff41c1
# Parent  1cf4faed8b220aa840ab56b825e68bbd5a5b2460
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules

diff -r 1cf4faed8b22 -r 78de6c7e8a58 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Feb 06 17:18:01 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 06 17:57:21 2013 +0100
@@ -11,6 +11,13 @@
 imports "~~/src/HOL/Complex_Main" Extended_Nat
 begin
 
+text {*
+
+For more lemmas about the extended real numbers go to
+  @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
+
+*}
+
 lemma LIMSEQ_SUP:
   fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   assumes "incseq X"
@@ -22,24 +29,37 @@
 lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
   by (cases P) (simp_all add: eventually_False)
 
-lemma (in complete_lattice) Inf_le_Sup:
-  assumes "A \<noteq> {}" shows "Inf A \<le> Sup A"
-proof -
-  from `A \<noteq> {}` obtain x where "x \<in> A" by auto
-  then show ?thesis
-    by (metis Sup_upper2 Inf_lower)
-qed
-
-lemma (in complete_lattice) INF_le_SUP:
-  "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+lemma (in complete_lattice) Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
+  by (metis Sup_upper2 Inf_lower ex_in_conv)
+
+lemma (in complete_lattice) INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
   unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
 
-text {*
-
-For more lemmas about the extended real numbers go to
-  @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
-
-*}
+lemma (in complete_linorder) le_Sup_iff:
+  "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
+proof safe
+  fix y assume "x \<le> Sup A" "y < x"
+  then have "y < Sup A" by auto
+  then show "\<exists>a\<in>A. y < a"
+    unfolding less_Sup_iff .
+qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper)
+
+lemma (in complete_linorder) le_SUP_iff:
+  "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+  unfolding le_Sup_iff SUP_def by simp
+
+lemma (in complete_linorder) Inf_le_iff:
+  "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
+proof safe
+  fix y assume "x \<ge> Inf A" "y > x"
+  then have "y > Inf A" by auto
+  then show "\<exists>a\<in>A. y > a"
+    unfolding Inf_less_iff .
+qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower)
+
+lemma (in complete_linorder) le_INF_iff:
+  "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+  unfolding Inf_le_iff INF_def by simp
 
 lemma (in complete_lattice) Sup_eqI:
   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
@@ -1429,8 +1449,7 @@
 
 lemma ereal_le_Sup:
   fixes x :: ereal
-  shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))"
-(is "?lhs <-> ?rhs")
+  shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs")
 proof-
 { assume "?rhs"
   { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
@@ -1994,18 +2013,13 @@
 qed
 
 lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
-  unfolding tendsto_def
-proof safe
-  fix S :: "ereal set" assume "open S" "\<infinity> \<in> S"
-  from open_PInfty[OF this] guess B .. note B = this
-  moreover
-  assume "\<forall>r::real. eventually (\<lambda>z. r < f z) F"
-  then have "eventually (\<lambda>z. f z \<in> {B <..}) F" by auto
-  ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
-next
-  fix x assume "\<forall>S. open S \<longrightarrow> \<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
-  from this[rule_format, of "{ereal x <..}"]
-  show "eventually (\<lambda>y. ereal x < f y) F" by auto
+proof -
+  { fix l :: ereal assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
+    from this[THEN spec, of "real l"]
+    have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
+      by (cases l) (auto elim: eventually_elim1) }
+  then show ?thesis
+    by (auto simp: order_tendsto_iff)
 qed
 
 lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
@@ -2209,7 +2223,6 @@
   "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
   by (metis sup_ereal_def sup_least)
 
-
 lemma ereal_LimI_finite:
   fixes x :: ereal
   assumes "\<bar>x\<bar> \<noteq> \<infinity>"
@@ -2403,25 +2416,142 @@
   shows "Limsup F X \<le> C"
   using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
 
+lemma le_Liminf_iff:
+  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
+  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
+proof -
+  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
+    then have "eventually (\<lambda>x. y < X x) F"
+      by (auto elim!: eventually_elim1 dest: less_INF_D) }
+  moreover
+  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
+    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
+    proof cases
+      assume "\<exists>z. y < z \<and> z < C"
+      then guess z ..
+      moreover then have "z \<le> INFI {x. z < X x} X"
+        by (auto intro!: INF_greatest)
+      ultimately show ?thesis
+        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
+    next
+      assume "\<not> (\<exists>z. y < z \<and> z < C)"
+      then have "C \<le> INFI {x. y < X x} X"
+        by (intro INF_greatest) auto
+      with `y < C` show ?thesis
+        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
+    qed }
+  ultimately show ?thesis
+    unfolding Liminf_def le_SUP_iff by auto
+qed
+
+lemma lim_imp_Liminf:
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Liminf F f = f0"
+proof (intro Liminf_eqI)
+  fix P assume P: "eventually P F"
+  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
+    by eventually_elim (auto intro!: INF_lower)
+  then show "INFI (Collect P) f \<le> f0"
+    by (rule tendsto_le[OF ntriv lim tendsto_const])
+next
+  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+  show "f0 \<le> y"
+  proof cases
+    assume "\<exists>z. y < z \<and> z < f0"
+    then guess z ..
+    moreover have "z \<le> INFI {x. z < f x} f"
+      by (rule INF_greatest) simp
+    ultimately show ?thesis
+      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
+  next
+    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
+    show ?thesis
+    proof (rule classical)
+      assume "\<not> f0 \<le> y"
+      then have "eventually (\<lambda>x. y < f x) F"
+        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
+      then have "eventually (\<lambda>x. f0 \<le> f x) F"
+        using discrete by (auto elim!: eventually_elim1)
+      then have "INFI {x. f0 \<le> f x} f \<le> y"
+        by (rule upper)
+      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
+        by (intro INF_greatest) simp
+      ultimately show "f0 \<le> y" by simp
+    qed
+  qed
+qed
+
+lemma lim_imp_Limsup:
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Limsup F f = f0"
+proof (intro Limsup_eqI)
+  fix P assume P: "eventually P F"
+  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
+    by eventually_elim (auto intro!: SUP_upper)
+  then show "f0 \<le> SUPR (Collect P) f"
+    by (rule tendsto_le[OF ntriv tendsto_const lim])
+next
+  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
+  show "y \<le> f0"
+  proof cases
+    assume "\<exists>z. f0 < z \<and> z < y"
+    then guess z ..
+    moreover have "SUPR {x. f x < z} f \<le> z"
+      by (rule SUP_least) simp
+    ultimately show ?thesis
+      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
+  next
+    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+    show ?thesis
+    proof (rule classical)
+      assume "\<not> y \<le> f0"
+      then have "eventually (\<lambda>x. f x < y) F"
+        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
+      then have "eventually (\<lambda>x. f x \<le> f0) F"
+        using discrete by (auto elim!: eventually_elim1 simp: not_less)
+      then have "y \<le> SUPR {x. f x \<le> f0} f"
+        by (rule lower)
+      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
+        by (intro SUP_least) simp
+      ultimately show "y \<le> f0" by simp
+    qed
+  qed
+qed
+
+lemma Liminf_eq_Limsup:
+  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+    and lim: "Liminf F f = f0" "Limsup F f = f0"
+  shows "(f ---> f0) F"
+proof (rule order_tendstoI)
+  fix a assume "f0 < a"
+  with assms have "Limsup F f < a" by simp
+  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
+    unfolding Limsup_def INF_less_iff by auto
+  then show "eventually (\<lambda>x. f x < a) F"
+    by (auto elim!: eventually_elim1 dest: SUP_lessD)
+next
+  fix a assume "a < f0"
+  with assms have "a < Liminf F f" by simp
+  then obtain P where "eventually P F" "a < INFI (Collect P) f"
+    unfolding Liminf_def less_SUP_iff by auto
+  then show "eventually (\<lambda>x. a < f x) F"
+    by (auto elim!: eventually_elim1 dest: less_INF_D)
+qed
+
+lemma tendsto_iff_Liminf_eq_Limsup:
+  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
+  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
+
 lemma liminf_bounded_iff:
   fixes x :: "nat \<Rightarrow> ereal"
   shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
-proof safe
-  fix B assume "B < C" "C \<le> liminf x"
-  then have "B < liminf x" by auto
-  then obtain N where "B < (INF m:{N..}. x m)"
-    unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
-  from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
-next
-  assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
-  { fix B assume "B<C"
-    then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
-    hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
-    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
-    finally have "B \<le> liminf x" .
-  } then show "?lhs"
-    by (metis * leD Liminf_bounded[OF sequentially_bot] linorder_le_less_linear eventually_sequentially)
-qed
+  unfolding le_Liminf_iff eventually_sequentially ..
 
 lemma liminf_subseq_mono:
   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
@@ -2449,56 +2579,6 @@
   then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
 qed
 
-lemma lim_imp_Liminf:
-  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes lim: "(f ---> f0) F"
-  shows "Liminf F f = f0"
-proof (rule Liminf_eqI)
-  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
-  show "f0 \<le> y"
-  proof (rule ereal_le_ereal)
-    fix B
-    assume "B < f0"
-    have "B \<le> INFI {x. B < f x} f"
-      by (rule INF_greatest) simp
-    also have "INFI {x. B < f x} f \<le> y"
-      using lim[THEN topological_tendstoD, of "{B <..}"] `B < f0` * by auto
-    finally show "B \<le> y" .
-  qed
-next
-  fix P assume P: "eventually P F"
-  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
-    by eventually_elim (auto intro!: INF_lower)
-  then show "INFI (Collect P) f \<le> f0"
-    by (rule tendsto_le[OF ntriv lim tendsto_const])
-qed
-
-lemma lim_imp_Limsup:
-  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes lim: "(f ---> f0) F"
-  shows "Limsup F f = f0"
-proof (rule Limsup_eqI)
-  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
-  show "y \<le> f0"
-  proof (rule ereal_ge_ereal, safe)
-    fix B
-    assume "f0 < B"
-    have "y \<le> SUPR {x. f x < B} f"
-      using lim[THEN topological_tendstoD, of "{..< B}"] `f0 < B` * by auto
-    also have "SUPR {x. f x < B} f \<le> B"
-      by (rule SUP_least) simp
-    finally show "y \<le> B" .
-  qed
-next
-  fix P assume P: "eventually P F"
-  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
-    by eventually_elim (auto intro!: SUP_upper)
-  then show "f0 \<le> SUPR (Collect P) f"
-    by (rule tendsto_le[OF ntriv tendsto_const lim])
-qed
-
 definition (in order) mono_set:
   "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
 
diff -r 1cf4faed8b22 -r 78de6c7e8a58 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Feb 06 17:18:01 2013 +0100
+++ b/src/HOL/Limits.thy	Wed Feb 06 17:57:21 2013 +0100
@@ -469,12 +469,6 @@
 apply (erule le_less_trans [OF dist_triangle])
 done
 
-lemma eventually_nhds_order:
-  "eventually P (nhds (a::'a::linorder_topology)) \<longleftrightarrow>
-    (\<exists>S. open_interval S \<and> a \<in> S \<and> (\<forall>z\<in>S. P z))"
-  (is "_ \<longleftrightarrow> ?rhs")
-  unfolding eventually_nhds by (auto dest!: open_orderD dest: open_interval_imp_open)
-
 lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   unfolding trivial_limit_def eventually_nhds by simp
 
@@ -838,6 +832,35 @@
   "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
   using tendstoI tendstoD by fast
 
+lemma order_tendstoI:
+  fixes y :: "_ :: order_topology"
+  assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
+  assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
+  shows "(f ---> y) F"
+proof (rule topological_tendstoI)
+  fix S assume "open S" "y \<in> S"
+  then show "eventually (\<lambda>x. f x \<in> S) F"
+    unfolding open_generated_order
+  proof induct
+    case (UN K)
+    then obtain k where "y \<in> k" "k \<in> K" by auto
+    with UN(2)[of k] show ?case
+      by (auto elim: eventually_elim1)
+  qed (insert assms, auto elim: eventually_elim2)
+qed
+
+lemma order_tendstoD:
+  fixes y :: "_ :: order_topology"
+  assumes y: "(f ---> y) F"
+  shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
+    and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
+  using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto
+
+lemma order_tendsto_iff: 
+  fixes f :: "_ \<Rightarrow> 'a :: order_topology"
+  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)"
+  by (metis order_tendstoI order_tendstoD)
+
 lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
   by (simp only: tendsto_iff Zfun_def dist_norm)
 
@@ -908,34 +931,18 @@
 qed
 
 lemma increasing_tendsto:
-  fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
+  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
       and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   shows "(f ---> l) F"
-proof (rule topological_tendstoI)
-  fix S assume "open S" "l \<in> S"
-  then show "eventually (\<lambda>x. f x \<in> S) F"
-  proof (induct rule: open_order_induct)
-    case (greaterThanLessThan a b) with en bdd show ?case
-      by (auto elim!: eventually_elim2)
-  qed (insert en bdd, auto elim!: eventually_elim1)
-qed
+  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
 
 lemma decreasing_tendsto:
-  fixes f :: "_ \<Rightarrow> 'a::linorder_topology"
+  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
       and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
   shows "(f ---> l) F"
-proof (rule topological_tendstoI)
-  fix S assume "open S" "l \<in> S"
-  then show "eventually (\<lambda>x. f x \<in> S) F"
-  proof (induct rule: open_order_induct)
-    case (greaterThanLessThan a b)
-    with en have "eventually (\<lambda>n. f n < b) F" by auto
-    with bdd show ?case
-      by eventually_elim (insert greaterThanLessThan, auto)
-  qed (insert en bdd, auto elim!: eventually_elim1)
-qed
+  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
 
 subsubsection {* Distance and norms *}
 
@@ -1039,20 +1046,16 @@
 qed
 
 lemma tendsto_sandwich:
-  fixes f g h :: "'a \<Rightarrow> 'b::linorder_topology"
+  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
   assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
   assumes lim: "(f ---> c) net" "(h ---> c) net"
   shows "(g ---> c) net"
-proof (rule topological_tendstoI)
-  fix S assume "open S" "c \<in> S"
-  from open_orderD[OF this] obtain T where "open_interval T" "c \<in> T" "T \<subseteq> S" by auto
-  with lim[THEN topological_tendstoD, of T]
-  have "eventually (\<lambda>x. f x \<in> T) net" "eventually (\<lambda>x. h x \<in> T) net"
-    by (auto dest: open_interval_imp_open)
-  with ev have "eventually (\<lambda>x. g x \<in> T) net"
-    by eventually_elim (insert `open_interval T`, auto dest: open_intervalD)
-  with `T \<subseteq> S` show "eventually (\<lambda>x. g x \<in> S) net"
-    by (auto elim: eventually_elim1)
+proof (rule order_tendstoI)
+  fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
+    using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
+next
+  fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
+    using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
 qed
 
 lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
@@ -1129,15 +1132,12 @@
   shows "y \<le> x"
 proof (rule ccontr)
   assume "\<not> y \<le> x"
-  then have "x < y" by simp
-  from less_separate[OF this] obtain a b where xy: "x \<in> {..<a}" "y \<in> {b <..}" "{..<a} \<inter> {b<..} = {}"
-    by auto
-  then have less: "\<And>x y. x < a \<Longrightarrow> b < y \<Longrightarrow> x < y"
-    by auto
-  from x[THEN topological_tendstoD, of "{..<a}"] y[THEN topological_tendstoD, of "{b <..}"] xy
-  have "eventually (\<lambda>x. f x \<in> {..<a}) F" "eventually (\<lambda>x. g x \<in> {b <..}) F" by auto
+  with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
+    by (auto simp: not_le)
+  then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
+    using x y by (auto intro: order_tendstoD)
   with ev have "eventually (\<lambda>x. False) F"
-    by eventually_elim (auto dest!: less)
+    by eventually_elim (insert xy, fastforce)
   with F show False
     by (simp add: eventually_False)
 qed
diff -r 1cf4faed8b22 -r 78de6c7e8a58 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Wed Feb 06 17:18:01 2013 +0100
+++ b/src/HOL/RealVector.thy	Wed Feb 06 17:57:21 2013 +0100
@@ -559,60 +559,6 @@
     by (simp add: closed_Int)
 qed
 
-inductive open_interval :: "'a::order set \<Rightarrow> bool" where
-  empty[intro]: "open_interval {}" |
-  UNIV[intro]: "open_interval UNIV" |
-  greaterThan[intro]: "open_interval {a <..}" |
-  lessThan[intro]: "open_interval {..< b}" |
-  greaterThanLessThan[intro]: "open_interval {a <..< b}"
-hide_fact (open) empty UNIV greaterThan lessThan greaterThanLessThan
-
-lemma open_intervalD:
-  "open_interval S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> S"
-  by (cases rule: open_interval.cases) auto
-
-lemma open_interval_Int[intro]:
-  fixes S T :: "'a :: linorder set"
-  assumes S: "open_interval S" and T: "open_interval T"
-  shows "open_interval (S \<inter> T)"
-proof -
-  { fix a b :: 'a have "{..<b} \<inter> {a<..} = { a <..} \<inter> {..< b }" by auto } note this[simp]
-  { fix a b :: 'a and A have "{a <..} \<inter> ({b <..} \<inter> A) = {max a b <..} \<inter> A" by auto } note this[simp]
-  { fix a b :: 'a and A have "{..<b} \<inter> (A \<inter> {..<a}) = A \<inter> {..<min a b}" by auto } note this[simp]
-  { fix a b :: 'a have "open_interval ({ a <..} \<inter> {..< b})"
-      unfolding greaterThanLessThan_eq[symmetric] by auto } note this[simp]
-  show ?thesis
-    by (cases rule: open_interval.cases[OF S, case_product open_interval.cases[OF T]])
-       (auto simp: greaterThanLessThan_eq lessThan_Int_lessThan greaterThan_Int_greaterThan Int_assoc)
-qed
-
-lemma open_interval_imp_open: "open_interval S \<Longrightarrow> open (S::'a::order_topology set)"
-  by (cases S rule: open_interval.cases) auto
-
-lemma open_orderD:
-  "open (S::'a::linorder_topology set) \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>T. open_interval T \<and> T \<subseteq> S \<and> x \<in> T"
-  unfolding open_generated_order
-proof (induct rule: generate_topology.induct)
-  case (UN K) then obtain k where "k \<in> K" "x \<in> k" by auto
-  with UN(2)[of k] show ?case by auto
-qed auto
-
-lemma open_order_induct[consumes 2, case_names subset UNIV lessThan greaterThan greaterThanLessThan]:
-  fixes S :: "'a::linorder_topology set"
-  assumes S: "open S" "x \<in> S"
-  assumes subset: "\<And>S T. P S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> P T"
-  assumes univ: "P UNIV"
-  assumes lt: "\<And>a. x < a \<Longrightarrow> P {..< a}"
-  assumes gt: "\<And>a. a < x \<Longrightarrow> P {a <..}"
-  assumes lgt: "\<And>a b. a < x \<Longrightarrow> x < b \<Longrightarrow> P {a <..< b}"
-  shows "P S"
-proof -
-  from open_orderD[OF S] obtain T where "open_interval T" "T \<subseteq> S" "x \<in> T"
-    by auto
-  then show "P S"
-    by induct (auto intro: univ subset lt gt lgt)
-qed
-
 subsection {* Metric spaces *}
 
 class dist =