--- 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
--- 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)"
--- 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])
--- 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
--- 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
--- 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]: