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