move filters to their own theory
authorhoelzl
Sun Apr 12 11:33:19 2015 +0200 (2015-04-12)
changeset 60036218fcc645d22
parent 60035 4b77fc0b3514
child 60037 071a99649dde
move filters to their own theory
src/HOL/Filter.thy
src/HOL/Main.thy
src/HOL/NSA/Filter.thy
src/HOL/NSA/Free_Ultrafilter.thy
src/HOL/NSA/StarDef.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Filter.thy	Sun Apr 12 11:33:19 2015 +0200
     1.3 @@ -0,0 +1,966 @@
     1.4 +(*  Title:      HOL/Filter.thy
     1.5 +    Author:     Brian Huffman
     1.6 +    Author:     Johannes Hölzl
     1.7 +*)
     1.8 +
     1.9 +section {* Filters on predicates *}
    1.10 +
    1.11 +theory Filter
    1.12 +imports Set_Interval Lifting_Set
    1.13 +begin
    1.14 +
    1.15 +subsection {* Filters *}
    1.16 +
    1.17 +text {*
    1.18 +  This definition also allows non-proper filters.
    1.19 +*}
    1.20 +
    1.21 +locale is_filter =
    1.22 +  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.23 +  assumes True: "F (\<lambda>x. True)"
    1.24 +  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
    1.25 +  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
    1.26 +
    1.27 +typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
    1.28 +proof
    1.29 +  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
    1.30 +qed
    1.31 +
    1.32 +lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
    1.33 +  using Rep_filter [of F] by simp
    1.34 +
    1.35 +lemma Abs_filter_inverse':
    1.36 +  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
    1.37 +  using assms by (simp add: Abs_filter_inverse)
    1.38 +
    1.39 +
    1.40 +subsubsection {* Eventually *}
    1.41 +
    1.42 +definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.43 +  where "eventually P F \<longleftrightarrow> Rep_filter F P"
    1.44 +
    1.45 +lemma eventually_Abs_filter:
    1.46 +  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
    1.47 +  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
    1.48 +
    1.49 +lemma filter_eq_iff:
    1.50 +  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
    1.51 +  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
    1.52 +
    1.53 +lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
    1.54 +  unfolding eventually_def
    1.55 +  by (rule is_filter.True [OF is_filter_Rep_filter])
    1.56 +
    1.57 +lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
    1.58 +proof -
    1.59 +  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
    1.60 +  thus "eventually P F" by simp
    1.61 +qed
    1.62 +
    1.63 +lemma eventually_mono:
    1.64 +  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
    1.65 +  unfolding eventually_def
    1.66 +  by (rule is_filter.mono [OF is_filter_Rep_filter])
    1.67 +
    1.68 +lemma eventually_conj:
    1.69 +  assumes P: "eventually (\<lambda>x. P x) F"
    1.70 +  assumes Q: "eventually (\<lambda>x. Q x) F"
    1.71 +  shows "eventually (\<lambda>x. P x \<and> Q x) F"
    1.72 +  using assms unfolding eventually_def
    1.73 +  by (rule is_filter.conj [OF is_filter_Rep_filter])
    1.74 +
    1.75 +lemma eventually_Ball_finite:
    1.76 +  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
    1.77 +  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
    1.78 +using assms by (induct set: finite, simp, simp add: eventually_conj)
    1.79 +
    1.80 +lemma eventually_all_finite:
    1.81 +  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
    1.82 +  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
    1.83 +  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
    1.84 +using eventually_Ball_finite [of UNIV P] assms by simp
    1.85 +
    1.86 +lemma eventually_mp:
    1.87 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.88 +  assumes "eventually (\<lambda>x. P x) F"
    1.89 +  shows "eventually (\<lambda>x. Q x) F"
    1.90 +proof (rule eventually_mono)
    1.91 +  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
    1.92 +  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
    1.93 +    using assms by (rule eventually_conj)
    1.94 +qed
    1.95 +
    1.96 +lemma eventually_rev_mp:
    1.97 +  assumes "eventually (\<lambda>x. P x) F"
    1.98 +  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.99 +  shows "eventually (\<lambda>x. Q x) F"
   1.100 +using assms(2) assms(1) by (rule eventually_mp)
   1.101 +
   1.102 +lemma eventually_conj_iff:
   1.103 +  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
   1.104 +  by (auto intro: eventually_conj elim: eventually_rev_mp)
   1.105 +
   1.106 +lemma eventually_elim1:
   1.107 +  assumes "eventually (\<lambda>i. P i) F"
   1.108 +  assumes "\<And>i. P i \<Longrightarrow> Q i"
   1.109 +  shows "eventually (\<lambda>i. Q i) F"
   1.110 +  using assms by (auto elim!: eventually_rev_mp)
   1.111 +
   1.112 +lemma eventually_elim2:
   1.113 +  assumes "eventually (\<lambda>i. P i) F"
   1.114 +  assumes "eventually (\<lambda>i. Q i) F"
   1.115 +  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
   1.116 +  shows "eventually (\<lambda>i. R i) F"
   1.117 +  using assms by (auto elim!: eventually_rev_mp)
   1.118 +
   1.119 +lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   1.120 +  by (auto intro: eventually_mp)
   1.121 +
   1.122 +lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
   1.123 +  by (metis always_eventually)
   1.124 +
   1.125 +lemma eventually_subst:
   1.126 +  assumes "eventually (\<lambda>n. P n = Q n) F"
   1.127 +  shows "eventually P F = eventually Q F" (is "?L = ?R")
   1.128 +proof -
   1.129 +  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   1.130 +      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
   1.131 +    by (auto elim: eventually_elim1)
   1.132 +  then show ?thesis by (auto elim: eventually_elim2)
   1.133 +qed
   1.134 +
   1.135 +ML {*
   1.136 +  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
   1.137 +    let
   1.138 +      val mp_thms = facts RL @{thms eventually_rev_mp}
   1.139 +      val raw_elim_thm =
   1.140 +        (@{thm allI} RS @{thm always_eventually})
   1.141 +        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
   1.142 +        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
   1.143 +      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
   1.144 +      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
   1.145 +    in
   1.146 +      CASES cases (rtac raw_elim_thm i)
   1.147 +    end)
   1.148 +*}
   1.149 +
   1.150 +method_setup eventually_elim = {*
   1.151 +  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
   1.152 +*} "elimination of eventually quantifiers"
   1.153 +
   1.154 +
   1.155 +subsubsection {* Finer-than relation *}
   1.156 +
   1.157 +text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
   1.158 +filter @{term F'}. *}
   1.159 +
   1.160 +instantiation filter :: (type) complete_lattice
   1.161 +begin
   1.162 +
   1.163 +definition le_filter_def:
   1.164 +  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
   1.165 +
   1.166 +definition
   1.167 +  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   1.168 +
   1.169 +definition
   1.170 +  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
   1.171 +
   1.172 +definition
   1.173 +  "bot = Abs_filter (\<lambda>P. True)"
   1.174 +
   1.175 +definition
   1.176 +  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
   1.177 +
   1.178 +definition
   1.179 +  "inf F F' = Abs_filter
   1.180 +      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.181 +
   1.182 +definition
   1.183 +  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
   1.184 +
   1.185 +definition
   1.186 +  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
   1.187 +
   1.188 +lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
   1.189 +  unfolding top_filter_def
   1.190 +  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
   1.191 +
   1.192 +lemma eventually_bot [simp]: "eventually P bot"
   1.193 +  unfolding bot_filter_def
   1.194 +  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
   1.195 +
   1.196 +lemma eventually_sup:
   1.197 +  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
   1.198 +  unfolding sup_filter_def
   1.199 +  by (rule eventually_Abs_filter, rule is_filter.intro)
   1.200 +     (auto elim!: eventually_rev_mp)
   1.201 +
   1.202 +lemma eventually_inf:
   1.203 +  "eventually P (inf F F') \<longleftrightarrow>
   1.204 +   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   1.205 +  unfolding inf_filter_def
   1.206 +  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.207 +  apply (fast intro: eventually_True)
   1.208 +  apply clarify
   1.209 +  apply (intro exI conjI)
   1.210 +  apply (erule (1) eventually_conj)
   1.211 +  apply (erule (1) eventually_conj)
   1.212 +  apply simp
   1.213 +  apply auto
   1.214 +  done
   1.215 +
   1.216 +lemma eventually_Sup:
   1.217 +  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
   1.218 +  unfolding Sup_filter_def
   1.219 +  apply (rule eventually_Abs_filter, rule is_filter.intro)
   1.220 +  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
   1.221 +  done
   1.222 +
   1.223 +instance proof
   1.224 +  fix F F' F'' :: "'a filter" and S :: "'a filter set"
   1.225 +  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   1.226 +    by (rule less_filter_def) }
   1.227 +  { show "F \<le> F"
   1.228 +    unfolding le_filter_def by simp }
   1.229 +  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
   1.230 +    unfolding le_filter_def by simp }
   1.231 +  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
   1.232 +    unfolding le_filter_def filter_eq_iff by fast }
   1.233 +  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
   1.234 +    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
   1.235 +  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
   1.236 +    unfolding le_filter_def eventually_inf
   1.237 +    by (auto elim!: eventually_mono intro: eventually_conj) }
   1.238 +  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
   1.239 +    unfolding le_filter_def eventually_sup by simp_all }
   1.240 +  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
   1.241 +    unfolding le_filter_def eventually_sup by simp }
   1.242 +  { assume "F'' \<in> S" thus "Inf S \<le> F''"
   1.243 +    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   1.244 +  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
   1.245 +    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   1.246 +  { assume "F \<in> S" thus "F \<le> Sup S"
   1.247 +    unfolding le_filter_def eventually_Sup by simp }
   1.248 +  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
   1.249 +    unfolding le_filter_def eventually_Sup by simp }
   1.250 +  { show "Inf {} = (top::'a filter)"
   1.251 +    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
   1.252 +      (metis (full_types) top_filter_def always_eventually eventually_top) }
   1.253 +  { show "Sup {} = (bot::'a filter)"
   1.254 +    by (auto simp: bot_filter_def Sup_filter_def) }
   1.255 +qed
   1.256 +
   1.257 +end
   1.258 +
   1.259 +lemma filter_leD:
   1.260 +  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
   1.261 +  unfolding le_filter_def by simp
   1.262 +
   1.263 +lemma filter_leI:
   1.264 +  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
   1.265 +  unfolding le_filter_def by simp
   1.266 +
   1.267 +lemma eventually_False:
   1.268 +  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   1.269 +  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
   1.270 +
   1.271 +abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   1.272 +  where "trivial_limit F \<equiv> F = bot"
   1.273 +
   1.274 +lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   1.275 +  by (rule eventually_False [symmetric])
   1.276 +
   1.277 +lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
   1.278 +  by (cases P) (simp_all add: eventually_False)
   1.279 +
   1.280 +lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
   1.281 +proof -
   1.282 +  let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
   1.283 +  
   1.284 +  { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
   1.285 +    proof (rule eventually_Abs_filter is_filter.intro)+
   1.286 +      show "?F (\<lambda>x. True)"
   1.287 +        by (rule exI[of _ "{}"]) (simp add: le_fun_def)
   1.288 +    next
   1.289 +      fix P Q
   1.290 +      assume "?F P" then guess X ..
   1.291 +      moreover
   1.292 +      assume "?F Q" then guess Y ..
   1.293 +      ultimately show "?F (\<lambda>x. P x \<and> Q x)"
   1.294 +        by (intro exI[of _ "X \<union> Y"])
   1.295 +           (auto simp: Inf_union_distrib eventually_inf)
   1.296 +    next
   1.297 +      fix P Q
   1.298 +      assume "?F P" then guess X ..
   1.299 +      moreover assume "\<forall>x. P x \<longrightarrow> Q x"
   1.300 +      ultimately show "?F Q"
   1.301 +        by (intro exI[of _ X]) (auto elim: eventually_elim1)
   1.302 +    qed }
   1.303 +  note eventually_F = this
   1.304 +
   1.305 +  have "Inf B = Abs_filter ?F"
   1.306 +  proof (intro antisym Inf_greatest)
   1.307 +    show "Inf B \<le> Abs_filter ?F"
   1.308 +      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
   1.309 +  next
   1.310 +    fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
   1.311 +      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
   1.312 +  qed
   1.313 +  then show ?thesis
   1.314 +    by (simp add: eventually_F)
   1.315 +qed
   1.316 +
   1.317 +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.318 +  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
   1.319 +  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
   1.320 +
   1.321 +lemma Inf_filter_not_bot:
   1.322 +  fixes B :: "'a filter set"
   1.323 +  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
   1.324 +  unfolding trivial_limit_def eventually_Inf[of _ B]
   1.325 +    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
   1.326 +
   1.327 +lemma INF_filter_not_bot:
   1.328 +  fixes F :: "'i \<Rightarrow> 'a filter"
   1.329 +  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.330 +  unfolding trivial_limit_def eventually_INF[of _ B]
   1.331 +    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
   1.332 +
   1.333 +lemma eventually_Inf_base:
   1.334 +  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.335 +  shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
   1.336 +proof (subst eventually_Inf, safe)
   1.337 +  fix X assume "finite X" "X \<subseteq> B"
   1.338 +  then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
   1.339 +  proof induct
   1.340 +    case empty then show ?case
   1.341 +      using `B \<noteq> {}` by auto
   1.342 +  next
   1.343 +    case (insert x X)
   1.344 +    then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
   1.345 +      by auto
   1.346 +    with `insert x X \<subseteq> B` base[of b x] show ?case
   1.347 +      by (auto intro: order_trans)
   1.348 +  qed
   1.349 +  then obtain b where "b \<in> B" "b \<le> Inf X"
   1.350 +    by (auto simp: le_Inf_iff)
   1.351 +  then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
   1.352 +    by (intro bexI[of _ b]) (auto simp: le_filter_def)
   1.353 +qed (auto intro!: exI[of _ "{x}" for x])
   1.354 +
   1.355 +lemma eventually_INF_base:
   1.356 +  "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.357 +    eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
   1.358 +  unfolding INF_def by (subst eventually_Inf_base) auto
   1.359 +
   1.360 +
   1.361 +subsubsection {* Map function for filters *}
   1.362 +
   1.363 +definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
   1.364 +  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
   1.365 +
   1.366 +lemma eventually_filtermap:
   1.367 +  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
   1.368 +  unfolding filtermap_def
   1.369 +  apply (rule eventually_Abs_filter)
   1.370 +  apply (rule is_filter.intro)
   1.371 +  apply (auto elim!: eventually_rev_mp)
   1.372 +  done
   1.373 +
   1.374 +lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
   1.375 +  by (simp add: filter_eq_iff eventually_filtermap)
   1.376 +
   1.377 +lemma filtermap_filtermap:
   1.378 +  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
   1.379 +  by (simp add: filter_eq_iff eventually_filtermap)
   1.380 +
   1.381 +lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
   1.382 +  unfolding le_filter_def eventually_filtermap by simp
   1.383 +
   1.384 +lemma filtermap_bot [simp]: "filtermap f bot = bot"
   1.385 +  by (simp add: filter_eq_iff eventually_filtermap)
   1.386 +
   1.387 +lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
   1.388 +  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
   1.389 +
   1.390 +lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
   1.391 +  by (auto simp: le_filter_def eventually_filtermap eventually_inf)
   1.392 +
   1.393 +lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
   1.394 +proof -
   1.395 +  { fix X :: "'c set" assume "finite X"
   1.396 +    then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
   1.397 +    proof induct
   1.398 +      case (insert x X)
   1.399 +      have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
   1.400 +        by (rule order_trans[OF _ filtermap_inf]) simp
   1.401 +      also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
   1.402 +        by (intro inf_mono insert order_refl)
   1.403 +      finally show ?case
   1.404 +        by simp
   1.405 +    qed simp }
   1.406 +  then show ?thesis
   1.407 +    unfolding le_filter_def eventually_filtermap
   1.408 +    by (subst (1 2) eventually_INF) auto
   1.409 +qed
   1.410 +subsubsection {* Standard filters *}
   1.411 +
   1.412 +definition principal :: "'a set \<Rightarrow> 'a filter" where
   1.413 +  "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
   1.414 +
   1.415 +lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
   1.416 +  unfolding principal_def
   1.417 +  by (rule eventually_Abs_filter, rule is_filter.intro) auto
   1.418 +
   1.419 +lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
   1.420 +  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
   1.421 +
   1.422 +lemma principal_UNIV[simp]: "principal UNIV = top"
   1.423 +  by (auto simp: filter_eq_iff eventually_principal)
   1.424 +
   1.425 +lemma principal_empty[simp]: "principal {} = bot"
   1.426 +  by (auto simp: filter_eq_iff eventually_principal)
   1.427 +
   1.428 +lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
   1.429 +  by (auto simp add: filter_eq_iff eventually_principal)
   1.430 +
   1.431 +lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
   1.432 +  by (auto simp: le_filter_def eventually_principal)
   1.433 +
   1.434 +lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
   1.435 +  unfolding le_filter_def eventually_principal
   1.436 +  apply safe
   1.437 +  apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
   1.438 +  apply (auto elim: eventually_elim1)
   1.439 +  done
   1.440 +
   1.441 +lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
   1.442 +  unfolding eq_iff by simp
   1.443 +
   1.444 +lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
   1.445 +  unfolding filter_eq_iff eventually_sup eventually_principal by auto
   1.446 +
   1.447 +lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
   1.448 +  unfolding filter_eq_iff eventually_inf eventually_principal
   1.449 +  by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
   1.450 +
   1.451 +lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
   1.452 +  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
   1.453 +
   1.454 +lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
   1.455 +  by (induct X rule: finite_induct) auto
   1.456 +
   1.457 +lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
   1.458 +  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
   1.459 +
   1.460 +subsubsection {* Order filters *}
   1.461 +
   1.462 +definition at_top :: "('a::order) filter"
   1.463 +  where "at_top = (INF k. principal {k ..})"
   1.464 +
   1.465 +lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
   1.466 +  by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
   1.467 +
   1.468 +lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
   1.469 +  unfolding at_top_def
   1.470 +  by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   1.471 +
   1.472 +lemma eventually_ge_at_top:
   1.473 +  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   1.474 +  unfolding eventually_at_top_linorder by auto
   1.475 +
   1.476 +lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
   1.477 +proof -
   1.478 +  have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
   1.479 +    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   1.480 +  also have "(INF k. principal {k::'a <..}) = at_top"
   1.481 +    unfolding at_top_def 
   1.482 +    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
   1.483 +  finally show ?thesis .
   1.484 +qed
   1.485 +
   1.486 +lemma eventually_gt_at_top:
   1.487 +  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
   1.488 +  unfolding eventually_at_top_dense by auto
   1.489 +
   1.490 +definition at_bot :: "('a::order) filter"
   1.491 +  where "at_bot = (INF k. principal {.. k})"
   1.492 +
   1.493 +lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
   1.494 +  by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
   1.495 +
   1.496 +lemma eventually_at_bot_linorder:
   1.497 +  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
   1.498 +  unfolding at_bot_def
   1.499 +  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   1.500 +
   1.501 +lemma eventually_le_at_bot:
   1.502 +  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   1.503 +  unfolding eventually_at_bot_linorder by auto
   1.504 +
   1.505 +lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
   1.506 +proof -
   1.507 +  have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
   1.508 +    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   1.509 +  also have "(INF k. principal {..< k::'a}) = at_bot"
   1.510 +    unfolding at_bot_def 
   1.511 +    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
   1.512 +  finally show ?thesis .
   1.513 +qed
   1.514 +
   1.515 +lemma eventually_gt_at_bot:
   1.516 +  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   1.517 +  unfolding eventually_at_bot_dense by auto
   1.518 +
   1.519 +lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
   1.520 +  unfolding trivial_limit_def
   1.521 +  by (metis eventually_at_bot_linorder order_refl)
   1.522 +
   1.523 +lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
   1.524 +  unfolding trivial_limit_def
   1.525 +  by (metis eventually_at_top_linorder order_refl)
   1.526 +
   1.527 +subsection {* Sequentially *}
   1.528 +
   1.529 +abbreviation sequentially :: "nat filter"
   1.530 +  where "sequentially \<equiv> at_top"
   1.531 +
   1.532 +lemma eventually_sequentially:
   1.533 +  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   1.534 +  by (rule eventually_at_top_linorder)
   1.535 +
   1.536 +lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   1.537 +  unfolding filter_eq_iff eventually_sequentially by auto
   1.538 +
   1.539 +lemmas trivial_limit_sequentially = sequentially_bot
   1.540 +
   1.541 +lemma eventually_False_sequentially [simp]:
   1.542 +  "\<not> eventually (\<lambda>n. False) sequentially"
   1.543 +  by (simp add: eventually_False)
   1.544 +
   1.545 +lemma le_sequentially:
   1.546 +  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   1.547 +  by (simp add: at_top_def le_INF_iff le_principal)
   1.548 +
   1.549 +lemma eventually_sequentiallyI:
   1.550 +  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   1.551 +  shows "eventually P sequentially"
   1.552 +using assms by (auto simp: eventually_sequentially)
   1.553 +
   1.554 +lemma eventually_sequentially_seg:
   1.555 +  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.556 +  unfolding eventually_sequentially
   1.557 +  apply safe
   1.558 +   apply (rule_tac x="N + k" in exI)
   1.559 +   apply rule
   1.560 +   apply (erule_tac x="n - k" in allE)
   1.561 +   apply auto []
   1.562 +  apply (rule_tac x=N in exI)
   1.563 +  apply auto []
   1.564 +  done
   1.565 +
   1.566 +
   1.567 +subsection {* Limits *}
   1.568 +
   1.569 +definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
   1.570 +  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
   1.571 +
   1.572 +syntax
   1.573 +  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
   1.574 +
   1.575 +translations
   1.576 +  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
   1.577 +
   1.578 +lemma filterlim_iff:
   1.579 +  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
   1.580 +  unfolding filterlim_def le_filter_def eventually_filtermap ..
   1.581 +
   1.582 +lemma filterlim_compose:
   1.583 +  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
   1.584 +  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
   1.585 +
   1.586 +lemma filterlim_mono:
   1.587 +  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
   1.588 +  unfolding filterlim_def by (metis filtermap_mono order_trans)
   1.589 +
   1.590 +lemma filterlim_ident: "LIM x F. x :> F"
   1.591 +  by (simp add: filterlim_def filtermap_ident)
   1.592 +
   1.593 +lemma filterlim_cong:
   1.594 +  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
   1.595 +  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
   1.596 +
   1.597 +lemma filterlim_mono_eventually:
   1.598 +  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
   1.599 +  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
   1.600 +  shows "filterlim f' F' G'"
   1.601 +  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
   1.602 +  apply (rule filterlim_mono[OF _ ord])
   1.603 +  apply fact
   1.604 +  done
   1.605 +
   1.606 +lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
   1.607 +  apply (auto intro!: filtermap_mono) []
   1.608 +  apply (auto simp: le_filter_def eventually_filtermap)
   1.609 +  apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
   1.610 +  apply auto
   1.611 +  done
   1.612 +
   1.613 +lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
   1.614 +  by (simp add: filtermap_mono_strong eq_iff)
   1.615 +
   1.616 +lemma filterlim_principal:
   1.617 +  "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   1.618 +  unfolding filterlim_def eventually_filtermap le_principal ..
   1.619 +
   1.620 +lemma filterlim_inf:
   1.621 +  "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   1.622 +  unfolding filterlim_def by simp
   1.623 +
   1.624 +lemma filterlim_INF:
   1.625 +  "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
   1.626 +  unfolding filterlim_def le_INF_iff ..
   1.627 +
   1.628 +lemma filterlim_INF_INF:
   1.629 +  "(\<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.630 +  unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
   1.631 +
   1.632 +lemma filterlim_base:
   1.633 +  "(\<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.634 +    LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
   1.635 +  by (force intro!: filterlim_INF_INF simp: image_subset_iff)
   1.636 +
   1.637 +lemma filterlim_base_iff: 
   1.638 +  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.639 +  shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
   1.640 +    (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
   1.641 +  unfolding filterlim_INF filterlim_principal
   1.642 +proof (subst eventually_INF_base)
   1.643 +  fix i j assume "i \<in> I" "j \<in> I"
   1.644 +  with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
   1.645 +    by auto
   1.646 +qed (auto simp: eventually_principal `I \<noteq> {}`)
   1.647 +
   1.648 +lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   1.649 +  unfolding filterlim_def filtermap_filtermap ..
   1.650 +
   1.651 +lemma filterlim_sup:
   1.652 +  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
   1.653 +  unfolding filterlim_def filtermap_sup by auto
   1.654 +
   1.655 +lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.656 +  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
   1.657 +
   1.658 +lemma filterlim_sequentially_Suc:
   1.659 +  "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
   1.660 +  unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
   1.661 +
   1.662 +lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
   1.663 +  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
   1.664 +
   1.665 +
   1.666 +subsection {* Limits to @{const at_top} and @{const at_bot} *}
   1.667 +
   1.668 +lemma filterlim_at_top:
   1.669 +  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.670 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
   1.671 +  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
   1.672 +
   1.673 +lemma filterlim_at_top_mono:
   1.674 +  "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
   1.675 +    LIM x F. g x :> at_top"
   1.676 +  by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
   1.677 +
   1.678 +lemma filterlim_at_top_dense:
   1.679 +  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
   1.680 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
   1.681 +  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
   1.682 +            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
   1.683 +
   1.684 +lemma filterlim_at_top_ge:
   1.685 +  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   1.686 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
   1.687 +  unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
   1.688 +
   1.689 +lemma filterlim_at_top_at_top:
   1.690 +  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
   1.691 +  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   1.692 +  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   1.693 +  assumes Q: "eventually Q at_top"
   1.694 +  assumes P: "eventually P at_top"
   1.695 +  shows "filterlim f at_top at_top"
   1.696 +proof -
   1.697 +  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
   1.698 +    unfolding eventually_at_top_linorder by auto
   1.699 +  show ?thesis
   1.700 +  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
   1.701 +    fix z assume "x \<le> z"
   1.702 +    with x have "P z" by auto
   1.703 +    have "eventually (\<lambda>x. g z \<le> x) at_top"
   1.704 +      by (rule eventually_ge_at_top)
   1.705 +    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
   1.706 +      by eventually_elim (metis mono bij `P z`)
   1.707 +  qed
   1.708 +qed
   1.709 +
   1.710 +lemma filterlim_at_top_gt:
   1.711 +  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   1.712 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
   1.713 +  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
   1.714 +
   1.715 +lemma filterlim_at_bot: 
   1.716 +  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   1.717 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
   1.718 +  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
   1.719 +
   1.720 +lemma filterlim_at_bot_dense:
   1.721 +  fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
   1.722 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
   1.723 +proof (auto simp add: filterlim_at_bot[of f F])
   1.724 +  fix Z :: 'b
   1.725 +  from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
   1.726 +  assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
   1.727 +  hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
   1.728 +  thus "eventually (\<lambda>x. f x < Z) F"
   1.729 +    apply (rule eventually_mono[rotated])
   1.730 +    using 1 by auto
   1.731 +  next 
   1.732 +    fix Z :: 'b 
   1.733 +    show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
   1.734 +      by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
   1.735 +qed
   1.736 +
   1.737 +lemma filterlim_at_bot_le:
   1.738 +  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   1.739 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
   1.740 +  unfolding filterlim_at_bot
   1.741 +proof safe
   1.742 +  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
   1.743 +  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
   1.744 +    by (auto elim!: eventually_elim1)
   1.745 +qed simp
   1.746 +
   1.747 +lemma filterlim_at_bot_lt:
   1.748 +  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   1.749 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
   1.750 +  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
   1.751 +
   1.752 +
   1.753 +subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
   1.754 +
   1.755 +context begin interpretation lifting_syntax .
   1.756 +
   1.757 +definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
   1.758 +where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
   1.759 +
   1.760 +lemma rel_filter_eventually:
   1.761 +  "rel_filter R F G \<longleftrightarrow> 
   1.762 +  ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
   1.763 +by(simp add: rel_filter_def eventually_def)
   1.764 +
   1.765 +lemma filtermap_id [simp, id_simps]: "filtermap id = id"
   1.766 +by(simp add: fun_eq_iff id_def filtermap_ident)
   1.767 +
   1.768 +lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
   1.769 +using filtermap_id unfolding id_def .
   1.770 +
   1.771 +lemma Quotient_filter [quot_map]:
   1.772 +  assumes Q: "Quotient R Abs Rep T"
   1.773 +  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
   1.774 +unfolding Quotient_alt_def
   1.775 +proof(intro conjI strip)
   1.776 +  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
   1.777 +    unfolding Quotient_alt_def by blast
   1.778 +
   1.779 +  fix F G
   1.780 +  assume "rel_filter T F G"
   1.781 +  thus "filtermap Abs F = G" unfolding filter_eq_iff
   1.782 +    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
   1.783 +next
   1.784 +  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
   1.785 +
   1.786 +  fix F
   1.787 +  show "rel_filter T (filtermap Rep F) F" 
   1.788 +    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
   1.789 +            del: iffI simp add: eventually_filtermap rel_filter_eventually)
   1.790 +qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
   1.791 +         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
   1.792 +
   1.793 +lemma eventually_parametric [transfer_rule]:
   1.794 +  "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
   1.795 +by(simp add: rel_fun_def rel_filter_eventually)
   1.796 +
   1.797 +lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
   1.798 +by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
   1.799 +
   1.800 +lemma rel_filter_mono [relator_mono]:
   1.801 +  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
   1.802 +unfolding rel_filter_eventually[abs_def]
   1.803 +by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
   1.804 +
   1.805 +lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
   1.806 +by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
   1.807 +
   1.808 +lemma is_filter_parametric_aux:
   1.809 +  assumes "is_filter F"
   1.810 +  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   1.811 +  and [transfer_rule]: "((A ===> op =) ===> op =) F G"
   1.812 +  shows "is_filter G"
   1.813 +proof -
   1.814 +  interpret is_filter F by fact
   1.815 +  show ?thesis
   1.816 +  proof
   1.817 +    have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
   1.818 +    thus "G (\<lambda>x. True)" by(simp add: True)
   1.819 +  next
   1.820 +    fix P' Q'
   1.821 +    assume "G P'" "G Q'"
   1.822 +    moreover
   1.823 +    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
   1.824 +    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
   1.825 +    have "F P = G P'" "F Q = G Q'" by transfer_prover+
   1.826 +    ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
   1.827 +    moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
   1.828 +    ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
   1.829 +  next
   1.830 +    fix P' Q'
   1.831 +    assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
   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'" by transfer_prover
   1.836 +    moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
   1.837 +    ultimately have "F Q" by(simp add: mono)
   1.838 +    moreover have "F Q = G Q'" by transfer_prover
   1.839 +    ultimately show "G Q'" by simp
   1.840 +  qed
   1.841 +qed
   1.842 +
   1.843 +lemma is_filter_parametric [transfer_rule]:
   1.844 +  "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
   1.845 +  \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
   1.846 +apply(rule rel_funI)
   1.847 +apply(rule iffI)
   1.848 + apply(erule (3) is_filter_parametric_aux)
   1.849 +apply(erule is_filter_parametric_aux[where A="conversep A"])
   1.850 +apply(auto simp add: rel_fun_def)
   1.851 +done
   1.852 +
   1.853 +lemma left_total_rel_filter [transfer_rule]:
   1.854 +  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   1.855 +  shows "left_total (rel_filter A)"
   1.856 +proof(rule left_totalI)
   1.857 +  fix F :: "'a filter"
   1.858 +  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
   1.859 +  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
   1.860 +    unfolding  bi_total_def by blast
   1.861 +  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
   1.862 +  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
   1.863 +  ultimately have "rel_filter A F (Abs_filter G)"
   1.864 +    by(simp add: rel_filter_eventually eventually_Abs_filter)
   1.865 +  thus "\<exists>G. rel_filter A F G" ..
   1.866 +qed
   1.867 +
   1.868 +lemma right_total_rel_filter [transfer_rule]:
   1.869 +  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
   1.870 +using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
   1.871 +
   1.872 +lemma bi_total_rel_filter [transfer_rule]:
   1.873 +  assumes "bi_total A" "bi_unique A"
   1.874 +  shows "bi_total (rel_filter A)"
   1.875 +unfolding bi_total_alt_def using assms
   1.876 +by(simp add: left_total_rel_filter right_total_rel_filter)
   1.877 +
   1.878 +lemma left_unique_rel_filter [transfer_rule]:
   1.879 +  assumes "left_unique A"
   1.880 +  shows "left_unique (rel_filter A)"
   1.881 +proof(rule left_uniqueI)
   1.882 +  fix F F' G
   1.883 +  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
   1.884 +  show "F = F'"
   1.885 +    unfolding filter_eq_iff
   1.886 +  proof
   1.887 +    fix P :: "'a \<Rightarrow> bool"
   1.888 +    obtain P' where [transfer_rule]: "(A ===> op =) P P'"
   1.889 +      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
   1.890 +    have "eventually P F = eventually P' G" 
   1.891 +      and "eventually P F' = eventually P' G" by transfer_prover+
   1.892 +    thus "eventually P F = eventually P F'" by simp
   1.893 +  qed
   1.894 +qed
   1.895 +
   1.896 +lemma right_unique_rel_filter [transfer_rule]:
   1.897 +  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
   1.898 +using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
   1.899 +
   1.900 +lemma bi_unique_rel_filter [transfer_rule]:
   1.901 +  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
   1.902 +by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
   1.903 +
   1.904 +lemma top_filter_parametric [transfer_rule]:
   1.905 +  "bi_total A \<Longrightarrow> (rel_filter A) top top"
   1.906 +by(simp add: rel_filter_eventually All_transfer)
   1.907 +
   1.908 +lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
   1.909 +by(simp add: rel_filter_eventually rel_fun_def)
   1.910 +
   1.911 +lemma sup_filter_parametric [transfer_rule]:
   1.912 +  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
   1.913 +by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
   1.914 +
   1.915 +lemma Sup_filter_parametric [transfer_rule]:
   1.916 +  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
   1.917 +proof(rule rel_funI)
   1.918 +  fix S T
   1.919 +  assume [transfer_rule]: "rel_set (rel_filter A) S T"
   1.920 +  show "rel_filter A (Sup S) (Sup T)"
   1.921 +    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
   1.922 +qed
   1.923 +
   1.924 +lemma principal_parametric [transfer_rule]:
   1.925 +  "(rel_set A ===> rel_filter A) principal principal"
   1.926 +proof(rule rel_funI)
   1.927 +  fix S S'
   1.928 +  assume [transfer_rule]: "rel_set A S S'"
   1.929 +  show "rel_filter A (principal S) (principal S')"
   1.930 +    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
   1.931 +qed
   1.932 +
   1.933 +context
   1.934 +  fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.935 +  assumes [transfer_rule]: "bi_unique A" 
   1.936 +begin
   1.937 +
   1.938 +lemma le_filter_parametric [transfer_rule]:
   1.939 +  "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
   1.940 +unfolding le_filter_def[abs_def] by transfer_prover
   1.941 +
   1.942 +lemma less_filter_parametric [transfer_rule]:
   1.943 +  "(rel_filter A ===> rel_filter A ===> op =) op < op <"
   1.944 +unfolding less_filter_def[abs_def] by transfer_prover
   1.945 +
   1.946 +context
   1.947 +  assumes [transfer_rule]: "bi_total A"
   1.948 +begin
   1.949 +
   1.950 +lemma Inf_filter_parametric [transfer_rule]:
   1.951 +  "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
   1.952 +unfolding Inf_filter_def[abs_def] by transfer_prover
   1.953 +
   1.954 +lemma inf_filter_parametric [transfer_rule]:
   1.955 +  "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
   1.956 +proof(intro rel_funI)+
   1.957 +  fix F F' G G'
   1.958 +  assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
   1.959 +  have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
   1.960 +  thus "rel_filter A (inf F G) (inf F' G')" by simp
   1.961 +qed
   1.962 +
   1.963 +end
   1.964 +
   1.965 +end
   1.966 +
   1.967 +end
   1.968 +
   1.969 +end
   1.970 \ No newline at end of file
     2.1 --- a/src/HOL/Main.thy	Sun Apr 12 16:04:53 2015 +0200
     2.2 +++ b/src/HOL/Main.thy	Sun Apr 12 11:33:19 2015 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  section {* Main HOL *}
     2.5  
     2.6  theory Main
     2.7 -imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint
     2.8 +imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/NSA/Filter.thy	Sun Apr 12 16:04:53 2015 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,413 +0,0 @@
     3.4 -(*  Title:      HOL/NSA/Filter.thy
     3.5 -    Author:     Jacques D. Fleuriot, University of Cambridge
     3.6 -    Author:     Lawrence C Paulson
     3.7 -    Author:     Brian Huffman
     3.8 -*) 
     3.9 -
    3.10 -section {* Filters and Ultrafilters *}
    3.11 -
    3.12 -theory Filter
    3.13 -imports "~~/src/HOL/Library/Infinite_Set"
    3.14 -begin
    3.15 -
    3.16 -subsection {* Definitions and basic properties *}
    3.17 -
    3.18 -subsubsection {* Filters *}
    3.19 -
    3.20 -locale filter =
    3.21 -  fixes F :: "'a set set"
    3.22 -  assumes UNIV [iff]:  "UNIV \<in> F"
    3.23 -  assumes empty [iff]: "{} \<notin> F"
    3.24 -  assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
    3.25 -  assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
    3.26 -begin
    3.27 -
    3.28 -lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
    3.29 -proof
    3.30 -  assume "A \<in> F" and "- A \<in> F"
    3.31 -  hence "A \<inter> (- A) \<in> F" by (rule Int)
    3.32 -  thus "False" by simp
    3.33 -qed
    3.34 -
    3.35 -lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
    3.36 -by (drule memD, simp)
    3.37 -
    3.38 -lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
    3.39 -by (auto elim: subset intro: Int)
    3.40 -
    3.41 -end
    3.42 -
    3.43 -subsubsection {* Ultrafilters *}
    3.44 -
    3.45 -locale ultrafilter = filter +
    3.46 -  assumes ultra: "A \<in> F \<or> - A \<in> F"
    3.47 -begin
    3.48 -
    3.49 -lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
    3.50 -using ultra [of A] by simp
    3.51 -
    3.52 -lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
    3.53 -by (rule memI, simp)
    3.54 -
    3.55 -lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
    3.56 -by (rule iffI [OF not_memD not_memI])
    3.57 -
    3.58 -lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
    3.59 -by (rule iffI [OF not_memI not_memD])
    3.60 -
    3.61 -lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
    3.62 - apply (rule iffI)
    3.63 -  apply (erule contrapos_pp)
    3.64 -  apply (simp add: Int_iff not_mem_iff)
    3.65 - apply (auto elim: subset)
    3.66 -done
    3.67 -
    3.68 -end
    3.69 -
    3.70 -subsubsection {* Free Ultrafilters *}
    3.71 -
    3.72 -locale freeultrafilter = ultrafilter +
    3.73 -  assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
    3.74 -begin
    3.75 -
    3.76 -lemma finite: "finite A \<Longrightarrow> A \<notin> F"
    3.77 -by (erule contrapos_pn, erule infinite)
    3.78 -
    3.79 -lemma singleton: "{x} \<notin> F"
    3.80 -by (rule finite, simp)
    3.81 -
    3.82 -lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
    3.83 -apply (subst insert_is_Un)
    3.84 -apply (subst Un_iff)
    3.85 -apply (simp add: singleton)
    3.86 -done
    3.87 -
    3.88 -lemma filter: "filter F" ..
    3.89 -
    3.90 -lemma ultrafilter: "ultrafilter F" ..
    3.91 -
    3.92 -end
    3.93 -
    3.94 -subsection {* Collect properties *}
    3.95 -
    3.96 -lemma (in filter) Collect_ex:
    3.97 -  "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
    3.98 -proof
    3.99 -  assume "{n. \<exists>x. P n x} \<in> F"
   3.100 -  hence "{n. P n (SOME x. P n x)} \<in> F"
   3.101 -    by (auto elim: someI subset)
   3.102 -  thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
   3.103 -next
   3.104 -  show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
   3.105 -    by (auto elim: subset)
   3.106 -qed
   3.107 -
   3.108 -lemma (in filter) Collect_conj:
   3.109 -  "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
   3.110 -by (subst Collect_conj_eq, rule Int_iff)
   3.111 -
   3.112 -lemma (in ultrafilter) Collect_not:
   3.113 -  "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
   3.114 -by (subst Collect_neg_eq, rule Compl_iff)
   3.115 -
   3.116 -lemma (in ultrafilter) Collect_disj:
   3.117 -  "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
   3.118 -by (subst Collect_disj_eq, rule Un_iff)
   3.119 -
   3.120 -lemma (in ultrafilter) Collect_all:
   3.121 -  "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
   3.122 -apply (rule Not_eq_iff [THEN iffD1])
   3.123 -apply (simp add: Collect_not [symmetric])
   3.124 -apply (rule Collect_ex)
   3.125 -done
   3.126 -
   3.127 -subsection {* Maximal filter = Ultrafilter *}
   3.128 -
   3.129 -text {*
   3.130 -   A filter F is an ultrafilter iff it is a maximal filter,
   3.131 -   i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
   3.132 -*}
   3.133 -text {*
   3.134 -  Lemmas that shows existence of an extension to what was assumed to
   3.135 -  be a maximal filter. Will be used to derive contradiction in proof of
   3.136 -  property of ultrafilter.
   3.137 -*}
   3.138 -
   3.139 -lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   3.140 -by blast
   3.141 -
   3.142 -lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   3.143 -by blast
   3.144 -
   3.145 -lemma (in filter) extend_filter:
   3.146 -assumes A: "- A \<notin> F"
   3.147 -shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
   3.148 -proof (rule filter.intro)
   3.149 -  show "UNIV \<in> ?X" by blast
   3.150 -next
   3.151 -  show "{} \<notin> ?X"
   3.152 -  proof (clarify)
   3.153 -    fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
   3.154 -    from Af have fA: "f \<subseteq> - A" by blast
   3.155 -    from f fA have "- A \<in> F" by (rule subset)
   3.156 -    with A show "False" by simp
   3.157 -  qed
   3.158 -next
   3.159 -  fix u and v
   3.160 -  assume u: "u \<in> ?X" and v: "v \<in> ?X"
   3.161 -  from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
   3.162 -  from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
   3.163 -  from f g have fg: "f \<inter> g \<in> F" by (rule Int)
   3.164 -  from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
   3.165 -  from fg Afg show "u \<inter> v \<in> ?X" by blast
   3.166 -next
   3.167 -  fix u and v
   3.168 -  assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
   3.169 -  from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
   3.170 -  from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
   3.171 -  from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
   3.172 -  thus "v \<in> ?X" by simp
   3.173 -qed
   3.174 -
   3.175 -lemma (in filter) max_filter_ultrafilter:
   3.176 -assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
   3.177 -shows "ultrafilter_axioms F"
   3.178 -proof (rule ultrafilter_axioms.intro)
   3.179 -  fix A show "A \<in> F \<or> - A \<in> F"
   3.180 -  proof (rule disjCI)
   3.181 -    let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   3.182 -    assume AF: "- A \<notin> F"
   3.183 -    from AF have X: "filter ?X" by (rule extend_filter)
   3.184 -    from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
   3.185 -    have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
   3.186 -    from X FX have "F = ?X" by (rule max)
   3.187 -    with AX show "A \<in> F" by simp
   3.188 -  qed
   3.189 -qed
   3.190 -
   3.191 -lemma (in ultrafilter) max_filter:
   3.192 -assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
   3.193 -proof
   3.194 -  show "F \<subseteq> G" using sub .
   3.195 -  show "G \<subseteq> F"
   3.196 -  proof
   3.197 -    fix A assume A: "A \<in> G"
   3.198 -    from G A have "- A \<notin> G" by (rule filter.memD)
   3.199 -    with sub have B: "- A \<notin> F" by blast
   3.200 -    thus "A \<in> F" by (rule memI)
   3.201 -  qed
   3.202 -qed
   3.203 -
   3.204 -subsection {* Ultrafilter Theorem *}
   3.205 -
   3.206 -text "A local context makes proof of ultrafilter Theorem more modular"
   3.207 -context
   3.208 -  fixes   frechet :: "'a set set"
   3.209 -  and     superfrechet :: "'a set set set"
   3.210 -
   3.211 -  assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
   3.212 -
   3.213 -  defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
   3.214 -  and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
   3.215 -begin
   3.216 -
   3.217 -lemma superfrechetI:
   3.218 -  "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
   3.219 -by (simp add: superfrechet_def)
   3.220 -
   3.221 -lemma superfrechetD1:
   3.222 -  "G \<in> superfrechet \<Longrightarrow> filter G"
   3.223 -by (simp add: superfrechet_def)
   3.224 -
   3.225 -lemma superfrechetD2:
   3.226 -  "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
   3.227 -by (simp add: superfrechet_def)
   3.228 -
   3.229 -text {* A few properties of free filters *}
   3.230 -
   3.231 -lemma filter_cofinite:
   3.232 -assumes inf: "infinite (UNIV :: 'a set)"
   3.233 -shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
   3.234 -proof (rule filter.intro)
   3.235 -  show "UNIV \<in> ?F" by simp
   3.236 -next
   3.237 -  show "{} \<notin> ?F" using inf by simp
   3.238 -next
   3.239 -  fix u v assume "u \<in> ?F" and "v \<in> ?F"
   3.240 -  thus "u \<inter> v \<in> ?F" by simp
   3.241 -next
   3.242 -  fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
   3.243 -  from uv have vu: "- v \<subseteq> - u" by simp
   3.244 -  from u show "v \<in> ?F"
   3.245 -    by (simp add: finite_subset [OF vu])
   3.246 -qed
   3.247 -
   3.248 -text {*
   3.249 -   We prove: 1. Existence of maximal filter i.e. ultrafilter;
   3.250 -             2. Freeness property i.e ultrafilter is free.
   3.251 -             Use a locale to prove various lemmas and then 
   3.252 -             export main result: The ultrafilter Theorem
   3.253 -*}
   3.254 -
   3.255 -lemma filter_frechet: "filter frechet"
   3.256 -by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
   3.257 -
   3.258 -lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
   3.259 -by (rule superfrechetI [OF filter_frechet subset_refl])
   3.260 -
   3.261 -lemma lemma_mem_chain_filter:
   3.262 -  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
   3.263 -by (unfold chains_def superfrechet_def, blast)
   3.264 -
   3.265 -
   3.266 -subsubsection {* Unions of chains of superfrechets *}
   3.267 -
   3.268 -text "In this section we prove that superfrechet is closed
   3.269 -with respect to unions of non-empty chains. We must show
   3.270 -  1) Union of a chain is a filter,
   3.271 -  2) Union of a chain contains frechet.
   3.272 -
   3.273 -Number 2 is trivial, but 1 requires us to prove all the filter rules."
   3.274 -
   3.275 -lemma Union_chain_UNIV:
   3.276 -  "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
   3.277 -proof -
   3.278 -  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   3.279 -  from 2 obtain x where 3: "x \<in> c" by blast
   3.280 -  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   3.281 -  hence "UNIV \<in> x" by (rule filter.UNIV)
   3.282 -  with 3 show "UNIV \<in> \<Union>c" by blast
   3.283 -qed
   3.284 -
   3.285 -lemma Union_chain_empty:
   3.286 -  "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
   3.287 -proof
   3.288 -  assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
   3.289 -  from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
   3.290 -  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   3.291 -  hence "{} \<notin> x" by (rule filter.empty)
   3.292 -  with 4 show "False" by simp
   3.293 -qed
   3.294 -
   3.295 -lemma Union_chain_Int:
   3.296 -  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
   3.297 -proof -
   3.298 -  assume c: "c \<in> chains superfrechet"
   3.299 -  assume "u \<in> \<Union>c"
   3.300 -    then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   3.301 -  assume "v \<in> \<Union>c"
   3.302 -    then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
   3.303 -  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
   3.304 -  with xc yc have xyc: "x \<union> y \<in> c"
   3.305 -    by (auto simp add: Un_absorb1 Un_absorb2)
   3.306 -  with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
   3.307 -  from ux have uxy: "u \<in> x \<union> y" by simp
   3.308 -  from vy have vxy: "v \<in> x \<union> y" by simp
   3.309 -  from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
   3.310 -  with xyc show "u \<inter> v \<in> \<Union>c" ..
   3.311 -qed
   3.312 -
   3.313 -lemma Union_chain_subset:
   3.314 -  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
   3.315 -proof -
   3.316 -  assume c: "c \<in> chains superfrechet"
   3.317 -     and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
   3.318 -  from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   3.319 -  from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
   3.320 -  from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
   3.321 -  with xc show "v \<in> \<Union>c" ..
   3.322 -qed
   3.323 -
   3.324 -lemma Union_chain_filter:
   3.325 -assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
   3.326 -shows "filter (\<Union>c)" 
   3.327 -proof (rule filter.intro)
   3.328 -  show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
   3.329 -next
   3.330 -  show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
   3.331 -next
   3.332 -  fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
   3.333 -  with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
   3.334 -next
   3.335 -  fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
   3.336 -  with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
   3.337 -qed
   3.338 -
   3.339 -lemma lemma_mem_chain_frechet_subset:
   3.340 -  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
   3.341 -by (unfold superfrechet_def chains_def, blast)
   3.342 -
   3.343 -lemma Union_chain_superfrechet:
   3.344 -  "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
   3.345 -proof (rule superfrechetI)
   3.346 -  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   3.347 -  thus "filter (\<Union>c)" by (rule Union_chain_filter)
   3.348 -  from 2 obtain x where 3: "x \<in> c" by blast
   3.349 -  from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
   3.350 -  also from 3 have "x \<subseteq> \<Union>c" by blast
   3.351 -  finally show "frechet \<subseteq> \<Union>c" .
   3.352 -qed
   3.353 -
   3.354 -subsubsection {* Existence of free ultrafilter *}
   3.355 -
   3.356 -lemma max_cofinite_filter_Ex:
   3.357 -  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
   3.358 -proof (rule Zorn_Lemma2, safe)
   3.359 -  fix c assume c: "c \<in> chains superfrechet"
   3.360 -  show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
   3.361 -  proof (cases)
   3.362 -    assume "c = {}"
   3.363 -    with frechet_in_superfrechet show "?U" by blast
   3.364 -  next
   3.365 -    assume A: "c \<noteq> {}"
   3.366 -    from A c have "\<Union>c \<in> superfrechet"
   3.367 -      by (rule Union_chain_superfrechet)
   3.368 -    thus "?U" by blast
   3.369 -  qed
   3.370 -qed
   3.371 -
   3.372 -lemma mem_superfrechet_all_infinite:
   3.373 -  "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
   3.374 -proof
   3.375 -  assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
   3.376 -  from U have fil: "filter U" and fre: "frechet \<subseteq> U"
   3.377 -    by (simp_all add: superfrechet_def)
   3.378 -  from fin have "- A \<in> frechet" by (simp add: frechet_def)
   3.379 -  with fre have cA: "- A \<in> U" by (rule subsetD)
   3.380 -  from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
   3.381 -  with fil show "False" by (simp add: filter.empty)
   3.382 -qed
   3.383 -
   3.384 -text {* There exists a free ultrafilter on any infinite set *}
   3.385 -
   3.386 -lemma freeultrafilter_Ex:
   3.387 -  "\<exists>U::'a set set. freeultrafilter U"
   3.388 -proof -
   3.389 -  from max_cofinite_filter_Ex obtain U
   3.390 -    where U: "U \<in> superfrechet"
   3.391 -      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
   3.392 -  from U have fil: "filter U" by (rule superfrechetD1)
   3.393 -  from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
   3.394 -  have ultra: "ultrafilter_axioms U"
   3.395 -  proof (rule filter.max_filter_ultrafilter [OF fil])
   3.396 -    fix G assume G: "filter G" and UG: "U \<subseteq> G"
   3.397 -    from fre UG have "frechet \<subseteq> G" by simp
   3.398 -    with G have "G \<in> superfrechet" by (rule superfrechetI)
   3.399 -    from this UG show "U = G" by (rule max[symmetric])
   3.400 -  qed
   3.401 -  have free: "freeultrafilter_axioms U"
   3.402 -  proof (rule freeultrafilter_axioms.intro)
   3.403 -    fix A assume "A \<in> U"
   3.404 -    with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   3.405 -  qed
   3.406 -  from fil ultra free have "freeultrafilter U"
   3.407 -    by (rule freeultrafilter.intro [OF ultrafilter.intro])
   3.408 -    (* FIXME: unfold_locales should use chained facts *)
   3.409 -  then show ?thesis ..
   3.410 -qed
   3.411 -
   3.412 -end
   3.413 -
   3.414 -hide_const (open) filter
   3.415 -
   3.416 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/NSA/Free_Ultrafilter.thy	Sun Apr 12 11:33:19 2015 +0200
     4.3 @@ -0,0 +1,413 @@
     4.4 +(*  Title:      HOL/NSA/Free_Ultrafilter.thy
     4.5 +    Author:     Jacques D. Fleuriot, University of Cambridge
     4.6 +    Author:     Lawrence C Paulson
     4.7 +    Author:     Brian Huffman
     4.8 +*) 
     4.9 +
    4.10 +section {* Filters and Ultrafilters *}
    4.11 +
    4.12 +theory Free_Ultrafilter
    4.13 +imports "~~/src/HOL/Library/Infinite_Set"
    4.14 +begin
    4.15 +
    4.16 +subsection {* Definitions and basic properties *}
    4.17 +
    4.18 +subsubsection {* Filters *}
    4.19 +
    4.20 +locale filter =
    4.21 +  fixes F :: "'a set set"
    4.22 +  assumes UNIV [iff]:  "UNIV \<in> F"
    4.23 +  assumes empty [iff]: "{} \<notin> F"
    4.24 +  assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
    4.25 +  assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
    4.26 +begin
    4.27 +
    4.28 +lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
    4.29 +proof
    4.30 +  assume "A \<in> F" and "- A \<in> F"
    4.31 +  hence "A \<inter> (- A) \<in> F" by (rule Int)
    4.32 +  thus "False" by simp
    4.33 +qed
    4.34 +
    4.35 +lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
    4.36 +by (drule memD, simp)
    4.37 +
    4.38 +lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
    4.39 +by (auto elim: subset intro: Int)
    4.40 +
    4.41 +end
    4.42 +
    4.43 +subsubsection {* Ultrafilters *}
    4.44 +
    4.45 +locale ultrafilter = filter +
    4.46 +  assumes ultra: "A \<in> F \<or> - A \<in> F"
    4.47 +begin
    4.48 +
    4.49 +lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
    4.50 +using ultra [of A] by simp
    4.51 +
    4.52 +lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
    4.53 +by (rule memI, simp)
    4.54 +
    4.55 +lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
    4.56 +by (rule iffI [OF not_memD not_memI])
    4.57 +
    4.58 +lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
    4.59 +by (rule iffI [OF not_memI not_memD])
    4.60 +
    4.61 +lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
    4.62 + apply (rule iffI)
    4.63 +  apply (erule contrapos_pp)
    4.64 +  apply (simp add: Int_iff not_mem_iff)
    4.65 + apply (auto elim: subset)
    4.66 +done
    4.67 +
    4.68 +end
    4.69 +
    4.70 +subsubsection {* Free Ultrafilters *}
    4.71 +
    4.72 +locale freeultrafilter = ultrafilter +
    4.73 +  assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
    4.74 +begin
    4.75 +
    4.76 +lemma finite: "finite A \<Longrightarrow> A \<notin> F"
    4.77 +by (erule contrapos_pn, erule infinite)
    4.78 +
    4.79 +lemma singleton: "{x} \<notin> F"
    4.80 +by (rule finite, simp)
    4.81 +
    4.82 +lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
    4.83 +apply (subst insert_is_Un)
    4.84 +apply (subst Un_iff)
    4.85 +apply (simp add: singleton)
    4.86 +done
    4.87 +
    4.88 +lemma filter: "filter F" ..
    4.89 +
    4.90 +lemma ultrafilter: "ultrafilter F" ..
    4.91 +
    4.92 +end
    4.93 +
    4.94 +subsection {* Collect properties *}
    4.95 +
    4.96 +lemma (in filter) Collect_ex:
    4.97 +  "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
    4.98 +proof
    4.99 +  assume "{n. \<exists>x. P n x} \<in> F"
   4.100 +  hence "{n. P n (SOME x. P n x)} \<in> F"
   4.101 +    by (auto elim: someI subset)
   4.102 +  thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
   4.103 +next
   4.104 +  show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
   4.105 +    by (auto elim: subset)
   4.106 +qed
   4.107 +
   4.108 +lemma (in filter) Collect_conj:
   4.109 +  "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
   4.110 +by (subst Collect_conj_eq, rule Int_iff)
   4.111 +
   4.112 +lemma (in ultrafilter) Collect_not:
   4.113 +  "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
   4.114 +by (subst Collect_neg_eq, rule Compl_iff)
   4.115 +
   4.116 +lemma (in ultrafilter) Collect_disj:
   4.117 +  "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
   4.118 +by (subst Collect_disj_eq, rule Un_iff)
   4.119 +
   4.120 +lemma (in ultrafilter) Collect_all:
   4.121 +  "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
   4.122 +apply (rule Not_eq_iff [THEN iffD1])
   4.123 +apply (simp add: Collect_not [symmetric])
   4.124 +apply (rule Collect_ex)
   4.125 +done
   4.126 +
   4.127 +subsection {* Maximal filter = Ultrafilter *}
   4.128 +
   4.129 +text {*
   4.130 +   A filter F is an ultrafilter iff it is a maximal filter,
   4.131 +   i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
   4.132 +*}
   4.133 +text {*
   4.134 +  Lemmas that shows existence of an extension to what was assumed to
   4.135 +  be a maximal filter. Will be used to derive contradiction in proof of
   4.136 +  property of ultrafilter.
   4.137 +*}
   4.138 +
   4.139 +lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   4.140 +by blast
   4.141 +
   4.142 +lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   4.143 +by blast
   4.144 +
   4.145 +lemma (in filter) extend_filter:
   4.146 +assumes A: "- A \<notin> F"
   4.147 +shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
   4.148 +proof (rule filter.intro)
   4.149 +  show "UNIV \<in> ?X" by blast
   4.150 +next
   4.151 +  show "{} \<notin> ?X"
   4.152 +  proof (clarify)
   4.153 +    fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
   4.154 +    from Af have fA: "f \<subseteq> - A" by blast
   4.155 +    from f fA have "- A \<in> F" by (rule subset)
   4.156 +    with A show "False" by simp
   4.157 +  qed
   4.158 +next
   4.159 +  fix u and v
   4.160 +  assume u: "u \<in> ?X" and v: "v \<in> ?X"
   4.161 +  from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
   4.162 +  from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
   4.163 +  from f g have fg: "f \<inter> g \<in> F" by (rule Int)
   4.164 +  from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
   4.165 +  from fg Afg show "u \<inter> v \<in> ?X" by blast
   4.166 +next
   4.167 +  fix u and v
   4.168 +  assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
   4.169 +  from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
   4.170 +  from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
   4.171 +  from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
   4.172 +  thus "v \<in> ?X" by simp
   4.173 +qed
   4.174 +
   4.175 +lemma (in filter) max_filter_ultrafilter:
   4.176 +assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
   4.177 +shows "ultrafilter_axioms F"
   4.178 +proof (rule ultrafilter_axioms.intro)
   4.179 +  fix A show "A \<in> F \<or> - A \<in> F"
   4.180 +  proof (rule disjCI)
   4.181 +    let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   4.182 +    assume AF: "- A \<notin> F"
   4.183 +    from AF have X: "filter ?X" by (rule extend_filter)
   4.184 +    from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
   4.185 +    have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
   4.186 +    from X FX have "F = ?X" by (rule max)
   4.187 +    with AX show "A \<in> F" by simp
   4.188 +  qed
   4.189 +qed
   4.190 +
   4.191 +lemma (in ultrafilter) max_filter:
   4.192 +assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
   4.193 +proof
   4.194 +  show "F \<subseteq> G" using sub .
   4.195 +  show "G \<subseteq> F"
   4.196 +  proof
   4.197 +    fix A assume A: "A \<in> G"
   4.198 +    from G A have "- A \<notin> G" by (rule filter.memD)
   4.199 +    with sub have B: "- A \<notin> F" by blast
   4.200 +    thus "A \<in> F" by (rule memI)
   4.201 +  qed
   4.202 +qed
   4.203 +
   4.204 +subsection {* Ultrafilter Theorem *}
   4.205 +
   4.206 +text "A local context makes proof of ultrafilter Theorem more modular"
   4.207 +context
   4.208 +  fixes   frechet :: "'a set set"
   4.209 +  and     superfrechet :: "'a set set set"
   4.210 +
   4.211 +  assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
   4.212 +
   4.213 +  defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
   4.214 +  and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
   4.215 +begin
   4.216 +
   4.217 +lemma superfrechetI:
   4.218 +  "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
   4.219 +by (simp add: superfrechet_def)
   4.220 +
   4.221 +lemma superfrechetD1:
   4.222 +  "G \<in> superfrechet \<Longrightarrow> filter G"
   4.223 +by (simp add: superfrechet_def)
   4.224 +
   4.225 +lemma superfrechetD2:
   4.226 +  "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
   4.227 +by (simp add: superfrechet_def)
   4.228 +
   4.229 +text {* A few properties of free filters *}
   4.230 +
   4.231 +lemma filter_cofinite:
   4.232 +assumes inf: "infinite (UNIV :: 'a set)"
   4.233 +shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
   4.234 +proof (rule filter.intro)
   4.235 +  show "UNIV \<in> ?F" by simp
   4.236 +next
   4.237 +  show "{} \<notin> ?F" using inf by simp
   4.238 +next
   4.239 +  fix u v assume "u \<in> ?F" and "v \<in> ?F"
   4.240 +  thus "u \<inter> v \<in> ?F" by simp
   4.241 +next
   4.242 +  fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
   4.243 +  from uv have vu: "- v \<subseteq> - u" by simp
   4.244 +  from u show "v \<in> ?F"
   4.245 +    by (simp add: finite_subset [OF vu])
   4.246 +qed
   4.247 +
   4.248 +text {*
   4.249 +   We prove: 1. Existence of maximal filter i.e. ultrafilter;
   4.250 +             2. Freeness property i.e ultrafilter is free.
   4.251 +             Use a locale to prove various lemmas and then 
   4.252 +             export main result: The ultrafilter Theorem
   4.253 +*}
   4.254 +
   4.255 +lemma filter_frechet: "filter frechet"
   4.256 +by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
   4.257 +
   4.258 +lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
   4.259 +by (rule superfrechetI [OF filter_frechet subset_refl])
   4.260 +
   4.261 +lemma lemma_mem_chain_filter:
   4.262 +  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
   4.263 +by (unfold chains_def superfrechet_def, blast)
   4.264 +
   4.265 +
   4.266 +subsubsection {* Unions of chains of superfrechets *}
   4.267 +
   4.268 +text "In this section we prove that superfrechet is closed
   4.269 +with respect to unions of non-empty chains. We must show
   4.270 +  1) Union of a chain is a filter,
   4.271 +  2) Union of a chain contains frechet.
   4.272 +
   4.273 +Number 2 is trivial, but 1 requires us to prove all the filter rules."
   4.274 +
   4.275 +lemma Union_chain_UNIV:
   4.276 +  "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
   4.277 +proof -
   4.278 +  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   4.279 +  from 2 obtain x where 3: "x \<in> c" by blast
   4.280 +  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   4.281 +  hence "UNIV \<in> x" by (rule filter.UNIV)
   4.282 +  with 3 show "UNIV \<in> \<Union>c" by blast
   4.283 +qed
   4.284 +
   4.285 +lemma Union_chain_empty:
   4.286 +  "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
   4.287 +proof
   4.288 +  assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
   4.289 +  from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
   4.290 +  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   4.291 +  hence "{} \<notin> x" by (rule filter.empty)
   4.292 +  with 4 show "False" by simp
   4.293 +qed
   4.294 +
   4.295 +lemma Union_chain_Int:
   4.296 +  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
   4.297 +proof -
   4.298 +  assume c: "c \<in> chains superfrechet"
   4.299 +  assume "u \<in> \<Union>c"
   4.300 +    then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   4.301 +  assume "v \<in> \<Union>c"
   4.302 +    then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
   4.303 +  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
   4.304 +  with xc yc have xyc: "x \<union> y \<in> c"
   4.305 +    by (auto simp add: Un_absorb1 Un_absorb2)
   4.306 +  with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
   4.307 +  from ux have uxy: "u \<in> x \<union> y" by simp
   4.308 +  from vy have vxy: "v \<in> x \<union> y" by simp
   4.309 +  from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
   4.310 +  with xyc show "u \<inter> v \<in> \<Union>c" ..
   4.311 +qed
   4.312 +
   4.313 +lemma Union_chain_subset:
   4.314 +  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
   4.315 +proof -
   4.316 +  assume c: "c \<in> chains superfrechet"
   4.317 +     and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
   4.318 +  from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   4.319 +  from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
   4.320 +  from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
   4.321 +  with xc show "v \<in> \<Union>c" ..
   4.322 +qed
   4.323 +
   4.324 +lemma Union_chain_filter:
   4.325 +assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
   4.326 +shows "filter (\<Union>c)" 
   4.327 +proof (rule filter.intro)
   4.328 +  show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
   4.329 +next
   4.330 +  show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
   4.331 +next
   4.332 +  fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
   4.333 +  with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
   4.334 +next
   4.335 +  fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
   4.336 +  with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
   4.337 +qed
   4.338 +
   4.339 +lemma lemma_mem_chain_frechet_subset:
   4.340 +  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
   4.341 +by (unfold superfrechet_def chains_def, blast)
   4.342 +
   4.343 +lemma Union_chain_superfrechet:
   4.344 +  "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
   4.345 +proof (rule superfrechetI)
   4.346 +  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   4.347 +  thus "filter (\<Union>c)" by (rule Union_chain_filter)
   4.348 +  from 2 obtain x where 3: "x \<in> c" by blast
   4.349 +  from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
   4.350 +  also from 3 have "x \<subseteq> \<Union>c" by blast
   4.351 +  finally show "frechet \<subseteq> \<Union>c" .
   4.352 +qed
   4.353 +
   4.354 +subsubsection {* Existence of free ultrafilter *}
   4.355 +
   4.356 +lemma max_cofinite_filter_Ex:
   4.357 +  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
   4.358 +proof (rule Zorn_Lemma2, safe)
   4.359 +  fix c assume c: "c \<in> chains superfrechet"
   4.360 +  show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
   4.361 +  proof (cases)
   4.362 +    assume "c = {}"
   4.363 +    with frechet_in_superfrechet show "?U" by blast
   4.364 +  next
   4.365 +    assume A: "c \<noteq> {}"
   4.366 +    from A c have "\<Union>c \<in> superfrechet"
   4.367 +      by (rule Union_chain_superfrechet)
   4.368 +    thus "?U" by blast
   4.369 +  qed
   4.370 +qed
   4.371 +
   4.372 +lemma mem_superfrechet_all_infinite:
   4.373 +  "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
   4.374 +proof
   4.375 +  assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
   4.376 +  from U have fil: "filter U" and fre: "frechet \<subseteq> U"
   4.377 +    by (simp_all add: superfrechet_def)
   4.378 +  from fin have "- A \<in> frechet" by (simp add: frechet_def)
   4.379 +  with fre have cA: "- A \<in> U" by (rule subsetD)
   4.380 +  from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
   4.381 +  with fil show "False" by (simp add: filter.empty)
   4.382 +qed
   4.383 +
   4.384 +text {* There exists a free ultrafilter on any infinite set *}
   4.385 +
   4.386 +lemma freeultrafilter_Ex:
   4.387 +  "\<exists>U::'a set set. freeultrafilter U"
   4.388 +proof -
   4.389 +  from max_cofinite_filter_Ex obtain U
   4.390 +    where U: "U \<in> superfrechet"
   4.391 +      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
   4.392 +  from U have fil: "filter U" by (rule superfrechetD1)
   4.393 +  from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
   4.394 +  have ultra: "ultrafilter_axioms U"
   4.395 +  proof (rule filter.max_filter_ultrafilter [OF fil])
   4.396 +    fix G assume G: "filter G" and UG: "U \<subseteq> G"
   4.397 +    from fre UG have "frechet \<subseteq> G" by simp
   4.398 +    with G have "G \<in> superfrechet" by (rule superfrechetI)
   4.399 +    from this UG show "U = G" by (rule max[symmetric])
   4.400 +  qed
   4.401 +  have free: "freeultrafilter_axioms U"
   4.402 +  proof (rule freeultrafilter_axioms.intro)
   4.403 +    fix A assume "A \<in> U"
   4.404 +    with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   4.405 +  qed
   4.406 +  from fil ultra free have "freeultrafilter U"
   4.407 +    by (rule freeultrafilter.intro [OF ultrafilter.intro])
   4.408 +    (* FIXME: unfold_locales should use chained facts *)
   4.409 +  then show ?thesis ..
   4.410 +qed
   4.411 +
   4.412 +end
   4.413 +
   4.414 +hide_const (open) filter
   4.415 +
   4.416 +end
     5.1 --- a/src/HOL/NSA/StarDef.thy	Sun Apr 12 16:04:53 2015 +0200
     5.2 +++ b/src/HOL/NSA/StarDef.thy	Sun Apr 12 11:33:19 2015 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  section {* Construction of Star Types Using Ultrafilters *}
     5.5  
     5.6  theory StarDef
     5.7 -imports Filter
     5.8 +imports Free_Ultrafilter
     5.9  begin
    5.10  
    5.11  subsection {* A Free Ultrafilter over the Naturals *}
     6.1 --- a/src/HOL/Topological_Spaces.thy	Sun Apr 12 16:04:53 2015 +0200
     6.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:33:19 2015 +0200
     6.3 @@ -322,557 +322,6 @@
     6.4      by auto
     6.5  qed
     6.6  
     6.7 -subsection {* Filters *}
     6.8 -
     6.9 -text {*
    6.10 -  This definition also allows non-proper filters.
    6.11 -*}
    6.12 -
    6.13 -locale is_filter =
    6.14 -  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
    6.15 -  assumes True: "F (\<lambda>x. True)"
    6.16 -  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
    6.17 -  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
    6.18 -
    6.19 -typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
    6.20 -proof
    6.21 -  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
    6.22 -qed
    6.23 -
    6.24 -lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
    6.25 -  using Rep_filter [of F] by simp
    6.26 -
    6.27 -lemma Abs_filter_inverse':
    6.28 -  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
    6.29 -  using assms by (simp add: Abs_filter_inverse)
    6.30 -
    6.31 -
    6.32 -subsubsection {* Eventually *}
    6.33 -
    6.34 -definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    6.35 -  where "eventually P F \<longleftrightarrow> Rep_filter F P"
    6.36 -
    6.37 -lemma eventually_Abs_filter:
    6.38 -  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
    6.39 -  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
    6.40 -
    6.41 -lemma filter_eq_iff:
    6.42 -  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
    6.43 -  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
    6.44 -
    6.45 -lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
    6.46 -  unfolding eventually_def
    6.47 -  by (rule is_filter.True [OF is_filter_Rep_filter])
    6.48 -
    6.49 -lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
    6.50 -proof -
    6.51 -  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
    6.52 -  thus "eventually P F" by simp
    6.53 -qed
    6.54 -
    6.55 -lemma eventually_mono:
    6.56 -  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
    6.57 -  unfolding eventually_def
    6.58 -  by (rule is_filter.mono [OF is_filter_Rep_filter])
    6.59 -
    6.60 -lemma eventually_conj:
    6.61 -  assumes P: "eventually (\<lambda>x. P x) F"
    6.62 -  assumes Q: "eventually (\<lambda>x. Q x) F"
    6.63 -  shows "eventually (\<lambda>x. P x \<and> Q x) F"
    6.64 -  using assms unfolding eventually_def
    6.65 -  by (rule is_filter.conj [OF is_filter_Rep_filter])
    6.66 -
    6.67 -lemma eventually_Ball_finite:
    6.68 -  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
    6.69 -  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
    6.70 -using assms by (induct set: finite, simp, simp add: eventually_conj)
    6.71 -
    6.72 -lemma eventually_all_finite:
    6.73 -  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
    6.74 -  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
    6.75 -  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
    6.76 -using eventually_Ball_finite [of UNIV P] assms by simp
    6.77 -
    6.78 -lemma eventually_mp:
    6.79 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    6.80 -  assumes "eventually (\<lambda>x. P x) F"
    6.81 -  shows "eventually (\<lambda>x. Q x) F"
    6.82 -proof (rule eventually_mono)
    6.83 -  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
    6.84 -  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
    6.85 -    using assms by (rule eventually_conj)
    6.86 -qed
    6.87 -
    6.88 -lemma eventually_rev_mp:
    6.89 -  assumes "eventually (\<lambda>x. P x) F"
    6.90 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    6.91 -  shows "eventually (\<lambda>x. Q x) F"
    6.92 -using assms(2) assms(1) by (rule eventually_mp)
    6.93 -
    6.94 -lemma eventually_conj_iff:
    6.95 -  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
    6.96 -  by (auto intro: eventually_conj elim: eventually_rev_mp)
    6.97 -
    6.98 -lemma eventually_elim1:
    6.99 -  assumes "eventually (\<lambda>i. P i) F"
   6.100 -  assumes "\<And>i. P i \<Longrightarrow> Q i"
   6.101 -  shows "eventually (\<lambda>i. Q i) F"
   6.102 -  using assms by (auto elim!: eventually_rev_mp)
   6.103 -
   6.104 -lemma eventually_elim2:
   6.105 -  assumes "eventually (\<lambda>i. P i) F"
   6.106 -  assumes "eventually (\<lambda>i. Q i) F"
   6.107 -  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
   6.108 -  shows "eventually (\<lambda>i. R i) F"
   6.109 -  using assms by (auto elim!: eventually_rev_mp)
   6.110 -
   6.111 -lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   6.112 -  by (auto intro: eventually_mp)
   6.113 -
   6.114 -lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
   6.115 -  by (metis always_eventually)
   6.116 -
   6.117 -lemma eventually_subst:
   6.118 -  assumes "eventually (\<lambda>n. P n = Q n) F"
   6.119 -  shows "eventually P F = eventually Q F" (is "?L = ?R")
   6.120 -proof -
   6.121 -  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   6.122 -      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
   6.123 -    by (auto elim: eventually_elim1)
   6.124 -  then show ?thesis by (auto elim: eventually_elim2)
   6.125 -qed
   6.126 -
   6.127 -ML {*
   6.128 -  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
   6.129 -    let
   6.130 -      val mp_thms = facts RL @{thms eventually_rev_mp}
   6.131 -      val raw_elim_thm =
   6.132 -        (@{thm allI} RS @{thm always_eventually})
   6.133 -        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
   6.134 -        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
   6.135 -      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
   6.136 -      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
   6.137 -    in
   6.138 -      CASES cases (rtac raw_elim_thm i)
   6.139 -    end)
   6.140 -*}
   6.141 -
   6.142 -method_setup eventually_elim = {*
   6.143 -  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
   6.144 -*} "elimination of eventually quantifiers"
   6.145 -
   6.146 -
   6.147 -subsubsection {* Finer-than relation *}
   6.148 -
   6.149 -text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
   6.150 -filter @{term F'}. *}
   6.151 -
   6.152 -instantiation filter :: (type) complete_lattice
   6.153 -begin
   6.154 -
   6.155 -definition le_filter_def:
   6.156 -  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
   6.157 -
   6.158 -definition
   6.159 -  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   6.160 -
   6.161 -definition
   6.162 -  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
   6.163 -
   6.164 -definition
   6.165 -  "bot = Abs_filter (\<lambda>P. True)"
   6.166 -
   6.167 -definition
   6.168 -  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
   6.169 -
   6.170 -definition
   6.171 -  "inf F F' = Abs_filter
   6.172 -      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   6.173 -
   6.174 -definition
   6.175 -  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
   6.176 -
   6.177 -definition
   6.178 -  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
   6.179 -
   6.180 -lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
   6.181 -  unfolding top_filter_def
   6.182 -  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
   6.183 -
   6.184 -lemma eventually_bot [simp]: "eventually P bot"
   6.185 -  unfolding bot_filter_def
   6.186 -  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
   6.187 -
   6.188 -lemma eventually_sup:
   6.189 -  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
   6.190 -  unfolding sup_filter_def
   6.191 -  by (rule eventually_Abs_filter, rule is_filter.intro)
   6.192 -     (auto elim!: eventually_rev_mp)
   6.193 -
   6.194 -lemma eventually_inf:
   6.195 -  "eventually P (inf F F') \<longleftrightarrow>
   6.196 -   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
   6.197 -  unfolding inf_filter_def
   6.198 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
   6.199 -  apply (fast intro: eventually_True)
   6.200 -  apply clarify
   6.201 -  apply (intro exI conjI)
   6.202 -  apply (erule (1) eventually_conj)
   6.203 -  apply (erule (1) eventually_conj)
   6.204 -  apply simp
   6.205 -  apply auto
   6.206 -  done
   6.207 -
   6.208 -lemma eventually_Sup:
   6.209 -  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
   6.210 -  unfolding Sup_filter_def
   6.211 -  apply (rule eventually_Abs_filter, rule is_filter.intro)
   6.212 -  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
   6.213 -  done
   6.214 -
   6.215 -instance proof
   6.216 -  fix F F' F'' :: "'a filter" and S :: "'a filter set"
   6.217 -  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
   6.218 -    by (rule less_filter_def) }
   6.219 -  { show "F \<le> F"
   6.220 -    unfolding le_filter_def by simp }
   6.221 -  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
   6.222 -    unfolding le_filter_def by simp }
   6.223 -  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
   6.224 -    unfolding le_filter_def filter_eq_iff by fast }
   6.225 -  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
   6.226 -    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
   6.227 -  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
   6.228 -    unfolding le_filter_def eventually_inf
   6.229 -    by (auto elim!: eventually_mono intro: eventually_conj) }
   6.230 -  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
   6.231 -    unfolding le_filter_def eventually_sup by simp_all }
   6.232 -  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
   6.233 -    unfolding le_filter_def eventually_sup by simp }
   6.234 -  { assume "F'' \<in> S" thus "Inf S \<le> F''"
   6.235 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   6.236 -  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
   6.237 -    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
   6.238 -  { assume "F \<in> S" thus "F \<le> Sup S"
   6.239 -    unfolding le_filter_def eventually_Sup by simp }
   6.240 -  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
   6.241 -    unfolding le_filter_def eventually_Sup by simp }
   6.242 -  { show "Inf {} = (top::'a filter)"
   6.243 -    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
   6.244 -      (metis (full_types) top_filter_def always_eventually eventually_top) }
   6.245 -  { show "Sup {} = (bot::'a filter)"
   6.246 -    by (auto simp: bot_filter_def Sup_filter_def) }
   6.247 -qed
   6.248 -
   6.249 -end
   6.250 -
   6.251 -lemma filter_leD:
   6.252 -  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
   6.253 -  unfolding le_filter_def by simp
   6.254 -
   6.255 -lemma filter_leI:
   6.256 -  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
   6.257 -  unfolding le_filter_def by simp
   6.258 -
   6.259 -lemma eventually_False:
   6.260 -  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   6.261 -  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
   6.262 -
   6.263 -abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   6.264 -  where "trivial_limit F \<equiv> F = bot"
   6.265 -
   6.266 -lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   6.267 -  by (rule eventually_False [symmetric])
   6.268 -
   6.269 -lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
   6.270 -  by (cases P) (simp_all add: eventually_False)
   6.271 -
   6.272 -lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
   6.273 -proof -
   6.274 -  let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
   6.275 -  
   6.276 -  { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
   6.277 -    proof (rule eventually_Abs_filter is_filter.intro)+
   6.278 -      show "?F (\<lambda>x. True)"
   6.279 -        by (rule exI[of _ "{}"]) (simp add: le_fun_def)
   6.280 -    next
   6.281 -      fix P Q
   6.282 -      assume "?F P" then guess X ..
   6.283 -      moreover
   6.284 -      assume "?F Q" then guess Y ..
   6.285 -      ultimately show "?F (\<lambda>x. P x \<and> Q x)"
   6.286 -        by (intro exI[of _ "X \<union> Y"])
   6.287 -           (auto simp: Inf_union_distrib eventually_inf)
   6.288 -    next
   6.289 -      fix P Q
   6.290 -      assume "?F P" then guess X ..
   6.291 -      moreover assume "\<forall>x. P x \<longrightarrow> Q x"
   6.292 -      ultimately show "?F Q"
   6.293 -        by (intro exI[of _ X]) (auto elim: eventually_elim1)
   6.294 -    qed }
   6.295 -  note eventually_F = this
   6.296 -
   6.297 -  have "Inf B = Abs_filter ?F"
   6.298 -  proof (intro antisym Inf_greatest)
   6.299 -    show "Inf B \<le> Abs_filter ?F"
   6.300 -      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
   6.301 -  next
   6.302 -    fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
   6.303 -      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
   6.304 -  qed
   6.305 -  then show ?thesis
   6.306 -    by (simp add: eventually_F)
   6.307 -qed
   6.308 -
   6.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))"
   6.310 -  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
   6.311 -  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
   6.312 -
   6.313 -lemma Inf_filter_not_bot:
   6.314 -  fixes B :: "'a filter set"
   6.315 -  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
   6.316 -  unfolding trivial_limit_def eventually_Inf[of _ B]
   6.317 -    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
   6.318 -
   6.319 -lemma INF_filter_not_bot:
   6.320 -  fixes F :: "'i \<Rightarrow> 'a filter"
   6.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"
   6.322 -  unfolding trivial_limit_def eventually_INF[of _ B]
   6.323 -    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
   6.324 -
   6.325 -lemma eventually_Inf_base:
   6.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"
   6.327 -  shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
   6.328 -proof (subst eventually_Inf, safe)
   6.329 -  fix X assume "finite X" "X \<subseteq> B"
   6.330 -  then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
   6.331 -  proof induct
   6.332 -    case empty then show ?case
   6.333 -      using `B \<noteq> {}` by auto
   6.334 -  next
   6.335 -    case (insert x X)
   6.336 -    then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
   6.337 -      by auto
   6.338 -    with `insert x X \<subseteq> B` base[of b x] show ?case
   6.339 -      by (auto intro: order_trans)
   6.340 -  qed
   6.341 -  then obtain b where "b \<in> B" "b \<le> Inf X"
   6.342 -    by (auto simp: le_Inf_iff)
   6.343 -  then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
   6.344 -    by (intro bexI[of _ b]) (auto simp: le_filter_def)
   6.345 -qed (auto intro!: exI[of _ "{x}" for x])
   6.346 -
   6.347 -lemma eventually_INF_base:
   6.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>
   6.349 -    eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
   6.350 -  unfolding INF_def by (subst eventually_Inf_base) auto
   6.351 -
   6.352 -
   6.353 -subsubsection {* Map function for filters *}
   6.354 -
   6.355 -definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
   6.356 -  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
   6.357 -
   6.358 -lemma eventually_filtermap:
   6.359 -  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
   6.360 -  unfolding filtermap_def
   6.361 -  apply (rule eventually_Abs_filter)
   6.362 -  apply (rule is_filter.intro)
   6.363 -  apply (auto elim!: eventually_rev_mp)
   6.364 -  done
   6.365 -
   6.366 -lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
   6.367 -  by (simp add: filter_eq_iff eventually_filtermap)
   6.368 -
   6.369 -lemma filtermap_filtermap:
   6.370 -  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
   6.371 -  by (simp add: filter_eq_iff eventually_filtermap)
   6.372 -
   6.373 -lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
   6.374 -  unfolding le_filter_def eventually_filtermap by simp
   6.375 -
   6.376 -lemma filtermap_bot [simp]: "filtermap f bot = bot"
   6.377 -  by (simp add: filter_eq_iff eventually_filtermap)
   6.378 -
   6.379 -lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
   6.380 -  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
   6.381 -
   6.382 -lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
   6.383 -  by (auto simp: le_filter_def eventually_filtermap eventually_inf)
   6.384 -
   6.385 -lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
   6.386 -proof -
   6.387 -  { fix X :: "'c set" assume "finite X"
   6.388 -    then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
   6.389 -    proof induct
   6.390 -      case (insert x X)
   6.391 -      have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
   6.392 -        by (rule order_trans[OF _ filtermap_inf]) simp
   6.393 -      also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
   6.394 -        by (intro inf_mono insert order_refl)
   6.395 -      finally show ?case
   6.396 -        by simp
   6.397 -    qed simp }
   6.398 -  then show ?thesis
   6.399 -    unfolding le_filter_def eventually_filtermap
   6.400 -    by (subst (1 2) eventually_INF) auto
   6.401 -qed
   6.402 -subsubsection {* Standard filters *}
   6.403 -
   6.404 -definition principal :: "'a set \<Rightarrow> 'a filter" where
   6.405 -  "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
   6.406 -
   6.407 -lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
   6.408 -  unfolding principal_def
   6.409 -  by (rule eventually_Abs_filter, rule is_filter.intro) auto
   6.410 -
   6.411 -lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
   6.412 -  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
   6.413 -
   6.414 -lemma principal_UNIV[simp]: "principal UNIV = top"
   6.415 -  by (auto simp: filter_eq_iff eventually_principal)
   6.416 -
   6.417 -lemma principal_empty[simp]: "principal {} = bot"
   6.418 -  by (auto simp: filter_eq_iff eventually_principal)
   6.419 -
   6.420 -lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
   6.421 -  by (auto simp add: filter_eq_iff eventually_principal)
   6.422 -
   6.423 -lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
   6.424 -  by (auto simp: le_filter_def eventually_principal)
   6.425 -
   6.426 -lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
   6.427 -  unfolding le_filter_def eventually_principal
   6.428 -  apply safe
   6.429 -  apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
   6.430 -  apply (auto elim: eventually_elim1)
   6.431 -  done
   6.432 -
   6.433 -lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
   6.434 -  unfolding eq_iff by simp
   6.435 -
   6.436 -lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
   6.437 -  unfolding filter_eq_iff eventually_sup eventually_principal by auto
   6.438 -
   6.439 -lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
   6.440 -  unfolding filter_eq_iff eventually_inf eventually_principal
   6.441 -  by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
   6.442 -
   6.443 -lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
   6.444 -  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
   6.445 -
   6.446 -lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
   6.447 -  by (induct X rule: finite_induct) auto
   6.448 -
   6.449 -lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
   6.450 -  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
   6.451 -
   6.452 -subsubsection {* Order filters *}
   6.453 -
   6.454 -definition at_top :: "('a::order) filter"
   6.455 -  where "at_top = (INF k. principal {k ..})"
   6.456 -
   6.457 -lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
   6.458 -  by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
   6.459 -
   6.460 -lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
   6.461 -  unfolding at_top_def
   6.462 -  by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   6.463 -
   6.464 -lemma eventually_ge_at_top:
   6.465 -  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   6.466 -  unfolding eventually_at_top_linorder by auto
   6.467 -
   6.468 -lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
   6.469 -proof -
   6.470 -  have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
   6.471 -    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
   6.472 -  also have "(INF k. principal {k::'a <..}) = at_top"
   6.473 -    unfolding at_top_def 
   6.474 -    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
   6.475 -  finally show ?thesis .
   6.476 -qed
   6.477 -
   6.478 -lemma eventually_gt_at_top:
   6.479 -  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
   6.480 -  unfolding eventually_at_top_dense by auto
   6.481 -
   6.482 -definition at_bot :: "('a::order) filter"
   6.483 -  where "at_bot = (INF k. principal {.. k})"
   6.484 -
   6.485 -lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
   6.486 -  by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
   6.487 -
   6.488 -lemma eventually_at_bot_linorder:
   6.489 -  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
   6.490 -  unfolding at_bot_def
   6.491 -  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   6.492 -
   6.493 -lemma eventually_le_at_bot:
   6.494 -  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   6.495 -  unfolding eventually_at_bot_linorder by auto
   6.496 -
   6.497 -lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
   6.498 -proof -
   6.499 -  have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
   6.500 -    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   6.501 -  also have "(INF k. principal {..< k::'a}) = at_bot"
   6.502 -    unfolding at_bot_def 
   6.503 -    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
   6.504 -  finally show ?thesis .
   6.505 -qed
   6.506 -
   6.507 -lemma eventually_gt_at_bot:
   6.508 -  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   6.509 -  unfolding eventually_at_bot_dense by auto
   6.510 -
   6.511 -lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
   6.512 -  unfolding trivial_limit_def
   6.513 -  by (metis eventually_at_bot_linorder order_refl)
   6.514 -
   6.515 -lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
   6.516 -  unfolding trivial_limit_def
   6.517 -  by (metis eventually_at_top_linorder order_refl)
   6.518 -
   6.519 -subsection {* Sequentially *}
   6.520 -
   6.521 -abbreviation sequentially :: "nat filter"
   6.522 -  where "sequentially \<equiv> at_top"
   6.523 -
   6.524 -lemma eventually_sequentially:
   6.525 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
   6.526 -  by (rule eventually_at_top_linorder)
   6.527 -
   6.528 -lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
   6.529 -  unfolding filter_eq_iff eventually_sequentially by auto
   6.530 -
   6.531 -lemmas trivial_limit_sequentially = sequentially_bot
   6.532 -
   6.533 -lemma eventually_False_sequentially [simp]:
   6.534 -  "\<not> eventually (\<lambda>n. False) sequentially"
   6.535 -  by (simp add: eventually_False)
   6.536 -
   6.537 -lemma le_sequentially:
   6.538 -  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   6.539 -  by (simp add: at_top_def le_INF_iff le_principal)
   6.540 -
   6.541 -lemma eventually_sequentiallyI:
   6.542 -  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   6.543 -  shows "eventually P sequentially"
   6.544 -using assms by (auto simp: eventually_sequentially)
   6.545 -
   6.546 -lemma eventually_sequentially_seg:
   6.547 -  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   6.548 -  unfolding eventually_sequentially
   6.549 -  apply safe
   6.550 -   apply (rule_tac x="N + k" in exI)
   6.551 -   apply rule
   6.552 -   apply (erule_tac x="n - k" in allE)
   6.553 -   apply auto []
   6.554 -  apply (rule_tac x=N in exI)
   6.555 -  apply auto []
   6.556 -  done
   6.557 -
   6.558  subsubsection {* Topological filters *}
   6.559  
   6.560  definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
   6.561 @@ -1005,104 +454,6 @@
   6.562    "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   6.563    by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   6.564  
   6.565 -subsection {* Limits *}
   6.566 -
   6.567 -definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
   6.568 -  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
   6.569 -
   6.570 -syntax
   6.571 -  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
   6.572 -
   6.573 -translations
   6.574 -  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
   6.575 -
   6.576 -lemma filterlim_iff:
   6.577 -  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
   6.578 -  unfolding filterlim_def le_filter_def eventually_filtermap ..
   6.579 -
   6.580 -lemma filterlim_compose:
   6.581 -  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
   6.582 -  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
   6.583 -
   6.584 -lemma filterlim_mono:
   6.585 -  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
   6.586 -  unfolding filterlim_def by (metis filtermap_mono order_trans)
   6.587 -
   6.588 -lemma filterlim_ident: "LIM x F. x :> F"
   6.589 -  by (simp add: filterlim_def filtermap_ident)
   6.590 -
   6.591 -lemma filterlim_cong:
   6.592 -  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
   6.593 -  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
   6.594 -
   6.595 -lemma filterlim_mono_eventually:
   6.596 -  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
   6.597 -  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
   6.598 -  shows "filterlim f' F' G'"
   6.599 -  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
   6.600 -  apply (rule filterlim_mono[OF _ ord])
   6.601 -  apply fact
   6.602 -  done
   6.603 -
   6.604 -lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
   6.605 -  apply (auto intro!: filtermap_mono) []
   6.606 -  apply (auto simp: le_filter_def eventually_filtermap)
   6.607 -  apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
   6.608 -  apply auto
   6.609 -  done
   6.610 -
   6.611 -lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
   6.612 -  by (simp add: filtermap_mono_strong eq_iff)
   6.613 -
   6.614 -lemma filterlim_principal:
   6.615 -  "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   6.616 -  unfolding filterlim_def eventually_filtermap le_principal ..
   6.617 -
   6.618 -lemma filterlim_inf:
   6.619 -  "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   6.620 -  unfolding filterlim_def by simp
   6.621 -
   6.622 -lemma filterlim_INF:
   6.623 -  "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
   6.624 -  unfolding filterlim_def le_INF_iff ..
   6.625 -
   6.626 -lemma filterlim_INF_INF:
   6.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)"
   6.628 -  unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
   6.629 -
   6.630 -lemma filterlim_base:
   6.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> 
   6.632 -    LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
   6.633 -  by (force intro!: filterlim_INF_INF simp: image_subset_iff)
   6.634 -
   6.635 -lemma filterlim_base_iff: 
   6.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"
   6.637 -  shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
   6.638 -    (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
   6.639 -  unfolding filterlim_INF filterlim_principal
   6.640 -proof (subst eventually_INF_base)
   6.641 -  fix i j assume "i \<in> I" "j \<in> I"
   6.642 -  with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
   6.643 -    by auto
   6.644 -qed (auto simp: eventually_principal `I \<noteq> {}`)
   6.645 -
   6.646 -lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   6.647 -  unfolding filterlim_def filtermap_filtermap ..
   6.648 -
   6.649 -lemma filterlim_sup:
   6.650 -  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
   6.651 -  unfolding filterlim_def filtermap_sup by auto
   6.652 -
   6.653 -lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
   6.654 -  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
   6.655 -
   6.656 -lemma filterlim_sequentially_Suc:
   6.657 -  "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
   6.658 -  unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
   6.659 -
   6.660 -lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
   6.661 -  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
   6.662 -
   6.663  subsubsection {* Tendsto *}
   6.664  
   6.665  abbreviation (in topological_space)
   6.666 @@ -1296,92 +647,6 @@
   6.667  lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   6.668    by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
   6.669  
   6.670 -subsection {* Limits to @{const at_top} and @{const at_bot} *}
   6.671 -
   6.672 -lemma filterlim_at_top:
   6.673 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   6.674 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
   6.675 -  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
   6.676 -
   6.677 -lemma filterlim_at_top_mono:
   6.678 -  "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
   6.679 -    LIM x F. g x :> at_top"
   6.680 -  by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
   6.681 -
   6.682 -lemma filterlim_at_top_dense:
   6.683 -  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
   6.684 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
   6.685 -  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
   6.686 -            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
   6.687 -
   6.688 -lemma filterlim_at_top_ge:
   6.689 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   6.690 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
   6.691 -  unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
   6.692 -
   6.693 -lemma filterlim_at_top_at_top:
   6.694 -  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
   6.695 -  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   6.696 -  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   6.697 -  assumes Q: "eventually Q at_top"
   6.698 -  assumes P: "eventually P at_top"
   6.699 -  shows "filterlim f at_top at_top"
   6.700 -proof -
   6.701 -  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
   6.702 -    unfolding eventually_at_top_linorder by auto
   6.703 -  show ?thesis
   6.704 -  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
   6.705 -    fix z assume "x \<le> z"
   6.706 -    with x have "P z" by auto
   6.707 -    have "eventually (\<lambda>x. g z \<le> x) at_top"
   6.708 -      by (rule eventually_ge_at_top)
   6.709 -    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
   6.710 -      by eventually_elim (metis mono bij `P z`)
   6.711 -  qed
   6.712 -qed
   6.713 -
   6.714 -lemma filterlim_at_top_gt:
   6.715 -  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   6.716 -  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
   6.717 -  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
   6.718 -
   6.719 -lemma filterlim_at_bot: 
   6.720 -  fixes f :: "'a \<Rightarrow> ('b::linorder)"
   6.721 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
   6.722 -  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
   6.723 -
   6.724 -lemma filterlim_at_bot_dense:
   6.725 -  fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
   6.726 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
   6.727 -proof (auto simp add: filterlim_at_bot[of f F])
   6.728 -  fix Z :: 'b
   6.729 -  from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
   6.730 -  assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
   6.731 -  hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
   6.732 -  thus "eventually (\<lambda>x. f x < Z) F"
   6.733 -    apply (rule eventually_mono[rotated])
   6.734 -    using 1 by auto
   6.735 -  next 
   6.736 -    fix Z :: 'b 
   6.737 -    show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
   6.738 -      by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
   6.739 -qed
   6.740 -
   6.741 -lemma filterlim_at_bot_le:
   6.742 -  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
   6.743 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
   6.744 -  unfolding filterlim_at_bot
   6.745 -proof safe
   6.746 -  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
   6.747 -  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
   6.748 -    by (auto elim!: eventually_elim1)
   6.749 -qed simp
   6.750 -
   6.751 -lemma filterlim_at_bot_lt:
   6.752 -  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
   6.753 -  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
   6.754 -  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
   6.755 -
   6.756  lemma filterlim_at_bot_at_right:
   6.757    fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   6.758    assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   6.759 @@ -2936,220 +2201,4 @@
   6.760    qed
   6.761  qed (intro cSUP_least `antimono f`[THEN antimonoD] cInf_lower S)
   6.762  
   6.763 -subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
   6.764 -
   6.765 -context begin interpretation lifting_syntax .
   6.766 -
   6.767 -definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
   6.768 -where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
   6.769 -
   6.770 -lemma rel_filter_eventually:
   6.771 -  "rel_filter R F G \<longleftrightarrow> 
   6.772 -  ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
   6.773 -by(simp add: rel_filter_def eventually_def)
   6.774 -
   6.775 -lemma filtermap_id [simp, id_simps]: "filtermap id = id"
   6.776 -by(simp add: fun_eq_iff id_def filtermap_ident)
   6.777 -
   6.778 -lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
   6.779 -using filtermap_id unfolding id_def .
   6.780 -
   6.781 -lemma Quotient_filter [quot_map]:
   6.782 -  assumes Q: "Quotient R Abs Rep T"
   6.783 -  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
   6.784 -unfolding Quotient_alt_def
   6.785 -proof(intro conjI strip)
   6.786 -  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
   6.787 -    unfolding Quotient_alt_def by blast
   6.788 -
   6.789 -  fix F G
   6.790 -  assume "rel_filter T F G"
   6.791 -  thus "filtermap Abs F = G" unfolding filter_eq_iff
   6.792 -    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
   6.793 -next
   6.794 -  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
   6.795 -
   6.796 -  fix F
   6.797 -  show "rel_filter T (filtermap Rep F) F" 
   6.798 -    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
   6.799 -            del: iffI simp add: eventually_filtermap rel_filter_eventually)
   6.800 -qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
   6.801 -         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
   6.802 -
   6.803 -lemma eventually_parametric [transfer_rule]:
   6.804 -  "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
   6.805 -by(simp add: rel_fun_def rel_filter_eventually)
   6.806 -
   6.807 -lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
   6.808 -by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
   6.809 -
   6.810 -lemma rel_filter_mono [relator_mono]:
   6.811 -  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
   6.812 -unfolding rel_filter_eventually[abs_def]
   6.813 -by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
   6.814 -
   6.815 -lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
   6.816 -by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
   6.817 -
   6.818 -lemma is_filter_parametric_aux:
   6.819 -  assumes "is_filter F"
   6.820 -  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   6.821 -  and [transfer_rule]: "((A ===> op =) ===> op =) F G"
   6.822 -  shows "is_filter G"
   6.823 -proof -
   6.824 -  interpret is_filter F by fact
   6.825 -  show ?thesis
   6.826 -  proof
   6.827 -    have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
   6.828 -    thus "G (\<lambda>x. True)" by(simp add: True)
   6.829 -  next
   6.830 -    fix P' Q'
   6.831 -    assume "G P'" "G Q'"
   6.832 -    moreover
   6.833 -    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
   6.834 -    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
   6.835 -    have "F P = G P'" "F Q = G Q'" by transfer_prover+
   6.836 -    ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
   6.837 -    moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
   6.838 -    ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
   6.839 -  next
   6.840 -    fix P' Q'
   6.841 -    assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
   6.842 -    moreover
   6.843 -    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
   6.844 -    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
   6.845 -    have "F P = G P'" by transfer_prover
   6.846 -    moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
   6.847 -    ultimately have "F Q" by(simp add: mono)
   6.848 -    moreover have "F Q = G Q'" by transfer_prover
   6.849 -    ultimately show "G Q'" by simp
   6.850 -  qed
   6.851 -qed
   6.852 -
   6.853 -lemma is_filter_parametric [transfer_rule]:
   6.854 -  "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
   6.855 -  \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
   6.856 -apply(rule rel_funI)
   6.857 -apply(rule iffI)
   6.858 - apply(erule (3) is_filter_parametric_aux)
   6.859 -apply(erule is_filter_parametric_aux[where A="conversep A"])
   6.860 -apply(auto simp add: rel_fun_def)
   6.861 -done
   6.862 -
   6.863 -lemma left_total_rel_filter [transfer_rule]:
   6.864 -  assumes [transfer_rule]: "bi_total A" "bi_unique A"
   6.865 -  shows "left_total (rel_filter A)"
   6.866 -proof(rule left_totalI)
   6.867 -  fix F :: "'a filter"
   6.868 -  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
   6.869 -  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
   6.870 -    unfolding  bi_total_def by blast
   6.871 -  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
   6.872 -  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
   6.873 -  ultimately have "rel_filter A F (Abs_filter G)"
   6.874 -    by(simp add: rel_filter_eventually eventually_Abs_filter)
   6.875 -  thus "\<exists>G. rel_filter A F G" ..
   6.876 -qed
   6.877 -
   6.878 -lemma right_total_rel_filter [transfer_rule]:
   6.879 -  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
   6.880 -using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
   6.881 -
   6.882 -lemma bi_total_rel_filter [transfer_rule]:
   6.883 -  assumes "bi_total A" "bi_unique A"
   6.884 -  shows "bi_total (rel_filter A)"
   6.885 -unfolding bi_total_alt_def using assms
   6.886 -by(simp add: left_total_rel_filter right_total_rel_filter)
   6.887 -
   6.888 -lemma left_unique_rel_filter [transfer_rule]:
   6.889 -  assumes "left_unique A"
   6.890 -  shows "left_unique (rel_filter A)"
   6.891 -proof(rule left_uniqueI)
   6.892 -  fix F F' G
   6.893 -  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
   6.894 -  show "F = F'"
   6.895 -    unfolding filter_eq_iff
   6.896 -  proof
   6.897 -    fix P :: "'a \<Rightarrow> bool"
   6.898 -    obtain P' where [transfer_rule]: "(A ===> op =) P P'"
   6.899 -      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
   6.900 -    have "eventually P F = eventually P' G" 
   6.901 -      and "eventually P F' = eventually P' G" by transfer_prover+
   6.902 -    thus "eventually P F = eventually P F'" by simp
   6.903 -  qed
   6.904 -qed
   6.905 -
   6.906 -lemma right_unique_rel_filter [transfer_rule]:
   6.907 -  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
   6.908 -using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
   6.909 -
   6.910 -lemma bi_unique_rel_filter [transfer_rule]:
   6.911 -  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
   6.912 -by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
   6.913 -
   6.914 -lemma top_filter_parametric [transfer_rule]:
   6.915 -  "bi_total A \<Longrightarrow> (rel_filter A) top top"
   6.916 -by(simp add: rel_filter_eventually All_transfer)
   6.917 -
   6.918 -lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
   6.919 -by(simp add: rel_filter_eventually rel_fun_def)
   6.920 -
   6.921 -lemma sup_filter_parametric [transfer_rule]:
   6.922 -  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
   6.923 -by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
   6.924 -
   6.925 -lemma Sup_filter_parametric [transfer_rule]:
   6.926 -  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
   6.927 -proof(rule rel_funI)
   6.928 -  fix S T
   6.929 -  assume [transfer_rule]: "rel_set (rel_filter A) S T"
   6.930 -  show "rel_filter A (Sup S) (Sup T)"
   6.931 -    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
   6.932 -qed
   6.933 -
   6.934 -lemma principal_parametric [transfer_rule]:
   6.935 -  "(rel_set A ===> rel_filter A) principal principal"
   6.936 -proof(rule rel_funI)
   6.937 -  fix S S'
   6.938 -  assume [transfer_rule]: "rel_set A S S'"
   6.939 -  show "rel_filter A (principal S) (principal S')"
   6.940 -    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
   6.941 -qed
   6.942 -
   6.943 -context
   6.944 -  fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   6.945 -  assumes [transfer_rule]: "bi_unique A" 
   6.946 -begin
   6.947 -
   6.948 -lemma le_filter_parametric [transfer_rule]:
   6.949 -  "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
   6.950 -unfolding le_filter_def[abs_def] by transfer_prover
   6.951 -
   6.952 -lemma less_filter_parametric [transfer_rule]:
   6.953 -  "(rel_filter A ===> rel_filter A ===> op =) op < op <"
   6.954 -unfolding less_filter_def[abs_def] by transfer_prover
   6.955 -
   6.956 -context
   6.957 -  assumes [transfer_rule]: "bi_total A"
   6.958 -begin
   6.959 -
   6.960 -lemma Inf_filter_parametric [transfer_rule]:
   6.961 -  "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
   6.962 -unfolding Inf_filter_def[abs_def] by transfer_prover
   6.963 -
   6.964 -lemma inf_filter_parametric [transfer_rule]:
   6.965 -  "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
   6.966 -proof(intro rel_funI)+
   6.967 -  fix F F' G G'
   6.968 -  assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
   6.969 -  have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
   6.970 -  thus "rel_filter A (inf F G) (inf F' G')" by simp
   6.971 -qed
   6.972 -
   6.973  end
   6.974 -
   6.975 -end
   6.976 -
   6.977 -end
   6.978 -
   6.979 -end
     7.1 --- a/src/HOL/Transcendental.thy	Sun Apr 12 16:04:53 2015 +0200
     7.2 +++ b/src/HOL/Transcendental.thy	Sun Apr 12 11:33:19 2015 +0200
     7.3 @@ -2321,7 +2321,7 @@
     7.4    shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
     7.5    apply (simp add: powr_def)
     7.6    apply (simp add: tendsto_def)
     7.7 -  apply (simp add: Topological_Spaces.eventually_conj_iff )
     7.8 +  apply (simp add: eventually_conj_iff )
     7.9    apply safe
    7.10    apply (case_tac "0 \<in> S")
    7.11    apply (auto simp: )