move topological_space to its own theory
authorhoelzl
Fri Mar 22 10:41:42 2013 +0100 (2013-03-22)
changeset 51471cad22a3cc09c
parent 51470 a981a5c8a505
child 51472 adb441e4b9e9
move topological_space to its own theory
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/RealVector.thy
src/HOL/SEQ.thy
src/HOL/Topological_Spaces.thy
     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.43      simp add: dist_norm le)
    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.73 -by (simp add: LIM_equal)
    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.582 -  Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
   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.748      by (simp add: tendsto_const)
   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.768      by (simp add: tendsto_const)
   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.81 -by (simp add: monoseq_def)
    5.82 -
    5.83 -lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
    5.84 -by (simp add: monoseq_def)
    5.85 -
    5.86 -lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
    5.87 -by (simp add: monoseq_Suc)
    5.88 -
    5.89 -lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
    5.90 -by (simp add: monoseq_Suc)
    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.109 -apply (simp add: subseq_def)
   5.110 -apply (auto dest!: less_imp_Suc_add)
   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.226  by (simp add: LIMSEQ_iff)
   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.262 -apply (simp add: le_diff_conv2)
   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.322 -apply (simp add: lim_def)
   5.323 -apply (blast intro: LIMSEQ_unique)
   5.324 -done
   5.325 -
   5.326 -lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
   5.327 -by (simp add: convergent_def)
   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.338  lemma convergent_add:
   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.845 +  Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
   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.1204 +by (simp add: monoseq_def)
  6.1205 +
  6.1206 +lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
  6.1207 +by (simp add: monoseq_def)
  6.1208 +
  6.1209 +lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
  6.1210 +by (simp add: monoseq_Suc)
  6.1211 +
  6.1212 +lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
  6.1213 +by (simp add: monoseq_Suc)
  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.1232 +apply (simp add: subseq_def)
  6.1233 +apply (auto dest!: less_imp_Suc_add)
  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.1363 +apply (simp add: le_diff_conv2)
  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.1393 +by (simp add: convergent_def)
  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.1418 +apply (simp add: lim_def)
  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 +