# HG changeset patch
# User hoelzl
# Date 1403094692 -7200
# Node ID 49c51eeaa62341381330b2cd4593fd53ebcaf826
# Parent  0ddb5b755cdc7d126fb09cfca57960f740fdadae
filters are easier to define with INF on filters.

diff -r 0ddb5b755cdc -r 49c51eeaa623 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Jun 18 07:31:12 2014 +0200
+++ b/src/HOL/Limits.thy	Wed Jun 18 14:31:32 2014 +0200
@@ -3,7 +3,6 @@
     Author:     Jacques D. Fleuriot, University of Cambridge
     Author:     Lawrence C Paulson
     Author:     Jeremy Avigad
-
 *)
 
 header {* Limits on Real Vector Spaces *}
@@ -15,43 +14,27 @@
 subsection {* Filter going to infinity norm *}
 
 definition at_infinity :: "'a::real_normed_vector filter" where
-  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
+  "at_infinity = (INF r. principal {x. r \<le> norm x})"
 
-lemma eventually_at_infinity:
-  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
-unfolding at_infinity_def
-proof (rule eventually_Abs_filter, rule is_filter.intro)
-  fix P Q :: "'a \<Rightarrow> bool"
-  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
-  then obtain r s where
-    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
-  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
-  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
-qed auto
+lemma eventually_at_infinity: "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
+  unfolding at_infinity_def
+  by (subst eventually_INF_base)
+     (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
 
 lemma at_infinity_eq_at_top_bot:
   "(at_infinity \<Colon> real filter) = sup at_top at_bot"
-  unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
-proof (intro arg_cong[where f=Abs_filter] ext iffI)
-  fix P :: "real \<Rightarrow> bool"
-  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
-  then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
-  then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
-  then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
-next
-  fix P :: "real \<Rightarrow> bool"
-  assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
-  then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
-  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
-    by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
-qed
+  apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity
+                   eventually_at_top_linorder eventually_at_bot_linorder)
+  apply safe
+  apply (rule_tac x="b" in exI, simp)
+  apply (rule_tac x="- b" in exI, simp)
+  apply (rule_tac x="max (- Na) N" in exI, auto simp: abs_real_def)
+  done
 
-lemma at_top_le_at_infinity:
-  "at_top \<le> (at_infinity :: real filter)"
+lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)"
   unfolding at_infinity_eq_at_top_bot by simp
 
-lemma at_bot_le_at_infinity:
-  "at_bot \<le> (at_infinity :: real filter)"
+lemma at_bot_le_at_infinity: "at_bot \<le> (at_infinity :: real filter)"
   unfolding at_infinity_eq_at_top_bot by simp
 
 lemma filterlim_at_top_imp_at_infinity:
diff -r 0ddb5b755cdc -r 49c51eeaa623 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 07:31:12 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 14:31:32 2014 +0200
@@ -3262,38 +3262,6 @@
 
 text{*Compactness expressed with filters*}
 
-definition "filter_from_subbase B = Abs_filter (\<lambda>P. \<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
-
-lemma eventually_filter_from_subbase:
-  "eventually P (filter_from_subbase B) \<longleftrightarrow> (\<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
-    (is "_ \<longleftrightarrow> ?R P")
-  unfolding filter_from_subbase_def
-proof (rule eventually_Abs_filter is_filter.intro)+
-  show "?R (\<lambda>x. True)"
-    by (rule exI[of _ "{}"]) (simp add: le_fun_def)
-next
-  fix P Q
-  assume "?R P" then guess X ..
-  moreover
-  assume "?R Q" then guess Y ..
-  ultimately show "?R (\<lambda>x. P x \<and> Q x)"
-    by (intro exI[of _ "X \<union> Y"]) auto
-next
-  fix P Q
-  assume "?R P" then guess X ..
-  moreover assume "\<forall>x. P x \<longrightarrow> Q x"
-  ultimately show "?R Q"
-    by (intro exI[of _ X]) auto
-qed
-
-lemma eventually_filter_from_subbaseI: "P \<in> B \<Longrightarrow> eventually P (filter_from_subbase B)"
-  by (subst eventually_filter_from_subbase) (auto intro!: exI[of _ "{P}"])
-
-lemma filter_from_subbase_not_bot:
-  "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot"
-  unfolding trivial_limit_def eventually_filter_from_subbase
-    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
-
 lemma closure_iff_nhds_not_empty:
   "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
 proof safe
@@ -3360,34 +3328,31 @@
 next
   fix A
   assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
-  def P' \<equiv> "(\<lambda>a (x::'a). x \<in> a)"
-  then have inj_P': "\<And>A. inj_on P' A"
-    by (auto intro!: inj_onI simp: fun_eq_iff)
-  def F \<equiv> "filter_from_subbase (P' ` insert U A)"
+  def F \<equiv> "INF a:insert U A. principal a"
   have "F \<noteq> bot"
     unfolding F_def
-  proof (safe intro!: filter_from_subbase_not_bot)
-    fix X
-    assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
-    then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
-      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq)
-    with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}"
+  proof (rule INF_filter_not_bot)
+    fix X assume "X \<subseteq> insert U A" "finite X"
+    moreover with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
       by auto
-    with B show False
-      by (auto simp: P'_def fun_eq_iff)
+    ultimately show "(INF a:X. principal a) \<noteq> bot"
+      by (auto simp add: INF_principal_finite principal_eq_bot_iff)
   qed
-  moreover have "eventually (\<lambda>x. x \<in> U) F"
-    unfolding F_def by (rule eventually_filter_from_subbaseI) (auto simp: P'_def)
+  moreover
+  have "F \<le> principal U"
+    unfolding F_def by auto
+  then have "eventually (\<lambda>x. x \<in> U) F"
+    by (auto simp: le_filter_def eventually_principal)
   moreover
   assume "\<forall>F. F \<noteq> bot \<longrightarrow> eventually (\<lambda>x. x \<in> U) F \<longrightarrow> (\<exists>x\<in>U. inf (nhds x) F \<noteq> bot)"
   ultimately obtain x where "x \<in> U" and x: "inf (nhds x) F \<noteq> bot"
     by auto
 
-  {
-    fix V
-    assume "V \<in> A"
+  { fix V assume "V \<in> A"
+    then have "F \<le> principal V"
+      unfolding F_def by (intro INF_lower2[of V]) auto
     then have V: "eventually (\<lambda>x. x \<in> V) F"
-      by (auto simp add: F_def image_iff P'_def intro!: eventually_filter_from_subbaseI)
+      by (auto simp: le_filter_def eventually_principal)
     have "x \<in> closure V"
       unfolding closure_iff_nhds_not_empty
     proof (intro impI allI)
diff -r 0ddb5b755cdc -r 49c51eeaa623 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 07:31:12 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 14:31:32 2014 +0200
@@ -875,40 +875,19 @@
 subsection {* The almost everywhere filter (i.e.\ quantifier) *}
 
 definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
-  "ae_filter M = Abs_filter (\<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)"
+  "ae_filter M = (INF N:null_sets M. principal (space M - N))"
 
-abbreviation
-  almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   "almost_everywhere M P \<equiv> eventually P (ae_filter M)"
 
 syntax
   "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
 
 translations
-  "AE x in M. P" == "CONST almost_everywhere M (%x. P)"
+  "AE x in M. P" == "CONST almost_everywhere M (\<lambda>x. P)"
 
-lemma eventually_ae_filter:
-  fixes M P
-  defines [simp]: "F \<equiv> \<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N" 
-  shows "eventually P (ae_filter M) \<longleftrightarrow> F P"
-  unfolding ae_filter_def F_def[symmetric]
-proof (rule eventually_Abs_filter)
-  show "is_filter F"
-  proof
-    fix P Q assume "F P" "F Q"
-    then obtain N L where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N"
-      and L: "L \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> L"
-      by auto
-    then have "L \<union> N \<in> null_sets M" "{x \<in> space M. \<not> (P x \<and> Q x)} \<subseteq> L \<union> N" by auto
-    then show "F (\<lambda>x. P x \<and> Q x)" by auto
-  next
-    fix P Q assume "F P"
-    then obtain N where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N" by auto
-    moreover assume "\<forall>x. P x \<longrightarrow> Q x"
-    ultimately have "N \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> N" by auto
-    then show "F Q" by auto
-  qed auto
-qed
+lemma eventually_ae_filter: "eventually P (ae_filter M) \<longleftrightarrow> (\<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)"
+  unfolding ae_filter_def by (subst eventually_INF_base) (auto simp: eventually_principal subset_eq)
 
 lemma AE_I':
   "N \<in> null_sets M \<Longrightarrow> {x\<in>space M. \<not> P x} \<subseteq> N \<Longrightarrow> (AE x in M. P x)"
diff -r 0ddb5b755cdc -r 49c51eeaa623 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 14:31:32 2014 +0200
@@ -1862,3 +1862,4 @@
 qed
 
 end
+
diff -r 0ddb5b755cdc -r 49c51eeaa623 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Jun 18 14:31:32 2014 +0200
@@ -530,6 +530,86 @@
 lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
   by (cases P) (simp_all add: eventually_False)
 
+lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
+proof -
+  let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
+  
+  { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
+    proof (rule eventually_Abs_filter is_filter.intro)+
+      show "?F (\<lambda>x. True)"
+        by (rule exI[of _ "{}"]) (simp add: le_fun_def)
+    next
+      fix P Q
+      assume "?F P" then guess X ..
+      moreover
+      assume "?F Q" then guess Y ..
+      ultimately show "?F (\<lambda>x. P x \<and> Q x)"
+        by (intro exI[of _ "X \<union> Y"])
+           (auto simp: Inf_union_distrib eventually_inf)
+    next
+      fix P Q
+      assume "?F P" then guess X ..
+      moreover assume "\<forall>x. P x \<longrightarrow> Q x"
+      ultimately show "?F Q"
+        by (intro exI[of _ X]) (auto elim: eventually_elim1)
+    qed }
+  note eventually_F = this
+
+  have "Inf B = Abs_filter ?F"
+  proof (intro antisym Inf_greatest)
+    show "Inf B \<le> Abs_filter ?F"
+      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
+  next
+    fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
+      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
+  qed
+  then show ?thesis
+    by (simp add: eventually_F)
+qed
+
+lemma eventually_INF: "eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (INF b:X. F b))"
+  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
+  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
+
+lemma Inf_filter_not_bot:
+  fixes B :: "'a filter set"
+  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
+  unfolding trivial_limit_def eventually_Inf[of _ B]
+    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
+
+lemma INF_filter_not_bot:
+  fixes F :: "'i \<Rightarrow> 'a filter"
+  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> (INF b:X. F b) \<noteq> bot) \<Longrightarrow> (INF b:B. F b) \<noteq> bot"
+  unfolding trivial_limit_def eventually_INF[of _ B]
+    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
+
+lemma eventually_Inf_base:
+  assumes "B \<noteq> {}" and base: "\<And>F G. F \<in> B \<Longrightarrow> G \<in> B \<Longrightarrow> \<exists>x\<in>B. x \<le> inf F G"
+  shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
+proof (subst eventually_Inf, safe)
+  fix X assume "finite X" "X \<subseteq> B"
+  then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
+  proof induct
+    case empty then show ?case
+      using `B \<noteq> {}` by auto
+  next
+    case (insert x X)
+    then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
+      by auto
+    with `insert x X \<subseteq> B` base[of b x] show ?case
+      by (auto intro: order_trans)
+  qed
+  then obtain b where "b \<in> B" "b \<le> Inf X"
+    by (auto simp: le_Inf_iff)
+  then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
+    by (intro bexI[of _ b]) (auto simp: le_filter_def)
+qed (auto intro!: exI[of _ "{x}" for x])
+
+lemma eventually_INF_base:
+  "B \<noteq> {} \<Longrightarrow> (\<And>a b. a \<in> B \<Longrightarrow> b \<in> B \<Longrightarrow> \<exists>x\<in>B. F x \<le> inf (F a) (F b)) \<Longrightarrow>
+    eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
+  unfolding INF_def by (subst eventually_Inf_base) auto
+
 
 subsubsection {* Map function for filters *}
 
@@ -560,124 +640,26 @@
 lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
   by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
 
-subsubsection {* Order filters *}
-
-definition at_top :: "('a::order) filter"
-  where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
-
-lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
-  unfolding at_top_def
-proof (rule eventually_Abs_filter, rule is_filter.intro)
-  fix P Q :: "'a \<Rightarrow> bool"
-  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
-  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
-  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
-  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
-qed auto
-
-lemma eventually_ge_at_top:
-  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
-  unfolding eventually_at_top_linorder by auto
-
-lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
-  unfolding eventually_at_top_linorder
-proof safe
-  fix N assume "\<forall>n\<ge>N. P n"
-  then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
-next
-  fix N assume "\<forall>n>N. P n"
-  moreover obtain y where "N < y" using gt_ex[of N] ..
-  ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
+lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
+  by (auto simp: le_filter_def eventually_filtermap eventually_inf)
+
+lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
+proof -
+  { fix X :: "'c set" assume "finite X"
+    then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
+    proof induct
+      case (insert x X)
+      have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
+        by (rule order_trans[OF _ filtermap_inf]) simp
+      also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
+        by (intro inf_mono insert order_refl)
+      finally show ?case
+        by simp
+    qed simp }
+  then show ?thesis
+    unfolding le_filter_def eventually_filtermap
+    by (subst (1 2) eventually_INF) auto
 qed
-
-lemma eventually_gt_at_top:
-  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
-  unfolding eventually_at_top_dense by auto
-
-definition at_bot :: "('a::order) filter"
-  where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"
-
-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
-proof (rule eventually_Abs_filter, rule is_filter.intro)
-  fix P Q :: "'a \<Rightarrow> bool"
-  assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n"
-  then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto
-  then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp
-  then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..
-qed auto
-
-lemma eventually_le_at_bot:
-  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
-  unfolding eventually_at_bot_linorder by auto
-
-lemma eventually_at_bot_dense:
-  fixes P :: "'a::unbounded_dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
-  unfolding eventually_at_bot_linorder
-proof safe
-  fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
-next
-  fix N assume "\<forall>n<N. P n" 
-  moreover obtain y where "y < N" using lt_ex[of N] ..
-  ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
-qed
-
-lemma eventually_gt_at_bot:
-  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
-  unfolding eventually_at_bot_dense by auto
-
-lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
-  unfolding trivial_limit_def
-  by (metis eventually_at_bot_linorder order_refl)
-
-lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
-  unfolding trivial_limit_def
-  by (metis eventually_at_top_linorder order_refl)
-
-subsection {* Sequentially *}
-
-abbreviation sequentially :: "nat filter"
-  where "sequentially == at_top"
-
-lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
-  unfolding at_top_def by simp
-
-lemma eventually_sequentially:
-  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
-  by (rule eventually_at_top_linorder)
-
-lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
-  unfolding filter_eq_iff eventually_sequentially by auto
-
-lemmas trivial_limit_sequentially = sequentially_bot
-
-lemma eventually_False_sequentially [simp]:
-  "\<not> eventually (\<lambda>n. False) sequentially"
-  by (simp add: eventually_False)
-
-lemma le_sequentially:
-  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
-  unfolding le_filter_def eventually_sequentially
-  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
-
-lemma eventually_sequentiallyI:
-  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
-  shows "eventually P sequentially"
-using assms by (auto simp: eventually_sequentially)
-
-lemma eventually_sequentially_seg:
-  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
-  unfolding eventually_sequentially
-  apply safe
-   apply (rule_tac x="N + k" in exI)
-   apply rule
-   apply (erule_tac x="n - k" in allE)
-   apply auto []
-  apply (rule_tac x=N in exI)
-  apply auto []
-  done
-
 subsubsection {* Standard filters *}
 
 definition principal :: "'a set \<Rightarrow> 'a filter" where
@@ -696,6 +678,9 @@
 lemma principal_empty[simp]: "principal {} = bot"
   by (auto simp: filter_eq_iff eventually_principal)
 
+lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
+  by (auto simp add: filter_eq_iff eventually_principal)
+
 lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
   by (auto simp: le_filter_def eventually_principal)
 
@@ -719,13 +704,122 @@
 lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
   unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
 
+lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
+  by (induct X rule: finite_induct) auto
+
 lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
   unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
 
+subsubsection {* Order filters *}
+
+definition at_top :: "('a::order) filter"
+  where "at_top = (INF k. principal {k ..})"
+
+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)
+
+lemma eventually_ge_at_top:
+  "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)"
+    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+  also have "(INF k. principal {k::'a <..}) = at_top"
+    unfolding at_top_def 
+    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
+  finally show ?thesis .
+qed
+
+lemma eventually_gt_at_top:
+  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
+  unfolding eventually_at_top_dense by auto
+
+definition at_bot :: "('a::order) filter"
+  where "at_bot = (INF k. principal {.. k})"
+
+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
+  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+
+lemma eventually_le_at_bot:
+  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
+  unfolding eventually_at_bot_linorder by auto
+
+lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
+proof -
+  have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
+    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+  also have "(INF k. principal {..< k::'a}) = at_bot"
+    unfolding at_bot_def 
+    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
+  finally show ?thesis .
+qed
+
+lemma eventually_gt_at_bot:
+  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
+  unfolding eventually_at_bot_dense by auto
+
+lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
+  unfolding trivial_limit_def
+  by (metis eventually_at_bot_linorder order_refl)
+
+lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
+  unfolding trivial_limit_def
+  by (metis eventually_at_top_linorder order_refl)
+
+subsection {* Sequentially *}
+
+abbreviation sequentially :: "nat filter"
+  where "sequentially \<equiv> at_top"
+
+lemma eventually_sequentially:
+  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
+  by (rule eventually_at_top_linorder)
+
+lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
+  unfolding filter_eq_iff eventually_sequentially by auto
+
+lemmas trivial_limit_sequentially = sequentially_bot
+
+lemma eventually_False_sequentially [simp]:
+  "\<not> eventually (\<lambda>n. False) sequentially"
+  by (simp add: eventually_False)
+
+lemma le_sequentially:
+  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
+  by (simp add: at_top_def le_INF_iff le_principal)
+
+lemma eventually_sequentiallyI:
+  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
+  shows "eventually P sequentially"
+using assms by (auto simp: eventually_sequentially)
+
+lemma eventually_sequentially_seg:
+  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
+  unfolding eventually_sequentially
+  apply safe
+   apply (rule_tac x="N + k" in exI)
+   apply rule
+   apply (erule_tac x="n - k" in allE)
+   apply auto []
+  apply (rule_tac x=N in exI)
+  apply auto []
+  done
+
 subsubsection {* Topological filters *}
 
 definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
-  where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
+  where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)"
 
 definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
   where "at a within s = inf (nhds a) (principal (s - {a}))"
@@ -741,21 +835,7 @@
 
 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
-proof (rule eventually_Abs_filter, rule is_filter.intro)
-  have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
-  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" ..
-next
-  fix P Q
-  assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
-     and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)"
-  then obtain S T where
-    "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
-    "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto
-  hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"
-    by (simp add: open_Int)
-  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" ..
-qed auto
+  unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
 
 lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   unfolding trivial_limit_def eventually_nhds by simp
@@ -893,6 +973,10 @@
   "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   unfolding filterlim_def by simp
 
+lemma filterlim_INF:
+  "(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_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   unfolding filterlim_def filtermap_filtermap ..
 
@@ -933,13 +1017,7 @@
 
 lemma (in topological_space) tendsto_def:
    "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
-  unfolding filterlim_def
-proof safe
-  fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
-  then show "eventually (\<lambda>x. f x \<in> S) F"
-    unfolding eventually_nhds eventually_filtermap le_filter_def
-    by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
-qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
+   unfolding nhds_def filterlim_INF filterlim_principal by auto
 
 lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   unfolding tendsto_def le_filter_def by fast
@@ -1120,7 +1198,7 @@
 
 subsubsection {* Rules about @{const Lim} *}
 
-lemma (in t2_space) tendsto_Lim:
+lemma tendsto_Lim:
   "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
   unfolding Lim_def using tendsto_unique[of net f] by auto
 
@@ -1565,9 +1643,7 @@
   unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
 
 lemma limI: "X ----> L ==> lim X = L"
-apply (simp add: lim_def)
-apply (blast intro: LIMSEQ_unique)
-done
+  by (rule tendsto_Lim) (rule trivial_limit_sequentially)
 
 lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
   using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
@@ -1767,6 +1843,7 @@
   fix X assume X: "\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a" "X ----> a"
   show "eventually (\<lambda>n. P (X n)) sequentially"
   proof (rule ccontr)
+
     assume "\<not> eventually (\<lambda>n. P (X n)) sequentially"
     from not_eventually_sequentiallyD[OF this]
     obtain r where "subseq r" "\<And>n. \<not> P (X (r n))"