# HG changeset patch
# User hoelzl
# Date 1404135925 -7200
# Node ID 159e45728ceb34f4c3e6b3e137228b91b938be63
# Parent  87429bdecad513d8923e563a610038bb6f81e6d9
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

diff -r 87429bdecad5 -r 159e45728ceb src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Mon Jun 30 15:45:21 2014 +0200
+++ b/src/HOL/Complete_Lattices.thy	Mon Jun 30 15:45:25 2014 +0200
@@ -415,6 +415,15 @@
   then show ?thesis by simp
 qed
 
+lemma INF_inf_const1:
+  "I \<noteq> {} \<Longrightarrow> (INF i:I. inf x (f i)) = inf x (INF i:I. f i)"
+  by (intro antisym INF_greatest inf_mono order_refl INF_lower)
+     (auto intro: INF_lower2 le_infI2 intro!: INF_mono)
+
+lemma INF_inf_const2:
+  "I \<noteq> {} \<Longrightarrow> (INF i:I. inf (f i) x) = inf (INF i:I. f i) x"
+  using INF_inf_const1[of I x f] by (simp add: inf_commute)
+
 lemma INF_constant:
   "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
   by simp
diff -r 87429bdecad5 -r 159e45728ceb src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Mon Jun 30 15:45:21 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Jun 30 15:45:25 2014 +0200
@@ -99,14 +99,14 @@
 by (fast elim: someI)
 
 lemma dependent_nat_choice:
-  assumes  1: "\<exists>x. P x" and 
-           2: "\<And>x n. P x \<Longrightarrow> \<exists>y. P y \<and> Q n x y"
-  shows "\<exists>f. \<forall>n. P (f n) \<and> Q n (f n) (f (Suc n))"
+  assumes  1: "\<exists>x. P 0 x" and 
+           2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
+  shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
 proof (intro exI allI conjI)
-  fix n def f \<equiv> "rec_nat (SOME x. P x) (\<lambda>n x. SOME y. P y \<and> Q n x y)"
-  then have "P (f 0)" "\<And>n. P (f n) \<Longrightarrow> P (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
+  fix n def f \<equiv> "rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
+  have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
     using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def)
-  then show "P (f n)" "Q n (f n) (f (Suc n))"
+  then show "P n (f n)" "Q n (f n) (f (Suc n))"
     by (induct n) auto
 qed
 
diff -r 87429bdecad5 -r 159e45728ceb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 30 15:45:21 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 30 15:45:25 2014 +0200
@@ -4616,41 +4616,31 @@
   using continuous_within_eps_delta [of x UNIV f] by simp
 
 lemma continuous_at_right_real_increasing:
-  assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
-  shows "(continuous (at_right (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f (a + delta) - f a < e)"
-  apply (auto simp add: continuous_within_eps_delta dist_real_def greaterThan_def)
-  apply (drule_tac x = e in spec, auto)
-  apply (drule_tac x = "a + d / 2" in spec)
-  apply (subst (asm) abs_of_nonneg)
-  apply (auto intro: nondecF simp add: field_simps)
-  apply (rule_tac x = "d / 2" in exI)
-  apply (auto simp add: field_simps)
-  apply (drule_tac x = e in spec, auto)
-  apply (rule_tac x = delta in exI, auto)
-  apply (subst abs_of_nonneg)
-  apply (auto intro: nondecF simp add: field_simps)
-  apply (rule le_less_trans)
-  prefer 2 apply assumption
-by (rule nondecF, auto)
+  fixes f :: "real \<Rightarrow> real"
+  assumes nondecF: "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y"
+  shows "continuous (at_right a) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f (a + d) - f a < e)"
+  apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
+  apply (intro all_cong ex_cong)
+  apply safe
+  apply (erule_tac x="a + d" in allE)
+  apply simp
+  apply (simp add: nondecF field_simps)
+  apply (drule nondecF)
+  apply simp
+  done
 
 lemma continuous_at_left_real_increasing:
   assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
   shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
-  apply (auto simp add: continuous_within_eps_delta dist_real_def lessThan_def)
-  apply (drule_tac x = e in spec, auto)
-  apply (drule_tac x = "a - d / 2" in spec)
-  apply (subst (asm) abs_of_nonpos)
-  apply (auto intro: nondecF simp add: field_simps)
-  apply (rule_tac x = "d / 2" in exI)
-  apply (auto simp add: field_simps)
-  apply (drule_tac x = e in spec, auto)
-  apply (rule_tac x = delta in exI, auto)
-  apply (subst abs_of_nonpos)
-  apply (auto intro: nondecF simp add: field_simps)
-  apply (rule less_le_trans)
-  apply assumption
-  apply auto
-by (rule nondecF, auto)
+  apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
+  apply (intro all_cong ex_cong)
+  apply safe
+  apply (erule_tac x="a - d" in allE)
+  apply simp
+  apply (simp add: nondecF field_simps)
+  apply (cut_tac x="a - d" and y="x" in nondecF)
+  apply simp_all
+  done
 
 text{* Versions in terms of open balls. *}
 
diff -r 87429bdecad5 -r 159e45728ceb src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Jun 30 15:45:21 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jun 30 15:45:25 2014 +0200
@@ -1466,18 +1466,31 @@
 
 subsection {* Filters and Limits on Metric Space *}
 
-lemma eventually_nhds_metric:
-  fixes a :: "'a :: metric_space"
-  shows "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
-unfolding eventually_nhds open_dist
-apply safe
-apply fast
-apply (rule_tac x="{x. dist x a < d}" in exI, simp)
-apply clarsimp
-apply (rule_tac x="d - dist x a" in exI, clarsimp)
-apply (simp only: less_diff_eq)
-apply (erule le_less_trans [OF dist_triangle])
-done
+lemma (in metric_space) nhds_metric: "nhds x = (INF e:{0 <..}. principal {y. dist y x < e})"
+  unfolding nhds_def
+proof (safe intro!: INF_eq)
+  fix S assume "open S" "x \<in> S"
+  then obtain e where "{y. dist y x < e} \<subseteq> S" "0 < e"
+    by (auto simp: open_dist subset_eq)
+  then show "\<exists>e\<in>{0<..}. principal {y. dist y x < e} \<le> principal S"
+    by auto
+qed (auto intro!: exI[of _ "{y. dist x y < e}" for e] open_ball simp: dist_commute)
+
+lemma (in metric_space) tendsto_iff:
+  "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
+  unfolding nhds_metric filterlim_INF filterlim_principal by auto
+
+lemma (in metric_space) tendstoI: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f ---> l) F"
+  by (auto simp: tendsto_iff)
+
+lemma (in metric_space) tendstoD: "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
+  by (auto simp: tendsto_iff)
+
+lemma (in metric_space) eventually_nhds_metric:
+  "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
+  unfolding nhds_metric
+  by (subst eventually_INF_base)
+     (auto simp: eventually_principal Bex_def subset_eq intro: exI[of _ "min a b" for a b])
 
 lemma eventually_at:
   fixes a :: "'a :: metric_space"
@@ -1493,34 +1506,6 @@
   apply auto
   done
 
-lemma tendstoI:
-  fixes l :: "'a :: metric_space"
-  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
-  shows "(f ---> l) F"
-  apply (rule topological_tendstoI)
-  apply (simp add: open_dist)
-  apply (drule (1) bspec, clarify)
-  apply (drule assms)
-  apply (erule eventually_elim1, simp)
-  done
-
-lemma tendstoD:
-  fixes l :: "'a :: metric_space"
-  shows "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
-  apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
-  apply (clarsimp simp add: open_dist)
-  apply (rule_tac x="e - dist x l" in exI, clarsimp)
-  apply (simp only: less_diff_eq)
-  apply (erule le_less_trans [OF dist_triangle])
-  apply simp
-  apply simp
-  done
-
-lemma tendsto_iff:
-  fixes l :: "'a :: metric_space"
-  shows "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
-  using tendstoI tendstoD by fast
-
 lemma metric_tendsto_imp_tendsto:
   fixes a :: "'a :: metric_space" and b :: "'b :: metric_space"
   assumes f: "(f ---> a) F"
@@ -1786,49 +1771,31 @@
   fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
   assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) ----> y"
   shows "(f ---> y) at_top"
-  unfolding filterlim_iff
-proof safe
-  fix P assume "eventually P (nhds y)"
-  then have seq: "\<And>f. f ----> y \<Longrightarrow> eventually (\<lambda>x. P (f x)) at_top"
-    unfolding eventually_nhds_iff_sequentially by simp
-
-  show "eventually (\<lambda>x. P (f x)) at_top"
-  proof (rule ccontr)
-    assume "\<not> eventually (\<lambda>x. P (f x)) at_top"
-    then have "\<And>X. \<exists>x>X. \<not> P (f x)"
-      unfolding eventually_at_top_dense by simp
-    then obtain r where not_P: "\<And>x. \<not> P (f (r x))" and r: "\<And>x. x < r x"
-      by metis
-    
-    def s \<equiv> "rec_nat (r 0) (\<lambda>_ x. r (x + 1))"
-    then have [simp]: "s 0 = r 0" "\<And>n. s (Suc n) = r (s n + 1)"
-      by auto
-
-    { fix n have "n < s n" using r
-        by (induct n) (auto simp add: real_of_nat_Suc intro: less_trans add_strict_right_mono) }
-    note s_subseq = this
+proof -
+  from nhds_countable[of y] guess A . note A = this
 
-    have "mono s"
-    proof (rule incseq_SucI)
-      fix n show "s n \<le> s (Suc n)"
-        using r[of "s n + 1"] by simp
-    qed
-
-    have "filterlim s at_top sequentially"
-      unfolding filterlim_at_top_gt[where c=0] eventually_sequentially
-    proof (safe intro!: exI)
-      fix Z :: real and n assume "0 < Z" "natceiling Z \<le> n"
-      with real_natceiling_ge[of Z] `n < s n`
-      show "Z \<le> s n"
-        by auto
-    qed
-    moreover then have "eventually (\<lambda>x. P (f (s x))) sequentially"
-      by (rule seq[OF *])
-    then obtain n where "P (f (s n))"
-      by (auto simp: eventually_sequentially)
-    then show False
-      using not_P by (cases n) auto
+  have "\<forall>m. \<exists>k. \<forall>x\<ge>k. f x \<in> A m"
+  proof (rule ccontr)
+    assume "\<not> (\<forall>m. \<exists>k. \<forall>x\<ge>k. f x \<in> A m)"
+    then obtain m where "\<And>k. \<exists>x\<ge>k. f x \<notin> A m"
+      by auto
+    then have "\<exists>X. \<forall>n. (f (X n) \<notin> A m) \<and> max n (X n) + 1 \<le> X (Suc n)"
+      by (intro dependent_nat_choice) (auto simp del: max.bounded_iff)
+    then obtain X where X: "\<And>n. f (X n) \<notin> A m" "\<And>n. max n (X n) + 1 \<le> X (Suc n)"
+      by auto
+    { fix n have "1 \<le> n \<longrightarrow> real n \<le> X n"
+        using X[of "n - 1"] by auto }
+    then have "filterlim X at_top sequentially"
+      by (force intro!: filterlim_at_top_mono[OF filterlim_real_sequentially]
+                simp: eventually_sequentially)
+    from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
+      by auto
   qed
+  then obtain k where "\<And>m x. k m \<le> x \<Longrightarrow> f x \<in> A m"
+    by metis
+  then show ?thesis
+    unfolding at_top_def A
+    by (intro filterlim_base[where i=k]) auto
 qed
 
 lemma tendsto_at_topI_sequentially_real:
diff -r 87429bdecad5 -r 159e45728ceb src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jun 30 15:45:21 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Jun 30 15:45:25 2014 +0200
@@ -175,6 +175,12 @@
   shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
   by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
 
+lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a"
+  by auto
+
+lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b"
+  by auto
+
 subsection {*Two-sided intervals*}
 
 context ord
diff -r 87429bdecad5 -r 159e45728ceb src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Jun 30 15:45:21 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Jun 30 15:45:25 2014 +0200
@@ -757,6 +757,9 @@
 definition at_top :: "('a::order) filter"
   where "at_top = (INF k. principal {k ..})"
 
+lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
+  by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
+
 lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
   unfolding at_top_def
   by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
@@ -765,12 +768,6 @@
   "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   unfolding eventually_at_top_linorder by auto
 
-lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a"
-  by auto
-
-lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b"
-  by auto
-
 lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
 proof -
   have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
@@ -788,6 +785,9 @@
 definition at_bot :: "('a::order) filter"
   where "at_bot = (INF k. principal {.. k})"
 
+lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
+  by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
+
 lemma eventually_at_bot_linorder:
   fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
   unfolding at_bot_def
@@ -875,6 +875,16 @@
 abbreviation (in order_topology) at_left :: "'a \<Rightarrow> 'a filter" where
   "at_left x \<equiv> at x within {..< x}"
 
+lemma (in topological_space) nhds_generated_topology:
+  "open = generate_topology T \<Longrightarrow> nhds x = (INF S:{S\<in>T. x \<in> S}. principal S)"
+  unfolding nhds_def
+proof (safe intro!: antisym INF_greatest)
+  fix S assume "generate_topology T S" "x \<in> S"
+  then show "(INF S:{S \<in> T. x \<in> S}. principal S) \<le> principal S"
+    by induction 
+       (auto intro: INF_lower order_trans simp add: inf_principal[symmetric] simp del: inf_principal)
+qed (auto intro!: INF_lower intro: generate_topology.intros)
+
 lemma (in topological_space) eventually_nhds:
   "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
@@ -882,6 +892,9 @@
 lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   unfolding trivial_limit_def eventually_nhds by simp
 
+lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
+  unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib)
+
 lemma eventually_at_filter:
   "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
   unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute)
@@ -910,39 +923,48 @@
 lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
   by (simp add: at_eq_bot_iff not_open_singleton)
 
-lemma eventually_at_right:
-  fixes x :: "'a :: linorder_topology"
-  assumes gt_ex: "x < y"
-  shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
-  unfolding eventually_at_topological
-proof safe
-  note gt_ex
-  moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
-  moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
-  ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
-    by (auto simp: subset_eq Ball_def)
-next
-  fix b assume "x < b" "\<forall>z. x < z \<and> z < b \<longrightarrow> P z"
-  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)"
-    by (intro exI[of _ "{..< b}"]) auto
+lemma (in order_topology) nhds_order: "nhds x =
+  inf (INF a:{x <..}. principal {..< a}) (INF a:{..< x}. principal {a <..})"
+proof -
+  have 1: "{S \<in> range lessThan \<union> range greaterThan. x \<in> S} = 
+      (\<lambda>a. {..< a}) ` {x <..} \<union> (\<lambda>a. {a <..}) ` {..< x}"
+    by auto
+  show ?thesis
+    unfolding nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def ..
 qed
 
-lemma eventually_at_left:
-  fixes x :: "'a :: linorder_topology"
-  assumes lt_ex: "y < x"
-  shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
-  unfolding eventually_at_topological
-proof safe
-  note lt_ex
-  moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
-  moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
-  ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
-    by (auto simp: subset_eq Ball_def)
-next
-  fix b assume "b < x" "\<forall>z. b < z \<and> z < x \<longrightarrow> P z"
-  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s)"
-    by (intro exI[of _ "{b <..}"]) auto
-qed
+lemma (in linorder_topology) at_within_order: "UNIV \<noteq> {x} \<Longrightarrow> 
+  at x within s = inf (INF a:{x <..}. principal ({..< a} \<inter> s - {x}))
+                      (INF a:{..< x}. principal ({a <..} \<inter> s - {x}))"
+proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split[case_product case_split])
+  assume "UNIV \<noteq> {x}" "{x<..} = {}" "{..< x} = {}"
+  moreover have "UNIV = {..< x} \<union> {x} \<union> {x <..}"
+    by auto
+  ultimately show ?thesis
+    by auto
+qed (auto simp: at_within_def nhds_order Int_Diff inf_principal[symmetric] INF_inf_const2
+                inf_sup_aci[where 'a="'a filter"]
+          simp del: inf_principal)
+
+lemma (in linorder_topology) at_left_eq:
+  "y < x \<Longrightarrow> at_left x = (INF a:{..< x}. principal {a <..< x})"
+  by (subst at_within_order)
+     (auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant
+           intro!: INF_lower2 inf_absorb2)
+
+lemma (in linorder_topology) eventually_at_left:
+  "y < x \<Longrightarrow> eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
+  unfolding at_left_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)
+
+lemma (in linorder_topology) at_right_eq:
+  "x < y \<Longrightarrow> at_right x = (INF a:{x <..}. principal {x <..< a})"
+  by (subst at_within_order)
+     (auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute
+           intro!: INF_lower2 inf_absorb1)
+
+lemma (in linorder_topology) eventually_at_right:
+  "x < y \<Longrightarrow> eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
+  unfolding at_right_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)
 
 lemma trivial_limit_at_right_top: "at_right (top::_::{order_top, linorder_topology}) = bot"
   unfolding filter_eq_iff eventually_at_topological by auto
@@ -1029,6 +1051,26 @@
   "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
   unfolding filterlim_def le_INF_iff ..
 
+lemma filterlim_INF_INF:
+  "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (INF i:I. F i). f x :> (INF j:J. G j)"
+  unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
+
+lemma filterlim_base:
+  "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow> 
+    LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
+  by (force intro!: filterlim_INF_INF simp: image_subset_iff)
+
+lemma filterlim_base_iff: 
+  assumes "I \<noteq> {}" and chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> F i \<subseteq> F j \<or> F j \<subseteq> F i"
+  shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
+    (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
+  unfolding filterlim_INF filterlim_principal
+proof (subst eventually_INF_base)
+  fix i j assume "i \<in> I" "j \<in> I"
+  with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
+    by auto
+qed (auto simp: eventually_principal `I \<noteq> {}`)
+
 lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   unfolding filterlim_def filtermap_filtermap ..
 
@@ -1096,40 +1138,25 @@
   "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
   unfolding tendsto_def by auto
 
-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"
+lemma (in order_topology) order_tendsto_iff:
+  "(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)"
+  unfolding nhds_order filterlim_inf filterlim_INF filterlim_principal by auto
+
+lemma (in order_topology) order_tendstoI:
+  "(\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F) \<Longrightarrow> (\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F) \<Longrightarrow>
+    (f ---> y) F"
+  unfolding order_tendsto_iff by auto
+
+lemma (in order_topology) order_tendstoD:
+  assumes "(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)
+  using assms unfolding order_tendsto_iff by auto
 
 lemma tendsto_bot [simp]: "(f ---> a) bot"
   unfolding tendsto_def by simp
 
-lemma tendsto_max:
-  fixes x y :: "'a::linorder_topology"
+lemma (in linorder_topology) tendsto_max:
   assumes X: "(X ---> x) net"
   assumes Y: "(Y ---> y) net"
   shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
@@ -1145,8 +1172,7 @@
     by (auto simp: eventually_conj_iff)
 qed
 
-lemma tendsto_min:
-  fixes x y :: "'a::linorder_topology"
+lemma (in linorder_topology) tendsto_min:
   assumes X: "(X ---> x) net"
   assumes Y: "(Y ---> y) net"
   shows "((\<lambda>x. min (X x) (Y x)) ---> min x y) net"
@@ -1162,7 +1188,6 @@
     by (auto simp: min_less_iff_disj elim: eventually_elim1)
 qed
 
-
 lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
   unfolding tendsto_def eventually_at_topological by auto
 
@@ -1170,7 +1195,7 @@
   by (simp add: tendsto_def)
 
 lemma (in t2_space) tendsto_unique:
-  assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
+  assumes "F \<noteq> bot" and "(f ---> a) F" and "(f ---> b) F"
   shows "a = b"
 proof (rule ccontr)
   assume "a \<noteq> b"
@@ -1271,6 +1296,11 @@
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
   by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
 
+lemma filterlim_at_top_mono:
+  "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
+    LIM x F. g x :> at_top"
+  by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
+
 lemma filterlim_at_top_dense:
   fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
@@ -1280,12 +1310,7 @@
 lemma filterlim_at_top_ge:
   fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
-  unfolding filterlim_at_top
-proof safe
-  fix Z assume *: "\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F"
-  with *[THEN spec, of "max Z c"] show "eventually (\<lambda>x. Z \<le> f x) F"
-    by (auto elim!: eventually_elim1)
-qed simp
+  unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
 
 lemma filterlim_at_top_at_top:
   fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
@@ -1546,45 +1571,30 @@
 text{* for any sequence, there is a monotonic subsequence *}
 lemma seq_monosub:
   fixes s :: "nat => 'a::linorder"
-  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
+  shows "\<exists>f. subseq f \<and> monoseq (\<lambda>n. (s (f n)))"
 proof cases
-  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
-  assume *: "\<forall>n. \<exists>p. ?P p n"
-  def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
-  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
-  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
-  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
-  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
-  then have "subseq f" unfolding subseq_Suc_iff by auto
-  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
-  proof (intro disjI2 allI)
-    fix n show "s (f (Suc n)) \<le> s (f n)"
-    proof (cases n)
-      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
-    next
-      case (Suc m)
-      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
-      with P_Suc Suc show ?thesis by simp
-    qed
-  qed
-  ultimately show ?thesis by auto
+  assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. s m \<le> s p"
+  then have "\<exists>f. \<forall>n. (\<forall>m\<ge>f n. s m \<le> s (f n)) \<and> f n < f (Suc n)"
+    by (intro dependent_nat_choice) (auto simp: conj_commute)
+  then obtain f where "subseq f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
+    by (auto simp: subseq_Suc_iff)
+  moreover 
+  then have "incseq f"
+    unfolding subseq_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
+  then have "monoseq (\<lambda>n. s (f n))"
+    by (auto simp add: incseq_def intro!: mono monoI2)
+  ultimately show ?thesis
+    by auto
 next
-  let "?P p m" = "m < p \<and> s m < s p"
   assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
   then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
-  def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
-  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
-  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat.rec(2) ..
-  have P_0: "?P (f 0) (Suc N)"
-    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
-  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
-      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
-  note P' = this
-  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
-      by (induct i) (insert P_0 P', auto) }
-  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
-    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
-  then show ?thesis by auto
+  have "\<exists>f. \<forall>n. N < f n \<and> f n < f (Suc n) \<and> s (f n) \<le> s (f (Suc n))"
+  proof (intro dependent_nat_choice)
+    fix x assume "N < x" with N[of x] show "\<exists>y>N. x < y \<and> s x \<le> s y"
+      by (auto intro: less_trans)
+  qed auto
+  then show ?thesis
+    by (auto simp: monoseq_iff incseq_Suc_iff subseq_Suc_iff)
 qed
 
 lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
@@ -1768,6 +1778,30 @@
   qed
 qed
 
+lemma (in first_countable_topology) nhds_countable:
+  obtains X :: "nat \<Rightarrow> 'a set"
+  where "decseq X" "\<And>n. open (X n)" "\<And>n. x \<in> X n" "nhds x = (INF n. principal (X n))"
+proof -
+  from first_countable_basis obtain A :: "nat \<Rightarrow> 'a set"
+    where A: "\<And>n. x \<in> A n" "\<And>n. open (A n)" "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>i. A i \<subseteq> S"
+    by metis
+  show thesis
+  proof
+    show "decseq (\<lambda>n. \<Inter>i\<le>n. A i)"
+      by (auto simp: decseq_def)
+    show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
+      using A by auto
+    show "nhds x = (INF n. principal (\<Inter> i\<le>n. A i))"
+      using A unfolding nhds_def
+      apply (intro INF_eq)
+      apply simp_all
+      apply force
+      apply (intro exI[of _ "\<Inter> i\<le>n. A i" for n] conjI open_INT)
+      apply auto
+      done
+  qed
+qed
+
 lemma (in first_countable_topology) countable_basis:
   obtains A :: "nat \<Rightarrow> 'a set" where
     "\<And>i. open (A i)" "\<And>i. x \<in> A i"