author hoelzl Fri Mar 22 10:41:42 2013 +0100 (2013-03-22) changeset 51471 cad22a3cc09c parent 51470 a981a5c8a505 child 51472 adb441e4b9e9
move topological_space to its own theory
 src/HOL/Lim.thy file | annotate | diff | revisions src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/RealVector.thy file | annotate | diff | revisions src/HOL/SEQ.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Lim.thy	Thu Mar 21 16:58:14 2013 +0100
1.2 +++ b/src/HOL/Lim.thy	Fri Mar 22 10:41:42 2013 +0100
1.3 @@ -10,28 +10,12 @@
1.4  imports SEQ
1.5  begin
1.6
1.7 -text{*Standard Definitions*}
1.8 -
1.9 -abbreviation
1.10 -  LIM :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a, 'b] \<Rightarrow> bool"
1.11 -        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
1.12 -  "f -- a --> L \<equiv> (f ---> L) (at a)"
1.13 -
1.14 -definition
1.15 -  isCont :: "['a::topological_space \<Rightarrow> 'b::topological_space, 'a] \<Rightarrow> bool" where
1.16 -  "isCont f a = (f -- a --> (f a))"
1.17 -
1.18  definition
1.19    isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
1.20    "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
1.21
1.22  subsection {* Limits of Functions *}
1.23
1.24 -lemma LIM_def: "f -- a --> L =
1.25 -     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
1.26 -        --> dist (f x) L < r)"
1.27 -unfolding tendsto_iff eventually_at ..
1.28 -
1.29  lemma metric_LIM_I:
1.30    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
1.31      \<Longrightarrow> f -- a --> L"
1.32 @@ -81,8 +65,6 @@
1.33    shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
1.34  by (drule_tac k="- a" in LIM_offset, simp)
1.35
1.36 -lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
1.37 -
1.38  lemma LIM_zero:
1.39    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.40    shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
1.41 @@ -114,36 +96,6 @@
1.42    by (rule metric_LIM_imp_LIM [OF f],
1.44
1.45 -lemma LIM_const_not_eq:
1.46 -  fixes a :: "'a::perfect_space"
1.47 -  fixes k L :: "'b::t2_space"
1.48 -  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
1.49 -  by (simp add: tendsto_const_iff)
1.50 -
1.51 -lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
1.52 -
1.53 -lemma LIM_const_eq:
1.54 -  fixes a :: "'a::perfect_space"
1.55 -  fixes k L :: "'b::t2_space"
1.56 -  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
1.57 -  by (simp add: tendsto_const_iff)
1.58 -
1.59 -lemma LIM_unique:
1.60 -  fixes a :: "'a::perfect_space"
1.61 -  fixes L M :: "'b::t2_space"
1.62 -  shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
1.63 -  using at_neq_bot by (rule tendsto_unique)
1.64 -
1.65 -text{*Limits are equal for functions equal except at limit point*}
1.66 -lemma LIM_equal:
1.67 -     "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
1.68 -unfolding tendsto_def eventually_at_topological by simp
1.69 -
1.70 -lemma LIM_cong:
1.71 -  "\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk>
1.72 -   \<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
1.74 -
1.75  lemma metric_LIM_equal2:
1.76    assumes 1: "0 < R"
1.77    assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
1.78 @@ -163,13 +115,6 @@
1.79    shows "g -- a --> l \<Longrightarrow> f -- a --> l"
1.80  by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
1.81
1.82 -lemma LIM_compose_eventually:
1.83 -  assumes f: "f -- a --> b"
1.84 -  assumes g: "g -- b --> c"
1.85 -  assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
1.86 -  shows "(\<lambda>x. g (f x)) -- a --> c"
1.87 -  using g f inj by (rule tendsto_compose_eventually)
1.88 -
1.89  lemma metric_LIM_compose2:
1.90    assumes f: "f -- a --> b"
1.91    assumes g: "g -- b --> c"
1.92 @@ -186,16 +131,13 @@
1.93    shows "(\<lambda>x. g (f x)) -- a --> c"
1.94  by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
1.95
1.96 -lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
1.97 -  unfolding o_def by (rule tendsto_compose)
1.98 -
1.99  lemma real_LIM_sandwich_zero:
1.100    fixes f g :: "'a::topological_space \<Rightarrow> real"
1.101    assumes f: "f -- a --> 0"
1.102    assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
1.103    assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
1.104    shows "g -- a --> 0"
1.105 -proof (rule LIM_imp_LIM [OF f])
1.106 +proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
1.107    fix x assume x: "x \<noteq> a"
1.108    have "norm (g x - 0) = g x" by (simp add: 1 x)
1.109    also have "g x \<le> f x" by (rule 2 [OF x])
1.110 @@ -217,12 +159,6 @@
1.111    shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
1.112  by (simp add: isCont_def LIM_isCont_iff)
1.113
1.114 -lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
1.115 -  unfolding isCont_def by (rule tendsto_ident_at)
1.116 -
1.117 -lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
1.118 -  unfolding isCont_def by (rule tendsto_const)
1.119 -
1.120  lemma isCont_norm [simp]:
1.121    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.122    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
1.123 @@ -263,10 +199,6 @@
1.124    shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
1.125    unfolding isCont_def by (rule tendsto_divide)
1.126
1.127 -lemma isCont_tendsto_compose:
1.128 -  "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
1.129 -  unfolding isCont_def by (rule tendsto_compose)
1.130 -
1.131  lemma metric_isCont_LIM_compose2:
1.132    assumes f [unfolded isCont_def]: "isCont f a"
1.133    assumes g: "g -- f a --> l"
1.134 @@ -282,12 +214,6 @@
1.135    shows "(\<lambda>x. g (f x)) -- a --> l"
1.136  by (rule LIM_compose2 [OF f g inj])
1.137
1.138 -lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
1.139 -  unfolding isCont_def by (rule tendsto_compose)
1.140 -
1.141 -lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
1.142 -  unfolding o_def by (rule isCont_o2)
1.143 -
1.144  lemma (in bounded_linear) isCont:
1.145    "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
1.146    unfolding isCont_def by (rule tendsto)
1.147 @@ -372,7 +298,7 @@
1.148    def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
1.149    assume "\<not> eventually P (at a within s)"
1.150    hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
1.151 -    unfolding Limits.eventually_within Limits.eventually_at by fast
1.152 +    unfolding eventually_within eventually_at by fast
1.153    hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
1.154    hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
1.155      unfolding F_def by (rule someI_ex)
```
```     2.1 --- a/src/HOL/Limits.thy	Thu Mar 21 16:58:14 2013 +0100
2.2 +++ b/src/HOL/Limits.thy	Fri Mar 22 10:41:42 2013 +0100
2.3 @@ -8,457 +8,9 @@
2.4  imports RealVector
2.5  begin
2.6
2.7 -subsection {* Filters *}
2.8 -
2.9 -text {*
2.10 -  This definition also allows non-proper filters.
2.11 -*}
2.12 -
2.13 -locale is_filter =
2.14 -  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
2.15 -  assumes True: "F (\<lambda>x. True)"
2.16 -  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
2.17 -  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
2.18 -
2.19 -typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
2.20 -proof
2.21 -  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
2.22 -qed
2.23 -
2.24 -lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
2.25 -  using Rep_filter [of F] by simp
2.26 -
2.27 -lemma Abs_filter_inverse':
2.28 -  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
2.29 -  using assms by (simp add: Abs_filter_inverse)
2.30 -
2.31 -
2.32 -subsection {* Eventually *}
2.33 -
2.34 -definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
2.35 -  where "eventually P F \<longleftrightarrow> Rep_filter F P"
2.36 -
2.37 -lemma eventually_Abs_filter:
2.38 -  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
2.39 -  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
2.40 -
2.41 -lemma filter_eq_iff:
2.42 -  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
2.43 -  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
2.44 -
2.45 -lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
2.46 -  unfolding eventually_def
2.47 -  by (rule is_filter.True [OF is_filter_Rep_filter])
2.48 -
2.49 -lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
2.50 -proof -
2.51 -  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
2.52 -  thus "eventually P F" by simp
2.53 -qed
2.54 -
2.55 -lemma eventually_mono:
2.56 -  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
2.57 -  unfolding eventually_def
2.58 -  by (rule is_filter.mono [OF is_filter_Rep_filter])
2.59 -
2.60 -lemma eventually_conj:
2.61 -  assumes P: "eventually (\<lambda>x. P x) F"
2.62 -  assumes Q: "eventually (\<lambda>x. Q x) F"
2.63 -  shows "eventually (\<lambda>x. P x \<and> Q x) F"
2.64 -  using assms unfolding eventually_def
2.65 -  by (rule is_filter.conj [OF is_filter_Rep_filter])
2.66 -
2.67 -lemma eventually_Ball_finite:
2.68 -  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
2.69 -  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
2.70 -using assms by (induct set: finite, simp, simp add: eventually_conj)
2.71 -
2.72 -lemma eventually_all_finite:
2.73 -  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
2.74 -  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
2.75 -  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
2.76 -using eventually_Ball_finite [of UNIV P] assms by simp
2.77 -
2.78 -lemma eventually_mp:
2.79 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
2.80 -  assumes "eventually (\<lambda>x. P x) F"
2.81 -  shows "eventually (\<lambda>x. Q x) F"
2.82 -proof (rule eventually_mono)
2.83 -  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
2.84 -  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
2.85 -    using assms by (rule eventually_conj)
2.86 -qed
2.87 -
2.88 -lemma eventually_rev_mp:
2.89 -  assumes "eventually (\<lambda>x. P x) F"
2.90 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
2.91 -  shows "eventually (\<lambda>x. Q x) F"
2.92 -using assms(2) assms(1) by (rule eventually_mp)
2.93 -
2.94 -lemma eventually_conj_iff:
2.95 -  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
2.96 -  by (auto intro: eventually_conj elim: eventually_rev_mp)
2.97 -
2.98 -lemma eventually_elim1:
2.99 -  assumes "eventually (\<lambda>i. P i) F"
2.100 -  assumes "\<And>i. P i \<Longrightarrow> Q i"
2.101 -  shows "eventually (\<lambda>i. Q i) F"
2.102 -  using assms by (auto elim!: eventually_rev_mp)
2.103 -
2.104 -lemma eventually_elim2:
2.105 -  assumes "eventually (\<lambda>i. P i) F"
2.106 -  assumes "eventually (\<lambda>i. Q i) F"
2.107 -  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
2.108 -  shows "eventually (\<lambda>i. R i) F"
2.109 -  using assms by (auto elim!: eventually_rev_mp)
2.110 -
2.111 -lemma eventually_subst:
2.112 -  assumes "eventually (\<lambda>n. P n = Q n) F"
2.113 -  shows "eventually P F = eventually Q F" (is "?L = ?R")
2.114 -proof -
2.115 -  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
2.116 -      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
2.117 -    by (auto elim: eventually_elim1)
2.118 -  then show ?thesis by (auto elim: eventually_elim2)
2.119 -qed
2.120 -
2.121 -ML {*
2.122 -  fun eventually_elim_tac ctxt thms thm =
2.123 -    let
2.124 -      val thy = Proof_Context.theory_of ctxt
2.125 -      val mp_thms = thms RL [@{thm eventually_rev_mp}]
2.126 -      val raw_elim_thm =
2.127 -        (@{thm allI} RS @{thm always_eventually})
2.128 -        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
2.129 -        |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
2.130 -      val cases_prop = prop_of (raw_elim_thm RS thm)
2.131 -      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
2.132 -    in
2.133 -      CASES cases (rtac raw_elim_thm 1) thm
2.134 -    end
2.135 -*}
2.136 -
2.137 -method_setup eventually_elim = {*
2.138 -  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
2.139 -*} "elimination of eventually quantifiers"
2.140 -
2.141 -
2.142 -subsection {* Finer-than relation *}
2.143 -
2.144 -text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
2.145 -filter @{term F'}. *}
2.146 -
2.147 -instantiation filter :: (type) complete_lattice
2.148 -begin
2.149 -
2.150 -definition le_filter_def:
2.151 -  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
2.152 -
2.153 -definition
2.154 -  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
2.155 -
2.156 -definition
2.157 -  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
2.158 -
2.159 -definition
2.160 -  "bot = Abs_filter (\<lambda>P. True)"
2.161 -
2.162 -definition
2.163 -  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
2.164 -
2.165 -definition
2.166 -  "inf F F' = Abs_filter
2.167 -      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
2.168 -
2.169 -definition
2.170 -  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
2.171 -
2.172 -definition
2.173 -  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
2.174 -
2.175 -lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
2.176 -  unfolding top_filter_def
2.177 -  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
2.178 -
2.179 -lemma eventually_bot [simp]: "eventually P bot"
2.180 -  unfolding bot_filter_def
2.181 -  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
2.182 -
2.183 -lemma eventually_sup:
2.184 -  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
2.185 -  unfolding sup_filter_def
2.186 -  by (rule eventually_Abs_filter, rule is_filter.intro)
2.187 -     (auto elim!: eventually_rev_mp)
2.188 -
2.189 -lemma eventually_inf:
2.190 -  "eventually P (inf F F') \<longleftrightarrow>
2.191 -   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
2.192 -  unfolding inf_filter_def
2.193 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
2.194 -  apply (fast intro: eventually_True)
2.195 -  apply clarify
2.196 -  apply (intro exI conjI)
2.197 -  apply (erule (1) eventually_conj)
2.198 -  apply (erule (1) eventually_conj)
2.199 -  apply simp
2.200 -  apply auto
2.201 -  done
2.202 -
2.203 -lemma eventually_Sup:
2.204 -  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
2.205 -  unfolding Sup_filter_def
2.206 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
2.207 -  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
2.208 -  done
2.209 -
2.210 -instance proof
2.211 -  fix F F' F'' :: "'a filter" and S :: "'a filter set"
2.212 -  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
2.213 -    by (rule less_filter_def) }
2.214 -  { show "F \<le> F"
2.215 -    unfolding le_filter_def by simp }
2.216 -  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
2.217 -    unfolding le_filter_def by simp }
2.218 -  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
2.219 -    unfolding le_filter_def filter_eq_iff by fast }
2.220 -  { show "F \<le> top"
2.221 -    unfolding le_filter_def eventually_top by (simp add: always_eventually) }
2.222 -  { show "bot \<le> F"
2.223 -    unfolding le_filter_def by simp }
2.224 -  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
2.225 -    unfolding le_filter_def eventually_sup by simp_all }
2.226 -  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
2.227 -    unfolding le_filter_def eventually_sup by simp }
2.228 -  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
2.229 -    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
2.230 -  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
2.231 -    unfolding le_filter_def eventually_inf
2.232 -    by (auto elim!: eventually_mono intro: eventually_conj) }
2.233 -  { assume "F \<in> S" thus "F \<le> Sup S"
2.234 -    unfolding le_filter_def eventually_Sup by simp }
2.235 -  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
2.236 -    unfolding le_filter_def eventually_Sup by simp }
2.237 -  { assume "F'' \<in> S" thus "Inf S \<le> F''"
2.238 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
2.239 -  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
2.240 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
2.241 -qed
2.242 -
2.243 -end
2.244 -
2.245 -lemma filter_leD:
2.246 -  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
2.247 -  unfolding le_filter_def by simp
2.248 -
2.249 -lemma filter_leI:
2.250 -  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
2.251 -  unfolding le_filter_def by simp
2.252 -
2.253 -lemma eventually_False:
2.254 -  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
2.255 -  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
2.256 -
2.257 -abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
2.258 -  where "trivial_limit F \<equiv> F = bot"
2.259 -
2.260 -lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
2.261 -  by (rule eventually_False [symmetric])
2.262 -
2.263 -lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
2.264 -  by (cases P) (simp_all add: eventually_False)
2.265 -
2.266 -
2.267 -subsection {* Map function for filters *}
2.268 -
2.269 -definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
2.270 -  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
2.271 -
2.272 -lemma eventually_filtermap:
2.273 -  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
2.274 -  unfolding filtermap_def
2.275 -  apply (rule eventually_Abs_filter)
2.276 -  apply (rule is_filter.intro)
2.277 -  apply (auto elim!: eventually_rev_mp)
2.278 -  done
2.279 -
2.280 -lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
2.281 -  by (simp add: filter_eq_iff eventually_filtermap)
2.282 -
2.283 -lemma filtermap_filtermap:
2.284 -  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
2.285 -  by (simp add: filter_eq_iff eventually_filtermap)
2.286 -
2.287 -lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
2.288 -  unfolding le_filter_def eventually_filtermap by simp
2.289 -
2.290 -lemma filtermap_bot [simp]: "filtermap f bot = bot"
2.291 -  by (simp add: filter_eq_iff eventually_filtermap)
2.292 -
2.293 -lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
2.294 -  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
2.295 -
2.296 -subsection {* Order filters *}
2.297 -
2.298 -definition at_top :: "('a::order) filter"
2.299 -  where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
2.300 -
2.301 -lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
2.302 -  unfolding at_top_def
2.303 -proof (rule eventually_Abs_filter, rule is_filter.intro)
2.304 -  fix P Q :: "'a \<Rightarrow> bool"
2.305 -  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
2.306 -  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
2.307 -  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
2.308 -  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
2.309 -qed auto
2.310 -
2.311 -lemma eventually_ge_at_top:
2.312 -  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
2.313 -  unfolding eventually_at_top_linorder by auto
2.314 -
2.315 -lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
2.316 -  unfolding eventually_at_top_linorder
2.317 -proof safe
2.318 -  fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
2.319 -next
2.320 -  fix N assume "\<forall>n>N. P n"
2.321 -  moreover from gt_ex[of N] guess y ..
2.322 -  ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
2.323 -qed
2.324 -
2.325 -lemma eventually_gt_at_top:
2.326 -  "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
2.327 -  unfolding eventually_at_top_dense by auto
2.328 -
2.329 -definition at_bot :: "('a::order) filter"
2.330 -  where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"
2.331 -
2.332 -lemma eventually_at_bot_linorder:
2.333 -  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
2.334 -  unfolding at_bot_def
2.335 -proof (rule eventually_Abs_filter, rule is_filter.intro)
2.336 -  fix P Q :: "'a \<Rightarrow> bool"
2.337 -  assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n"
2.338 -  then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto
2.339 -  then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp
2.340 -  then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..
2.341 -qed auto
2.342 -
2.343 -lemma eventually_le_at_bot:
2.344 -  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
2.345 -  unfolding eventually_at_bot_linorder by auto
2.346 -
2.347 -lemma eventually_at_bot_dense:
2.348 -  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
2.349 -  unfolding eventually_at_bot_linorder
2.350 -proof safe
2.351 -  fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
2.352 -next
2.353 -  fix N assume "\<forall>n<N. P n"
2.354 -  moreover from lt_ex[of N] guess y ..
2.355 -  ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
2.356 -qed
2.357 -
2.358 -lemma eventually_gt_at_bot:
2.359 -  "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
2.360 -  unfolding eventually_at_bot_dense by auto
2.361 -
2.362 -subsection {* Sequentially *}
2.363 -
2.364 -abbreviation sequentially :: "nat filter"
2.365 -  where "sequentially == at_top"
2.366 -
2.367 -lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
2.368 -  unfolding at_top_def by simp
2.369 -
2.370 -lemma eventually_sequentially:
2.371 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
2.372 -  by (rule eventually_at_top_linorder)
2.373 -
2.374 -lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
2.375 -  unfolding filter_eq_iff eventually_sequentially by auto
2.376 -
2.377 -lemmas trivial_limit_sequentially = sequentially_bot
2.378 -
2.379 -lemma eventually_False_sequentially [simp]:
2.380 -  "\<not> eventually (\<lambda>n. False) sequentially"
2.381 -  by (simp add: eventually_False)
2.382 -
2.383 -lemma le_sequentially:
2.384 -  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
2.385 -  unfolding le_filter_def eventually_sequentially
2.386 -  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
2.387 -
2.388 -lemma eventually_sequentiallyI:
2.389 -  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
2.390 -  shows "eventually P sequentially"
2.391 -using assms by (auto simp: eventually_sequentially)
2.392 -
2.393 -
2.394 -subsection {* Standard filters *}
2.395 -
2.396 -definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
2.397 -  where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
2.398 -
2.399 -definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
2.400 -  where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
2.401 -
2.402 -definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
2.403 -  where "at a = nhds a within - {a}"
2.404 -
2.405 -abbreviation at_right :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
2.406 -  "at_right x \<equiv> at x within {x <..}"
2.407 -
2.408 -abbreviation at_left :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
2.409 -  "at_left x \<equiv> at x within {..< x}"
2.410 -
2.411  definition at_infinity :: "'a::real_normed_vector filter" where
2.412    "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
2.413
2.414 -lemma eventually_within:
2.415 -  "eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F"
2.416 -  unfolding within_def
2.417 -  by (rule eventually_Abs_filter, rule is_filter.intro)
2.418 -     (auto elim!: eventually_rev_mp)
2.419 -
2.420 -lemma within_UNIV [simp]: "F within UNIV = F"
2.421 -  unfolding filter_eq_iff eventually_within by simp
2.422 -
2.423 -lemma within_empty [simp]: "F within {} = bot"
2.424 -  unfolding filter_eq_iff eventually_within by simp
2.425 -
2.426 -lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
2.427 -  by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
2.428 -
2.429 -lemma at_within_eq: "at x within T = nhds x within (T - {x})"
2.430 -  unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
2.431 -
2.432 -lemma within_le: "F within S \<le> F"
2.433 -  unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
2.434 -
2.435 -lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
2.436 -  unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
2.437 -
2.438 -lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
2.439 -  by (blast intro: within_le le_withinI order_trans)
2.440 -
2.441 -lemma eventually_nhds:
2.442 -  "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
2.443 -unfolding nhds_def
2.444 -proof (rule eventually_Abs_filter, rule is_filter.intro)
2.445 -  have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
2.446 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" ..
2.447 -next
2.448 -  fix P Q
2.449 -  assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
2.450 -     and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)"
2.451 -  then obtain S T where
2.452 -    "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
2.453 -    "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto
2.454 -  hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"
2.455 -    by (simp add: open_Int)
2.456 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" ..
2.457 -qed auto
2.458
2.459  lemma eventually_nhds_metric:
2.460    "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
2.461 @@ -472,18 +24,10 @@
2.462  apply (erule le_less_trans [OF dist_triangle])
2.463  done
2.464
2.465 -lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
2.466 -  unfolding trivial_limit_def eventually_nhds by simp
2.467 -
2.468 -lemma eventually_at_topological:
2.469 -  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
2.470 -unfolding at_def eventually_within eventually_nhds by simp
2.471 -
2.472  lemma eventually_at:
2.473    fixes a :: "'a::metric_space"
2.474    shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
2.475  unfolding at_def eventually_within eventually_nhds_metric by auto
2.476 -
2.477  lemma eventually_within_less: (* COPY FROM Topo/eventually_within *)
2.478    "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
2.479    unfolding eventually_within eventually_at dist_nz by auto
2.480 @@ -492,29 +36,6 @@
2.481    "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)"
2.482    unfolding eventually_within_less by auto (metis dense order_le_less_trans)
2.483
2.484 -lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
2.485 -  unfolding trivial_limit_def eventually_at_topological
2.486 -  by (safe, case_tac "S = {a}", simp, fast, fast)
2.487 -
2.488 -lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
2.489 -  by (simp add: at_eq_bot_iff not_open_singleton)
2.490 -
2.491 -lemma trivial_limit_at_left_real [simp]: (* maybe generalize type *)
2.492 -  "\<not> trivial_limit (at_left (x::real))"
2.493 -  unfolding trivial_limit_def eventually_within_le
2.494 -  apply clarsimp
2.495 -  apply (rule_tac x="x - d/2" in bexI)
2.496 -  apply (auto simp: dist_real_def)
2.497 -  done
2.498 -
2.499 -lemma trivial_limit_at_right_real [simp]: (* maybe generalize type *)
2.500 -  "\<not> trivial_limit (at_right (x::real))"
2.501 -  unfolding trivial_limit_def eventually_within_le
2.502 -  apply clarsimp
2.503 -  apply (rule_tac x="x + d/2" in bexI)
2.504 -  apply (auto simp: dist_real_def)
2.505 -  done
2.506 -
2.507  lemma eventually_at_infinity:
2.508    "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
2.509  unfolding at_infinity_def
2.510 @@ -722,214 +243,9 @@
2.511  lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
2.512  lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
2.513
2.514 -
2.515 -subsection {* Limits *}
2.516 -
2.517 -definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
2.518 -  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
2.519 -
2.520 -syntax
2.521 -  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
2.522 -
2.523 -translations
2.524 -  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
2.525 -
2.526 -lemma filterlim_iff:
2.527 -  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
2.528 -  unfolding filterlim_def le_filter_def eventually_filtermap ..
2.529 -
2.530 -lemma filterlim_compose:
2.531 -  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
2.532 -  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
2.533 -
2.534 -lemma filterlim_mono:
2.535 -  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
2.536 -  unfolding filterlim_def by (metis filtermap_mono order_trans)
2.537 -
2.538 -lemma filterlim_ident: "LIM x F. x :> F"
2.539 -  by (simp add: filterlim_def filtermap_ident)
2.540 -
2.541 -lemma filterlim_cong:
2.542 -  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
2.543 -  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
2.544 -
2.545 -lemma filterlim_within:
2.546 -  "(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))"
2.547 -  unfolding filterlim_def
2.548 -proof safe
2.549 -  assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1"
2.550 -    by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
2.551 -qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
2.552 -
2.553 -lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
2.554 -  unfolding filterlim_def filtermap_filtermap ..
2.555 -
2.556 -lemma filterlim_sup:
2.557 -  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
2.558 -  unfolding filterlim_def filtermap_sup by auto
2.559 -
2.560 -lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
2.561 -  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
2.562 -
2.563 -abbreviation (in topological_space)
2.564 -  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
2.565 -  "(f ---> l) F \<equiv> filterlim f (nhds l) F"
2.566 -
2.567 -lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
2.568 -  by simp
2.569 -
2.570 -ML {*
2.571 -
2.572 -structure Tendsto_Intros = Named_Thms
2.573 -(
2.574 -  val name = @{binding tendsto_intros}
2.575 -  val description = "introduction rules for tendsto"
2.576 -)
2.577 -
2.578 -*}
2.579 -
2.580 -setup {*
2.581 -  Tendsto_Intros.setup #>
2.583 -    map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
2.584 -*}
2.585 -
2.586 -lemma tendsto_def: "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
2.587 -  unfolding filterlim_def
2.588 -proof safe
2.589 -  fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
2.590 -  then show "eventually (\<lambda>x. f x \<in> S) F"
2.591 -    unfolding eventually_nhds eventually_filtermap le_filter_def
2.592 -    by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
2.593 -qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
2.594 -
2.595 -lemma filterlim_at:
2.596 -  "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
2.597 -  by (simp add: at_def filterlim_within)
2.598 -
2.599 -lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
2.600 -  unfolding tendsto_def le_filter_def by fast
2.601 -
2.602 -lemma topological_tendstoI:
2.603 -  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F)
2.604 -    \<Longrightarrow> (f ---> l) F"
2.605 -  unfolding tendsto_def by auto
2.606 -
2.607 -lemma topological_tendstoD:
2.608 -  "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
2.609 -  unfolding tendsto_def by auto
2.610 -
2.611 -lemma tendstoI:
2.612 -  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
2.613 -  shows "(f ---> l) F"
2.614 -  apply (rule topological_tendstoI)
2.615 -  apply (simp add: open_dist)
2.616 -  apply (drule (1) bspec, clarify)
2.617 -  apply (drule assms)
2.618 -  apply (erule eventually_elim1, simp)
2.619 -  done
2.620 -
2.621 -lemma tendstoD:
2.622 -  "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
2.623 -  apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
2.624 -  apply (clarsimp simp add: open_dist)
2.625 -  apply (rule_tac x="e - dist x l" in exI, clarsimp)
2.626 -  apply (simp only: less_diff_eq)
2.627 -  apply (erule le_less_trans [OF dist_triangle])
2.628 -  apply simp
2.629 -  apply simp
2.630 -  done
2.631 -
2.632 -lemma tendsto_iff:
2.633 -  "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
2.634 -  using tendstoI tendstoD by fast
2.635 -
2.636 -lemma order_tendstoI:
2.637 -  fixes y :: "_ :: order_topology"
2.638 -  assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
2.639 -  assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
2.640 -  shows "(f ---> y) F"
2.641 -proof (rule topological_tendstoI)
2.642 -  fix S assume "open S" "y \<in> S"
2.643 -  then show "eventually (\<lambda>x. f x \<in> S) F"
2.644 -    unfolding open_generated_order
2.645 -  proof induct
2.646 -    case (UN K)
2.647 -    then obtain k where "y \<in> k" "k \<in> K" by auto
2.648 -    with UN(2)[of k] show ?case
2.649 -      by (auto elim: eventually_elim1)
2.650 -  qed (insert assms, auto elim: eventually_elim2)
2.651 -qed
2.652 -
2.653 -lemma order_tendstoD:
2.654 -  fixes y :: "_ :: order_topology"
2.655 -  assumes y: "(f ---> y) F"
2.656 -  shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
2.657 -    and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
2.658 -  using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto
2.659 -
2.660 -lemma order_tendsto_iff:
2.661 -  fixes f :: "_ \<Rightarrow> 'a :: order_topology"
2.662 -  shows "(f ---> x) F \<longleftrightarrow>(\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
2.663 -  by (metis order_tendstoI order_tendstoD)
2.664 -
2.665  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
2.666    by (simp only: tendsto_iff Zfun_def dist_norm)
2.667
2.668 -lemma tendsto_bot [simp]: "(f ---> a) bot"
2.669 -  unfolding tendsto_def by simp
2.670 -
2.671 -lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
2.672 -  unfolding tendsto_def eventually_at_topological by auto
2.673 -
2.674 -lemma tendsto_ident_at_within [tendsto_intros]:
2.675 -  "((\<lambda>x. x) ---> a) (at a within S)"
2.676 -  unfolding tendsto_def eventually_within eventually_at_topological by auto
2.677 -
2.678 -lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
2.679 -  by (simp add: tendsto_def)
2.680 -
2.681 -lemma tendsto_unique:
2.682 -  fixes f :: "'a \<Rightarrow> 'b::t2_space"
2.683 -  assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
2.684 -  shows "a = b"
2.685 -proof (rule ccontr)
2.686 -  assume "a \<noteq> b"
2.687 -  obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
2.688 -    using hausdorff [OF `a \<noteq> b`] by fast
2.689 -  have "eventually (\<lambda>x. f x \<in> U) F"
2.690 -    using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD)
2.691 -  moreover
2.692 -  have "eventually (\<lambda>x. f x \<in> V) F"
2.693 -    using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
2.694 -  ultimately
2.695 -  have "eventually (\<lambda>x. False) F"
2.696 -  proof eventually_elim
2.697 -    case (elim x)
2.698 -    hence "f x \<in> U \<inter> V" by simp
2.699 -    with `U \<inter> V = {}` show ?case by simp
2.700 -  qed
2.701 -  with `\<not> trivial_limit F` show "False"
2.702 -    by (simp add: trivial_limit_def)
2.703 -qed
2.704 -
2.705 -lemma tendsto_const_iff:
2.706 -  fixes a b :: "'a::t2_space"
2.707 -  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
2.708 -  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
2.709 -
2.710 -lemma tendsto_at_iff_tendsto_nhds:
2.711 -  "(g ---> g l) (at l) \<longleftrightarrow> (g ---> g l) (nhds l)"
2.712 -  unfolding tendsto_def at_def eventually_within
2.713 -  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
2.714 -
2.715 -lemma tendsto_compose:
2.716 -  "(g ---> g l) (at l) \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
2.717 -  unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
2.718 -
2.719 -lemma tendsto_compose_eventually:
2.720 -  "(g ---> m) (at l) \<Longrightarrow> (f ---> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> m) F"
2.721 -  by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
2.722
2.723  lemma metric_tendsto_imp_tendsto:
2.724    assumes f: "(f ---> a) F"
2.725 @@ -941,21 +257,6 @@
2.726    with le show "eventually (\<lambda>x. dist (g x) b < e) F"
2.727      using le_less_trans by (rule eventually_elim2)
2.728  qed
2.729 -
2.730 -lemma increasing_tendsto:
2.731 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
2.732 -  assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
2.733 -      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
2.734 -  shows "(f ---> l) F"
2.735 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
2.736 -
2.737 -lemma decreasing_tendsto:
2.738 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
2.739 -  assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
2.740 -      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
2.741 -  shows "(f ---> l) F"
2.742 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
2.743 -
2.744  subsubsection {* Distance and norms *}
2.745
2.746  lemma tendsto_dist [tendsto_intros]:
2.747 @@ -1057,19 +358,6 @@
2.749  qed
2.750
2.751 -lemma tendsto_sandwich:
2.752 -  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
2.753 -  assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
2.754 -  assumes lim: "(f ---> c) net" "(h ---> c) net"
2.755 -  shows "(g ---> c) net"
2.756 -proof (rule order_tendstoI)
2.757 -  fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
2.758 -    using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
2.759 -next
2.760 -  fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
2.761 -    using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
2.762 -qed
2.763 -
2.764  lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
2.765
2.766  subsubsection {* Linear operators and multiplication *}
2.767 @@ -1136,31 +424,6 @@
2.769  qed
2.770
2.771 -lemma tendsto_le:
2.772 -  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
2.773 -  assumes F: "\<not> trivial_limit F"
2.774 -  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
2.775 -  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
2.776 -  shows "y \<le> x"
2.777 -proof (rule ccontr)
2.778 -  assume "\<not> y \<le> x"
2.779 -  with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
2.780 -    by (auto simp: not_le)
2.781 -  then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
2.782 -    using x y by (auto intro: order_tendstoD)
2.783 -  with ev have "eventually (\<lambda>x. False) F"
2.784 -    by eventually_elim (insert xy, fastforce)
2.785 -  with F show False
2.786 -    by (simp add: eventually_False)
2.787 -qed
2.788 -
2.789 -lemma tendsto_le_const:
2.790 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
2.791 -  assumes F: "\<not> trivial_limit F"
2.792 -  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
2.793 -  shows "a \<le> x"
2.794 -  using F x tendsto_const a by (rule tendsto_le)
2.795 -
2.796  subsubsection {* Inverse and division *}
2.797
2.798  lemma (in bounded_bilinear) Zfun_prod_Bfun:
2.799 @@ -1281,75 +544,6 @@
2.800    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
2.801    unfolding sgn_div_norm by (simp add: tendsto_intros)
2.802
2.803 -subsection {* Limits to @{const at_top} and @{const at_bot} *}
2.804 -
2.805 -lemma filterlim_at_top:
2.806 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
2.807 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
2.808 -  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
2.809 -
2.810 -lemma filterlim_at_top_dense:
2.811 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
2.812 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
2.813 -  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
2.814 -            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
2.815 -
2.816 -lemma filterlim_at_top_ge:
2.817 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
2.818 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
2.819 -  unfolding filterlim_at_top
2.820 -proof safe
2.821 -  fix Z assume *: "\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F"
2.822 -  with *[THEN spec, of "max Z c"] show "eventually (\<lambda>x. Z \<le> f x) F"
2.823 -    by (auto elim!: eventually_elim1)
2.824 -qed simp
2.825 -
2.826 -lemma filterlim_at_top_at_top:
2.827 -  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
2.828 -  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
2.829 -  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
2.830 -  assumes Q: "eventually Q at_top"
2.831 -  assumes P: "eventually P at_top"
2.832 -  shows "filterlim f at_top at_top"
2.833 -proof -
2.834 -  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
2.835 -    unfolding eventually_at_top_linorder by auto
2.836 -  show ?thesis
2.837 -  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
2.838 -    fix z assume "x \<le> z"
2.839 -    with x have "P z" by auto
2.840 -    have "eventually (\<lambda>x. g z \<le> x) at_top"
2.841 -      by (rule eventually_ge_at_top)
2.842 -    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
2.843 -      by eventually_elim (metis mono bij `P z`)
2.844 -  qed
2.845 -qed
2.846 -
2.847 -lemma filterlim_at_top_gt:
2.848 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
2.849 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
2.850 -  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
2.851 -
2.852 -lemma filterlim_at_bot:
2.853 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
2.854 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
2.855 -  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
2.856 -
2.857 -lemma filterlim_at_bot_le:
2.858 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
2.859 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
2.860 -  unfolding filterlim_at_bot
2.861 -proof safe
2.862 -  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
2.863 -  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
2.864 -    by (auto elim!: eventually_elim1)
2.865 -qed simp
2.866 -
2.867 -lemma filterlim_at_bot_lt:
2.868 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
2.869 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
2.870 -  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
2.871 -
2.872  lemma filterlim_at_bot_at_right:
2.873    fixes f :: "real \<Rightarrow> 'b::linorder"
2.874    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
2.875 @@ -1429,13 +623,7 @@
2.876
2.877  *}
2.878
2.879 -lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
2.880 -  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup
2.881 -           elim: eventually_elim2 eventually_elim1)
2.882 -
2.883 -lemma filterlim_split_at_real:
2.884 -  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
2.885 -  by (subst at_eq_sup_left_right) (rule filterlim_sup)
2.886 +lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
2.887
2.888  lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
2.889    unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
2.890 @@ -1486,14 +674,6 @@
2.891    "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
2.892    unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
2.893
2.894 -lemma filterlim_at_split:
2.895 -  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
2.896 -  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
2.897 -
2.898 -lemma eventually_at_split:
2.899 -  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
2.900 -  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
2.901 -
2.902  lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
2.903    unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
2.904    by (metis le_minus_iff minus_minus)
2.905 @@ -1765,5 +945,10 @@
2.906      by (auto simp: norm_power)
2.907  qed simp
2.908
2.909 +
2.910 +(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
2.911 +   Hence it was references as Limits.within, but now it is Basic_Topology.eventually_within *)
2.912 +lemmas eventually_within = eventually_within
2.913 +
2.914  end
2.915
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Mar 21 16:58:14 2013 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:42 2013 +0100
3.3 @@ -1340,11 +1340,11 @@
3.4
3.5  text {* Some property holds "sufficiently close" to the limit point. *}
3.6
3.7 -lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
3.8 +lemma eventually_at: (* FIXME: this replaces Metric_Spaces.eventually_at *)
3.9    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
3.10  unfolding eventually_at dist_nz by auto
3.11
3.12 -lemma eventually_within: (* FIXME: this replaces Limits.eventually_within *)
3.13 +lemma eventually_within: (* FIXME: this replaces Topological_Spaces.eventually_within *)
3.14    "eventually P (at a within S) \<longleftrightarrow>
3.15          (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
3.16    by (rule eventually_within_less)
3.17 @@ -1448,12 +1448,12 @@
3.18    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
3.19    { assume "?lhs"
3.20      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
3.21 -      unfolding Limits.eventually_within Limits.eventually_at_topological
3.22 +      unfolding Limits.eventually_within eventually_at_topological
3.23        by auto
3.24      with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
3.25        by auto
3.26      then have "?rhs"
3.27 -      unfolding Limits.eventually_at_topological by auto
3.28 +      unfolding eventually_at_topological by auto
3.29    } moreover
3.30    { assume "?rhs" hence "?lhs"
3.31        unfolding Limits.eventually_within
```
```     4.1 --- a/src/HOL/RealVector.thy	Thu Mar 21 16:58:14 2013 +0100
4.2 +++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:42 2013 +0100
4.3 @@ -434,131 +434,6 @@
4.4    by (rule Reals_cases) auto
4.5
4.6
4.7 -subsection {* Topological spaces *}
4.8 -
4.9 -class "open" =
4.10 -  fixes "open" :: "'a set \<Rightarrow> bool"
4.11 -
4.12 -class topological_space = "open" +
4.13 -  assumes open_UNIV [simp, intro]: "open UNIV"
4.14 -  assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
4.15 -  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
4.16 -begin
4.17 -
4.18 -definition
4.19 -  closed :: "'a set \<Rightarrow> bool" where
4.20 -  "closed S \<longleftrightarrow> open (- S)"
4.21 -
4.22 -lemma open_empty [intro, simp]: "open {}"
4.23 -  using open_Union [of "{}"] by simp
4.24 -
4.25 -lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
4.26 -  using open_Union [of "{S, T}"] by simp
4.27 -
4.28 -lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
4.29 -  unfolding SUP_def by (rule open_Union) auto
4.30 -
4.31 -lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
4.32 -  by (induct set: finite) auto
4.33 -
4.34 -lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
4.35 -  unfolding INF_def by (rule open_Inter) auto
4.36 -
4.37 -lemma closed_empty [intro, simp]:  "closed {}"
4.38 -  unfolding closed_def by simp
4.39 -
4.40 -lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
4.41 -  unfolding closed_def by auto
4.42 -
4.43 -lemma closed_UNIV [intro, simp]: "closed UNIV"
4.44 -  unfolding closed_def by simp
4.45 -
4.46 -lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
4.47 -  unfolding closed_def by auto
4.48 -
4.49 -lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
4.50 -  unfolding closed_def by auto
4.51 -
4.52 -lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
4.53 -  unfolding closed_def uminus_Inf by auto
4.54 -
4.55 -lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
4.56 -  by (induct set: finite) auto
4.57 -
4.58 -lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
4.59 -  unfolding SUP_def by (rule closed_Union) auto
4.60 -
4.61 -lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
4.62 -  unfolding closed_def by simp
4.63 -
4.64 -lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
4.65 -  unfolding closed_def by simp
4.66 -
4.67 -lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
4.68 -  unfolding closed_open Diff_eq by (rule open_Int)
4.69 -
4.70 -lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
4.71 -  unfolding open_closed Diff_eq by (rule closed_Int)
4.72 -
4.73 -lemma open_Compl [intro]: "closed S \<Longrightarrow> open (- S)"
4.74 -  unfolding closed_open .
4.75 -
4.76 -lemma closed_Compl [intro]: "open S \<Longrightarrow> closed (- S)"
4.77 -  unfolding open_closed .
4.78 -
4.79 -end
4.80 -
4.81 -inductive generate_topology for S where
4.82 -  UNIV: "generate_topology S UNIV"
4.83 -| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"
4.84 -| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
4.85 -| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
4.86 -
4.87 -hide_fact (open) UNIV Int UN Basis
4.88 -
4.89 -lemma generate_topology_Union:
4.90 -  "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
4.91 -  unfolding SUP_def by (intro generate_topology.UN) auto
4.92 -
4.93 -lemma topological_space_generate_topology:
4.94 -  "class.topological_space (generate_topology S)"
4.95 -  by default (auto intro: generate_topology.intros)
4.96 -
4.97 -class order_topology = order + "open" +
4.98 -  assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
4.99 -begin
4.100 -
4.101 -subclass topological_space
4.102 -  unfolding open_generated_order
4.103 -  by (rule topological_space_generate_topology)
4.104 -
4.105 -lemma open_greaterThan [simp]: "open {a <..}"
4.106 -  unfolding open_generated_order by (auto intro: generate_topology.Basis)
4.107 -
4.108 -lemma open_lessThan [simp]: "open {..< a}"
4.109 -  unfolding open_generated_order by (auto intro: generate_topology.Basis)
4.110 -
4.111 -lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
4.112 -   unfolding greaterThanLessThan_eq by (simp add: open_Int)
4.113 -
4.114 -end
4.115 -
4.116 -class linorder_topology = linorder + order_topology
4.117 -
4.118 -lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
4.119 -  by (simp add: closed_open)
4.120 -
4.121 -lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
4.122 -  by (simp add: closed_open)
4.123 -
4.124 -lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
4.125 -proof -
4.126 -  have "{a .. b} = {a ..} \<inter> {.. b}"
4.127 -    by auto
4.128 -  then show ?thesis
4.129 -    by (simp add: closed_Int)
4.130 -qed
4.131 -
4.132  subsection {* Metric spaces *}
4.133
4.134  class dist =
4.135 @@ -1182,78 +1057,6 @@
4.136  lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
4.137    unfolding of_real_def by (rule bounded_linear_scaleR_left)
4.138
4.139 -subsection{* Hausdorff and other separation properties *}
4.140 -
4.141 -class t0_space = topological_space +
4.142 -  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
4.143 -
4.144 -class t1_space = topological_space +
4.145 -  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
4.146 -
4.147 -instance t1_space \<subseteq> t0_space
4.148 -proof qed (fast dest: t1_space)
4.149 -
4.150 -lemma separation_t1:
4.151 -  fixes x y :: "'a::t1_space"
4.152 -  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
4.153 -  using t1_space[of x y] by blast
4.154 -
4.155 -lemma closed_singleton:
4.156 -  fixes a :: "'a::t1_space"
4.157 -  shows "closed {a}"
4.158 -proof -
4.159 -  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
4.160 -  have "open ?T" by (simp add: open_Union)
4.161 -  also have "?T = - {a}"
4.162 -    by (simp add: set_eq_iff separation_t1, auto)
4.163 -  finally show "closed {a}" unfolding closed_def .
4.164 -qed
4.165 -
4.166 -lemma closed_insert [simp]:
4.167 -  fixes a :: "'a::t1_space"
4.168 -  assumes "closed S" shows "closed (insert a S)"
4.169 -proof -
4.170 -  from closed_singleton assms
4.171 -  have "closed ({a} \<union> S)" by (rule closed_Un)
4.172 -  thus "closed (insert a S)" by simp
4.173 -qed
4.174 -
4.175 -lemma finite_imp_closed:
4.176 -  fixes S :: "'a::t1_space set"
4.177 -  shows "finite S \<Longrightarrow> closed S"
4.178 -by (induct set: finite, simp_all)
4.179 -
4.180 -text {* T2 spaces are also known as Hausdorff spaces. *}
4.181 -
4.182 -class t2_space = topological_space +
4.183 -  assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
4.184 -
4.185 -instance t2_space \<subseteq> t1_space
4.186 -proof qed (fast dest: hausdorff)
4.187 -
4.188 -lemma (in linorder) less_separate:
4.189 -  assumes "x < y"
4.190 -  shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
4.191 -proof cases
4.192 -  assume "\<exists>z. x < z \<and> z < y"
4.193 -  then guess z ..
4.194 -  then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
4.195 -    by auto
4.196 -  then show ?thesis by blast
4.197 -next
4.198 -  assume "\<not> (\<exists>z. x < z \<and> z < y)"
4.199 -  with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
4.200 -    by auto
4.201 -  then show ?thesis by blast
4.202 -qed
4.203 -
4.204 -instance linorder_topology \<subseteq> t2_space
4.205 -proof
4.206 -  fix x y :: 'a
4.207 -  from less_separate[of x y] less_separate[of y x]
4.208 -  show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
4.209 -    by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
4.210 -qed
4.211
4.212  instance metric_space \<subseteq> t2_space
4.213  proof
4.214 @@ -1269,22 +1072,6 @@
4.215    then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
4.216      by blast
4.217  qed
4.218 -
4.219 -lemma separation_t2:
4.220 -  fixes x y :: "'a::t2_space"
4.221 -  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
4.222 -  using hausdorff[of x y] by blast
4.223 -
4.224 -lemma separation_t0:
4.225 -  fixes x y :: "'a::t0_space"
4.226 -  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
4.227 -  using t0_space[of x y] by blast
4.228 -
4.229 -text {* A perfect space is a topological space with no isolated points. *}
4.230 -
4.231 -class perfect_space = topological_space +
4.232 -  assumes not_open_singleton: "\<not> open {x}"
4.233 -
4.234  instance real_normed_algebra_1 \<subseteq> perfect_space
4.235  proof
4.236    fix x::'a
```
```     5.1 --- a/src/HOL/SEQ.thy	Thu Mar 21 16:58:14 2013 +0100
5.2 +++ b/src/HOL/SEQ.thy	Fri Mar 22 10:41:42 2013 +0100
5.3 @@ -10,219 +10,11 @@
5.4  header {* Sequences and Convergence *}
5.5
5.6  theory SEQ
5.7 -imports Limits RComplete
5.8 +imports Limits
5.9  begin
5.10
5.11 -subsection {* Monotone sequences and subsequences *}
5.12 -
5.13 -definition
5.14 -  monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
5.15 -    --{*Definition of monotonicity.
5.16 -        The use of disjunction here complicates proofs considerably.
5.17 -        One alternative is to add a Boolean argument to indicate the direction.
5.18 -        Another is to develop the notions of increasing and decreasing first.*}
5.19 -  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
5.20 -
5.21 -definition
5.22 -  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
5.23 -    --{*Increasing sequence*}
5.24 -  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
5.25 -
5.26 -definition
5.27 -  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
5.28 -    --{*Decreasing sequence*}
5.29 -  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
5.30 -
5.31 -definition
5.32 -  subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
5.33 -    --{*Definition of subsequence*}
5.34 -  "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
5.35 -
5.36 -lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
5.37 -  unfolding mono_def incseq_def by auto
5.38 -
5.39 -lemma incseq_SucI:
5.40 -  "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
5.41 -  using lift_Suc_mono_le[of X]
5.42 -  by (auto simp: incseq_def)
5.43 -
5.44 -lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j"
5.45 -  by (auto simp: incseq_def)
5.46 -
5.47 -lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)"
5.48 -  using incseqD[of A i "Suc i"] by auto
5.49 -
5.50 -lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
5.51 -  by (auto intro: incseq_SucI dest: incseq_SucD)
5.52 -
5.53 -lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)"
5.54 -  unfolding incseq_def by auto
5.55 -
5.56 -lemma decseq_SucI:
5.57 -  "(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X"
5.58 -  using order.lift_Suc_mono_le[OF dual_order, of X]
5.59 -  by (auto simp: decseq_def)
5.60 -
5.61 -lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i"
5.62 -  by (auto simp: decseq_def)
5.63 -
5.64 -lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i"
5.65 -  using decseqD[of A i "Suc i"] by auto
5.66 -
5.67 -lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
5.68 -  by (auto intro: decseq_SucI dest: decseq_SucD)
5.69 -
5.70 -lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)"
5.71 -  unfolding decseq_def by auto
5.72 -
5.73 -lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X"
5.74 -  unfolding monoseq_def incseq_def decseq_def ..
5.75 -
5.76 -lemma monoseq_Suc:
5.77 -  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
5.78 -  unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..
5.79 -
5.80 -lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
5.82 -
5.83 -lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
5.85 -
5.86 -lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
5.88 -
5.89 -lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
5.91 -
5.92 -lemma monoseq_minus:
5.93 -  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
5.94 -  assumes "monoseq a"
5.95 -  shows "monoseq (\<lambda> n. - a n)"
5.96 -proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
5.97 -  case True
5.98 -  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
5.99 -  thus ?thesis by (rule monoI2)
5.100 -next
5.101 -  case False
5.102 -  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto
5.103 -  thus ?thesis by (rule monoI1)
5.104 -qed
5.105 -
5.106 -text{*Subsequence (alternative definition, (e.g. Hoskins)*}
5.107 -
5.108 -lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
5.111 -apply (induct_tac k)
5.112 -apply (auto intro: less_trans)
5.113 -done
5.114 -
5.115 -text{* for any sequence, there is a monotonic subsequence *}
5.116 -lemma seq_monosub:
5.117 -  fixes s :: "nat => 'a::linorder"
5.118 -  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
5.119 -proof cases
5.120 -  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
5.121 -  assume *: "\<forall>n. \<exists>p. ?P p n"
5.122 -  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
5.123 -  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
5.124 -  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
5.125 -  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
5.126 -  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
5.127 -  then have "subseq f" unfolding subseq_Suc_iff by auto
5.128 -  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
5.129 -  proof (intro disjI2 allI)
5.130 -    fix n show "s (f (Suc n)) \<le> s (f n)"
5.131 -    proof (cases n)
5.132 -      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
5.133 -    next
5.134 -      case (Suc m)
5.135 -      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
5.136 -      with P_Suc Suc show ?thesis by simp
5.137 -    qed
5.138 -  qed
5.139 -  ultimately show ?thesis by auto
5.140 -next
5.141 -  let "?P p m" = "m < p \<and> s m < s p"
5.142 -  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
5.143 -  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
5.144 -  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
5.145 -  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
5.146 -  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
5.147 -  have P_0: "?P (f 0) (Suc N)"
5.148 -    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
5.149 -  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
5.150 -      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
5.151 -  note P' = this
5.152 -  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
5.153 -      by (induct i) (insert P_0 P', auto) }
5.154 -  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
5.155 -    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
5.156 -  then show ?thesis by auto
5.157 -qed
5.158 -
5.159 -lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
5.160 -proof(induct n)
5.161 -  case 0 thus ?case by simp
5.162 -next
5.163 -  case (Suc n)
5.164 -  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
5.165 -  have "n < f (Suc n)" by arith
5.166 -  thus ?case by arith
5.167 -qed
5.168 -
5.169 -lemma eventually_subseq:
5.170 -  "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
5.171 -  unfolding eventually_sequentially by (metis seq_suble le_trans)
5.172 -
5.173 -lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
5.174 -  unfolding filterlim_iff by (metis eventually_subseq)
5.175 -
5.176 -lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
5.177 -  unfolding subseq_def by simp
5.178 -
5.179 -lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
5.180 -  using assms by (auto simp: subseq_def)
5.181 -
5.182 -lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
5.183 -  by (simp add: incseq_def monoseq_def)
5.184 -
5.185 -lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
5.186 -  by (simp add: decseq_def monoseq_def)
5.187 -
5.188 -lemma decseq_eq_incseq:
5.189 -  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
5.190 -  by (simp add: decseq_def incseq_def)
5.191 -
5.192 -lemma INT_decseq_offset:
5.193 -  assumes "decseq F"
5.194 -  shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
5.195 -proof safe
5.196 -  fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
5.197 -  show "x \<in> F i"
5.198 -  proof cases
5.199 -    from x have "x \<in> F n" by auto
5.200 -    also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
5.201 -      unfolding decseq_def by simp
5.202 -    finally show ?thesis .
5.203 -  qed (insert x, simp)
5.204 -qed auto
5.205 -
5.206  subsection {* Defintions of limits *}
5.207
5.208 -abbreviation (in topological_space)
5.209 -  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
5.210 -    ("((_)/ ----> (_))" [60, 60] 60) where
5.211 -  "X ----> L \<equiv> (X ---> L) sequentially"
5.212 -
5.213 -definition
5.214 -  lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where
5.215 -    --{*Standard definition of limit using choice operator*}
5.216 -  "lim X = (THE L. X ----> L)"
5.217 -
5.218 -definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
5.219 -  "convergent X = (\<exists>L. X ----> L)"
5.220 -
5.221  definition
5.222    Bseq :: "(nat => 'a::real_normed_vector) => bool" where
5.223      --{*Standard definition for bounded sequence*}
5.224 @@ -317,78 +109,10 @@
5.225    shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
5.227
5.228 -lemma LIMSEQ_const_iff:
5.229 -  fixes k l :: "'a::t2_space"
5.230 -  shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
5.231 -  using trivial_limit_sequentially by (rule tendsto_const_iff)
5.232 -
5.233 -lemma LIMSEQ_SUP:
5.234 -  "incseq X \<Longrightarrow> X ----> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})"
5.235 -  by (intro increasing_tendsto)
5.236 -     (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
5.237 -
5.238 -lemma LIMSEQ_INF:
5.239 -  "decseq X \<Longrightarrow> X ----> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})"
5.240 -  by (intro decreasing_tendsto)
5.241 -     (auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans)
5.242 -
5.243 -lemma LIMSEQ_ignore_initial_segment:
5.244 -  "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
5.245 -apply (rule topological_tendstoI)
5.246 -apply (drule (2) topological_tendstoD)
5.247 -apply (simp only: eventually_sequentially)
5.248 -apply (erule exE, rename_tac N)
5.249 -apply (rule_tac x=N in exI)
5.250 -apply simp
5.251 -done
5.252 -
5.253 -lemma LIMSEQ_offset:
5.254 -  "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
5.255 -apply (rule topological_tendstoI)
5.256 -apply (drule (2) topological_tendstoD)
5.257 -apply (simp only: eventually_sequentially)
5.258 -apply (erule exE, rename_tac N)
5.259 -apply (rule_tac x="N + k" in exI)
5.260 -apply clarify
5.261 -apply (drule_tac x="n - k" in spec)
5.263 -done
5.264 -
5.265 -lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
5.266 -by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
5.267 -
5.268 -lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
5.269 -by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
5.270 -
5.271 -lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
5.272 -by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
5.273 -
5.274  lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
5.275    unfolding tendsto_def eventually_sequentially
5.276    by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
5.277
5.278 -lemma LIMSEQ_unique:
5.279 -  fixes a b :: "'a::t2_space"
5.280 -  shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
5.281 -  using trivial_limit_sequentially by (rule tendsto_unique)
5.282 -
5.283 -lemma increasing_LIMSEQ:
5.284 -  fixes f :: "nat \<Rightarrow> real"
5.285 -  assumes inc: "\<And>n. f n \<le> f (Suc n)"
5.286 -      and bdd: "\<And>n. f n \<le> l"
5.287 -      and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
5.288 -  shows "f ----> l"
5.289 -proof (rule increasing_tendsto)
5.290 -  fix x assume "x < l"
5.291 -  with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
5.292 -    by auto
5.293 -  from en[OF `0 < e`] obtain n where "l - e \<le> f n"
5.294 -    by (auto simp: field_simps)
5.295 -  with `e < l - x` `0 < e` have "x < f n" by simp
5.296 -  with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially"
5.297 -    by (auto simp: eventually_sequentially incseq_def intro: less_le_trans)
5.298 -qed (insert bdd, auto)
5.299 -
5.300  lemma Bseq_inverse_lemma:
5.301    fixes x :: "'a::real_normed_div_algebra"
5.302    shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
5.303 @@ -443,37 +167,8 @@
5.304    using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
5.305    by auto
5.306
5.307 -lemma LIMSEQ_le_const:
5.308 -  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
5.309 -  using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
5.310 -
5.311 -lemma LIMSEQ_le:
5.312 -  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
5.313 -  using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
5.314 -
5.315 -lemma LIMSEQ_le_const2:
5.316 -  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
5.317 -  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
5.318 -
5.319  subsection {* Convergence *}
5.320
5.321 -lemma limI: "X ----> L ==> lim X = L"
5.323 -apply (blast intro: LIMSEQ_unique)
5.324 -done
5.325 -
5.326 -lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
5.328 -
5.329 -lemma convergentI: "(X ----> L) ==> convergent X"
5.330 -by (auto simp add: convergent_def)
5.331 -
5.332 -lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
5.333 -by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
5.334 -
5.335 -lemma convergent_const: "convergent (\<lambda>n. c)"
5.336 -  by (rule convergentI, rule tendsto_const)
5.337 -
5.339    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
5.340    assumes "convergent (\<lambda>n. X n)"
5.341 @@ -508,22 +203,6 @@
5.342  apply (drule tendsto_minus, auto)
5.343  done
5.344
5.345 -lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::real)) \<Longrightarrow> lim f \<le> x"
5.346 -  using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
5.347 -
5.348 -lemma monoseq_le:
5.349 -  "monoseq a \<Longrightarrow> a ----> (x::real) \<Longrightarrow>
5.350 -    ((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
5.351 -  by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
5.352 -
5.353 -lemma LIMSEQ_subseq_LIMSEQ:
5.354 -  "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
5.355 -  unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq])
5.356 -
5.357 -lemma convergent_subseq_convergent:
5.358 -  "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
5.359 -  unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
5.360 -
5.361
5.362  subsection {* Bounded Monotonic Sequences *}
5.363
5.364 @@ -665,14 +344,6 @@
5.365    by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
5.366              Bseq_mono_convergent)
5.367
5.368 -subsubsection{*Increasing and Decreasing Series*}
5.369 -
5.370 -lemma incseq_le: "incseq X \<Longrightarrow> X ----> L \<Longrightarrow> X n \<le> (L::real)"
5.371 -  by (metis incseq_def LIMSEQ_le_const)
5.372 -
5.373 -lemma decseq_le: "decseq X \<Longrightarrow> X ----> L \<Longrightarrow> (L::real) \<le> X n"
5.374 -  by (metis decseq_def LIMSEQ_le_const2)
5.375 -
5.376  subsection {* Cauchy Sequences *}
5.377
5.378  lemma metric_CauchyI:
```
```     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:42 2013 +0100
6.3 @@ -0,0 +1,1511 @@
6.4 +(*  Title:      HOL/Basic_Topology.thy
6.5 +    Author:     Brian Huffman
6.6 +    Author:     Johannes HÃ¶lzl
6.7 +*)
6.8 +
6.9 +header {* Topological Spaces *}
6.10 +
6.11 +theory Topological_Spaces
6.12 +imports Main
6.13 +begin
6.14 +
6.15 +subsection {* Topological space *}
6.16 +
6.17 +class "open" =
6.18 +  fixes "open" :: "'a set \<Rightarrow> bool"
6.19 +
6.20 +class topological_space = "open" +
6.21 +  assumes open_UNIV [simp, intro]: "open UNIV"
6.22 +  assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
6.23 +  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
6.24 +begin
6.25 +
6.26 +definition
6.27 +  closed :: "'a set \<Rightarrow> bool" where
6.28 +  "closed S \<longleftrightarrow> open (- S)"
6.29 +
6.30 +lemma open_empty [intro, simp]: "open {}"
6.31 +  using open_Union [of "{}"] by simp
6.32 +
6.33 +lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
6.34 +  using open_Union [of "{S, T}"] by simp
6.35 +
6.36 +lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
6.37 +  unfolding SUP_def by (rule open_Union) auto
6.38 +
6.39 +lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
6.40 +  by (induct set: finite) auto
6.41 +
6.42 +lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
6.43 +  unfolding INF_def by (rule open_Inter) auto
6.44 +
6.45 +lemma closed_empty [intro, simp]:  "closed {}"
6.46 +  unfolding closed_def by simp
6.47 +
6.48 +lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
6.49 +  unfolding closed_def by auto
6.50 +
6.51 +lemma closed_UNIV [intro, simp]: "closed UNIV"
6.52 +  unfolding closed_def by simp
6.53 +
6.54 +lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
6.55 +  unfolding closed_def by auto
6.56 +
6.57 +lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
6.58 +  unfolding closed_def by auto
6.59 +
6.60 +lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
6.61 +  unfolding closed_def uminus_Inf by auto
6.62 +
6.63 +lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
6.64 +  by (induct set: finite) auto
6.65 +
6.66 +lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
6.67 +  unfolding SUP_def by (rule closed_Union) auto
6.68 +
6.69 +lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
6.70 +  unfolding closed_def by simp
6.71 +
6.72 +lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
6.73 +  unfolding closed_def by simp
6.74 +
6.75 +lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
6.76 +  unfolding closed_open Diff_eq by (rule open_Int)
6.77 +
6.78 +lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
6.79 +  unfolding open_closed Diff_eq by (rule closed_Int)
6.80 +
6.81 +lemma open_Compl [intro]: "closed S \<Longrightarrow> open (- S)"
6.82 +  unfolding closed_open .
6.83 +
6.84 +lemma closed_Compl [intro]: "open S \<Longrightarrow> closed (- S)"
6.85 +  unfolding open_closed .
6.86 +
6.87 +end
6.88 +
6.89 +subsection{* Hausdorff and other separation properties *}
6.90 +
6.91 +class t0_space = topological_space +
6.92 +  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
6.93 +
6.94 +class t1_space = topological_space +
6.95 +  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
6.96 +
6.97 +instance t1_space \<subseteq> t0_space
6.98 +proof qed (fast dest: t1_space)
6.99 +
6.100 +lemma separation_t1:
6.101 +  fixes x y :: "'a::t1_space"
6.102 +  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
6.103 +  using t1_space[of x y] by blast
6.104 +
6.105 +lemma closed_singleton:
6.106 +  fixes a :: "'a::t1_space"
6.107 +  shows "closed {a}"
6.108 +proof -
6.109 +  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
6.110 +  have "open ?T" by (simp add: open_Union)
6.111 +  also have "?T = - {a}"
6.112 +    by (simp add: set_eq_iff separation_t1, auto)
6.113 +  finally show "closed {a}" unfolding closed_def .
6.114 +qed
6.115 +
6.116 +lemma closed_insert [simp]:
6.117 +  fixes a :: "'a::t1_space"
6.118 +  assumes "closed S" shows "closed (insert a S)"
6.119 +proof -
6.120 +  from closed_singleton assms
6.121 +  have "closed ({a} \<union> S)" by (rule closed_Un)
6.122 +  thus "closed (insert a S)" by simp
6.123 +qed
6.124 +
6.125 +lemma finite_imp_closed:
6.126 +  fixes S :: "'a::t1_space set"
6.127 +  shows "finite S \<Longrightarrow> closed S"
6.128 +by (induct set: finite, simp_all)
6.129 +
6.130 +text {* T2 spaces are also known as Hausdorff spaces. *}
6.131 +
6.132 +class t2_space = topological_space +
6.133 +  assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
6.134 +
6.135 +instance t2_space \<subseteq> t1_space
6.136 +proof qed (fast dest: hausdorff)
6.137 +
6.138 +lemma separation_t2:
6.139 +  fixes x y :: "'a::t2_space"
6.140 +  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
6.141 +  using hausdorff[of x y] by blast
6.142 +
6.143 +lemma separation_t0:
6.144 +  fixes x y :: "'a::t0_space"
6.145 +  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
6.146 +  using t0_space[of x y] by blast
6.147 +
6.148 +text {* A perfect space is a topological space with no isolated points. *}
6.149 +
6.150 +class perfect_space = topological_space +
6.151 +  assumes not_open_singleton: "\<not> open {x}"
6.152 +
6.153 +
6.154 +subsection {* Generators for toplogies *}
6.155 +
6.156 +inductive generate_topology for S where
6.157 +  UNIV: "generate_topology S UNIV"
6.158 +| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"
6.159 +| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
6.160 +| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
6.161 +
6.162 +hide_fact (open) UNIV Int UN Basis
6.163 +
6.164 +lemma generate_topology_Union:
6.165 +  "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
6.166 +  unfolding SUP_def by (intro generate_topology.UN) auto
6.167 +
6.168 +lemma topological_space_generate_topology:
6.169 +  "class.topological_space (generate_topology S)"
6.170 +  by default (auto intro: generate_topology.intros)
6.171 +
6.172 +subsection {* Order topologies *}
6.173 +
6.174 +class order_topology = order + "open" +
6.175 +  assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
6.176 +begin
6.177 +
6.178 +subclass topological_space
6.179 +  unfolding open_generated_order
6.180 +  by (rule topological_space_generate_topology)
6.181 +
6.182 +lemma open_greaterThan [simp]: "open {a <..}"
6.183 +  unfolding open_generated_order by (auto intro: generate_topology.Basis)
6.184 +
6.185 +lemma open_lessThan [simp]: "open {..< a}"
6.186 +  unfolding open_generated_order by (auto intro: generate_topology.Basis)
6.187 +
6.188 +lemma open_greaterThanLessThan [simp]: "open {a <..< b}"
6.189 +   unfolding greaterThanLessThan_eq by (simp add: open_Int)
6.190 +
6.191 +end
6.192 +
6.193 +class linorder_topology = linorder + order_topology
6.194 +
6.195 +lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"
6.196 +  by (simp add: closed_open)
6.197 +
6.198 +lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"
6.199 +  by (simp add: closed_open)
6.200 +
6.201 +lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"
6.202 +proof -
6.203 +  have "{a .. b} = {a ..} \<inter> {.. b}"
6.204 +    by auto
6.205 +  then show ?thesis
6.206 +    by (simp add: closed_Int)
6.207 +qed
6.208 +
6.209 +lemma (in linorder) less_separate:
6.210 +  assumes "x < y"
6.211 +  shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
6.212 +proof cases
6.213 +  assume "\<exists>z. x < z \<and> z < y"
6.214 +  then guess z ..
6.215 +  then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
6.216 +    by auto
6.217 +  then show ?thesis by blast
6.218 +next
6.219 +  assume "\<not> (\<exists>z. x < z \<and> z < y)"
6.220 +  with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
6.221 +    by auto
6.222 +  then show ?thesis by blast
6.223 +qed
6.224 +
6.225 +instance linorder_topology \<subseteq> t2_space
6.226 +proof
6.227 +  fix x y :: 'a
6.228 +  from less_separate[of x y] less_separate[of y x]
6.229 +  show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
6.230 +    by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
6.231 +qed
6.232 +
6.233 +lemma open_right:
6.234 +  fixes S :: "'a :: {no_top, linorder_topology} set"
6.235 +  assumes "open S" "x \<in> S" shows "\<exists>b>x. {x ..< b} \<subseteq> S"
6.236 +  using assms unfolding open_generated_order
6.237 +proof induction
6.238 +  case (Int A B)
6.239 +  then obtain a b where "a > x" "{x ..< a} \<subseteq> A"  "b > x" "{x ..< b} \<subseteq> B" by auto
6.240 +  then show ?case by (auto intro!: exI[of _ "min a b"])
6.241 +next
6.242 +  case (Basis S)
6.243 +  moreover from gt_ex[of x] guess b ..
6.244 +  ultimately show ?case by (fastforce intro: exI[of _ b])
6.245 +qed (fastforce intro: gt_ex)+
6.246 +
6.247 +lemma open_left:
6.248 +  fixes S :: "'a :: {no_bot, linorder_topology} set"
6.249 +  assumes "open S" "x \<in> S" shows "\<exists>b<x. {b <.. x} \<subseteq> S"
6.250 +  using assms unfolding open_generated_order
6.251 +proof induction
6.252 +  case (Int A B)
6.253 +  then obtain a b where "a < x" "{a <.. x} \<subseteq> A"  "b < x" "{b <.. x} \<subseteq> B" by auto
6.254 +  then show ?case by (auto intro!: exI[of _ "max a b"])
6.255 +next
6.256 +  case (Basis S)
6.257 +  moreover from lt_ex[of x] guess b ..
6.258 +  ultimately show ?case by (fastforce intro: exI[of _ b])
6.259 +next
6.260 +  case UN then show ?case by blast
6.261 +qed (fastforce intro: lt_ex)
6.262 +
6.263 +subsection {* Filters *}
6.264 +
6.265 +text {*
6.266 +  This definition also allows non-proper filters.
6.267 +*}
6.268 +
6.269 +locale is_filter =
6.270 +  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
6.271 +  assumes True: "F (\<lambda>x. True)"
6.272 +  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
6.273 +  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
6.274 +
6.275 +typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
6.276 +proof
6.277 +  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
6.278 +qed
6.279 +
6.280 +lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
6.281 +  using Rep_filter [of F] by simp
6.282 +
6.283 +lemma Abs_filter_inverse':
6.284 +  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
6.285 +  using assms by (simp add: Abs_filter_inverse)
6.286 +
6.287 +
6.288 +subsubsection {* Eventually *}
6.289 +
6.290 +definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
6.291 +  where "eventually P F \<longleftrightarrow> Rep_filter F P"
6.292 +
6.293 +lemma eventually_Abs_filter:
6.294 +  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
6.295 +  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
6.296 +
6.297 +lemma filter_eq_iff:
6.298 +  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
6.299 +  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
6.300 +
6.301 +lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
6.302 +  unfolding eventually_def
6.303 +  by (rule is_filter.True [OF is_filter_Rep_filter])
6.304 +
6.305 +lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
6.306 +proof -
6.307 +  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
6.308 +  thus "eventually P F" by simp
6.309 +qed
6.310 +
6.311 +lemma eventually_mono:
6.312 +  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
6.313 +  unfolding eventually_def
6.314 +  by (rule is_filter.mono [OF is_filter_Rep_filter])
6.315 +
6.316 +lemma eventually_conj:
6.317 +  assumes P: "eventually (\<lambda>x. P x) F"
6.318 +  assumes Q: "eventually (\<lambda>x. Q x) F"
6.319 +  shows "eventually (\<lambda>x. P x \<and> Q x) F"
6.320 +  using assms unfolding eventually_def
6.321 +  by (rule is_filter.conj [OF is_filter_Rep_filter])
6.322 +
6.323 +lemma eventually_Ball_finite:
6.324 +  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
6.325 +  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
6.326 +using assms by (induct set: finite, simp, simp add: eventually_conj)
6.327 +
6.328 +lemma eventually_all_finite:
6.329 +  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
6.330 +  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
6.331 +  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
6.332 +using eventually_Ball_finite [of UNIV P] assms by simp
6.333 +
6.334 +lemma eventually_mp:
6.335 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
6.336 +  assumes "eventually (\<lambda>x. P x) F"
6.337 +  shows "eventually (\<lambda>x. Q x) F"
6.338 +proof (rule eventually_mono)
6.339 +  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
6.340 +  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
6.341 +    using assms by (rule eventually_conj)
6.342 +qed
6.343 +
6.344 +lemma eventually_rev_mp:
6.345 +  assumes "eventually (\<lambda>x. P x) F"
6.346 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
6.347 +  shows "eventually (\<lambda>x. Q x) F"
6.348 +using assms(2) assms(1) by (rule eventually_mp)
6.349 +
6.350 +lemma eventually_conj_iff:
6.351 +  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
6.352 +  by (auto intro: eventually_conj elim: eventually_rev_mp)
6.353 +
6.354 +lemma eventually_elim1:
6.355 +  assumes "eventually (\<lambda>i. P i) F"
6.356 +  assumes "\<And>i. P i \<Longrightarrow> Q i"
6.357 +  shows "eventually (\<lambda>i. Q i) F"
6.358 +  using assms by (auto elim!: eventually_rev_mp)
6.359 +
6.360 +lemma eventually_elim2:
6.361 +  assumes "eventually (\<lambda>i. P i) F"
6.362 +  assumes "eventually (\<lambda>i. Q i) F"
6.363 +  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
6.364 +  shows "eventually (\<lambda>i. R i) F"
6.365 +  using assms by (auto elim!: eventually_rev_mp)
6.366 +
6.367 +lemma eventually_subst:
6.368 +  assumes "eventually (\<lambda>n. P n = Q n) F"
6.369 +  shows "eventually P F = eventually Q F" (is "?L = ?R")
6.370 +proof -
6.371 +  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
6.372 +      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
6.373 +    by (auto elim: eventually_elim1)
6.374 +  then show ?thesis by (auto elim: eventually_elim2)
6.375 +qed
6.376 +
6.377 +ML {*
6.378 +  fun eventually_elim_tac ctxt thms thm =
6.379 +    let
6.380 +      val thy = Proof_Context.theory_of ctxt
6.381 +      val mp_thms = thms RL [@{thm eventually_rev_mp}]
6.382 +      val raw_elim_thm =
6.383 +        (@{thm allI} RS @{thm always_eventually})
6.384 +        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
6.385 +        |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
6.386 +      val cases_prop = prop_of (raw_elim_thm RS thm)
6.387 +      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
6.388 +    in
6.389 +      CASES cases (rtac raw_elim_thm 1) thm
6.390 +    end
6.391 +*}
6.392 +
6.393 +method_setup eventually_elim = {*
6.394 +  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
6.395 +*} "elimination of eventually quantifiers"
6.396 +
6.397 +
6.398 +subsubsection {* Finer-than relation *}
6.399 +
6.400 +text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
6.401 +filter @{term F'}. *}
6.402 +
6.403 +instantiation filter :: (type) complete_lattice
6.404 +begin
6.405 +
6.406 +definition le_filter_def:
6.407 +  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
6.408 +
6.409 +definition
6.410 +  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
6.411 +
6.412 +definition
6.413 +  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
6.414 +
6.415 +definition
6.416 +  "bot = Abs_filter (\<lambda>P. True)"
6.417 +
6.418 +definition
6.419 +  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
6.420 +
6.421 +definition
6.422 +  "inf F F' = Abs_filter
6.423 +      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
6.424 +
6.425 +definition
6.426 +  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
6.427 +
6.428 +definition
6.429 +  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
6.430 +
6.431 +lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
6.432 +  unfolding top_filter_def
6.433 +  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
6.434 +
6.435 +lemma eventually_bot [simp]: "eventually P bot"
6.436 +  unfolding bot_filter_def
6.437 +  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
6.438 +
6.439 +lemma eventually_sup:
6.440 +  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
6.441 +  unfolding sup_filter_def
6.442 +  by (rule eventually_Abs_filter, rule is_filter.intro)
6.443 +     (auto elim!: eventually_rev_mp)
6.444 +
6.445 +lemma eventually_inf:
6.446 +  "eventually P (inf F F') \<longleftrightarrow>
6.447 +   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
6.448 +  unfolding inf_filter_def
6.449 +  apply (rule eventually_Abs_filter, rule is_filter.intro)
6.450 +  apply (fast intro: eventually_True)
6.451 +  apply clarify
6.452 +  apply (intro exI conjI)
6.453 +  apply (erule (1) eventually_conj)
6.454 +  apply (erule (1) eventually_conj)
6.455 +  apply simp
6.456 +  apply auto
6.457 +  done
6.458 +
6.459 +lemma eventually_Sup:
6.460 +  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
6.461 +  unfolding Sup_filter_def
6.462 +  apply (rule eventually_Abs_filter, rule is_filter.intro)
6.463 +  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
6.464 +  done
6.465 +
6.466 +instance proof
6.467 +  fix F F' F'' :: "'a filter" and S :: "'a filter set"
6.468 +  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
6.469 +    by (rule less_filter_def) }
6.470 +  { show "F \<le> F"
6.471 +    unfolding le_filter_def by simp }
6.472 +  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
6.473 +    unfolding le_filter_def by simp }
6.474 +  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
6.475 +    unfolding le_filter_def filter_eq_iff by fast }
6.476 +  { show "F \<le> top"
6.477 +    unfolding le_filter_def eventually_top by (simp add: always_eventually) }
6.478 +  { show "bot \<le> F"
6.479 +    unfolding le_filter_def by simp }
6.480 +  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
6.481 +    unfolding le_filter_def eventually_sup by simp_all }
6.482 +  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
6.483 +    unfolding le_filter_def eventually_sup by simp }
6.484 +  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
6.485 +    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
6.486 +  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
6.487 +    unfolding le_filter_def eventually_inf
6.488 +    by (auto elim!: eventually_mono intro: eventually_conj) }
6.489 +  { assume "F \<in> S" thus "F \<le> Sup S"
6.490 +    unfolding le_filter_def eventually_Sup by simp }
6.491 +  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
6.492 +    unfolding le_filter_def eventually_Sup by simp }
6.493 +  { assume "F'' \<in> S" thus "Inf S \<le> F''"
6.494 +    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
6.495 +  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
6.496 +    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
6.497 +qed
6.498 +
6.499 +end
6.500 +
6.501 +lemma filter_leD:
6.502 +  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
6.503 +  unfolding le_filter_def by simp
6.504 +
6.505 +lemma filter_leI:
6.506 +  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
6.507 +  unfolding le_filter_def by simp
6.508 +
6.509 +lemma eventually_False:
6.510 +  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
6.511 +  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
6.512 +
6.513 +abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
6.514 +  where "trivial_limit F \<equiv> F = bot"
6.515 +
6.516 +lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
6.517 +  by (rule eventually_False [symmetric])
6.518 +
6.519 +lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
6.520 +  by (cases P) (simp_all add: eventually_False)
6.521 +
6.522 +
6.523 +subsubsection {* Map function for filters *}
6.524 +
6.525 +definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
6.526 +  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
6.527 +
6.528 +lemma eventually_filtermap:
6.529 +  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
6.530 +  unfolding filtermap_def
6.531 +  apply (rule eventually_Abs_filter)
6.532 +  apply (rule is_filter.intro)
6.533 +  apply (auto elim!: eventually_rev_mp)
6.534 +  done
6.535 +
6.536 +lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
6.537 +  by (simp add: filter_eq_iff eventually_filtermap)
6.538 +
6.539 +lemma filtermap_filtermap:
6.540 +  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
6.541 +  by (simp add: filter_eq_iff eventually_filtermap)
6.542 +
6.543 +lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
6.544 +  unfolding le_filter_def eventually_filtermap by simp
6.545 +
6.546 +lemma filtermap_bot [simp]: "filtermap f bot = bot"
6.547 +  by (simp add: filter_eq_iff eventually_filtermap)
6.548 +
6.549 +lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
6.550 +  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
6.551 +
6.552 +subsubsection {* Order filters *}
6.553 +
6.554 +definition at_top :: "('a::order) filter"
6.555 +  where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
6.556 +
6.557 +lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
6.558 +  unfolding at_top_def
6.559 +proof (rule eventually_Abs_filter, rule is_filter.intro)
6.560 +  fix P Q :: "'a \<Rightarrow> bool"
6.561 +  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
6.562 +  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
6.563 +  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
6.564 +  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
6.565 +qed auto
6.566 +
6.567 +lemma eventually_ge_at_top:
6.568 +  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
6.569 +  unfolding eventually_at_top_linorder by auto
6.570 +
6.571 +lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
6.572 +  unfolding eventually_at_top_linorder
6.573 +proof safe
6.574 +  fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
6.575 +next
6.576 +  fix N assume "\<forall>n>N. P n"
6.577 +  moreover from gt_ex[of N] guess y ..
6.578 +  ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
6.579 +qed
6.580 +
6.581 +lemma eventually_gt_at_top:
6.582 +  "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
6.583 +  unfolding eventually_at_top_dense by auto
6.584 +
6.585 +definition at_bot :: "('a::order) filter"
6.586 +  where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"
6.587 +
6.588 +lemma eventually_at_bot_linorder:
6.589 +  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
6.590 +  unfolding at_bot_def
6.591 +proof (rule eventually_Abs_filter, rule is_filter.intro)
6.592 +  fix P Q :: "'a \<Rightarrow> bool"
6.593 +  assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n"
6.594 +  then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto
6.595 +  then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp
6.596 +  then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..
6.597 +qed auto
6.598 +
6.599 +lemma eventually_le_at_bot:
6.600 +  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
6.601 +  unfolding eventually_at_bot_linorder by auto
6.602 +
6.603 +lemma eventually_at_bot_dense:
6.604 +  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
6.605 +  unfolding eventually_at_bot_linorder
6.606 +proof safe
6.607 +  fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
6.608 +next
6.609 +  fix N assume "\<forall>n<N. P n"
6.610 +  moreover from lt_ex[of N] guess y ..
6.611 +  ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
6.612 +qed
6.613 +
6.614 +lemma eventually_gt_at_bot:
6.615 +  "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
6.616 +  unfolding eventually_at_bot_dense by auto
6.617 +
6.618 +subsection {* Sequentially *}
6.619 +
6.620 +abbreviation sequentially :: "nat filter"
6.621 +  where "sequentially == at_top"
6.622 +
6.623 +lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
6.624 +  unfolding at_top_def by simp
6.625 +
6.626 +lemma eventually_sequentially:
6.627 +  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
6.628 +  by (rule eventually_at_top_linorder)
6.629 +
6.630 +lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
6.631 +  unfolding filter_eq_iff eventually_sequentially by auto
6.632 +
6.633 +lemmas trivial_limit_sequentially = sequentially_bot
6.634 +
6.635 +lemma eventually_False_sequentially [simp]:
6.636 +  "\<not> eventually (\<lambda>n. False) sequentially"
6.637 +  by (simp add: eventually_False)
6.638 +
6.639 +lemma le_sequentially:
6.640 +  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
6.641 +  unfolding le_filter_def eventually_sequentially
6.642 +  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
6.643 +
6.644 +lemma eventually_sequentiallyI:
6.645 +  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
6.646 +  shows "eventually P sequentially"
6.647 +using assms by (auto simp: eventually_sequentially)
6.648 +
6.649 +
6.650 +subsubsection {* Standard filters *}
6.651 +
6.652 +definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
6.653 +  where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
6.654 +
6.655 +lemma eventually_within:
6.656 +  "eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F"
6.657 +  unfolding within_def
6.658 +  by (rule eventually_Abs_filter, rule is_filter.intro)
6.659 +     (auto elim!: eventually_rev_mp)
6.660 +
6.661 +lemma within_UNIV [simp]: "F within UNIV = F"
6.662 +  unfolding filter_eq_iff eventually_within by simp
6.663 +
6.664 +lemma within_empty [simp]: "F within {} = bot"
6.665 +  unfolding filter_eq_iff eventually_within by simp
6.666 +
6.667 +lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
6.668 +  by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
6.669 +
6.670 +lemma within_le: "F within S \<le> F"
6.671 +  unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
6.672 +
6.673 +lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
6.674 +  unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
6.675 +
6.676 +lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
6.677 +  by (blast intro: within_le le_withinI order_trans)
6.678 +
6.679 +subsubsection {* Topological filters *}
6.680 +
6.681 +definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
6.682 +  where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
6.683 +
6.684 +definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
6.685 +  where "at a = nhds a within - {a}"
6.686 +
6.687 +abbreviation at_right :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
6.688 +  "at_right x \<equiv> at x within {x <..}"
6.689 +
6.690 +abbreviation at_left :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
6.691 +  "at_left x \<equiv> at x within {..< x}"
6.692 +
6.693 +lemma eventually_nhds:
6.694 +  "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
6.695 +  unfolding nhds_def
6.696 +proof (rule eventually_Abs_filter, rule is_filter.intro)
6.697 +  have "open (UNIV :: 'a :: topological_space set) \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
6.698 +  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" ..
6.699 +next
6.700 +  fix P Q
6.701 +  assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
6.702 +     and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)"
6.703 +  then obtain S T where
6.704 +    "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
6.705 +    "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto
6.706 +  hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"
6.707 +    by (simp add: open_Int)
6.708 +  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" ..
6.709 +qed auto
6.710 +
6.711 +lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
6.712 +  unfolding trivial_limit_def eventually_nhds by simp
6.713 +
6.714 +lemma eventually_at_topological:
6.715 +  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
6.716 +unfolding at_def eventually_within eventually_nhds by simp
6.717 +
6.718 +lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
6.719 +  unfolding trivial_limit_def eventually_at_topological
6.720 +  by (safe, case_tac "S = {a}", simp, fast, fast)
6.721 +
6.722 +lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
6.723 +  by (simp add: at_eq_bot_iff not_open_singleton)
6.724 +
6.725 +lemma eventually_at_right:
6.726 +  fixes x :: "'a :: {no_top, linorder_topology}"
6.727 +  shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
6.728 +  unfolding eventually_nhds eventually_within at_def
6.729 +proof safe
6.730 +  fix S assume "open S" "x \<in> S"
6.731 +  note open_right[OF this]
6.732 +  moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
6.733 +  ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
6.734 +    by (auto simp: subset_eq Ball_def)
6.735 +next
6.736 +  fix b assume "x < b" "\<forall>z. x < z \<and> z < b \<longrightarrow> P z"
6.737 +  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in> - {x} \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)"
6.738 +    by (intro exI[of _ "{..< b}"]) auto
6.739 +qed
6.740 +
6.741 +lemma eventually_at_left:
6.742 +  fixes x :: "'a :: {no_bot, linorder_topology}"
6.743 +  shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
6.744 +  unfolding eventually_nhds eventually_within at_def
6.745 +proof safe
6.746 +  fix S assume "open S" "x \<in> S"
6.747 +  note open_left[OF this]
6.748 +  moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
6.749 +  ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
6.750 +    by (auto simp: subset_eq Ball_def)
6.751 +next
6.752 +  fix b assume "b < x" "\<forall>z. b < z \<and> z < x \<longrightarrow> P z"
6.753 +  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in> - {x} \<longrightarrow> xa \<in> {..<x} \<longrightarrow> P xa)"
6.754 +    by (intro exI[of _ "{b <..}"]) auto
6.755 +qed
6.756 +
6.757 +lemma trivial_limit_at_left_real [simp]:
6.758 +  "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_linorder, linorder_topology}))"
6.759 +  unfolding trivial_limit_def eventually_at_left by (auto dest: dense)
6.760 +
6.761 +lemma trivial_limit_at_right_real [simp]:
6.762 +  "\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
6.763 +  unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
6.764 +
6.765 +lemma at_within_eq: "at x within T = nhds x within (T - {x})"
6.766 +  unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
6.767 +
6.768 +lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
6.769 +  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup
6.770 +           elim: eventually_elim2 eventually_elim1)
6.771 +
6.772 +lemma eventually_at_split:
6.773 +  "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
6.774 +  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
6.775 +
6.776 +subsection {* Limits *}
6.777 +
6.778 +definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
6.779 +  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
6.780 +
6.781 +syntax
6.782 +  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
6.783 +
6.784 +translations
6.785 +  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
6.786 +
6.787 +lemma filterlim_iff:
6.788 +  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
6.789 +  unfolding filterlim_def le_filter_def eventually_filtermap ..
6.790 +
6.791 +lemma filterlim_compose:
6.792 +  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
6.793 +  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
6.794 +
6.795 +lemma filterlim_mono:
6.796 +  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
6.797 +  unfolding filterlim_def by (metis filtermap_mono order_trans)
6.798 +
6.799 +lemma filterlim_ident: "LIM x F. x :> F"
6.800 +  by (simp add: filterlim_def filtermap_ident)
6.801 +
6.802 +lemma filterlim_cong:
6.803 +  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
6.804 +  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
6.805 +
6.806 +lemma filterlim_within:
6.807 +  "(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))"
6.808 +  unfolding filterlim_def
6.809 +proof safe
6.810 +  assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1"
6.811 +    by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
6.812 +qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
6.813 +
6.814 +lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
6.815 +  unfolding filterlim_def filtermap_filtermap ..
6.816 +
6.817 +lemma filterlim_sup:
6.818 +  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
6.819 +  unfolding filterlim_def filtermap_sup by auto
6.820 +
6.821 +lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
6.822 +  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
6.823 +
6.824 +subsubsection {* Tendsto *}
6.825 +
6.826 +abbreviation (in topological_space)
6.827 +  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
6.828 +  "(f ---> l) F \<equiv> filterlim f (nhds l) F"
6.829 +
6.830 +lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
6.831 +  by simp
6.832 +
6.833 +ML {*
6.834 +
6.835 +structure Tendsto_Intros = Named_Thms
6.836 +(
6.837 +  val name = @{binding tendsto_intros}
6.838 +  val description = "introduction rules for tendsto"
6.839 +)
6.840 +
6.841 +*}
6.842 +
6.843 +setup {*
6.844 +  Tendsto_Intros.setup #>
6.846 +    map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
6.847 +*}
6.848 +
6.849 +lemma tendsto_def: "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
6.850 +  unfolding filterlim_def
6.851 +proof safe
6.852 +  fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
6.853 +  then show "eventually (\<lambda>x. f x \<in> S) F"
6.854 +    unfolding eventually_nhds eventually_filtermap le_filter_def
6.855 +    by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
6.856 +qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
6.857 +
6.858 +lemma filterlim_at:
6.859 +  "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
6.860 +  by (simp add: at_def filterlim_within)
6.861 +
6.862 +lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
6.863 +  unfolding tendsto_def le_filter_def by fast
6.864 +
6.865 +lemma topological_tendstoI:
6.866 +  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F)
6.867 +    \<Longrightarrow> (f ---> l) F"
6.868 +  unfolding tendsto_def by auto
6.869 +
6.870 +lemma topological_tendstoD:
6.871 +  "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
6.872 +  unfolding tendsto_def by auto
6.873 +
6.874 +lemma order_tendstoI:
6.875 +  fixes y :: "_ :: order_topology"
6.876 +  assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
6.877 +  assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
6.878 +  shows "(f ---> y) F"
6.879 +proof (rule topological_tendstoI)
6.880 +  fix S assume "open S" "y \<in> S"
6.881 +  then show "eventually (\<lambda>x. f x \<in> S) F"
6.882 +    unfolding open_generated_order
6.883 +  proof induct
6.884 +    case (UN K)
6.885 +    then obtain k where "y \<in> k" "k \<in> K" by auto
6.886 +    with UN(2)[of k] show ?case
6.887 +      by (auto elim: eventually_elim1)
6.888 +  qed (insert assms, auto elim: eventually_elim2)
6.889 +qed
6.890 +
6.891 +lemma order_tendstoD:
6.892 +  fixes y :: "_ :: order_topology"
6.893 +  assumes y: "(f ---> y) F"
6.894 +  shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
6.895 +    and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
6.896 +  using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto
6.897 +
6.898 +lemma order_tendsto_iff:
6.899 +  fixes f :: "_ \<Rightarrow> 'a :: order_topology"
6.900 +  shows "(f ---> x) F \<longleftrightarrow>(\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
6.901 +  by (metis order_tendstoI order_tendstoD)
6.902 +
6.903 +lemma tendsto_bot [simp]: "(f ---> a) bot"
6.904 +  unfolding tendsto_def by simp
6.905 +
6.906 +lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
6.907 +  unfolding tendsto_def eventually_at_topological by auto
6.908 +
6.909 +lemma tendsto_ident_at_within [tendsto_intros]:
6.910 +  "((\<lambda>x. x) ---> a) (at a within S)"
6.911 +  unfolding tendsto_def eventually_within eventually_at_topological by auto
6.912 +
6.913 +lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
6.914 +  by (simp add: tendsto_def)
6.915 +
6.916 +lemma tendsto_unique:
6.917 +  fixes f :: "'a \<Rightarrow> 'b::t2_space"
6.918 +  assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
6.919 +  shows "a = b"
6.920 +proof (rule ccontr)
6.921 +  assume "a \<noteq> b"
6.922 +  obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
6.923 +    using hausdorff [OF `a \<noteq> b`] by fast
6.924 +  have "eventually (\<lambda>x. f x \<in> U) F"
6.925 +    using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD)
6.926 +  moreover
6.927 +  have "eventually (\<lambda>x. f x \<in> V) F"
6.928 +    using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
6.929 +  ultimately
6.930 +  have "eventually (\<lambda>x. False) F"
6.931 +  proof eventually_elim
6.932 +    case (elim x)
6.933 +    hence "f x \<in> U \<inter> V" by simp
6.934 +    with `U \<inter> V = {}` show ?case by simp
6.935 +  qed
6.936 +  with `\<not> trivial_limit F` show "False"
6.937 +    by (simp add: trivial_limit_def)
6.938 +qed
6.939 +
6.940 +lemma tendsto_const_iff:
6.941 +  fixes a b :: "'a::t2_space"
6.942 +  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
6.943 +  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
6.944 +
6.945 +lemma increasing_tendsto:
6.946 +  fixes f :: "_ \<Rightarrow> 'a::order_topology"
6.947 +  assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
6.948 +      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
6.949 +  shows "(f ---> l) F"
6.950 +  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
6.951 +
6.952 +lemma decreasing_tendsto:
6.953 +  fixes f :: "_ \<Rightarrow> 'a::order_topology"
6.954 +  assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
6.955 +      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
6.956 +  shows "(f ---> l) F"
6.957 +  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
6.958 +
6.959 +lemma tendsto_sandwich:
6.960 +  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
6.961 +  assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
6.962 +  assumes lim: "(f ---> c) net" "(h ---> c) net"
6.963 +  shows "(g ---> c) net"
6.964 +proof (rule order_tendstoI)
6.965 +  fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
6.966 +    using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
6.967 +next
6.968 +  fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
6.969 +    using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
6.970 +qed
6.971 +
6.972 +lemma tendsto_le:
6.973 +  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
6.974 +  assumes F: "\<not> trivial_limit F"
6.975 +  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
6.976 +  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
6.977 +  shows "y \<le> x"
6.978 +proof (rule ccontr)
6.979 +  assume "\<not> y \<le> x"
6.980 +  with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
6.981 +    by (auto simp: not_le)
6.982 +  then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
6.983 +    using x y by (auto intro: order_tendstoD)
6.984 +  with ev have "eventually (\<lambda>x. False) F"
6.985 +    by eventually_elim (insert xy, fastforce)
6.986 +  with F show False
6.987 +    by (simp add: eventually_False)
6.988 +qed
6.989 +
6.990 +lemma tendsto_le_const:
6.991 +  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
6.992 +  assumes F: "\<not> trivial_limit F"
6.993 +  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
6.994 +  shows "a \<le> x"
6.995 +  using F x tendsto_const a by (rule tendsto_le)
6.996 +
6.997 +subsection {* Limits to @{const at_top} and @{const at_bot} *}
6.998 +
6.999 +lemma filterlim_at_top:
6.1000 +  fixes f :: "'a \<Rightarrow> ('b::linorder)"
6.1001 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
6.1002 +  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
6.1003 +
6.1004 +lemma filterlim_at_top_dense:
6.1005 +  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
6.1006 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
6.1007 +  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
6.1008 +            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
6.1009 +
6.1010 +lemma filterlim_at_top_ge:
6.1011 +  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
6.1012 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
6.1013 +  unfolding filterlim_at_top
6.1014 +proof safe
6.1015 +  fix Z assume *: "\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F"
6.1016 +  with *[THEN spec, of "max Z c"] show "eventually (\<lambda>x. Z \<le> f x) F"
6.1017 +    by (auto elim!: eventually_elim1)
6.1018 +qed simp
6.1019 +
6.1020 +lemma filterlim_at_top_at_top:
6.1021 +  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
6.1022 +  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
6.1023 +  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
6.1024 +  assumes Q: "eventually Q at_top"
6.1025 +  assumes P: "eventually P at_top"
6.1026 +  shows "filterlim f at_top at_top"
6.1027 +proof -
6.1028 +  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
6.1029 +    unfolding eventually_at_top_linorder by auto
6.1030 +  show ?thesis
6.1031 +  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
6.1032 +    fix z assume "x \<le> z"
6.1033 +    with x have "P z" by auto
6.1034 +    have "eventually (\<lambda>x. g z \<le> x) at_top"
6.1035 +      by (rule eventually_ge_at_top)
6.1036 +    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
6.1037 +      by eventually_elim (metis mono bij `P z`)
6.1038 +  qed
6.1039 +qed
6.1040 +
6.1041 +lemma filterlim_at_top_gt:
6.1042 +  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
6.1043 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
6.1044 +  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
6.1045 +
6.1046 +lemma filterlim_at_bot:
6.1047 +  fixes f :: "'a \<Rightarrow> ('b::linorder)"
6.1048 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
6.1049 +  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
6.1050 +
6.1051 +lemma filterlim_at_bot_le:
6.1052 +  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
6.1053 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
6.1054 +  unfolding filterlim_at_bot
6.1055 +proof safe
6.1056 +  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
6.1057 +  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
6.1058 +    by (auto elim!: eventually_elim1)
6.1059 +qed simp
6.1060 +
6.1061 +lemma filterlim_at_bot_lt:
6.1062 +  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
6.1063 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
6.1064 +  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
6.1065 +
6.1066 +lemma filterlim_at_bot_at_right:
6.1067 +  fixes f :: "'a::{no_top, linorder_topology} \<Rightarrow> 'b::linorder"
6.1068 +  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
6.1069 +  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
6.1070 +  assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b"
6.1071 +  assumes P: "eventually P at_bot"
6.1072 +  shows "filterlim f at_bot (at_right a)"
6.1073 +proof -
6.1074 +  from P obtain x where x: "\<And>y. y \<le> x \<Longrightarrow> P y"
6.1075 +    unfolding eventually_at_bot_linorder by auto
6.1076 +  show ?thesis
6.1077 +  proof (intro filterlim_at_bot_le[THEN iffD2] allI impI)
6.1078 +    fix z assume "z \<le> x"
6.1079 +    with x have "P z" by auto
6.1080 +    have "eventually (\<lambda>x. x \<le> g z) (at_right a)"
6.1081 +      using bound[OF bij(2)[OF `P z`]]
6.1082 +      unfolding eventually_at_right by (auto intro!: exI[of _ "g z"])
6.1083 +    with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)"
6.1084 +      by eventually_elim (metis bij `P z` mono)
6.1085 +  qed
6.1086 +qed
6.1087 +
6.1088 +lemma filterlim_at_top_at_left:
6.1089 +  fixes f :: "'a::{no_bot, linorder_topology} \<Rightarrow> 'b::linorder"
6.1090 +  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
6.1091 +  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
6.1092 +  assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a"
6.1093 +  assumes P: "eventually P at_top"
6.1094 +  shows "filterlim f at_top (at_left a)"
6.1095 +proof -
6.1096 +  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
6.1097 +    unfolding eventually_at_top_linorder by auto
6.1098 +  show ?thesis
6.1099 +  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
6.1100 +    fix z assume "x \<le> z"
6.1101 +    with x have "P z" by auto
6.1102 +    have "eventually (\<lambda>x. g z \<le> x) (at_left a)"
6.1103 +      using bound[OF bij(2)[OF `P z`]]
6.1104 +      unfolding eventually_at_left by (auto intro!: exI[of _ "g z"])
6.1105 +    with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)"
6.1106 +      by eventually_elim (metis bij `P z` mono)
6.1107 +  qed
6.1108 +qed
6.1109 +
6.1110 +lemma filterlim_split_at:
6.1111 +  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::'a::linorder_topology))"
6.1112 +  by (subst at_eq_sup_left_right) (rule filterlim_sup)
6.1113 +
6.1114 +lemma filterlim_at_split:
6.1115 +  "filterlim f F (at (x::'a::linorder_topology)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
6.1116 +  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
6.1117 +
6.1118 +
6.1119 +subsection {* Limits on sequences *}
6.1120 +
6.1121 +abbreviation (in topological_space)
6.1122 +  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
6.1123 +    ("((_)/ ----> (_))" [60, 60] 60) where
6.1124 +  "X ----> L \<equiv> (X ---> L) sequentially"
6.1125 +
6.1126 +definition
6.1127 +  lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where
6.1128 +    --{*Standard definition of limit using choice operator*}
6.1129 +  "lim X = (THE L. X ----> L)"
6.1130 +
6.1131 +definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
6.1132 +  "convergent X = (\<exists>L. X ----> L)"
6.1133 +
6.1134 +subsubsection {* Monotone sequences and subsequences *}
6.1135 +
6.1136 +definition
6.1137 +  monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
6.1138 +    --{*Definition of monotonicity.
6.1139 +        The use of disjunction here complicates proofs considerably.
6.1140 +        One alternative is to add a Boolean argument to indicate the direction.
6.1141 +        Another is to develop the notions of increasing and decreasing first.*}
6.1142 +  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
6.1143 +
6.1144 +definition
6.1145 +  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
6.1146 +    --{*Increasing sequence*}
6.1147 +  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
6.1148 +
6.1149 +definition
6.1150 +  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
6.1151 +    --{*Decreasing sequence*}
6.1152 +  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
6.1153 +
6.1154 +definition
6.1155 +  subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
6.1156 +    --{*Definition of subsequence*}
6.1157 +  "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
6.1158 +
6.1159 +lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
6.1160 +  unfolding mono_def incseq_def by auto
6.1161 +
6.1162 +lemma incseq_SucI:
6.1163 +  "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
6.1164 +  using lift_Suc_mono_le[of X]
6.1165 +  by (auto simp: incseq_def)
6.1166 +
6.1167 +lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j"
6.1168 +  by (auto simp: incseq_def)
6.1169 +
6.1170 +lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)"
6.1171 +  using incseqD[of A i "Suc i"] by auto
6.1172 +
6.1173 +lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
6.1174 +  by (auto intro: incseq_SucI dest: incseq_SucD)
6.1175 +
6.1176 +lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)"
6.1177 +  unfolding incseq_def by auto
6.1178 +
6.1179 +lemma decseq_SucI:
6.1180 +  "(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X"
6.1181 +  using order.lift_Suc_mono_le[OF dual_order, of X]
6.1182 +  by (auto simp: decseq_def)
6.1183 +
6.1184 +lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i"
6.1185 +  by (auto simp: decseq_def)
6.1186 +
6.1187 +lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i"
6.1188 +  using decseqD[of A i "Suc i"] by auto
6.1189 +
6.1190 +lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
6.1191 +  by (auto intro: decseq_SucI dest: decseq_SucD)
6.1192 +
6.1193 +lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)"
6.1194 +  unfolding decseq_def by auto
6.1195 +
6.1196 +lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X"
6.1197 +  unfolding monoseq_def incseq_def decseq_def ..
6.1198 +
6.1199 +lemma monoseq_Suc:
6.1200 +  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
6.1201 +  unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..
6.1202 +
6.1203 +lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
6.1205 +
6.1206 +lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
6.1208 +
6.1209 +lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
6.1211 +
6.1212 +lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
6.1214 +
6.1215 +lemma monoseq_minus:
6.1216 +  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
6.1217 +  assumes "monoseq a"
6.1218 +  shows "monoseq (\<lambda> n. - a n)"
6.1219 +proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
6.1220 +  case True
6.1221 +  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
6.1222 +  thus ?thesis by (rule monoI2)
6.1223 +next
6.1224 +  case False
6.1225 +  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto
6.1226 +  thus ?thesis by (rule monoI1)
6.1227 +qed
6.1228 +
6.1229 +text{*Subsequence (alternative definition, (e.g. Hoskins)*}
6.1230 +
6.1231 +lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
6.1234 +apply (induct_tac k)
6.1235 +apply (auto intro: less_trans)
6.1236 +done
6.1237 +
6.1238 +text{* for any sequence, there is a monotonic subsequence *}
6.1239 +lemma seq_monosub:
6.1240 +  fixes s :: "nat => 'a::linorder"
6.1241 +  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
6.1242 +proof cases
6.1243 +  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
6.1244 +  assume *: "\<forall>n. \<exists>p. ?P p n"
6.1245 +  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
6.1246 +  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
6.1247 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
6.1248 +  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
6.1249 +  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
6.1250 +  then have "subseq f" unfolding subseq_Suc_iff by auto
6.1251 +  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
6.1252 +  proof (intro disjI2 allI)
6.1253 +    fix n show "s (f (Suc n)) \<le> s (f n)"
6.1254 +    proof (cases n)
6.1255 +      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
6.1256 +    next
6.1257 +      case (Suc m)
6.1258 +      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
6.1259 +      with P_Suc Suc show ?thesis by simp
6.1260 +    qed
6.1261 +  qed
6.1262 +  ultimately show ?thesis by auto
6.1263 +next
6.1264 +  let "?P p m" = "m < p \<and> s m < s p"
6.1265 +  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
6.1266 +  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
6.1267 +  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
6.1268 +  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
6.1269 +  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
6.1270 +  have P_0: "?P (f 0) (Suc N)"
6.1271 +    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
6.1272 +  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
6.1273 +      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
6.1274 +  note P' = this
6.1275 +  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
6.1276 +      by (induct i) (insert P_0 P', auto) }
6.1277 +  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
6.1278 +    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
6.1279 +  then show ?thesis by auto
6.1280 +qed
6.1281 +
6.1282 +lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
6.1283 +proof(induct n)
6.1284 +  case 0 thus ?case by simp
6.1285 +next
6.1286 +  case (Suc n)
6.1287 +  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
6.1288 +  have "n < f (Suc n)" by arith
6.1289 +  thus ?case by arith
6.1290 +qed
6.1291 +
6.1292 +lemma eventually_subseq:
6.1293 +  "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
6.1294 +  unfolding eventually_sequentially by (metis seq_suble le_trans)
6.1295 +
6.1296 +lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
6.1297 +  unfolding filterlim_iff by (metis eventually_subseq)
6.1298 +
6.1299 +lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
6.1300 +  unfolding subseq_def by simp
6.1301 +
6.1302 +lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
6.1303 +  using assms by (auto simp: subseq_def)
6.1304 +
6.1305 +lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
6.1306 +  by (simp add: incseq_def monoseq_def)
6.1307 +
6.1308 +lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
6.1309 +  by (simp add: decseq_def monoseq_def)
6.1310 +
6.1311 +lemma decseq_eq_incseq:
6.1312 +  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)"
6.1313 +  by (simp add: decseq_def incseq_def)
6.1314 +
6.1315 +lemma INT_decseq_offset:
6.1316 +  assumes "decseq F"
6.1317 +  shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
6.1318 +proof safe
6.1319 +  fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
6.1320 +  show "x \<in> F i"
6.1321 +  proof cases
6.1322 +    from x have "x \<in> F n" by auto
6.1323 +    also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
6.1324 +      unfolding decseq_def by simp
6.1325 +    finally show ?thesis .
6.1326 +  qed (insert x, simp)
6.1327 +qed auto
6.1328 +
6.1329 +lemma LIMSEQ_const_iff:
6.1330 +  fixes k l :: "'a::t2_space"
6.1331 +  shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
6.1332 +  using trivial_limit_sequentially by (rule tendsto_const_iff)
6.1333 +
6.1334 +lemma LIMSEQ_SUP:
6.1335 +  "incseq X \<Longrightarrow> X ----> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})"
6.1336 +  by (intro increasing_tendsto)
6.1337 +     (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
6.1338 +
6.1339 +lemma LIMSEQ_INF:
6.1340 +  "decseq X \<Longrightarrow> X ----> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})"
6.1341 +  by (intro decreasing_tendsto)
6.1342 +     (auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans)
6.1343 +
6.1344 +lemma LIMSEQ_ignore_initial_segment:
6.1345 +  "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
6.1346 +apply (rule topological_tendstoI)
6.1347 +apply (drule (2) topological_tendstoD)
6.1348 +apply (simp only: eventually_sequentially)
6.1349 +apply (erule exE, rename_tac N)
6.1350 +apply (rule_tac x=N in exI)
6.1351 +apply simp
6.1352 +done
6.1353 +
6.1354 +lemma LIMSEQ_offset:
6.1355 +  "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
6.1356 +apply (rule topological_tendstoI)
6.1357 +apply (drule (2) topological_tendstoD)
6.1358 +apply (simp only: eventually_sequentially)
6.1359 +apply (erule exE, rename_tac N)
6.1360 +apply (rule_tac x="N + k" in exI)
6.1361 +apply clarify
6.1362 +apply (drule_tac x="n - k" in spec)
6.1364 +done
6.1365 +
6.1366 +lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
6.1367 +by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
6.1368 +
6.1369 +lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
6.1370 +by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
6.1371 +
6.1372 +lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
6.1373 +by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
6.1374 +
6.1375 +lemma LIMSEQ_unique:
6.1376 +  fixes a b :: "'a::t2_space"
6.1377 +  shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
6.1378 +  using trivial_limit_sequentially by (rule tendsto_unique)
6.1379 +
6.1380 +lemma LIMSEQ_le_const:
6.1381 +  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
6.1382 +  using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
6.1383 +
6.1384 +lemma LIMSEQ_le:
6.1385 +  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
6.1386 +  using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
6.1387 +
6.1388 +lemma LIMSEQ_le_const2:
6.1389 +  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
6.1390 +  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
6.1391 +
6.1392 +lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
6.1394 +
6.1395 +lemma convergentI: "(X ----> L) ==> convergent X"
6.1396 +by (auto simp add: convergent_def)
6.1397 +
6.1398 +lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
6.1399 +by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
6.1400 +
6.1401 +lemma convergent_const: "convergent (\<lambda>n. c)"
6.1402 +  by (rule convergentI, rule tendsto_const)
6.1403 +
6.1404 +lemma monoseq_le:
6.1405 +  "monoseq a \<Longrightarrow> a ----> (x::'a::linorder_topology) \<Longrightarrow>
6.1406 +    ((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
6.1407 +  by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
6.1408 +
6.1409 +lemma LIMSEQ_subseq_LIMSEQ:
6.1410 +  "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
6.1411 +  unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq])
6.1412 +
6.1413 +lemma convergent_subseq_convergent:
6.1414 +  "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
6.1415 +  unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
6.1416 +
6.1417 +lemma limI: "X ----> L ==> lim X = L"
6.1419 +apply (blast intro: LIMSEQ_unique)
6.1420 +done
6.1421 +
6.1422 +lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
6.1423 +  using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
6.1424 +
6.1425 +subsubsection{*Increasing and Decreasing Series*}
6.1426 +
6.1427 +lemma incseq_le: "incseq X \<Longrightarrow> X ----> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)"
6.1428 +  by (metis incseq_def LIMSEQ_le_const)
6.1429 +
6.1430 +lemma decseq_le: "decseq X \<Longrightarrow> X ----> L \<Longrightarrow> (L::'a::linorder_topology) \<le> X n"
6.1431 +  by (metis decseq_def LIMSEQ_le_const2)
6.1432 +
6.1433 +subsection {* Function limit at a point *}
6.1434 +
6.1435 +abbreviation
6.1436 +  LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
6.1437 +        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
6.1438 +  "f -- a --> L \<equiv> (f ---> L) (at a)"
6.1439 +
6.1440 +lemma LIM_const_not_eq[tendsto_intros]:
6.1441 +  fixes a :: "'a::perfect_space"
6.1442 +  fixes k L :: "'b::t2_space"
6.1443 +  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
6.1444 +  by (simp add: tendsto_const_iff)
6.1445 +
6.1446 +lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
6.1447 +
6.1448 +lemma LIM_const_eq:
6.1449 +  fixes a :: "'a::perfect_space"
6.1450 +  fixes k L :: "'b::t2_space"
6.1451 +  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
6.1452 +  by (simp add: tendsto_const_iff)
6.1453 +
6.1454 +lemma LIM_unique:
6.1455 +  fixes a :: "'a::perfect_space" and L M :: "'b::t2_space"
6.1456 +  shows "f -- a --> L \<Longrightarrow> f -- a --> M \<Longrightarrow> L = M"
6.1457 +  using at_neq_bot by (rule tendsto_unique)
6.1458 +
6.1459 +text {* Limits are equal for functions equal except at limit point *}
6.1460 +
6.1461 +lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- a --> l)"
6.1462 +  unfolding tendsto_def eventually_at_topological by simp
6.1463 +
6.1464 +lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- b --> m)"
6.1465 +  by (simp add: LIM_equal)
6.1466 +
6.1467 +lemma LIM_cong_limit: "f -- x --> L \<Longrightarrow> K = L \<Longrightarrow> f -- x --> K"
6.1468 +  by simp
6.1469 +
6.1470 +lemma tendsto_at_iff_tendsto_nhds:
6.1471 +  "g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
6.1472 +  unfolding tendsto_def at_def eventually_within
6.1473 +  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
6.1474 +
6.1475 +lemma tendsto_compose:
6.1476 +  "g -- l --> g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
6.1477 +  unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
6.1478 +
6.1479 +lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
6.1480 +  unfolding o_def by (rule tendsto_compose)
6.1481 +
6.1482 +lemma tendsto_compose_eventually:
6.1483 +  "g -- l --> m \<Longrightarrow> (f ---> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> m) F"
6.1484 +  by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
6.1485 +
6.1486 +lemma LIM_compose_eventually:
6.1487 +  assumes f: "f -- a --> b"
6.1488 +  assumes g: "g -- b --> c"
6.1489 +  assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
6.1490 +  shows "(\<lambda>x. g (f x)) -- a --> c"
6.1491 +  using g f inj by (rule tendsto_compose_eventually)
6.1492 +
6.1493 +subsection {* Continuity *}
6.1494 +
6.1495 +definition isCont :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
6.1496 +  "isCont f a \<longleftrightarrow> f -- a --> f a"
6.1497 +
6.1498 +lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
6.1499 +  unfolding isCont_def by (rule tendsto_ident_at)
6.1500 +
6.1501 +lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
6.1502 +  unfolding isCont_def by (rule tendsto_const)
6.1503 +
6.1504 +lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
6.1505 +  unfolding isCont_def by (rule tendsto_compose)
6.1506 +
6.1507 +lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
6.1508 +  unfolding isCont_def by (rule tendsto_compose)
6.1509 +
6.1510 +lemma isCont_o: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g o f) a"
6.1511 +  unfolding o_def by (rule isCont_o2)
6.1512 +
6.1513 +end
6.1514 +
```