
wenzelm@41959: (*  Title:      HOL/NSA/Filter.thy
wenzelm@41589:     Author:     Jacques D. Fleuriot, University of Cambridge
wenzelm@41589:     Author:     Lawrence C Paulson
wenzelm@41589:     Author:     Brian Huffman
huffman@27468: *) 
huffman@27468: 
huffman@27468: header {* Filters and Ultrafilters *}
huffman@27468: 
huffman@27468: theory Filter
huffman@27468: imports "~~/src/HOL/Library/Zorn" "~~/src/HOL/Library/Infinite_Set"
huffman@27468: begin
huffman@27468: 
huffman@27468: subsection {* Definitions and basic properties *}
huffman@27468: 
huffman@27468: subsubsection {* Filters *}
huffman@27468: 
huffman@27468: locale filter =
huffman@27468:   fixes F :: "'a set set"
huffman@27468:   assumes UNIV [iff]:  "UNIV \<in> F"
huffman@27468:   assumes empty [iff]: "{} \<notin> F"
huffman@27468:   assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
huffman@27468:   assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
huffman@47486: begin
huffman@27468: 
huffman@47486: lemma memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
huffman@27468: proof
huffman@27468:   assume "A \<in> F" and "- A \<in> F"
huffman@27468:   hence "A \<inter> (- A) \<in> F" by (rule Int)
huffman@27468:   thus "False" by simp
huffman@27468: qed
huffman@27468: 
huffman@47486: lemma not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
huffman@27468: by (drule memD, simp)
huffman@27468: 
huffman@47486: lemma Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
huffman@27468: by (auto elim: subset intro: Int)
huffman@27468: 
huffman@47486: end
huffman@47486: 
huffman@27468: subsubsection {* Ultrafilters *}
huffman@27468: 
huffman@27468: locale ultrafilter = filter +
huffman@27468:   assumes ultra: "A \<in> F \<or> - A \<in> F"
huffman@47486: begin
huffman@27468: 
huffman@47486: lemma memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
huffman@47486: using ultra [of A] by simp
huffman@27468: 
huffman@47486: lemma not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
huffman@27468: by (rule memI, simp)
huffman@27468: 
huffman@47486: lemma not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
huffman@27468: by (rule iffI [OF not_memD not_memI])
huffman@27468: 
huffman@47486: lemma Compl_iff: "(- A \<in> F) = (A \<notin> F)"
huffman@27468: by (rule iffI [OF not_memI not_memD])
huffman@27468: 
huffman@47486: lemma Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
huffman@27468:  apply (rule iffI)
huffman@27468:   apply (erule contrapos_pp)
huffman@27468:   apply (simp add: Int_iff not_mem_iff)
huffman@27468:  apply (auto elim: subset)
huffman@27468: done
huffman@27468: 
huffman@47486: end
huffman@47486: 
huffman@27468: subsubsection {* Free Ultrafilters *}
huffman@27468: 
huffman@27468: locale freeultrafilter = ultrafilter +
huffman@27468:   assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
huffman@47486: begin
huffman@27468: 
huffman@47486: lemma finite: "finite A \<Longrightarrow> A \<notin> F"
huffman@27468: by (erule contrapos_pn, erule infinite)
huffman@27468: 
huffman@47486: lemma singleton: "{x} \<notin> F"
huffman@27468: by (rule finite, simp)
huffman@27468: 
huffman@47486: lemma insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
huffman@27468: apply (subst insert_is_Un)
huffman@27468: apply (subst Un_iff)
huffman@27468: apply (simp add: singleton)
huffman@27468: done
huffman@27468: 
huffman@47486: lemma filter: "filter F" ..
huffman@27468: 
huffman@47486: lemma ultrafilter: "ultrafilter F" ..
huffman@27468: 
huffman@47486: end
huffman@27468: 
huffman@27468: subsection {* Collect properties *}
huffman@27468: 
huffman@27468: lemma (in filter) Collect_ex:
huffman@27468:   "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
huffman@27468: proof
huffman@27468:   assume "{n. \<exists>x. P n x} \<in> F"
huffman@27468:   hence "{n. P n (SOME x. P n x)} \<in> F"
huffman@27468:     by (auto elim: someI subset)
huffman@27468:   thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
huffman@27468: next
huffman@27468:   show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
huffman@27468:     by (auto elim: subset)
huffman@27468: qed
huffman@27468: 
huffman@27468: lemma (in filter) Collect_conj:
huffman@27468:   "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
huffman@27468: by (subst Collect_conj_eq, rule Int_iff)
huffman@27468: 
huffman@27468: lemma (in ultrafilter) Collect_not:
huffman@27468:   "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
huffman@27468: by (subst Collect_neg_eq, rule Compl_iff)
huffman@27468: 
huffman@27468: lemma (in ultrafilter) Collect_disj:
huffman@27468:   "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
huffman@27468: by (subst Collect_disj_eq, rule Un_iff)
huffman@27468: 
huffman@27468: lemma (in ultrafilter) Collect_all:
huffman@27468:   "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
huffman@27468: apply (rule Not_eq_iff [THEN iffD1])
huffman@27468: apply (simp add: Collect_not [symmetric])
huffman@27468: apply (rule Collect_ex)
huffman@27468: done
huffman@27468: 
huffman@27468: subsection {* Maximal filter = Ultrafilter *}
huffman@27468: 
huffman@27468: text {*
huffman@27468:    A filter F is an ultrafilter iff it is a maximal filter,
huffman@27468:    i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
huffman@27468: *}
huffman@27468: text {*
huffman@27468:   Lemmas that shows existence of an extension to what was assumed to
huffman@27468:   be a maximal filter. Will be used to derive contradiction in proof of
huffman@27468:   property of ultrafilter.
huffman@27468: *}
huffman@27468: 
huffman@27468: lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
huffman@27468: by blast
huffman@27468: 
huffman@27468: lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
huffman@27468: by blast
huffman@27468: 
huffman@27468: lemma (in filter) extend_filter:
huffman@27468: assumes A: "- A \<notin> F"
huffman@27468: shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
huffman@27468: proof (rule filter.intro)
huffman@27468:   show "UNIV \<in> ?X" by blast
huffman@27468: next
huffman@27468:   show "{} \<notin> ?X"
huffman@27468:   proof (clarify)
huffman@27468:     fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
huffman@27468:     from Af have fA: "f \<subseteq> - A" by blast
huffman@27468:     from f fA have "- A \<in> F" by (rule subset)
huffman@27468:     with A show "False" by simp
huffman@27468:   qed
huffman@27468: next
huffman@27468:   fix u and v
huffman@27468:   assume u: "u \<in> ?X" and v: "v \<in> ?X"
huffman@27468:   from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
huffman@27468:   from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
huffman@27468:   from f g have fg: "f \<inter> g \<in> F" by (rule Int)
huffman@27468:   from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
huffman@27468:   from fg Afg show "u \<inter> v \<in> ?X" by blast
huffman@27468: next
huffman@27468:   fix u and v
huffman@27468:   assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
huffman@27468:   from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
huffman@27468:   from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
huffman@27468:   from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
huffman@27468:   thus "v \<in> ?X" by simp
huffman@27468: qed
huffman@27468: 
huffman@27468: lemma (in filter) max_filter_ultrafilter:
huffman@27468: assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
huffman@27468: shows "ultrafilter_axioms F"
huffman@27468: proof (rule ultrafilter_axioms.intro)
huffman@27468:   fix A show "A \<in> F \<or> - A \<in> F"
huffman@27468:   proof (rule disjCI)
huffman@27468:     let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
huffman@27468:     assume AF: "- A \<notin> F"
huffman@27468:     from AF have X: "filter ?X" by (rule extend_filter)
huffman@27468:     from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
huffman@27468:     have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
huffman@27468:     from X FX have "F = ?X" by (rule max)
huffman@27468:     with AX show "A \<in> F" by simp
huffman@27468:   qed
huffman@27468: qed
huffman@27468: 
huffman@27468: lemma (in ultrafilter) max_filter:
huffman@27468: assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
huffman@27468: proof
huffman@27468:   show "F \<subseteq> G" using sub .
huffman@27468:   show "G \<subseteq> F"
huffman@27468:   proof
huffman@27468:     fix A assume A: "A \<in> G"
huffman@27468:     from G A have "- A \<notin> G" by (rule filter.memD)
huffman@27468:     with sub have B: "- A \<notin> F" by blast
huffman@27468:     thus "A \<in> F" by (rule memI)
huffman@27468:   qed
huffman@27468: qed
huffman@27468: 
huffman@27468: subsection {* Ultrafilter Theorem *}
huffman@27468: 
huffman@47486: text "A local context makes proof of ultrafilter Theorem more modular"
huffman@47486: context
huffman@27468:   fixes   frechet :: "'a set set"
huffman@27468:   and     superfrechet :: "'a set set set"
huffman@27468: 
huffman@27468:   assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
huffman@27468: 
huffman@27468:   defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
huffman@27468:   and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
huffman@47486: begin
huffman@27468: 
huffman@47486: lemma superfrechetI:
huffman@27468:   "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
huffman@27468: by (simp add: superfrechet_def)
huffman@27468: 
huffman@47486: lemma superfrechetD1:
huffman@27468:   "G \<in> superfrechet \<Longrightarrow> filter G"
huffman@27468: by (simp add: superfrechet_def)
huffman@27468: 
huffman@47486: lemma superfrechetD2:
huffman@27468:   "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
huffman@27468: by (simp add: superfrechet_def)
huffman@27468: 
huffman@27468: text {* A few properties of free filters *}
huffman@27468: 
huffman@27468: lemma filter_cofinite:
huffman@27468: assumes inf: "infinite (UNIV :: 'a set)"
huffman@27468: shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
huffman@27468: proof (rule filter.intro)
huffman@27468:   show "UNIV \<in> ?F" by simp
huffman@27468: next
huffman@27468:   show "{} \<notin> ?F" using inf by simp
huffman@27468: next
huffman@27468:   fix u v assume "u \<in> ?F" and "v \<in> ?F"
huffman@27468:   thus "u \<inter> v \<in> ?F" by simp
huffman@27468: next
huffman@27468:   fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
huffman@27468:   from uv have vu: "- v \<subseteq> - u" by simp
huffman@27468:   from u show "v \<in> ?F"
huffman@27468:     by (simp add: finite_subset [OF vu])
huffman@27468: qed
huffman@27468: 
huffman@27468: text {*
huffman@27468:    We prove: 1. Existence of maximal filter i.e. ultrafilter;
huffman@27468:              2. Freeness property i.e ultrafilter is free.
huffman@27468:              Use a locale to prove various lemmas and then 
huffman@27468:              export main result: The ultrafilter Theorem
huffman@27468: *}
huffman@27468: 
huffman@47486: lemma filter_frechet: "filter frechet"
huffman@27468: by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
huffman@27468: 
huffman@47486: lemma frechet_in_superfrechet: "frechet \<in> superfrechet"
huffman@27468: by (rule superfrechetI [OF filter_frechet subset_refl])
huffman@27468: 
huffman@47486: lemma lemma_mem_chain_filter:
popescua@52183:   "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
popescua@52183: by (unfold chains_def superfrechet_def, blast)
huffman@27468: 
huffman@27468: 
huffman@27468: subsubsection {* Unions of chains of superfrechets *}
huffman@27468: 
huffman@27468: text "In this section we prove that superfrechet is closed
huffman@27468: with respect to unions of non-empty chains. We must show
popescua@52183:   1) Union of a chain is afind_theorems name: Union_chain_UNIV filter,
huffman@27468:   2) Union of a chain contains frechet.
huffman@27468: 
huffman@27468: Number 2 is trivial, but 1 requires us to prove all the filter rules."
huffman@27468: 
huffman@47486: lemma Union_chain_UNIV:
popescua@52183:   "\<lbrakk>c \<in> chains superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
huffman@27468: proof -
popescua@52183:   assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
huffman@27468:   from 2 obtain x where 3: "x \<in> c" by blast
huffman@27468:   from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
huffman@27468:   hence "UNIV \<in> x" by (rule filter.UNIV)
huffman@27468:   with 3 show "UNIV \<in> \<Union>c" by blast
huffman@27468: qed
huffman@27468: 
huffman@47486: lemma Union_chain_empty:
popescua@52183:   "c \<in> chains superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
huffman@27468: proof
popescua@52183:   assume 1: "c \<in> chains superfrechet" and 2: "{} \<in> \<Union>c"
huffman@27468:   from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
huffman@27468:   from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
huffman@27468:   hence "{} \<notin> x" by (rule filter.empty)
huffman@27468:   with 4 show "False" by simp
huffman@27468: qed
huffman@27468: 
huffman@47486: lemma Union_chain_Int:
popescua@52183:   "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
huffman@27468: proof -
popescua@52183:   assume c: "c \<in> chains superfrechet"
huffman@27468:   assume "u \<in> \<Union>c"
huffman@27468:     then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
huffman@27468:   assume "v \<in> \<Union>c"
huffman@27468:     then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
popescua@52183:   from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" using c unfolding chains_def chain_subset_def by auto
huffman@27468:   with xc yc have xyc: "x \<union> y \<in> c"
huffman@27468:     by (auto simp add: Un_absorb1 Un_absorb2)
huffman@27468:   with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
huffman@27468:   from ux have uxy: "u \<in> x \<union> y" by simp
huffman@27468:   from vy have vxy: "v \<in> x \<union> y" by simp
huffman@27468:   from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
huffman@27468:   with xyc show "u \<inter> v \<in> \<Union>c" ..
huffman@27468: qed
huffman@27468: 
huffman@47486: lemma Union_chain_subset:
popescua@52183:   "\<lbrakk>c \<in> chains superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
huffman@27468: proof -
popescua@52183:   assume c: "c \<in> chains superfrechet"
huffman@27468:      and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
huffman@27468:   from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
huffman@27468:   from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
huffman@27468:   from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
huffman@27468:   with xc show "v \<in> \<Union>c" ..
huffman@27468: qed
huffman@27468: 
huffman@47486: lemma Union_chain_filter:
popescua@52183: assumes chain: "c \<in> chains superfrechet" and nonempty: "c \<noteq> {}"
popescua@52183: shows "filter (\<Union>c)" 
huffman@27468: proof (rule filter.intro)
huffman@27468:   show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
huffman@27468: next
huffman@27468:   show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
huffman@27468: next
huffman@27468:   fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
huffman@27468:   with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
huffman@27468: next
huffman@27468:   fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
huffman@27468:   with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
huffman@27468: qed
huffman@27468: 
huffman@47486: lemma lemma_mem_chain_frechet_subset:
popescua@52183:   "\<lbrakk>c \<in> chains superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
popescua@52183: by (unfold superfrechet_def chains_def, blast)
huffman@27468: 
huffman@47486: lemma Union_chain_superfrechet:
popescua@52183:   "\<lbrakk>c \<noteq> {}; c \<in> chains superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
huffman@27468: proof (rule superfrechetI)
popescua@52183:   assume 1: "c \<in> chains superfrechet" and 2: "c \<noteq> {}"
huffman@27468:   thus "filter (\<Union>c)" by (rule Union_chain_filter)
huffman@27468:   from 2 obtain x where 3: "x \<in> c" by blast
huffman@27468:   from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
huffman@27468:   also from 3 have "x \<subseteq> \<Union>c" by blast
huffman@27468:   finally show "frechet \<subseteq> \<Union>c" .
huffman@27468: qed
huffman@27468: 
huffman@27468: subsubsection {* Existence of free ultrafilter *}
huffman@27468: 
huffman@47486: lemma max_cofinite_filter_Ex:
popescua@52183:   "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" 
popescua@52183: proof (rule Zorn_Lemma2, safe)
popescua@52183:   fix c assume c: "c \<in> chains superfrechet"
huffman@27468:   show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
huffman@27468:   proof (cases)
huffman@27468:     assume "c = {}"
huffman@27468:     with frechet_in_superfrechet show "?U" by blast
huffman@27468:   next
huffman@27468:     assume A: "c \<noteq> {}"
huffman@27468:     from A c have "\<Union>c \<in> superfrechet"
huffman@27468:       by (rule Union_chain_superfrechet)
huffman@27468:     thus "?U" by blast
huffman@27468:   qed
huffman@27468: qed
huffman@27468: 
huffman@47486: lemma mem_superfrechet_all_infinite:
huffman@27468:   "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
huffman@27468: proof
huffman@27468:   assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
huffman@27468:   from U have fil: "filter U" and fre: "frechet \<subseteq> U"
huffman@27468:     by (simp_all add: superfrechet_def)
huffman@27468:   from fin have "- A \<in> frechet" by (simp add: frechet_def)
huffman@27468:   with fre have cA: "- A \<in> U" by (rule subsetD)
huffman@27468:   from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
huffman@27468:   with fil show "False" by (simp add: filter.empty)
huffman@27468: qed
huffman@27468: 
huffman@27468: text {* There exists a free ultrafilter on any infinite set *}
huffman@27468: 
huffman@47486: lemma freeultrafilter_Ex:
huffman@27468:   "\<exists>U::'a set set. freeultrafilter U"
huffman@27468: proof -
huffman@27468:   from max_cofinite_filter_Ex obtain U
huffman@27468:     where U: "U \<in> superfrechet"
popescua@52183:       and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> G = U" ..
huffman@27468:   from U have fil: "filter U" by (rule superfrechetD1)
huffman@27468:   from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
huffman@27468:   have ultra: "ultrafilter_axioms U"
huffman@27468:   proof (rule filter.max_filter_ultrafilter [OF fil])
huffman@27468:     fix G assume G: "filter G" and UG: "U \<subseteq> G"
huffman@27468:     from fre UG have "frechet \<subseteq> G" by simp
huffman@27468:     with G have "G \<in> superfrechet" by (rule superfrechetI)
popescua@52183:     from this UG show "U = G" by (rule max[symmetric])
huffman@27468:   qed
huffman@27468:   have free: "freeultrafilter_axioms U"
huffman@27468:   proof (rule freeultrafilter_axioms.intro)
huffman@27468:     fix A assume "A \<in> U"
huffman@27468:     with U show "infinite A" by (rule mem_superfrechet_all_infinite)
huffman@27468:   qed
wenzelm@46008:   from fil ultra free have "freeultrafilter U"
wenzelm@46008:     by (rule freeultrafilter.intro [OF ultrafilter.intro])
wenzelm@46008:     (* FIXME: unfold_locales should use chained facts *)
wenzelm@46008:   then show ?thesis ..
huffman@27468: qed
huffman@27468: 
huffman@47486: end
huffman@27468: 
wenzelm@36176: hide_const (open) filter
huffman@27468: 
huffman@27468: end




