src/HOL/Real/Hyperreal/Filter.ML
author paulson
Fri Nov 27 11:24:27 1998 +0100 (1998-11-27)
changeset 5979 11cbf236ca16
child 6024 cb87f103d114
permissions -rw-r--r--
Addition of Hyperreal theories Zorn and Filter
paulson@5979
     1
(*  Title       : Filter.ML
paulson@5979
     2
    Author      : Jacques D. Fleuriot
paulson@5979
     3
    Copyright   : 1998  University of Cambridge
paulson@5979
     4
    Description : Filters and Ultrafilter
paulson@5979
     5
*) 
paulson@5979
     6
paulson@5979
     7
open Filter;
paulson@5979
     8
paulson@5979
     9
paulson@5979
    10
(*------------------------------------------------------------------
paulson@5979
    11
      Properties of Filters and Freefilters - 
paulson@5979
    12
      rules for intro, destruction etc.
paulson@5979
    13
 ------------------------------------------------------------------*)
paulson@5979
    14
paulson@5979
    15
Goalw [is_Filter_def] "is_Filter X S ==> X <= Pow(S)";
paulson@5979
    16
by (Blast_tac 1);
paulson@5979
    17
qed "is_FilterD1";
paulson@5979
    18
paulson@5979
    19
Goalw [is_Filter_def] "is_Filter X S ==> X ~= {}";
paulson@5979
    20
by (Blast_tac 1);
paulson@5979
    21
qed "is_FilterD2";
paulson@5979
    22
paulson@5979
    23
Goalw [is_Filter_def] "is_Filter X S ==> {} ~: X";
paulson@5979
    24
by (Blast_tac 1);
paulson@5979
    25
qed "is_FilterD3";
paulson@5979
    26
paulson@5979
    27
Goalw [Filter_def] "is_Filter X S ==> X : Filter S";
paulson@5979
    28
by (Blast_tac 1);
paulson@5979
    29
qed "mem_FiltersetI";
paulson@5979
    30
paulson@5979
    31
Goalw [Filter_def] "X : Filter S ==> is_Filter X S";
paulson@5979
    32
by (Blast_tac 1);
paulson@5979
    33
qed "mem_FiltersetD";
paulson@5979
    34
paulson@5979
    35
Goal "X : Filter S ==> {} ~: X";
paulson@5979
    36
by (etac (mem_FiltersetD RS is_FilterD3) 1);
paulson@5979
    37
qed "Filter_empty_not_mem";
paulson@5979
    38
paulson@5979
    39
bind_thm ("Filter_empty_not_memE",(Filter_empty_not_mem RS notE));
paulson@5979
    40
paulson@5979
    41
Goalw [Filter_def,is_Filter_def] 
paulson@5979
    42
      "[| X: Filter S; A: X; B: X |] ==> A Int B : X";
paulson@5979
    43
by (Blast_tac 1);
paulson@5979
    44
qed "mem_FiltersetD1";
paulson@5979
    45
paulson@5979
    46
Goalw [Filter_def,is_Filter_def] 
paulson@5979
    47
      "[| X: Filter S; A: X; A <= B; B <= S|] ==> B : X";
paulson@5979
    48
by (Blast_tac 1);
paulson@5979
    49
qed "mem_FiltersetD2";
paulson@5979
    50
paulson@5979
    51
Goalw [Filter_def,is_Filter_def] 
paulson@5979
    52
      "[| X: Filter S; A: X |] ==> A : Pow S";
paulson@5979
    53
by (Blast_tac 1);
paulson@5979
    54
qed "mem_FiltersetD3";
paulson@5979
    55
paulson@5979
    56
Goalw [Filter_def,is_Filter_def] 
paulson@5979
    57
      "X: Filter S  ==> S : X";
paulson@5979
    58
by (Blast_tac 1);
paulson@5979
    59
qed "mem_FiltersetD4";
paulson@5979
    60
paulson@5979
    61
Goalw [is_Filter_def] 
paulson@5979
    62
      "[| X <= Pow(S);\
paulson@5979
    63
\              S : X; \
paulson@5979
    64
\              X ~= {}; \
paulson@5979
    65
\              {} ~: X; \
paulson@5979
    66
\              ALL u: X. ALL v: X. u Int v : X; \
paulson@5979
    67
\              ALL u v. u: X & u<=v & v<=S --> v: X \
paulson@5979
    68
\           |] ==> is_Filter X S";
paulson@5979
    69
by (Blast_tac 1); 
paulson@5979
    70
qed "is_FilterI";
paulson@5979
    71
paulson@5979
    72
Goal "[| X <= Pow(S);\
paulson@5979
    73
\              S : X; \
paulson@5979
    74
\              X ~= {}; \
paulson@5979
    75
\              {} ~: X; \
paulson@5979
    76
\              ALL u: X. ALL v: X. u Int v : X; \
paulson@5979
    77
\              ALL u v. u: X & u<=v & v<=S --> v: X \
paulson@5979
    78
\           |] ==> X: Filter S";
paulson@5979
    79
by (blast_tac (claset() addIs [mem_FiltersetI,is_FilterI]) 1);
paulson@5979
    80
qed "mem_FiltersetI2";
paulson@5979
    81
paulson@5979
    82
Goalw [is_Filter_def]
paulson@5979
    83
      "is_Filter X S ==> X <= Pow(S) & \
paulson@5979
    84
\                          S : X & \
paulson@5979
    85
\                          X ~= {} & \
paulson@5979
    86
\                          {} ~: X  & \
paulson@5979
    87
\                          (ALL u: X. ALL v: X. u Int v : X) & \
paulson@5979
    88
\                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
paulson@5979
    89
by (Fast_tac 1);
paulson@5979
    90
qed "is_FilterE_lemma";
paulson@5979
    91
paulson@5979
    92
Goalw [is_Filter_def]
paulson@5979
    93
      "X : Filter S ==> X <= Pow(S) &\
paulson@5979
    94
\                          S : X & \
paulson@5979
    95
\                          X ~= {} & \
paulson@5979
    96
\                          {} ~: X  & \
paulson@5979
    97
\                          (ALL u: X. ALL v: X. u Int v : X) & \
paulson@5979
    98
\                          (ALL u v. u: X & u <= v & v<=S --> v: X)";
paulson@5979
    99
by (etac (mem_FiltersetD RS is_FilterE_lemma) 1);
paulson@5979
   100
qed "memFiltersetE_lemma";
paulson@5979
   101
paulson@5979
   102
Goalw [Filter_def,Freefilter_def] 
paulson@5979
   103
      "X: Freefilter S ==> X: Filter S";
paulson@5979
   104
by (Fast_tac 1);
paulson@5979
   105
qed "Freefilter_Filter";
paulson@5979
   106
paulson@5979
   107
Goalw [Freefilter_def] 
paulson@5979
   108
      "X: Freefilter S ==> ALL y: X. ~finite(y)";
paulson@5979
   109
by (Blast_tac 1);
paulson@5979
   110
qed "mem_Freefilter_not_finite";
paulson@5979
   111
paulson@5979
   112
Goal "[| X: Freefilter S; x: X |] ==> ~ finite x";
paulson@5979
   113
by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
paulson@5979
   114
qed "mem_FreefiltersetD1";
paulson@5979
   115
paulson@5979
   116
bind_thm ("mem_FreefiltersetE1", (mem_FreefiltersetD1 RS notE));
paulson@5979
   117
paulson@5979
   118
Goal "[| X: Freefilter S; finite x|] ==> x ~: X";
paulson@5979
   119
by (blast_tac (claset() addSDs [mem_Freefilter_not_finite]) 1);
paulson@5979
   120
qed "mem_FreefiltersetD2";
paulson@5979
   121
paulson@5979
   122
Goalw [Freefilter_def] 
paulson@5979
   123
      "[| X: Filter S; ALL x. ~(x: X & finite x) |] ==> X: Freefilter S";
paulson@5979
   124
by (Blast_tac 1);
paulson@5979
   125
qed "mem_FreefiltersetI1";
paulson@5979
   126
paulson@5979
   127
Goalw [Freefilter_def]
paulson@5979
   128
      "[| X: Filter S; ALL x. (x ~: X | ~ finite x) |] ==> X: Freefilter S";
paulson@5979
   129
by (Blast_tac 1);
paulson@5979
   130
qed "mem_FreefiltersetI2";
paulson@5979
   131
paulson@5979
   132
Goal "[| X: Filter S; A: X; B: X |] ==> A Int B ~= {}";
paulson@5979
   133
by (forw_inst_tac [("A","A"),("B","B")] mem_FiltersetD1 1);
paulson@5979
   134
by (auto_tac (claset() addSDs [Filter_empty_not_mem],simpset()));
paulson@5979
   135
qed "Filter_Int_not_empty";
paulson@5979
   136
paulson@5979
   137
bind_thm ("Filter_Int_not_emptyE",(Filter_Int_not_empty RS notE));
paulson@5979
   138
paulson@5979
   139
(*----------------------------------------------------------------------------------
paulson@5979
   140
              Ultrafilters and Free ultrafilters
paulson@5979
   141
 ----------------------------------------------------------------------------------*)
paulson@5979
   142
paulson@5979
   143
Goalw [Ultrafilter_def] "X : Ultrafilter S ==> X: Filter S";
paulson@5979
   144
by (Blast_tac 1);
paulson@5979
   145
qed "Ultrafilter_Filter";
paulson@5979
   146
paulson@5979
   147
Goalw [Ultrafilter_def] 
paulson@5979
   148
      "X : Ultrafilter S ==> !A: Pow(S). A : X | S - A: X";
paulson@5979
   149
by (Blast_tac 1);
paulson@5979
   150
qed "mem_UltrafiltersetD2";
paulson@5979
   151
paulson@5979
   152
Goalw [Ultrafilter_def] 
paulson@5979
   153
      "[|X : Ultrafilter S; A <= S; A ~: X |] ==> S - A: X";
paulson@5979
   154
by (Blast_tac 1);
paulson@5979
   155
qed "mem_UltrafiltersetD3";
paulson@5979
   156
paulson@5979
   157
Goalw [Ultrafilter_def] 
paulson@5979
   158
      "[|X : Ultrafilter S; A <= S; S - A ~: X |] ==> A: X";
paulson@5979
   159
by (Blast_tac 1);
paulson@5979
   160
qed "mem_UltrafiltersetD4";
paulson@5979
   161
paulson@5979
   162
Goalw [Ultrafilter_def]
paulson@5979
   163
     "[| X: Filter S; \
paulson@5979
   164
\             ALL A: Pow(S). A: X | S - A : X |] ==> X: Ultrafilter S";
paulson@5979
   165
by (Blast_tac 1);
paulson@5979
   166
qed "mem_UltrafiltersetI";
paulson@5979
   167
paulson@5979
   168
Goalw [Ultrafilter_def,FreeUltrafilter_def]
paulson@5979
   169
     "X: FreeUltrafilter S ==> X: Ultrafilter S";
paulson@5979
   170
by (Blast_tac 1);
paulson@5979
   171
qed "FreeUltrafilter_Ultrafilter";
paulson@5979
   172
paulson@5979
   173
Goalw [FreeUltrafilter_def]
paulson@5979
   174
     "X: FreeUltrafilter S ==> ALL y: X. ~finite(y)";
paulson@5979
   175
by (Blast_tac 1);
paulson@5979
   176
qed "mem_FreeUltrafilter_not_finite";
paulson@5979
   177
paulson@5979
   178
Goal "[| X: FreeUltrafilter S; x: X |] ==> ~ finite x";
paulson@5979
   179
by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
paulson@5979
   180
qed "mem_FreeUltrafiltersetD1";
paulson@5979
   181
paulson@5979
   182
bind_thm ("mem_FreeUltrafiltersetE1", (mem_FreeUltrafiltersetD1 RS notE));
paulson@5979
   183
paulson@5979
   184
Goal "[| X: FreeUltrafilter S; finite x|] ==> x ~: X";
paulson@5979
   185
by (blast_tac (claset() addSDs [mem_FreeUltrafilter_not_finite]) 1);
paulson@5979
   186
qed "mem_FreeUltrafiltersetD2";
paulson@5979
   187
paulson@5979
   188
Goalw [FreeUltrafilter_def] 
paulson@5979
   189
      "[| X: Ultrafilter S; \
paulson@5979
   190
\              ALL x. ~(x: X & finite x) |] ==> X: FreeUltrafilter S";
paulson@5979
   191
by (Blast_tac 1);
paulson@5979
   192
qed "mem_FreeUltrafiltersetI1";
paulson@5979
   193
paulson@5979
   194
Goalw [FreeUltrafilter_def]
paulson@5979
   195
      "[| X: Ultrafilter S; \
paulson@5979
   196
\              ALL x. (x ~: X | ~ finite x) |] ==> X: FreeUltrafilter S";
paulson@5979
   197
by (Blast_tac 1);
paulson@5979
   198
qed "mem_FreeUltrafiltersetI2";
paulson@5979
   199
paulson@5979
   200
Goalw [FreeUltrafilter_def,Freefilter_def,Ultrafilter_def]
paulson@5979
   201
     "(X: FreeUltrafilter S) = (X: Freefilter S & (ALL x:Pow(S). x: X | S - x: X))";
paulson@5979
   202
by (Blast_tac 1);
paulson@5979
   203
qed "FreeUltrafilter_iff";
paulson@5979
   204
paulson@5979
   205
(*-------------------------------------------------------------------
paulson@5979
   206
   A Filter F on S is an ultrafilter iff it is a maximal filter 
paulson@5979
   207
   i.e. whenever G is a filter on I and F <= F then F = G
paulson@5979
   208
 --------------------------------------------------------------------*)
paulson@5979
   209
(*---------------------------------------------------------------------
paulson@5979
   210
  lemmas that shows existence of an extension to what was assumed to
paulson@5979
   211
  be a maximal filter. Will be used to derive contradiction in proof of
paulson@5979
   212
  property of ultrafilter 
paulson@5979
   213
 ---------------------------------------------------------------------*)
paulson@5979
   214
Goal "[| F ~= {}; A <= S |] ==> \
paulson@5979
   215
\        EX x. x: {X. X <= S & (EX f:F. A Int f <= X)}";
paulson@5979
   216
by (Blast_tac 1);
paulson@5979
   217
qed "lemma_set_extend";
paulson@5979
   218
paulson@5979
   219
Goal "a: X ==> X ~= {}";
paulson@5979
   220
by (Step_tac 1);
paulson@5979
   221
qed "lemma_set_not_empty";
paulson@5979
   222
paulson@5979
   223
Goal "x Int F <= {} ==> F <= - x";
paulson@5979
   224
by (Blast_tac 1);
paulson@5979
   225
qed "lemma_empty_Int_subset_Compl";
paulson@5979
   226
paulson@5979
   227
Goalw [Filter_def,is_Filter_def]
paulson@5979
   228
      "[| F: Filter S; A ~: F; A <= S|] \
paulson@5979
   229
\          ==> ALL B. B ~: F | ~ B <= A";
paulson@5979
   230
by (Blast_tac 1);
paulson@5979
   231
qed "mem_Filterset_disjI";
paulson@5979
   232
paulson@5979
   233
Goal "F : Ultrafilter S ==> \
paulson@5979
   234
\         (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
paulson@5979
   235
by (auto_tac (claset(),simpset() addsimps [Ultrafilter_def]));
paulson@5979
   236
by (dres_inst_tac [("x","x")] bspec 1);
paulson@5979
   237
by (etac mem_FiltersetD3 1 THEN assume_tac 1);
paulson@5979
   238
by (Step_tac 1);
paulson@5979
   239
by (dtac subsetD 1 THEN assume_tac 1);
paulson@5979
   240
by (blast_tac (claset() addSDs [Filter_Int_not_empty]) 1);
paulson@5979
   241
qed "Ultrafilter_max_Filter";
paulson@5979
   242
paulson@5979
   243
paulson@5979
   244
(*--------------------------------------------------------------------------------
paulson@5979
   245
     This is a very long and tedious proof; need to break it into parts.
paulson@5979
   246
     Have proof that {X. X <= S & (EX f: F. A Int f <= X)} is a filter as 
paulson@5979
   247
     a lemma
paulson@5979
   248
--------------------------------------------------------------------------------*)
paulson@5979
   249
Goalw [Ultrafilter_def] 
paulson@5979
   250
      "[| F: Filter S; \
paulson@5979
   251
\              ALL G: Filter S. F <= G --> F = G |] ==> F : Ultrafilter S";
paulson@5979
   252
by (Step_tac 1);
paulson@5979
   253
by (rtac ccontr 1);
paulson@5979
   254
by (forward_tac [mem_FiltersetD RS is_FilterD2] 1);
paulson@5979
   255
by (forw_inst_tac [("x","{X. X <= S & (EX f: F. A Int f <= X)}")] bspec 1);
paulson@5979
   256
by (EVERY1[rtac mem_FiltersetI2, Blast_tac, Asm_full_simp_tac]);
paulson@5979
   257
by (blast_tac (claset() addDs [mem_FiltersetD3]) 1);
paulson@5979
   258
by (etac (lemma_set_extend RS exE) 1);
paulson@5979
   259
by (assume_tac 1 THEN etac lemma_set_not_empty 1);
paulson@5979
   260
by (REPEAT(rtac ballI 2) THEN Asm_full_simp_tac 2);
paulson@5979
   261
by (rtac conjI 2 THEN Blast_tac 2);
paulson@5979
   262
by (REPEAT(etac conjE 2) THEN REPEAT(etac bexE 2));
paulson@5979
   263
by (res_inst_tac [("x","f Int fa")] bexI 2);
paulson@5979
   264
by (etac mem_FiltersetD1 3);
paulson@5979
   265
by (assume_tac 3 THEN assume_tac 3);
paulson@5979
   266
by (Fast_tac 2);
paulson@5979
   267
by (EVERY[REPEAT(rtac allI 2), rtac impI 2,Asm_full_simp_tac 2]);
paulson@5979
   268
by (EVERY[REPEAT(etac conjE 2), etac bexE 2]);
paulson@5979
   269
by (res_inst_tac [("x","f")] bexI 2);
paulson@5979
   270
by (rtac subsetI 2);
paulson@5979
   271
by (Fast_tac 2 THEN assume_tac 2);
paulson@5979
   272
by (Step_tac 2);
paulson@5979
   273
by (Blast_tac 3);
paulson@5979
   274
by (eres_inst_tac [("c","A")] equalityCE 3);
paulson@5979
   275
by (REPEAT(Blast_tac 3));
paulson@5979
   276
by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2);
paulson@5979
   277
by (Blast_tac 2);
paulson@5979
   278
by (dtac lemma_empty_Int_subset_Compl 1);
paulson@5979
   279
by (EVERY1[forward_tac [mem_Filterset_disjI], assume_tac, Fast_tac]);
paulson@5979
   280
by (dtac mem_FiltersetD3 1 THEN assume_tac 1);
paulson@5979
   281
by (dres_inst_tac [("x","f")] spec 1);
paulson@5979
   282
by (Blast_tac 1);
paulson@5979
   283
qed "max_Filter_Ultrafilter";
paulson@5979
   284
paulson@5979
   285
Goal "(F : Ultrafilter S) = (F: Filter S & (ALL G: Filter S. F <= G --> F = G))";
paulson@5979
   286
by (blast_tac (claset() addSIs [Ultrafilter_max_Filter,max_Filter_Ultrafilter]) 1);
paulson@5979
   287
qed "Ultrafilter_iff";
paulson@5979
   288
paulson@5979
   289
(*--------------------------------------------------------------------
paulson@5979
   290
             A few properties of freefilters
paulson@5979
   291
 -------------------------------------------------------------------*)
paulson@5979
   292
paulson@5979
   293
Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int - Y) Int F1)";
paulson@5979
   294
by (Auto_tac);
paulson@5979
   295
qed "lemma_Compl_cancel_eq";
paulson@5979
   296
paulson@5979
   297
Goal "finite X ==> finite (X Int Y)";
paulson@5979
   298
by (etac (Int_lower1 RS finite_subset) 1);
paulson@5979
   299
qed "finite_IntI1";
paulson@5979
   300
paulson@5979
   301
Goal "finite Y ==> finite (X Int Y)";
paulson@5979
   302
by (etac (Int_lower2 RS finite_subset) 1);
paulson@5979
   303
qed "finite_IntI2";
paulson@5979
   304
paulson@5979
   305
Goal "[| finite (F1 Int Y); \
paulson@5979
   306
\                 finite (F2 Int - Y) \
paulson@5979
   307
\              |] ==> finite (F1 Int F2)";
paulson@5979
   308
by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1);
paulson@5979
   309
by (rtac finite_UnI 1);
paulson@5979
   310
by (auto_tac (claset() addSIs [finite_IntI1,finite_IntI2],simpset()));
paulson@5979
   311
qed "finite_Int_Compl_cancel";
paulson@5979
   312
paulson@5979
   313
Goal "U: Freefilter S  ==> \
paulson@5979
   314
\         ~ (EX f1: U. EX f2: U. finite (f1 Int x) \
paulson@5979
   315
\                            & finite (f2 Int (- x)))";
paulson@5979
   316
by (Step_tac 1);
paulson@5979
   317
by (forw_inst_tac [("A","f1"),("B","f2")] 
paulson@5979
   318
    (Freefilter_Filter RS mem_FiltersetD1) 1);
paulson@5979
   319
by (dres_inst_tac [("x","f1 Int f2")] mem_FreefiltersetD1 3);
paulson@5979
   320
by (dtac finite_Int_Compl_cancel 4);
paulson@5979
   321
by (Auto_tac);
paulson@5979
   322
qed "Freefilter_lemma_not_finite";
paulson@5979
   323
paulson@5979
   324
(* the lemmas below follow *)
paulson@5979
   325
Goal "U: Freefilter S ==> \
paulson@5979
   326
\          ALL f: U. ~ finite (f Int x) | ~finite (f Int (- x))";
paulson@5979
   327
by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
paulson@5979
   328
qed "Freefilter_Compl_not_finite_disjI";
paulson@5979
   329
paulson@5979
   330
Goal "U: Freefilter S ==> \
paulson@5979
   331
\          (ALL f: U. ~ finite (f Int x)) | (ALL f:U. ~finite (f Int (- x)))";
paulson@5979
   332
by (blast_tac (claset() addSDs [Freefilter_lemma_not_finite,bspec]) 1);
paulson@5979
   333
qed "Freefilter_Compl_not_finite_disjI2";
paulson@5979
   334
paulson@5979
   335
Goal "- UNIV = {}";
paulson@5979
   336
by (Auto_tac );
paulson@5979
   337
qed "Compl_UNIV_eq";
paulson@5979
   338
paulson@5979
   339
Addsimps [Compl_UNIV_eq];
paulson@5979
   340
paulson@5979
   341
Goal "- {} = UNIV";
paulson@5979
   342
by (Auto_tac );
paulson@5979
   343
qed "Compl_empty_eq";
paulson@5979
   344
paulson@5979
   345
Addsimps [Compl_empty_eq];
paulson@5979
   346
paulson@5979
   347
val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
paulson@5979
   348
\            {A:: 'a set. finite (- A)} : Filter UNIV";
paulson@5979
   349
by (cut_facts_tac [prem] 1);
paulson@5979
   350
by (rtac mem_FiltersetI2 1);
paulson@5979
   351
by (auto_tac (claset(),simpset() addsimps [Compl_Int]));
paulson@5979
   352
by (eres_inst_tac [("c","UNIV")] equalityCE 1);
paulson@5979
   353
by (Auto_tac);
paulson@5979
   354
by (etac (Compl_anti_mono RS finite_subset) 1);
paulson@5979
   355
by (assume_tac 1);
paulson@5979
   356
qed "cofinite_Filter";
paulson@5979
   357
paulson@5979
   358
Goal "~finite(UNIV :: 'a set) ==> ~finite (X :: 'a set) | ~finite (- X)";
paulson@5979
   359
by (dres_inst_tac [("A1","X")] (Compl_partition RS ssubst) 1);
paulson@5979
   360
by (Asm_full_simp_tac 1); 
paulson@5979
   361
qed "not_finite_UNIV_disjI";
paulson@5979
   362
paulson@5979
   363
Goal "[| ~finite(UNIV :: 'a set); \
paulson@5979
   364
\                 finite (X :: 'a set) \
paulson@5979
   365
\              |] ==>  ~finite (- X)";
paulson@5979
   366
by (dres_inst_tac [("X","X")] not_finite_UNIV_disjI 1);
paulson@5979
   367
by (Blast_tac 1);
paulson@5979
   368
qed "not_finite_UNIV_Compl";
paulson@5979
   369
paulson@5979
   370
val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
paulson@5979
   371
\            !X: {A:: 'a set. finite (- A)}. ~ finite X";
paulson@5979
   372
by (cut_facts_tac [prem] 1);
paulson@5979
   373
by (auto_tac (claset() addDs [not_finite_UNIV_disjI],simpset()));
paulson@5979
   374
qed "mem_cofinite_Filter_not_finite";
paulson@5979
   375
paulson@5979
   376
val [prem] = goal thy "~ finite (UNIV:: 'a set) ==> \
paulson@5979
   377
\            {A:: 'a set. finite (- A)} : Freefilter UNIV";
paulson@5979
   378
by (cut_facts_tac [prem] 1);
paulson@5979
   379
by (rtac mem_FreefiltersetI2 1);
paulson@5979
   380
by (rtac cofinite_Filter 1 THEN assume_tac 1);
paulson@5979
   381
by (blast_tac (claset() addSDs [mem_cofinite_Filter_not_finite]) 1);
paulson@5979
   382
qed "cofinite_Freefilter";
paulson@5979
   383
paulson@5979
   384
Goal "UNIV - x = - x";
paulson@5979
   385
by (Auto_tac);
paulson@5979
   386
qed "UNIV_diff_Compl";
paulson@5979
   387
Addsimps [UNIV_diff_Compl];
paulson@5979
   388
paulson@5979
   389
Goalw [Ultrafilter_def,FreeUltrafilter_def]
paulson@5979
   390
     "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\
paulson@5979
   391
\         |] ==> {X. finite(- X)} <= U";
paulson@5979
   392
by (forward_tac [cofinite_Filter] 1);
paulson@5979
   393
by (Step_tac 1);
paulson@5979
   394
by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1);
paulson@5979
   395
by (assume_tac 1);
paulson@5979
   396
by (Step_tac 1 THEN Fast_tac 1);
paulson@5979
   397
by (dres_inst_tac [("x","x")] bspec 1);
paulson@5979
   398
by (Blast_tac 1);
paulson@5979
   399
by (asm_full_simp_tac (simpset() addsimps [UNIV_diff_Compl]) 1);
paulson@5979
   400
qed "FreeUltrafilter_contains_cofinite_set";
paulson@5979
   401
paulson@5979
   402
(*--------------------------------------------------------------------
paulson@5979
   403
   We prove: 1. Existence of maximal filter i.e. ultrafilter
paulson@5979
   404
             2. Freeness property i.e ultrafilter is free
paulson@5979
   405
             Use a locale to prove various lemmas and then 
paulson@5979
   406
             export main result- The Ultrafilter Theorem
paulson@5979
   407
 -------------------------------------------------------------------*)
paulson@5979
   408
Open_locale "UFT"; 
paulson@5979
   409
paulson@5979
   410
Goalw [chain_def, thm "superfrechet_def", thm "frechet_def"]
paulson@5979
   411
   "!!(c :: 'a set set set). c : chain (superfrechet S) ==>  Union c <= Pow S";
paulson@5979
   412
by (Step_tac 1);
paulson@5979
   413
by (dtac subsetD 1 THEN assume_tac 1);
paulson@5979
   414
by (Step_tac 1);
paulson@5979
   415
by (dres_inst_tac [("X","X")] mem_FiltersetD3 1);
paulson@5979
   416
by (Auto_tac);
paulson@5979
   417
qed "chain_Un_subset_Pow";
paulson@5979
   418
paulson@5979
   419
Goalw [chain_def,Filter_def,is_Filter_def,
paulson@5979
   420
           thm "superfrechet_def", thm "frechet_def"] 
paulson@5979
   421
          "!!(c :: 'a set set set). c: chain (superfrechet S) \
paulson@5979
   422
\         ==> !x: c. {} < x";
paulson@5979
   423
by (blast_tac (claset() addSIs [psubsetI]) 1);
paulson@5979
   424
qed "mem_chain_psubset_empty";
paulson@5979
   425
paulson@5979
   426
Goal "!!(c :: 'a set set set). \
paulson@5979
   427
\            [| c: chain (superfrechet S);\
paulson@5979
   428
\               c ~= {} \
paulson@5979
   429
\            |]\
paulson@5979
   430
\            ==> Union(c) ~= {}";
paulson@5979
   431
by (dtac mem_chain_psubset_empty 1);
paulson@5979
   432
by (Step_tac 1);
paulson@5979
   433
by (dtac bspec 1 THEN assume_tac 1);
paulson@5979
   434
by (auto_tac (claset() addDs [Union_upper,bspec],
paulson@5979
   435
    simpset() addsimps [psubset_def]));
paulson@5979
   436
qed "chain_Un_not_empty";
paulson@5979
   437
paulson@5979
   438
Goalw [is_Filter_def,Filter_def,chain_def,thm "superfrechet_def"] 
paulson@5979
   439
           "!!(c :: 'a set set set). \
paulson@5979
   440
\           c : chain (superfrechet S)  \
paulson@5979
   441
\           ==> {} ~: Union(c)";
paulson@5979
   442
by (Blast_tac 1);
paulson@5979
   443
qed "Filter_empty_not_mem_Un";
paulson@5979
   444
paulson@5979
   445
Goal "c: chain (superfrechet S) \
paulson@5979
   446
\         ==> ALL u : Union(c). ALL v: Union(c). u Int v : Union(c)";
paulson@5979
   447
by (Step_tac 1);
paulson@5979
   448
by (forw_inst_tac [("x","X"),("y","Xa")] chainD 1);
paulson@5979
   449
by (REPEAT(assume_tac 1));
paulson@5979
   450
by (dtac chainD2 1);
paulson@5979
   451
by (etac disjE 1);
paulson@5979
   452
by (res_inst_tac [("X","Xa")] UnionI 1 THEN assume_tac 1);
paulson@5979
   453
by (dres_inst_tac [("A","X")] subsetD 1 THEN assume_tac 1);
paulson@5979
   454
by (dres_inst_tac [("c","Xa")] subsetD 1 THEN assume_tac 1);
paulson@5979
   455
by (res_inst_tac [("X","X")] UnionI 2 THEN assume_tac 2);
paulson@5979
   456
by (dres_inst_tac [("A","Xa")] subsetD 2 THEN assume_tac 2);
paulson@5979
   457
by (dres_inst_tac [("c","X")] subsetD 2 THEN assume_tac 2);
paulson@5979
   458
by (auto_tac (claset() addIs [mem_FiltersetD1], 
paulson@5979
   459
     simpset() addsimps [thm "superfrechet_def"]));
paulson@5979
   460
qed "Filter_Un_Int";
paulson@5979
   461
paulson@5979
   462
Goal "c: chain (superfrechet S) \
paulson@5979
   463
\         ==> ALL u v. u: Union(c) & \
paulson@5979
   464
\                 (u :: 'a set) <= v & v <= S --> v: Union(c)";
paulson@5979
   465
by (Step_tac 1);
paulson@5979
   466
by (dtac chainD2 1);
paulson@5979
   467
by (dtac subsetD 1 THEN assume_tac 1);
paulson@5979
   468
by (rtac UnionI 1 THEN assume_tac 1);
paulson@5979
   469
by (auto_tac (claset() addIs [mem_FiltersetD2], 
paulson@5979
   470
     simpset() addsimps [thm "superfrechet_def"]));
paulson@5979
   471
qed "Filter_Un_subset";
paulson@5979
   472
paulson@5979
   473
Goalw [chain_def,thm "superfrechet_def"]
paulson@5979
   474
      "!!(c :: 'a set set set). \
paulson@5979
   475
\            [| c: chain (superfrechet S);\
paulson@5979
   476
\               x: c \
paulson@5979
   477
\            |] ==> x : Filter S";
paulson@5979
   478
by (Blast_tac 1);
paulson@5979
   479
qed "lemma_mem_chain_Filter";
paulson@5979
   480
paulson@5979
   481
Goalw [chain_def,thm "superfrechet_def"]
paulson@5979
   482
     "!!(c :: 'a set set set). \
paulson@5979
   483
\            [| c: chain (superfrechet S);\
paulson@5979
   484
\               x: c \
paulson@5979
   485
\            |] ==> frechet S <= x";
paulson@5979
   486
by (Blast_tac 1);
paulson@5979
   487
qed "lemma_mem_chain_frechet_subset";
paulson@5979
   488
paulson@5979
   489
Goal "!!(c :: 'a set set set). \
paulson@5979
   490
\         [| c ~= {}; \
paulson@5979
   491
\            c : chain (superfrechet (UNIV :: 'a set))\
paulson@5979
   492
\         |] ==> Union c : superfrechet (UNIV)";
paulson@5979
   493
by (simp_tac (simpset() addsimps 
paulson@5979
   494
    [thm "superfrechet_def",thm "frechet_def"]) 1);
paulson@5979
   495
by (Step_tac 1);
paulson@5979
   496
by (rtac mem_FiltersetI2 1);
paulson@5979
   497
by (etac chain_Un_subset_Pow 1);
paulson@5979
   498
by (rtac UnionI 1 THEN assume_tac 1);
paulson@5979
   499
by (etac (lemma_mem_chain_Filter RS mem_FiltersetD4) 1 THEN assume_tac 1);
paulson@5979
   500
by (etac chain_Un_not_empty 1);
paulson@5979
   501
by (etac Filter_empty_not_mem_Un 2);
paulson@5979
   502
by (etac Filter_Un_Int 2);
paulson@5979
   503
by (etac Filter_Un_subset 2);
paulson@5979
   504
by (subgoal_tac "xa : frechet (UNIV)" 2);
paulson@5979
   505
by (rtac UnionI 2 THEN assume_tac 2);
paulson@5979
   506
by (rtac (lemma_mem_chain_frechet_subset RS subsetD) 2);
paulson@5979
   507
by (auto_tac (claset(),simpset() addsimps [thm "frechet_def"]));
paulson@5979
   508
qed "Un_chain_mem_cofinite_Filter_set";
paulson@5979
   509
paulson@5979
   510
Goal "EX U: superfrechet (UNIV). \
paulson@5979
   511
\               ALL G: superfrechet (UNIV). U <= G --> U = G";
paulson@5979
   512
by (rtac Zorn_Lemma2 1);
paulson@5979
   513
by (cut_facts_tac [thm "not_finite_UNIV" RS cofinite_Filter] 1);
paulson@5979
   514
by (Step_tac 1);
paulson@5979
   515
by (res_inst_tac [("Q","c={}")] (excluded_middle RS disjE) 1);
paulson@5979
   516
by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1);
paulson@5979
   517
by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1));
paulson@5979
   518
by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1);
paulson@5979
   519
by (auto_tac (claset(),simpset() addsimps 
paulson@5979
   520
        [thm "superfrechet_def", thm "frechet_def"]));
paulson@5979
   521
qed "max_cofinite_Filter_Ex";
paulson@5979
   522
paulson@5979
   523
Goal "EX U: superfrechet UNIV. (\
paulson@5979
   524
\               ALL G: superfrechet UNIV. U <= G --> U = G) \ 
paulson@5979
   525
\                             & (ALL x: U. ~finite x)";
paulson@5979
   526
by (cut_facts_tac [thm "not_finite_UNIV" RS 
paulson@5979
   527
         (export max_cofinite_Filter_Ex)] 1);
paulson@5979
   528
by (Step_tac 1);
paulson@5979
   529
by (res_inst_tac [("x","U")] bexI 1);
paulson@5979
   530
by (auto_tac (claset(),simpset() addsimps 
paulson@5979
   531
        [thm "superfrechet_def", thm "frechet_def"]));
paulson@5979
   532
by (dres_inst_tac [("c","- x")] subsetD 1);
paulson@5979
   533
by (Asm_simp_tac 1);
paulson@5979
   534
by (forw_inst_tac [("A","x"),("B","- x")] mem_FiltersetD1 1);
paulson@5979
   535
by (dtac Filter_empty_not_mem 3);
paulson@5979
   536
by (ALLGOALS(Asm_full_simp_tac ));
paulson@5979
   537
qed "max_cofinite_Freefilter_Ex";
paulson@5979
   538
paulson@5979
   539
(*--------------------------------------------------------------------------------
paulson@5979
   540
               There exists a free ultrafilter on any infinite set
paulson@5979
   541
 --------------------------------------------------------------------------------*)
paulson@5979
   542
paulson@5979
   543
Goalw [FreeUltrafilter_def] "EX U. U: FreeUltrafilter (UNIV :: 'a set)";
paulson@5979
   544
by (cut_facts_tac [thm "not_finite_UNIV" RS (export max_cofinite_Freefilter_Ex)] 1);
paulson@5979
   545
by (asm_full_simp_tac (simpset() addsimps 
paulson@5979
   546
    [thm "superfrechet_def", Ultrafilter_iff, thm "frechet_def"]) 1);
paulson@5979
   547
by (Step_tac 1);
paulson@5979
   548
by (res_inst_tac [("x","U")] exI 1);
paulson@5979
   549
by (Step_tac 1);
paulson@5979
   550
by (Blast_tac 1);
paulson@5979
   551
qed "FreeUltrafilter_ex";
paulson@5979
   552
paulson@5979
   553
val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
paulson@5979
   554
paulson@5979
   555
Close_locale();
paulson@5979
   556
paulson@5979
   557