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