# HG changeset patch
# User nipkow
# Date 1428920032 -7200
# Node ID 7c4a2e87e4d0596b1d206ac5338da5fa49b123d0
# Parent  7ff7fdfbb9a079134c21fbdff96d3b7824b554d4# Parent  177d740a0d48a243a6a66765bdedc0c3c6434305
merged

diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/Filter.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Filter.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -0,0 +1,1133 @@
+(*  Title:      HOL/Filter.thy
+    Author:     Brian Huffman
+    Author:     Johannes Hölzl
+*)
+
+section {* Filters on predicates *}
+
+theory Filter
+imports Set_Interval Lifting_Set
+begin
+
+subsection {* Filters *}
+
+text {*
+  This definition also allows non-proper filters.
+*}
+
+locale is_filter =
+  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
+  assumes True: "F (\<lambda>x. True)"
+  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
+  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
+
+typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
+proof
+  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
+qed
+
+lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
+  using Rep_filter [of F] by simp
+
+lemma Abs_filter_inverse':
+  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
+  using assms by (simp add: Abs_filter_inverse)
+
+
+subsubsection {* Eventually *}
+
+definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
+  where "eventually P F \<longleftrightarrow> Rep_filter F P"
+
+syntax (xsymbols)
+  "_eventually"  :: "pttrn => 'a filter => bool => bool"      ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+
+translations
+  "\<forall>\<^sub>Fx in F. P" == "CONST eventually (\<lambda>x. P) F"
+
+lemma eventually_Abs_filter:
+  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
+  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
+
+lemma filter_eq_iff:
+  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
+  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
+
+lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
+  unfolding eventually_def
+  by (rule is_filter.True [OF is_filter_Rep_filter])
+
+lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
+proof -
+  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
+  thus "eventually P F" by simp
+qed
+
+lemma eventuallyI: "(\<And>x. P x) \<Longrightarrow> eventually P F"
+  by (auto intro: always_eventually)
+
+lemma eventually_mono:
+  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
+  unfolding eventually_def
+  by (rule is_filter.mono [OF is_filter_Rep_filter])
+
+lemma eventually_conj:
+  assumes P: "eventually (\<lambda>x. P x) F"
+  assumes Q: "eventually (\<lambda>x. Q x) F"
+  shows "eventually (\<lambda>x. P x \<and> Q x) F"
+  using assms unfolding eventually_def
+  by (rule is_filter.conj [OF is_filter_Rep_filter])
+
+lemma eventually_mp:
+  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+  assumes "eventually (\<lambda>x. P x) F"
+  shows "eventually (\<lambda>x. Q x) F"
+proof (rule eventually_mono)
+  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
+  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
+    using assms by (rule eventually_conj)
+qed
+
+lemma eventually_rev_mp:
+  assumes "eventually (\<lambda>x. P x) F"
+  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+  shows "eventually (\<lambda>x. Q x) F"
+using assms(2) assms(1) by (rule eventually_mp)
+
+lemma eventually_conj_iff:
+  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
+  by (auto intro: eventually_conj elim: eventually_rev_mp)
+
+lemma eventually_elim1:
+  assumes "eventually (\<lambda>i. P i) F"
+  assumes "\<And>i. P i \<Longrightarrow> Q i"
+  shows "eventually (\<lambda>i. Q i) F"
+  using assms by (auto elim!: eventually_rev_mp)
+
+lemma eventually_elim2:
+  assumes "eventually (\<lambda>i. P i) F"
+  assumes "eventually (\<lambda>i. Q i) F"
+  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
+  shows "eventually (\<lambda>i. R i) F"
+  using assms by (auto elim!: eventually_rev_mp)
+
+lemma eventually_ball_finite_distrib:
+  "finite A \<Longrightarrow> (eventually (\<lambda>x. \<forall>y\<in>A. P x y) net) \<longleftrightarrow> (\<forall>y\<in>A. eventually (\<lambda>x. P x y) net)"
+  by (induction A rule: finite_induct) (auto simp: eventually_conj_iff)
+
+lemma eventually_ball_finite:
+  "finite A \<Longrightarrow> \<forall>y\<in>A. eventually (\<lambda>x. P x y) net \<Longrightarrow> eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
+  by (auto simp: eventually_ball_finite_distrib)
+
+lemma eventually_all_finite:
+  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
+  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
+  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
+using eventually_ball_finite [of UNIV P] assms by simp
+
+lemma eventually_ex: "(\<forall>\<^sub>Fx in F. \<exists>y. P x y) \<longleftrightarrow> (\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x))"
+proof
+  assume "\<forall>\<^sub>Fx in F. \<exists>y. P x y"
+  then have "\<forall>\<^sub>Fx in F. P x (SOME y. P x y)"
+    by (auto intro: someI_ex eventually_elim1)
+  then show "\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x)"
+    by auto
+qed (auto intro: eventually_elim1)
+
+lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+  by (auto intro: eventually_mp)
+
+lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
+  by (metis always_eventually)
+
+lemma eventually_subst:
+  assumes "eventually (\<lambda>n. P n = Q n) F"
+  shows "eventually P F = eventually Q F" (is "?L = ?R")
+proof -
+  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
+    by (auto elim: eventually_elim1)
+  then show ?thesis by (auto elim: eventually_elim2)
+qed
+
+subsection \<open> Frequently as dual to eventually \<close>
+
+definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
+  where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
+
+syntax (xsymbols)
+  "_frequently"  :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+
+translations
+  "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
+
+lemma not_frequently_False [simp]: "\<not> (\<exists>\<^sub>Fx in F. False)"
+  by (simp add: frequently_def)
+
+lemma frequently_ex: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> \<exists>x. P x"
+  by (auto simp: frequently_def dest: not_eventuallyD)
+
+lemma frequentlyE: assumes "frequently P F" obtains x where "P x"
+  using frequently_ex[OF assms] by auto
+
+lemma frequently_mp:
+  assumes ev: "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x" and P: "\<exists>\<^sub>Fx in F. P x" shows "\<exists>\<^sub>Fx in F. Q x"
+proof - 
+  from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
+    by (rule eventually_rev_mp) (auto intro!: always_eventually)
+  from eventually_mp[OF this] P show ?thesis
+    by (auto simp: frequently_def)
+qed
+
+lemma frequently_rev_mp:
+  assumes "\<exists>\<^sub>Fx in F. P x"
+  assumes "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x"
+  shows "\<exists>\<^sub>Fx in F. Q x"
+using assms(2) assms(1) by (rule frequently_mp)
+
+lemma frequently_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> frequently P F \<Longrightarrow> frequently Q F"
+  using frequently_mp[of P Q] by (simp add: always_eventually)
+
+lemma frequently_elim1: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> (\<And>i. P i \<Longrightarrow> Q i) \<Longrightarrow> \<exists>\<^sub>Fx in F. Q x"
+  by (metis frequently_mono)
+
+lemma frequently_disj_iff: "(\<exists>\<^sub>Fx in F. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<or> (\<exists>\<^sub>Fx in F. Q x)"
+  by (simp add: frequently_def eventually_conj_iff)
+
+lemma frequently_disj: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> \<exists>\<^sub>Fx in F. Q x \<Longrightarrow> \<exists>\<^sub>Fx in F. P x \<or> Q x"
+  by (simp add: frequently_disj_iff)
+
+lemma frequently_bex_finite_distrib:
+  assumes "finite A" shows "(\<exists>\<^sub>Fx in F. \<exists>y\<in>A. P x y) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>\<^sub>Fx in F. P x y)"
+  using assms by induction (auto simp: frequently_disj_iff)
+
+lemma frequently_bex_finite: "finite A \<Longrightarrow> \<exists>\<^sub>Fx in F. \<exists>y\<in>A. P x y \<Longrightarrow> \<exists>y\<in>A. \<exists>\<^sub>Fx in F. P x y"
+  by (simp add: frequently_bex_finite_distrib)
+
+lemma frequently_all: "(\<exists>\<^sub>Fx in F. \<forall>y. P x y) \<longleftrightarrow> (\<forall>Y. \<exists>\<^sub>Fx in F. P x (Y x))"
+  using eventually_ex[of "\<lambda>x y. \<not> P x y" F] by (simp add: frequently_def)
+
+lemma
+  shows not_eventually: "\<not> eventually P F \<longleftrightarrow> (\<exists>\<^sub>Fx in F. \<not> P x)"
+    and not_frequently: "\<not> frequently P F \<longleftrightarrow> (\<forall>\<^sub>Fx in F. \<not> P x)"
+  by (auto simp: frequently_def)
+
+lemma frequently_imp_iff:
+  "(\<exists>\<^sub>Fx in F. P x \<longrightarrow> Q x) \<longleftrightarrow> (eventually P F \<longrightarrow> frequently Q F)"
+  unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] ..
+
+lemma eventually_frequently_const_simps:
+  "(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
+  "(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
+  "(\<forall>\<^sub>Fx in F. P x \<or> C) \<longleftrightarrow> (\<forall>\<^sub>Fx in F. P x) \<or> C"
+  "(\<forall>\<^sub>Fx in F. C \<or> P x) \<longleftrightarrow> C \<or> (\<forall>\<^sub>Fx in F. P x)"
+  "(\<forall>\<^sub>Fx in F. P x \<longrightarrow> C) \<longleftrightarrow> ((\<exists>\<^sub>Fx in F. P x) \<longrightarrow> C)"
+  "(\<forall>\<^sub>Fx in F. C \<longrightarrow> P x) \<longleftrightarrow> (C \<longrightarrow> (\<forall>\<^sub>Fx in F. P x))"
+  by (cases C; simp add: not_frequently)+
+
+lemmas eventually_frequently_simps = 
+  eventually_frequently_const_simps
+  not_eventually
+  eventually_conj_iff
+  eventually_ball_finite_distrib
+  eventually_ex
+  not_frequently
+  frequently_disj_iff
+  frequently_bex_finite_distrib
+  frequently_all
+  frequently_imp_iff
+
+ML {*
+  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
+    let
+      val mp_thms = facts RL @{thms eventually_rev_mp}
+      val raw_elim_thm =
+        (@{thm allI} RS @{thm always_eventually})
+        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
+        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
+      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
+      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
+    in
+      CASES cases (rtac raw_elim_thm i)
+    end)
+*}
+
+method_setup eventually_elim = {*
+  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
+*} "elimination of eventually quantifiers"
+
+subsubsection {* Finer-than relation *}
+
+text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
+filter @{term F'}. *}
+
+instantiation filter :: (type) complete_lattice
+begin
+
+definition le_filter_def:
+  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
+
+definition
+  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
+
+definition
+  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
+
+definition
+  "bot = Abs_filter (\<lambda>P. True)"
+
+definition
+  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
+
+definition
+  "inf F F' = Abs_filter
+      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+
+definition
+  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
+
+definition
+  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
+
+lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
+  unfolding top_filter_def
+  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
+
+lemma eventually_bot [simp]: "eventually P bot"
+  unfolding bot_filter_def
+  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
+
+lemma eventually_sup:
+  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
+  unfolding sup_filter_def
+  by (rule eventually_Abs_filter, rule is_filter.intro)
+     (auto elim!: eventually_rev_mp)
+
+lemma eventually_inf:
+  "eventually P (inf F F') \<longleftrightarrow>
+   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+  unfolding inf_filter_def
+  apply (rule eventually_Abs_filter, rule is_filter.intro)
+  apply (fast intro: eventually_True)
+  apply clarify
+  apply (intro exI conjI)
+  apply (erule (1) eventually_conj)
+  apply (erule (1) eventually_conj)
+  apply simp
+  apply auto
+  done
+
+lemma eventually_Sup:
+  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
+  unfolding Sup_filter_def
+  apply (rule eventually_Abs_filter, rule is_filter.intro)
+  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
+  done
+
+instance proof
+  fix F F' F'' :: "'a filter" and S :: "'a filter set"
+  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
+    by (rule less_filter_def) }
+  { show "F \<le> F"
+    unfolding le_filter_def by simp }
+  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
+    unfolding le_filter_def by simp }
+  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
+    unfolding le_filter_def filter_eq_iff by fast }
+  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
+    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
+  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
+    unfolding le_filter_def eventually_inf
+    by (auto elim!: eventually_mono intro: eventually_conj) }
+  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
+    unfolding le_filter_def eventually_sup by simp_all }
+  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
+    unfolding le_filter_def eventually_sup by simp }
+  { assume "F'' \<in> S" thus "Inf S \<le> F''"
+    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
+    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+  { assume "F \<in> S" thus "F \<le> Sup S"
+    unfolding le_filter_def eventually_Sup by simp }
+  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
+    unfolding le_filter_def eventually_Sup by simp }
+  { show "Inf {} = (top::'a filter)"
+    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
+      (metis (full_types) top_filter_def always_eventually eventually_top) }
+  { show "Sup {} = (bot::'a filter)"
+    by (auto simp: bot_filter_def Sup_filter_def) }
+qed
+
+end
+
+lemma filter_leD:
+  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
+  unfolding le_filter_def by simp
+
+lemma filter_leI:
+  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
+  unfolding le_filter_def by simp
+
+lemma eventually_False:
+  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
+  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
+
+lemma eventually_frequently: "F \<noteq> bot \<Longrightarrow> eventually P F \<Longrightarrow> frequently P F"
+  using eventually_conj[of P F "\<lambda>x. \<not> P x"]
+  by (auto simp add: frequently_def eventually_False)
+
+lemma eventually_const_iff: "eventually (\<lambda>x. P) F \<longleftrightarrow> P \<or> F = bot"
+  by (cases P) (auto simp: eventually_False)
+
+lemma eventually_const[simp]: "F \<noteq> bot \<Longrightarrow> eventually (\<lambda>x. P) F \<longleftrightarrow> P"
+  by (simp add: eventually_const_iff)
+
+lemma frequently_const_iff: "frequently (\<lambda>x. P) F \<longleftrightarrow> P \<and> F \<noteq> bot"
+  by (simp add: frequently_def eventually_const_iff)
+
+lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
+  by (simp add: frequently_const_iff)
+
+abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
+  where "trivial_limit F \<equiv> F = bot"
+
+lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
+  by (rule eventually_False [symmetric])
+
+lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
+proof -
+  let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
+  
+  { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
+    proof (rule eventually_Abs_filter is_filter.intro)+
+      show "?F (\<lambda>x. True)"
+        by (rule exI[of _ "{}"]) (simp add: le_fun_def)
+    next
+      fix P Q
+      assume "?F P" then guess X ..
+      moreover
+      assume "?F Q" then guess Y ..
+      ultimately show "?F (\<lambda>x. P x \<and> Q x)"
+        by (intro exI[of _ "X \<union> Y"])
+           (auto simp: Inf_union_distrib eventually_inf)
+    next
+      fix P Q
+      assume "?F P" then guess X ..
+      moreover assume "\<forall>x. P x \<longrightarrow> Q x"
+      ultimately show "?F Q"
+        by (intro exI[of _ X]) (auto elim: eventually_elim1)
+    qed }
+  note eventually_F = this
+
+  have "Inf B = Abs_filter ?F"
+  proof (intro antisym Inf_greatest)
+    show "Inf B \<le> Abs_filter ?F"
+      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
+  next
+    fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
+      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
+  qed
+  then show ?thesis
+    by (simp add: eventually_F)
+qed
+
+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))"
+  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
+  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
+
+lemma Inf_filter_not_bot:
+  fixes B :: "'a filter set"
+  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
+  unfolding trivial_limit_def eventually_Inf[of _ B]
+    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
+
+lemma INF_filter_not_bot:
+  fixes F :: "'i \<Rightarrow> 'a filter"
+  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"
+  unfolding trivial_limit_def eventually_INF[of _ B]
+    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
+
+lemma eventually_Inf_base:
+  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"
+  shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
+proof (subst eventually_Inf, safe)
+  fix X assume "finite X" "X \<subseteq> B"
+  then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
+  proof induct
+    case empty then show ?case
+      using `B \<noteq> {}` by auto
+  next
+    case (insert x X)
+    then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
+      by auto
+    with `insert x X \<subseteq> B` base[of b x] show ?case
+      by (auto intro: order_trans)
+  qed
+  then obtain b where "b \<in> B" "b \<le> Inf X"
+    by (auto simp: le_Inf_iff)
+  then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
+    by (intro bexI[of _ b]) (auto simp: le_filter_def)
+qed (auto intro!: exI[of _ "{x}" for x])
+
+lemma eventually_INF_base:
+  "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>
+    eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
+  unfolding INF_def by (subst eventually_Inf_base) auto
+
+
+subsubsection {* Map function for filters *}
+
+definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
+  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
+
+lemma eventually_filtermap:
+  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
+  unfolding filtermap_def
+  apply (rule eventually_Abs_filter)
+  apply (rule is_filter.intro)
+  apply (auto elim!: eventually_rev_mp)
+  done
+
+lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
+  by (simp add: filter_eq_iff eventually_filtermap)
+
+lemma filtermap_filtermap:
+  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
+  by (simp add: filter_eq_iff eventually_filtermap)
+
+lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
+  unfolding le_filter_def eventually_filtermap by simp
+
+lemma filtermap_bot [simp]: "filtermap f bot = bot"
+  by (simp add: filter_eq_iff eventually_filtermap)
+
+lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
+  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
+
+lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
+  by (auto simp: le_filter_def eventually_filtermap eventually_inf)
+
+lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
+proof -
+  { fix X :: "'c set" assume "finite X"
+    then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
+    proof induct
+      case (insert x X)
+      have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
+        by (rule order_trans[OF _ filtermap_inf]) simp
+      also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
+        by (intro inf_mono insert order_refl)
+      finally show ?case
+        by simp
+    qed simp }
+  then show ?thesis
+    unfolding le_filter_def eventually_filtermap
+    by (subst (1 2) eventually_INF) auto
+qed
+subsubsection {* Standard filters *}
+
+definition principal :: "'a set \<Rightarrow> 'a filter" where
+  "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
+
+lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
+  unfolding principal_def
+  by (rule eventually_Abs_filter, rule is_filter.intro) auto
+
+lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
+  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
+
+lemma principal_UNIV[simp]: "principal UNIV = top"
+  by (auto simp: filter_eq_iff eventually_principal)
+
+lemma principal_empty[simp]: "principal {} = bot"
+  by (auto simp: filter_eq_iff eventually_principal)
+
+lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
+  by (auto simp add: filter_eq_iff eventually_principal)
+
+lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
+  by (auto simp: le_filter_def eventually_principal)
+
+lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
+  unfolding le_filter_def eventually_principal
+  apply safe
+  apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
+  apply (auto elim: eventually_elim1)
+  done
+
+lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
+  unfolding eq_iff by simp
+
+lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
+  unfolding filter_eq_iff eventually_sup eventually_principal by auto
+
+lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
+  unfolding filter_eq_iff eventually_inf eventually_principal
+  by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
+
+lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
+  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
+
+lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
+  by (induct X rule: finite_induct) auto
+
+lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
+  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
+
+subsubsection {* Order filters *}
+
+definition at_top :: "('a::order) filter"
+  where "at_top = (INF k. principal {k ..})"
+
+lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
+  by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
+
+lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
+  unfolding at_top_def
+  by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+
+lemma eventually_ge_at_top:
+  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
+  unfolding eventually_at_top_linorder by auto
+
+lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
+proof -
+  have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
+    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+  also have "(INF k. principal {k::'a <..}) = at_top"
+    unfolding at_top_def 
+    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
+  finally show ?thesis .
+qed
+
+lemma eventually_gt_at_top:
+  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
+  unfolding eventually_at_top_dense by auto
+
+definition at_bot :: "('a::order) filter"
+  where "at_bot = (INF k. principal {.. k})"
+
+lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
+  by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
+
+lemma eventually_at_bot_linorder:
+  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
+  unfolding at_bot_def
+  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+
+lemma eventually_le_at_bot:
+  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
+  unfolding eventually_at_bot_linorder by auto
+
+lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
+proof -
+  have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
+    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
+  also have "(INF k. principal {..< k::'a}) = at_bot"
+    unfolding at_bot_def 
+    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
+  finally show ?thesis .
+qed
+
+lemma eventually_gt_at_bot:
+  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
+  unfolding eventually_at_bot_dense by auto
+
+lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
+  unfolding trivial_limit_def
+  by (metis eventually_at_bot_linorder order_refl)
+
+lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
+  unfolding trivial_limit_def
+  by (metis eventually_at_top_linorder order_refl)
+
+subsection {* Sequentially *}
+
+abbreviation sequentially :: "nat filter"
+  where "sequentially \<equiv> at_top"
+
+lemma eventually_sequentially:
+  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
+  by (rule eventually_at_top_linorder)
+
+lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
+  unfolding filter_eq_iff eventually_sequentially by auto
+
+lemmas trivial_limit_sequentially = sequentially_bot
+
+lemma eventually_False_sequentially [simp]:
+  "\<not> eventually (\<lambda>n. False) sequentially"
+  by (simp add: eventually_False)
+
+lemma le_sequentially:
+  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
+  by (simp add: at_top_def le_INF_iff le_principal)
+
+lemma eventually_sequentiallyI:
+  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
+  shows "eventually P sequentially"
+using assms by (auto simp: eventually_sequentially)
+
+lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
+  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
+
+lemma eventually_sequentially_seg: "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
+  using eventually_sequentially_Suc[of "\<lambda>n. P (n + k)" for k] by (induction k) auto
+
+subsection \<open> The cofinite filter \<close>
+
+definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
+
+abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
+  "Inf_many P \<equiv> frequently P cofinite"
+
+abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
+  "Alm_all P \<equiv> eventually P cofinite"
+
+notation (xsymbols)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
+  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
+
+notation (HTML output)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
+  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
+
+lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
+  unfolding cofinite_def
+proof (rule eventually_Abs_filter, rule is_filter.intro)
+  fix P Q :: "'a \<Rightarrow> bool" assume "finite {x. \<not> P x}" "finite {x. \<not> Q x}"
+  from finite_UnI[OF this] show "finite {x. \<not> (P x \<and> Q x)}"
+    by (rule rev_finite_subset) auto
+next
+  fix P Q :: "'a \<Rightarrow> bool" assume P: "finite {x. \<not> P x}" and *: "\<forall>x. P x \<longrightarrow> Q x"
+  from * show "finite {x. \<not> Q x}"
+    by (intro finite_subset[OF _ P]) auto
+qed simp
+
+lemma frequently_cofinite: "frequently P cofinite \<longleftrightarrow> \<not> finite {x. P x}"
+  by (simp add: frequently_def eventually_cofinite)
+
+lemma cofinite_bot[simp]: "cofinite = (bot::'a filter) \<longleftrightarrow> finite (UNIV :: 'a set)"
+  unfolding trivial_limit_def eventually_cofinite by simp
+
+lemma cofinite_eq_sequentially: "cofinite = sequentially"
+  unfolding filter_eq_iff eventually_sequentially eventually_cofinite
+proof safe
+  fix P :: "nat \<Rightarrow> bool" assume [simp]: "finite {x. \<not> P x}"
+  show "\<exists>N. \<forall>n\<ge>N. P n"
+  proof cases
+    assume "{x. \<not> P x} \<noteq> {}" then show ?thesis
+      by (intro exI[of _ "Suc (Max {x. \<not> P x})"]) (auto simp: Suc_le_eq)
+  qed auto
+next
+  fix P :: "nat \<Rightarrow> bool" and N :: nat assume "\<forall>n\<ge>N. P n"
+  then have "{x. \<not> P x} \<subseteq> {..< N}"
+    by (auto simp: not_le)
+  then show "finite {x. \<not> P x}"
+    by (blast intro: finite_subset)
+qed
+
+subsection {* Limits *}
+
+definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
+  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
+
+syntax
+  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
+
+translations
+  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
+
+lemma filterlim_iff:
+  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
+  unfolding filterlim_def le_filter_def eventually_filtermap ..
+
+lemma filterlim_compose:
+  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
+  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
+
+lemma filterlim_mono:
+  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
+  unfolding filterlim_def by (metis filtermap_mono order_trans)
+
+lemma filterlim_ident: "LIM x F. x :> F"
+  by (simp add: filterlim_def filtermap_ident)
+
+lemma filterlim_cong:
+  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
+  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
+
+lemma filterlim_mono_eventually:
+  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
+  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
+  shows "filterlim f' F' G'"
+  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
+  apply (rule filterlim_mono[OF _ ord])
+  apply fact
+  done
+
+lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
+  apply (auto intro!: filtermap_mono) []
+  apply (auto simp: le_filter_def eventually_filtermap)
+  apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
+  apply auto
+  done
+
+lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
+  by (simp add: filtermap_mono_strong eq_iff)
+
+lemma filterlim_principal:
+  "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
+  unfolding filterlim_def eventually_filtermap le_principal ..
+
+lemma filterlim_inf:
+  "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
+  unfolding filterlim_def by simp
+
+lemma filterlim_INF:
+  "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
+  unfolding filterlim_def le_INF_iff ..
+
+lemma filterlim_INF_INF:
+  "(\<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)"
+  unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
+
+lemma filterlim_base:
+  "(\<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> 
+    LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
+  by (force intro!: filterlim_INF_INF simp: image_subset_iff)
+
+lemma filterlim_base_iff: 
+  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"
+  shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
+    (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
+  unfolding filterlim_INF filterlim_principal
+proof (subst eventually_INF_base)
+  fix i j assume "i \<in> I" "j \<in> I"
+  with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
+    by auto
+qed (auto simp: eventually_principal `I \<noteq> {}`)
+
+lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
+  unfolding filterlim_def filtermap_filtermap ..
+
+lemma filterlim_sup:
+  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
+  unfolding filterlim_def filtermap_sup by auto
+
+lemma filterlim_sequentially_Suc:
+  "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
+  unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
+
+lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
+  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
+
+
+subsection {* Limits to @{const at_top} and @{const at_bot} *}
+
+lemma filterlim_at_top:
+  fixes f :: "'a \<Rightarrow> ('b::linorder)"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
+  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
+
+lemma filterlim_at_top_mono:
+  "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
+    LIM x F. g x :> at_top"
+  by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
+
+lemma filterlim_at_top_dense:
+  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
+  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
+            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
+
+lemma filterlim_at_top_ge:
+  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
+  unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
+
+lemma filterlim_at_top_at_top:
+  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
+  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
+  assumes Q: "eventually Q at_top"
+  assumes P: "eventually P at_top"
+  shows "filterlim f at_top at_top"
+proof -
+  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
+    unfolding eventually_at_top_linorder by auto
+  show ?thesis
+  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
+    fix z assume "x \<le> z"
+    with x have "P z" by auto
+    have "eventually (\<lambda>x. g z \<le> x) at_top"
+      by (rule eventually_ge_at_top)
+    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
+      by eventually_elim (metis mono bij `P z`)
+  qed
+qed
+
+lemma filterlim_at_top_gt:
+  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
+  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
+
+lemma filterlim_at_bot: 
+  fixes f :: "'a \<Rightarrow> ('b::linorder)"
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
+  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
+
+lemma filterlim_at_bot_dense:
+  fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
+proof (auto simp add: filterlim_at_bot[of f F])
+  fix Z :: 'b
+  from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
+  assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
+  hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
+  thus "eventually (\<lambda>x. f x < Z) F"
+    apply (rule eventually_mono[rotated])
+    using 1 by auto
+  next 
+    fix Z :: 'b 
+    show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
+      by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
+qed
+
+lemma filterlim_at_bot_le:
+  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
+  unfolding filterlim_at_bot
+proof safe
+  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
+  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
+    by (auto elim!: eventually_elim1)
+qed simp
+
+lemma filterlim_at_bot_lt:
+  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
+  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
+  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
+
+
+subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
+
+context begin interpretation lifting_syntax .
+
+definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
+where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
+
+lemma rel_filter_eventually:
+  "rel_filter R F G \<longleftrightarrow> 
+  ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
+by(simp add: rel_filter_def eventually_def)
+
+lemma filtermap_id [simp, id_simps]: "filtermap id = id"
+by(simp add: fun_eq_iff id_def filtermap_ident)
+
+lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
+using filtermap_id unfolding id_def .
+
+lemma Quotient_filter [quot_map]:
+  assumes Q: "Quotient R Abs Rep T"
+  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
+unfolding Quotient_alt_def
+proof(intro conjI strip)
+  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
+    unfolding Quotient_alt_def by blast
+
+  fix F G
+  assume "rel_filter T F G"
+  thus "filtermap Abs F = G" unfolding filter_eq_iff
+    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
+next
+  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
+
+  fix F
+  show "rel_filter T (filtermap Rep F) F" 
+    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
+            del: iffI simp add: eventually_filtermap rel_filter_eventually)
+qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
+         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
+
+lemma eventually_parametric [transfer_rule]:
+  "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
+by(simp add: rel_fun_def rel_filter_eventually)
+
+lemma frequently_parametric [transfer_rule]:
+  "((A ===> op =) ===> rel_filter A ===> op =) frequently frequently"
+  unfolding frequently_def[abs_def] by transfer_prover
+
+lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
+by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
+
+lemma rel_filter_mono [relator_mono]:
+  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
+unfolding rel_filter_eventually[abs_def]
+by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
+
+lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
+by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+
+lemma is_filter_parametric_aux:
+  assumes "is_filter F"
+  assumes [transfer_rule]: "bi_total A" "bi_unique A"
+  and [transfer_rule]: "((A ===> op =) ===> op =) F G"
+  shows "is_filter G"
+proof -
+  interpret is_filter F by fact
+  show ?thesis
+  proof
+    have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
+    thus "G (\<lambda>x. True)" by(simp add: True)
+  next
+    fix P' Q'
+    assume "G P'" "G Q'"
+    moreover
+    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
+    have "F P = G P'" "F Q = G Q'" by transfer_prover+
+    ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
+    moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
+    ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
+  next
+    fix P' Q'
+    assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
+    moreover
+    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
+    have "F P = G P'" by transfer_prover
+    moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
+    ultimately have "F Q" by(simp add: mono)
+    moreover have "F Q = G Q'" by transfer_prover
+    ultimately show "G Q'" by simp
+  qed
+qed
+
+lemma is_filter_parametric [transfer_rule]:
+  "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
+  \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
+apply(rule rel_funI)
+apply(rule iffI)
+ apply(erule (3) is_filter_parametric_aux)
+apply(erule is_filter_parametric_aux[where A="conversep A"])
+apply(auto simp add: rel_fun_def)
+done
+
+lemma left_total_rel_filter [transfer_rule]:
+  assumes [transfer_rule]: "bi_total A" "bi_unique A"
+  shows "left_total (rel_filter A)"
+proof(rule left_totalI)
+  fix F :: "'a filter"
+  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
+  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
+    unfolding  bi_total_def by blast
+  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
+  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
+  ultimately have "rel_filter A F (Abs_filter G)"
+    by(simp add: rel_filter_eventually eventually_Abs_filter)
+  thus "\<exists>G. rel_filter A F G" ..
+qed
+
+lemma right_total_rel_filter [transfer_rule]:
+  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
+using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
+
+lemma bi_total_rel_filter [transfer_rule]:
+  assumes "bi_total A" "bi_unique A"
+  shows "bi_total (rel_filter A)"
+unfolding bi_total_alt_def using assms
+by(simp add: left_total_rel_filter right_total_rel_filter)
+
+lemma left_unique_rel_filter [transfer_rule]:
+  assumes "left_unique A"
+  shows "left_unique (rel_filter A)"
+proof(rule left_uniqueI)
+  fix F F' G
+  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
+  show "F = F'"
+    unfolding filter_eq_iff
+  proof
+    fix P :: "'a \<Rightarrow> bool"
+    obtain P' where [transfer_rule]: "(A ===> op =) P P'"
+      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
+    have "eventually P F = eventually P' G" 
+      and "eventually P F' = eventually P' G" by transfer_prover+
+    thus "eventually P F = eventually P F'" by simp
+  qed
+qed
+
+lemma right_unique_rel_filter [transfer_rule]:
+  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
+using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
+
+lemma bi_unique_rel_filter [transfer_rule]:
+  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
+by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
+
+lemma top_filter_parametric [transfer_rule]:
+  "bi_total A \<Longrightarrow> (rel_filter A) top top"
+by(simp add: rel_filter_eventually All_transfer)
+
+lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
+by(simp add: rel_filter_eventually rel_fun_def)
+
+lemma sup_filter_parametric [transfer_rule]:
+  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
+by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
+
+lemma Sup_filter_parametric [transfer_rule]:
+  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
+proof(rule rel_funI)
+  fix S T
+  assume [transfer_rule]: "rel_set (rel_filter A) S T"
+  show "rel_filter A (Sup S) (Sup T)"
+    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
+qed
+
+lemma principal_parametric [transfer_rule]:
+  "(rel_set A ===> rel_filter A) principal principal"
+proof(rule rel_funI)
+  fix S S'
+  assume [transfer_rule]: "rel_set A S S'"
+  show "rel_filter A (principal S) (principal S')"
+    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
+qed
+
+context
+  fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+  assumes [transfer_rule]: "bi_unique A" 
+begin
+
+lemma le_filter_parametric [transfer_rule]:
+  "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
+unfolding le_filter_def[abs_def] by transfer_prover
+
+lemma less_filter_parametric [transfer_rule]:
+  "(rel_filter A ===> rel_filter A ===> op =) op < op <"
+unfolding less_filter_def[abs_def] by transfer_prover
+
+context
+  assumes [transfer_rule]: "bi_total A"
+begin
+
+lemma Inf_filter_parametric [transfer_rule]:
+  "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
+unfolding Inf_filter_def[abs_def] by transfer_prover
+
+lemma inf_filter_parametric [transfer_rule]:
+  "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
+proof(intro rel_funI)+
+  fix F F' G G'
+  assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
+  have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
+  thus "rel_filter A (inf F G) (inf F' G')" by simp
+qed
+
+end
+
+end
+
+end
+
+end
\ No newline at end of file
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -12,38 +12,6 @@
 
 default_sort type
 
-lemma MOST_INFM:
-  assumes inf: "infinite (UNIV::'a set)"
-  shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
-  unfolding Alm_all_def Inf_many_def
-  apply (auto simp add: Collect_neg_eq)
-  apply (drule (1) finite_UnI)
-  apply (simp add: Compl_partition2 inf)
-  done
-
-lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
-by (rule MOST_inj [OF _ inj_Suc])
-
-lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
-unfolding MOST_nat
-apply (clarify, rule_tac x="Suc m" in exI, clarify)
-apply (erule Suc_lessE, simp)
-done
-
-lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
-by (rule iffI [OF MOST_SucD MOST_SucI])
-
-lemma INFM_finite_Bex_distrib:
-  "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
-by (induct set: finite, simp, simp add: INFM_disj_distrib)
-
-lemma MOST_finite_Ball_distrib:
-  "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
-by (induct set: finite, simp, simp add: MOST_conj_distrib)
-
-lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
-unfolding MOST_nat_le by fast
-
 subsection {* Eventually constant sequences *}
 
 definition
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/HOLCF/Plain_HOLCF.thy
--- a/src/HOL/HOLCF/Plain_HOLCF.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -12,4 +12,6 @@
   Basic HOLCF concepts and types; does not include definition packages.
 *}
 
+hide_const (open) Filter.principal
+
 end
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -67,36 +67,22 @@
   infinite.
 *}
 
-lemma finite_nat_bounded: assumes S: "finite (S::nat set)" shows "\<exists>k. S \<subseteq> {..<k}"
-proof cases
-  assume "S \<noteq> {}" with Max_less_iff[OF S this] show ?thesis
-    by auto
-qed simp
+lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
+  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
+  by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
+
+lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
+  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
+  by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
 
 lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
-  by (auto intro: finite_nat_bounded dest: finite_subset)
+  using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
 
-lemma finite_nat_iff_bounded_le:
-  "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})"  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?lhs
-  then obtain k where "S \<subseteq> {..<k}"
-    by (blast dest: finite_nat_bounded)
-  then have "S \<subseteq> {..k}" by auto
-  then show ?rhs ..
-next
-  assume ?rhs
-  then obtain k where "S \<subseteq> {..k}" ..
-  then show "finite S"
-    by (rule finite_subset) simp
-qed
+lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
+  using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
 
-lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)"
-  unfolding finite_nat_iff_bounded_le by (auto simp: subset_eq not_le)
-
-lemma infinite_nat_iff_unbounded_le:
-  "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)"
-  unfolding finite_nat_iff_bounded by (auto simp: subset_eq not_less)
+lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
+  by (simp add: finite_nat_iff_bounded)
 
 text {*
   For a set of natural numbers to be infinite, it is enough to know
@@ -104,25 +90,9 @@
   number that is an element of the set.
 *}
 
-lemma unbounded_k_infinite:
-  assumes k: "\<forall>m. k < m \<longrightarrow> (\<exists>n. m < n \<and> n \<in> S)"
-  shows "infinite (S::nat set)"
-proof -
-  {
-    fix m have "\<exists>n. m < n \<and> n \<in> S"
-    proof (cases "k < m")
-      case True
-      with k show ?thesis by blast
-    next
-      case False
-      from k obtain n where "Suc k < n \<and> n \<in> S" by auto
-      with False have "m < n \<and> n \<in> S" by auto
-      then show ?thesis ..
-    qed
-  }
-  then show ?thesis
-    by (auto simp add: infinite_nat_iff_unbounded)
-qed
+lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
+  by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
+            not_less_iff_gr_or_eq sup.bounded_iff)
 
 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   by simp
@@ -178,181 +148,106 @@
   we introduce corresponding binders and their proof rules.
 *}
 
-definition Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10)
-  where "Inf_many P \<longleftrightarrow> infinite {x. P x}"
-
-definition Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10)
-  where "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)"
-
-notation (xsymbols)
-  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
-  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
-
-notation (HTML output)
-  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
-  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
-
-lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
-  unfolding Inf_many_def ..
-
-lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
-  unfolding Alm_all_def Inf_many_def by simp
-
-(* legacy name *)
-lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
-
-lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
-  unfolding Alm_all_def not_not ..
-
-lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
-  unfolding Alm_all_def not_not ..
+(* The following two lemmas are available as filter-rules, but not in the simp-set *)
+lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
+lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
 
 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
-  unfolding Inf_many_def by simp
+  by (simp add: frequently_const_iff)
 
 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
-  unfolding Alm_all_def by simp
-
-lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
-  apply (erule contrapos_pp)
-  apply simp
-  done
-
-lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
-  by simp
-
-lemma INFM_E:
-  assumes "INFM x. P x"
-  obtains x where "P x"
-  using INFM_EX [OF assms] by (rule exE)
-
-lemma MOST_I:
-  assumes "\<And>x. P x"
-  shows "MOST x. P x"
-  using assms by simp
+  by (simp add: eventually_const_iff)
 
-lemma INFM_mono:
-  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
-  shows "\<exists>\<^sub>\<infinity>x. Q x"
-proof -
-  from inf have "infinite {x. P x}" unfolding Inf_many_def .
-  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
-  ultimately show ?thesis
-    using Inf_many_def infinite_super by blast
-qed
-
-lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
-  unfolding Alm_all_def by (blast intro: INFM_mono)
-
-lemma INFM_disj_distrib:
-  "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
-  unfolding Inf_many_def by (simp add: Collect_disj_eq)
-
-lemma INFM_imp_distrib:
-  "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
-  by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
+lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
+  by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
 
-lemma MOST_conj_distrib:
-  "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
-  unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
-
-lemma MOST_conjI:
-  "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
-  by (simp add: MOST_conj_distrib)
-
-lemma INFM_conjI:
-  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
-  unfolding MOST_iff_cofinite INFM_iff_infinite
-  apply (drule (1) Diff_infinite_finite)
-  apply (simp add: Collect_conj_eq Collect_neg_eq)
-  done
+lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
+  by (auto intro: eventually_rev_mp eventually_elim1)
 
-lemma MOST_rev_mp:
-  assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
-  shows "\<forall>\<^sub>\<infinity>x. Q x"
-proof -
-  have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
-    using assms by (rule MOST_conjI)
-  thus ?thesis by (rule MOST_mono) simp
-qed
-
-lemma MOST_imp_iff:
-  assumes "MOST x. P x"
-  shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
-proof
-  assume "MOST x. P x \<longrightarrow> Q x"
-  with assms show "MOST x. Q x" by (rule MOST_rev_mp)
-next
-  assume "MOST x. Q x"
-  then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
-qed
-
-lemma INFM_MOST_simps [simp]:
-  "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
-  "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
-  "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
-  "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
-  "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
-  "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
-  unfolding Alm_all_def Inf_many_def
-  by (simp_all add: Collect_conj_eq)
+lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
+  by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
 
 text {* Properties of quantifiers with injective functions. *}
 
 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
-  unfolding INFM_iff_infinite
-  apply clarify
-  apply (drule (1) finite_vimageI)
-  apply simp
-  done
+  using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
 
 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
-  unfolding MOST_iff_cofinite
-  apply (drule (1) finite_vimageI)
-  apply simp
-  done
+  using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
 
 text {* Properties of quantifiers with singletons. *}
 
 lemma not_INFM_eq [simp]:
   "\<not> (INFM x. x = a)"
   "\<not> (INFM x. a = x)"
-  unfolding INFM_iff_infinite by simp_all
+  unfolding frequently_cofinite by simp_all
 
 lemma MOST_neq [simp]:
   "MOST x. x \<noteq> a"
   "MOST x. a \<noteq> x"
-  unfolding MOST_iff_cofinite by simp_all
+  unfolding eventually_cofinite by simp_all
 
 lemma INFM_neq [simp]:
   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
-  unfolding INFM_iff_infinite by simp_all
+  unfolding frequently_cofinite by simp_all
 
 lemma MOST_eq [simp]:
   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
-  unfolding MOST_iff_cofinite by simp_all
+  unfolding eventually_cofinite by simp_all
 
 lemma MOST_eq_imp:
   "MOST x. x = a \<longrightarrow> P x"
   "MOST x. a = x \<longrightarrow> P x"
-  unfolding MOST_iff_cofinite by simp_all
+  unfolding eventually_cofinite by simp_all
 
 text {* Properties of quantifiers over the naturals. *}
 
-lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> P n)"
-  by (simp add: Inf_many_def infinite_nat_iff_unbounded)
+lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
+  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
+
+lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
+  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
+
+lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
+  by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
 
-lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> P n)"
-  by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
+lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
+  by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
+
+lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
+  by (simp add: eventually_frequently)
+
+lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
+  by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
 
-lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m < n \<longrightarrow> P n)"
-  by (simp add: Alm_all_def INFM_nat)
+lemma
+  shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
+    and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
+  by (simp_all add: MOST_Suc_iff)
+
+lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
+  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
 
-lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m \<le> n \<longrightarrow> P n)"
-  by (simp add: Alm_all_def INFM_nat_le)
-
+(* legacy names *)
+lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
+lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
+lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
+lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
+lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
+lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
+lemma INFM_mono: "\<exists>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<exists>\<^sub>\<infinity>x. Q x" by (fact frequently_elim1)
+lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_elim1)
+lemma INFM_disj_distrib: "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)" by (fact frequently_disj_iff)
+lemma MOST_rev_mp: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_rev_mp)
+lemma MOST_conj_distrib: "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)" by (fact eventually_conj_iff)
+lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
+lemma INFM_finite_Bex_distrib: "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" by (fact frequently_bex_finite_distrib)
+lemma MOST_finite_Ball_distrib: "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" by (fact eventually_ball_finite_distrib)
+lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
+lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
+lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
 
 subsection "Enumeration of an Infinite Set"
 
@@ -360,6 +255,11 @@
   The set's element type must be wellordered (e.g. the natural numbers).
 *}
 
+text \<open>
+  Could be generalized to
+    @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
+\<close>
+
 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
 where
   enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
@@ -368,7 +268,7 @@
 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   by simp
 
-lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
+lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
   apply (induct n arbitrary: S)
    apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
   apply simp
@@ -382,13 +282,13 @@
    apply (rule order_le_neq_trans)
     apply (simp add: enumerate_0 Least_le enumerate_in_set)
    apply (simp only: enumerate_Suc')
-   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
+   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
     apply (blast intro: sym)
    apply (simp add: enumerate_in_set del: Diff_iff)
   apply (simp add: enumerate_Suc')
   done
 
-lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
+lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   apply (erule less_Suc_induct)
   apply (auto intro: enumerate_step)
   done
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -50,9 +50,6 @@
   "tl (x ## xs) = xs"
   by (simp add: cCons_def)
 
-lemma MOST_SucD: "(\<forall>\<^sub>\<infinity> n. P (Suc n)) \<Longrightarrow> (\<forall>\<^sub>\<infinity> n. P n)"
-  by (auto simp: MOST_nat) (metis Suc_lessE)
-
 subsection {* Definition of type @{text poly} *}
 
 typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
@@ -501,9 +498,9 @@
 
 lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n + coeff q n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
-  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n + coeff q n = 0"
-    by simp
+proof -
+  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
+    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
 qed
 
 lemma coeff_add [simp]:
@@ -527,9 +524,9 @@
 
 lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n - coeff q n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
-  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n - coeff q n = 0"
-    by simp
+proof -
+  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
+    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
 qed
 
 lemma coeff_diff [simp]:
@@ -551,9 +548,9 @@
 
 lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p n. - coeff p n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0])
-  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> - coeff p n = 0"
-    by simp
+proof -
+  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
+    using MOST_coeff_eq_0 by simp
 qed
 
 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
@@ -707,11 +704,9 @@
 
 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>a p n. a * coeff p n"
-proof (intro MOST_nat[THEN iffD2] exI allI impI) 
-  fix a :: 'a and p :: "'a poly" and i
-  assume "degree p < i"
-  then show "a * coeff p i = 0"
-    by (simp add: coeff_eq_0)
+proof -
+  fix a :: 'a and p :: "'a poly" show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
+    using MOST_coeff_eq_0[of p] by eventually_elim simp
 qed
 
 lemma coeff_smult [simp]:
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/Main.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -1,7 +1,7 @@
 section {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint
+imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
 begin
 
 text {*
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -3331,10 +3331,8 @@
   have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   proof (intro allI impI)
     fix B assume "finite B" "B \<subseteq> Z"
-    with `finite B` ev_Z have "eventually (\<lambda>x. \<forall>b\<in>B. x \<in> b) F"
-      by (auto intro!: eventually_Ball_finite)
-    with F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
-      by eventually_elim auto
+    with `finite B` ev_Z F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
+      by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)
     with F show "U \<inter> \<Inter>B \<noteq> {}"
       by (intro notI) (simp add: eventually_False)
   qed
@@ -7506,7 +7504,7 @@
   then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
     unfolding continuous_on_eq_continuous_within
     by (intro continuous_dist ballI continuous_within_compose)
-       (auto intro!:  continuous_fst continuous_snd continuous_within_id simp: image_image)
+       (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
 
   obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
     using continuous_attains_inf[OF D cont] by auto
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/NSA/Filter.thy
--- a/src/HOL/NSA/Filter.thy	Mon Apr 13 10:36:06 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,413 +0,0 @@
-(*  Title:      HOL/NSA/Filter.thy
-    Author:     Jacques D. Fleuriot, University of Cambridge
-    Author:     Lawrence C Paulson
-    Author:     Brian Huffman
-*) 
-
-section {* Filters and Ultrafilters *}
-
-theory Filter
-imports "~~/src/HOL/Library/Infinite_Set"
-begin
-
-subsection {* Definitions and basic properties *}
-
-subsubsection {* Filters *}
-
-locale filter =
-  fixes F :: "'a set set"
-  assumes UNIV [iff]:  "UNIV \<in> F"
-  assumes empty [iff]: "{} \<notin> F"
-  assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
-  assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
-begin
-
-lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
-proof
-  assume "A \<in> F" and "- A \<in> F"
-  hence "A \<inter> (- A) \<in> F" by (rule Int)
-  thus "False" by simp
-qed
-
-lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
-by (drule memD, simp)
-
-lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
-by (auto elim: subset intro: Int)
-
-end
-
-subsubsection {* Ultrafilters *}
-
-locale ultrafilter = filter +
-  assumes ultra: "A \<in> F \<or> - A \<in> F"
-begin
-
-lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
-using ultra [of A] by simp
-
-lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
-by (rule memI, simp)
-
-lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
-by (rule iffI [OF not_memD not_memI])
-
-lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
-by (rule iffI [OF not_memI not_memD])
-
-lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
- apply (rule iffI)
-  apply (erule contrapos_pp)
-  apply (simp add: Int_iff not_mem_iff)
- apply (auto elim: subset)
-done
-
-end
-
-subsubsection {* Free Ultrafilters *}
-
-locale freeultrafilter = ultrafilter +
-  assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
-begin
-
-lemma finite: "finite A \<Longrightarrow> A \<notin> F"
-by (erule contrapos_pn, erule infinite)
-
-lemma singleton: "{x} \<notin> F"
-by (rule finite, simp)
-
-lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
-apply (subst insert_is_Un)
-apply (subst Un_iff)
-apply (simp add: singleton)
-done
-
-lemma filter: "filter F" ..
-
-lemma ultrafilter: "ultrafilter F" ..
-
-end
-
-subsection {* Collect properties *}
-
-lemma (in filter) Collect_ex:
-  "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
-proof
-  assume "{n. \<exists>x. P n x} \<in> F"
-  hence "{n. P n (SOME x. P n x)} \<in> F"
-    by (auto elim: someI subset)
-  thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
-next
-  show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
-    by (auto elim: subset)
-qed
-
-lemma (in filter) Collect_conj:
-  "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
-by (subst Collect_conj_eq, rule Int_iff)
-
-lemma (in ultrafilter) Collect_not:
-  "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
-by (subst Collect_neg_eq, rule Compl_iff)
-
-lemma (in ultrafilter) Collect_disj:
-  "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
-by (subst Collect_disj_eq, rule Un_iff)
-
-lemma (in ultrafilter) Collect_all:
-  "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
-apply (rule Not_eq_iff [THEN iffD1])
-apply (simp add: Collect_not [symmetric])
-apply (rule Collect_ex)
-done
-
-subsection {* Maximal filter = Ultrafilter *}
-
-text {*
-   A filter F is an ultrafilter iff it is a maximal filter,
-   i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
-*}
-text {*
-  Lemmas that shows existence of an extension to what was assumed to
-  be a maximal filter. Will be used to derive contradiction in proof of
-  property of ultrafilter.
-*}
-
-lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
-by blast
-
-lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
-by blast
-
-lemma (in filter) extend_filter:
-assumes A: "- A \<notin> F"
-shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
-proof (rule filter.intro)
-  show "UNIV \<in> ?X" by blast
-next
-  show "{} \<notin> ?X"
-  proof (clarify)
-    fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
-    from Af have fA: "f \<subseteq> - A" by blast
-    from f fA have "- A \<in> F" by (rule subset)
-    with A show "False" by simp
-  qed
-next
-  fix u and v
-  assume u: "u \<in> ?X" and v: "v \<in> ?X"
-  from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
-  from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
-  from f g have fg: "f \<inter> g \<in> F" by (rule Int)
-  from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
-  from fg Afg show "u \<inter> v \<in> ?X" by blast
-next
-  fix u and v
-  assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
-  from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
-  from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
-  from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
-  thus "v \<in> ?X" by simp
-qed
-
-lemma (in filter) max_filter_ultrafilter:
-assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
-shows "ultrafilter_axioms F"
-proof (rule ultrafilter_axioms.intro)
-  fix A show "A \<in> F \<or> - A \<in> F"
-  proof (rule disjCI)
-    let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
-    assume AF: "- A \<notin> F"
-    from AF have X: "filter ?X" by (rule extend_filter)
-    from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
-    have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
-    from X FX have "F = ?X" by (rule max)
-    with AX show "A \<in> F" by simp
-  qed
-qed
-
-lemma (in ultrafilter) max_filter:
-assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
-proof
-  show "F \<subseteq> G" using sub .
-  show "G \<subseteq> F"
-  proof
-    fix A assume A: "A \<in> G"
-    from G A have "- A \<notin> G" by (rule filter.memD)
-    with sub have B: "- A \<notin> F" by blast
-    thus "A \<in> F" by (rule memI)
-  qed
-qed
-
-subsection {* Ultrafilter Theorem *}
-
-text "A local context makes proof of ultrafilter Theorem more modular"
-context
-  fixes   frechet :: "'a set set"
-  and     superfrechet :: "'a set set set"
-
-  assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
-
-  defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
-  and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
-begin
-
-lemma superfrechetI:
-  "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
-by (simp add: superfrechet_def)
-
-lemma superfrechetD1:
-  "G \<in> superfrechet \<Longrightarrow> filter G"
-by (simp add: superfrechet_def)
-
-lemma superfrechetD2:
-  "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
-by (simp add: superfrechet_def)
-
-text {* A few properties of free filters *}
-
-lemma filter_cofinite:
-assumes inf: "infinite (UNIV :: 'a set)"
-shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
-proof (rule filter.intro)
-  show "UNIV \<in> ?F" by simp
-next
-  show "{} \<notin> ?F" using inf by simp
-next
-  fix u v assume "u \<in> ?F" and "v \<in> ?F"
-  thus "u \<inter> v \<in> ?F" by simp
-next
-  fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
-  from uv have vu: "- v \<subseteq> - u" by simp
-  from u show "v \<in> ?F"
-    by (simp add: finite_subset [OF vu])
-qed
-
-text {*
-   We prove: 1. Existence of maximal filter i.e. ultrafilter;
-             2. Freeness property i.e ultrafilter is free.
-             Use a locale to prove various lemmas and then 
-             export main result: The ultrafilter Theorem
-*}
-
-lemma filter_frechet: "filter frechet"
-by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
-
-lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
-by (rule superfrechetI [OF filter_frechet subset_refl])
-
-lemma lemma_mem_chain_filter:
-  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
-by (unfold chains_def superfrechet_def, blast)
-
-
-subsubsection {* Unions of chains of superfrechets *}
-
-text "In this section we prove that superfrechet is closed
-with respect to unions of non-empty chains. We must show
-  1) Union of a chain is a filter,
-  2) Union of a chain contains frechet.
-
-Number 2 is trivial, but 1 requires us to prove all the filter rules."
-
-lemma Union_chain_UNIV:
-  "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
-proof -
-  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
-  from 2 obtain x where 3: "x \<in> c" by blast
-  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
-  hence "UNIV \<in> x" by (rule filter.UNIV)
-  with 3 show "UNIV \<in> \<Union>c" by blast
-qed
-
-lemma Union_chain_empty:
-  "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
-proof
-  assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
-  from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
-  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
-  hence "{} \<notin> x" by (rule filter.empty)
-  with 4 show "False" by simp
-qed
-
-lemma Union_chain_Int:
-  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
-proof -
-  assume c: "c \<in> chains superfrechet"
-  assume "u \<in> \<Union>c"
-    then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
-  assume "v \<in> \<Union>c"
-    then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
-  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
-  with xc yc have xyc: "x \<union> y \<in> c"
-    by (auto simp add: Un_absorb1 Un_absorb2)
-  with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
-  from ux have uxy: "u \<in> x \<union> y" by simp
-  from vy have vxy: "v \<in> x \<union> y" by simp
-  from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
-  with xyc show "u \<inter> v \<in> \<Union>c" ..
-qed
-
-lemma Union_chain_subset:
-  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
-proof -
-  assume c: "c \<in> chains superfrechet"
-     and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
-  from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
-  from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
-  from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
-  with xc show "v \<in> \<Union>c" ..
-qed
-
-lemma Union_chain_filter:
-assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
-shows "filter (\<Union>c)" 
-proof (rule filter.intro)
-  show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
-next
-  show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
-next
-  fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
-  with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
-next
-  fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
-  with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
-qed
-
-lemma lemma_mem_chain_frechet_subset:
-  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
-by (unfold superfrechet_def chains_def, blast)
-
-lemma Union_chain_superfrechet:
-  "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
-proof (rule superfrechetI)
-  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
-  thus "filter (\<Union>c)" by (rule Union_chain_filter)
-  from 2 obtain x where 3: "x \<in> c" by blast
-  from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
-  also from 3 have "x \<subseteq> \<Union>c" by blast
-  finally show "frechet \<subseteq> \<Union>c" .
-qed
-
-subsubsection {* Existence of free ultrafilter *}
-
-lemma max_cofinite_filter_Ex:
-  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
-proof (rule Zorn_Lemma2, safe)
-  fix c assume c: "c \<in> chains superfrechet"
-  show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
-  proof (cases)
-    assume "c = {}"
-    with frechet_in_superfrechet show "?U" by blast
-  next
-    assume A: "c \<noteq> {}"
-    from A c have "\<Union>c \<in> superfrechet"
-      by (rule Union_chain_superfrechet)
-    thus "?U" by blast
-  qed
-qed
-
-lemma mem_superfrechet_all_infinite:
-  "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
-proof
-  assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
-  from U have fil: "filter U" and fre: "frechet \<subseteq> U"
-    by (simp_all add: superfrechet_def)
-  from fin have "- A \<in> frechet" by (simp add: frechet_def)
-  with fre have cA: "- A \<in> U" by (rule subsetD)
-  from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
-  with fil show "False" by (simp add: filter.empty)
-qed
-
-text {* There exists a free ultrafilter on any infinite set *}
-
-lemma freeultrafilter_Ex:
-  "\<exists>U::'a set set. freeultrafilter U"
-proof -
-  from max_cofinite_filter_Ex obtain U
-    where U: "U \<in> superfrechet"
-      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
-  from U have fil: "filter U" by (rule superfrechetD1)
-  from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
-  have ultra: "ultrafilter_axioms U"
-  proof (rule filter.max_filter_ultrafilter [OF fil])
-    fix G assume G: "filter G" and UG: "U \<subseteq> G"
-    from fre UG have "frechet \<subseteq> G" by simp
-    with G have "G \<in> superfrechet" by (rule superfrechetI)
-    from this UG show "U = G" by (rule max[symmetric])
-  qed
-  have free: "freeultrafilter_axioms U"
-  proof (rule freeultrafilter_axioms.intro)
-    fix A assume "A \<in> U"
-    with U show "infinite A" by (rule mem_superfrechet_all_infinite)
-  qed
-  from fil ultra free have "freeultrafilter U"
-    by (rule freeultrafilter.intro [OF ultrafilter.intro])
-    (* FIXME: unfold_locales should use chained facts *)
-  then show ?thesis ..
-qed
-
-end
-
-hide_const (open) filter
-
-end
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/NSA/Free_Ultrafilter.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NSA/Free_Ultrafilter.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -0,0 +1,200 @@
+(*  Title:      HOL/NSA/Free_Ultrafilter.thy
+    Author:     Jacques D. Fleuriot, University of Cambridge
+    Author:     Lawrence C Paulson
+    Author:     Brian Huffman
+*) 
+
+section {* Filters and Ultrafilters *}
+
+theory Free_Ultrafilter
+imports "~~/src/HOL/Library/Infinite_Set"
+begin
+
+subsection {* Definitions and basic properties *}
+
+subsubsection {* Ultrafilters *}
+
+locale ultrafilter =
+  fixes F :: "'a filter"
+  assumes proper: "F \<noteq> bot"
+  assumes ultra: "eventually P F \<or> eventually (\<lambda>x. \<not> P x) F"
+begin
+
+lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F"
+  using ultra[of P] by (simp add: frequently_def)
+
+lemma frequently_eq_eventually: "frequently P F = eventually P F"
+  using eventually_imp_frequently eventually_frequently[OF proper] ..
+
+lemma eventually_disj_iff: "eventually (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> eventually P F \<or> eventually Q F"
+  unfolding frequently_eq_eventually[symmetric] frequently_disj_iff ..
+
+lemma eventually_all_iff: "eventually (\<lambda>x. \<forall>y. P x y) F = (\<forall>Y. eventually (\<lambda>x. P x (Y x)) F)"
+  using frequently_all[of P F] by (simp add: frequently_eq_eventually)
+
+lemma eventually_imp_iff: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longrightarrow> eventually Q F)"
+  using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually)
+
+lemma eventually_iff_iff: "eventually (\<lambda>x. P x \<longleftrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longleftrightarrow> eventually Q F)"
+  unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp
+
+lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F"
+  unfolding not_eventually frequently_eq_eventually ..
+
+end
+
+subsection {* Maximal filter = Ultrafilter *}
+
+text {*
+   A filter F is an ultrafilter iff it is a maximal filter,
+   i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
+*}
+text {*
+  Lemmas that shows existence of an extension to what was assumed to
+  be a maximal filter. Will be used to derive contradiction in proof of
+  property of ultrafilter.
+*}
+
+lemma extend_filter:
+  "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot"
+  unfolding trivial_limit_def eventually_inf_principal by (simp add: not_eventually)
+
+lemma max_filter_ultrafilter:
+  assumes proper: "F \<noteq> bot"
+  assumes max: "\<And>G. G \<noteq> bot \<Longrightarrow> G \<le> F \<Longrightarrow> F = G"
+  shows "ultrafilter F"
+proof
+  fix P show "eventually P F \<or> (\<forall>\<^sub>Fx in F. \<not> P x)"
+  proof (rule disjCI)
+    assume "\<not> (\<forall>\<^sub>Fx in F. \<not> P x)"
+    then have "inf F (principal {x. P x}) \<noteq> bot"
+      by (simp add: not_eventually extend_filter)
+    then have F: "F = inf F (principal {x. P x})"
+      by (rule max) simp
+    show "eventually P F"
+      by (subst F) (simp add: eventually_inf_principal)
+  qed
+qed fact
+
+lemma le_filter_frequently: "F \<le> G \<longleftrightarrow> (\<forall>P. frequently P F \<longrightarrow> frequently P G)"
+  unfolding frequently_def le_filter_def
+  apply auto
+  apply (erule_tac x="\<lambda>x. \<not> P x" in allE)
+  apply auto
+  done
+
+lemma (in ultrafilter) max_filter:
+  assumes G: "G \<noteq> bot" and sub: "G \<le> F" shows "F = G"
+proof (rule antisym)
+  show "F \<le> G"
+    using sub
+    by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G]
+             intro!: eventually_frequently G proper)
+qed fact
+
+subsection {* Ultrafilter Theorem *}
+
+text "A local context makes proof of ultrafilter Theorem more modular"
+
+lemma ex_max_ultrafilter:
+  fixes F :: "'a filter"
+  assumes F: "F \<noteq> bot"
+  shows "\<exists>U\<le>F. ultrafilter U"
+proof -
+  let ?X = "{G. G \<noteq> bot \<and> G \<le> F}"
+  let ?R = "{(b, a). a \<noteq> bot \<and> a \<le> b \<and> b \<le> F}"
+
+  have bot_notin_R: "\<And>c. c \<in> Chains ?R \<Longrightarrow> bot \<notin> c"
+    by (auto simp: Chains_def)
+
+  have [simp]: "Field ?R = ?X"
+    by (auto simp: Field_def bot_unique)
+
+  have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m"
+  proof (rule Zorns_po_lemma)
+    show "Partial_order ?R"
+      unfolding partial_order_on_def preorder_on_def
+      by (auto simp: antisym_def refl_on_def trans_def Field_def bot_unique)
+    show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R"
+    proof (safe intro!: bexI del: notI)
+      fix c x assume c: "c \<in> Chains ?R"
+
+      { assume "c \<noteq> {}"
+        with c have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)"
+          unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
+        with c have 1: "Inf c \<noteq> bot"
+          by (simp add: bot_notin_R)
+        from `c \<noteq> {}` obtain x where "x \<in> c" by auto
+        with c have 2: "Inf c \<le> F"
+          by (auto intro!: Inf_lower2[of x] simp: Chains_def)
+        note 1 2 }
+      note Inf_c = this
+      then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)"
+        using c by (auto simp add: inf_absorb2)
+
+      show "inf F (Inf c) \<noteq> bot"
+        using c by (simp add: F Inf_c)
+
+      show "inf F (Inf c) \<in> Field ?R"
+        using c by (simp add: Chains_def Inf_c F)
+
+      assume x: "x \<in> c"
+      with c show "inf F (Inf c) \<le> x" "x \<le> F"
+        by (auto intro: Inf_lower simp: Chains_def)
+    qed
+  qed
+  then guess U ..
+  then show ?thesis
+    by (intro exI[of _ U] conjI max_filter_ultrafilter) auto
+qed
+
+subsubsection {* Free Ultrafilters *}
+
+text {* There exists a free ultrafilter on any infinite set *}
+
+locale freeultrafilter = ultrafilter +
+  assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}"
+begin
+
+lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F"
+  by (erule contrapos_pn, erule infinite)
+
+lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F"
+  by (drule finite) (simp add: not_eventually frequently_eq_eventually)
+
+lemma le_cofinite: "F \<le> cofinite"
+  by (intro filter_leI)
+     (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite)
+
+lemma singleton: "\<not> eventually (\<lambda>x. x = a) F"
+by (rule finite, simp)
+
+lemma singleton': "\<not> eventually (op = a) F"
+by (rule finite, simp)
+
+lemma ultrafilter: "ultrafilter F" ..
+
+end
+
+lemma freeultrafilter_Ex:
+  assumes [simp]: "infinite (UNIV :: 'a set)"
+  shows "\<exists>U::'a filter. freeultrafilter U"
+proof -
+  from ex_max_ultrafilter[of "cofinite :: 'a filter"]
+  obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U"
+    by auto
+  interpret ultrafilter U by fact
+  have "freeultrafilter U"
+  proof
+    fix P assume "eventually P U"
+    with proper have "frequently P U"
+      by (rule eventually_frequently)
+    then have "frequently P cofinite"
+      using `U \<le> cofinite` by (simp add: le_filter_frequently)
+    then show "infinite {x. P x}"
+      by (simp add: frequently_cofinite)
+  qed
+  then show ?thesis ..
+qed
+
+end
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -178,7 +178,7 @@
 by (cases x, simp add: star_n_def)
 
 lemma Rep_star_star_n_iff [simp]:
-  "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
+  "(X \<in> Rep_star (star_n Y)) = (eventually (\<lambda>n. Y n = X n) \<U>)"
 by (simp add: star_n_def)
 
 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
@@ -207,12 +207,11 @@
 by (simp only: star_inverse_def starfun_star_n)
 
 lemma star_n_le:
-      "star_n X \<le> star_n Y =
-       ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
+      "star_n X \<le> star_n Y = (eventually (\<lambda>n. X n \<le> Y n) FreeUltrafilterNat)"
 by (simp only: star_le_def starP2_star_n)
 
 lemma star_n_less:
-      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
+      "star_n X < star_n Y = (eventually (\<lambda>n. X n < Y n) FreeUltrafilterNat)"
 by (simp only: star_less_def starP2_star_n)
 
 lemma star_n_zero_num: "0 = star_n (%n. 0)"
@@ -273,7 +272,7 @@
 by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
 
 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
-by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
+by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper
          del: star_of_zero)
 
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/NSA/HyperNat.thy
--- a/src/HOL/NSA/HyperNat.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/NSA/HyperNat.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -274,10 +274,10 @@
   hypnat_omega_def: "whn = star_n (%n::nat. n)"
 
 lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
+by (simp add: FreeUltrafilterNat.singleton' hypnat_omega_def star_of_def star_n_eq_iff)
 
 lemma whn_neq_hypnat_of_nat: "whn \<noteq> hypnat_of_nat n"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
+by (simp add: FreeUltrafilterNat.singleton hypnat_omega_def star_of_def star_n_eq_iff)
 
 lemma whn_not_Nats [simp]: "whn \<notin> Nats"
 by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)
@@ -285,15 +285,9 @@
 lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
 by (simp add: HNatInfinite_def)
 
-lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
-apply (insert finite_atMost [of m])
-apply (drule FreeUltrafilterNat.finite)
-apply (drule FreeUltrafilterNat.not_memD)
-apply (simp add: Collect_neg_eq [symmetric] linorder_not_le atMost_def)
-done
-
-lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
-by (simp add: Collect_neg_eq [symmetric] linorder_not_le) 
+lemma lemma_unbounded_set [simp]: "eventually (\<lambda>n::nat. m < n) \<U>"
+  by (rule filter_leD[OF FreeUltrafilterNat.le_cofinite])
+     (auto simp add: cofinite_eq_sequentially eventually_at_top_dense)
 
 lemma hypnat_of_nat_eq:
      "hypnat_of_nat m  = star_n (%n::nat. m)"
@@ -327,14 +321,14 @@
 
 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
 lemma HNatInfinite_FreeUltrafilterNat_lemma:
-  assumes "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat"
-  shows "{n. N < f n} \<in> FreeUltrafilterNat"
+  assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
+  shows "eventually (\<lambda>n. N < f n) \<U>"
 apply (induct N)
 using assms
 apply (drule_tac x = 0 in spec, simp)
 using assms
 apply (drule_tac x = "Suc N" in spec)
-apply (elim ultra, auto)
+apply (auto elim: eventually_elim2)
 done
 
 lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
@@ -347,18 +341,18 @@
 Free Ultrafilter*}
 
 lemma HNatInfinite_FreeUltrafilterNat:
-     "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
+     "star_n X \<in> HNatInfinite ==> \<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat"
 apply (auto simp add: HNatInfinite_iff SHNat_eq)
 apply (drule_tac x="star_of u" in spec, simp)
 apply (simp add: star_of_def star_less_def starP2_star_n)
 done
 
 lemma FreeUltrafilterNat_HNatInfinite:
-     "\<forall>u. {n. u < X n}:  FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
+     "\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
 by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 
 lemma HNatInfinite_FreeUltrafilterNat_iff:
-     "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
+     "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat)"
 by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
                  FreeUltrafilterNat_HNatInfinite])
 
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/NSA/NSA.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -1915,7 +1915,7 @@
 
 lemma HFinite_FreeUltrafilterNat:
     "star_n X \<in> HFinite
-     ==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
+   ==> \<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat"
 apply (auto simp add: HFinite_def SReal_def)
 apply (rule_tac x=r in exI)
 apply (simp add: hnorm_def star_of_def starfun_star_n)
@@ -1923,7 +1923,7 @@
 done
 
 lemma FreeUltrafilterNat_HFinite:
-     "\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat
+     "\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat
        ==>  star_n X \<in> HFinite"
 apply (auto simp add: HFinite_def mem_Rep_star_iff)
 apply (rule_tac x="star_of u" in bexI)
@@ -1933,7 +1933,7 @@
 done
 
 lemma HFinite_FreeUltrafilterNat_iff:
-     "(star_n X \<in> HFinite) = (\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat)"
+     "(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)"
 by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
 
 subsubsection {* @{term HInfinite} *}
@@ -1957,20 +1957,19 @@
   ultrafilter for Infinite numbers!
  -------------------------------------*)
 lemma FreeUltrafilterNat_const_Finite:
-     "{n. norm (X n) = u} \<in> FreeUltrafilterNat ==> star_n X \<in> HFinite"
+     "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \<in> HFinite"
 apply (rule FreeUltrafilterNat_HFinite)
 apply (rule_tac x = "u + 1" in exI)
-apply (erule ultra, simp)
+apply (auto elim: eventually_elim1)
 done
 
 lemma HInfinite_FreeUltrafilterNat:
-     "star_n X \<in> HInfinite ==> \<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat"
+     "star_n X \<in> HInfinite ==> \<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat"
 apply (drule HInfinite_HFinite_iff [THEN iffD1])
 apply (simp add: HFinite_FreeUltrafilterNat_iff)
 apply (rule allI, drule_tac x="u + 1" in spec)
-apply (drule FreeUltrafilterNat.not_memD)
-apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)
-apply (erule ultra, simp)
+apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
+apply (auto elim: eventually_elim1)
 done
 
 lemma lemma_Int_HI:
@@ -1981,17 +1980,20 @@
 by (auto intro: order_less_asym)
 
 lemma FreeUltrafilterNat_HInfinite:
-     "\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat ==> star_n X \<in> HInfinite"
+     "\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat ==> star_n X \<in> HInfinite"
 apply (rule HInfinite_HFinite_iff [THEN iffD2])
 apply (safe, drule HFinite_FreeUltrafilterNat, safe)
 apply (drule_tac x = u in spec)
-apply (drule (1) FreeUltrafilterNat.Int)
-apply (simp add: Collect_conj_eq [symmetric])
-apply (subgoal_tac "\<forall>n. \<not> (norm (X n) < u \<and> u < norm (X n))", auto)
-done
+proof -
+  fix u assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)"
+  then have "\<forall>\<^sub>F x in \<U>. False"
+    by eventually_elim auto
+  then show False
+    by (simp add: eventually_False FreeUltrafilterNat.proper)
+qed
 
 lemma HInfinite_FreeUltrafilterNat_iff:
-     "(star_n X \<in> HInfinite) = (\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat)"
+     "(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)"
 by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
 
 subsubsection {* @{term Infinitesimal} *}
@@ -2000,21 +2002,21 @@
 by (unfold SReal_def, auto)
 
 lemma Infinitesimal_FreeUltrafilterNat:
-     "star_n X \<in> Infinitesimal ==> \<forall>u>0. {n. norm (X n) < u} \<in> \<U>"
+     "star_n X \<in> Infinitesimal ==> \<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>"
 apply (simp add: Infinitesimal_def ball_SReal_eq)
 apply (simp add: hnorm_def starfun_star_n star_of_def)
 apply (simp add: star_less_def starP2_star_n)
 done
 
 lemma FreeUltrafilterNat_Infinitesimal:
-     "\<forall>u>0. {n. norm (X n) < u} \<in> \<U> ==> star_n X \<in> Infinitesimal"
+     "\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U> ==> star_n X \<in> Infinitesimal"
 apply (simp add: Infinitesimal_def ball_SReal_eq)
 apply (simp add: hnorm_def starfun_star_n star_of_def)
 apply (simp add: star_less_def starP2_star_n)
 done
 
 lemma Infinitesimal_FreeUltrafilterNat_iff:
-     "(star_n X \<in> Infinitesimal) = (\<forall>u>0. {n. norm (X n) < u} \<in> \<U>)"
+     "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)"
 by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
 
 (*------------------------------------------------------------------------
@@ -2087,14 +2089,13 @@
 done
 
 lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
-     "{n. abs(real n) \<le> u} \<notin> FreeUltrafilterNat"
+     "\<not> eventually (\<lambda>n. abs(real n) \<le> u) FreeUltrafilterNat"
 by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
 
-lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat"
-apply (rule ccontr, drule FreeUltrafilterNat.not_memD)
-apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \<le> u}")
-prefer 2 apply force
-apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat.finite])
+lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
+apply (rule FreeUltrafilterNat.finite')
+apply (subgoal_tac "{n::nat. \<not> u < real n} = {n. real n \<le> u}")
+apply (auto simp add: finite_real_of_nat_le_real)
 done
 
 (*--------------------------------------------------------------
@@ -2108,10 +2109,8 @@
 
 text{*@{term omega} is a member of @{term HInfinite}*}
 
-lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> FreeUltrafilterNat"
-apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat)
-apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_real_le_eq)
-done
+lemma FreeUltrafilterNat_omega: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
+  by (fact FreeUltrafilterNat_nat_gt_real)
 
 theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
 apply (simp add: omega_def)
@@ -2165,7 +2164,7 @@
 by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real)
 
 lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
-     "0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
+     "0 < u ==> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) FreeUltrafilterNat"
 by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
 
 (*--------------------------------------------------------------
@@ -2179,9 +2178,9 @@
 
 
 lemma FreeUltrafilterNat_inverse_real_of_posnat:
-     "0 < u ==>
-      {n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
-by (metis Compl_le_inverse_eq FreeUltrafilterNat.ultra inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
+     "0 < u ==> eventually (\<lambda>n. inverse(real(Suc n)) < u) FreeUltrafilterNat"
+by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
+   (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
 
 text{* Example of an hypersequence (i.e. an extended standard sequence)
    whose term with an hypernatural suffix is an infinitesimal i.e.
@@ -2208,8 +2207,8 @@
      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
      ==> star_n X - star_of x \<in> Infinitesimal"
 unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
-by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int 
-         intro: order_less_trans FreeUltrafilterNat.subset)
+by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat  
+         intro: order_less_trans elim!: eventually_elim1)
 
 lemma real_seq_to_hypreal_approx:
      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
@@ -2225,7 +2224,7 @@
      "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
       ==> star_n X - star_n Y \<in> Infinitesimal"
 unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
-by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat
-         intro: order_less_trans FreeUltrafilterNat.subset)
+by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
+         intro: order_less_trans elim!: eventually_elim1)
 
 end
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/NSA/Star.thy
--- a/src/HOL/NSA/Star.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/NSA/Star.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -22,8 +22,8 @@
 definition
   (* nonstandard extension of function *)
   is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
-  "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
-                        ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
+  "is_starext F f =
+    (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). ((y = (F x)) = (eventually (\<lambda>n. Y n = f(X n)) \<U>)))"
 
 definition
   (* internal functions *)
@@ -71,7 +71,7 @@
 lemma STAR_real_seq_to_hypreal:
     "\<forall>n. (X n) \<notin> M ==> star_n X \<notin> *s* M"
 apply (unfold starset_def star_of_def)
-apply (simp add: Iset_star_n)
+apply (simp add: Iset_star_n FreeUltrafilterNat.proper)
 done
 
 lemma STAR_singleton: "*s* {x} = {star_of x}"
@@ -304,9 +304,7 @@
    In this theory since @{text hypreal_hrabs} proved here. Maybe
    move both theorems??*}
 lemma Infinitesimal_FreeUltrafilterNat_iff2:
-     "(star_n X \<in> Infinitesimal) =
-      (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
-                \<in>  FreeUltrafilterNat)"
+     "(star_n X \<in> Infinitesimal) = (\<forall>m. eventually (\<lambda>n. norm(X n) < inverse(real(Suc m))) \<U>)"
 by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
      hnorm_def star_of_nat_def starfun_star_n
      star_n_inverse star_n_less real_of_nat_def)
@@ -318,11 +316,11 @@
       HNatInfinite_FreeUltrafilterNat_iff
       Infinitesimal_FreeUltrafilterNat_iff2)
 apply (drule_tac x="Suc m" in spec)
-apply (erule ultra, simp)
+apply (auto elim!: eventually_elim1)
 done
 
 lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
-      (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
+      (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
 apply (subst approx_minus_iff)
 apply (rule mem_infmal_iff [THEN subst])
 apply (simp add: star_n_diff)
@@ -330,8 +328,7 @@
 done
 
 lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
-      (\<forall>m. {n. norm (X n - Y n) <
-                  inverse(real(Suc m))} : FreeUltrafilterNat)"
+      (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse(real(Suc m))) \<U>)"
 apply (subst approx_minus_iff)
 apply (rule mem_infmal_iff [THEN subst])
 apply (simp add: star_n_diff)
@@ -342,7 +339,7 @@
 apply (rule inj_onI)
 apply (rule ext, rule ccontr)
 apply (drule_tac x = "star_n (%n. xa)" in fun_cong)
-apply (auto simp add: starfun star_n_eq_iff)
+apply (auto simp add: starfun star_n_eq_iff FreeUltrafilterNat.proper)
 done
 
 end
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -5,13 +5,13 @@
 section {* Construction of Star Types Using Ultrafilters *}
 
 theory StarDef
-imports Filter
+imports Free_Ultrafilter
 begin
 
 subsection {* A Free Ultrafilter over the Naturals *}
 
 definition
-  FreeUltrafilterNat :: "nat set set"  ("\<U>") where
+  FreeUltrafilterNat :: "nat filter"  ("\<U>") where
   "\<U> = (SOME U. freeultrafilter U)"
 
 lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
@@ -24,19 +24,11 @@
 interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
 by (rule freeultrafilter_FreeUltrafilterNat)
 
-text {* This rule takes the place of the old ultra tactic *}
-
-lemma ultra:
-  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
-by (simp add: Collect_imp_eq
-    FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff)
-
-
 subsection {* Definition of @{text star} type constructor *}
 
 definition
   starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
-  "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
+  "starrel = {(X,Y). eventually (\<lambda>n. X n = Y n) \<U>}"
 
 definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
 
@@ -59,14 +51,14 @@
 
 text {* Proving that @{term starrel} is an equivalence relation *}
 
-lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
+lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = (eventually (\<lambda>n. X n = Y n) \<U>)"
 by (simp add: starrel_def)
 
 lemma equiv_starrel: "equiv UNIV starrel"
 proof (rule equivI)
   show "refl starrel" by (simp add: refl_on_def)
   show "sym starrel" by (simp add: sym_def eq_commute)
-  show "trans starrel" by (auto intro: transI elim!: ultra)
+  show "trans starrel" by (intro transI) (auto elim: eventually_elim2)
 qed
 
 lemmas equiv_starrel_iff =
@@ -75,7 +67,7 @@
 lemma starrel_in_star: "starrel``{x} \<in> star"
 by (simp add: star_def quotientI)
 
-lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
+lemma star_n_eq_iff: "(star_n X = star_n Y) = (eventually (\<lambda>n. X n = Y n) \<U>)"
 by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
 
 
@@ -83,8 +75,8 @@
 
 text {* This introduction rule starts each transfer proof. *}
 lemma transfer_start:
-  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
-by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
+  "P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+  by (simp add: FreeUltrafilterNat.proper)
 
 text {*Initialize transfer tactic.*}
 ML_file "transfer.ML"
@@ -98,66 +90,66 @@
 text {* Transfer introduction rules. *}
 
 lemma transfer_ex [transfer_intro]:
-  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
-by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> eventually (\<lambda>n. \<exists>x. P n x) \<U>"
+by (simp only: ex_star_eq eventually_ex)
 
 lemma transfer_all [transfer_intro]:
-  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
-by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> eventually (\<lambda>n. \<forall>x. P n x) \<U>"
+by (simp only: all_star_eq FreeUltrafilterNat.eventually_all_iff)
 
 lemma transfer_not [transfer_intro]:
-  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
-by (simp only: FreeUltrafilterNat.Collect_not)
+  "\<lbrakk>p \<equiv> eventually P \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> eventually (\<lambda>n. \<not> P n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_not_iff)
 
 lemma transfer_conj [transfer_intro]:
-  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
-by (simp only: FreeUltrafilterNat.Collect_conj)
+  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+    \<Longrightarrow> p \<and> q \<equiv> eventually (\<lambda>n. P n \<and> Q n) \<U>"
+by (simp only: eventually_conj_iff)
 
 lemma transfer_disj [transfer_intro]:
-  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
-by (simp only: FreeUltrafilterNat.Collect_disj)
+  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+    \<Longrightarrow> p \<or> q \<equiv> eventually (\<lambda>n. P n \<or> Q n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_disj_iff)
 
 lemma transfer_imp [transfer_intro]:
-  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
-by (simp only: imp_conv_disj transfer_disj transfer_not)
+  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+    \<Longrightarrow> p \<longrightarrow> q \<equiv> eventually (\<lambda>n. P n \<longrightarrow> Q n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_imp_iff)
 
 lemma transfer_iff [transfer_intro]:
-  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
-by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
+  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
+    \<Longrightarrow> p = q \<equiv> eventually (\<lambda>n. P n = Q n) \<U>"
+by (simp only: FreeUltrafilterNat.eventually_iff_iff)
 
 lemma transfer_if_bool [transfer_intro]:
-  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
+  "\<lbrakk>p \<equiv> eventually P \<U>; x \<equiv> eventually X \<U>; y \<equiv> eventually Y \<U>\<rbrakk>
+    \<Longrightarrow> (if p then x else y) \<equiv> eventually (\<lambda>n. if P n then X n else Y n) \<U>"
 by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
 
 lemma transfer_eq [transfer_intro]:
-  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
+  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> eventually (\<lambda>n. X n = Y n) \<U>"
 by (simp only: star_n_eq_iff)
 
 lemma transfer_if [transfer_intro]:
-  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
+  "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
     \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
 apply (rule eq_reflection)
-apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
+apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1)
 done
 
 lemma transfer_fun_eq [transfer_intro]:
   "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
-    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
-      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
+    \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk>
+      \<Longrightarrow> f = g \<equiv> eventually (\<lambda>n. F n = G n) \<U>"
 by (simp only: fun_eq_iff transfer_all)
 
 lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
 by (rule reflexive)
 
-lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
-by (simp add: atomize_eq)
+lemma transfer_bool [transfer_intro]: "p \<equiv> eventually (\<lambda>n. p) \<U>"
+by (simp add: FreeUltrafilterNat.proper)
 
 
 subsection {* Standard elements *}
@@ -191,7 +183,7 @@
 
 lemma Ifun_congruent2:
   "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
-by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
+by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp)
 
 lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
 by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
@@ -298,7 +290,7 @@
 definition unstar :: "bool star \<Rightarrow> bool" where
   "unstar b \<longleftrightarrow> b = star_of True"
 
-lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
+lemma unstar_star_n: "unstar (star_n P) = (eventually P \<U>)"
 by (simp add: unstar_def star_of_def star_n_eq_iff)
 
 lemma unstar_star_of [simp]: "unstar (star_of p) = p"
@@ -308,7 +300,7 @@
 setup {* Transfer_Principle.add_const @{const_name unstar} *}
 
 lemma transfer_unstar [transfer_intro]:
-  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
+  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
 by (simp only: unstar_star_n)
 
 definition
@@ -322,11 +314,11 @@
 declare starP_def [transfer_unfold]
 declare starP2_def [transfer_unfold]
 
-lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
+lemma starP_star_n: "( *p* P) (star_n X) = (eventually (\<lambda>n. P (X n)) \<U>)"
 by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
 
 lemma starP2_star_n:
-  "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
+  "( *p2* P) (star_n X) (star_n Y) = (eventually (\<lambda>n. P (X n) (Y n)) \<U>)"
 by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
 
 lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
@@ -343,7 +335,7 @@
   "Iset A = {x. ( *p2* op \<in>) x A}"
 
 lemma Iset_star_n:
-  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
+  "(star_n X \<in> Iset (star_n A)) = (eventually (\<lambda>n. X n \<in> A n) \<U>)"
 by (simp add: Iset_def starP2_star_n)
 
 text {* Transfer tactic should remove occurrences of @{term Iset} *}
@@ -351,27 +343,27 @@
 
 lemma transfer_mem [transfer_intro]:
   "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
-    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
+    \<Longrightarrow> x \<in> a \<equiv> eventually (\<lambda>n. X n \<in> A n) \<U>"
 by (simp only: Iset_star_n)
 
 lemma transfer_Collect [transfer_intro]:
-  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
     \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
 by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n)
 
 lemma transfer_set_eq [transfer_intro]:
   "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
-    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
+    \<Longrightarrow> a = b \<equiv> eventually (\<lambda>n. A n = B n) \<U>"
 by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem)
 
 lemma transfer_ball [transfer_intro]:
-  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
+  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<forall>x\<in>A n. P n x) \<U>"
 by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
 
 lemma transfer_bex [transfer_intro]:
-  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
+  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
+    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<exists>x\<in>A n. P n x) \<U>"
 by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
 
 lemma transfer_Iset [transfer_intro]:
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -322,557 +322,6 @@
     by auto
 qed
 
-subsection {* Filters *}
-
-text {*
-  This definition also allows non-proper filters.
-*}
-
-locale is_filter =
-  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
-  assumes True: "F (\<lambda>x. True)"
-  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
-  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
-
-typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
-proof
-  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
-qed
-
-lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
-  using Rep_filter [of F] by simp
-
-lemma Abs_filter_inverse':
-  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
-  using assms by (simp add: Abs_filter_inverse)
-
-
-subsubsection {* Eventually *}
-
-definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
-  where "eventually P F \<longleftrightarrow> Rep_filter F P"
-
-lemma eventually_Abs_filter:
-  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
-  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
-
-lemma filter_eq_iff:
-  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"
-  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
-
-lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"
-  unfolding eventually_def
-  by (rule is_filter.True [OF is_filter_Rep_filter])
-
-lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"
-proof -
-  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
-  thus "eventually P F" by simp
-qed
-
-lemma eventually_mono:
-  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
-  unfolding eventually_def
-  by (rule is_filter.mono [OF is_filter_Rep_filter])
-
-lemma eventually_conj:
-  assumes P: "eventually (\<lambda>x. P x) F"
-  assumes Q: "eventually (\<lambda>x. Q x) F"
-  shows "eventually (\<lambda>x. P x \<and> Q x) F"
-  using assms unfolding eventually_def
-  by (rule is_filter.conj [OF is_filter_Rep_filter])
-
-lemma eventually_Ball_finite:
-  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
-  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
-using assms by (induct set: finite, simp, simp add: eventually_conj)
-
-lemma eventually_all_finite:
-  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
-  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
-  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
-using eventually_Ball_finite [of UNIV P] assms by simp
-
-lemma eventually_mp:
-  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
-  assumes "eventually (\<lambda>x. P x) F"
-  shows "eventually (\<lambda>x. Q x) F"
-proof (rule eventually_mono)
-  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
-  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
-    using assms by (rule eventually_conj)
-qed
-
-lemma eventually_rev_mp:
-  assumes "eventually (\<lambda>x. P x) F"
-  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
-  shows "eventually (\<lambda>x. Q x) F"
-using assms(2) assms(1) by (rule eventually_mp)
-
-lemma eventually_conj_iff:
-  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
-  by (auto intro: eventually_conj elim: eventually_rev_mp)
-
-lemma eventually_elim1:
-  assumes "eventually (\<lambda>i. P i) F"
-  assumes "\<And>i. P i \<Longrightarrow> Q i"
-  shows "eventually (\<lambda>i. Q i) F"
-  using assms by (auto elim!: eventually_rev_mp)
-
-lemma eventually_elim2:
-  assumes "eventually (\<lambda>i. P i) F"
-  assumes "eventually (\<lambda>i. Q i) F"
-  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
-  shows "eventually (\<lambda>i. R i) F"
-  using assms by (auto elim!: eventually_rev_mp)
-
-lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
-  by (auto intro: eventually_mp)
-
-lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
-  by (metis always_eventually)
-
-lemma eventually_subst:
-  assumes "eventually (\<lambda>n. P n = Q n) F"
-  shows "eventually P F = eventually Q F" (is "?L = ?R")
-proof -
-  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
-      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
-    by (auto elim: eventually_elim1)
-  then show ?thesis by (auto elim: eventually_elim2)
-qed
-
-ML {*
-  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
-    let
-      val mp_thms = facts RL @{thms eventually_rev_mp}
-      val raw_elim_thm =
-        (@{thm allI} RS @{thm always_eventually})
-        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
-        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
-      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
-      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
-    in
-      CASES cases (rtac raw_elim_thm i)
-    end)
-*}
-
-method_setup eventually_elim = {*
-  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
-*} "elimination of eventually quantifiers"
-
-
-subsubsection {* Finer-than relation *}
-
-text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
-filter @{term F'}. *}
-
-instantiation filter :: (type) complete_lattice
-begin
-
-definition le_filter_def:
-  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"
-
-definition
-  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
-
-definition
-  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
-
-definition
-  "bot = Abs_filter (\<lambda>P. True)"
-
-definition
-  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"
-
-definition
-  "inf F F' = Abs_filter
-      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
-
-definition
-  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"
-
-definition
-  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"
-
-lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
-  unfolding top_filter_def
-  by (rule eventually_Abs_filter, rule is_filter.intro, auto)
-
-lemma eventually_bot [simp]: "eventually P bot"
-  unfolding bot_filter_def
-  by (subst eventually_Abs_filter, rule is_filter.intro, auto)
-
-lemma eventually_sup:
-  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"
-  unfolding sup_filter_def
-  by (rule eventually_Abs_filter, rule is_filter.intro)
-     (auto elim!: eventually_rev_mp)
-
-lemma eventually_inf:
-  "eventually P (inf F F') \<longleftrightarrow>
-   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
-  unfolding inf_filter_def
-  apply (rule eventually_Abs_filter, rule is_filter.intro)
-  apply (fast intro: eventually_True)
-  apply clarify
-  apply (intro exI conjI)
-  apply (erule (1) eventually_conj)
-  apply (erule (1) eventually_conj)
-  apply simp
-  apply auto
-  done
-
-lemma eventually_Sup:
-  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"
-  unfolding Sup_filter_def
-  apply (rule eventually_Abs_filter, rule is_filter.intro)
-  apply (auto intro: eventually_conj elim!: eventually_rev_mp)
-  done
-
-instance proof
-  fix F F' F'' :: "'a filter" and S :: "'a filter set"
-  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"
-    by (rule less_filter_def) }
-  { show "F \<le> F"
-    unfolding le_filter_def by simp }
-  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"
-    unfolding le_filter_def by simp }
-  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
-    unfolding le_filter_def filter_eq_iff by fast }
-  { show "inf F F' \<le> F" and "inf F F' \<le> F'"
-    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
-  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
-    unfolding le_filter_def eventually_inf
-    by (auto elim!: eventually_mono intro: eventually_conj) }
-  { show "F \<le> sup F F'" and "F' \<le> sup F F'"
-    unfolding le_filter_def eventually_sup by simp_all }
-  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
-    unfolding le_filter_def eventually_sup by simp }
-  { assume "F'' \<in> S" thus "Inf S \<le> F''"
-    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
-  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
-    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
-  { assume "F \<in> S" thus "F \<le> Sup S"
-    unfolding le_filter_def eventually_Sup by simp }
-  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
-    unfolding le_filter_def eventually_Sup by simp }
-  { show "Inf {} = (top::'a filter)"
-    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
-      (metis (full_types) top_filter_def always_eventually eventually_top) }
-  { show "Sup {} = (bot::'a filter)"
-    by (auto simp: bot_filter_def Sup_filter_def) }
-qed
-
-end
-
-lemma filter_leD:
-  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"
-  unfolding le_filter_def by simp
-
-lemma filter_leI:
-  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"
-  unfolding le_filter_def by simp
-
-lemma eventually_False:
-  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
-  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
-
-abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
-  where "trivial_limit F \<equiv> F = bot"
-
-lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
-  by (rule eventually_False [symmetric])
-
-lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
-  by (cases P) (simp_all add: eventually_False)
-
-lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
-proof -
-  let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
-  
-  { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
-    proof (rule eventually_Abs_filter is_filter.intro)+
-      show "?F (\<lambda>x. True)"
-        by (rule exI[of _ "{}"]) (simp add: le_fun_def)
-    next
-      fix P Q
-      assume "?F P" then guess X ..
-      moreover
-      assume "?F Q" then guess Y ..
-      ultimately show "?F (\<lambda>x. P x \<and> Q x)"
-        by (intro exI[of _ "X \<union> Y"])
-           (auto simp: Inf_union_distrib eventually_inf)
-    next
-      fix P Q
-      assume "?F P" then guess X ..
-      moreover assume "\<forall>x. P x \<longrightarrow> Q x"
-      ultimately show "?F Q"
-        by (intro exI[of _ X]) (auto elim: eventually_elim1)
-    qed }
-  note eventually_F = this
-
-  have "Inf B = Abs_filter ?F"
-  proof (intro antisym Inf_greatest)
-    show "Inf B \<le> Abs_filter ?F"
-      by (auto simp: le_filter_def eventually_F dest: Inf_superset_mono)
-  next
-    fix F assume "F \<in> B" then show "Abs_filter ?F \<le> F"
-      by (auto simp add: le_filter_def eventually_F intro!: exI[of _ "{F}"])
-  qed
-  then show ?thesis
-    by (simp add: eventually_F)
-qed
-
-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))"
-  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
-  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
-
-lemma Inf_filter_not_bot:
-  fixes B :: "'a filter set"
-  shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> Inf X \<noteq> bot) \<Longrightarrow> Inf B \<noteq> bot"
-  unfolding trivial_limit_def eventually_Inf[of _ B]
-    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
-
-lemma INF_filter_not_bot:
-  fixes F :: "'i \<Rightarrow> 'a filter"
-  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"
-  unfolding trivial_limit_def eventually_INF[of _ B]
-    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
-
-lemma eventually_Inf_base:
-  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"
-  shows "eventually P (Inf B) \<longleftrightarrow> (\<exists>b\<in>B. eventually P b)"
-proof (subst eventually_Inf, safe)
-  fix X assume "finite X" "X \<subseteq> B"
-  then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
-  proof induct
-    case empty then show ?case
-      using `B \<noteq> {}` by auto
-  next
-    case (insert x X)
-    then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
-      by auto
-    with `insert x X \<subseteq> B` base[of b x] show ?case
-      by (auto intro: order_trans)
-  qed
-  then obtain b where "b \<in> B" "b \<le> Inf X"
-    by (auto simp: le_Inf_iff)
-  then show "eventually P (Inf X) \<Longrightarrow> Bex B (eventually P)"
-    by (intro bexI[of _ b]) (auto simp: le_filter_def)
-qed (auto intro!: exI[of _ "{x}" for x])
-
-lemma eventually_INF_base:
-  "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>
-    eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
-  unfolding INF_def by (subst eventually_Inf_base) auto
-
-
-subsubsection {* Map function for filters *}
-
-definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
-  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
-
-lemma eventually_filtermap:
-  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"
-  unfolding filtermap_def
-  apply (rule eventually_Abs_filter)
-  apply (rule is_filter.intro)
-  apply (auto elim!: eventually_rev_mp)
-  done
-
-lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
-  by (simp add: filter_eq_iff eventually_filtermap)
-
-lemma filtermap_filtermap:
-  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"
-  by (simp add: filter_eq_iff eventually_filtermap)
-
-lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"
-  unfolding le_filter_def eventually_filtermap by simp
-
-lemma filtermap_bot [simp]: "filtermap f bot = bot"
-  by (simp add: filter_eq_iff eventually_filtermap)
-
-lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"
-  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)
-
-lemma filtermap_inf: "filtermap f (inf F1 F2) \<le> inf (filtermap f F1) (filtermap f F2)"
-  by (auto simp: le_filter_def eventually_filtermap eventually_inf)
-
-lemma filtermap_INF: "filtermap f (INF b:B. F b) \<le> (INF b:B. filtermap f (F b))"
-proof -
-  { fix X :: "'c set" assume "finite X"
-    then have "filtermap f (INFIMUM X F) \<le> (INF b:X. filtermap f (F b))"
-    proof induct
-      case (insert x X)
-      have "filtermap f (INF a:insert x X. F a) \<le> inf (filtermap f (F x)) (filtermap f (INF a:X. F a))"
-        by (rule order_trans[OF _ filtermap_inf]) simp
-      also have "\<dots> \<le> inf (filtermap f (F x)) (INF a:X. filtermap f (F a))"
-        by (intro inf_mono insert order_refl)
-      finally show ?case
-        by simp
-    qed simp }
-  then show ?thesis
-    unfolding le_filter_def eventually_filtermap
-    by (subst (1 2) eventually_INF) auto
-qed
-subsubsection {* Standard filters *}
-
-definition principal :: "'a set \<Rightarrow> 'a filter" where
-  "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
-
-lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
-  unfolding principal_def
-  by (rule eventually_Abs_filter, rule is_filter.intro) auto
-
-lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
-  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
-
-lemma principal_UNIV[simp]: "principal UNIV = top"
-  by (auto simp: filter_eq_iff eventually_principal)
-
-lemma principal_empty[simp]: "principal {} = bot"
-  by (auto simp: filter_eq_iff eventually_principal)
-
-lemma principal_eq_bot_iff: "principal X = bot \<longleftrightarrow> X = {}"
-  by (auto simp add: filter_eq_iff eventually_principal)
-
-lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
-  by (auto simp: le_filter_def eventually_principal)
-
-lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
-  unfolding le_filter_def eventually_principal
-  apply safe
-  apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
-  apply (auto elim: eventually_elim1)
-  done
-
-lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
-  unfolding eq_iff by simp
-
-lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
-  unfolding filter_eq_iff eventually_sup eventually_principal by auto
-
-lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
-  unfolding filter_eq_iff eventually_inf eventually_principal
-  by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
-
-lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
-  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
-
-lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
-  by (induct X rule: finite_induct) auto
-
-lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
-  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
-
-subsubsection {* Order filters *}
-
-definition at_top :: "('a::order) filter"
-  where "at_top = (INF k. principal {k ..})"
-
-lemma at_top_sub: "at_top = (INF k:{c::'a::linorder..}. principal {k ..})"
-  by (auto intro!: INF_eq max.cobounded1 max.cobounded2 simp: at_top_def)
-
-lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
-  unfolding at_top_def
-  by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
-
-lemma eventually_ge_at_top:
-  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
-  unfolding eventually_at_top_linorder by auto
-
-lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::{no_top, linorder}. \<forall>n>N. P n)"
-proof -
-  have "eventually P (INF k. principal {k <..}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n>N. P n)"
-    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
-  also have "(INF k. principal {k::'a <..}) = at_top"
-    unfolding at_top_def 
-    by (intro INF_eq) (auto intro: less_imp_le simp: Ici_subset_Ioi_iff gt_ex)
-  finally show ?thesis .
-qed
-
-lemma eventually_gt_at_top:
-  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
-  unfolding eventually_at_top_dense by auto
-
-definition at_bot :: "('a::order) filter"
-  where "at_bot = (INF k. principal {.. k})"
-
-lemma at_bot_sub: "at_bot = (INF k:{.. c::'a::linorder}. principal {.. k})"
-  by (auto intro!: INF_eq min.cobounded1 min.cobounded2 simp: at_bot_def)
-
-lemma eventually_at_bot_linorder:
-  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
-  unfolding at_bot_def
-  by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
-
-lemma eventually_le_at_bot:
-  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
-  unfolding eventually_at_bot_linorder by auto
-
-lemma eventually_at_bot_dense: "eventually P at_bot \<longleftrightarrow> (\<exists>N::'a::{no_bot, linorder}. \<forall>n<N. P n)"
-proof -
-  have "eventually P (INF k. principal {..< k}) \<longleftrightarrow> (\<exists>N::'a. \<forall>n<N. P n)"
-    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
-  also have "(INF k. principal {..< k::'a}) = at_bot"
-    unfolding at_bot_def 
-    by (intro INF_eq) (auto intro: less_imp_le simp: Iic_subset_Iio_iff lt_ex)
-  finally show ?thesis .
-qed
-
-lemma eventually_gt_at_bot:
-  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
-  unfolding eventually_at_bot_dense by auto
-
-lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
-  unfolding trivial_limit_def
-  by (metis eventually_at_bot_linorder order_refl)
-
-lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
-  unfolding trivial_limit_def
-  by (metis eventually_at_top_linorder order_refl)
-
-subsection {* Sequentially *}
-
-abbreviation sequentially :: "nat filter"
-  where "sequentially \<equiv> at_top"
-
-lemma eventually_sequentially:
-  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
-  by (rule eventually_at_top_linorder)
-
-lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
-  unfolding filter_eq_iff eventually_sequentially by auto
-
-lemmas trivial_limit_sequentially = sequentially_bot
-
-lemma eventually_False_sequentially [simp]:
-  "\<not> eventually (\<lambda>n. False) sequentially"
-  by (simp add: eventually_False)
-
-lemma le_sequentially:
-  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
-  by (simp add: at_top_def le_INF_iff le_principal)
-
-lemma eventually_sequentiallyI:
-  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
-  shows "eventually P sequentially"
-using assms by (auto simp: eventually_sequentially)
-
-lemma eventually_sequentially_seg:
-  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
-  unfolding eventually_sequentially
-  apply safe
-   apply (rule_tac x="N + k" in exI)
-   apply rule
-   apply (erule_tac x="n - k" in allE)
-   apply auto []
-  apply (rule_tac x=N in exI)
-  apply auto []
-  done
-
 subsubsection {* Topological filters *}
 
 definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
@@ -1005,104 +454,6 @@
   "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   by (subst at_eq_sup_left_right) (simp add: eventually_sup)
 
-subsection {* Limits *}
-
-definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
-  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
-
-syntax
-  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
-
-translations
-  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"
-
-lemma filterlim_iff:
-  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
-  unfolding filterlim_def le_filter_def eventually_filtermap ..
-
-lemma filterlim_compose:
-  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"
-  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)
-
-lemma filterlim_mono:
-  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"
-  unfolding filterlim_def by (metis filtermap_mono order_trans)
-
-lemma filterlim_ident: "LIM x F. x :> F"
-  by (simp add: filterlim_def filtermap_ident)
-
-lemma filterlim_cong:
-  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
-  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
-
-lemma filterlim_mono_eventually:
-  assumes "filterlim f F G" and ord: "F \<le> F'" "G' \<le> G"
-  assumes eq: "eventually (\<lambda>x. f x = f' x) G'"
-  shows "filterlim f' F' G'"
-  apply (rule filterlim_cong[OF refl refl eq, THEN iffD1])
-  apply (rule filterlim_mono[OF _ ord])
-  apply fact
-  done
-
-lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
-  apply (auto intro!: filtermap_mono) []
-  apply (auto simp: le_filter_def eventually_filtermap)
-  apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
-  apply auto
-  done
-
-lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
-  by (simp add: filtermap_mono_strong eq_iff)
-
-lemma filterlim_principal:
-  "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
-  unfolding filterlim_def eventually_filtermap le_principal ..
-
-lemma filterlim_inf:
-  "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
-  unfolding filterlim_def by simp
-
-lemma filterlim_INF:
-  "(LIM x F. f x :> (INF b:B. G b)) \<longleftrightarrow> (\<forall>b\<in>B. LIM x F. f x :> G b)"
-  unfolding filterlim_def le_INF_iff ..
-
-lemma filterlim_INF_INF:
-  "(\<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)"
-  unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
-
-lemma filterlim_base:
-  "(\<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> 
-    LIM x (INF i:I. principal (F i)). f x :> (INF j:J. principal (G j))"
-  by (force intro!: filterlim_INF_INF simp: image_subset_iff)
-
-lemma filterlim_base_iff: 
-  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"
-  shows "(LIM x (INF i:I. principal (F i)). f x :> INF j:J. principal (G j)) \<longleftrightarrow>
-    (\<forall>j\<in>J. \<exists>i\<in>I. \<forall>x\<in>F i. f x \<in> G j)"
-  unfolding filterlim_INF filterlim_principal
-proof (subst eventually_INF_base)
-  fix i j assume "i \<in> I" "j \<in> I"
-  with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
-    by auto
-qed (auto simp: eventually_principal `I \<noteq> {}`)
-
-lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
-  unfolding filterlim_def filtermap_filtermap ..
-
-lemma filterlim_sup:
-  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
-  unfolding filterlim_def filtermap_sup by auto
-
-lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
-  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
-
-lemma filterlim_sequentially_Suc:
-  "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
-  unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
-
-lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
-  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
-
 subsubsection {* Tendsto *}
 
 abbreviation (in topological_space)
@@ -1296,92 +647,6 @@
 lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
 
-subsection {* Limits to @{const at_top} and @{const at_bot} *}
-
-lemma filterlim_at_top:
-  fixes f :: "'a \<Rightarrow> ('b::linorder)"
-  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
-  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
-
-lemma filterlim_at_top_mono:
-  "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
-    LIM x F. g x :> at_top"
-  by (auto simp: filterlim_at_top elim: eventually_elim2 intro: order_trans)
-
-lemma filterlim_at_top_dense:
-  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
-  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
-  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
-            filterlim_at_top[of f F] filterlim_iff[of f at_top F])
-
-lemma filterlim_at_top_ge:
-  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
-  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z\<ge>c. eventually (\<lambda>x. Z \<le> f x) F)"
-  unfolding at_top_sub[of c] filterlim_INF by (auto simp add: filterlim_principal)
-
-lemma filterlim_at_top_at_top:
-  fixes f :: "'a::linorder \<Rightarrow> 'b::linorder"
-  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
-  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
-  assumes Q: "eventually Q at_top"
-  assumes P: "eventually P at_top"
-  shows "filterlim f at_top at_top"
-proof -
-  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
-    unfolding eventually_at_top_linorder by auto
-  show ?thesis
-  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
-    fix z assume "x \<le> z"
-    with x have "P z" by auto
-    have "eventually (\<lambda>x. g z \<le> x) at_top"
-      by (rule eventually_ge_at_top)
-    with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
-      by eventually_elim (metis mono bij `P z`)
-  qed
-qed
-
-lemma filterlim_at_top_gt:
-  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
-  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z>c. eventually (\<lambda>x. Z \<le> f x) F)"
-  by (metis filterlim_at_top order_less_le_trans gt_ex filterlim_at_top_ge)
-
-lemma filterlim_at_bot: 
-  fixes f :: "'a \<Rightarrow> ('b::linorder)"
-  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
-  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
-
-lemma filterlim_at_bot_dense:
-  fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
-  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
-proof (auto simp add: filterlim_at_bot[of f F])
-  fix Z :: 'b
-  from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
-  assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
-  hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
-  thus "eventually (\<lambda>x. f x < Z) F"
-    apply (rule eventually_mono[rotated])
-    using 1 by auto
-  next 
-    fix Z :: 'b 
-    show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
-      by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
-qed
-
-lemma filterlim_at_bot_le:
-  fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
-  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
-  unfolding filterlim_at_bot
-proof safe
-  fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
-  with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
-    by (auto elim!: eventually_elim1)
-qed simp
-
-lemma filterlim_at_bot_lt:
-  fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
-  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
-  by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
-
 lemma filterlim_at_bot_at_right:
   fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
@@ -2371,7 +1636,7 @@
     by (rule compactE)
   from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
   with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
-    by (simp add: eventually_Ball_finite)
+    by (simp add: eventually_ball_finite)
   with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
     by (auto elim!: eventually_mono [rotated])
   thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
@@ -2936,220 +2201,4 @@
   qed
 qed (intro cSUP_least `antimono f`[THEN antimonoD] cInf_lower S)
 
-subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
-
-context begin interpretation lifting_syntax .
-
-definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
-where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"
-
-lemma rel_filter_eventually:
-  "rel_filter R F G \<longleftrightarrow> 
-  ((R ===> op =) ===> op =) (\<lambda>P. eventually P F) (\<lambda>P. eventually P G)"
-by(simp add: rel_filter_def eventually_def)
-
-lemma filtermap_id [simp, id_simps]: "filtermap id = id"
-by(simp add: fun_eq_iff id_def filtermap_ident)
-
-lemma filtermap_id' [simp]: "filtermap (\<lambda>x. x) = (\<lambda>F. F)"
-using filtermap_id unfolding id_def .
-
-lemma Quotient_filter [quot_map]:
-  assumes Q: "Quotient R Abs Rep T"
-  shows "Quotient (rel_filter R) (filtermap Abs) (filtermap Rep) (rel_filter T)"
-unfolding Quotient_alt_def
-proof(intro conjI strip)
-  from Q have *: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
-    unfolding Quotient_alt_def by blast
-
-  fix F G
-  assume "rel_filter T F G"
-  thus "filtermap Abs F = G" unfolding filter_eq_iff
-    by(auto simp add: eventually_filtermap rel_filter_eventually * rel_funI del: iffI elim!: rel_funD)
-next
-  from Q have *: "\<And>x. T (Rep x) x" unfolding Quotient_alt_def by blast
-
-  fix F
-  show "rel_filter T (filtermap Rep F) F" 
-    by(auto elim: rel_funD intro: * intro!: ext arg_cong[where f="\<lambda>P. eventually P F"] rel_funI
-            del: iffI simp add: eventually_filtermap rel_filter_eventually)
-qed(auto simp add: map_fun_def o_def eventually_filtermap filter_eq_iff fun_eq_iff rel_filter_eventually
-         fun_quotient[OF fun_quotient[OF Q identity_quotient] identity_quotient, unfolded Quotient_alt_def])
-
-lemma eventually_parametric [transfer_rule]:
-  "((A ===> op =) ===> rel_filter A ===> op =) eventually eventually"
-by(simp add: rel_fun_def rel_filter_eventually)
-
-lemma rel_filter_eq [relator_eq]: "rel_filter op = = op ="
-by(auto simp add: rel_filter_eventually rel_fun_eq fun_eq_iff filter_eq_iff)
-
-lemma rel_filter_mono [relator_mono]:
-  "A \<le> B \<Longrightarrow> rel_filter A \<le> rel_filter B"
-unfolding rel_filter_eventually[abs_def]
-by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
-
-lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
-
-lemma is_filter_parametric_aux:
-  assumes "is_filter F"
-  assumes [transfer_rule]: "bi_total A" "bi_unique A"
-  and [transfer_rule]: "((A ===> op =) ===> op =) F G"
-  shows "is_filter G"
-proof -
-  interpret is_filter F by fact
-  show ?thesis
-  proof
-    have "F (\<lambda>_. True) = G (\<lambda>x. True)" by transfer_prover
-    thus "G (\<lambda>x. True)" by(simp add: True)
-  next
-    fix P' Q'
-    assume "G P'" "G Q'"
-    moreover
-    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
-    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
-    have "F P = G P'" "F Q = G Q'" by transfer_prover+
-    ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
-    moreover have "F (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)" by transfer_prover
-    ultimately show "G (\<lambda>x. P' x \<and> Q' x)" by simp
-  next
-    fix P' Q'
-    assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
-    moreover
-    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
-    obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
-    have "F P = G P'" by transfer_prover
-    moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
-    ultimately have "F Q" by(simp add: mono)
-    moreover have "F Q = G Q'" by transfer_prover
-    ultimately show "G Q'" by simp
-  qed
-qed
-
-lemma is_filter_parametric [transfer_rule]:
-  "\<lbrakk> bi_total A; bi_unique A \<rbrakk>
-  \<Longrightarrow> (((A ===> op =) ===> op =) ===> op =) is_filter is_filter"
-apply(rule rel_funI)
-apply(rule iffI)
- apply(erule (3) is_filter_parametric_aux)
-apply(erule is_filter_parametric_aux[where A="conversep A"])
-apply(auto simp add: rel_fun_def)
-done
-
-lemma left_total_rel_filter [transfer_rule]:
-  assumes [transfer_rule]: "bi_total A" "bi_unique A"
-  shows "left_total (rel_filter A)"
-proof(rule left_totalI)
-  fix F :: "'a filter"
-  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
-  obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
-    unfolding  bi_total_def by blast
-  moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover
-  hence "is_filter G" by(simp add: eventually_def is_filter_Rep_filter)
-  ultimately have "rel_filter A F (Abs_filter G)"
-    by(simp add: rel_filter_eventually eventually_Abs_filter)
-  thus "\<exists>G. rel_filter A F G" ..
-qed
-
-lemma right_total_rel_filter [transfer_rule]:
-  "\<lbrakk> bi_total A; bi_unique A \<rbrakk> \<Longrightarrow> right_total (rel_filter A)"
-using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp
-
-lemma bi_total_rel_filter [transfer_rule]:
-  assumes "bi_total A" "bi_unique A"
-  shows "bi_total (rel_filter A)"
-unfolding bi_total_alt_def using assms
-by(simp add: left_total_rel_filter right_total_rel_filter)
-
-lemma left_unique_rel_filter [transfer_rule]:
-  assumes "left_unique A"
-  shows "left_unique (rel_filter A)"
-proof(rule left_uniqueI)
-  fix F F' G
-  assume [transfer_rule]: "rel_filter A F G" "rel_filter A F' G"
-  show "F = F'"
-    unfolding filter_eq_iff
-  proof
-    fix P :: "'a \<Rightarrow> bool"
-    obtain P' where [transfer_rule]: "(A ===> op =) P P'"
-      using left_total_fun[OF assms left_total_eq] unfolding left_total_def by blast
-    have "eventually P F = eventually P' G" 
-      and "eventually P F' = eventually P' G" by transfer_prover+
-    thus "eventually P F = eventually P F'" by simp
-  qed
-qed
-
-lemma right_unique_rel_filter [transfer_rule]:
-  "right_unique A \<Longrightarrow> right_unique (rel_filter A)"
-using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp
-
-lemma bi_unique_rel_filter [transfer_rule]:
-  "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)"
-by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter)
-
-lemma top_filter_parametric [transfer_rule]:
-  "bi_total A \<Longrightarrow> (rel_filter A) top top"
-by(simp add: rel_filter_eventually All_transfer)
-
-lemma bot_filter_parametric [transfer_rule]: "(rel_filter A) bot bot"
-by(simp add: rel_filter_eventually rel_fun_def)
-
-lemma sup_filter_parametric [transfer_rule]:
-  "(rel_filter A ===> rel_filter A ===> rel_filter A) sup sup"
-by(fastforce simp add: rel_filter_eventually[abs_def] eventually_sup dest: rel_funD)
-
-lemma Sup_filter_parametric [transfer_rule]:
-  "(rel_set (rel_filter A) ===> rel_filter A) Sup Sup"
-proof(rule rel_funI)
-  fix S T
-  assume [transfer_rule]: "rel_set (rel_filter A) S T"
-  show "rel_filter A (Sup S) (Sup T)"
-    by(simp add: rel_filter_eventually eventually_Sup) transfer_prover
-qed
-
-lemma principal_parametric [transfer_rule]:
-  "(rel_set A ===> rel_filter A) principal principal"
-proof(rule rel_funI)
-  fix S S'
-  assume [transfer_rule]: "rel_set A S S'"
-  show "rel_filter A (principal S) (principal S')"
-    by(simp add: rel_filter_eventually eventually_principal) transfer_prover
-qed
-
-context
-  fixes A :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
-  assumes [transfer_rule]: "bi_unique A" 
-begin
-
-lemma le_filter_parametric [transfer_rule]:
-  "(rel_filter A ===> rel_filter A ===> op =) op \<le> op \<le>"
-unfolding le_filter_def[abs_def] by transfer_prover
-
-lemma less_filter_parametric [transfer_rule]:
-  "(rel_filter A ===> rel_filter A ===> op =) op < op <"
-unfolding less_filter_def[abs_def] by transfer_prover
-
-context
-  assumes [transfer_rule]: "bi_total A"
-begin
-
-lemma Inf_filter_parametric [transfer_rule]:
-  "(rel_set (rel_filter A) ===> rel_filter A) Inf Inf"
-unfolding Inf_filter_def[abs_def] by transfer_prover
-
-lemma inf_filter_parametric [transfer_rule]:
-  "(rel_filter A ===> rel_filter A ===> rel_filter A) inf inf"
-proof(intro rel_funI)+
-  fix F F' G G'
-  assume [transfer_rule]: "rel_filter A F F'" "rel_filter A G G'"
-  have "rel_filter A (Inf {F, G}) (Inf {F', G'})" by transfer_prover
-  thus "rel_filter A (inf F G) (inf F' G')" by simp
-qed
-
 end
-
-end
-
-end
-
-end
diff -r 177d740a0d48 -r 7c4a2e87e4d0 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Apr 13 10:36:06 2015 +0200
+++ b/src/HOL/Transcendental.thy	Mon Apr 13 12:13:52 2015 +0200
@@ -2321,7 +2321,7 @@
   shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
   apply (simp add: powr_def)
   apply (simp add: tendsto_def)
-  apply (simp add: Topological_Spaces.eventually_conj_iff )
+  apply (simp add: eventually_conj_iff )
   apply safe
   apply (case_tac "0 \<in> S")
   apply (auto simp: )
@@ -5201,7 +5201,7 @@
   then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
     using Suc  by auto
   then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
-    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity}*}
+    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity*}
   then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
     using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
     by (force simp add: Limits.isCont_iff)