replace Filters in NSA by HOL-Filters
authorhoelzl
Sun Apr 12 11:34:16 2015 +0200 (2015-04-12)
changeset 600416c86d58ab0ca
parent 60040 1fa1023b13b9
child 60042 7ff7fdfbb9a0
replace Filters in NSA by HOL-Filters
src/HOL/NSA/Free_Ultrafilter.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/HyperNat.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/Star.thy
src/HOL/NSA/StarDef.thy
     1.1 --- a/src/HOL/NSA/Free_Ultrafilter.thy	Sun Apr 12 11:34:09 2015 +0200
     1.2 +++ b/src/HOL/NSA/Free_Ultrafilter.thy	Sun Apr 12 11:34:16 2015 +0200
     1.3 @@ -12,115 +12,37 @@
     1.4  
     1.5  subsection {* Definitions and basic properties *}
     1.6  
     1.7 -subsubsection {* Filters *}
     1.8 +subsubsection {* Ultrafilters *}
     1.9  
    1.10 -locale filter =
    1.11 -  fixes F :: "'a set set"
    1.12 -  assumes UNIV [iff]:  "UNIV \<in> F"
    1.13 -  assumes empty [iff]: "{} \<notin> F"
    1.14 -  assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
    1.15 -  assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
    1.16 +locale ultrafilter =
    1.17 +  fixes F :: "'a filter"
    1.18 +  assumes proper: "F \<noteq> bot"
    1.19 +  assumes ultra: "eventually P F \<or> eventually (\<lambda>x. \<not> P x) F"
    1.20  begin
    1.21  
    1.22 -lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
    1.23 -proof
    1.24 -  assume "A \<in> F" and "- A \<in> F"
    1.25 -  hence "A \<inter> (- A) \<in> F" by (rule Int)
    1.26 -  thus "False" by simp
    1.27 -qed
    1.28 +lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F"
    1.29 +  using ultra[of P] by (simp add: frequently_def)
    1.30  
    1.31 -lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
    1.32 -by (drule memD, simp)
    1.33 +lemma frequently_eq_eventually: "frequently P F = eventually P F"
    1.34 +  using eventually_imp_frequently eventually_frequently[OF proper] ..
    1.35  
    1.36 -lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
    1.37 -by (auto elim: subset intro: Int)
    1.38 -
    1.39 -end
    1.40 -
    1.41 -subsubsection {* Ultrafilters *}
    1.42 +lemma eventually_disj_iff: "eventually (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> eventually P F \<or> eventually Q F"
    1.43 +  unfolding frequently_eq_eventually[symmetric] frequently_disj_iff ..
    1.44  
    1.45 -locale ultrafilter = filter +
    1.46 -  assumes ultra: "A \<in> F \<or> - A \<in> F"
    1.47 -begin
    1.48 +lemma eventually_all_iff: "eventually (\<lambda>x. \<forall>y. P x y) F = (\<forall>Y. eventually (\<lambda>x. P x (Y x)) F)"
    1.49 +  using frequently_all[of P F] by (simp add: frequently_eq_eventually)
    1.50  
    1.51 -lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
    1.52 -using ultra [of A] by simp
    1.53 -
    1.54 -lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
    1.55 -by (rule memI, simp)
    1.56 +lemma eventually_imp_iff: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longrightarrow> eventually Q F)"
    1.57 +  using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually)
    1.58  
    1.59 -lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
    1.60 -by (rule iffI [OF not_memD not_memI])
    1.61 -
    1.62 -lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
    1.63 -by (rule iffI [OF not_memI not_memD])
    1.64 +lemma eventually_iff_iff: "eventually (\<lambda>x. P x \<longleftrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longleftrightarrow> eventually Q F)"
    1.65 +  unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp
    1.66  
    1.67 -lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
    1.68 - apply (rule iffI)
    1.69 -  apply (erule contrapos_pp)
    1.70 -  apply (simp add: Int_iff not_mem_iff)
    1.71 - apply (auto elim: subset)
    1.72 -done
    1.73 +lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F"
    1.74 +  unfolding not_eventually frequently_eq_eventually ..
    1.75  
    1.76  end
    1.77  
    1.78 -subsubsection {* Free Ultrafilters *}
    1.79 -
    1.80 -locale freeultrafilter = ultrafilter +
    1.81 -  assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
    1.82 -begin
    1.83 -
    1.84 -lemma finite: "finite A \<Longrightarrow> A \<notin> F"
    1.85 -by (erule contrapos_pn, erule infinite)
    1.86 -
    1.87 -lemma singleton: "{x} \<notin> F"
    1.88 -by (rule finite, simp)
    1.89 -
    1.90 -lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
    1.91 -apply (subst insert_is_Un)
    1.92 -apply (subst Un_iff)
    1.93 -apply (simp add: singleton)
    1.94 -done
    1.95 -
    1.96 -lemma filter: "filter F" ..
    1.97 -
    1.98 -lemma ultrafilter: "ultrafilter F" ..
    1.99 -
   1.100 -end
   1.101 -
   1.102 -subsection {* Collect properties *}
   1.103 -
   1.104 -lemma (in filter) Collect_ex:
   1.105 -  "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
   1.106 -proof
   1.107 -  assume "{n. \<exists>x. P n x} \<in> F"
   1.108 -  hence "{n. P n (SOME x. P n x)} \<in> F"
   1.109 -    by (auto elim: someI subset)
   1.110 -  thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
   1.111 -next
   1.112 -  show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
   1.113 -    by (auto elim: subset)
   1.114 -qed
   1.115 -
   1.116 -lemma (in filter) Collect_conj:
   1.117 -  "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
   1.118 -by (subst Collect_conj_eq, rule Int_iff)
   1.119 -
   1.120 -lemma (in ultrafilter) Collect_not:
   1.121 -  "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
   1.122 -by (subst Collect_neg_eq, rule Compl_iff)
   1.123 -
   1.124 -lemma (in ultrafilter) Collect_disj:
   1.125 -  "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
   1.126 -by (subst Collect_disj_eq, rule Un_iff)
   1.127 -
   1.128 -lemma (in ultrafilter) Collect_all:
   1.129 -  "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
   1.130 -apply (rule Not_eq_iff [THEN iffD1])
   1.131 -apply (simp add: Collect_not [symmetric])
   1.132 -apply (rule Collect_ex)
   1.133 -done
   1.134 -
   1.135  subsection {* Maximal filter = Ultrafilter *}
   1.136  
   1.137  text {*
   1.138 @@ -133,281 +55,146 @@
   1.139    property of ultrafilter.
   1.140  *}
   1.141  
   1.142 -lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   1.143 -by blast
   1.144 -
   1.145 -lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   1.146 -by blast
   1.147 +lemma extend_filter:
   1.148 +  "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot"
   1.149 +  unfolding trivial_limit_def eventually_inf_principal by (simp add: not_eventually)
   1.150  
   1.151 -lemma (in filter) extend_filter:
   1.152 -assumes A: "- A \<notin> F"
   1.153 -shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
   1.154 -proof (rule filter.intro)
   1.155 -  show "UNIV \<in> ?X" by blast
   1.156 -next
   1.157 -  show "{} \<notin> ?X"
   1.158 -  proof (clarify)
   1.159 -    fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
   1.160 -    from Af have fA: "f \<subseteq> - A" by blast
   1.161 -    from f fA have "- A \<in> F" by (rule subset)
   1.162 -    with A show "False" by simp
   1.163 +lemma max_filter_ultrafilter:
   1.164 +  assumes proper: "F \<noteq> bot"
   1.165 +  assumes max: "\<And>G. G \<noteq> bot \<Longrightarrow> G \<le> F \<Longrightarrow> F = G"
   1.166 +  shows "ultrafilter F"
   1.167 +proof
   1.168 +  fix P show "eventually P F \<or> (\<forall>\<^sub>Fx in F. \<not> P x)"
   1.169 +  proof (rule disjCI)
   1.170 +    assume "\<not> (\<forall>\<^sub>Fx in F. \<not> P x)"
   1.171 +    then have "inf F (principal {x. P x}) \<noteq> bot"
   1.172 +      by (simp add: not_eventually extend_filter)
   1.173 +    then have F: "F = inf F (principal {x. P x})"
   1.174 +      by (rule max) simp
   1.175 +    show "eventually P F"
   1.176 +      by (subst F) (simp add: eventually_inf_principal)
   1.177    qed
   1.178 -next
   1.179 -  fix u and v
   1.180 -  assume u: "u \<in> ?X" and v: "v \<in> ?X"
   1.181 -  from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
   1.182 -  from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
   1.183 -  from f g have fg: "f \<inter> g \<in> F" by (rule Int)
   1.184 -  from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
   1.185 -  from fg Afg show "u \<inter> v \<in> ?X" by blast
   1.186 -next
   1.187 -  fix u and v
   1.188 -  assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
   1.189 -  from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
   1.190 -  from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
   1.191 -  from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
   1.192 -  thus "v \<in> ?X" by simp
   1.193 -qed
   1.194 +qed fact
   1.195  
   1.196 -lemma (in filter) max_filter_ultrafilter:
   1.197 -assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
   1.198 -shows "ultrafilter_axioms F"
   1.199 -proof (rule ultrafilter_axioms.intro)
   1.200 -  fix A show "A \<in> F \<or> - A \<in> F"
   1.201 -  proof (rule disjCI)
   1.202 -    let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   1.203 -    assume AF: "- A \<notin> F"
   1.204 -    from AF have X: "filter ?X" by (rule extend_filter)
   1.205 -    from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
   1.206 -    have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
   1.207 -    from X FX have "F = ?X" by (rule max)
   1.208 -    with AX show "A \<in> F" by simp
   1.209 -  qed
   1.210 -qed
   1.211 +lemma le_filter_frequently: "F \<le> G \<longleftrightarrow> (\<forall>P. frequently P F \<longrightarrow> frequently P G)"
   1.212 +  unfolding frequently_def le_filter_def
   1.213 +  apply auto
   1.214 +  apply (erule_tac x="\<lambda>x. \<not> P x" in allE)
   1.215 +  apply auto
   1.216 +  done
   1.217  
   1.218  lemma (in ultrafilter) max_filter:
   1.219 -assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
   1.220 -proof
   1.221 -  show "F \<subseteq> G" using sub .
   1.222 -  show "G \<subseteq> F"
   1.223 -  proof
   1.224 -    fix A assume A: "A \<in> G"
   1.225 -    from G A have "- A \<notin> G" by (rule filter.memD)
   1.226 -    with sub have B: "- A \<notin> F" by blast
   1.227 -    thus "A \<in> F" by (rule memI)
   1.228 -  qed
   1.229 -qed
   1.230 +  assumes G: "G \<noteq> bot" and sub: "G \<le> F" shows "F = G"
   1.231 +proof (rule antisym)
   1.232 +  show "F \<le> G"
   1.233 +    using sub
   1.234 +    by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G]
   1.235 +             intro!: eventually_frequently G proper)
   1.236 +qed fact
   1.237  
   1.238  subsection {* Ultrafilter Theorem *}
   1.239  
   1.240  text "A local context makes proof of ultrafilter Theorem more modular"
   1.241 -context
   1.242 -  fixes   frechet :: "'a set set"
   1.243 -  and     superfrechet :: "'a set set set"
   1.244 -
   1.245 -  assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
   1.246  
   1.247 -  defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
   1.248 -  and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
   1.249 -begin
   1.250 +lemma ex_max_ultrafilter:
   1.251 +  fixes F :: "'a filter"
   1.252 +  assumes F: "F \<noteq> bot"
   1.253 +  shows "\<exists>U\<le>F. ultrafilter U"
   1.254 +proof -
   1.255 +  let ?X = "{G. G \<noteq> bot \<and> G \<le> F}"
   1.256 +  let ?R = "{(b, a). a \<noteq> bot \<and> a \<le> b \<and> b \<le> F}"
   1.257  
   1.258 -lemma superfrechetI:
   1.259 -  "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
   1.260 -by (simp add: superfrechet_def)
   1.261 -
   1.262 -lemma superfrechetD1:
   1.263 -  "G \<in> superfrechet \<Longrightarrow> filter G"
   1.264 -by (simp add: superfrechet_def)
   1.265 +  have bot_notin_R: "\<And>c. c \<in> Chains ?R \<Longrightarrow> bot \<notin> c"
   1.266 +    by (auto simp: Chains_def)
   1.267  
   1.268 -lemma superfrechetD2:
   1.269 -  "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
   1.270 -by (simp add: superfrechet_def)
   1.271 -
   1.272 -text {* A few properties of free filters *}
   1.273 +  have [simp]: "Field ?R = ?X"
   1.274 +    by (auto simp: Field_def bot_unique)
   1.275  
   1.276 -lemma filter_cofinite:
   1.277 -assumes inf: "infinite (UNIV :: 'a set)"
   1.278 -shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
   1.279 -proof (rule filter.intro)
   1.280 -  show "UNIV \<in> ?F" by simp
   1.281 -next
   1.282 -  show "{} \<notin> ?F" using inf by simp
   1.283 -next
   1.284 -  fix u v assume "u \<in> ?F" and "v \<in> ?F"
   1.285 -  thus "u \<inter> v \<in> ?F" by simp
   1.286 -next
   1.287 -  fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
   1.288 -  from uv have vu: "- v \<subseteq> - u" by simp
   1.289 -  from u show "v \<in> ?F"
   1.290 -    by (simp add: finite_subset [OF vu])
   1.291 -qed
   1.292 +  have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m"
   1.293 +  proof (rule Zorns_po_lemma)
   1.294 +    show "Partial_order ?R"
   1.295 +      unfolding partial_order_on_def preorder_on_def
   1.296 +      by (auto simp: antisym_def refl_on_def trans_def Field_def bot_unique)
   1.297 +    show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R"
   1.298 +    proof (safe intro!: bexI del: notI)
   1.299 +      fix c x assume c: "c \<in> Chains ?R"
   1.300  
   1.301 -text {*
   1.302 -   We prove: 1. Existence of maximal filter i.e. ultrafilter;
   1.303 -             2. Freeness property i.e ultrafilter is free.
   1.304 -             Use a locale to prove various lemmas and then 
   1.305 -             export main result: The ultrafilter Theorem
   1.306 -*}
   1.307 -
   1.308 -lemma filter_frechet: "filter frechet"
   1.309 -by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
   1.310 -
   1.311 -lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
   1.312 -by (rule superfrechetI [OF filter_frechet subset_refl])
   1.313 -
   1.314 -lemma lemma_mem_chain_filter:
   1.315 -  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
   1.316 -by (unfold chains_def superfrechet_def, blast)
   1.317 -
   1.318 -
   1.319 -subsubsection {* Unions of chains of superfrechets *}
   1.320 +      { assume "c \<noteq> {}"
   1.321 +        with c have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)"
   1.322 +          unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
   1.323 +        with c have 1: "Inf c \<noteq> bot"
   1.324 +          by (simp add: bot_notin_R)
   1.325 +        from `c \<noteq> {}` obtain x where "x \<in> c" by auto
   1.326 +        with c have 2: "Inf c \<le> F"
   1.327 +          by (auto intro!: Inf_lower2[of x] simp: Chains_def)
   1.328 +        note 1 2 }
   1.329 +      note Inf_c = this
   1.330 +      then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)"
   1.331 +        using c by (auto simp add: inf_absorb2)
   1.332  
   1.333 -text "In this section we prove that superfrechet is closed
   1.334 -with respect to unions of non-empty chains. We must show
   1.335 -  1) Union of a chain is a filter,
   1.336 -  2) Union of a chain contains frechet.
   1.337 +      show "inf F (Inf c) \<noteq> bot"
   1.338 +        using c by (simp add: F Inf_c)
   1.339  
   1.340 -Number 2 is trivial, but 1 requires us to prove all the filter rules."
   1.341 +      show "inf F (Inf c) \<in> Field ?R"
   1.342 +        using c by (simp add: Chains_def Inf_c F)
   1.343  
   1.344 -lemma Union_chain_UNIV:
   1.345 -  "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
   1.346 -proof -
   1.347 -  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   1.348 -  from 2 obtain x where 3: "x \<in> c" by blast
   1.349 -  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   1.350 -  hence "UNIV \<in> x" by (rule filter.UNIV)
   1.351 -  with 3 show "UNIV \<in> \<Union>c" by blast
   1.352 -qed
   1.353 -
   1.354 -lemma Union_chain_empty:
   1.355 -  "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
   1.356 -proof
   1.357 -  assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
   1.358 -  from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
   1.359 -  from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   1.360 -  hence "{} \<notin> x" by (rule filter.empty)
   1.361 -  with 4 show "False" by simp
   1.362 +      assume x: "x \<in> c"
   1.363 +      with c show "inf F (Inf c) \<le> x" "x \<le> F"
   1.364 +        by (auto intro: Inf_lower simp: Chains_def)
   1.365 +    qed
   1.366 +  qed
   1.367 +  then guess U ..
   1.368 +  then show ?thesis
   1.369 +    by (intro exI[of _ U] conjI max_filter_ultrafilter) auto
   1.370  qed
   1.371  
   1.372 -lemma Union_chain_Int:
   1.373 -  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
   1.374 -proof -
   1.375 -  assume c: "c \<in> chains superfrechet"
   1.376 -  assume "u \<in> \<Union>c"
   1.377 -    then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   1.378 -  assume "v \<in> \<Union>c"
   1.379 -    then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
   1.380 -  from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
   1.381 -  with xc yc have xyc: "x \<union> y \<in> c"
   1.382 -    by (auto simp add: Un_absorb1 Un_absorb2)
   1.383 -  with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
   1.384 -  from ux have uxy: "u \<in> x \<union> y" by simp
   1.385 -  from vy have vxy: "v \<in> x \<union> y" by simp
   1.386 -  from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
   1.387 -  with xyc show "u \<inter> v \<in> \<Union>c" ..
   1.388 -qed
   1.389 -
   1.390 -lemma Union_chain_subset:
   1.391 -  "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
   1.392 -proof -
   1.393 -  assume c: "c \<in> chains superfrechet"
   1.394 -     and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
   1.395 -  from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   1.396 -  from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
   1.397 -  from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
   1.398 -  with xc show "v \<in> \<Union>c" ..
   1.399 -qed
   1.400 -
   1.401 -lemma Union_chain_filter:
   1.402 -assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
   1.403 -shows "filter (\<Union>c)" 
   1.404 -proof (rule filter.intro)
   1.405 -  show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
   1.406 -next
   1.407 -  show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
   1.408 -next
   1.409 -  fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
   1.410 -  with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
   1.411 -next
   1.412 -  fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
   1.413 -  with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
   1.414 -qed
   1.415 -
   1.416 -lemma lemma_mem_chain_frechet_subset:
   1.417 -  "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
   1.418 -by (unfold superfrechet_def chains_def, blast)
   1.419 -
   1.420 -lemma Union_chain_superfrechet:
   1.421 -  "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
   1.422 -proof (rule superfrechetI)
   1.423 -  assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
   1.424 -  thus "filter (\<Union>c)" by (rule Union_chain_filter)
   1.425 -  from 2 obtain x where 3: "x \<in> c" by blast
   1.426 -  from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
   1.427 -  also from 3 have "x \<subseteq> \<Union>c" by blast
   1.428 -  finally show "frechet \<subseteq> \<Union>c" .
   1.429 -qed
   1.430 -
   1.431 -subsubsection {* Existence of free ultrafilter *}
   1.432 -
   1.433 -lemma max_cofinite_filter_Ex:
   1.434 -  "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
   1.435 -proof (rule Zorn_Lemma2, safe)
   1.436 -  fix c assume c: "c \<in> chains superfrechet"
   1.437 -  show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
   1.438 -  proof (cases)
   1.439 -    assume "c = {}"
   1.440 -    with frechet_in_superfrechet show "?U" by blast
   1.441 -  next
   1.442 -    assume A: "c \<noteq> {}"
   1.443 -    from A c have "\<Union>c \<in> superfrechet"
   1.444 -      by (rule Union_chain_superfrechet)
   1.445 -    thus "?U" by blast
   1.446 -  qed
   1.447 -qed
   1.448 -
   1.449 -lemma mem_superfrechet_all_infinite:
   1.450 -  "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
   1.451 -proof
   1.452 -  assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
   1.453 -  from U have fil: "filter U" and fre: "frechet \<subseteq> U"
   1.454 -    by (simp_all add: superfrechet_def)
   1.455 -  from fin have "- A \<in> frechet" by (simp add: frechet_def)
   1.456 -  with fre have cA: "- A \<in> U" by (rule subsetD)
   1.457 -  from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
   1.458 -  with fil show "False" by (simp add: filter.empty)
   1.459 -qed
   1.460 +subsubsection {* Free Ultrafilters *}
   1.461  
   1.462  text {* There exists a free ultrafilter on any infinite set *}
   1.463  
   1.464 +locale freeultrafilter = ultrafilter +
   1.465 +  assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}"
   1.466 +begin
   1.467 +
   1.468 +lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F"
   1.469 +  by (erule contrapos_pn, erule infinite)
   1.470 +
   1.471 +lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F"
   1.472 +  by (drule finite) (simp add: not_eventually frequently_eq_eventually)
   1.473 +
   1.474 +lemma le_cofinite: "F \<le> cofinite"
   1.475 +  by (intro filter_leI)
   1.476 +     (auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite)
   1.477 +
   1.478 +lemma singleton: "\<not> eventually (\<lambda>x. x = a) F"
   1.479 +by (rule finite, simp)
   1.480 +
   1.481 +lemma singleton': "\<not> eventually (op = a) F"
   1.482 +by (rule finite, simp)
   1.483 +
   1.484 +lemma ultrafilter: "ultrafilter F" ..
   1.485 +
   1.486 +end
   1.487 +
   1.488  lemma freeultrafilter_Ex:
   1.489 -  "\<exists>U::'a set set. freeultrafilter U"
   1.490 +  assumes [simp]: "infinite (UNIV :: 'a set)"
   1.491 +  shows "\<exists>U::'a filter. freeultrafilter U"
   1.492  proof -
   1.493 -  from max_cofinite_filter_Ex obtain U
   1.494 -    where U: "U \<in> superfrechet"
   1.495 -      and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
   1.496 -  from U have fil: "filter U" by (rule superfrechetD1)
   1.497 -  from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
   1.498 -  have ultra: "ultrafilter_axioms U"
   1.499 -  proof (rule filter.max_filter_ultrafilter [OF fil])
   1.500 -    fix G assume G: "filter G" and UG: "U \<subseteq> G"
   1.501 -    from fre UG have "frechet \<subseteq> G" by simp
   1.502 -    with G have "G \<in> superfrechet" by (rule superfrechetI)
   1.503 -    from this UG show "U = G" by (rule max[symmetric])
   1.504 +  from ex_max_ultrafilter[of "cofinite :: 'a filter"]
   1.505 +  obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U"
   1.506 +    by auto
   1.507 +  interpret ultrafilter U by fact
   1.508 +  have "freeultrafilter U"
   1.509 +  proof
   1.510 +    fix P assume "eventually P U"
   1.511 +    with proper have "frequently P U"
   1.512 +      by (rule eventually_frequently)
   1.513 +    then have "frequently P cofinite"
   1.514 +      using `U \<le> cofinite` by (simp add: le_filter_frequently)
   1.515 +    then show "infinite {x. P x}"
   1.516 +      by (simp add: frequently_cofinite)
   1.517    qed
   1.518 -  have free: "freeultrafilter_axioms U"
   1.519 -  proof (rule freeultrafilter_axioms.intro)
   1.520 -    fix A assume "A \<in> U"
   1.521 -    with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   1.522 -  qed
   1.523 -  from fil ultra free have "freeultrafilter U"
   1.524 -    by (rule freeultrafilter.intro [OF ultrafilter.intro])
   1.525 -    (* FIXME: unfold_locales should use chained facts *)
   1.526    then show ?thesis ..
   1.527  qed
   1.528  
   1.529  end
   1.530 -
   1.531 -hide_const (open) filter
   1.532 -
   1.533 -end
     2.1 --- a/src/HOL/NSA/HyperDef.thy	Sun Apr 12 11:34:09 2015 +0200
     2.2 +++ b/src/HOL/NSA/HyperDef.thy	Sun Apr 12 11:34:16 2015 +0200
     2.3 @@ -178,7 +178,7 @@
     2.4  by (cases x, simp add: star_n_def)
     2.5  
     2.6  lemma Rep_star_star_n_iff [simp]:
     2.7 -  "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
     2.8 +  "(X \<in> Rep_star (star_n Y)) = (eventually (\<lambda>n. Y n = X n) \<U>)"
     2.9  by (simp add: star_n_def)
    2.10  
    2.11  lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
    2.12 @@ -207,12 +207,11 @@
    2.13  by (simp only: star_inverse_def starfun_star_n)
    2.14  
    2.15  lemma star_n_le:
    2.16 -      "star_n X \<le> star_n Y =
    2.17 -       ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
    2.18 +      "star_n X \<le> star_n Y = (eventually (\<lambda>n. X n \<le> Y n) FreeUltrafilterNat)"
    2.19  by (simp only: star_le_def starP2_star_n)
    2.20  
    2.21  lemma star_n_less:
    2.22 -      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
    2.23 +      "star_n X < star_n Y = (eventually (\<lambda>n. X n < Y n) FreeUltrafilterNat)"
    2.24  by (simp only: star_less_def starP2_star_n)
    2.25  
    2.26  lemma star_n_zero_num: "0 = star_n (%n. 0)"
    2.27 @@ -273,7 +272,7 @@
    2.28  by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
    2.29  
    2.30  lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
    2.31 -by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
    2.32 +by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper
    2.33           del: star_of_zero)
    2.34  
    2.35  lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
     3.1 --- a/src/HOL/NSA/HyperNat.thy	Sun Apr 12 11:34:09 2015 +0200
     3.2 +++ b/src/HOL/NSA/HyperNat.thy	Sun Apr 12 11:34:16 2015 +0200
     3.3 @@ -274,10 +274,10 @@
     3.4    hypnat_omega_def: "whn = star_n (%n::nat. n)"
     3.5  
     3.6  lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
     3.7 -by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
     3.8 +by (simp add: FreeUltrafilterNat.singleton' hypnat_omega_def star_of_def star_n_eq_iff)
     3.9  
    3.10  lemma whn_neq_hypnat_of_nat: "whn \<noteq> hypnat_of_nat n"
    3.11 -by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
    3.12 +by (simp add: FreeUltrafilterNat.singleton hypnat_omega_def star_of_def star_n_eq_iff)
    3.13  
    3.14  lemma whn_not_Nats [simp]: "whn \<notin> Nats"
    3.15  by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)
    3.16 @@ -285,15 +285,9 @@
    3.17  lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
    3.18  by (simp add: HNatInfinite_def)
    3.19  
    3.20 -lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
    3.21 -apply (insert finite_atMost [of m])
    3.22 -apply (drule FreeUltrafilterNat.finite)
    3.23 -apply (drule FreeUltrafilterNat.not_memD)
    3.24 -apply (simp add: Collect_neg_eq [symmetric] linorder_not_le atMost_def)
    3.25 -done
    3.26 -
    3.27 -lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
    3.28 -by (simp add: Collect_neg_eq [symmetric] linorder_not_le) 
    3.29 +lemma lemma_unbounded_set [simp]: "eventually (\<lambda>n::nat. m < n) \<U>"
    3.30 +  by (rule filter_leD[OF FreeUltrafilterNat.le_cofinite])
    3.31 +     (auto simp add: cofinite_eq_sequentially eventually_at_top_dense)
    3.32  
    3.33  lemma hypnat_of_nat_eq:
    3.34       "hypnat_of_nat m  = star_n (%n::nat. m)"
    3.35 @@ -327,14 +321,14 @@
    3.36  
    3.37  (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
    3.38  lemma HNatInfinite_FreeUltrafilterNat_lemma:
    3.39 -  assumes "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat"
    3.40 -  shows "{n. N < f n} \<in> FreeUltrafilterNat"
    3.41 +  assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
    3.42 +  shows "eventually (\<lambda>n. N < f n) \<U>"
    3.43  apply (induct N)
    3.44  using assms
    3.45  apply (drule_tac x = 0 in spec, simp)
    3.46  using assms
    3.47  apply (drule_tac x = "Suc N" in spec)
    3.48 -apply (elim ultra, auto)
    3.49 +apply (auto elim: eventually_elim2)
    3.50  done
    3.51  
    3.52  lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
    3.53 @@ -347,18 +341,18 @@
    3.54  Free Ultrafilter*}
    3.55  
    3.56  lemma HNatInfinite_FreeUltrafilterNat:
    3.57 -     "star_n X \<in> HNatInfinite ==> \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
    3.58 +     "star_n X \<in> HNatInfinite ==> \<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat"
    3.59  apply (auto simp add: HNatInfinite_iff SHNat_eq)
    3.60  apply (drule_tac x="star_of u" in spec, simp)
    3.61  apply (simp add: star_of_def star_less_def starP2_star_n)
    3.62  done
    3.63  
    3.64  lemma FreeUltrafilterNat_HNatInfinite:
    3.65 -     "\<forall>u. {n. u < X n}:  FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
    3.66 +     "\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat ==> star_n X \<in> HNatInfinite"
    3.67  by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
    3.68  
    3.69  lemma HNatInfinite_FreeUltrafilterNat_iff:
    3.70 -     "(star_n X \<in> HNatInfinite) = (\<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
    3.71 +     "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat)"
    3.72  by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
    3.73                   FreeUltrafilterNat_HNatInfinite])
    3.74  
     4.1 --- a/src/HOL/NSA/NSA.thy	Sun Apr 12 11:34:09 2015 +0200
     4.2 +++ b/src/HOL/NSA/NSA.thy	Sun Apr 12 11:34:16 2015 +0200
     4.3 @@ -1915,7 +1915,7 @@
     4.4  
     4.5  lemma HFinite_FreeUltrafilterNat:
     4.6      "star_n X \<in> HFinite
     4.7 -     ==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
     4.8 +   ==> \<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat"
     4.9  apply (auto simp add: HFinite_def SReal_def)
    4.10  apply (rule_tac x=r in exI)
    4.11  apply (simp add: hnorm_def star_of_def starfun_star_n)
    4.12 @@ -1923,7 +1923,7 @@
    4.13  done
    4.14  
    4.15  lemma FreeUltrafilterNat_HFinite:
    4.16 -     "\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat
    4.17 +     "\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat
    4.18         ==>  star_n X \<in> HFinite"
    4.19  apply (auto simp add: HFinite_def mem_Rep_star_iff)
    4.20  apply (rule_tac x="star_of u" in bexI)
    4.21 @@ -1933,7 +1933,7 @@
    4.22  done
    4.23  
    4.24  lemma HFinite_FreeUltrafilterNat_iff:
    4.25 -     "(star_n X \<in> HFinite) = (\<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat)"
    4.26 +     "(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)"
    4.27  by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
    4.28  
    4.29  subsubsection {* @{term HInfinite} *}
    4.30 @@ -1957,20 +1957,19 @@
    4.31    ultrafilter for Infinite numbers!
    4.32   -------------------------------------*)
    4.33  lemma FreeUltrafilterNat_const_Finite:
    4.34 -     "{n. norm (X n) = u} \<in> FreeUltrafilterNat ==> star_n X \<in> HFinite"
    4.35 +     "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \<in> HFinite"
    4.36  apply (rule FreeUltrafilterNat_HFinite)
    4.37  apply (rule_tac x = "u + 1" in exI)
    4.38 -apply (erule ultra, simp)
    4.39 +apply (auto elim: eventually_elim1)
    4.40  done
    4.41  
    4.42  lemma HInfinite_FreeUltrafilterNat:
    4.43 -     "star_n X \<in> HInfinite ==> \<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat"
    4.44 +     "star_n X \<in> HInfinite ==> \<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat"
    4.45  apply (drule HInfinite_HFinite_iff [THEN iffD1])
    4.46  apply (simp add: HFinite_FreeUltrafilterNat_iff)
    4.47  apply (rule allI, drule_tac x="u + 1" in spec)
    4.48 -apply (drule FreeUltrafilterNat.not_memD)
    4.49 -apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)
    4.50 -apply (erule ultra, simp)
    4.51 +apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
    4.52 +apply (auto elim: eventually_elim1)
    4.53  done
    4.54  
    4.55  lemma lemma_Int_HI:
    4.56 @@ -1981,17 +1980,20 @@
    4.57  by (auto intro: order_less_asym)
    4.58  
    4.59  lemma FreeUltrafilterNat_HInfinite:
    4.60 -     "\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat ==> star_n X \<in> HInfinite"
    4.61 +     "\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat ==> star_n X \<in> HInfinite"
    4.62  apply (rule HInfinite_HFinite_iff [THEN iffD2])
    4.63  apply (safe, drule HFinite_FreeUltrafilterNat, safe)
    4.64  apply (drule_tac x = u in spec)
    4.65 -apply (drule (1) FreeUltrafilterNat.Int)
    4.66 -apply (simp add: Collect_conj_eq [symmetric])
    4.67 -apply (subgoal_tac "\<forall>n. \<not> (norm (X n) < u \<and> u < norm (X n))", auto)
    4.68 -done
    4.69 +proof -
    4.70 +  fix u assume "\<forall>\<^sub>Fn in \<U>. norm (X n) < u" "\<forall>\<^sub>Fn in \<U>. u < norm (X n)"
    4.71 +  then have "\<forall>\<^sub>F x in \<U>. False"
    4.72 +    by eventually_elim auto
    4.73 +  then show False
    4.74 +    by (simp add: eventually_False FreeUltrafilterNat.proper)
    4.75 +qed
    4.76  
    4.77  lemma HInfinite_FreeUltrafilterNat_iff:
    4.78 -     "(star_n X \<in> HInfinite) = (\<forall>u. {n. u < norm (X n)} \<in> FreeUltrafilterNat)"
    4.79 +     "(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)"
    4.80  by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
    4.81  
    4.82  subsubsection {* @{term Infinitesimal} *}
    4.83 @@ -2000,21 +2002,21 @@
    4.84  by (unfold SReal_def, auto)
    4.85  
    4.86  lemma Infinitesimal_FreeUltrafilterNat:
    4.87 -     "star_n X \<in> Infinitesimal ==> \<forall>u>0. {n. norm (X n) < u} \<in> \<U>"
    4.88 +     "star_n X \<in> Infinitesimal ==> \<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>"
    4.89  apply (simp add: Infinitesimal_def ball_SReal_eq)
    4.90  apply (simp add: hnorm_def starfun_star_n star_of_def)
    4.91  apply (simp add: star_less_def starP2_star_n)
    4.92  done
    4.93  
    4.94  lemma FreeUltrafilterNat_Infinitesimal:
    4.95 -     "\<forall>u>0. {n. norm (X n) < u} \<in> \<U> ==> star_n X \<in> Infinitesimal"
    4.96 +     "\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U> ==> star_n X \<in> Infinitesimal"
    4.97  apply (simp add: Infinitesimal_def ball_SReal_eq)
    4.98  apply (simp add: hnorm_def starfun_star_n star_of_def)
    4.99  apply (simp add: star_less_def starP2_star_n)
   4.100  done
   4.101  
   4.102  lemma Infinitesimal_FreeUltrafilterNat_iff:
   4.103 -     "(star_n X \<in> Infinitesimal) = (\<forall>u>0. {n. norm (X n) < u} \<in> \<U>)"
   4.104 +     "(star_n X \<in> Infinitesimal) = (\<forall>u>0. eventually (\<lambda>n. norm (X n) < u) \<U>)"
   4.105  by (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
   4.106  
   4.107  (*------------------------------------------------------------------------
   4.108 @@ -2087,14 +2089,13 @@
   4.109  done
   4.110  
   4.111  lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
   4.112 -     "{n. abs(real n) \<le> u} \<notin> FreeUltrafilterNat"
   4.113 +     "\<not> eventually (\<lambda>n. abs(real n) \<le> u) FreeUltrafilterNat"
   4.114  by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
   4.115  
   4.116 -lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat"
   4.117 -apply (rule ccontr, drule FreeUltrafilterNat.not_memD)
   4.118 -apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \<le> u}")
   4.119 -prefer 2 apply force
   4.120 -apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat.finite])
   4.121 +lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
   4.122 +apply (rule FreeUltrafilterNat.finite')
   4.123 +apply (subgoal_tac "{n::nat. \<not> u < real n} = {n. real n \<le> u}")
   4.124 +apply (auto simp add: finite_real_of_nat_le_real)
   4.125  done
   4.126  
   4.127  (*--------------------------------------------------------------
   4.128 @@ -2108,10 +2109,8 @@
   4.129  
   4.130  text{*@{term omega} is a member of @{term HInfinite}*}
   4.131  
   4.132 -lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> FreeUltrafilterNat"
   4.133 -apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat)
   4.134 -apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_real_le_eq)
   4.135 -done
   4.136 +lemma FreeUltrafilterNat_omega: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
   4.137 +  by (fact FreeUltrafilterNat_nat_gt_real)
   4.138  
   4.139  theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
   4.140  apply (simp add: omega_def)
   4.141 @@ -2165,7 +2164,7 @@
   4.142  by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real)
   4.143  
   4.144  lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
   4.145 -     "0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
   4.146 +     "0 < u ==> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) FreeUltrafilterNat"
   4.147  by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
   4.148  
   4.149  (*--------------------------------------------------------------
   4.150 @@ -2179,9 +2178,9 @@
   4.151  
   4.152  
   4.153  lemma FreeUltrafilterNat_inverse_real_of_posnat:
   4.154 -     "0 < u ==>
   4.155 -      {n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
   4.156 -by (metis Compl_le_inverse_eq FreeUltrafilterNat.ultra inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
   4.157 +     "0 < u ==> eventually (\<lambda>n. inverse(real(Suc n)) < u) FreeUltrafilterNat"
   4.158 +by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
   4.159 +   (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
   4.160  
   4.161  text{* Example of an hypersequence (i.e. an extended standard sequence)
   4.162     whose term with an hypernatural suffix is an infinitesimal i.e.
   4.163 @@ -2208,8 +2207,8 @@
   4.164       "\<forall>n. norm(X n - x) < inverse(real(Suc n))
   4.165       ==> star_n X - star_of x \<in> Infinitesimal"
   4.166  unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
   4.167 -by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int 
   4.168 -         intro: order_less_trans FreeUltrafilterNat.subset)
   4.169 +by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat  
   4.170 +         intro: order_less_trans elim!: eventually_elim1)
   4.171  
   4.172  lemma real_seq_to_hypreal_approx:
   4.173       "\<forall>n. norm(X n - x) < inverse(real(Suc n))
   4.174 @@ -2225,7 +2224,7 @@
   4.175       "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
   4.176        ==> star_n X - star_n Y \<in> Infinitesimal"
   4.177  unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
   4.178 -by (auto dest: FreeUltrafilterNat_inverse_real_of_posnat
   4.179 -         intro: order_less_trans FreeUltrafilterNat.subset)
   4.180 +by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
   4.181 +         intro: order_less_trans elim!: eventually_elim1)
   4.182  
   4.183  end
     5.1 --- a/src/HOL/NSA/Star.thy	Sun Apr 12 11:34:09 2015 +0200
     5.2 +++ b/src/HOL/NSA/Star.thy	Sun Apr 12 11:34:16 2015 +0200
     5.3 @@ -22,8 +22,8 @@
     5.4  definition
     5.5    (* nonstandard extension of function *)
     5.6    is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
     5.7 -  "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
     5.8 -                        ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
     5.9 +  "is_starext F f =
    5.10 +    (\<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>)))"
    5.11  
    5.12  definition
    5.13    (* internal functions *)
    5.14 @@ -71,7 +71,7 @@
    5.15  lemma STAR_real_seq_to_hypreal:
    5.16      "\<forall>n. (X n) \<notin> M ==> star_n X \<notin> *s* M"
    5.17  apply (unfold starset_def star_of_def)
    5.18 -apply (simp add: Iset_star_n)
    5.19 +apply (simp add: Iset_star_n FreeUltrafilterNat.proper)
    5.20  done
    5.21  
    5.22  lemma STAR_singleton: "*s* {x} = {star_of x}"
    5.23 @@ -304,9 +304,7 @@
    5.24     In this theory since @{text hypreal_hrabs} proved here. Maybe
    5.25     move both theorems??*}
    5.26  lemma Infinitesimal_FreeUltrafilterNat_iff2:
    5.27 -     "(star_n X \<in> Infinitesimal) =
    5.28 -      (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
    5.29 -                \<in>  FreeUltrafilterNat)"
    5.30 +     "(star_n X \<in> Infinitesimal) = (\<forall>m. eventually (\<lambda>n. norm(X n) < inverse(real(Suc m))) \<U>)"
    5.31  by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
    5.32       hnorm_def star_of_nat_def starfun_star_n
    5.33       star_n_inverse star_n_less real_of_nat_def)
    5.34 @@ -318,11 +316,11 @@
    5.35        HNatInfinite_FreeUltrafilterNat_iff
    5.36        Infinitesimal_FreeUltrafilterNat_iff2)
    5.37  apply (drule_tac x="Suc m" in spec)
    5.38 -apply (erule ultra, simp)
    5.39 +apply (auto elim!: eventually_elim1)
    5.40  done
    5.41  
    5.42  lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
    5.43 -      (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
    5.44 +      (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
    5.45  apply (subst approx_minus_iff)
    5.46  apply (rule mem_infmal_iff [THEN subst])
    5.47  apply (simp add: star_n_diff)
    5.48 @@ -330,8 +328,7 @@
    5.49  done
    5.50  
    5.51  lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
    5.52 -      (\<forall>m. {n. norm (X n - Y n) <
    5.53 -                  inverse(real(Suc m))} : FreeUltrafilterNat)"
    5.54 +      (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse(real(Suc m))) \<U>)"
    5.55  apply (subst approx_minus_iff)
    5.56  apply (rule mem_infmal_iff [THEN subst])
    5.57  apply (simp add: star_n_diff)
    5.58 @@ -342,7 +339,7 @@
    5.59  apply (rule inj_onI)
    5.60  apply (rule ext, rule ccontr)
    5.61  apply (drule_tac x = "star_n (%n. xa)" in fun_cong)
    5.62 -apply (auto simp add: starfun star_n_eq_iff)
    5.63 +apply (auto simp add: starfun star_n_eq_iff FreeUltrafilterNat.proper)
    5.64  done
    5.65  
    5.66  end
     6.1 --- a/src/HOL/NSA/StarDef.thy	Sun Apr 12 11:34:09 2015 +0200
     6.2 +++ b/src/HOL/NSA/StarDef.thy	Sun Apr 12 11:34:16 2015 +0200
     6.3 @@ -11,7 +11,7 @@
     6.4  subsection {* A Free Ultrafilter over the Naturals *}
     6.5  
     6.6  definition
     6.7 -  FreeUltrafilterNat :: "nat set set"  ("\<U>") where
     6.8 +  FreeUltrafilterNat :: "nat filter"  ("\<U>") where
     6.9    "\<U> = (SOME U. freeultrafilter U)"
    6.10  
    6.11  lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
    6.12 @@ -24,19 +24,11 @@
    6.13  interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
    6.14  by (rule freeultrafilter_FreeUltrafilterNat)
    6.15  
    6.16 -text {* This rule takes the place of the old ultra tactic *}
    6.17 -
    6.18 -lemma ultra:
    6.19 -  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
    6.20 -by (simp add: Collect_imp_eq
    6.21 -    FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff)
    6.22 -
    6.23 -
    6.24  subsection {* Definition of @{text star} type constructor *}
    6.25  
    6.26  definition
    6.27    starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
    6.28 -  "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
    6.29 +  "starrel = {(X,Y). eventually (\<lambda>n. X n = Y n) \<U>}"
    6.30  
    6.31  definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
    6.32  
    6.33 @@ -59,14 +51,14 @@
    6.34  
    6.35  text {* Proving that @{term starrel} is an equivalence relation *}
    6.36  
    6.37 -lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
    6.38 +lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = (eventually (\<lambda>n. X n = Y n) \<U>)"
    6.39  by (simp add: starrel_def)
    6.40  
    6.41  lemma equiv_starrel: "equiv UNIV starrel"
    6.42  proof (rule equivI)
    6.43    show "refl starrel" by (simp add: refl_on_def)
    6.44    show "sym starrel" by (simp add: sym_def eq_commute)
    6.45 -  show "trans starrel" by (auto intro: transI elim!: ultra)
    6.46 +  show "trans starrel" by (intro transI) (auto elim: eventually_elim2)
    6.47  qed
    6.48  
    6.49  lemmas equiv_starrel_iff =
    6.50 @@ -75,7 +67,7 @@
    6.51  lemma starrel_in_star: "starrel``{x} \<in> star"
    6.52  by (simp add: star_def quotientI)
    6.53  
    6.54 -lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
    6.55 +lemma star_n_eq_iff: "(star_n X = star_n Y) = (eventually (\<lambda>n. X n = Y n) \<U>)"
    6.56  by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
    6.57  
    6.58  
    6.59 @@ -83,8 +75,8 @@
    6.60  
    6.61  text {* This introduction rule starts each transfer proof. *}
    6.62  lemma transfer_start:
    6.63 -  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    6.64 -by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
    6.65 +  "P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    6.66 +  by (simp add: FreeUltrafilterNat.proper)
    6.67  
    6.68  text {*Initialize transfer tactic.*}
    6.69  ML_file "transfer.ML"
    6.70 @@ -98,66 +90,66 @@
    6.71  text {* Transfer introduction rules. *}
    6.72  
    6.73  lemma transfer_ex [transfer_intro]:
    6.74 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
    6.75 -    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
    6.76 -by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex)
    6.77 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
    6.78 +    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> eventually (\<lambda>n. \<exists>x. P n x) \<U>"
    6.79 +by (simp only: ex_star_eq eventually_ex)
    6.80  
    6.81  lemma transfer_all [transfer_intro]:
    6.82 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
    6.83 -    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
    6.84 -by (simp only: all_star_eq FreeUltrafilterNat.Collect_all)
    6.85 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
    6.86 +    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> eventually (\<lambda>n. \<forall>x. P n x) \<U>"
    6.87 +by (simp only: all_star_eq FreeUltrafilterNat.eventually_all_iff)
    6.88  
    6.89  lemma transfer_not [transfer_intro]:
    6.90 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
    6.91 -by (simp only: FreeUltrafilterNat.Collect_not)
    6.92 +  "\<lbrakk>p \<equiv> eventually P \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> eventually (\<lambda>n. \<not> P n) \<U>"
    6.93 +by (simp only: FreeUltrafilterNat.eventually_not_iff)
    6.94  
    6.95  lemma transfer_conj [transfer_intro]:
    6.96 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
    6.97 -    \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
    6.98 -by (simp only: FreeUltrafilterNat.Collect_conj)
    6.99 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   6.100 +    \<Longrightarrow> p \<and> q \<equiv> eventually (\<lambda>n. P n \<and> Q n) \<U>"
   6.101 +by (simp only: eventually_conj_iff)
   6.102  
   6.103  lemma transfer_disj [transfer_intro]:
   6.104 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   6.105 -    \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
   6.106 -by (simp only: FreeUltrafilterNat.Collect_disj)
   6.107 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   6.108 +    \<Longrightarrow> p \<or> q \<equiv> eventually (\<lambda>n. P n \<or> Q n) \<U>"
   6.109 +by (simp only: FreeUltrafilterNat.eventually_disj_iff)
   6.110  
   6.111  lemma transfer_imp [transfer_intro]:
   6.112 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   6.113 -    \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
   6.114 -by (simp only: imp_conv_disj transfer_disj transfer_not)
   6.115 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   6.116 +    \<Longrightarrow> p \<longrightarrow> q \<equiv> eventually (\<lambda>n. P n \<longrightarrow> Q n) \<U>"
   6.117 +by (simp only: FreeUltrafilterNat.eventually_imp_iff)
   6.118  
   6.119  lemma transfer_iff [transfer_intro]:
   6.120 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   6.121 -    \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
   6.122 -by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
   6.123 +  "\<lbrakk>p \<equiv> eventually P \<U>; q \<equiv> eventually Q \<U>\<rbrakk>
   6.124 +    \<Longrightarrow> p = q \<equiv> eventually (\<lambda>n. P n = Q n) \<U>"
   6.125 +by (simp only: FreeUltrafilterNat.eventually_iff_iff)
   6.126  
   6.127  lemma transfer_if_bool [transfer_intro]:
   6.128 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
   6.129 -    \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
   6.130 +  "\<lbrakk>p \<equiv> eventually P \<U>; x \<equiv> eventually X \<U>; y \<equiv> eventually Y \<U>\<rbrakk>
   6.131 +    \<Longrightarrow> (if p then x else y) \<equiv> eventually (\<lambda>n. if P n then X n else Y n) \<U>"
   6.132  by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
   6.133  
   6.134  lemma transfer_eq [transfer_intro]:
   6.135 -  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
   6.136 +  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> eventually (\<lambda>n. X n = Y n) \<U>"
   6.137  by (simp only: star_n_eq_iff)
   6.138  
   6.139  lemma transfer_if [transfer_intro]:
   6.140 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
   6.141 +  "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
   6.142      \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
   6.143  apply (rule eq_reflection)
   6.144 -apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
   6.145 +apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1)
   6.146  done
   6.147  
   6.148  lemma transfer_fun_eq [transfer_intro]:
   6.149    "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
   6.150 -    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
   6.151 -      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
   6.152 +    \<equiv> eventually (\<lambda>n. F n (X n) = G n (X n)) \<U>\<rbrakk>
   6.153 +      \<Longrightarrow> f = g \<equiv> eventually (\<lambda>n. F n = G n) \<U>"
   6.154  by (simp only: fun_eq_iff transfer_all)
   6.155  
   6.156  lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
   6.157  by (rule reflexive)
   6.158  
   6.159 -lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
   6.160 -by (simp add: atomize_eq)
   6.161 +lemma transfer_bool [transfer_intro]: "p \<equiv> eventually (\<lambda>n. p) \<U>"
   6.162 +by (simp add: FreeUltrafilterNat.proper)
   6.163  
   6.164  
   6.165  subsection {* Standard elements *}
   6.166 @@ -191,7 +183,7 @@
   6.167  
   6.168  lemma Ifun_congruent2:
   6.169    "congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})"
   6.170 -by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
   6.171 +by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp)
   6.172  
   6.173  lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
   6.174  by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
   6.175 @@ -298,7 +290,7 @@
   6.176  definition unstar :: "bool star \<Rightarrow> bool" where
   6.177    "unstar b \<longleftrightarrow> b = star_of True"
   6.178  
   6.179 -lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
   6.180 +lemma unstar_star_n: "unstar (star_n P) = (eventually P \<U>)"
   6.181  by (simp add: unstar_def star_of_def star_n_eq_iff)
   6.182  
   6.183  lemma unstar_star_of [simp]: "unstar (star_of p) = p"
   6.184 @@ -308,7 +300,7 @@
   6.185  setup {* Transfer_Principle.add_const @{const_name unstar} *}
   6.186  
   6.187  lemma transfer_unstar [transfer_intro]:
   6.188 -  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
   6.189 +  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
   6.190  by (simp only: unstar_star_n)
   6.191  
   6.192  definition
   6.193 @@ -322,11 +314,11 @@
   6.194  declare starP_def [transfer_unfold]
   6.195  declare starP2_def [transfer_unfold]
   6.196  
   6.197 -lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
   6.198 +lemma starP_star_n: "( *p* P) (star_n X) = (eventually (\<lambda>n. P (X n)) \<U>)"
   6.199  by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
   6.200  
   6.201  lemma starP2_star_n:
   6.202 -  "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
   6.203 +  "( *p2* P) (star_n X) (star_n Y) = (eventually (\<lambda>n. P (X n) (Y n)) \<U>)"
   6.204  by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
   6.205  
   6.206  lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
   6.207 @@ -343,7 +335,7 @@
   6.208    "Iset A = {x. ( *p2* op \<in>) x A}"
   6.209  
   6.210  lemma Iset_star_n:
   6.211 -  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
   6.212 +  "(star_n X \<in> Iset (star_n A)) = (eventually (\<lambda>n. X n \<in> A n) \<U>)"
   6.213  by (simp add: Iset_def starP2_star_n)
   6.214  
   6.215  text {* Transfer tactic should remove occurrences of @{term Iset} *}
   6.216 @@ -351,27 +343,27 @@
   6.217  
   6.218  lemma transfer_mem [transfer_intro]:
   6.219    "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
   6.220 -    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
   6.221 +    \<Longrightarrow> x \<in> a \<equiv> eventually (\<lambda>n. X n \<in> A n) \<U>"
   6.222  by (simp only: Iset_star_n)
   6.223  
   6.224  lemma transfer_Collect [transfer_intro]:
   6.225 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   6.226 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
   6.227      \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
   6.228  by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n)
   6.229  
   6.230  lemma transfer_set_eq [transfer_intro]:
   6.231    "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
   6.232 -    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
   6.233 +    \<Longrightarrow> a = b \<equiv> eventually (\<lambda>n. A n = B n) \<U>"
   6.234  by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem)
   6.235  
   6.236  lemma transfer_ball [transfer_intro]:
   6.237 -  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   6.238 -    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
   6.239 +  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
   6.240 +    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<forall>x\<in>A n. P n x) \<U>"
   6.241  by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
   6.242  
   6.243  lemma transfer_bex [transfer_intro]:
   6.244 -  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   6.245 -    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
   6.246 +  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
   6.247 +    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> eventually (\<lambda>n. \<exists>x\<in>A n. P n x) \<U>"
   6.248  by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
   6.249  
   6.250  lemma transfer_Iset [transfer_intro]: