Theory Filter

theory Filter
imports Zorn Infinite_Set
(*  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