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 \ F" huffman@27468: assumes empty [iff]: "{} \ F" huffman@27468: assumes Int: "\u \ F; v \ F\ \ u \ v \ F" huffman@27468: assumes subset: "\u \ F; u \ v\ \ v \ F" huffman@27468: huffman@27468: lemma (in filter) memD: "A \ F \ - A \ F" huffman@27468: proof huffman@27468: assume "A \ F" and "- A \ F" huffman@27468: hence "A \ (- A) \ F" by (rule Int) huffman@27468: thus "False" by simp huffman@27468: qed huffman@27468: huffman@27468: lemma (in filter) not_memI: "- A \ F \ A \ F" huffman@27468: by (drule memD, simp) huffman@27468: huffman@27468: lemma (in filter) Int_iff: "(x \ y \ F) = (x \ F \ y \ F)" huffman@27468: by (auto elim: subset intro: Int) huffman@27468: huffman@27468: subsubsection {* Ultrafilters *} huffman@27468: huffman@27468: locale ultrafilter = filter + huffman@27468: assumes ultra: "A \ F \ - A \ F" huffman@27468: huffman@27468: lemma (in ultrafilter) memI: "- A \ F \ A \ F" huffman@27468: by (cut_tac ultra [of A], simp) huffman@27468: huffman@27468: lemma (in ultrafilter) not_memD: "A \ F \ - A \ F" huffman@27468: by (rule memI, simp) huffman@27468: huffman@27468: lemma (in ultrafilter) not_mem_iff: "(A \ F) = (- A \ F)" huffman@27468: by (rule iffI [OF not_memD not_memI]) huffman@27468: huffman@27468: lemma (in ultrafilter) Compl_iff: "(- A \ F) = (A \ F)" huffman@27468: by (rule iffI [OF not_memI not_memD]) huffman@27468: huffman@27468: lemma (in ultrafilter) Un_iff: "(x \ y \ F) = (x \ F \ y \ 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@27468: subsubsection {* Free Ultrafilters *} huffman@27468: huffman@27468: locale freeultrafilter = ultrafilter + huffman@27468: assumes infinite: "A \ F \ infinite A" huffman@27468: huffman@27468: lemma (in freeultrafilter) finite: "finite A \ A \ F" huffman@27468: by (erule contrapos_pn, erule infinite) huffman@27468: huffman@27468: lemma (in freeultrafilter) singleton: "{x} \ F" huffman@27468: by (rule finite, simp) huffman@27468: huffman@27468: lemma (in freeultrafilter) insert_iff [simp]: "(insert x A \ F) = (A \ 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: haftmann@28823: lemma (in freeultrafilter) filter: "filter F" .. huffman@27468: haftmann@28823: lemma (in freeultrafilter) ultrafilter: "ultrafilter F" .. huffman@27468: huffman@27468: huffman@27468: subsection {* Collect properties *} huffman@27468: huffman@27468: lemma (in filter) Collect_ex: huffman@27468: "({n. \x. P n x} \ F) = (\X. {n. P n (X n)} \ F)" huffman@27468: proof huffman@27468: assume "{n. \x. P n x} \ F" huffman@27468: hence "{n. P n (SOME x. P n x)} \ F" huffman@27468: by (auto elim: someI subset) huffman@27468: thus "\X. {n. P n (X n)} \ F" by fast huffman@27468: next huffman@27468: show "\X. {n. P n (X n)} \ F \ {n. \x. P n x} \ F" huffman@27468: by (auto elim: subset) huffman@27468: qed huffman@27468: huffman@27468: lemma (in filter) Collect_conj: huffman@27468: "({n. P n \ Q n} \ F) = ({n. P n} \ F \ {n. Q n} \ F)" huffman@27468: by (subst Collect_conj_eq, rule Int_iff) huffman@27468: huffman@27468: lemma (in ultrafilter) Collect_not: huffman@27468: "({n. \ P n} \ F) = ({n. P n} \ 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 \ Q n} \ F) = ({n. P n} \ F \ {n. Q n} \ F)" huffman@27468: by (subst Collect_disj_eq, rule Un_iff) huffman@27468: huffman@27468: lemma (in ultrafilter) Collect_all: huffman@27468: "({n. \x. P n x} \ F) = (\X. {n. P n (X n)} \ 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 \ 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 \ F \ A \ {X. \f\F. A \ f \ X}" huffman@27468: by blast huffman@27468: huffman@27468: lemma extend_lemma2: "F \ {X. \f\F. A \ f \ X}" huffman@27468: by blast huffman@27468: huffman@27468: lemma (in filter) extend_filter: huffman@27468: assumes A: "- A \ F" huffman@27468: shows "filter {X. \f\F. A \ f \ X}" (is "filter ?X") huffman@27468: proof (rule filter.intro) huffman@27468: show "UNIV \ ?X" by blast huffman@27468: next huffman@27468: show "{} \ ?X" huffman@27468: proof (clarify) huffman@27468: fix f assume f: "f \ F" and Af: "A \ f \ {}" huffman@27468: from Af have fA: "f \ - A" by blast huffman@27468: from f fA have "- A \ 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 \ ?X" and v: "v \ ?X" huffman@27468: from u obtain f where f: "f \ F" and Af: "A \ f \ u" by blast huffman@27468: from v obtain g where g: "g \ F" and Ag: "A \ g \ v" by blast huffman@27468: from f g have fg: "f \ g \ F" by (rule Int) huffman@27468: from Af Ag have Afg: "A \ (f \ g) \ u \ v" by blast huffman@27468: from fg Afg show "u \ v \ ?X" by blast huffman@27468: next huffman@27468: fix u and v huffman@27468: assume uv: "u \ v" and u: "u \ ?X" huffman@27468: from u obtain f where f: "f \ F" and Afu: "A \ f \ u" by blast huffman@27468: from Afu uv have Afv: "A \ f \ v" by blast huffman@27468: from f Afv have "\f\F. A \ f \ v" by blast huffman@27468: thus "v \ ?X" by simp huffman@27468: qed huffman@27468: huffman@27468: lemma (in filter) max_filter_ultrafilter: huffman@27468: assumes max: "\G. \filter G; F \ G\ \ F = G" huffman@27468: shows "ultrafilter_axioms F" huffman@27468: proof (rule ultrafilter_axioms.intro) huffman@27468: fix A show "A \ F \ - A \ F" huffman@27468: proof (rule disjCI) huffman@27468: let ?X = "{X. \f\F. A \ f \ X}" huffman@27468: assume AF: "- A \ F" huffman@27468: from AF have X: "filter ?X" by (rule extend_filter) huffman@27468: from UNIV have AX: "A \ ?X" by (rule extend_lemma1) huffman@27468: have FX: "F \ ?X" by (rule extend_lemma2) huffman@27468: from X FX have "F = ?X" by (rule max) huffman@27468: with AX show "A \ 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 \ G" shows "F = G" huffman@27468: proof huffman@27468: show "F \ G" using sub . huffman@27468: show "G \ F" huffman@27468: proof huffman@27468: fix A assume A: "A \ G" huffman@27468: from G A have "- A \ G" by (rule filter.memD) huffman@27468: with sub have B: "- A \ F" by blast huffman@27468: thus "A \ F" by (rule memI) huffman@27468: qed huffman@27468: qed huffman@27468: huffman@27468: subsection {* Ultrafilter Theorem *} huffman@27468: huffman@27468: text "A locale makes proof of ultrafilter Theorem more modular" haftmann@27681: locale UFT = 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 \ {A. finite (- A)}" huffman@27468: and superfrechet_def: "superfrechet \ {G. filter G \ frechet \ G}" huffman@27468: huffman@27468: lemma (in UFT) superfrechetI: huffman@27468: "\filter G; frechet \ G\ \ G \ superfrechet" huffman@27468: by (simp add: superfrechet_def) huffman@27468: huffman@27468: lemma (in UFT) superfrechetD1: huffman@27468: "G \ superfrechet \ filter G" huffman@27468: by (simp add: superfrechet_def) huffman@27468: huffman@27468: lemma (in UFT) superfrechetD2: huffman@27468: "G \ superfrechet \ frechet \ 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 \ ?F" by simp huffman@27468: next huffman@27468: show "{} \ ?F" using inf by simp huffman@27468: next huffman@27468: fix u v assume "u \ ?F" and "v \ ?F" huffman@27468: thus "u \ v \ ?F" by simp huffman@27468: next huffman@27468: fix u v assume uv: "u \ v" and u: "u \ ?F" huffman@27468: from uv have vu: "- v \ - u" by simp huffman@27468: from u show "v \ ?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@27468: lemma (in UFT) filter_frechet: "filter frechet" huffman@27468: by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV]) huffman@27468: huffman@27468: lemma (in UFT) frechet_in_superfrechet: "frechet \ superfrechet" huffman@27468: by (rule superfrechetI [OF filter_frechet subset_refl]) huffman@27468: huffman@27468: lemma (in UFT) lemma_mem_chain_filter: huffman@27468: "\c \ chain superfrechet; x \ c\ \ filter x" huffman@27468: by (unfold chain_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 huffman@27468: 1) Union of a chain is a 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@27468: lemma (in UFT) Union_chain_UNIV: huffman@27468: "\c \ chain superfrechet; c \ {}\ \ UNIV \ \c" huffman@27468: proof - huffman@27468: assume 1: "c \ chain superfrechet" and 2: "c \ {}" huffman@27468: from 2 obtain x where 3: "x \ c" by blast huffman@27468: from 1 3 have "filter x" by (rule lemma_mem_chain_filter) huffman@27468: hence "UNIV \ x" by (rule filter.UNIV) huffman@27468: with 3 show "UNIV \ \c" by blast huffman@27468: qed huffman@27468: huffman@27468: lemma (in UFT) Union_chain_empty: huffman@27468: "c \ chain superfrechet \ {} \ \c" huffman@27468: proof huffman@27468: assume 1: "c \ chain superfrechet" and 2: "{} \ \c" huffman@27468: from 2 obtain x where 3: "x \ c" and 4: "{} \ x" .. huffman@27468: from 1 3 have "filter x" by (rule lemma_mem_chain_filter) huffman@27468: hence "{} \ x" by (rule filter.empty) huffman@27468: with 4 show "False" by simp huffman@27468: qed huffman@27468: huffman@27468: lemma (in UFT) Union_chain_Int: huffman@27468: "\c \ chain superfrechet; u \ \c; v \ \c\ \ u \ v \ \c" huffman@27468: proof - huffman@27468: assume c: "c \ chain superfrechet" huffman@27468: assume "u \ \c" huffman@27468: then obtain x where ux: "u \ x" and xc: "x \ c" .. huffman@27468: assume "v \ \c" huffman@27468: then obtain y where vy: "v \ y" and yc: "y \ c" .. huffman@27468: from c xc yc have "x \ y \ y \ x" by (rule chainD) huffman@27468: with xc yc have xyc: "x \ y \ c" huffman@27468: by (auto simp add: Un_absorb1 Un_absorb2) huffman@27468: with c have fxy: "filter (x \ y)" by (rule lemma_mem_chain_filter) huffman@27468: from ux have uxy: "u \ x \ y" by simp huffman@27468: from vy have vxy: "v \ x \ y" by simp huffman@27468: from fxy uxy vxy have "u \ v \ x \ y" by (rule filter.Int) huffman@27468: with xyc show "u \ v \ \c" .. huffman@27468: qed huffman@27468: huffman@27468: lemma (in UFT) Union_chain_subset: huffman@27468: "\c \ chain superfrechet; u \ \c; u \ v\ \ v \ \c" huffman@27468: proof - huffman@27468: assume c: "c \ chain superfrechet" huffman@27468: and u: "u \ \c" and uv: "u \ v" huffman@27468: from u obtain x where ux: "u \ x" and xc: "x \ 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 \ x" by (rule filter.subset) huffman@27468: with xc show "v \ \c" .. huffman@27468: qed huffman@27468: huffman@27468: lemma (in UFT) Union_chain_filter: huffman@27468: assumes chain: "c \ chain superfrechet" and nonempty: "c \ {}" huffman@27468: shows "filter (\c)" huffman@27468: proof (rule filter.intro) huffman@27468: show "UNIV \ \c" using chain nonempty by (rule Union_chain_UNIV) huffman@27468: next huffman@27468: show "{} \ \c" using chain by (rule Union_chain_empty) huffman@27468: next huffman@27468: fix u v assume "u \ \c" and "v \ \c" huffman@27468: with chain show "u \ v \ \c" by (rule Union_chain_Int) huffman@27468: next huffman@27468: fix u v assume "u \ \c" and "u \ v" huffman@27468: with chain show "v \ \c" by (rule Union_chain_subset) huffman@27468: qed huffman@27468: huffman@27468: lemma (in UFT) lemma_mem_chain_frechet_subset: huffman@27468: "\c \ chain superfrechet; x \ c\ \ frechet \ x" huffman@27468: by (unfold superfrechet_def chain_def, blast) huffman@27468: huffman@27468: lemma (in UFT) Union_chain_superfrechet: huffman@27468: "\c \ {}; c \ chain superfrechet\ \ \c \ superfrechet" huffman@27468: proof (rule superfrechetI) huffman@27468: assume 1: "c \ chain superfrechet" and 2: "c \ {}" huffman@27468: thus "filter (\c)" by (rule Union_chain_filter) huffman@27468: from 2 obtain x where 3: "x \ c" by blast huffman@27468: from 1 3 have "frechet \ x" by (rule lemma_mem_chain_frechet_subset) huffman@27468: also from 3 have "x \ \c" by blast huffman@27468: finally show "frechet \ \c" . huffman@27468: qed huffman@27468: huffman@27468: subsubsection {* Existence of free ultrafilter *} huffman@27468: huffman@27468: lemma (in UFT) max_cofinite_filter_Ex: huffman@27468: "\U\superfrechet. \G\superfrechet. U \ G \ U = G" huffman@27468: proof (rule Zorn_Lemma2 [rule_format]) huffman@27468: fix c assume c: "c \ chain superfrechet" huffman@27468: show "\U\superfrechet. \G\c. G \ 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 \ {}" huffman@27468: from A c have "\c \ superfrechet" huffman@27468: by (rule Union_chain_superfrechet) huffman@27468: thus "?U" by blast huffman@27468: qed huffman@27468: qed huffman@27468: huffman@27468: lemma (in UFT) mem_superfrechet_all_infinite: huffman@27468: "\U \ superfrechet; A \ U\ \ infinite A" huffman@27468: proof huffman@27468: assume U: "U \ superfrechet" and A: "A \ U" and fin: "finite A" huffman@27468: from U have fil: "filter U" and fre: "frechet \ U" huffman@27468: by (simp_all add: superfrechet_def) huffman@27468: from fin have "- A \ frechet" by (simp add: frechet_def) huffman@27468: with fre have cA: "- A \ U" by (rule subsetD) huffman@27468: from fil A cA have "A \ - A \ 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@27468: lemma (in UFT) freeultrafilter_ex: huffman@27468: "\U::'a set set. freeultrafilter U" huffman@27468: proof - huffman@27468: from max_cofinite_filter_Ex obtain U huffman@27468: where U: "U \ superfrechet" huffman@27468: and max [rule_format]: "\G\superfrechet. U \ G \ U = G" .. huffman@27468: from U have fil: "filter U" by (rule superfrechetD1) huffman@27468: from U have fre: "frechet \ 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 \ G" huffman@27468: from fre UG have "frechet \ G" by simp huffman@27468: with G have "G \ superfrechet" by (rule superfrechetI) huffman@27468: from this UG show "U = G" by (rule max) huffman@27468: qed huffman@27468: have free: "freeultrafilter_axioms U" huffman@27468: proof (rule freeultrafilter_axioms.intro) huffman@27468: fix A assume "A \ U" huffman@27468: with U show "infinite A" by (rule mem_superfrechet_all_infinite) huffman@27468: qed huffman@27468: show ?thesis huffman@27468: proof huffman@27468: from fil ultra free show "freeultrafilter U" huffman@27468: by (rule freeultrafilter.intro [OF ultrafilter.intro]) huffman@27468: (* FIXME: unfold_locales should use chained facts *) huffman@27468: qed huffman@27468: qed huffman@27468: haftmann@27681: lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro] huffman@27468: wenzelm@36176: hide_const (open) filter huffman@27468: huffman@27468: end