(* Title : Filter.thy ID : $Id: Filter.thy,v 1.6 2005/09/12 21:14:41 huffman Exp $ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Conversion to Isar and new proofs by Lawrence C Paulson, 2004 Conversion to locales by Brian Huffman, 2005 *) header {* Filters and Ultrafilters *} theory Filter imports Zorn begin subsection {* Definitions and basic properties *} subsubsection {* Filters *} locale filter = fixes F :: "'a set set" assumes UNIV [iff]: "UNIV ∈ F" assumes empty [iff]: "{} ∉ F" assumes Int: "[|u ∈ F; v ∈ F|] ==> u ∩ v ∈ F" assumes subset: "[|u ∈ F; u ⊆ v|] ==> v ∈ F" lemma (in filter) memD: "A ∈ F ==> - A ∉ F" proof assume "A ∈ F" and "- A ∈ F" hence "A ∩ (- A) ∈ F" by (rule Int) thus "False" by simp qed lemma (in filter) not_memI: "- A ∈ F ==> A ∉ F" by (drule memD, simp) lemma (in filter) Int_iff: "(x ∩ y ∈ F) = (x ∈ F ∧ y ∈ F)" by (auto elim: subset intro: Int) subsubsection {* Ultrafilters *} locale ultrafilter = filter + assumes ultra: "A ∈ F ∨ - A ∈ F" lemma (in ultrafilter) memI: "- A ∉ F ==> A ∈ F" by (cut_tac ultra [of A], simp) lemma (in ultrafilter) not_memD: "A ∉ F ==> - A ∈ F" by (rule memI, simp) lemma (in ultrafilter) not_mem_iff: "(A ∉ F) = (- A ∈ F)" by (rule iffI [OF not_memD not_memI]) lemma (in ultrafilter) Compl_iff: "(- A ∈ F) = (A ∉ F)" by (rule iffI [OF not_memI not_memD]) lemma (in ultrafilter) Un_iff: "(x ∪ y ∈ F) = (x ∈ F ∨ y ∈ F)" apply (rule iffI) apply (erule contrapos_pp) apply (simp add: Int_iff not_mem_iff) apply (auto elim: subset) done subsubsection {* Free Ultrafilters *} locale freeultrafilter = ultrafilter + assumes infinite: "A ∈ F ==> infinite A" lemma (in freeultrafilter) finite: "finite A ==> A ∉ F" by (erule contrapos_pn, erule infinite) lemma (in freeultrafilter) filter: "filter F" . lemma (in freeultrafilter) ultrafilter: "ultrafilter F" by (rule ultrafilter.intro) subsection {* Collect properties *} lemma (in filter) Collect_ex: "({n. ∃x. P n x} ∈ F) = (∃X. {n. P n (X n)} ∈ F)" proof assume "{n. ∃x. P n x} ∈ F" hence "{n. P n (SOME x. P n x)} ∈ F" by (auto elim: someI subset) thus "∃X. {n. P n (X n)} ∈ F" by fast next show "∃X. {n. P n (X n)} ∈ F ==> {n. ∃x. P n x} ∈ F" by (auto elim: subset) qed lemma (in filter) Collect_conj: "({n. P n ∧ Q n} ∈ F) = ({n. P n} ∈ F ∧ {n. Q n} ∈ F)" by (subst Collect_conj_eq, rule Int_iff) lemma (in ultrafilter) Collect_not: "({n. ¬ P n} ∈ F) = ({n. P n} ∉ F)" by (subst Collect_neg_eq, rule Compl_iff) lemma (in ultrafilter) Collect_disj: "({n. P n ∨ Q n} ∈ F) = ({n. P n} ∈ F ∨ {n. Q n} ∈ F)" by (subst Collect_disj_eq, rule Un_iff) lemma (in ultrafilter) Collect_all: "({n. ∀x. P n x} ∈ F) = (∀X. {n. P n (X n)} ∈ F)" apply (rule Not_eq_iff [THEN iffD1]) apply (simp add: Collect_not [symmetric]) apply (rule Collect_ex) done subsection {* Maximal filter = Ultrafilter *} text {* A filter F is an ultrafilter iff it is a maximal filter, i.e. whenever G is a filter and @{term "F ⊆ G"} then @{term "F = G"} *} text {* Lemmas that shows existence of an extension to what was assumed to be a maximal filter. Will be used to derive contradiction in proof of property of ultrafilter. *} lemma extend_lemma1: "UNIV ∈ F ==> A ∈ {X. ∃f∈F. A ∩ f ⊆ X}" by blast lemma extend_lemma2: "F ⊆ {X. ∃f∈F. A ∩ f ⊆ X}" by blast lemma (in filter) extend_filter: assumes A: "- A ∉ F" shows "filter {X. ∃f∈F. A ∩ f ⊆ X}" (is "filter ?X") proof (rule filter.intro) show "UNIV ∈ ?X" by blast next show "{} ∉ ?X" proof (clarify) fix f assume f: "f ∈ F" and Af: "A ∩ f ⊆ {}" from Af have fA: "f ⊆ - A" by blast from f fA have "- A ∈ F" by (rule subset) with A show "False" by simp qed next fix u and v assume u: "u ∈ ?X" and v: "v ∈ ?X" from u obtain f where f: "f ∈ F" and Af: "A ∩ f ⊆ u" by blast from v obtain g where g: "g ∈ F" and Ag: "A ∩ g ⊆ v" by blast from f g have fg: "f ∩ g ∈ F" by (rule Int) from Af Ag have Afg: "A ∩ (f ∩ g) ⊆ u ∩ v" by blast from fg Afg show "u ∩ v ∈ ?X" by blast next fix u and v assume uv: "u ⊆ v" and u: "u ∈ ?X" from u obtain f where f: "f ∈ F" and Afu: "A ∩ f ⊆ u" by blast from Afu uv have Afv: "A ∩ f ⊆ v" by blast from f Afv have "∃f∈F. A ∩ f ⊆ v" by blast thus "v ∈ ?X" by simp qed lemma (in filter) max_filter_ultrafilter: assumes max: "!!G. [|filter G; F ⊆ G|] ==> F = G" shows "ultrafilter_axioms F" proof (rule ultrafilter_axioms.intro) fix A show "A ∈ F ∨ - A ∈ F" proof (rule disjCI) let ?X = "{X. ∃f∈F. A ∩ f ⊆ X}" assume AF: "- A ∉ F" from AF have X: "filter ?X" by (rule extend_filter) from UNIV have AX: "A ∈ ?X" by (rule extend_lemma1) have FX: "F ⊆ ?X" by (rule extend_lemma2) from X FX have "F = ?X" by (rule max) with AX show "A ∈ F" by simp qed qed lemma (in ultrafilter) max_filter: assumes G: "filter G" and sub: "F ⊆ G" shows "F = G" proof show "F ⊆ G" . show "G ⊆ F" proof fix A assume A: "A ∈ G" from G A have "- A ∉ G" by (rule filter.memD) with sub have B: "- A ∉ F" by blast thus "A ∈ F" by (rule memI) qed qed subsection {* Ultrafilter Theorem *} text "A locale makes proof of ultrafilter Theorem more modular" locale (open) UFT = fixes frechet :: "'a set set" and superfrechet :: "'a set set set" assumes infinite_UNIV: "infinite (UNIV :: 'a set)" defines frechet_def: "frechet ≡ {A. finite (- A)}" and superfrechet_def: "superfrechet ≡ {G. filter G ∧ frechet ⊆ G}" lemma (in UFT) superfrechetI: "[|filter G; frechet ⊆ G|] ==> G ∈ superfrechet" by (simp add: superfrechet_def) lemma (in UFT) superfrechetD1: "G ∈ superfrechet ==> filter G" by (simp add: superfrechet_def) lemma (in UFT) superfrechetD2: "G ∈ superfrechet ==> frechet ⊆ G" by (simp add: superfrechet_def) text {* A few properties of free filters *} lemma filter_cofinite: assumes inf: "infinite (UNIV :: 'a set)" shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F") proof (rule filter.intro) show "UNIV ∈ ?F" by simp next show "{} ∉ ?F" by simp next fix u v assume "u ∈ ?F" and "v ∈ ?F" thus "u ∩ v ∈ ?F" by simp next fix u v assume uv: "u ⊆ v" and u: "u ∈ ?F" from uv have vu: "- v ⊆ - u" by simp from u show "v ∈ ?F" by (simp add: finite_subset [OF vu]) qed text {* We prove: 1. Existence of maximal filter i.e. ultrafilter; 2. Freeness property i.e ultrafilter is free. Use a locale to prove various lemmas and then export main result: The ultrafilter Theorem *} lemma (in UFT) filter_frechet: "filter frechet" by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV]) lemma (in UFT) frechet_in_superfrechet: "frechet ∈ superfrechet" by (rule superfrechetI [OF filter_frechet subset_refl]) lemma (in UFT) lemma_mem_chain_filter: "[|c ∈ chain superfrechet; x ∈ c|] ==> filter x" by (unfold chain_def superfrechet_def, blast) subsubsection {* Unions of chains of superfrechets *} text "In this section we prove that superfrechet is closed with respect to unions of non-empty chains. We must show 1) Union of a chain is a filter, 2) Union of a chain contains frechet. Number 2 is trivial, but 1 requires us to prove all the filter rules." lemma (in UFT) Union_chain_UNIV: "[|c ∈ chain superfrechet; c ≠ {}|] ==> UNIV ∈ \<Union>c" proof - assume 1: "c ∈ chain superfrechet" and 2: "c ≠ {}" from 2 obtain x where 3: "x ∈ c" by blast from 1 3 have "filter x" by (rule lemma_mem_chain_filter) hence "UNIV ∈ x" by (rule filter.UNIV) with 3 show "UNIV ∈ \<Union>c" by blast qed lemma (in UFT) Union_chain_empty: "c ∈ chain superfrechet ==> {} ∉ \<Union>c" proof assume 1: "c ∈ chain superfrechet" and 2: "{} ∈ \<Union>c" from 2 obtain x where 3: "x ∈ c" and 4: "{} ∈ x" .. from 1 3 have "filter x" by (rule lemma_mem_chain_filter) hence "{} ∉ x" by (rule filter.empty) with 4 show "False" by simp qed lemma (in UFT) Union_chain_Int: "[|c ∈ chain superfrechet; u ∈ \<Union>c; v ∈ \<Union>c|] ==> u ∩ v ∈ \<Union>c" proof - assume c: "c ∈ chain superfrechet" assume "u ∈ \<Union>c" then obtain x where ux: "u ∈ x" and xc: "x ∈ c" .. assume "v ∈ \<Union>c" then obtain y where vy: "v ∈ y" and yc: "y ∈ c" .. from c xc yc have "x ⊆ y ∨ y ⊆ x" by (rule chainD) with xc yc have xyc: "x ∪ y ∈ c" by (auto simp add: Un_absorb1 Un_absorb2) with c have fxy: "filter (x ∪ y)" by (rule lemma_mem_chain_filter) from ux have uxy: "u ∈ x ∪ y" by simp from vy have vxy: "v ∈ x ∪ y" by simp from fxy uxy vxy have "u ∩ v ∈ x ∪ y" by (rule filter.Int) with xyc show "u ∩ v ∈ \<Union>c" .. qed lemma (in UFT) Union_chain_subset: "[|c ∈ chain superfrechet; u ∈ \<Union>c; u ⊆ v|] ==> v ∈ \<Union>c" proof - assume c: "c ∈ chain superfrechet" and u: "u ∈ \<Union>c" and uv: "u ⊆ v" from u obtain x where ux: "u ∈ x" and xc: "x ∈ c" .. from c xc have fx: "filter x" by (rule lemma_mem_chain_filter) from fx ux uv have vx: "v ∈ x" by (rule filter.subset) with xc show "v ∈ \<Union>c" .. qed lemma (in UFT) Union_chain_filter: assumes "c ∈ chain superfrechet" and "c ≠ {}" shows "filter (\<Union>c)" proof (rule filter.intro) show "UNIV ∈ \<Union>c" by (rule Union_chain_UNIV) next show "{} ∉ \<Union>c" by (rule Union_chain_empty) next fix u v assume "u ∈ \<Union>c" and "v ∈ \<Union>c" show "u ∩ v ∈ \<Union>c" by (rule Union_chain_Int) next fix u v assume "u ∈ \<Union>c" and "u ⊆ v" show "v ∈ \<Union>c" by (rule Union_chain_subset) qed lemma (in UFT) lemma_mem_chain_frechet_subset: "[|c ∈ chain superfrechet; x ∈ c|] ==> frechet ⊆ x" by (unfold superfrechet_def chain_def, blast) lemma (in UFT) Union_chain_superfrechet: "[|c ≠ {}; c ∈ chain superfrechet|] ==> \<Union>c ∈ superfrechet" proof (rule superfrechetI) assume 1: "c ∈ chain superfrechet" and 2: "c ≠ {}" thus "filter (\<Union>c)" by (rule Union_chain_filter) from 2 obtain x where 3: "x ∈ c" by blast from 1 3 have "frechet ⊆ x" by (rule lemma_mem_chain_frechet_subset) also from 3 have "x ⊆ \<Union>c" by blast finally show "frechet ⊆ \<Union>c" . qed subsubsection {* Existence of free ultrafilter *} lemma (in UFT) max_cofinite_filter_Ex: "∃U∈superfrechet. ∀G∈superfrechet. U ⊆ G --> U = G" proof (rule Zorn_Lemma2 [rule_format]) fix c assume c: "c ∈ chain superfrechet" show "∃U∈superfrechet. ∀G∈c. G ⊆ U" (is "?U") proof (cases) assume "c = {}" with frechet_in_superfrechet show "?U" by blast next assume A: "c ≠ {}" from A c have "\<Union>c ∈ superfrechet" by (rule Union_chain_superfrechet) thus "?U" by blast qed qed lemma (in UFT) mem_superfrechet_all_infinite: "[|U ∈ superfrechet; A ∈ U|] ==> infinite A" proof assume U: "U ∈ superfrechet" and A: "A ∈ U" and fin: "finite A" from U have fil: "filter U" and fre: "frechet ⊆ U" by (simp_all add: superfrechet_def) from fin have "- A ∈ frechet" by (simp add: frechet_def) with fre have cA: "- A ∈ U" by (rule subsetD) from fil A cA have "A ∩ - A ∈ U" by (rule filter.Int) with fil show "False" by (simp add: filter.empty) qed text {* There exists a free ultrafilter on any infinite set *} lemma (in UFT) freeultrafilter_ex: "∃U::'a set set. freeultrafilter U" proof - from max_cofinite_filter_Ex obtain U where U: "U ∈ superfrechet" and max [rule_format]: "∀G∈superfrechet. U ⊆ G --> U = G" .. from U have fil: "filter U" by (rule superfrechetD1) from U have fre: "frechet ⊆ 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 ⊆ G" from fre UG have "frechet ⊆ G" by simp with G have "G ∈ superfrechet" by (rule superfrechetI) from this UG show "U = G" by (rule max) qed have free: "freeultrafilter_axioms U" proof (rule freeultrafilter_axioms.intro) fix A assume "A ∈ U" with U show "infinite A" by (rule mem_superfrechet_all_infinite) qed from fil ultra free have "freeultrafilter U" by (rule freeultrafilter.intro) thus ?thesis .. qed lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex end
lemma memD:
[| Filter.filter F; A ∈ F |] ==> - A ∉ F
lemma not_memI:
[| Filter.filter F; - A ∈ F |] ==> A ∉ F
lemma Int_iff:
Filter.filter F ==> (x ∩ y ∈ F) = (x ∈ F ∧ y ∈ F)
lemma memI:
[| ultrafilter F; - A ∉ F |] ==> A ∈ F
lemma not_memD:
[| ultrafilter F; A ∉ F |] ==> - A ∈ F
lemma not_mem_iff:
ultrafilter F ==> (A ∉ F) = (- A ∈ F)
lemma Compl_iff:
ultrafilter F ==> (- A ∈ F) = (A ∉ F)
lemma Un_iff:
ultrafilter F ==> (x ∪ y ∈ F) = (x ∈ F ∨ y ∈ F)
lemma finite:
[| freeultrafilter F; finite A |] ==> A ∉ F
lemma filter:
freeultrafilter F ==> Filter.filter F
lemma ultrafilter:
freeultrafilter F ==> ultrafilter F
lemma Collect_ex:
Filter.filter F ==> ({n. ∃x. P n x} ∈ F) = (∃X. {n. P n (X n)} ∈ F)
lemma Collect_conj:
Filter.filter F ==> ({n. P n ∧ Q n} ∈ F) = ({n. P n} ∈ F ∧ {n. Q n} ∈ F)
lemma Collect_not:
ultrafilter F ==> ({n. ¬ P n} ∈ F) = ({n. P n} ∉ F)
lemma Collect_disj:
ultrafilter F ==> ({n. P n ∨ Q n} ∈ F) = ({n. P n} ∈ F ∨ {n. Q n} ∈ F)
lemma Collect_all:
ultrafilter F ==> ({n. ∀x. P n x} ∈ F) = (∀X. {n. P n (X n)} ∈ F)
lemma extend_lemma1:
UNIV ∈ F ==> A ∈ {X. ∃f∈F. A ∩ f ⊆ X}
lemma extend_lemma2:
F ⊆ {X. ∃f∈F. A ∩ f ⊆ X}
lemma extend_filter:
[| Filter.filter F; - A ∉ F |] ==> Filter.filter {X. ∃f∈F. A ∩ f ⊆ X}
lemma max_filter_ultrafilter:
[| Filter.filter F; !!G. [| Filter.filter G; F ⊆ G |] ==> F = G |] ==> ultrafilter_axioms F
lemma max_filter:
[| ultrafilter F; Filter.filter G; F ⊆ G |] ==> F = G
lemma superfrechetI:
[| infinite UNIV; Filter.filter G; {A. finite (- A)} ⊆ G |] ==> G ∈ {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}
lemma superfrechetD1:
[| infinite UNIV; G ∈ {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G} |] ==> Filter.filter G
lemma superfrechetD2:
[| infinite UNIV; G ∈ {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G} |] ==> {A. finite (- A)} ⊆ G
lemma filter_cofinite:
infinite UNIV ==> Filter.filter {A. finite (- A)}
lemma filter_frechet:
infinite UNIV ==> Filter.filter {A. finite (- A)}
lemma frechet_in_superfrechet:
infinite UNIV ==> {A. finite (- A)} ∈ {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}
lemma lemma_mem_chain_filter:
[| infinite UNIV; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}; x ∈ c |] ==> Filter.filter x
lemma Union_chain_UNIV:
[| infinite UNIV; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}; c ≠ {} |] ==> UNIV ∈ Union c
lemma Union_chain_empty:
[| infinite UNIV; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G} |] ==> {} ∉ Union c
lemma Union_chain_Int:
[| infinite UNIV; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}; u ∈ Union c; v ∈ Union c |] ==> u ∩ v ∈ Union c
lemma Union_chain_subset:
[| infinite UNIV; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}; u ∈ Union c; u ⊆ v |] ==> v ∈ Union c
lemma Union_chain_filter:
[| infinite UNIV; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}; c ≠ {} |] ==> Filter.filter (Union c)
lemma lemma_mem_chain_frechet_subset:
[| infinite UNIV; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}; x ∈ c |] ==> {A. finite (- A)} ⊆ x
lemma Union_chain_superfrechet:
[| infinite UNIV; c ≠ {}; c ∈ chain {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G} |] ==> Union c ∈ {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}
lemma max_cofinite_filter_Ex:
infinite UNIV ==> ∃U∈{G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}. ∀G∈{G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}. U ⊆ G --> U = G
lemma mem_superfrechet_all_infinite:
[| infinite UNIV; U ∈ {G. Filter.filter G ∧ {A. finite (- A)} ⊆ G}; A ∈ U |] ==> infinite A
lemma freeultrafilter_ex:
infinite UNIV ==> ∃U. freeultrafilter U
lemmas freeultrafilter_Ex:
infinite UNIV ==> ∃U. freeultrafilter U
lemmas freeultrafilter_Ex:
infinite UNIV ==> ∃U. freeultrafilter U