src/HOL/NSA/Filter.thy
author wenzelm
Fri Apr 16 21:28:09 2010 +0200 (2010-04-16)
changeset 36176 3fe7e97ccca8
parent 28823 dcbef866c9e2
child 41589 bbd861837ebc
permissions -rw-r--r--
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
     1 (*  Title       : Filter.thy
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     6     Conversion to locales by Brian Huffman, 2005
     7 *) 
     8 
     9 header {* Filters and Ultrafilters *}
    10 
    11 theory Filter
    12 imports "~~/src/HOL/Library/Zorn" "~~/src/HOL/Library/Infinite_Set"
    13 begin
    14 
    15 subsection {* Definitions and basic properties *}
    16 
    17 subsubsection {* Filters *}
    18 
    19 locale filter =
    20   fixes F :: "'a set set"
    21   assumes UNIV [iff]:  "UNIV \<in> F"
    22   assumes empty [iff]: "{} \<notin> F"
    23   assumes Int:         "\<lbrakk>u \<in> F; v \<in> F\<rbrakk> \<Longrightarrow> u \<inter> v \<in> F"
    24   assumes subset:      "\<lbrakk>u \<in> F; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> F"
    25 
    26 lemma (in filter) memD: "A \<in> F \<Longrightarrow> - A \<notin> F"
    27 proof
    28   assume "A \<in> F" and "- A \<in> F"
    29   hence "A \<inter> (- A) \<in> F" by (rule Int)
    30   thus "False" by simp
    31 qed
    32 
    33 lemma (in filter) not_memI: "- A \<in> F \<Longrightarrow> A \<notin> F"
    34 by (drule memD, simp)
    35 
    36 lemma (in filter) Int_iff: "(x \<inter> y \<in> F) = (x \<in> F \<and> y \<in> F)"
    37 by (auto elim: subset intro: Int)
    38 
    39 subsubsection {* Ultrafilters *}
    40 
    41 locale ultrafilter = filter +
    42   assumes ultra: "A \<in> F \<or> - A \<in> F"
    43 
    44 lemma (in ultrafilter) memI: "- A \<notin> F \<Longrightarrow> A \<in> F"
    45 by (cut_tac ultra [of A], simp)
    46 
    47 lemma (in ultrafilter) not_memD: "A \<notin> F \<Longrightarrow> - A \<in> F"
    48 by (rule memI, simp)
    49 
    50 lemma (in ultrafilter) not_mem_iff: "(A \<notin> F) = (- A \<in> F)"
    51 by (rule iffI [OF not_memD not_memI])
    52 
    53 lemma (in ultrafilter) Compl_iff: "(- A \<in> F) = (A \<notin> F)"
    54 by (rule iffI [OF not_memI not_memD])
    55 
    56 lemma (in ultrafilter) Un_iff: "(x \<union> y \<in> F) = (x \<in> F \<or> y \<in> F)"
    57  apply (rule iffI)
    58   apply (erule contrapos_pp)
    59   apply (simp add: Int_iff not_mem_iff)
    60  apply (auto elim: subset)
    61 done
    62 
    63 subsubsection {* Free Ultrafilters *}
    64 
    65 locale freeultrafilter = ultrafilter +
    66   assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
    67 
    68 lemma (in freeultrafilter) finite: "finite A \<Longrightarrow> A \<notin> F"
    69 by (erule contrapos_pn, erule infinite)
    70 
    71 lemma (in freeultrafilter) singleton: "{x} \<notin> F"
    72 by (rule finite, simp)
    73 
    74 lemma (in freeultrafilter) insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)"
    75 apply (subst insert_is_Un)
    76 apply (subst Un_iff)
    77 apply (simp add: singleton)
    78 done
    79 
    80 lemma (in freeultrafilter) filter: "filter F" ..
    81 
    82 lemma (in freeultrafilter) ultrafilter: "ultrafilter F" ..
    83 
    84 
    85 subsection {* Collect properties *}
    86 
    87 lemma (in filter) Collect_ex:
    88   "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
    89 proof
    90   assume "{n. \<exists>x. P n x} \<in> F"
    91   hence "{n. P n (SOME x. P n x)} \<in> F"
    92     by (auto elim: someI subset)
    93   thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
    94 next
    95   show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
    96     by (auto elim: subset)
    97 qed
    98 
    99 lemma (in filter) Collect_conj:
   100   "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
   101 by (subst Collect_conj_eq, rule Int_iff)
   102 
   103 lemma (in ultrafilter) Collect_not:
   104   "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
   105 by (subst Collect_neg_eq, rule Compl_iff)
   106 
   107 lemma (in ultrafilter) Collect_disj:
   108   "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
   109 by (subst Collect_disj_eq, rule Un_iff)
   110 
   111 lemma (in ultrafilter) Collect_all:
   112   "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
   113 apply (rule Not_eq_iff [THEN iffD1])
   114 apply (simp add: Collect_not [symmetric])
   115 apply (rule Collect_ex)
   116 done
   117 
   118 subsection {* Maximal filter = Ultrafilter *}
   119 
   120 text {*
   121    A filter F is an ultrafilter iff it is a maximal filter,
   122    i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
   123 *}
   124 text {*
   125   Lemmas that shows existence of an extension to what was assumed to
   126   be a maximal filter. Will be used to derive contradiction in proof of
   127   property of ultrafilter.
   128 *}
   129 
   130 lemma extend_lemma1: "UNIV \<in> F \<Longrightarrow> A \<in> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   131 by blast
   132 
   133 lemma extend_lemma2: "F \<subseteq> {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   134 by blast
   135 
   136 lemma (in filter) extend_filter:
   137 assumes A: "- A \<notin> F"
   138 shows "filter {X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}" (is "filter ?X")
   139 proof (rule filter.intro)
   140   show "UNIV \<in> ?X" by blast
   141 next
   142   show "{} \<notin> ?X"
   143   proof (clarify)
   144     fix f assume f: "f \<in> F" and Af: "A \<inter> f \<subseteq> {}"
   145     from Af have fA: "f \<subseteq> - A" by blast
   146     from f fA have "- A \<in> F" by (rule subset)
   147     with A show "False" by simp
   148   qed
   149 next
   150   fix u and v
   151   assume u: "u \<in> ?X" and v: "v \<in> ?X"
   152   from u obtain f where f: "f \<in> F" and Af: "A \<inter> f \<subseteq> u" by blast
   153   from v obtain g where g: "g \<in> F" and Ag: "A \<inter> g \<subseteq> v" by blast
   154   from f g have fg: "f \<inter> g \<in> F" by (rule Int)
   155   from Af Ag have Afg: "A \<inter> (f \<inter> g) \<subseteq> u \<inter> v" by blast
   156   from fg Afg show "u \<inter> v \<in> ?X" by blast
   157 next
   158   fix u and v
   159   assume uv: "u \<subseteq> v" and u: "u \<in> ?X"
   160   from u obtain f where f: "f \<in> F" and Afu: "A \<inter> f \<subseteq> u" by blast
   161   from Afu uv have Afv: "A \<inter> f \<subseteq> v" by blast
   162   from f Afv have "\<exists>f\<in>F. A \<inter> f \<subseteq> v" by blast
   163   thus "v \<in> ?X" by simp
   164 qed
   165 
   166 lemma (in filter) max_filter_ultrafilter:
   167 assumes max: "\<And>G. \<lbrakk>filter G; F \<subseteq> G\<rbrakk> \<Longrightarrow> F = G"
   168 shows "ultrafilter_axioms F"
   169 proof (rule ultrafilter_axioms.intro)
   170   fix A show "A \<in> F \<or> - A \<in> F"
   171   proof (rule disjCI)
   172     let ?X = "{X. \<exists>f\<in>F. A \<inter> f \<subseteq> X}"
   173     assume AF: "- A \<notin> F"
   174     from AF have X: "filter ?X" by (rule extend_filter)
   175     from UNIV have AX: "A \<in> ?X" by (rule extend_lemma1)
   176     have FX: "F \<subseteq> ?X" by (rule extend_lemma2)
   177     from X FX have "F = ?X" by (rule max)
   178     with AX show "A \<in> F" by simp
   179   qed
   180 qed
   181 
   182 lemma (in ultrafilter) max_filter:
   183 assumes G: "filter G" and sub: "F \<subseteq> G" shows "F = G"
   184 proof
   185   show "F \<subseteq> G" using sub .
   186   show "G \<subseteq> F"
   187   proof
   188     fix A assume A: "A \<in> G"
   189     from G A have "- A \<notin> G" by (rule filter.memD)
   190     with sub have B: "- A \<notin> F" by blast
   191     thus "A \<in> F" by (rule memI)
   192   qed
   193 qed
   194 
   195 subsection {* Ultrafilter Theorem *}
   196 
   197 text "A locale makes proof of ultrafilter Theorem more modular"
   198 locale UFT =
   199   fixes   frechet :: "'a set set"
   200   and     superfrechet :: "'a set set set"
   201 
   202   assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
   203 
   204   defines frechet_def: "frechet \<equiv> {A. finite (- A)}"
   205   and     superfrechet_def: "superfrechet \<equiv> {G. filter G \<and> frechet \<subseteq> G}"
   206 
   207 lemma (in UFT) superfrechetI:
   208   "\<lbrakk>filter G; frechet \<subseteq> G\<rbrakk> \<Longrightarrow> G \<in> superfrechet"
   209 by (simp add: superfrechet_def)
   210 
   211 lemma (in UFT) superfrechetD1:
   212   "G \<in> superfrechet \<Longrightarrow> filter G"
   213 by (simp add: superfrechet_def)
   214 
   215 lemma (in UFT) superfrechetD2:
   216   "G \<in> superfrechet \<Longrightarrow> frechet \<subseteq> G"
   217 by (simp add: superfrechet_def)
   218 
   219 text {* A few properties of free filters *}
   220 
   221 lemma filter_cofinite:
   222 assumes inf: "infinite (UNIV :: 'a set)"
   223 shows "filter {A:: 'a set. finite (- A)}" (is "filter ?F")
   224 proof (rule filter.intro)
   225   show "UNIV \<in> ?F" by simp
   226 next
   227   show "{} \<notin> ?F" using inf by simp
   228 next
   229   fix u v assume "u \<in> ?F" and "v \<in> ?F"
   230   thus "u \<inter> v \<in> ?F" by simp
   231 next
   232   fix u v assume uv: "u \<subseteq> v" and u: "u \<in> ?F"
   233   from uv have vu: "- v \<subseteq> - u" by simp
   234   from u show "v \<in> ?F"
   235     by (simp add: finite_subset [OF vu])
   236 qed
   237 
   238 text {*
   239    We prove: 1. Existence of maximal filter i.e. ultrafilter;
   240              2. Freeness property i.e ultrafilter is free.
   241              Use a locale to prove various lemmas and then 
   242              export main result: The ultrafilter Theorem
   243 *}
   244 
   245 lemma (in UFT) filter_frechet: "filter frechet"
   246 by (unfold frechet_def, rule filter_cofinite [OF infinite_UNIV])
   247 
   248 lemma (in UFT) frechet_in_superfrechet: "frechet \<in> superfrechet"
   249 by (rule superfrechetI [OF filter_frechet subset_refl])
   250 
   251 lemma (in UFT) lemma_mem_chain_filter:
   252   "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> filter x"
   253 by (unfold chain_def superfrechet_def, blast)
   254 
   255 
   256 subsubsection {* Unions of chains of superfrechets *}
   257 
   258 text "In this section we prove that superfrechet is closed
   259 with respect to unions of non-empty chains. We must show
   260   1) Union of a chain is a filter,
   261   2) Union of a chain contains frechet.
   262 
   263 Number 2 is trivial, but 1 requires us to prove all the filter rules."
   264 
   265 lemma (in UFT) Union_chain_UNIV:
   266 "\<lbrakk>c \<in> chain superfrechet; c \<noteq> {}\<rbrakk> \<Longrightarrow> UNIV \<in> \<Union>c"
   267 proof -
   268   assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
   269   from 2 obtain x where 3: "x \<in> c" by blast
   270   from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   271   hence "UNIV \<in> x" by (rule filter.UNIV)
   272   with 3 show "UNIV \<in> \<Union>c" by blast
   273 qed
   274 
   275 lemma (in UFT) Union_chain_empty:
   276 "c \<in> chain superfrechet \<Longrightarrow> {} \<notin> \<Union>c"
   277 proof
   278   assume 1: "c \<in> chain superfrechet" and 2: "{} \<in> \<Union>c"
   279   from 2 obtain x where 3: "x \<in> c" and 4: "{} \<in> x" ..
   280   from 1 3 have "filter x" by (rule lemma_mem_chain_filter)
   281   hence "{} \<notin> x" by (rule filter.empty)
   282   with 4 show "False" by simp
   283 qed
   284 
   285 lemma (in UFT) Union_chain_Int:
   286 "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; v \<in> \<Union>c\<rbrakk> \<Longrightarrow> u \<inter> v \<in> \<Union>c"
   287 proof -
   288   assume c: "c \<in> chain superfrechet"
   289   assume "u \<in> \<Union>c"
   290     then obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   291   assume "v \<in> \<Union>c"
   292     then obtain y where vy: "v \<in> y" and yc: "y \<in> c" ..
   293   from c xc yc have "x \<subseteq> y \<or> y \<subseteq> x" by (rule chainD)
   294   with xc yc have xyc: "x \<union> y \<in> c"
   295     by (auto simp add: Un_absorb1 Un_absorb2)
   296   with c have fxy: "filter (x \<union> y)" by (rule lemma_mem_chain_filter)
   297   from ux have uxy: "u \<in> x \<union> y" by simp
   298   from vy have vxy: "v \<in> x \<union> y" by simp
   299   from fxy uxy vxy have "u \<inter> v \<in> x \<union> y" by (rule filter.Int)
   300   with xyc show "u \<inter> v \<in> \<Union>c" ..
   301 qed
   302 
   303 lemma (in UFT) Union_chain_subset:
   304 "\<lbrakk>c \<in> chain superfrechet; u \<in> \<Union>c; u \<subseteq> v\<rbrakk> \<Longrightarrow> v \<in> \<Union>c"
   305 proof -
   306   assume c: "c \<in> chain superfrechet"
   307      and u: "u \<in> \<Union>c" and uv: "u \<subseteq> v"
   308   from u obtain x where ux: "u \<in> x" and xc: "x \<in> c" ..
   309   from c xc have fx: "filter x" by (rule lemma_mem_chain_filter)
   310   from fx ux uv have vx: "v \<in> x" by (rule filter.subset)
   311   with xc show "v \<in> \<Union>c" ..
   312 qed
   313 
   314 lemma (in UFT) Union_chain_filter:
   315 assumes chain: "c \<in> chain superfrechet" and nonempty: "c \<noteq> {}"
   316 shows "filter (\<Union>c)"
   317 proof (rule filter.intro)
   318   show "UNIV \<in> \<Union>c" using chain nonempty by (rule Union_chain_UNIV)
   319 next
   320   show "{} \<notin> \<Union>c" using chain by (rule Union_chain_empty)
   321 next
   322   fix u v assume "u \<in> \<Union>c" and "v \<in> \<Union>c"
   323   with chain show "u \<inter> v \<in> \<Union>c" by (rule Union_chain_Int)
   324 next
   325   fix u v assume "u \<in> \<Union>c" and "u \<subseteq> v"
   326   with chain show "v \<in> \<Union>c" by (rule Union_chain_subset)
   327 qed
   328 
   329 lemma (in UFT) lemma_mem_chain_frechet_subset:
   330   "\<lbrakk>c \<in> chain superfrechet; x \<in> c\<rbrakk> \<Longrightarrow> frechet \<subseteq> x"
   331 by (unfold superfrechet_def chain_def, blast)
   332 
   333 lemma (in UFT) Union_chain_superfrechet:
   334   "\<lbrakk>c \<noteq> {}; c \<in> chain superfrechet\<rbrakk> \<Longrightarrow> \<Union>c \<in> superfrechet"
   335 proof (rule superfrechetI)
   336   assume 1: "c \<in> chain superfrechet" and 2: "c \<noteq> {}"
   337   thus "filter (\<Union>c)" by (rule Union_chain_filter)
   338   from 2 obtain x where 3: "x \<in> c" by blast
   339   from 1 3 have "frechet \<subseteq> x" by (rule lemma_mem_chain_frechet_subset)
   340   also from 3 have "x \<subseteq> \<Union>c" by blast
   341   finally show "frechet \<subseteq> \<Union>c" .
   342 qed
   343 
   344 subsubsection {* Existence of free ultrafilter *}
   345 
   346 lemma (in UFT) max_cofinite_filter_Ex:
   347   "\<exists>U\<in>superfrechet. \<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G"
   348 proof (rule Zorn_Lemma2 [rule_format])
   349   fix c assume c: "c \<in> chain superfrechet"
   350   show "\<exists>U\<in>superfrechet. \<forall>G\<in>c. G \<subseteq> U" (is "?U")
   351   proof (cases)
   352     assume "c = {}"
   353     with frechet_in_superfrechet show "?U" by blast
   354   next
   355     assume A: "c \<noteq> {}"
   356     from A c have "\<Union>c \<in> superfrechet"
   357       by (rule Union_chain_superfrechet)
   358     thus "?U" by blast
   359   qed
   360 qed
   361 
   362 lemma (in UFT) mem_superfrechet_all_infinite:
   363   "\<lbrakk>U \<in> superfrechet; A \<in> U\<rbrakk> \<Longrightarrow> infinite A"
   364 proof
   365   assume U: "U \<in> superfrechet" and A: "A \<in> U" and fin: "finite A"
   366   from U have fil: "filter U" and fre: "frechet \<subseteq> U"
   367     by (simp_all add: superfrechet_def)
   368   from fin have "- A \<in> frechet" by (simp add: frechet_def)
   369   with fre have cA: "- A \<in> U" by (rule subsetD)
   370   from fil A cA have "A \<inter> - A \<in> U" by (rule filter.Int)
   371   with fil show "False" by (simp add: filter.empty)
   372 qed
   373 
   374 text {* There exists a free ultrafilter on any infinite set *}
   375 
   376 lemma (in UFT) freeultrafilter_ex:
   377   "\<exists>U::'a set set. freeultrafilter U"
   378 proof -
   379   from max_cofinite_filter_Ex obtain U
   380     where U: "U \<in> superfrechet"
   381       and max [rule_format]: "\<forall>G\<in>superfrechet. U \<subseteq> G \<longrightarrow> U = G" ..
   382   from U have fil: "filter U" by (rule superfrechetD1)
   383   from U have fre: "frechet \<subseteq> U" by (rule superfrechetD2)
   384   have ultra: "ultrafilter_axioms U"
   385   proof (rule filter.max_filter_ultrafilter [OF fil])
   386     fix G assume G: "filter G" and UG: "U \<subseteq> G"
   387     from fre UG have "frechet \<subseteq> G" by simp
   388     with G have "G \<in> superfrechet" by (rule superfrechetI)
   389     from this UG show "U = G" by (rule max)
   390   qed
   391   have free: "freeultrafilter_axioms U"
   392   proof (rule freeultrafilter_axioms.intro)
   393     fix A assume "A \<in> U"
   394     with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   395   qed
   396   show ?thesis
   397   proof
   398     from fil ultra free show "freeultrafilter U"
   399       by (rule freeultrafilter.intro [OF ultrafilter.intro])
   400       (* FIXME: unfold_locales should use chained facts *)
   401   qed
   402 qed
   403 
   404 lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
   405 
   406 hide_const (open) filter
   407 
   408 end