# Theory Filter

Up to index of Isabelle/HOL/HOL-Complex

theory Filter
imports Zorn
begin

    (*  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

### Definitions and basic properties

#### Filters

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)

#### Ultrafilters

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)

#### Free Ultrafilters

lemma finite:

      [| freeultrafilter F; finite A |] ==> A ∉ F

lemma filter:

      freeultrafilter F ==> Filter.filter F

lemma ultrafilter:

      freeultrafilter F ==> ultrafilter F

### Collect properties

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)

### Maximal filter = Ultrafilter

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

### Ultrafilter Theorem

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

#### Unions of chains of superfrechets

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}

#### Existence of free ultrafilter

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