src/HOL/Hyperreal/Filter.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15094 a7d1a3fdc30d
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
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
paulson@10750
     6
*) 
paulson@10750
     7
paulson@15094
     8
header{*Filters and Ultrafilters*}
paulson@15094
     9
nipkow@15131
    10
theory Filter
nipkow@15131
    11
import Zorn
nipkow@15131
    12
begin
paulson@10750
    13
paulson@10750
    14
constdefs
paulson@10750
    15
paulson@15094
    16
  is_Filter       :: "['a set set,'a set] => bool"
paulson@15094
    17
  "is_Filter F S == (F <= Pow(S) & S \<in> F & {} ~: F &
paulson@15094
    18
                   (\<forall>u \<in> F. \<forall>v \<in> F. u Int v \<in> F) &
paulson@15094
    19
                   (\<forall>u v. u \<in> F & u <= v & v <= S --> v \<in> F))" 
paulson@10750
    20
paulson@15094
    21
  Filter          :: "'a set => 'a set set set"
paulson@10750
    22
  "Filter S == {X. is_Filter X S}"
paulson@10750
    23
 
paulson@10750
    24
  (* free filter does not contain any finite set *)
paulson@10750
    25
paulson@15094
    26
  Freefilter      :: "'a set => 'a set set set"
paulson@15094
    27
  "Freefilter S == {X. X \<in> Filter S & (\<forall>x \<in> X. ~ finite x)}"
paulson@10750
    28
paulson@15094
    29
  Ultrafilter     :: "'a set => 'a set set set"
paulson@15094
    30
  "Ultrafilter S == {X. X \<in> Filter S & (\<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X)}"
paulson@10750
    31
paulson@15094
    32
  FreeUltrafilter :: "'a set => 'a set set set"
paulson@15094
    33
  "FreeUltrafilter S == {X. X \<in> Ultrafilter S & (\<forall>x \<in> X. ~ finite x)}" 
paulson@10750
    34
paulson@10750
    35
  (* A locale makes proof of Ultrafilter Theorem more modular *)
paulson@15094
    36
locale (open) UFT = 
paulson@15094
    37
  fixes frechet      :: "'a set => 'a set set"
paulson@15094
    38
    and superfrechet :: "'a set => 'a set set set"
paulson@15094
    39
  assumes not_finite_UNIV:  "~finite (UNIV :: 'a set)"
paulson@15094
    40
  defines frechet_def:  
paulson@15094
    41
		"frechet S == {A. finite (S - A)}"
paulson@15094
    42
      and superfrechet_def:
paulson@15094
    43
		"superfrechet S == {G.  G \<in> Filter S & frechet S <= G}"
paulson@15094
    44
paulson@15094
    45
paulson@15094
    46
(*------------------------------------------------------------------
paulson@15094
    47
      Properties of Filters and Freefilters - 
paulson@15094
    48
      rules for intro, destruction etc.
paulson@15094
    49
 ------------------------------------------------------------------*)
paulson@15094
    50
paulson@15094
    51
lemma is_FilterD1: "is_Filter X S ==> X <= Pow(S)"
paulson@15094
    52
apply (simp add: is_Filter_def)
paulson@15094
    53
done
paulson@15094
    54
paulson@15094
    55
lemma is_FilterD2: "is_Filter X S ==> X ~= {}"
paulson@15094
    56
apply (auto simp add: is_Filter_def)
paulson@15094
    57
done
paulson@15094
    58
paulson@15094
    59
lemma is_FilterD3: "is_Filter X S ==> {} ~: X"
paulson@15094
    60
apply (simp add: is_Filter_def)
paulson@15094
    61
done
paulson@15094
    62
paulson@15094
    63
lemma mem_FiltersetI: "is_Filter X S ==> X \<in> Filter S"
paulson@15094
    64
apply (simp add: Filter_def)
paulson@15094
    65
done
paulson@15094
    66
paulson@15094
    67
lemma mem_FiltersetD: "X \<in> Filter S ==> is_Filter X S"
paulson@15094
    68
apply (simp add: Filter_def)
paulson@15094
    69
done
paulson@15094
    70
paulson@15094
    71
lemma Filter_empty_not_mem: "X \<in> Filter S ==> {} ~: X"
paulson@15094
    72
apply (erule mem_FiltersetD [THEN is_FilterD3])
paulson@15094
    73
done
paulson@15094
    74
paulson@15094
    75
lemmas Filter_empty_not_memE = Filter_empty_not_mem [THEN notE, standard]
paulson@15094
    76
paulson@15094
    77
lemma mem_FiltersetD1: "[| X \<in> Filter S; A \<in> X; B \<in> X |] ==> A Int B \<in> X"
paulson@15094
    78
apply (unfold Filter_def is_Filter_def)
paulson@15094
    79
apply blast
paulson@15094
    80
done
paulson@15094
    81
paulson@15094
    82
lemma mem_FiltersetD2: "[| X \<in> Filter S; A \<in> X; A <= B; B <= S|] ==> B \<in> X"
paulson@15094
    83
apply (unfold Filter_def is_Filter_def)
paulson@15094
    84
apply blast
paulson@15094
    85
done
paulson@15094
    86
paulson@15094
    87
lemma mem_FiltersetD3: "[| X \<in> Filter S; A \<in> X |] ==> A \<in> Pow S"
paulson@15094
    88
apply (unfold Filter_def is_Filter_def)
paulson@15094
    89
apply blast
paulson@15094
    90
done
paulson@15094
    91
paulson@15094
    92
lemma mem_FiltersetD4: "X \<in> Filter S  ==> S \<in> X"
paulson@15094
    93
apply (unfold Filter_def is_Filter_def)
paulson@15094
    94
apply blast
paulson@15094
    95
done
paulson@15094
    96
paulson@15094
    97
lemma is_FilterI: 
paulson@15094
    98
      "[| X <= Pow(S); 
paulson@15094
    99
               S \<in> X;  
paulson@15094
   100
               X ~= {};  
paulson@15094
   101
               {} ~: X;  
paulson@15094
   102
               \<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X;  
paulson@15094
   103
               \<forall>u v. u \<in> X & u<=v & v<=S --> v \<in> X  
paulson@15094
   104
            |] ==> is_Filter X S"
paulson@15094
   105
apply (unfold is_Filter_def)
paulson@15094
   106
apply blast
paulson@15094
   107
done
paulson@15094
   108
paulson@15094
   109
lemma mem_FiltersetI2: "[| X <= Pow(S); 
paulson@15094
   110
               S \<in> X;  
paulson@15094
   111
               X ~= {};  
paulson@15094
   112
               {} ~: X;  
paulson@15094
   113
               \<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X;  
paulson@15094
   114
               \<forall>u v. u \<in> X & u<=v & v<=S --> v \<in> X  
paulson@15094
   115
            |] ==> X \<in> Filter S"
paulson@15094
   116
by (blast intro: mem_FiltersetI is_FilterI)
paulson@15094
   117
paulson@15094
   118
lemma is_FilterE_lemma: 
paulson@15094
   119
      "is_Filter X S ==> X <= Pow(S) &  
paulson@15094
   120
                           S \<in> X &  
paulson@15094
   121
                           X ~= {} &  
paulson@15094
   122
                           {} ~: X  &  
paulson@15094
   123
                           (\<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X) &  
paulson@15094
   124
                           (\<forall>u v. u \<in> X & u <= v & v<=S --> v \<in> X)"
paulson@15094
   125
apply (unfold is_Filter_def)
paulson@15094
   126
apply fast
paulson@15094
   127
done
paulson@15094
   128
paulson@15094
   129
lemma memFiltersetE_lemma: 
paulson@15094
   130
      "X \<in> Filter S ==> X <= Pow(S) & 
paulson@15094
   131
                           S \<in> X &  
paulson@15094
   132
                           X ~= {} &  
paulson@15094
   133
                           {} ~: X  &  
paulson@15094
   134
                           (\<forall>u \<in> X. \<forall>v \<in> X. u Int v \<in> X) &  
paulson@15094
   135
                           (\<forall>u v. u \<in> X & u <= v & v<=S --> v \<in> X)"
paulson@15094
   136
by (erule mem_FiltersetD [THEN is_FilterE_lemma])
paulson@15094
   137
paulson@15094
   138
lemma Freefilter_Filter: "X \<in> Freefilter S ==> X \<in> Filter S"
paulson@15094
   139
apply (simp add: Filter_def Freefilter_def)
paulson@15094
   140
done
paulson@15094
   141
paulson@15094
   142
lemma mem_Freefilter_not_finite: "X \<in> Freefilter S ==> \<forall>y \<in> X. ~finite(y)"
paulson@15094
   143
apply (simp add: Freefilter_def)
paulson@15094
   144
done
paulson@15094
   145
paulson@15094
   146
lemma mem_FreefiltersetD1: "[| X \<in> Freefilter S; x \<in> X |] ==> ~ finite x"
paulson@15094
   147
apply (blast dest!: mem_Freefilter_not_finite)
paulson@15094
   148
done
paulson@10750
   149
paulson@15094
   150
lemmas mem_FreefiltersetE1 = mem_FreefiltersetD1 [THEN notE, standard]
paulson@15094
   151
paulson@15094
   152
lemma mem_FreefiltersetD2: "[| X \<in> Freefilter S; finite x|] ==> x ~: X"
paulson@15094
   153
apply (blast dest!: mem_Freefilter_not_finite)
paulson@15094
   154
done
paulson@15094
   155
paulson@15094
   156
lemma mem_FreefiltersetI1: 
paulson@15094
   157
      "[| X \<in> Filter S; \<forall>x. ~(x \<in> X & finite x) |] ==> X \<in> Freefilter S"
paulson@15094
   158
by (simp add: Freefilter_def)
paulson@15094
   159
paulson@15094
   160
lemma mem_FreefiltersetI2: 
paulson@15094
   161
      "[| X \<in> Filter S; \<forall>x. (x ~: X | ~ finite x) |] ==> X \<in> Freefilter S"
paulson@15094
   162
by (simp add: Freefilter_def)
paulson@15094
   163
paulson@15094
   164
lemma Filter_Int_not_empty: "[| X \<in> Filter S; A \<in> X; B \<in> X |] ==> A Int B ~= {}"
paulson@15094
   165
apply (frule_tac A = "A" and B = "B" in mem_FiltersetD1)
paulson@15094
   166
apply (auto dest!: Filter_empty_not_mem)
paulson@15094
   167
done
paulson@15094
   168
paulson@15094
   169
lemmas Filter_Int_not_emptyE = Filter_Int_not_empty [THEN notE, standard]
paulson@15094
   170
paulson@15094
   171
subsection{*Ultrafilters and Free Ultrafilters*}
paulson@15094
   172
paulson@15094
   173
lemma Ultrafilter_Filter: "X \<in> Ultrafilter S ==> X \<in> Filter S"
paulson@15094
   174
apply (simp add: Ultrafilter_def)
paulson@15094
   175
done
paulson@15094
   176
paulson@15094
   177
lemma mem_UltrafiltersetD2: 
paulson@15094
   178
      "X \<in> Ultrafilter S ==> \<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X"
paulson@15094
   179
by (auto simp add: Ultrafilter_def)
paulson@15094
   180
paulson@15094
   181
lemma mem_UltrafiltersetD3: 
paulson@15094
   182
      "[|X \<in> Ultrafilter S; A <= S; A ~: X |] ==> S - A \<in> X"
paulson@15094
   183
by (auto simp add: Ultrafilter_def)
paulson@15094
   184
paulson@15094
   185
lemma mem_UltrafiltersetD4: 
paulson@15094
   186
      "[|X \<in> Ultrafilter S; A <= S; S - A ~: X |] ==> A \<in> X"
paulson@15094
   187
by (auto simp add: Ultrafilter_def)
paulson@15094
   188
paulson@15094
   189
lemma mem_UltrafiltersetI: 
paulson@15094
   190
     "[| X \<in> Filter S;  
paulson@15094
   191
         \<forall>A \<in> Pow(S). A \<in> X | S - A \<in> X |] ==> X \<in> Ultrafilter S"
paulson@15094
   192
by (simp add: Ultrafilter_def)
paulson@15094
   193
paulson@15094
   194
lemma FreeUltrafilter_Ultrafilter: 
paulson@15094
   195
     "X \<in> FreeUltrafilter S ==> X \<in> Ultrafilter S"
paulson@15094
   196
by (auto simp add: Ultrafilter_def FreeUltrafilter_def)
paulson@15094
   197
paulson@15094
   198
lemma mem_FreeUltrafilter_not_finite: 
paulson@15094
   199
     "X \<in> FreeUltrafilter S ==> \<forall>y \<in> X. ~finite(y)"
paulson@15094
   200
by (simp add: FreeUltrafilter_def)
paulson@15094
   201
paulson@15094
   202
lemma mem_FreeUltrafiltersetD1: "[| X \<in> FreeUltrafilter S; x \<in> X |] ==> ~ finite x"
paulson@15094
   203
apply (blast dest!: mem_FreeUltrafilter_not_finite)
paulson@15094
   204
done
paulson@10750
   205
paulson@15094
   206
lemmas mem_FreeUltrafiltersetE1 = mem_FreeUltrafiltersetD1 [THEN notE, standard]
paulson@15094
   207
paulson@15094
   208
lemma mem_FreeUltrafiltersetD2: "[| X \<in> FreeUltrafilter S; finite x|] ==> x ~: X"
paulson@15094
   209
apply (blast dest!: mem_FreeUltrafilter_not_finite)
paulson@15094
   210
done
paulson@15094
   211
paulson@15094
   212
lemma mem_FreeUltrafiltersetI1: 
paulson@15094
   213
      "[| X \<in> Ultrafilter S;  
paulson@15094
   214
          \<forall>x. ~(x \<in> X & finite x) |] ==> X \<in> FreeUltrafilter S"
paulson@15094
   215
by (simp add: FreeUltrafilter_def)
paulson@15094
   216
paulson@15094
   217
lemma mem_FreeUltrafiltersetI2: 
paulson@15094
   218
      "[| X \<in> Ultrafilter S;  
paulson@15094
   219
          \<forall>x. (x ~: X | ~ finite x) |] ==> X \<in> FreeUltrafilter S"
paulson@15094
   220
by (simp add: FreeUltrafilter_def)
paulson@15094
   221
paulson@15094
   222
lemma FreeUltrafilter_iff: 
paulson@15094
   223
     "(X \<in> FreeUltrafilter S) = (X \<in> Freefilter S & (\<forall>x \<in> Pow(S). x \<in> X | S - x \<in> X))"
paulson@15094
   224
by (auto simp add: FreeUltrafilter_def Freefilter_def Ultrafilter_def)
paulson@15094
   225
paulson@15094
   226
paulson@15094
   227
(*-------------------------------------------------------------------
paulson@15094
   228
   A Filter F on S is an ultrafilter iff it is a maximal filter 
paulson@15094
   229
   i.e. whenever G is a filter on I and F <= F then F = G
paulson@15094
   230
 --------------------------------------------------------------------*)
paulson@15094
   231
(*---------------------------------------------------------------------
paulson@15094
   232
  lemmas that shows existence of an extension to what was assumed to
paulson@15094
   233
  be a maximal filter. Will be used to derive contradiction in proof of
paulson@15094
   234
  property of ultrafilter 
paulson@15094
   235
 ---------------------------------------------------------------------*)
paulson@15094
   236
lemma lemma_set_extend: "[| F ~= {}; A <= S |] ==> \<exists>x. x \<in> {X. X <= S & (\<exists>f \<in> F. A Int f <= X)}"
paulson@15094
   237
apply blast
paulson@15094
   238
done
paulson@15094
   239
paulson@15094
   240
lemma lemma_set_not_empty: "a \<in> X ==> X ~= {}"
paulson@15094
   241
apply (safe)
paulson@15094
   242
done
paulson@15094
   243
paulson@15094
   244
lemma lemma_empty_Int_subset_Compl: "x Int F <= {} ==> F <= - x"
paulson@15094
   245
apply blast
paulson@15094
   246
done
paulson@15094
   247
paulson@15094
   248
lemma mem_Filterset_disjI: 
paulson@15094
   249
      "[| F \<in> Filter S; A ~: F; A <= S|]  
paulson@15094
   250
           ==> \<forall>B. B ~: F | ~ B <= A"
paulson@15094
   251
apply (unfold Filter_def is_Filter_def)
paulson@15094
   252
apply blast
paulson@15094
   253
done
paulson@15094
   254
paulson@15094
   255
lemma Ultrafilter_max_Filter: "F \<in> Ultrafilter S ==>  
paulson@15094
   256
          (F \<in> Filter S & (\<forall>G \<in> Filter S. F <= G --> F = G))"
paulson@15094
   257
apply (auto simp add: Ultrafilter_def)
paulson@15094
   258
apply (drule_tac x = "x" in bspec)
paulson@15094
   259
apply (erule mem_FiltersetD3 , assumption)
paulson@15094
   260
apply (safe)
paulson@15094
   261
apply (drule subsetD , assumption)
paulson@15094
   262
apply (blast dest!: Filter_Int_not_empty)
paulson@15094
   263
done
paulson@10750
   264
paulson@10750
   265
paulson@15094
   266
(*--------------------------------------------------------------------------------
paulson@15094
   267
     This is a very long and tedious proof; need to break it into parts.
paulson@15094
   268
     Have proof that {X. X <= S & (\<exists>f \<in> F. A Int f <= X)} is a filter as 
paulson@15094
   269
     a lemma
paulson@15094
   270
--------------------------------------------------------------------------------*)
paulson@15094
   271
lemma max_Filter_Ultrafilter: 
paulson@15094
   272
      "[| F \<in> Filter S;  
paulson@15094
   273
          \<forall>G \<in> Filter S. F <= G --> F = G |] ==> F \<in> Ultrafilter S"
paulson@15094
   274
apply (simp add: Ultrafilter_def)
paulson@15094
   275
apply (safe)
paulson@15094
   276
apply (rule ccontr)
paulson@15094
   277
apply (frule mem_FiltersetD [THEN is_FilterD2])
paulson@15094
   278
apply (frule_tac x = "{X. X <= S & (\<exists>f \<in> F. A Int f <= X) }" in bspec)
paulson@15094
   279
apply (rule mem_FiltersetI2) 
paulson@15094
   280
apply (blast intro: elim:); 
paulson@15094
   281
apply (simp add: ); 
paulson@15094
   282
apply (blast dest: mem_FiltersetD3)
paulson@15094
   283
apply (erule lemma_set_extend [THEN exE])
paulson@15094
   284
apply (assumption , erule lemma_set_not_empty)
paulson@15094
   285
txt{*First we prove @{term "{} \<notin> {X. X \<subseteq> S \<and> (\<exists>f\<in>F. A \<inter> f \<subseteq> X)}"}*}
paulson@15094
   286
   apply (clarify ); 
paulson@15094
   287
   apply (drule lemma_empty_Int_subset_Compl)
paulson@15094
   288
   apply (frule mem_Filterset_disjI) 
paulson@15094
   289
   apply assumption; 
paulson@15094
   290
   apply (blast intro: elim:); 
paulson@15094
   291
   apply (fast dest: mem_FiltersetD3 elim:) 
paulson@15094
   292
txt{*Next case: @{term "u \<inter> v"} is an element*}
paulson@15094
   293
  apply (intro ballI) 
paulson@15094
   294
apply (simp add: ); 
paulson@15094
   295
  apply (rule conjI, blast) 
paulson@15094
   296
apply (clarify ); 
paulson@15094
   297
  apply (rule_tac x = "f Int fa" in bexI)
paulson@15094
   298
   apply (fast intro: elim:); 
paulson@15094
   299
  apply (blast dest: mem_FiltersetD1 elim:)
paulson@15094
   300
 apply force;
paulson@15094
   301
apply (blast dest: mem_FiltersetD3 elim:) 
paulson@15094
   302
done
paulson@15094
   303
paulson@15094
   304
lemma Ultrafilter_iff: "(F \<in> Ultrafilter S) = (F \<in> Filter S & (\<forall>G \<in> Filter S. F <= G --> F = G))"
paulson@15094
   305
apply (blast intro!: Ultrafilter_max_Filter max_Filter_Ultrafilter)
paulson@15094
   306
done
paulson@10750
   307
paulson@10750
   308
paulson@15094
   309
subsection{* A Few Properties of Freefilters*}
paulson@15094
   310
paulson@15094
   311
lemma lemma_Compl_cancel_eq: "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)"
paulson@15094
   312
apply auto
paulson@15094
   313
done
paulson@15094
   314
paulson@15094
   315
lemma finite_IntI1: "finite X ==> finite (X Int Y)"
paulson@15094
   316
apply (erule Int_lower1 [THEN finite_subset])
paulson@15094
   317
done
paulson@15094
   318
paulson@15094
   319
lemma finite_IntI2: "finite Y ==> finite (X Int Y)"
paulson@15094
   320
apply (erule Int_lower2 [THEN finite_subset])
paulson@15094
   321
done
paulson@15094
   322
paulson@15094
   323
lemma finite_Int_Compl_cancel: "[| finite (F1 Int Y);  
paulson@15094
   324
                  finite (F2 Int (- Y))  
paulson@15094
   325
               |] ==> finite (F1 Int F2)"
paulson@15094
   326
apply (rule_tac Y1 = "Y" in lemma_Compl_cancel_eq [THEN ssubst])
paulson@15094
   327
apply (rule finite_UnI)
paulson@15094
   328
apply (auto intro!: finite_IntI1 finite_IntI2)
paulson@15094
   329
done
paulson@15094
   330
paulson@15094
   331
lemma Freefilter_lemma_not_finite: "U \<in> Freefilter S  ==>  
paulson@15094
   332
          ~ (\<exists>f1 \<in> U. \<exists>f2 \<in> U. finite (f1 Int x)  
paulson@15094
   333
                             & finite (f2 Int (- x)))"
paulson@15094
   334
apply (safe)
paulson@15094
   335
apply (frule_tac A = "f1" and B = "f2" in Freefilter_Filter [THEN mem_FiltersetD1])
paulson@15094
   336
apply (drule_tac [3] x = "f1 Int f2" in mem_FreefiltersetD1)
paulson@15094
   337
apply (drule_tac [4] finite_Int_Compl_cancel)
paulson@15094
   338
apply auto
paulson@15094
   339
done
paulson@15094
   340
paulson@15094
   341
(* the lemmas below follow *)
paulson@15094
   342
lemma Freefilter_Compl_not_finite_disjI: "U \<in> Freefilter S ==>  
paulson@15094
   343
           \<forall>f \<in> U. ~ finite (f Int x) | ~finite (f Int (- x))"
paulson@15094
   344
by (blast dest!: Freefilter_lemma_not_finite bspec)
paulson@15094
   345
paulson@15094
   346
lemma Freefilter_Compl_not_finite_disjI2: "U \<in> Freefilter S ==> (\<forall>f \<in> U. ~ finite (f Int x)) | (\<forall>f \<in> U. ~finite (f Int (- x)))"
paulson@15094
   347
apply (blast dest!: Freefilter_lemma_not_finite bspec)
paulson@15094
   348
done
paulson@15094
   349
paulson@15094
   350
lemma cofinite_Filter: "~ finite (UNIV:: 'a set) ==> {A:: 'a set. finite (- A)} \<in> Filter UNIV"
paulson@15094
   351
apply (rule mem_FiltersetI2)
paulson@15094
   352
apply (auto simp del: Collect_empty_eq)
paulson@15094
   353
apply (erule_tac c = "UNIV" in equalityCE)
paulson@15094
   354
apply auto
paulson@15094
   355
apply (erule Compl_anti_mono [THEN finite_subset])
paulson@15094
   356
apply assumption
paulson@15094
   357
done
paulson@15094
   358
paulson@15094
   359
lemma not_finite_UNIV_disjI: "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)" 
paulson@15094
   360
apply (drule_tac A1 = "X" in Compl_partition [THEN ssubst])
paulson@15094
   361
apply simp
paulson@15094
   362
done
paulson@15094
   363
paulson@15094
   364
lemma not_finite_UNIV_Compl: "[| ~finite(UNIV :: 'a set); finite (X :: 'a set) |] ==>  ~finite (- X)"
paulson@15094
   365
apply (drule_tac X = "X" in not_finite_UNIV_disjI)
paulson@15094
   366
apply blast
paulson@15094
   367
done
paulson@15094
   368
paulson@15094
   369
lemma mem_cofinite_Filter_not_finite:
paulson@15094
   370
     "~ finite (UNIV:: 'a set) 
paulson@15094
   371
      ==> \<forall>X \<in> {A:: 'a set. finite (- A)}. ~ finite X"
paulson@15094
   372
by (auto dest: not_finite_UNIV_disjI)
paulson@15094
   373
paulson@15094
   374
lemma cofinite_Freefilter:
paulson@15094
   375
    "~ finite (UNIV:: 'a set) ==> {A:: 'a set. finite (- A)} \<in> Freefilter UNIV"
paulson@15094
   376
apply (rule mem_FreefiltersetI2)
paulson@15094
   377
apply (rule cofinite_Filter , assumption)
paulson@15094
   378
apply (blast dest!: mem_cofinite_Filter_not_finite)
paulson@15094
   379
done
paulson@15094
   380
paulson@15094
   381
(*????Set.thy*)
paulson@15094
   382
lemma UNIV_diff_Compl [simp]: "UNIV - x = - x"
paulson@15094
   383
apply auto
paulson@15094
   384
done
paulson@15094
   385
paulson@15094
   386
lemma FreeUltrafilter_contains_cofinite_set: 
paulson@15094
   387
     "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV 
paulson@15094
   388
          |] ==> {X. finite(- X)} <= U"
paulson@15094
   389
by (auto simp add: Ultrafilter_def FreeUltrafilter_def)
paulson@15094
   390
paulson@15094
   391
(*--------------------------------------------------------------------
paulson@15094
   392
   We prove: 1. Existence of maximal filter i.e. ultrafilter
paulson@15094
   393
             2. Freeness property i.e ultrafilter is free
paulson@15094
   394
             Use a locale to prove various lemmas and then 
paulson@15094
   395
             export main result: The Ultrafilter Theorem
paulson@15094
   396
 -------------------------------------------------------------------*)
paulson@15094
   397
paulson@15094
   398
lemma (in UFT) chain_Un_subset_Pow: 
paulson@15094
   399
   "!!(c :: 'a set set set). c \<in> chain (superfrechet S) ==>  Union c <= Pow S"
paulson@15094
   400
apply (simp add: chain_def superfrechet_def frechet_def)
paulson@15094
   401
apply (blast dest: mem_FiltersetD3 elim:) 
paulson@15094
   402
done
paulson@15094
   403
paulson@15094
   404
lemma (in UFT) mem_chain_psubset_empty: 
paulson@15094
   405
          "!!(c :: 'a set set set). c: chain (superfrechet S)  
paulson@15094
   406
          ==> !x: c. {} < x"
paulson@15094
   407
by (auto simp add: chain_def Filter_def is_Filter_def superfrechet_def frechet_def)
paulson@15094
   408
paulson@15094
   409
lemma (in UFT) chain_Un_not_empty: "!!(c :: 'a set set set).  
paulson@15094
   410
             [| c: chain (superfrechet S); 
paulson@15094
   411
                c ~= {} |] 
paulson@15094
   412
             ==> Union(c) ~= {}"
paulson@15094
   413
apply (drule mem_chain_psubset_empty)
paulson@15094
   414
apply (safe)
paulson@15094
   415
apply (drule bspec , assumption)
paulson@15094
   416
apply (auto dest: Union_upper bspec simp add: psubset_def)
paulson@15094
   417
done
paulson@15094
   418
paulson@15094
   419
lemma (in UFT) Filter_empty_not_mem_Un: 
paulson@15094
   420
       "!!(c :: 'a set set set). c \<in> chain (superfrechet S) ==> {} ~: Union(c)"
paulson@15094
   421
by (auto simp add: is_Filter_def Filter_def chain_def superfrechet_def)
paulson@15094
   422
paulson@15094
   423
lemma (in UFT) Filter_Un_Int: "c \<in> chain (superfrechet S)  
paulson@15094
   424
          ==> \<forall>u \<in> Union(c). \<forall>v \<in> Union(c). u Int v \<in> Union(c)"
paulson@15094
   425
apply (safe)
paulson@15094
   426
apply (frule_tac x = "X" and y = "Xa" in chainD)
paulson@15094
   427
apply (assumption)+
paulson@15094
   428
apply (drule chainD2)
paulson@15094
   429
apply (erule disjE)
paulson@15094
   430
 apply (rule_tac [2] X = "X" in UnionI)
paulson@15094
   431
  apply (rule_tac X = "Xa" in UnionI)
paulson@15094
   432
apply (auto intro: mem_FiltersetD1 simp add: superfrechet_def)
paulson@15094
   433
done
paulson@15094
   434
paulson@15094
   435
lemma (in UFT) Filter_Un_subset: "c \<in> chain (superfrechet S)  
paulson@15094
   436
          ==> \<forall>u v. u \<in> Union(c) &  
paulson@15094
   437
                  (u :: 'a set) <= v & v <= S --> v \<in> Union(c)"
paulson@15094
   438
apply (safe)
paulson@15094
   439
apply (drule chainD2)
paulson@15094
   440
apply (drule subsetD , assumption)
paulson@15094
   441
apply (rule UnionI , assumption)
paulson@15094
   442
apply (auto intro: mem_FiltersetD2 simp add: superfrechet_def)
paulson@15094
   443
done
paulson@15094
   444
paulson@15094
   445
lemma (in UFT) lemma_mem_chain_Filter:
paulson@15094
   446
      "!!(c :: 'a set set set).  
paulson@15094
   447
             [| c \<in> chain (superfrechet S); 
paulson@15094
   448
                x \<in> c  
paulson@15094
   449
             |] ==> x \<in> Filter S"
paulson@15094
   450
by (auto simp add: chain_def superfrechet_def)
paulson@15094
   451
paulson@15094
   452
lemma (in UFT) lemma_mem_chain_frechet_subset: 
paulson@15094
   453
     "!!(c :: 'a set set set).  
paulson@15094
   454
             [| c \<in> chain (superfrechet S); 
paulson@15094
   455
                x \<in> c  
paulson@15094
   456
             |] ==> frechet S <= x"
paulson@15094
   457
by (auto simp add: chain_def superfrechet_def)
paulson@15094
   458
paulson@15094
   459
lemma (in UFT) Un_chain_mem_cofinite_Filter_set: "!!(c :: 'a set set set).  
paulson@15094
   460
          [| c ~= {};  
paulson@15094
   461
             c \<in> chain (superfrechet (UNIV :: 'a set)) 
paulson@15094
   462
          |] ==> Union c \<in> superfrechet (UNIV)"
paulson@15094
   463
apply (simp (no_asm) add: superfrechet_def frechet_def)
paulson@15094
   464
apply (safe)
paulson@15094
   465
apply (rule mem_FiltersetI2)
paulson@15094
   466
apply (erule chain_Un_subset_Pow)
paulson@15094
   467
apply (rule UnionI , assumption)
paulson@15094
   468
apply (erule lemma_mem_chain_Filter [THEN mem_FiltersetD4] , assumption)
paulson@15094
   469
apply (erule chain_Un_not_empty)
paulson@15094
   470
apply (erule_tac [2] Filter_empty_not_mem_Un)
paulson@15094
   471
apply (erule_tac [2] Filter_Un_Int)
paulson@15094
   472
apply (erule_tac [2] Filter_Un_subset)
paulson@15094
   473
apply (subgoal_tac [2] "xa \<in> frechet (UNIV) ")
paulson@15094
   474
apply (blast intro: elim:); 
paulson@15094
   475
apply (rule UnionI)
paulson@15094
   476
apply assumption; 
paulson@15094
   477
apply (rule lemma_mem_chain_frechet_subset [THEN subsetD])
paulson@15094
   478
apply (auto simp add: frechet_def)
paulson@15094
   479
done
paulson@15094
   480
paulson@15094
   481
lemma (in UFT) max_cofinite_Filter_Ex: "\<exists>U \<in> superfrechet (UNIV).  
paulson@15094
   482
                \<forall>G \<in> superfrechet (UNIV). U <= G --> U = G"
paulson@15094
   483
apply (rule Zorn_Lemma2)
paulson@15094
   484
apply (insert not_finite_UNIV [THEN cofinite_Filter])
paulson@15094
   485
apply (safe)
paulson@15094
   486
apply (rule_tac Q = "c={}" in excluded_middle [THEN disjE])
paulson@15094
   487
apply (rule_tac x = "Union c" in bexI , blast)
paulson@15094
   488
apply (rule Un_chain_mem_cofinite_Filter_set);
paulson@15094
   489
apply (auto simp add: superfrechet_def frechet_def)
paulson@15094
   490
done
paulson@15094
   491
paulson@15094
   492
lemma (in UFT) max_cofinite_Freefilter_Ex: "\<exists>U \<in> superfrechet UNIV. ( 
paulson@15094
   493
                \<forall>G \<in> superfrechet UNIV. U <= G --> U = G)   
paulson@15094
   494
                              & (\<forall>x \<in> U. ~finite x)"
paulson@15094
   495
apply (insert not_finite_UNIV [THEN UFT.max_cofinite_Filter_Ex]);
paulson@15094
   496
apply (safe)
paulson@15094
   497
apply (rule_tac x = "U" in bexI)
paulson@15094
   498
apply (auto simp add: superfrechet_def frechet_def)
paulson@15094
   499
apply (drule_tac c = "- x" in subsetD)
paulson@15094
   500
apply (simp (no_asm_simp))
paulson@15094
   501
apply (frule_tac A = "x" and B = "- x" in mem_FiltersetD1)
paulson@15094
   502
apply (drule_tac [3] Filter_empty_not_mem)
paulson@15094
   503
apply (auto ); 
paulson@15094
   504
done
paulson@15094
   505
paulson@15094
   506
text{*There exists a free ultrafilter on any infinite set*}
paulson@15094
   507
paulson@15094
   508
theorem (in UFT) FreeUltrafilter_ex: "\<exists>U. U \<in> FreeUltrafilter (UNIV :: 'a set)"
paulson@15094
   509
apply (simp add: FreeUltrafilter_def)
paulson@15094
   510
apply (insert not_finite_UNIV [THEN UFT.max_cofinite_Freefilter_Ex])
paulson@15094
   511
apply (simp add: superfrechet_def Ultrafilter_iff frechet_def)
paulson@15094
   512
apply (safe)
paulson@15094
   513
apply (rule_tac x = "U" in exI)
paulson@15094
   514
apply (safe)
paulson@15094
   515
apply blast
paulson@15094
   516
done
paulson@15094
   517
paulson@15094
   518
theorems FreeUltrafilter_Ex = UFT.FreeUltrafilter_ex
paulson@15094
   519
paulson@15094
   520
end