src/HOL/Topological_Spaces.thy
changeset 60036 218fcc645d22
parent 59976 046399298519
child 60040 1fa1023b13b9
     1.1 --- a/src/HOL/Topological_Spaces.thy	Sun Apr 12 16:04:53 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:33:19 2015 +0200
     1.3 @@ -322,557 +322,6 @@
     1.4      by auto
     1.5  qed
     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 -subsubsection {* 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 not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   1.112 -  by (auto intro: eventually_mp)
   1.113 -
   1.114 -lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
   1.115 -  by (metis always_eventually)
   1.116 -
   1.117 -lemma eventually_subst:
   1.118 -  assumes "eventually (\<lambda>n. P n = Q n) F"
   1.119 -  shows "eventually P F = eventually Q F" (is "?L = ?R")
   1.120 -proof -
   1.121 -  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   1.122 -      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
   1.123 -    by (auto elim: eventually_elim1)
   1.124 -  then show ?thesis by (auto elim: eventually_elim2)
   1.125 -qed
   1.126 -
   1.127 -ML {*
   1.128 -  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
   1.129 -    let
   1.130 -      val mp_thms = facts RL @{thms eventually_rev_mp}
   1.131 -      val raw_elim_thm =
   1.132 -        (@{thm allI} RS @{thm always_eventually})
   1.133 -        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
   1.134 -        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
   1.135 -      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
   1.136 -      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
   1.137 -    in
   1.138 -      CASES cases (rtac raw_elim_thm i)
   1.139 -    end)
   1.140 -*}
   1.141 -
   1.142 -method_setup eventually_elim = {*
   1.143 -  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
   1.144 -*} "elimination of eventually quantifiers"
   1.145 -
   1.146 -
   1.147 -subsubsection {* Finer-than relation *}
   1.148 -
   1.149 -text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
   1.150 -filter @{term F'}. *}
   1.151 -
   1.152 -instantiation filter :: (type) complete_lattice
   1.153 -begin
   1.154 -
   1.155 -definition le_filter_def:
   1.156 -  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
   1.157 -
   1.158 -definition
   1.159 -  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   1.160 -
   1.161 -definition
   1.162 -  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
   1.163 -
   1.164 -definition
   1.165 -  "bot = Abs_filter (\<lambda>P. True)"
   1.166 -
   1.167 -definition
   1.168 -  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
   1.169 -
   1.170 -definition
   1.171 -  "inf F F' = Abs_filter
   1.172 -      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.173 -
   1.174 -definition
   1.175 -  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
   1.176 -
   1.177 -definition
   1.178 -  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
   1.179 -
   1.180 -lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
   1.181 -  unfolding top_filter_def
   1.182 -  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
   1.183 -
   1.184 -lemma eventually_bot [simp]: "eventually P bot"
   1.185 -  unfolding bot_filter_def
   1.186 -  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
   1.187 -
   1.188 -lemma eventually_sup:
   1.189 -  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
   1.190 -  unfolding sup_filter_def
   1.191 -  by (rule eventually_Abs_filter, rule is_filter.intro)
   1.192 -     (auto elim!: eventually_rev_mp)
   1.193 -
   1.194 -lemma eventually_inf:
   1.195 -  "eventually P (inf F F') \<longleftrightarrow>
   1.196 -   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.197 -  unfolding inf_filter_def
   1.198 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.199 -  apply (fast intro: eventually_True)
   1.200 -  apply clarify
   1.201 -  apply (intro exI conjI)
   1.202 -  apply (erule (1) eventually_conj)
   1.203 -  apply (erule (1) eventually_conj)
   1.204 -  apply simp
   1.205 -  apply auto
   1.206 -  done
   1.207 -
   1.208 -lemma eventually_Sup:
   1.209 -  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
   1.210 -  unfolding Sup_filter_def
   1.211 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.212 -  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
   1.213 -  done
   1.214 -
   1.215 -instance proof
   1.216 -  fix F F' F'' :: "'a filter" and S :: "'a filter set"
   1.217 -  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   1.218 -    by (rule less_filter_def) }
   1.219 -  { show "F \<le> F"
   1.220 -    unfolding le_filter_def by simp }
   1.221 -  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
   1.222 -    unfolding le_filter_def by simp }
   1.223 -  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
   1.224 -    unfolding le_filter_def filter_eq_iff by fast }
   1.225 -  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
   1.226 -    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
   1.227 -  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
   1.228 -    unfolding le_filter_def eventually_inf
   1.229 -    by (auto elim!: eventually_mono intro: eventually_conj) }
   1.230 -  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
   1.231 -    unfolding le_filter_def eventually_sup by simp_all }
   1.232 -  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
   1.233 -    unfolding le_filter_def eventually_sup by simp }
   1.234 -  { assume "F'' \<in> S" thus "Inf S \<le> F''"
   1.235 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   1.236 -  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
   1.237 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   1.238 -  { assume "F \<in> S" thus "F \<le> Sup S"
   1.239 -    unfolding le_filter_def eventually_Sup by simp }
   1.240 -  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
   1.241 -    unfolding le_filter_def eventually_Sup by simp }
   1.242 -  { show "Inf {} = (top::'a filter)"
   1.243 -    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
   1.244 -      (metis (full_types) top_filter_def always_eventually eventually_top) }
   1.245 -  { show "Sup {} = (bot::'a filter)"
   1.246 -    by (auto simp: bot_filter_def Sup_filter_def) }
   1.247 -qed
   1.248 -
   1.249 -end
   1.250 -
   1.251 -lemma filter_leD:
   1.252 -  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
   1.253 -  unfolding le_filter_def by simp
   1.254 -
   1.255 -lemma filter_leI:
   1.256 -  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
   1.257 -  unfolding le_filter_def by simp
   1.258 -
   1.259 -lemma eventually_False:
   1.260 -  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   1.261 -  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
   1.262 -
   1.263 -abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   1.264 -  where "trivial_limit F \<equiv> F = bot"
   1.265 -
   1.266 -lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   1.267 -  by (rule eventually_False [symmetric])
   1.268 -
   1.269 -lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
   1.270 -  by (cases P) (simp_all add: eventually_False)
   1.271 -
   1.272 -lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
   1.273 -proof -
   1.274 -  let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
   1.275 -  
   1.276 -  { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
   1.277 -    proof (rule eventually_Abs_filter is_filter.intro)+
   1.278 -      show "?F (\<lambda>x. True)"
   1.279 -        by (rule exI[of _ "{}"]) (simp add: le_fun_def)
   1.280 -    next
   1.281 -      fix P Q
   1.282 -      assume "?F P" then guess X ..
   1.283 -      moreover
   1.284 -      assume "?F Q" then guess Y ..
   1.285 -      ultimately show "?F (\<lambda>x. P x \<and> Q x)"
   1.286 -        by (intro exI[of _ "X \<union> Y"])
   1.287 -           (auto simp: Inf_union_distrib eventually_inf)
   1.288 -    next
   1.289 -      fix P Q
   1.290 -      assume "?F P" then guess X ..
   1.291 -      moreover assume "\<forall>x. P x \<longrightarrow> Q x"
   1.292 -      ultimately show "?F Q"
   1.293 -        by (intro exI[of _ X]) (auto elim: eventually_elim1)
   1.294 -    qed }
   1.295 -  note eventually_F = this
   1.296 -
   1.297 -  have "Inf B = Abs_filter ?F"
   1.298 -  proof (intro antisym Inf_greatest)
   1.299 -    show "Inf B \<le> Abs_filter ?F"
   1.300 -      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
   1.301 -  next
   1.302 -    fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
   1.303 -      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
   1.304 -  qed
   1.305 -  then show ?thesis
   1.306 -    by (simp add: eventually_F)
   1.307 -qed
   1.308 -
   1.309 -lemma eventually_INF: "eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (INF b:X. F b))"
   1.310 -  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
   1.311 -  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
   1.312 -
   1.313 -lemma Inf_filter_not_bot:
   1.314 -  fixes B :: "'a filter set"
   1.315 -  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
   1.316 -  unfolding trivial_limit_def eventually_Inf[of _ B]
   1.317 -    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
   1.318 -
   1.319 -lemma INF_filter_not_bot:
   1.320 -  fixes F :: "'i \<Rightarrow> 'a filter"
   1.321 -  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> (INF b:X. F b) \<noteq> bot) \<Longrightarrow> (INF b:B. F b) \<noteq> bot"
   1.322 -  unfolding trivial_limit_def eventually_INF[of _ B]
   1.323 -    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
   1.324 -
   1.325 -lemma eventually_Inf_base:
   1.326 -  assumes "B \<noteq> {}" and base: "\<And>F G. F \<in> B \<Longrightarrow> G \<in> B \<Longrightarrow> \<exists>x\<in>B. x \<le> inf F G"
   1.327 -  shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
   1.328 -proof (subst eventually_Inf, safe)
   1.329 -  fix X assume "finite X" "X \<subseteq> B"
   1.330 -  then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
   1.331 -  proof induct
   1.332 -    case empty then show ?case
   1.333 -      using `B \<noteq> {}` by auto
   1.334 -  next
   1.335 -    case (insert x X)
   1.336 -    then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
   1.337 -      by auto
   1.338 -    with `insert x X \<subseteq> B` base[of b x] show ?case
   1.339 -      by (auto intro: order_trans)
   1.340 -  qed
   1.341 -  then obtain b where "b \<in> B" "b \<le> Inf X"
   1.342 -    by (auto simp: le_Inf_iff)
   1.343 -  then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
   1.344 -    by (intro bexI[of _ b]) (auto simp: le_filter_def)
   1.345 -qed (auto intro!: exI[of _ "{x}" for x])
   1.346 -
   1.347 -lemma eventually_INF_base:
   1.348 -  "B \<noteq> {} \<Longrightarrow> (\<And>a b. a \<in> B \<Longrightarrow> b \<in> B \<Longrightarrow> \<exists>x\<in>B. F x \<le> inf (F a) (F b)) \<Longrightarrow>
   1.349 -    eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
   1.350 -  unfolding INF_def by (subst eventually_Inf_base) auto
   1.351 -
   1.352 -
   1.353 -subsubsection {* Map function for filters *}
   1.354 -
   1.355 -definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
   1.356 -  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
   1.357 -
   1.358 -lemma eventually_filtermap:
   1.359 -  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
   1.360 -  unfolding filtermap_def
   1.361 -  apply (rule eventually_Abs_filter)
   1.362 -  apply (rule is_filter.intro)
   1.363 -  apply (auto elim!: eventually_rev_mp)
   1.364 -  done
   1.365 -
   1.366 -lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
   1.367 -  by (simp add: filter_eq_iff eventually_filtermap)
   1.368 -
   1.369 -lemma filtermap_filtermap:
   1.370 -  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
   1.371 -  by (simp add: filter_eq_iff eventually_filtermap)
   1.372 -
   1.373 -lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
   1.374 -  unfolding le_filter_def eventually_filtermap by simp
   1.375 -
   1.376 -lemma filtermap_bot [simp]: "filtermap f bot = bot"
   1.377 -  by (simp add: filter_eq_iff eventually_filtermap)
   1.378 -
   1.379 -lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
   1.380 -  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
   1.381 -
   1.382 -lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
   1.383 -  by (auto simp: le_filter_def eventually_filtermap eventually_inf)
   1.384 -
   1.385 -lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
   1.386 -proof -
   1.387 -  { fix X :: "'c set" assume "finite X"
   1.388 -    then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
   1.389 -    proof induct
   1.390 -      case (insert x X)
   1.391 -      have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
   1.392 -        by (rule order_trans[OF _ filtermap_inf]) simp
   1.393 -      also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
   1.394 -        by (intro inf_mono insert order_refl)
   1.395 -      finally show ?case
   1.396 -        by simp
   1.397 -    qed simp }
   1.398 -  then show ?thesis
   1.399 -    unfolding le_filter_def eventually_filtermap
   1.400 -    by (subst (1 2) eventually_INF) auto
   1.401 -qed
   1.402 -subsubsection {* Standard filters *}
   1.403 -
   1.404 -definition principal :: "'a set \<Rightarrow> 'a filter" where
   1.405 -  "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
   1.406 -
   1.407 -lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
   1.408 -  unfolding principal_def
   1.409 -  by (rule eventually_Abs_filter, rule is_filter.intro) auto
   1.410 -
   1.411 -lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
   1.412 -  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
   1.413 -
   1.414 -lemma principal_UNIV[simp]: "principal UNIV = top"
   1.415 -  by (auto simp: filter_eq_iff eventually_principal)
   1.416 -
   1.417 -lemma principal_empty[simp]: "principal {} = bot"
   1.418 -  by (auto simp: filter_eq_iff eventually_principal)
   1.419 -
   1.420 -lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
   1.421 -  by (auto simp add: filter_eq_iff eventually_principal)
   1.422 -
   1.423 -lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
   1.424 -  by (auto simp: le_filter_def eventually_principal)
   1.425 -
   1.426 -lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
   1.427 -  unfolding le_filter_def eventually_principal
   1.428 -  apply safe
   1.429 -  apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
   1.430 -  apply (auto elim: eventually_elim1)
   1.431 -  done
   1.432 -
   1.433 -lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
   1.434 -  unfolding eq_iff by simp
   1.435 -
   1.436 -lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
   1.437 -  unfolding filter_eq_iff eventually_sup eventually_principal by auto
   1.438 -
   1.439 -lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
   1.440 -  unfolding filter_eq_iff eventually_inf eventually_principal
   1.441 -  by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
   1.442 -
   1.443 -lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
   1.444 -  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
   1.445 -
   1.446 -lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
   1.447 -  by (induct X rule: finite_induct) auto
   1.448 -
   1.449 -lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
   1.450 -  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
   1.451 -
   1.452 -subsubsection {* Order filters *}
   1.453 -
   1.454 -definition at_top :: "('a::order) filter"
   1.455 -  where "at_top = (INF k. principal {k ..})"
   1.456 -
   1.457 -lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
   1.458 -  by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
   1.459 -
   1.460 -lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
   1.461 -  unfolding at_top_def
   1.462 -  by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   1.463 -
   1.464 -lemma eventually_ge_at_top:
   1.465 -  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   1.466 -  unfolding eventually_at_top_linorder by auto
   1.467 -
   1.468 -lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
   1.469 -proof -
   1.470 -  have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
   1.471 -    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   1.472 -  also have "(INF k. principal {k::'a <..}) = at_top"
   1.473 -    unfolding at_top_def 
   1.474 -    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
   1.475 -  finally show ?thesis .
   1.476 -qed
   1.477 -
   1.478 -lemma eventually_gt_at_top:
   1.479 -  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
   1.480 -  unfolding eventually_at_top_dense by auto
   1.481 -
   1.482 -definition at_bot :: "('a::order) filter"
   1.483 -  where "at_bot = (INF k. principal {.. k})"
   1.484 -
   1.485 -lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
   1.486 -  by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
   1.487 -
   1.488 -lemma eventually_at_bot_linorder:
   1.489 -  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
   1.490 -  unfolding at_bot_def
   1.491 -  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   1.492 -
   1.493 -lemma eventually_le_at_bot:
   1.494 -  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   1.495 -  unfolding eventually_at_bot_linorder by auto
   1.496 -
   1.497 -lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
   1.498 -proof -
   1.499 -  have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
   1.500 -    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   1.501 -  also have "(INF k. principal {..< k::'a}) = at_bot"
   1.502 -    unfolding at_bot_def 
   1.503 -    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
   1.504 -  finally show ?thesis .
   1.505 -qed
   1.506 -
   1.507 -lemma eventually_gt_at_bot:
   1.508 -  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   1.509 -  unfolding eventually_at_bot_dense by auto
   1.510 -
   1.511 -lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
   1.512 -  unfolding trivial_limit_def
   1.513 -  by (metis eventually_at_bot_linorder order_refl)
   1.514 -
   1.515 -lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
   1.516 -  unfolding trivial_limit_def
   1.517 -  by (metis eventually_at_top_linorder order_refl)
   1.518 -
   1.519 -subsection {* Sequentially *}
   1.520 -
   1.521 -abbreviation sequentially :: "nat filter"
   1.522 -  where "sequentially \<equiv> at_top"
   1.523 -
   1.524 -lemma eventually_sequentially:
   1.525 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   1.526 -  by (rule eventually_at_top_linorder)
   1.527 -
   1.528 -lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   1.529 -  unfolding filter_eq_iff eventually_sequentially by auto
   1.530 -
   1.531 -lemmas trivial_limit_sequentially = sequentially_bot
   1.532 -
   1.533 -lemma eventually_False_sequentially [simp]:
   1.534 -  "\<not> eventually (\<lambda>n. False) sequentially"
   1.535 -  by (simp add: eventually_False)
   1.536 -
   1.537 -lemma le_sequentially:
   1.538 -  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   1.539 -  by (simp add: at_top_def le_INF_iff le_principal)
   1.540 -
   1.541 -lemma eventually_sequentiallyI:
   1.542 -  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   1.543 -  shows "eventually P sequentially"
   1.544 -using assms by (auto simp: eventually_sequentially)
   1.545 -
   1.546 -lemma eventually_sequentially_seg:
   1.547 -  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.548 -  unfolding eventually_sequentially
   1.549 -  apply safe
   1.550 -   apply (rule_tac x="N + k" in exI)
   1.551 -   apply rule
   1.552 -   apply (erule_tac x="n - k" in allE)
   1.553 -   apply auto []
   1.554 -  apply (rule_tac x=N in exI)
   1.555 -  apply auto []
   1.556 -  done
   1.557 -
   1.558  subsubsection {* Topological filters *}
   1.559  
   1.560  definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
   1.561 @@ -1005,104 +454,6 @@
   1.562    "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   1.563    by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   1.564  
   1.565 -subsection {* Limits *}
   1.566 -
   1.567 -definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
   1.568 -  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
   1.569 -
   1.570 -syntax
   1.571 -  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
   1.572 -
   1.573 -translations
   1.574 -  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
   1.575 -
   1.576 -lemma filterlim_iff:
   1.577 -  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
   1.578 -  unfolding filterlim_def le_filter_def eventually_filtermap ..
   1.579 -
   1.580 -lemma filterlim_compose:
   1.581 -  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
   1.582 -  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
   1.583 -
   1.584 -lemma filterlim_mono:
   1.585 -  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
   1.586 -  unfolding filterlim_def by (metis filtermap_mono order_trans)
   1.587 -
   1.588 -lemma filterlim_ident: "LIM x F. x :> F"
   1.589 -  by (simp add: filterlim_def filtermap_ident)
   1.590 -
   1.591 -lemma filterlim_cong:
   1.592 -  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
   1.593 -  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
   1.594 -
   1.595 -lemma filterlim_mono_eventually:
   1.596 -  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
   1.597 -  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
   1.598 -  shows "filterlim f' F' G'"
   1.599 -  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
   1.600 -  apply (rule filterlim_mono[OF _ ord])
   1.601 -  apply fact
   1.602 -  done
   1.603 -
   1.604 -lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
   1.605 -  apply (auto intro!: filtermap_mono) []
   1.606 -  apply (auto simp: le_filter_def eventually_filtermap)
   1.607 -  apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
   1.608 -  apply auto
   1.609 -  done
   1.610 -
   1.611 -lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
   1.612 -  by (simp add: filtermap_mono_strong eq_iff)
   1.613 -
   1.614 -lemma filterlim_principal:
   1.615 -  "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   1.616 -  unfolding filterlim_def eventually_filtermap le_principal ..
   1.617 -
   1.618 -lemma filterlim_inf:
   1.619 -  "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   1.620 -  unfolding filterlim_def by simp
   1.621 -
   1.622 -lemma filterlim_INF:
   1.623 -  "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
   1.624 -  unfolding filterlim_def le_INF_iff ..
   1.625 -
   1.626 -lemma filterlim_INF_INF:
   1.627 -  "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (INF i:I. F i). f x :> (INF j:J. G j)"
   1.628 -  unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
   1.629 -
   1.630 -lemma filterlim_base:
   1.631 -  "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow> 
   1.632 -    LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
   1.633 -  by (force intro!: filterlim_INF_INF simp: image_subset_iff)
   1.634 -
   1.635 -lemma filterlim_base_iff: 
   1.636 -  assumes "I \<noteq> {}" and chain: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> F i \<subseteq> F j \<or> F j \<subseteq> F i"
   1.637 -  shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
   1.638 -    (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
   1.639 -  unfolding filterlim_INF filterlim_principal
   1.640 -proof (subst eventually_INF_base)
   1.641 -  fix i j assume "i \<in> I" "j \<in> I"
   1.642 -  with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
   1.643 -    by auto
   1.644 -qed (auto simp: eventually_principal `I \<noteq> {}`)
   1.645 -
   1.646 -lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   1.647 -  unfolding filterlim_def filtermap_filtermap ..
   1.648 -
   1.649 -lemma filterlim_sup:
   1.650 -  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
   1.651 -  unfolding filterlim_def filtermap_sup by auto
   1.652 -
   1.653 -lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.654 -  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
   1.655 -
   1.656 -lemma filterlim_sequentially_Suc:
   1.657 -  "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
   1.658 -  unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
   1.659 -
   1.660 -lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
   1.661 -  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
   1.662 -
   1.663  subsubsection {* Tendsto *}
   1.664  
   1.665  abbreviation (in topological_space)
   1.666 @@ -1296,92 +647,6 @@
   1.667  lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   1.668    by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
   1.669  
   1.670 -subsection {* Limits to @{const at_top} and @{const at_bot} *}
   1.671 -
   1.672 -lemma filterlim_at_top:
   1.673 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.674 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
   1.675 -  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
   1.676 -
   1.677 -lemma filterlim_at_top_mono:
   1.678 -  "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
   1.679 -    LIM x F. g x :> at_top"
   1.680 -  by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
   1.681 -
   1.682 -lemma filterlim_at_top_dense:
   1.683 -  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
   1.684 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
   1.685 -  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
   1.686 -            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
   1.687 -
   1.688 -lemma filterlim_at_top_ge:
   1.689 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   1.690 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
   1.691 -  unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
   1.692 -
   1.693 -lemma filterlim_at_top_at_top:
   1.694 -  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
   1.695 -  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   1.696 -  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   1.697 -  assumes Q: "eventually Q at_top"
   1.698 -  assumes P: "eventually P at_top"
   1.699 -  shows "filterlim f at_top at_top"
   1.700 -proof -
   1.701 -  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
   1.702 -    unfolding eventually_at_top_linorder by auto
   1.703 -  show ?thesis
   1.704 -  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
   1.705 -    fix z assume "x \<le> z"
   1.706 -    with x have "P z" by auto
   1.707 -    have "eventually (\<lambda>x. g z \<le> x) at_top"
   1.708 -      by (rule eventually_ge_at_top)
   1.709 -    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
   1.710 -      by eventually_elim (metis mono bij `P z`)
   1.711 -  qed
   1.712 -qed
   1.713 -
   1.714 -lemma filterlim_at_top_gt:
   1.715 -  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   1.716 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
   1.717 -  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
   1.718 -
   1.719 -lemma filterlim_at_bot: 
   1.720 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.721 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
   1.722 -  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
   1.723 -
   1.724 -lemma filterlim_at_bot_dense:
   1.725 -  fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
   1.726 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
   1.727 -proof (auto simp add: filterlim_at_bot[of f F])
   1.728 -  fix Z :: 'b
   1.729 -  from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
   1.730 -  assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
   1.731 -  hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
   1.732 -  thus "eventually (\<lambda>x. f x < Z) F"
   1.733 -    apply (rule eventually_mono[rotated])
   1.734 -    using 1 by auto
   1.735 -  next 
   1.736 -    fix Z :: 'b 
   1.737 -    show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
   1.738 -      by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
   1.739 -qed
   1.740 -
   1.741 -lemma filterlim_at_bot_le:
   1.742 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   1.743 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
   1.744 -  unfolding filterlim_at_bot
   1.745 -proof safe
   1.746 -  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
   1.747 -  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
   1.748 -    by (auto elim!: eventually_elim1)
   1.749 -qed simp
   1.750 -
   1.751 -lemma filterlim_at_bot_lt:
   1.752 -  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   1.753 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
   1.754 -  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
   1.755 -
   1.756  lemma filterlim_at_bot_at_right:
   1.757    fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   1.758    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   1.759 @@ -2936,220 +2201,4 @@
   1.760    qed
   1.761  qed (intro cSUP_least `antimono f`[THEN antimonoD] cInf_lower S)
   1.762  
   1.763 -subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
   1.764 -
   1.765 -context begin interpretation lifting_syntax .
   1.766 -
   1.767 -definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
   1.768 -where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
   1.769 -
   1.770 -lemma rel_filter_eventually:
   1.771 -  "rel_filter R F G \<longleftrightarrow> 
   1.772 -  ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
   1.773 -by(simp add: rel_filter_def eventually_def)
   1.774 -
   1.775 -lemma filtermap_id [simp, id_simps]: "filtermap id = id"
   1.776 -by(simp add: fun_eq_iff id_def filtermap_ident)
   1.777 -
   1.778 -lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
   1.779 -using filtermap_id unfolding id_def .
   1.780 -
   1.781 -lemma Quotient_filter [quot_map]:
   1.782 -  assumes Q: "Quotient R Abs Rep T"
   1.783 -  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
   1.784 -unfolding Quotient_alt_def
   1.785 -proof(intro conjI strip)
   1.786 -  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
   1.787 -    unfolding Quotient_alt_def by blast
   1.788 -
   1.789 -  fix F G
   1.790 -  assume "rel_filter T F G"
   1.791 -  thus "filtermap Abs F = G" unfolding filter_eq_iff
   1.792 -    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
   1.793 -next
   1.794 -  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
   1.795 -
   1.796 -  fix F
   1.797 -  show "rel_filter T (filtermap Rep F) F" 
   1.798 -    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
   1.799 -            del: iffI simp add: eventually_filtermap rel_filter_eventually)
   1.800 -qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
   1.801 -         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
   1.802 -
   1.803 -lemma eventually_parametric [transfer_rule]:
   1.804 -  "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
   1.805 -by(simp add: rel_fun_def rel_filter_eventually)
   1.806 -
   1.807 -lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
   1.808 -by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
   1.809 -
   1.810 -lemma rel_filter_mono [relator_mono]:
   1.811 -  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
   1.812 -unfolding rel_filter_eventually[abs_def]
   1.813 -by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
   1.814 -
   1.815 -lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
   1.816 -by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
   1.817 -
   1.818 -lemma is_filter_parametric_aux:
   1.819 -  assumes "is_filter F"
   1.820 -  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   1.821 -  and [transfer_rule]: "((A ===> op =) ===> op =) F G"
   1.822 -  shows "is_filter G"
   1.823 -proof -
   1.824 -  interpret is_filter F by fact
   1.825 -  show ?thesis
   1.826 -  proof
   1.827 -    have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
   1.828 -    thus "G (\<lambda>x. True)" by(simp add: True)
   1.829 -  next
   1.830 -    fix P' Q'
   1.831 -    assume "G P'" "G Q'"
   1.832 -    moreover
   1.833 -    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
   1.834 -    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
   1.835 -    have "F P = G P'" "F Q = G Q'" by transfer_prover+
   1.836 -    ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
   1.837 -    moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
   1.838 -    ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
   1.839 -  next
   1.840 -    fix P' Q'
   1.841 -    assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
   1.842 -    moreover
   1.843 -    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
   1.844 -    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
   1.845 -    have "F P = G P'" by transfer_prover
   1.846 -    moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
   1.847 -    ultimately have "F Q" by(simp add: mono)
   1.848 -    moreover have "F Q = G Q'" by transfer_prover
   1.849 -    ultimately show "G Q'" by simp
   1.850 -  qed
   1.851 -qed
   1.852 -
   1.853 -lemma is_filter_parametric [transfer_rule]:
   1.854 -  "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
   1.855 -  \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
   1.856 -apply(rule rel_funI)
   1.857 -apply(rule iffI)
   1.858 - apply(erule (3) is_filter_parametric_aux)
   1.859 -apply(erule is_filter_parametric_aux[where A="conversep A"])
   1.860 -apply(auto simp add: rel_fun_def)
   1.861 -done
   1.862 -
   1.863 -lemma left_total_rel_filter [transfer_rule]:
   1.864 -  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   1.865 -  shows "left_total (rel_filter A)"
   1.866 -proof(rule left_totalI)
   1.867 -  fix F :: "'a filter"
   1.868 -  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
   1.869 -  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
   1.870 -    unfolding  bi_total_def by blast
   1.871 -  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
   1.872 -  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
   1.873 -  ultimately have "rel_filter A F (Abs_filter G)"
   1.874 -    by(simp add: rel_filter_eventually eventually_Abs_filter)
   1.875 -  thus "\<exists>G. rel_filter A F G" ..
   1.876 -qed
   1.877 -
   1.878 -lemma right_total_rel_filter [transfer_rule]:
   1.879 -  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
   1.880 -using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
   1.881 -
   1.882 -lemma bi_total_rel_filter [transfer_rule]:
   1.883 -  assumes "bi_total A" "bi_unique A"
   1.884 -  shows "bi_total (rel_filter A)"
   1.885 -unfolding bi_total_alt_def using assms
   1.886 -by(simp add: left_total_rel_filter right_total_rel_filter)
   1.887 -
   1.888 -lemma left_unique_rel_filter [transfer_rule]:
   1.889 -  assumes "left_unique A"
   1.890 -  shows "left_unique (rel_filter A)"
   1.891 -proof(rule left_uniqueI)
   1.892 -  fix F F' G
   1.893 -  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
   1.894 -  show "F = F'"
   1.895 -    unfolding filter_eq_iff
   1.896 -  proof
   1.897 -    fix P :: "'a \<Rightarrow> bool"
   1.898 -    obtain P' where [transfer_rule]: "(A ===> op =) P P'"
   1.899 -      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
   1.900 -    have "eventually P F = eventually P' G" 
   1.901 -      and "eventually P F' = eventually P' G" by transfer_prover+
   1.902 -    thus "eventually P F = eventually P F'" by simp
   1.903 -  qed
   1.904 -qed
   1.905 -
   1.906 -lemma right_unique_rel_filter [transfer_rule]:
   1.907 -  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
   1.908 -using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
   1.909 -
   1.910 -lemma bi_unique_rel_filter [transfer_rule]:
   1.911 -  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
   1.912 -by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
   1.913 -
   1.914 -lemma top_filter_parametric [transfer_rule]:
   1.915 -  "bi_total A \<Longrightarrow> (rel_filter A) top top"
   1.916 -by(simp add: rel_filter_eventually All_transfer)
   1.917 -
   1.918 -lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
   1.919 -by(simp add: rel_filter_eventually rel_fun_def)
   1.920 -
   1.921 -lemma sup_filter_parametric [transfer_rule]:
   1.922 -  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
   1.923 -by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
   1.924 -
   1.925 -lemma Sup_filter_parametric [transfer_rule]:
   1.926 -  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
   1.927 -proof(rule rel_funI)
   1.928 -  fix S T
   1.929 -  assume [transfer_rule]: "rel_set (rel_filter A) S T"
   1.930 -  show "rel_filter A (Sup S) (Sup T)"
   1.931 -    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
   1.932 -qed
   1.933 -
   1.934 -lemma principal_parametric [transfer_rule]:
   1.935 -  "(rel_set A ===> rel_filter A) principal principal"
   1.936 -proof(rule rel_funI)
   1.937 -  fix S S'
   1.938 -  assume [transfer_rule]: "rel_set A S S'"
   1.939 -  show "rel_filter A (principal S) (principal S')"
   1.940 -    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
   1.941 -qed
   1.942 -
   1.943 -context
   1.944 -  fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.945 -  assumes [transfer_rule]: "bi_unique A" 
   1.946 -begin
   1.947 -
   1.948 -lemma le_filter_parametric [transfer_rule]:
   1.949 -  "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
   1.950 -unfolding le_filter_def[abs_def] by transfer_prover
   1.951 -
   1.952 -lemma less_filter_parametric [transfer_rule]:
   1.953 -  "(rel_filter A ===> rel_filter A ===> op =) op < op <"
   1.954 -unfolding less_filter_def[abs_def] by transfer_prover
   1.955 -
   1.956 -context
   1.957 -  assumes [transfer_rule]: "bi_total A"
   1.958 -begin
   1.959 -
   1.960 -lemma Inf_filter_parametric [transfer_rule]:
   1.961 -  "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
   1.962 -unfolding Inf_filter_def[abs_def] by transfer_prover
   1.963 -
   1.964 -lemma inf_filter_parametric [transfer_rule]:
   1.965 -  "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
   1.966 -proof(intro rel_funI)+
   1.967 -  fix F F' G G'
   1.968 -  assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
   1.969 -  have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
   1.970 -  thus "rel_filter A (inf F G) (inf F' G')" by simp
   1.971 -qed
   1.972 -
   1.973  end
   1.974 -
   1.975 -end
   1.976 -
   1.977 -end
   1.978 -
   1.979 -end