(* Title: HOL/NSA/Filter.thy Author: Jacques D. Fleuriot, University of Cambridge Author: Lawrence C Paulson Author: Brian Huffman *) header {* Filters and Ultrafilters *} theory Filter imports "~~/src/HOL/Library/Infinite_Set" 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" begin lemma 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 not_memI: "- A ∈ F ==> A ∉ F" by (drule memD, simp) lemma Int_iff: "(x ∩ y ∈ F) = (x ∈ F ∧ y ∈ F)" by (auto elim: subset intro: Int) end subsubsection {* Ultrafilters *} locale ultrafilter = filter + assumes ultra: "A ∈ F ∨ - A ∈ F" begin lemma memI: "- A ∉ F ==> A ∈ F" using ultra [of A] by simp lemma not_memD: "A ∉ F ==> - A ∈ F" by (rule memI, simp) lemma not_mem_iff: "(A ∉ F) = (- A ∈ F)" by (rule iffI [OF not_memD not_memI]) lemma Compl_iff: "(- A ∈ F) = (A ∉ F)" by (rule iffI [OF not_memI not_memD]) lemma 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 end subsubsection {* Free Ultrafilters *} locale freeultrafilter = ultrafilter + assumes infinite: "A ∈ F ==> infinite A" begin lemma finite: "finite A ==> A ∉ F" by (erule contrapos_pn, erule infinite) lemma singleton: "{x} ∉ F" by (rule finite, simp) lemma insert_iff [simp]: "(insert x A ∈ F) = (A ∈ 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. ∃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" using sub . 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 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 ≡ {A. finite (- A)}" and superfrechet_def: "superfrechet ≡ {G. filter G ∧ frechet ⊆ G}" begin lemma superfrechetI: "[|filter G; frechet ⊆ G|] ==> G ∈ superfrechet" by (simp add: superfrechet_def) lemma superfrechetD1: "G ∈ superfrechet ==> filter G" by (simp add: superfrechet_def) lemma 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" using inf 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 filter_frechet: "filter frechet" by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV]) lemma frechet_in_superfrechet: "frechet ∈ superfrechet" by (rule superfrechetI [OF filter_frechet subset_refl]) lemma lemma_mem_chain_filter: "[|c ∈ chains superfrechet; x ∈ c|] ==> filter x" by (unfold chains_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 Union_chain_UNIV: "[|c ∈ chains superfrechet; c ≠ {}|] ==> UNIV ∈ \<Union>c" proof - assume 1: "c ∈ chains 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 Union_chain_empty: "c ∈ chains superfrechet ==> {} ∉ \<Union>c" proof assume 1: "c ∈ chains 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 Union_chain_Int: "[|c ∈ chains superfrechet; u ∈ \<Union>c; v ∈ \<Union>c|] ==> u ∩ v ∈ \<Union>c" proof - assume c: "c ∈ chains 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" using c unfolding chains_def chain_subset_def by auto 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 Union_chain_subset: "[|c ∈ chains superfrechet; u ∈ \<Union>c; u ⊆ v|] ==> v ∈ \<Union>c" proof - assume c: "c ∈ chains 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 Union_chain_filter: assumes chain: "c ∈ chains superfrechet" and nonempty: "c ≠ {}" shows "filter (\<Union>c)" proof (rule filter.intro) show "UNIV ∈ \<Union>c" using chain nonempty by (rule Union_chain_UNIV) next show "{} ∉ \<Union>c" using chain by (rule Union_chain_empty) next fix u v assume "u ∈ \<Union>c" and "v ∈ \<Union>c" with chain show "u ∩ v ∈ \<Union>c" by (rule Union_chain_Int) next fix u v assume "u ∈ \<Union>c" and "u ⊆ v" with chain show "v ∈ \<Union>c" by (rule Union_chain_subset) qed lemma lemma_mem_chain_frechet_subset: "[|c ∈ chains superfrechet; x ∈ c|] ==> frechet ⊆ x" by (unfold superfrechet_def chains_def, blast) lemma Union_chain_superfrechet: "[|c ≠ {}; c ∈ chains superfrechet|] ==> \<Union>c ∈ superfrechet" proof (rule superfrechetI) assume 1: "c ∈ chains 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 max_cofinite_filter_Ex: "∃U∈superfrechet. ∀G∈superfrechet. U ⊆ G --> G = U" proof (rule Zorn_Lemma2, safe) fix c assume c: "c ∈ chains 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 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 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 --> G = U" .. 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[symmetric]) 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 [OF ultrafilter.intro]) (* FIXME: unfold_locales should use chained facts *) then show ?thesis .. qed end hide_const (open) filter end