author hoelzl Wed Jun 18 14:31:32 2014 +0200 (2014-06-18) changeset 57276 49c51eeaa623 parent 57275 0ddb5b755cdc child 57277 31b35f5a5fdb
filters are easier to define with INF on filters.
 src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Probability/Measure_Space.thy file | annotate | diff | revisions src/HOL/Real_Vector_Spaces.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions
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.10  header {* Limits on Real Vector Spaces *}
1.11 @@ -15,43 +14,27 @@
1.12  subsection {* Filter going to infinity norm *}
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.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.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.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.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.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.5  text{*Compactness expressed with filters*}
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.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.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.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.15  syntax
3.16    "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
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.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.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.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.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.88  subsubsection {* Map function for filters *}
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.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.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.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.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.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.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.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.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.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.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.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.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.188 -subsection {* Sequentially *}
5.190 -abbreviation sequentially :: "nat filter"
5.191 -  where "sequentially == at_top"
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.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.200 -lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
5.201 -  unfolding filter_eq_iff eventually_sequentially by auto
5.203 -lemmas trivial_limit_sequentially = sequentially_bot
5.205 -lemma eventually_False_sequentially [simp]:
5.206 -  "\<not> eventually (\<lambda>n. False) sequentially"
5.207 -  by (simp add: eventually_False)
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.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.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.231  subsubsection {* Standard filters *}
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.238 +lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
5.239 +  by (auto simp add: filter_eq_iff eventually_principal)
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.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.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.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.254 +subsubsection {* Order filters *}
5.256 +definition at_top :: "('a::order) filter"
5.257 +  where "at_top = (INF k. principal {k ..})"
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.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.267 +lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a"
5.268 +  by auto
5.270 +lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b"
5.271 +  by auto
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.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.287 +definition at_bot :: "('a::order) filter"
5.288 +  where "at_bot = (INF k. principal {.. k})"
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.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.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.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.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.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.321 +subsection {* Sequentially *}
5.323 +abbreviation sequentially :: "nat filter"
5.324 +  where "sequentially \<equiv> at_top"
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.330 +lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
5.331 +  unfolding filter_eq_iff eventually_sequentially by auto
5.333 +lemmas trivial_limit_sequentially = sequentially_bot
5.335 +lemma eventually_False_sequentially [simp]:
5.336 +  "\<not> eventually (\<lambda>n. False) sequentially"
5.337 +  by (simp add: eventually_False)
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.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.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.360  subsubsection {* Topological filters *}
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.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.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.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.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.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.402 @@ -933,13 +1017,7 @@
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.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.419  subsubsection {* Rules about @{const Lim} *}
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.426 @@ -1565,9 +1643,7 @@
5.427    unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
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.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.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))"