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