(* 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/Zorn" "~~/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