filters are easier to define with INF on filters.
authorhoelzl
Wed Jun 18 14:31:32 2014 +0200 (2014-06-18)
changeset 5727649c51eeaa623
parent 57275 0ddb5b755cdc
child 57277 31b35f5a5fdb
filters are easier to define with INF on filters.
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Limits.thy	Wed Jun 18 07:31:12 2014 +0200
     1.2 +++ b/src/HOL/Limits.thy	Wed Jun 18 14:31:32 2014 +0200
     1.3 @@ -3,7 +3,6 @@
     1.4      Author:     Jacques D. Fleuriot, University of Cambridge
     1.5      Author:     Lawrence C Paulson
     1.6      Author:     Jeremy Avigad
     1.7 -
     1.8  *)
     1.9  
    1.10  header {* Limits on Real Vector Spaces *}
    1.11 @@ -15,43 +14,27 @@
    1.12  subsection {* Filter going to infinity norm *}
    1.13  
    1.14  definition at_infinity :: "'a::real_normed_vector filter" where
    1.15 -  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
    1.16 +  "at_infinity = (INF r. principal {x. r \<le> norm x})"
    1.17  
    1.18 -lemma eventually_at_infinity:
    1.19 -  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
    1.20 -unfolding at_infinity_def
    1.21 -proof (rule eventually_Abs_filter, rule is_filter.intro)
    1.22 -  fix P Q :: "'a \<Rightarrow> bool"
    1.23 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
    1.24 -  then obtain r s where
    1.25 -    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
    1.26 -  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
    1.27 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
    1.28 -qed auto
    1.29 +lemma eventually_at_infinity: "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
    1.30 +  unfolding at_infinity_def
    1.31 +  by (subst eventually_INF_base)
    1.32 +     (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
    1.33  
    1.34  lemma at_infinity_eq_at_top_bot:
    1.35    "(at_infinity \<Colon> real filter) = sup at_top at_bot"
    1.36 -  unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
    1.37 -proof (intro arg_cong[where f=Abs_filter] ext iffI)
    1.38 -  fix P :: "real \<Rightarrow> bool"
    1.39 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    1.40 -  then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
    1.41 -  then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
    1.42 -  then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
    1.43 -next
    1.44 -  fix P :: "real \<Rightarrow> bool"
    1.45 -  assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
    1.46 -  then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
    1.47 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    1.48 -    by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
    1.49 -qed
    1.50 +  apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity
    1.51 +                   eventually_at_top_linorder eventually_at_bot_linorder)
    1.52 +  apply safe
    1.53 +  apply (rule_tac x="b" in exI, simp)
    1.54 +  apply (rule_tac x="- b" in exI, simp)
    1.55 +  apply (rule_tac x="max (- Na) N" in exI, auto simp: abs_real_def)
    1.56 +  done
    1.57  
    1.58 -lemma at_top_le_at_infinity:
    1.59 -  "at_top \<le> (at_infinity :: real filter)"
    1.60 +lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)"
    1.61    unfolding at_infinity_eq_at_top_bot by simp
    1.62  
    1.63 -lemma at_bot_le_at_infinity:
    1.64 -  "at_bot \<le> (at_infinity :: real filter)"
    1.65 +lemma at_bot_le_at_infinity: "at_bot \<le> (at_infinity :: real filter)"
    1.66    unfolding at_infinity_eq_at_top_bot by simp
    1.67  
    1.68  lemma filterlim_at_top_imp_at_infinity:
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 07:31:12 2014 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 14:31:32 2014 +0200
     2.3 @@ -3262,38 +3262,6 @@
     2.4  
     2.5  text{*Compactness expressed with filters*}
     2.6  
     2.7 -definition "filter_from_subbase B = Abs_filter (\<lambda>P. \<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
     2.8 -
     2.9 -lemma eventually_filter_from_subbase:
    2.10 -  "eventually P (filter_from_subbase B) \<longleftrightarrow> (\<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
    2.11 -    (is "_ \<longleftrightarrow> ?R P")
    2.12 -  unfolding filter_from_subbase_def
    2.13 -proof (rule eventually_Abs_filter is_filter.intro)+
    2.14 -  show "?R (\<lambda>x. True)"
    2.15 -    by (rule exI[of _ "{}"]) (simp add: le_fun_def)
    2.16 -next
    2.17 -  fix P Q
    2.18 -  assume "?R P" then guess X ..
    2.19 -  moreover
    2.20 -  assume "?R Q" then guess Y ..
    2.21 -  ultimately show "?R (\<lambda>x. P x \<and> Q x)"
    2.22 -    by (intro exI[of _ "X \<union> Y"]) auto
    2.23 -next
    2.24 -  fix P Q
    2.25 -  assume "?R P" then guess X ..
    2.26 -  moreover assume "\<forall>x. P x \<longrightarrow> Q x"
    2.27 -  ultimately show "?R Q"
    2.28 -    by (intro exI[of _ X]) auto
    2.29 -qed
    2.30 -
    2.31 -lemma eventually_filter_from_subbaseI: "P \<in> B \<Longrightarrow> eventually P (filter_from_subbase B)"
    2.32 -  by (subst eventually_filter_from_subbase) (auto intro!: exI[of _ "{P}"])
    2.33 -
    2.34 -lemma filter_from_subbase_not_bot:
    2.35 -  "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot"
    2.36 -  unfolding trivial_limit_def eventually_filter_from_subbase
    2.37 -    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
    2.38 -
    2.39  lemma closure_iff_nhds_not_empty:
    2.40    "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
    2.41  proof safe
    2.42 @@ -3360,34 +3328,31 @@
    2.43  next
    2.44    fix A
    2.45    assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
    2.46 -  def P' \<equiv> "(\<lambda>a (x::'a). x \<in> a)"
    2.47 -  then have inj_P': "\<And>A. inj_on P' A"
    2.48 -    by (auto intro!: inj_onI simp: fun_eq_iff)
    2.49 -  def F \<equiv> "filter_from_subbase (P' ` insert U A)"
    2.50 +  def F \<equiv> "INF a:insert U A. principal a"
    2.51    have "F \<noteq> bot"
    2.52      unfolding F_def
    2.53 -  proof (safe intro!: filter_from_subbase_not_bot)
    2.54 -    fix X
    2.55 -    assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
    2.56 -    then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
    2.57 -      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq)
    2.58 -    with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}"
    2.59 +  proof (rule INF_filter_not_bot)
    2.60 +    fix X assume "X \<subseteq> insert U A" "finite X"
    2.61 +    moreover with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
    2.62        by auto
    2.63 -    with B show False
    2.64 -      by (auto simp: P'_def fun_eq_iff)
    2.65 +    ultimately show "(INF a:X. principal a) \<noteq> bot"
    2.66 +      by (auto simp add: INF_principal_finite principal_eq_bot_iff)
    2.67    qed
    2.68 -  moreover have "eventually (\<lambda>x. x \<in> U) F"
    2.69 -    unfolding F_def by (rule eventually_filter_from_subbaseI) (auto simp: P'_def)
    2.70 +  moreover
    2.71 +  have "F \<le> principal U"
    2.72 +    unfolding F_def by auto
    2.73 +  then have "eventually (\<lambda>x. x \<in> U) F"
    2.74 +    by (auto simp: le_filter_def eventually_principal)
    2.75    moreover
    2.76    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)"
    2.77    ultimately obtain x where "x \<in> U" and x: "inf (nhds x) F \<noteq> bot"
    2.78      by auto
    2.79  
    2.80 -  {
    2.81 -    fix V
    2.82 -    assume "V \<in> A"
    2.83 +  { fix V assume "V \<in> A"
    2.84 +    then have "F \<le> principal V"
    2.85 +      unfolding F_def by (intro INF_lower2[of V]) auto
    2.86      then have V: "eventually (\<lambda>x. x \<in> V) F"
    2.87 -      by (auto simp add: F_def image_iff P'_def intro!: eventually_filter_from_subbaseI)
    2.88 +      by (auto simp: le_filter_def eventually_principal)
    2.89      have "x \<in> closure V"
    2.90        unfolding closure_iff_nhds_not_empty
    2.91      proof (intro impI allI)
     3.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 07:31:12 2014 +0200
     3.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Jun 18 14:31:32 2014 +0200
     3.3 @@ -875,40 +875,19 @@
     3.4  subsection {* The almost everywhere filter (i.e.\ quantifier) *}
     3.5  
     3.6  definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
     3.7 -  "ae_filter M = Abs_filter (\<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)"
     3.8 +  "ae_filter M = (INF N:null_sets M. principal (space M - N))"
     3.9  
    3.10 -abbreviation
    3.11 -  almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    3.12 +abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    3.13    "almost_everywhere M P \<equiv> eventually P (ae_filter M)"
    3.14  
    3.15  syntax
    3.16    "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
    3.17  
    3.18  translations
    3.19 -  "AE x in M. P" == "CONST almost_everywhere M (%x. P)"
    3.20 +  "AE x in M. P" == "CONST almost_everywhere M (\<lambda>x. P)"
    3.21  
    3.22 -lemma eventually_ae_filter:
    3.23 -  fixes M P
    3.24 -  defines [simp]: "F \<equiv> \<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N" 
    3.25 -  shows "eventually P (ae_filter M) \<longleftrightarrow> F P"
    3.26 -  unfolding ae_filter_def F_def[symmetric]
    3.27 -proof (rule eventually_Abs_filter)
    3.28 -  show "is_filter F"
    3.29 -  proof
    3.30 -    fix P Q assume "F P" "F Q"
    3.31 -    then obtain N L where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N"
    3.32 -      and L: "L \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> L"
    3.33 -      by auto
    3.34 -    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
    3.35 -    then show "F (\<lambda>x. P x \<and> Q x)" by auto
    3.36 -  next
    3.37 -    fix P Q assume "F P"
    3.38 -    then obtain N where N: "N \<in> null_sets M" "{x \<in> space M. \<not> P x} \<subseteq> N" by auto
    3.39 -    moreover assume "\<forall>x. P x \<longrightarrow> Q x"
    3.40 -    ultimately have "N \<in> null_sets M" "{x \<in> space M. \<not> Q x} \<subseteq> N" by auto
    3.41 -    then show "F Q" by auto
    3.42 -  qed auto
    3.43 -qed
    3.44 +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)"
    3.45 +  unfolding ae_filter_def by (subst eventually_INF_base) (auto simp: eventually_principal subset_eq)
    3.46  
    3.47  lemma AE_I':
    3.48    "N \<in> null_sets M \<Longrightarrow> {x\<in>space M. \<not> P x} \<subseteq> N \<Longrightarrow> (AE x in M. P x)"
     4.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
     4.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 14:31:32 2014 +0200
     4.3 @@ -1862,3 +1862,4 @@
     4.4  qed
     4.5  
     4.6  end
     4.7 +
     5.1 --- a/src/HOL/Topological_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
     5.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Jun 18 14:31:32 2014 +0200
     5.3 @@ -530,6 +530,86 @@
     5.4  lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
     5.5    by (cases P) (simp_all add: eventually_False)
     5.6  
     5.7 +lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
     5.8 +proof -
     5.9 +  let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
    5.10 +  
    5.11 +  { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
    5.12 +    proof (rule eventually_Abs_filter is_filter.intro)+
    5.13 +      show "?F (\<lambda>x. True)"
    5.14 +        by (rule exI[of _ "{}"]) (simp add: le_fun_def)
    5.15 +    next
    5.16 +      fix P Q
    5.17 +      assume "?F P" then guess X ..
    5.18 +      moreover
    5.19 +      assume "?F Q" then guess Y ..
    5.20 +      ultimately show "?F (\<lambda>x. P x \<and> Q x)"
    5.21 +        by (intro exI[of _ "X \<union> Y"])
    5.22 +           (auto simp: Inf_union_distrib eventually_inf)
    5.23 +    next
    5.24 +      fix P Q
    5.25 +      assume "?F P" then guess X ..
    5.26 +      moreover assume "\<forall>x. P x \<longrightarrow> Q x"
    5.27 +      ultimately show "?F Q"
    5.28 +        by (intro exI[of _ X]) (auto elim: eventually_elim1)
    5.29 +    qed }
    5.30 +  note eventually_F = this
    5.31 +
    5.32 +  have "Inf B = Abs_filter ?F"
    5.33 +  proof (intro antisym Inf_greatest)
    5.34 +    show "Inf B \<le> Abs_filter ?F"
    5.35 +      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
    5.36 +  next
    5.37 +    fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
    5.38 +      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
    5.39 +  qed
    5.40 +  then show ?thesis
    5.41 +    by (simp add: eventually_F)
    5.42 +qed
    5.43 +
    5.44 +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))"
    5.45 +  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
    5.46 +  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
    5.47 +
    5.48 +lemma Inf_filter_not_bot:
    5.49 +  fixes B :: "'a filter set"
    5.50 +  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
    5.51 +  unfolding trivial_limit_def eventually_Inf[of _ B]
    5.52 +    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
    5.53 +
    5.54 +lemma INF_filter_not_bot:
    5.55 +  fixes F :: "'i \<Rightarrow> 'a filter"
    5.56 +  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"
    5.57 +  unfolding trivial_limit_def eventually_INF[of _ B]
    5.58 +    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
    5.59 +
    5.60 +lemma eventually_Inf_base:
    5.61 +  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"
    5.62 +  shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
    5.63 +proof (subst eventually_Inf, safe)
    5.64 +  fix X assume "finite X" "X \<subseteq> B"
    5.65 +  then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
    5.66 +  proof induct
    5.67 +    case empty then show ?case
    5.68 +      using `B \<noteq> {}` by auto
    5.69 +  next
    5.70 +    case (insert x X)
    5.71 +    then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
    5.72 +      by auto
    5.73 +    with `insert x X \<subseteq> B` base[of b x] show ?case
    5.74 +      by (auto intro: order_trans)
    5.75 +  qed
    5.76 +  then obtain b where "b \<in> B" "b \<le> Inf X"
    5.77 +    by (auto simp: le_Inf_iff)
    5.78 +  then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
    5.79 +    by (intro bexI[of _ b]) (auto simp: le_filter_def)
    5.80 +qed (auto intro!: exI[of _ "{x}" for x])
    5.81 +
    5.82 +lemma eventually_INF_base:
    5.83 +  "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>
    5.84 +    eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
    5.85 +  unfolding INF_def by (subst eventually_Inf_base) auto
    5.86 +
    5.87  
    5.88  subsubsection {* Map function for filters *}
    5.89  
    5.90 @@ -560,124 +640,26 @@
    5.91  lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
    5.92    by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
    5.93  
    5.94 -subsubsection {* Order filters *}
    5.95 -
    5.96 -definition at_top :: "('a::order) filter"
    5.97 -  where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
    5.98 -
    5.99 -lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
   5.100 -  unfolding at_top_def
   5.101 -proof (rule eventually_Abs_filter, rule is_filter.intro)
   5.102 -  fix P Q :: "'a \<Rightarrow> bool"
   5.103 -  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
   5.104 -  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
   5.105 -  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
   5.106 -  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
   5.107 -qed auto
   5.108 -
   5.109 -lemma eventually_ge_at_top:
   5.110 -  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   5.111 -  unfolding eventually_at_top_linorder by auto
   5.112 -
   5.113 -lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"
   5.114 -  unfolding eventually_at_top_linorder
   5.115 -proof safe
   5.116 -  fix N assume "\<forall>n\<ge>N. P n"
   5.117 -  then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
   5.118 -next
   5.119 -  fix N assume "\<forall>n>N. P n"
   5.120 -  moreover obtain y where "N < y" using gt_ex[of N] ..
   5.121 -  ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
   5.122 +lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
   5.123 +  by (auto simp: le_filter_def eventually_filtermap eventually_inf)
   5.124 +
   5.125 +lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
   5.126 +proof -
   5.127 +  { fix X :: "'c set" assume "finite X"
   5.128 +    then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
   5.129 +    proof induct
   5.130 +      case (insert x X)
   5.131 +      have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
   5.132 +        by (rule order_trans[OF _ filtermap_inf]) simp
   5.133 +      also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
   5.134 +        by (intro inf_mono insert order_refl)
   5.135 +      finally show ?case
   5.136 +        by simp
   5.137 +    qed simp }
   5.138 +  then show ?thesis
   5.139 +    unfolding le_filter_def eventually_filtermap
   5.140 +    by (subst (1 2) eventually_INF) auto
   5.141  qed
   5.142 -
   5.143 -lemma eventually_gt_at_top:
   5.144 -  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
   5.145 -  unfolding eventually_at_top_dense by auto
   5.146 -
   5.147 -definition at_bot :: "('a::order) filter"
   5.148 -  where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"
   5.149 -
   5.150 -lemma eventually_at_bot_linorder:
   5.151 -  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
   5.152 -  unfolding at_bot_def
   5.153 -proof (rule eventually_Abs_filter, rule is_filter.intro)
   5.154 -  fix P Q :: "'a \<Rightarrow> bool"
   5.155 -  assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n"
   5.156 -  then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto
   5.157 -  then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp
   5.158 -  then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..
   5.159 -qed auto
   5.160 -
   5.161 -lemma eventually_le_at_bot:
   5.162 -  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   5.163 -  unfolding eventually_at_bot_linorder by auto
   5.164 -
   5.165 -lemma eventually_at_bot_dense:
   5.166 -  fixes P :: "'a::unbounded_dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
   5.167 -  unfolding eventually_at_bot_linorder
   5.168 -proof safe
   5.169 -  fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
   5.170 -next
   5.171 -  fix N assume "\<forall>n<N. P n" 
   5.172 -  moreover obtain y where "y < N" using lt_ex[of N] ..
   5.173 -  ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
   5.174 -qed
   5.175 -
   5.176 -lemma eventually_gt_at_bot:
   5.177 -  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   5.178 -  unfolding eventually_at_bot_dense by auto
   5.179 -
   5.180 -lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
   5.181 -  unfolding trivial_limit_def
   5.182 -  by (metis eventually_at_bot_linorder order_refl)
   5.183 -
   5.184 -lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
   5.185 -  unfolding trivial_limit_def
   5.186 -  by (metis eventually_at_top_linorder order_refl)
   5.187 -
   5.188 -subsection {* Sequentially *}
   5.189 -
   5.190 -abbreviation sequentially :: "nat filter"
   5.191 -  where "sequentially == at_top"
   5.192 -
   5.193 -lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
   5.194 -  unfolding at_top_def by simp
   5.195 -
   5.196 -lemma eventually_sequentially:
   5.197 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   5.198 -  by (rule eventually_at_top_linorder)
   5.199 -
   5.200 -lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   5.201 -  unfolding filter_eq_iff eventually_sequentially by auto
   5.202 -
   5.203 -lemmas trivial_limit_sequentially = sequentially_bot
   5.204 -
   5.205 -lemma eventually_False_sequentially [simp]:
   5.206 -  "\<not> eventually (\<lambda>n. False) sequentially"
   5.207 -  by (simp add: eventually_False)
   5.208 -
   5.209 -lemma le_sequentially:
   5.210 -  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   5.211 -  unfolding le_filter_def eventually_sequentially
   5.212 -  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
   5.213 -
   5.214 -lemma eventually_sequentiallyI:
   5.215 -  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   5.216 -  shows "eventually P sequentially"
   5.217 -using assms by (auto simp: eventually_sequentially)
   5.218 -
   5.219 -lemma eventually_sequentially_seg:
   5.220 -  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   5.221 -  unfolding eventually_sequentially
   5.222 -  apply safe
   5.223 -   apply (rule_tac x="N + k" in exI)
   5.224 -   apply rule
   5.225 -   apply (erule_tac x="n - k" in allE)
   5.226 -   apply auto []
   5.227 -  apply (rule_tac x=N in exI)
   5.228 -  apply auto []
   5.229 -  done
   5.230 -
   5.231  subsubsection {* Standard filters *}
   5.232  
   5.233  definition principal :: "'a set \<Rightarrow> 'a filter" where
   5.234 @@ -696,6 +678,9 @@
   5.235  lemma principal_empty[simp]: "principal {} = bot"
   5.236    by (auto simp: filter_eq_iff eventually_principal)
   5.237  
   5.238 +lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
   5.239 +  by (auto simp add: filter_eq_iff eventually_principal)
   5.240 +
   5.241  lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
   5.242    by (auto simp: le_filter_def eventually_principal)
   5.243  
   5.244 @@ -719,13 +704,122 @@
   5.245  lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
   5.246    unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
   5.247  
   5.248 +lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
   5.249 +  by (induct X rule: finite_induct) auto
   5.250 +
   5.251  lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
   5.252    unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
   5.253  
   5.254 +subsubsection {* Order filters *}
   5.255 +
   5.256 +definition at_top :: "('a::order) filter"
   5.257 +  where "at_top = (INF k. principal {k ..})"
   5.258 +
   5.259 +lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
   5.260 +  unfolding at_top_def
   5.261 +  by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   5.262 +
   5.263 +lemma eventually_ge_at_top:
   5.264 +  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   5.265 +  unfolding eventually_at_top_linorder by auto
   5.266 +
   5.267 +lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a"
   5.268 +  by auto
   5.269 +
   5.270 +lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b"
   5.271 +  by auto
   5.272 +
   5.273 +lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
   5.274 +proof -
   5.275 +  have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
   5.276 +    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   5.277 +  also have "(INF k. principal {k::'a <..}) = at_top"
   5.278 +    unfolding at_top_def 
   5.279 +    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
   5.280 +  finally show ?thesis .
   5.281 +qed
   5.282 +
   5.283 +lemma eventually_gt_at_top:
   5.284 +  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
   5.285 +  unfolding eventually_at_top_dense by auto
   5.286 +
   5.287 +definition at_bot :: "('a::order) filter"
   5.288 +  where "at_bot = (INF k. principal {.. k})"
   5.289 +
   5.290 +lemma eventually_at_bot_linorder:
   5.291 +  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
   5.292 +  unfolding at_bot_def
   5.293 +  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   5.294 +
   5.295 +lemma eventually_le_at_bot:
   5.296 +  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   5.297 +  unfolding eventually_at_bot_linorder by auto
   5.298 +
   5.299 +lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
   5.300 +proof -
   5.301 +  have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
   5.302 +    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   5.303 +  also have "(INF k. principal {..< k::'a}) = at_bot"
   5.304 +    unfolding at_bot_def 
   5.305 +    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
   5.306 +  finally show ?thesis .
   5.307 +qed
   5.308 +
   5.309 +lemma eventually_gt_at_bot:
   5.310 +  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   5.311 +  unfolding eventually_at_bot_dense by auto
   5.312 +
   5.313 +lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
   5.314 +  unfolding trivial_limit_def
   5.315 +  by (metis eventually_at_bot_linorder order_refl)
   5.316 +
   5.317 +lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
   5.318 +  unfolding trivial_limit_def
   5.319 +  by (metis eventually_at_top_linorder order_refl)
   5.320 +
   5.321 +subsection {* Sequentially *}
   5.322 +
   5.323 +abbreviation sequentially :: "nat filter"
   5.324 +  where "sequentially \<equiv> at_top"
   5.325 +
   5.326 +lemma eventually_sequentially:
   5.327 +  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   5.328 +  by (rule eventually_at_top_linorder)
   5.329 +
   5.330 +lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   5.331 +  unfolding filter_eq_iff eventually_sequentially by auto
   5.332 +
   5.333 +lemmas trivial_limit_sequentially = sequentially_bot
   5.334 +
   5.335 +lemma eventually_False_sequentially [simp]:
   5.336 +  "\<not> eventually (\<lambda>n. False) sequentially"
   5.337 +  by (simp add: eventually_False)
   5.338 +
   5.339 +lemma le_sequentially:
   5.340 +  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   5.341 +  by (simp add: at_top_def le_INF_iff le_principal)
   5.342 +
   5.343 +lemma eventually_sequentiallyI:
   5.344 +  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   5.345 +  shows "eventually P sequentially"
   5.346 +using assms by (auto simp: eventually_sequentially)
   5.347 +
   5.348 +lemma eventually_sequentially_seg:
   5.349 +  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   5.350 +  unfolding eventually_sequentially
   5.351 +  apply safe
   5.352 +   apply (rule_tac x="N + k" in exI)
   5.353 +   apply rule
   5.354 +   apply (erule_tac x="n - k" in allE)
   5.355 +   apply auto []
   5.356 +  apply (rule_tac x=N in exI)
   5.357 +  apply auto []
   5.358 +  done
   5.359 +
   5.360  subsubsection {* Topological filters *}
   5.361  
   5.362  definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
   5.363 -  where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   5.364 +  where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)"
   5.365  
   5.366  definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
   5.367    where "at a within s = inf (nhds a) (principal (s - {a}))"
   5.368 @@ -741,21 +835,7 @@
   5.369  
   5.370  lemma (in topological_space) eventually_nhds:
   5.371    "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   5.372 -  unfolding nhds_def
   5.373 -proof (rule eventually_Abs_filter, rule is_filter.intro)
   5.374 -  have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
   5.375 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" ..
   5.376 -next
   5.377 -  fix P Q
   5.378 -  assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
   5.379 -     and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)"
   5.380 -  then obtain S T where
   5.381 -    "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
   5.382 -    "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto
   5.383 -  hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"
   5.384 -    by (simp add: open_Int)
   5.385 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" ..
   5.386 -qed auto
   5.387 +  unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
   5.388  
   5.389  lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   5.390    unfolding trivial_limit_def eventually_nhds by simp
   5.391 @@ -893,6 +973,10 @@
   5.392    "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   5.393    unfolding filterlim_def by simp
   5.394  
   5.395 +lemma filterlim_INF:
   5.396 +  "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
   5.397 +  unfolding filterlim_def le_INF_iff ..
   5.398 +
   5.399  lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   5.400    unfolding filterlim_def filtermap_filtermap ..
   5.401  
   5.402 @@ -933,13 +1017,7 @@
   5.403  
   5.404  lemma (in topological_space) tendsto_def:
   5.405     "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   5.406 -  unfolding filterlim_def
   5.407 -proof safe
   5.408 -  fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
   5.409 -  then show "eventually (\<lambda>x. f x \<in> S) F"
   5.410 -    unfolding eventually_nhds eventually_filtermap le_filter_def
   5.411 -    by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
   5.412 -qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
   5.413 +   unfolding nhds_def filterlim_INF filterlim_principal by auto
   5.414  
   5.415  lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   5.416    unfolding tendsto_def le_filter_def by fast
   5.417 @@ -1120,7 +1198,7 @@
   5.418  
   5.419  subsubsection {* Rules about @{const Lim} *}
   5.420  
   5.421 -lemma (in t2_space) tendsto_Lim:
   5.422 +lemma tendsto_Lim:
   5.423    "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
   5.424    unfolding Lim_def using tendsto_unique[of net f] by auto
   5.425  
   5.426 @@ -1565,9 +1643,7 @@
   5.427    unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
   5.428  
   5.429  lemma limI: "X ----> L ==> lim X = L"
   5.430 -apply (simp add: lim_def)
   5.431 -apply (blast intro: LIMSEQ_unique)
   5.432 -done
   5.433 +  by (rule tendsto_Lim) (rule trivial_limit_sequentially)
   5.434  
   5.435  lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
   5.436    using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
   5.437 @@ -1767,6 +1843,7 @@
   5.438    fix X assume X: "\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a" "X ----> a"
   5.439    show "eventually (\<lambda>n. P (X n)) sequentially"
   5.440    proof (rule ccontr)
   5.441 +
   5.442      assume "\<not> eventually (\<lambda>n. P (X n)) sequentially"
   5.443      from not_eventually_sequentiallyD[OF this]
   5.444      obtain r where "subseq r" "\<And>n. \<not> P (X (r n))"