src/HOL/Limits.thy
changeset 51471 cad22a3cc09c
parent 51360 c4367ed99b5e
child 51472 adb441e4b9e9
     1.1 --- a/src/HOL/Limits.thy	Thu Mar 21 16:58:14 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Fri Mar 22 10:41:42 2013 +0100
     1.3 @@ -8,457 +8,9 @@
     1.4  imports RealVector
     1.5  begin
     1.6  
     1.7 -subsection {* Filters *}
     1.8 -
     1.9 -text {*
    1.10 -  This definition also allows non-proper filters.
    1.11 -*}
    1.12 -
    1.13 -locale is_filter =
    1.14 -  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.15 -  assumes True: "F (\<lambda>x. True)"
    1.16 -  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
    1.17 -  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
    1.18 -
    1.19 -typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
    1.20 -proof
    1.21 -  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
    1.22 -qed
    1.23 -
    1.24 -lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
    1.25 -  using Rep_filter [of F] by simp
    1.26 -
    1.27 -lemma Abs_filter_inverse':
    1.28 -  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
    1.29 -  using assms by (simp add: Abs_filter_inverse)
    1.30 -
    1.31 -
    1.32 -subsection {* Eventually *}
    1.33 -
    1.34 -definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.35 -  where "eventually P F \<longleftrightarrow> Rep_filter F P"
    1.36 -
    1.37 -lemma eventually_Abs_filter:
    1.38 -  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
    1.39 -  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
    1.40 -
    1.41 -lemma filter_eq_iff:
    1.42 -  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
    1.43 -  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
    1.44 -
    1.45 -lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
    1.46 -  unfolding eventually_def
    1.47 -  by (rule is_filter.True [OF is_filter_Rep_filter])
    1.48 -
    1.49 -lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
    1.50 -proof -
    1.51 -  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
    1.52 -  thus "eventually P F" by simp
    1.53 -qed
    1.54 -
    1.55 -lemma eventually_mono:
    1.56 -  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
    1.57 -  unfolding eventually_def
    1.58 -  by (rule is_filter.mono [OF is_filter_Rep_filter])
    1.59 -
    1.60 -lemma eventually_conj:
    1.61 -  assumes P: "eventually (\<lambda>x. P x) F"
    1.62 -  assumes Q: "eventually (\<lambda>x. Q x) F"
    1.63 -  shows "eventually (\<lambda>x. P x \<and> Q x) F"
    1.64 -  using assms unfolding eventually_def
    1.65 -  by (rule is_filter.conj [OF is_filter_Rep_filter])
    1.66 -
    1.67 -lemma eventually_Ball_finite:
    1.68 -  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
    1.69 -  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
    1.70 -using assms by (induct set: finite, simp, simp add: eventually_conj)
    1.71 -
    1.72 -lemma eventually_all_finite:
    1.73 -  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
    1.74 -  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
    1.75 -  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
    1.76 -using eventually_Ball_finite [of UNIV P] assms by simp
    1.77 -
    1.78 -lemma eventually_mp:
    1.79 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.80 -  assumes "eventually (\<lambda>x. P x) F"
    1.81 -  shows "eventually (\<lambda>x. Q x) F"
    1.82 -proof (rule eventually_mono)
    1.83 -  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
    1.84 -  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
    1.85 -    using assms by (rule eventually_conj)
    1.86 -qed
    1.87 -
    1.88 -lemma eventually_rev_mp:
    1.89 -  assumes "eventually (\<lambda>x. P x) F"
    1.90 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.91 -  shows "eventually (\<lambda>x. Q x) F"
    1.92 -using assms(2) assms(1) by (rule eventually_mp)
    1.93 -
    1.94 -lemma eventually_conj_iff:
    1.95 -  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
    1.96 -  by (auto intro: eventually_conj elim: eventually_rev_mp)
    1.97 -
    1.98 -lemma eventually_elim1:
    1.99 -  assumes "eventually (\<lambda>i. P i) F"
   1.100 -  assumes "\<And>i. P i \<Longrightarrow> Q i"
   1.101 -  shows "eventually (\<lambda>i. Q i) F"
   1.102 -  using assms by (auto elim!: eventually_rev_mp)
   1.103 -
   1.104 -lemma eventually_elim2:
   1.105 -  assumes "eventually (\<lambda>i. P i) F"
   1.106 -  assumes "eventually (\<lambda>i. Q i) F"
   1.107 -  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
   1.108 -  shows "eventually (\<lambda>i. R i) F"
   1.109 -  using assms by (auto elim!: eventually_rev_mp)
   1.110 -
   1.111 -lemma eventually_subst:
   1.112 -  assumes "eventually (\<lambda>n. P n = Q n) F"
   1.113 -  shows "eventually P F = eventually Q F" (is "?L = ?R")
   1.114 -proof -
   1.115 -  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   1.116 -      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
   1.117 -    by (auto elim: eventually_elim1)
   1.118 -  then show ?thesis by (auto elim: eventually_elim2)
   1.119 -qed
   1.120 -
   1.121 -ML {*
   1.122 -  fun eventually_elim_tac ctxt thms thm =
   1.123 -    let
   1.124 -      val thy = Proof_Context.theory_of ctxt
   1.125 -      val mp_thms = thms RL [@{thm eventually_rev_mp}]
   1.126 -      val raw_elim_thm =
   1.127 -        (@{thm allI} RS @{thm always_eventually})
   1.128 -        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
   1.129 -        |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
   1.130 -      val cases_prop = prop_of (raw_elim_thm RS thm)
   1.131 -      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
   1.132 -    in
   1.133 -      CASES cases (rtac raw_elim_thm 1) thm
   1.134 -    end
   1.135 -*}
   1.136 -
   1.137 -method_setup eventually_elim = {*
   1.138 -  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
   1.139 -*} "elimination of eventually quantifiers"
   1.140 -
   1.141 -
   1.142 -subsection {* Finer-than relation *}
   1.143 -
   1.144 -text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
   1.145 -filter @{term F'}. *}
   1.146 -
   1.147 -instantiation filter :: (type) complete_lattice
   1.148 -begin
   1.149 -
   1.150 -definition le_filter_def:
   1.151 -  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
   1.152 -
   1.153 -definition
   1.154 -  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   1.155 -
   1.156 -definition
   1.157 -  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
   1.158 -
   1.159 -definition
   1.160 -  "bot = Abs_filter (\<lambda>P. True)"
   1.161 -
   1.162 -definition
   1.163 -  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
   1.164 -
   1.165 -definition
   1.166 -  "inf F F' = Abs_filter
   1.167 -      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.168 -
   1.169 -definition
   1.170 -  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
   1.171 -
   1.172 -definition
   1.173 -  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
   1.174 -
   1.175 -lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
   1.176 -  unfolding top_filter_def
   1.177 -  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
   1.178 -
   1.179 -lemma eventually_bot [simp]: "eventually P bot"
   1.180 -  unfolding bot_filter_def
   1.181 -  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
   1.182 -
   1.183 -lemma eventually_sup:
   1.184 -  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
   1.185 -  unfolding sup_filter_def
   1.186 -  by (rule eventually_Abs_filter, rule is_filter.intro)
   1.187 -     (auto elim!: eventually_rev_mp)
   1.188 -
   1.189 -lemma eventually_inf:
   1.190 -  "eventually P (inf F F') \<longleftrightarrow>
   1.191 -   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.192 -  unfolding inf_filter_def
   1.193 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.194 -  apply (fast intro: eventually_True)
   1.195 -  apply clarify
   1.196 -  apply (intro exI conjI)
   1.197 -  apply (erule (1) eventually_conj)
   1.198 -  apply (erule (1) eventually_conj)
   1.199 -  apply simp
   1.200 -  apply auto
   1.201 -  done
   1.202 -
   1.203 -lemma eventually_Sup:
   1.204 -  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
   1.205 -  unfolding Sup_filter_def
   1.206 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.207 -  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
   1.208 -  done
   1.209 -
   1.210 -instance proof
   1.211 -  fix F F' F'' :: "'a filter" and S :: "'a filter set"
   1.212 -  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   1.213 -    by (rule less_filter_def) }
   1.214 -  { show "F \<le> F"
   1.215 -    unfolding le_filter_def by simp }
   1.216 -  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
   1.217 -    unfolding le_filter_def by simp }
   1.218 -  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
   1.219 -    unfolding le_filter_def filter_eq_iff by fast }
   1.220 -  { show "F \<le> top"
   1.221 -    unfolding le_filter_def eventually_top by (simp add: always_eventually) }
   1.222 -  { show "bot \<le> F"
   1.223 -    unfolding le_filter_def by simp }
   1.224 -  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
   1.225 -    unfolding le_filter_def eventually_sup by simp_all }
   1.226 -  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
   1.227 -    unfolding le_filter_def eventually_sup by simp }
   1.228 -  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
   1.229 -    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
   1.230 -  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
   1.231 -    unfolding le_filter_def eventually_inf
   1.232 -    by (auto elim!: eventually_mono intro: eventually_conj) }
   1.233 -  { assume "F \<in> S" thus "F \<le> Sup S"
   1.234 -    unfolding le_filter_def eventually_Sup by simp }
   1.235 -  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
   1.236 -    unfolding le_filter_def eventually_Sup by simp }
   1.237 -  { assume "F'' \<in> S" thus "Inf S \<le> F''"
   1.238 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   1.239 -  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
   1.240 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   1.241 -qed
   1.242 -
   1.243 -end
   1.244 -
   1.245 -lemma filter_leD:
   1.246 -  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
   1.247 -  unfolding le_filter_def by simp
   1.248 -
   1.249 -lemma filter_leI:
   1.250 -  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
   1.251 -  unfolding le_filter_def by simp
   1.252 -
   1.253 -lemma eventually_False:
   1.254 -  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   1.255 -  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
   1.256 -
   1.257 -abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   1.258 -  where "trivial_limit F \<equiv> F = bot"
   1.259 -
   1.260 -lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   1.261 -  by (rule eventually_False [symmetric])
   1.262 -
   1.263 -lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
   1.264 -  by (cases P) (simp_all add: eventually_False)
   1.265 -
   1.266 -
   1.267 -subsection {* Map function for filters *}
   1.268 -
   1.269 -definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
   1.270 -  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
   1.271 -
   1.272 -lemma eventually_filtermap:
   1.273 -  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
   1.274 -  unfolding filtermap_def
   1.275 -  apply (rule eventually_Abs_filter)
   1.276 -  apply (rule is_filter.intro)
   1.277 -  apply (auto elim!: eventually_rev_mp)
   1.278 -  done
   1.279 -
   1.280 -lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
   1.281 -  by (simp add: filter_eq_iff eventually_filtermap)
   1.282 -
   1.283 -lemma filtermap_filtermap:
   1.284 -  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
   1.285 -  by (simp add: filter_eq_iff eventually_filtermap)
   1.286 -
   1.287 -lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
   1.288 -  unfolding le_filter_def eventually_filtermap by simp
   1.289 -
   1.290 -lemma filtermap_bot [simp]: "filtermap f bot = bot"
   1.291 -  by (simp add: filter_eq_iff eventually_filtermap)
   1.292 -
   1.293 -lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
   1.294 -  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
   1.295 -
   1.296 -subsection {* Order filters *}
   1.297 -
   1.298 -definition at_top :: "('a::order) filter"
   1.299 -  where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
   1.300 -
   1.301 -lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
   1.302 -  unfolding at_top_def
   1.303 -proof (rule eventually_Abs_filter, rule is_filter.intro)
   1.304 -  fix P Q :: "'a \<Rightarrow> bool"
   1.305 -  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
   1.306 -  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
   1.307 -  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
   1.308 -  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
   1.309 -qed auto
   1.310 -
   1.311 -lemma eventually_ge_at_top:
   1.312 -  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   1.313 -  unfolding eventually_at_top_linorder by auto
   1.314 -
   1.315 -lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
   1.316 -  unfolding eventually_at_top_linorder
   1.317 -proof safe
   1.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])
   1.319 -next
   1.320 -  fix N assume "\<forall>n>N. P n"
   1.321 -  moreover from gt_ex[of N] guess y ..
   1.322 -  ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
   1.323 -qed
   1.324 -
   1.325 -lemma eventually_gt_at_top:
   1.326 -  "eventually (\<lambda>x. (c::_::dense_linorder) < x) at_top"
   1.327 -  unfolding eventually_at_top_dense by auto
   1.328 -
   1.329 -definition at_bot :: "('a::order) filter"
   1.330 -  where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"
   1.331 -
   1.332 -lemma eventually_at_bot_linorder:
   1.333 -  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
   1.334 -  unfolding at_bot_def
   1.335 -proof (rule eventually_Abs_filter, rule is_filter.intro)
   1.336 -  fix P Q :: "'a \<Rightarrow> bool"
   1.337 -  assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n"
   1.338 -  then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto
   1.339 -  then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp
   1.340 -  then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..
   1.341 -qed auto
   1.342 -
   1.343 -lemma eventually_le_at_bot:
   1.344 -  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   1.345 -  unfolding eventually_at_bot_linorder by auto
   1.346 -
   1.347 -lemma eventually_at_bot_dense:
   1.348 -  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
   1.349 -  unfolding eventually_at_bot_linorder
   1.350 -proof safe
   1.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])
   1.352 -next
   1.353 -  fix N assume "\<forall>n<N. P n" 
   1.354 -  moreover from lt_ex[of N] guess y ..
   1.355 -  ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
   1.356 -qed
   1.357 -
   1.358 -lemma eventually_gt_at_bot:
   1.359 -  "eventually (\<lambda>x. x < (c::_::dense_linorder)) at_bot"
   1.360 -  unfolding eventually_at_bot_dense by auto
   1.361 -
   1.362 -subsection {* Sequentially *}
   1.363 -
   1.364 -abbreviation sequentially :: "nat filter"
   1.365 -  where "sequentially == at_top"
   1.366 -
   1.367 -lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
   1.368 -  unfolding at_top_def by simp
   1.369 -
   1.370 -lemma eventually_sequentially:
   1.371 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   1.372 -  by (rule eventually_at_top_linorder)
   1.373 -
   1.374 -lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   1.375 -  unfolding filter_eq_iff eventually_sequentially by auto
   1.376 -
   1.377 -lemmas trivial_limit_sequentially = sequentially_bot
   1.378 -
   1.379 -lemma eventually_False_sequentially [simp]:
   1.380 -  "\<not> eventually (\<lambda>n. False) sequentially"
   1.381 -  by (simp add: eventually_False)
   1.382 -
   1.383 -lemma le_sequentially:
   1.384 -  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   1.385 -  unfolding le_filter_def eventually_sequentially
   1.386 -  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
   1.387 -
   1.388 -lemma eventually_sequentiallyI:
   1.389 -  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   1.390 -  shows "eventually P sequentially"
   1.391 -using assms by (auto simp: eventually_sequentially)
   1.392 -
   1.393 -
   1.394 -subsection {* Standard filters *}
   1.395 -
   1.396 -definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
   1.397 -  where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
   1.398 -
   1.399 -definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
   1.400 -  where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   1.401 -
   1.402 -definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
   1.403 -  where "at a = nhds a within - {a}"
   1.404 -
   1.405 -abbreviation at_right :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
   1.406 -  "at_right x \<equiv> at x within {x <..}"
   1.407 -
   1.408 -abbreviation at_left :: "'a\<Colon>{topological_space, order} \<Rightarrow> 'a filter" where
   1.409 -  "at_left x \<equiv> at x within {..< x}"
   1.410 -
   1.411  definition at_infinity :: "'a::real_normed_vector filter" where
   1.412    "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
   1.413  
   1.414 -lemma eventually_within:
   1.415 -  "eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F"
   1.416 -  unfolding within_def
   1.417 -  by (rule eventually_Abs_filter, rule is_filter.intro)
   1.418 -     (auto elim!: eventually_rev_mp)
   1.419 -
   1.420 -lemma within_UNIV [simp]: "F within UNIV = F"
   1.421 -  unfolding filter_eq_iff eventually_within by simp
   1.422 -
   1.423 -lemma within_empty [simp]: "F within {} = bot"
   1.424 -  unfolding filter_eq_iff eventually_within by simp
   1.425 -
   1.426 -lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
   1.427 -  by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
   1.428 -
   1.429 -lemma at_within_eq: "at x within T = nhds x within (T - {x})"
   1.430 -  unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
   1.431 -
   1.432 -lemma within_le: "F within S \<le> F"
   1.433 -  unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
   1.434 -
   1.435 -lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
   1.436 -  unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
   1.437 -
   1.438 -lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
   1.439 -  by (blast intro: within_le le_withinI order_trans)
   1.440 -
   1.441 -lemma eventually_nhds:
   1.442 -  "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   1.443 -unfolding nhds_def
   1.444 -proof (rule eventually_Abs_filter, rule is_filter.intro)
   1.445 -  have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
   1.446 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" ..
   1.447 -next
   1.448 -  fix P Q
   1.449 -  assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
   1.450 -     and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)"
   1.451 -  then obtain S T where
   1.452 -    "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
   1.453 -    "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto
   1.454 -  hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"
   1.455 -    by (simp add: open_Int)
   1.456 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" ..
   1.457 -qed auto
   1.458  
   1.459  lemma eventually_nhds_metric:
   1.460    "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
   1.461 @@ -472,18 +24,10 @@
   1.462  apply (erule le_less_trans [OF dist_triangle])
   1.463  done
   1.464  
   1.465 -lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   1.466 -  unfolding trivial_limit_def eventually_nhds by simp
   1.467 -
   1.468 -lemma eventually_at_topological:
   1.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))"
   1.470 -unfolding at_def eventually_within eventually_nhds by simp
   1.471 -
   1.472  lemma eventually_at:
   1.473    fixes a :: "'a::metric_space"
   1.474    shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
   1.475  unfolding at_def eventually_within eventually_nhds_metric by auto
   1.476 -
   1.477  lemma eventually_within_less: (* COPY FROM Topo/eventually_within *)
   1.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)"
   1.479    unfolding eventually_within eventually_at dist_nz by auto
   1.480 @@ -492,29 +36,6 @@
   1.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)"
   1.482    unfolding eventually_within_less by auto (metis dense order_le_less_trans)
   1.483  
   1.484 -lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   1.485 -  unfolding trivial_limit_def eventually_at_topological
   1.486 -  by (safe, case_tac "S = {a}", simp, fast, fast)
   1.487 -
   1.488 -lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
   1.489 -  by (simp add: at_eq_bot_iff not_open_singleton)
   1.490 -
   1.491 -lemma trivial_limit_at_left_real [simp]: (* maybe generalize type *)
   1.492 -  "\<not> trivial_limit (at_left (x::real))"
   1.493 -  unfolding trivial_limit_def eventually_within_le
   1.494 -  apply clarsimp
   1.495 -  apply (rule_tac x="x - d/2" in bexI)
   1.496 -  apply (auto simp: dist_real_def)
   1.497 -  done
   1.498 -
   1.499 -lemma trivial_limit_at_right_real [simp]: (* maybe generalize type *)
   1.500 -  "\<not> trivial_limit (at_right (x::real))"
   1.501 -  unfolding trivial_limit_def eventually_within_le
   1.502 -  apply clarsimp
   1.503 -  apply (rule_tac x="x + d/2" in bexI)
   1.504 -  apply (auto simp: dist_real_def)
   1.505 -  done
   1.506 -
   1.507  lemma eventually_at_infinity:
   1.508    "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
   1.509  unfolding at_infinity_def
   1.510 @@ -722,214 +243,9 @@
   1.511  lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
   1.512  lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
   1.513  
   1.514 -
   1.515 -subsection {* Limits *}
   1.516 -
   1.517 -definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
   1.518 -  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
   1.519 -
   1.520 -syntax
   1.521 -  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
   1.522 -
   1.523 -translations
   1.524 -  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
   1.525 -
   1.526 -lemma filterlim_iff:
   1.527 -  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
   1.528 -  unfolding filterlim_def le_filter_def eventually_filtermap ..
   1.529 -
   1.530 -lemma filterlim_compose:
   1.531 -  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
   1.532 -  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
   1.533 -
   1.534 -lemma filterlim_mono:
   1.535 -  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
   1.536 -  unfolding filterlim_def by (metis filtermap_mono order_trans)
   1.537 -
   1.538 -lemma filterlim_ident: "LIM x F. x :> F"
   1.539 -  by (simp add: filterlim_def filtermap_ident)
   1.540 -
   1.541 -lemma filterlim_cong:
   1.542 -  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
   1.543 -  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
   1.544 -
   1.545 -lemma filterlim_within:
   1.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))"
   1.547 -  unfolding filterlim_def
   1.548 -proof safe
   1.549 -  assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1"
   1.550 -    by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
   1.551 -qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
   1.552 -
   1.553 -lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   1.554 -  unfolding filterlim_def filtermap_filtermap ..
   1.555 -
   1.556 -lemma filterlim_sup:
   1.557 -  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
   1.558 -  unfolding filterlim_def filtermap_sup by auto
   1.559 -
   1.560 -lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
   1.561 -  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
   1.562 -
   1.563 -abbreviation (in topological_space)
   1.564 -  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   1.565 -  "(f ---> l) F \<equiv> filterlim f (nhds l) F"
   1.566 -
   1.567 -lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
   1.568 -  by simp
   1.569 -
   1.570 -ML {*
   1.571 -
   1.572 -structure Tendsto_Intros = Named_Thms
   1.573 -(
   1.574 -  val name = @{binding tendsto_intros}
   1.575 -  val description = "introduction rules for tendsto"
   1.576 -)
   1.577 -
   1.578 -*}
   1.579 -
   1.580 -setup {*
   1.581 -  Tendsto_Intros.setup #>
   1.582 -  Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
   1.583 -    map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
   1.584 -*}
   1.585 -
   1.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)"
   1.587 -  unfolding filterlim_def
   1.588 -proof safe
   1.589 -  fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
   1.590 -  then show "eventually (\<lambda>x. f x \<in> S) F"
   1.591 -    unfolding eventually_nhds eventually_filtermap le_filter_def
   1.592 -    by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
   1.593 -qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
   1.594 -
   1.595 -lemma filterlim_at:
   1.596 -  "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
   1.597 -  by (simp add: at_def filterlim_within)
   1.598 -
   1.599 -lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   1.600 -  unfolding tendsto_def le_filter_def by fast
   1.601 -
   1.602 -lemma topological_tendstoI:
   1.603 -  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F)
   1.604 -    \<Longrightarrow> (f ---> l) F"
   1.605 -  unfolding tendsto_def by auto
   1.606 -
   1.607 -lemma topological_tendstoD:
   1.608 -  "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
   1.609 -  unfolding tendsto_def by auto
   1.610 -
   1.611 -lemma tendstoI:
   1.612 -  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
   1.613 -  shows "(f ---> l) F"
   1.614 -  apply (rule topological_tendstoI)
   1.615 -  apply (simp add: open_dist)
   1.616 -  apply (drule (1) bspec, clarify)
   1.617 -  apply (drule assms)
   1.618 -  apply (erule eventually_elim1, simp)
   1.619 -  done
   1.620 -
   1.621 -lemma tendstoD:
   1.622 -  "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
   1.623 -  apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
   1.624 -  apply (clarsimp simp add: open_dist)
   1.625 -  apply (rule_tac x="e - dist x l" in exI, clarsimp)
   1.626 -  apply (simp only: less_diff_eq)
   1.627 -  apply (erule le_less_trans [OF dist_triangle])
   1.628 -  apply simp
   1.629 -  apply simp
   1.630 -  done
   1.631 -
   1.632 -lemma tendsto_iff:
   1.633 -  "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
   1.634 -  using tendstoI tendstoD by fast
   1.635 -
   1.636 -lemma order_tendstoI:
   1.637 -  fixes y :: "_ :: order_topology"
   1.638 -  assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
   1.639 -  assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
   1.640 -  shows "(f ---> y) F"
   1.641 -proof (rule topological_tendstoI)
   1.642 -  fix S assume "open S" "y \<in> S"
   1.643 -  then show "eventually (\<lambda>x. f x \<in> S) F"
   1.644 -    unfolding open_generated_order
   1.645 -  proof induct
   1.646 -    case (UN K)
   1.647 -    then obtain k where "y \<in> k" "k \<in> K" by auto
   1.648 -    with UN(2)[of k] show ?case
   1.649 -      by (auto elim: eventually_elim1)
   1.650 -  qed (insert assms, auto elim: eventually_elim2)
   1.651 -qed
   1.652 -
   1.653 -lemma order_tendstoD:
   1.654 -  fixes y :: "_ :: order_topology"
   1.655 -  assumes y: "(f ---> y) F"
   1.656 -  shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
   1.657 -    and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
   1.658 -  using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto
   1.659 -
   1.660 -lemma order_tendsto_iff: 
   1.661 -  fixes f :: "_ \<Rightarrow> 'a :: order_topology"
   1.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)"
   1.663 -  by (metis order_tendstoI order_tendstoD)
   1.664 -
   1.665  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
   1.666    by (simp only: tendsto_iff Zfun_def dist_norm)
   1.667  
   1.668 -lemma tendsto_bot [simp]: "(f ---> a) bot"
   1.669 -  unfolding tendsto_def by simp
   1.670 -
   1.671 -lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
   1.672 -  unfolding tendsto_def eventually_at_topological by auto
   1.673 -
   1.674 -lemma tendsto_ident_at_within [tendsto_intros]:
   1.675 -  "((\<lambda>x. x) ---> a) (at a within S)"
   1.676 -  unfolding tendsto_def eventually_within eventually_at_topological by auto
   1.677 -
   1.678 -lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
   1.679 -  by (simp add: tendsto_def)
   1.680 -
   1.681 -lemma tendsto_unique:
   1.682 -  fixes f :: "'a \<Rightarrow> 'b::t2_space"
   1.683 -  assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"
   1.684 -  shows "a = b"
   1.685 -proof (rule ccontr)
   1.686 -  assume "a \<noteq> b"
   1.687 -  obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
   1.688 -    using hausdorff [OF `a \<noteq> b`] by fast
   1.689 -  have "eventually (\<lambda>x. f x \<in> U) F"
   1.690 -    using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD)
   1.691 -  moreover
   1.692 -  have "eventually (\<lambda>x. f x \<in> V) F"
   1.693 -    using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)
   1.694 -  ultimately
   1.695 -  have "eventually (\<lambda>x. False) F"
   1.696 -  proof eventually_elim
   1.697 -    case (elim x)
   1.698 -    hence "f x \<in> U \<inter> V" by simp
   1.699 -    with `U \<inter> V = {}` show ?case by simp
   1.700 -  qed
   1.701 -  with `\<not> trivial_limit F` show "False"
   1.702 -    by (simp add: trivial_limit_def)
   1.703 -qed
   1.704 -
   1.705 -lemma tendsto_const_iff:
   1.706 -  fixes a b :: "'a::t2_space"
   1.707 -  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a) ---> b) F \<longleftrightarrow> a = b"
   1.708 -  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
   1.709 -
   1.710 -lemma tendsto_at_iff_tendsto_nhds:
   1.711 -  "(g ---> g l) (at l) \<longleftrightarrow> (g ---> g l) (nhds l)"
   1.712 -  unfolding tendsto_def at_def eventually_within
   1.713 -  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
   1.714 -
   1.715 -lemma tendsto_compose:
   1.716 -  "(g ---> g l) (at l) \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
   1.717 -  unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
   1.718 -
   1.719 -lemma tendsto_compose_eventually:
   1.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"
   1.721 -  by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
   1.722  
   1.723  lemma metric_tendsto_imp_tendsto:
   1.724    assumes f: "(f ---> a) F"
   1.725 @@ -941,21 +257,6 @@
   1.726    with le show "eventually (\<lambda>x. dist (g x) b < e) F"
   1.727      using le_less_trans by (rule eventually_elim2)
   1.728  qed
   1.729 -
   1.730 -lemma increasing_tendsto:
   1.731 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   1.732 -  assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
   1.733 -      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   1.734 -  shows "(f ---> l) F"
   1.735 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
   1.736 -
   1.737 -lemma decreasing_tendsto:
   1.738 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   1.739 -  assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
   1.740 -      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
   1.741 -  shows "(f ---> l) F"
   1.742 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
   1.743 -
   1.744  subsubsection {* Distance and norms *}
   1.745  
   1.746  lemma tendsto_dist [tendsto_intros]:
   1.747 @@ -1057,19 +358,6 @@
   1.748      by (simp add: tendsto_const)
   1.749  qed
   1.750  
   1.751 -lemma tendsto_sandwich:
   1.752 -  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
   1.753 -  assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
   1.754 -  assumes lim: "(f ---> c) net" "(h ---> c) net"
   1.755 -  shows "(g ---> c) net"
   1.756 -proof (rule order_tendstoI)
   1.757 -  fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
   1.758 -    using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
   1.759 -next
   1.760 -  fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
   1.761 -    using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
   1.762 -qed
   1.763 -
   1.764  lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
   1.765  
   1.766  subsubsection {* Linear operators and multiplication *}
   1.767 @@ -1136,31 +424,6 @@
   1.768      by (simp add: tendsto_const)
   1.769  qed
   1.770  
   1.771 -lemma tendsto_le:
   1.772 -  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
   1.773 -  assumes F: "\<not> trivial_limit F"
   1.774 -  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
   1.775 -  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
   1.776 -  shows "y \<le> x"
   1.777 -proof (rule ccontr)
   1.778 -  assume "\<not> y \<le> x"
   1.779 -  with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
   1.780 -    by (auto simp: not_le)
   1.781 -  then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
   1.782 -    using x y by (auto intro: order_tendstoD)
   1.783 -  with ev have "eventually (\<lambda>x. False) F"
   1.784 -    by eventually_elim (insert xy, fastforce)
   1.785 -  with F show False
   1.786 -    by (simp add: eventually_False)
   1.787 -qed
   1.788 -
   1.789 -lemma tendsto_le_const:
   1.790 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   1.791 -  assumes F: "\<not> trivial_limit F"
   1.792 -  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
   1.793 -  shows "a \<le> x"
   1.794 -  using F x tendsto_const a by (rule tendsto_le)
   1.795 -
   1.796  subsubsection {* Inverse and division *}
   1.797  
   1.798  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   1.799 @@ -1281,75 +544,6 @@
   1.800    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
   1.801    unfolding sgn_div_norm by (simp add: tendsto_intros)
   1.802  
   1.803 -subsection {* Limits to @{const at_top} and @{const at_bot} *}
   1.804 -
   1.805 -lemma filterlim_at_top:
   1.806 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.807 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
   1.808 -  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
   1.809 -
   1.810 -lemma filterlim_at_top_dense:
   1.811 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
   1.812 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
   1.813 -  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
   1.814 -            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
   1.815 -
   1.816 -lemma filterlim_at_top_ge:
   1.817 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   1.818 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
   1.819 -  unfolding filterlim_at_top
   1.820 -proof safe
   1.821 -  fix Z assume *: "\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F"
   1.822 -  with *[THEN spec, of "max Z c"] show "eventually (\<lambda>x. Z \<le> f x) F"
   1.823 -    by (auto elim!: eventually_elim1)
   1.824 -qed simp
   1.825 -
   1.826 -lemma filterlim_at_top_at_top:
   1.827 -  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
   1.828 -  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   1.829 -  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   1.830 -  assumes Q: "eventually Q at_top"
   1.831 -  assumes P: "eventually P at_top"
   1.832 -  shows "filterlim f at_top at_top"
   1.833 -proof -
   1.834 -  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
   1.835 -    unfolding eventually_at_top_linorder by auto
   1.836 -  show ?thesis
   1.837 -  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
   1.838 -    fix z assume "x \<le> z"
   1.839 -    with x have "P z" by auto
   1.840 -    have "eventually (\<lambda>x. g z \<le> x) at_top"
   1.841 -      by (rule eventually_ge_at_top)
   1.842 -    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
   1.843 -      by eventually_elim (metis mono bij `P z`)
   1.844 -  qed
   1.845 -qed
   1.846 -
   1.847 -lemma filterlim_at_top_gt:
   1.848 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
   1.849 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
   1.850 -  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
   1.851 -
   1.852 -lemma filterlim_at_bot: 
   1.853 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.854 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
   1.855 -  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
   1.856 -
   1.857 -lemma filterlim_at_bot_le:
   1.858 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   1.859 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
   1.860 -  unfolding filterlim_at_bot
   1.861 -proof safe
   1.862 -  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
   1.863 -  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
   1.864 -    by (auto elim!: eventually_elim1)
   1.865 -qed simp
   1.866 -
   1.867 -lemma filterlim_at_bot_lt:
   1.868 -  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)" and c :: "'b"
   1.869 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
   1.870 -  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
   1.871 -
   1.872  lemma filterlim_at_bot_at_right:
   1.873    fixes f :: "real \<Rightarrow> 'b::linorder"
   1.874    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   1.875 @@ -1429,13 +623,7 @@
   1.876  
   1.877  *}
   1.878  
   1.879 -lemma at_eq_sup_left_right: "at (x::real) = sup (at_left x) (at_right x)"
   1.880 -  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
   1.881 -           elim: eventually_elim2 eventually_elim1)
   1.882 -
   1.883 -lemma filterlim_split_at_real:
   1.884 -  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::real))"
   1.885 -  by (subst at_eq_sup_left_right) (rule filterlim_sup)
   1.886 +lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
   1.887  
   1.888  lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
   1.889    unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
   1.890 @@ -1486,14 +674,6 @@
   1.891    "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
   1.892    unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
   1.893  
   1.894 -lemma filterlim_at_split:
   1.895 -  "filterlim f F (at (x::real)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
   1.896 -  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
   1.897 -
   1.898 -lemma eventually_at_split:
   1.899 -  "eventually P (at (x::real)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   1.900 -  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   1.901 -
   1.902  lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
   1.903    unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
   1.904    by (metis le_minus_iff minus_minus)
   1.905 @@ -1765,5 +945,10 @@
   1.906      by (auto simp: norm_power)
   1.907  qed simp
   1.908  
   1.909 +
   1.910 +(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
   1.911 +   Hence it was references as Limits.within, but now it is Basic_Topology.eventually_within *)
   1.912 +lemmas eventually_within = eventually_within
   1.913 +
   1.914  end
   1.915