# HG changeset patch
# User hoelzl
# Date 1428831256 -7200
# Node ID 6c86d58ab0ca6324573d2e0d48f2b0fe8d4bf8c6
# Parent  1fa1023b13b9cb1fcf810859213afffd2a506162
replace Filters in NSA by HOL-Filters

diff -r 1fa1023b13b9 -r 6c86d58ab0ca src/HOL/NSA/Free_Ultrafilter.thy
--- a/src/HOL/NSA/Free_Ultrafilter.thy	Sun Apr 12 11:34:09 2015 +0200
+++ b/src/HOL/NSA/Free_Ultrafilter.thy	Sun Apr 12 11:34:16 2015 +0200
@@ -12,115 +12,37 @@
 
 subsection {* Definitions and basic properties *}
 
-subsubsection {* Filters *}
+subsubsection {* Ultrafilters *}
 
-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"
+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 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 eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F"
+  using ultra[of P] by (simp add: frequently_def)
 
-lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
-by (drule memD, simp)
+lemma frequently_eq_eventually: "frequently P F = eventually P F"
+  using eventually_imp_frequently eventually_frequently[OF proper] ..
 
-lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
-by (auto elim: subset intro: Int)
-
-end
-
-subsubsection {* Ultrafilters *}
+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 ..
 
-locale ultrafilter = filter +
-  assumes ultra: "A \<in> F \<or> - A \<in> F"
-begin
+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 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 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 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 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 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
+lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F"
+  unfolding not_eventually frequently_eq_eventually ..
 
 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 {*
@@ -133,281 +55,146 @@
   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 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 (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
+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
-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
+qed fact
 
-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 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: "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
+  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"
-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 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}"
 
-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)
+  have bot_notin_R: "\<And>c. c \<in> Chains ?R \<Longrightarrow> bot \<notin> c"
+    by (auto simp: Chains_def)
 
-lemma superfrechetD2:
-  "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
-by (simp add: superfrechet_def)
-
-text {* A few properties of free filters *}
+  have [simp]: "Field ?R = ?X"
+    by (auto simp: Field_def bot_unique)
 
-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
+  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"
 
-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 *}
+      { 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)
 
-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.
+      show "inf F (Inf c) \<noteq> bot"
+        using c by (simp add: F Inf_c)
 
-Number 2 is trivial, but 1 requires us to prove all the filter rules."
+      show "inf F (Inf c) \<in> Field ?R"
+        using c by (simp add: Chains_def Inf_c F)
 
-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
+      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
 
-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
+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:
-  "\<exists>U::'a set set. freeultrafilter U"
+  assumes [simp]: "infinite (UNIV :: 'a set)"
+  shows "\<exists>U::'a filter. 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])
+  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
-  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 1fa1023b13b9 -r 6c86d58ab0ca src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Sun Apr 12 11:34:09 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Sun Apr 12 11:34:16 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 1fa1023b13b9 -r 6c86d58ab0ca src/HOL/NSA/HyperNat.thy
--- a/src/HOL/NSA/HyperNat.thy	Sun Apr 12 11:34:09 2015 +0200
+++ b/src/HOL/NSA/HyperNat.thy	Sun Apr 12 11:34:16 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 1fa1023b13b9 -r 6c86d58ab0ca src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Sun Apr 12 11:34:09 2015 +0200
+++ b/src/HOL/NSA/NSA.thy	Sun Apr 12 11:34:16 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 1fa1023b13b9 -r 6c86d58ab0ca src/HOL/NSA/Star.thy
--- a/src/HOL/NSA/Star.thy	Sun Apr 12 11:34:09 2015 +0200
+++ b/src/HOL/NSA/Star.thy	Sun Apr 12 11:34:16 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 1fa1023b13b9 -r 6c86d58ab0ca src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Sun Apr 12 11:34:09 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy	Sun Apr 12 11:34:16 2015 +0200
@@ -11,7 +11,7 @@
 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]: