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