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