src/ZF/Zorn.thy
author paulson
Thu May 23 17:05:21 2002 +0200 (2002-05-23)
changeset 13175 81082cfa5618
parent 13134 bf37a3049251
child 13269 3ba9be497c33
permissions -rw-r--r--
new definition of "apply" and new simprule "beta_if"
clasohm@1478
     1
(*  Title:      ZF/Zorn.thy
lcp@516
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     4
    Copyright   1994  University of Cambridge
lcp@516
     5
lcp@516
     6
Based upon the article
lcp@516
     7
    Abrial & Laffitte, 
lcp@516
     8
    Towards the Mechanization of the Proofs of Some 
lcp@516
     9
    Classical Theorems of Set Theory. 
lcp@516
    10
lcp@516
    11
Union_in_Pow is proved in ZF.ML
lcp@516
    12
*)
lcp@516
    13
paulson@13134
    14
theory Zorn = OrderArith + AC + Inductive:
lcp@516
    15
paulson@13134
    16
constdefs
paulson@13134
    17
  Subset_rel :: "i=>i"
paulson@13134
    18
   "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
paulson@13134
    19
paulson@13134
    20
  chain      :: "i=>i"
paulson@13134
    21
   "chain(A)      == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}"
lcp@516
    22
paulson@13134
    23
  maxchain   :: "i=>i"
paulson@13134
    24
   "maxchain(A)   == {c: chain(A). super(A,c)=0}"
paulson@13134
    25
  
paulson@13134
    26
  super      :: "[i,i]=>i"
paulson@13134
    27
   "super(A,c)    == {d: chain(A). c<=d & c~=d}"
lcp@485
    28
lcp@516
    29
paulson@13134
    30
constdefs
paulson@13134
    31
  increasing :: "i=>i"
paulson@13134
    32
    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
lcp@516
    33
lcp@516
    34
(** We could make the inductive definition conditional on next: increasing(S)
lcp@516
    35
    but instead we make this a side-condition of an introduction rule.  Thus
lcp@516
    36
    the induction rule lets us assume that condition!  Many inductive proofs
lcp@516
    37
    are therefore unconditional.
lcp@516
    38
**)
lcp@516
    39
consts
paulson@13134
    40
  "TFin" :: "[i,i]=>i"
lcp@516
    41
lcp@516
    42
inductive
lcp@516
    43
  domains       "TFin(S,next)" <= "Pow(S)"
paulson@13134
    44
  intros
paulson@13134
    45
    nextI:       "[| x : TFin(S,next);  next: increasing(S) |]
paulson@13134
    46
                  ==> next`x : TFin(S,next)"
lcp@516
    47
paulson@13134
    48
    Pow_UnionI: "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"
lcp@516
    49
paulson@6053
    50
  monos         Pow_mono
paulson@6053
    51
  con_defs      increasing_def
paulson@13134
    52
  type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow
paulson@13134
    53
paulson@13134
    54
paulson@13134
    55
(*** Section 1.  Mathematical Preamble ***)
paulson@13134
    56
paulson@13134
    57
lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
paulson@13134
    58
apply blast
paulson@13134
    59
done
paulson@13134
    60
paulson@13134
    61
lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
paulson@13134
    62
apply blast
paulson@13134
    63
done
paulson@13134
    64
paulson@13134
    65
paulson@13134
    66
(*** Section 2.  The Transfinite Construction ***)
paulson@13134
    67
paulson@13134
    68
lemma increasingD1: "f: increasing(A) ==> f: Pow(A)->Pow(A)"
paulson@13134
    69
apply (unfold increasing_def)
paulson@13134
    70
apply (erule CollectD1)
paulson@13134
    71
done
paulson@13134
    72
paulson@13134
    73
lemma increasingD2: "[| f: increasing(A); x<=A |] ==> x <= f`x"
paulson@13134
    74
apply (unfold increasing_def)
paulson@13134
    75
apply (blast intro: elim:); 
paulson@13134
    76
done
paulson@13134
    77
paulson@13134
    78
lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
paulson@13134
    79
paulson@13134
    80
lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard]
paulson@13134
    81
paulson@13134
    82
paulson@13134
    83
(** Structural induction on TFin(S,next) **)
paulson@13134
    84
paulson@13134
    85
lemma TFin_induct:
paulson@13134
    86
  "[| n: TFin(S,next);   
paulson@13134
    87
      !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x);  
paulson@13134
    88
      !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y))  
paulson@13134
    89
   |] ==> P(n)"
paulson@13134
    90
apply (erule TFin.induct)
paulson@13134
    91
apply blast+
paulson@13134
    92
done
paulson@13134
    93
paulson@13134
    94
paulson@13134
    95
(*** Section 3.  Some Properties of the Transfinite Construction ***)
paulson@13134
    96
paulson@13134
    97
lemmas increasing_trans = subset_trans [OF _ increasingD2, 
paulson@13134
    98
                                        OF _ _ TFin_is_subset]
paulson@13134
    99
paulson@13134
   100
(*Lemma 1 of section 3.1*)
paulson@13134
   101
lemma TFin_linear_lemma1:
paulson@13134
   102
     "[| n: TFin(S,next);  m: TFin(S,next);   
paulson@13134
   103
         ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m |] 
paulson@13134
   104
      ==> n<=m | next`m<=n"
paulson@13134
   105
apply (erule TFin_induct)
paulson@13134
   106
apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
paulson@13134
   107
(*downgrade subsetI from intro! to intro*)
paulson@13134
   108
apply (blast dest: increasing_trans)
paulson@13134
   109
done
paulson@13134
   110
paulson@13134
   111
(*Lemma 2 of section 3.2.  Interesting in its own right!
paulson@13134
   112
  Requires next: increasing(S) in the second induction step. *)
paulson@13134
   113
lemma TFin_linear_lemma2:
paulson@13134
   114
    "[| m: TFin(S,next);  next: increasing(S) |] 
paulson@13134
   115
     ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m"
paulson@13134
   116
apply (erule TFin_induct)
paulson@13134
   117
apply (rule impI [THEN ballI])
paulson@13134
   118
(*case split using TFin_linear_lemma1*)
paulson@13134
   119
apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
paulson@13134
   120
       assumption+)
paulson@13134
   121
apply (blast del: subsetI
paulson@13134
   122
	     intro: increasing_trans subsetI)
paulson@13134
   123
apply (blast intro: elim:); 
paulson@13134
   124
(*second induction step*)
paulson@13134
   125
apply (rule impI [THEN ballI])
paulson@13134
   126
apply (rule Union_lemma0 [THEN disjE])
paulson@13134
   127
apply (erule_tac [3] disjI2)
paulson@13134
   128
prefer 2 apply (blast intro: elim:); 
paulson@13134
   129
apply (rule ballI)
paulson@13134
   130
apply (drule bspec, assumption) 
paulson@13134
   131
apply (drule subsetD, assumption) 
paulson@13134
   132
apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
paulson@13134
   133
       assumption+)
paulson@13134
   134
apply (blast intro: elim:); 
paulson@13134
   135
apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
paulson@13134
   136
apply (blast dest: TFin_is_subset)+
paulson@13134
   137
done
paulson@13134
   138
paulson@13134
   139
(*a more convenient form for Lemma 2*)
paulson@13134
   140
lemma TFin_subsetD:
paulson@13134
   141
     "[| n<=m;  m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |]  
paulson@13134
   142
      ==> n=m | next`n<=m"
paulson@13134
   143
by (blast dest: TFin_linear_lemma2 [rule_format]) 
paulson@13134
   144
paulson@13134
   145
(*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
paulson@13134
   146
lemma TFin_subset_linear:
paulson@13134
   147
     "[| m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |]  
paulson@13134
   148
      ==> n<=m | m<=n"
paulson@13134
   149
apply (rule disjE) 
paulson@13134
   150
apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
paulson@13134
   151
apply (assumption+, erule disjI2)
paulson@13134
   152
apply (blast del: subsetI 
paulson@13134
   153
             intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)
paulson@13134
   154
done
paulson@13134
   155
paulson@13134
   156
paulson@13134
   157
(*Lemma 3 of section 3.3*)
paulson@13134
   158
lemma equal_next_upper:
paulson@13134
   159
     "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m"
paulson@13134
   160
apply (erule TFin_induct)
paulson@13134
   161
apply (drule TFin_subsetD)
paulson@13134
   162
apply (assumption+)
paulson@13134
   163
apply (force ); 
paulson@13134
   164
apply (blast)
paulson@13134
   165
done
paulson@13134
   166
paulson@13134
   167
(*Property 3.3 of section 3.3*)
paulson@13134
   168
lemma equal_next_Union: "[| m: TFin(S,next);  next: increasing(S) |]   
paulson@13134
   169
      ==> m = next`m <-> m = Union(TFin(S,next))"
paulson@13134
   170
apply (rule iffI)
paulson@13134
   171
apply (rule Union_upper [THEN equalityI])
paulson@13134
   172
apply (rule_tac [2] equal_next_upper [THEN Union_least])
paulson@13134
   173
apply (assumption+)
paulson@13134
   174
apply (erule ssubst)
paulson@13134
   175
apply (rule increasingD2 [THEN equalityI] , assumption)
paulson@13134
   176
apply (blast del: subsetI
paulson@13134
   177
	     intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
paulson@13134
   178
done
paulson@13134
   179
paulson@13134
   180
paulson@13134
   181
(*** Section 4.  Hausdorff's Theorem: every set contains a maximal chain ***)
paulson@13134
   182
(*** NB: We assume the partial ordering is <=, the subset relation! **)
paulson@13134
   183
paulson@13134
   184
(** Defining the "next" operation for Hausdorff's Theorem **)
paulson@13134
   185
paulson@13134
   186
lemma chain_subset_Pow: "chain(A) <= Pow(A)"
paulson@13134
   187
apply (unfold chain_def)
paulson@13134
   188
apply (rule Collect_subset)
paulson@13134
   189
done
paulson@13134
   190
paulson@13134
   191
lemma super_subset_chain: "super(A,c) <= chain(A)"
paulson@13134
   192
apply (unfold super_def)
paulson@13134
   193
apply (rule Collect_subset)
paulson@13134
   194
done
paulson@13134
   195
paulson@13134
   196
lemma maxchain_subset_chain: "maxchain(A) <= chain(A)"
paulson@13134
   197
apply (unfold maxchain_def)
paulson@13134
   198
apply (rule Collect_subset)
paulson@13134
   199
done
paulson@13134
   200
paulson@13134
   201
lemma choice_super: "[| ch : (PROD X:Pow(chain(S)) - {0}. X);   
paulson@13134
   202
         X : chain(S);  X ~: maxchain(S) |]      
paulson@13134
   203
      ==> ch ` super(S,X) : super(S,X)"
paulson@13134
   204
apply (erule apply_type)
paulson@13134
   205
apply (unfold super_def maxchain_def)
paulson@13134
   206
apply blast
paulson@13134
   207
done
paulson@13134
   208
paulson@13134
   209
lemma choice_not_equals:
paulson@13134
   210
     "[| ch : (PROD X:Pow(chain(S)) - {0}. X);       
paulson@13134
   211
         X : chain(S);  X ~: maxchain(S) |]      
paulson@13134
   212
      ==> ch ` super(S,X) ~= X"
paulson@13134
   213
apply (rule notI)
paulson@13134
   214
apply (drule choice_super)
paulson@13134
   215
apply assumption
paulson@13134
   216
apply assumption
paulson@13134
   217
apply (simp add: super_def)
paulson@13134
   218
done
paulson@13134
   219
paulson@13134
   220
(*This justifies Definition 4.4*)
paulson@13134
   221
lemma Hausdorff_next_exists:
paulson@13134
   222
     "ch: (PROD X: Pow(chain(S))-{0}. X) ==>         
paulson@13134
   223
      EX next: increasing(S). ALL X: Pow(S).        
paulson@13134
   224
                   next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)"
paulson@13175
   225
apply (rule_tac x="\<lambda>X\<in>Pow(S). 
paulson@13175
   226
                   if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X" 
paulson@13175
   227
       in bexI)
paulson@13175
   228
apply (force ); 
paulson@13134
   229
apply (unfold increasing_def)
paulson@13134
   230
apply (rule CollectI)
paulson@13134
   231
apply (rule lam_type)
paulson@13134
   232
apply (simp (no_asm_simp))
paulson@13134
   233
apply (blast dest: super_subset_chain [THEN subsetD] chain_subset_Pow [THEN subsetD] choice_super)
paulson@13134
   234
(*Now, verify that it increases*)
paulson@13134
   235
apply (simp (no_asm_simp) add: Pow_iff subset_refl)
paulson@13134
   236
apply safe
paulson@13134
   237
apply (drule choice_super)
paulson@13134
   238
apply (assumption+)
paulson@13175
   239
apply (simp add: super_def)
paulson@13134
   240
apply blast
paulson@13134
   241
done
paulson@13134
   242
paulson@13134
   243
(*Lemma 4*)
paulson@13134
   244
lemma TFin_chain_lemma4:
paulson@13134
   245
     "[| c: TFin(S,next);                               
paulson@13134
   246
         ch: (PROD X: Pow(chain(S))-{0}. X);            
paulson@13134
   247
         next: increasing(S);                           
paulson@13134
   248
         ALL X: Pow(S). next`X =        
paulson@13134
   249
                          if(X: chain(S)-maxchain(S), ch`super(S,X), X) |] 
paulson@13134
   250
     ==> c: chain(S)"
paulson@13134
   251
apply (erule TFin_induct)
paulson@13134
   252
apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] 
paulson@13134
   253
            choice_super [THEN super_subset_chain [THEN subsetD]])
paulson@13134
   254
apply (unfold chain_def)
paulson@13134
   255
apply (rule CollectI , blast)
paulson@13134
   256
apply safe
paulson@13134
   257
apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE])
paulson@13134
   258
apply fast+ (*Blast_tac's slow*)
paulson@13134
   259
done
paulson@13134
   260
paulson@13134
   261
lemma Hausdorff: "EX c. c : maxchain(S)"
paulson@13134
   262
apply (rule AC_Pi_Pow [THEN exE])
paulson@13134
   263
apply (rule Hausdorff_next_exists [THEN bexE])
paulson@13134
   264
apply assumption
paulson@13134
   265
apply (rename_tac ch "next")
paulson@13134
   266
apply (subgoal_tac "Union (TFin (S,next)) : chain (S) ")
paulson@13134
   267
prefer 2
paulson@13134
   268
 apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
paulson@13134
   269
apply (rule_tac x = "Union (TFin (S,next))" in exI)
paulson@13134
   270
apply (rule classical)
paulson@13134
   271
apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))")
paulson@13134
   272
apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
paulson@13134
   273
apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
paulson@13134
   274
prefer 2 apply (assumption)
paulson@13134
   275
apply (rule_tac [2] refl)
paulson@13134
   276
apply (simp add: subset_refl [THEN TFin_UnionI, 
paulson@13134
   277
                              THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
paulson@13134
   278
apply (erule choice_not_equals [THEN notE])
paulson@13134
   279
apply (assumption+)
paulson@13134
   280
done
paulson@13134
   281
paulson@13134
   282
paulson@13134
   283
(*** Section 5.  Zorn's Lemma: if all chains in S have upper bounds in S 
paulson@13134
   284
                               then S contains a maximal element ***)
paulson@13134
   285
paulson@13134
   286
(*Used in the proof of Zorn's Lemma*)
paulson@13134
   287
lemma chain_extend: 
paulson@13134
   288
    "[| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"
paulson@13134
   289
apply (unfold chain_def)
paulson@13134
   290
apply blast
paulson@13134
   291
done
paulson@13134
   292
paulson@13134
   293
lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"
paulson@13134
   294
apply (rule Hausdorff [THEN exE])
paulson@13134
   295
apply (simp add: maxchain_def)
paulson@13134
   296
apply (rename_tac c)
paulson@13134
   297
apply (rule_tac x = "Union (c)" in bexI)
paulson@13134
   298
prefer 2 apply (blast)
paulson@13134
   299
apply safe
paulson@13134
   300
apply (rename_tac z)
paulson@13134
   301
apply (rule classical)
paulson@13134
   302
apply (subgoal_tac "cons (z,c) : super (S,c) ")
paulson@13134
   303
apply (blast elim: equalityE)
paulson@13134
   304
apply (unfold super_def)
paulson@13134
   305
apply safe
paulson@13134
   306
apply (fast elim: chain_extend)
paulson@13134
   307
apply (fast elim: equalityE)
paulson@13134
   308
done
paulson@13134
   309
paulson@13134
   310
paulson@13134
   311
(*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
paulson@13134
   312
paulson@13134
   313
(*Lemma 5*)
paulson@13134
   314
lemma TFin_well_lemma5:
paulson@13134
   315
     "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z |]   
paulson@13134
   316
      ==> ALL m:Z. n<=m"
paulson@13134
   317
apply (erule TFin_induct)
paulson@13134
   318
prefer 2 apply (blast) (*second induction step is easy*)
paulson@13134
   319
apply (rule ballI)
paulson@13134
   320
apply (rule bspec [THEN TFin_subsetD, THEN disjE])
paulson@13134
   321
apply (auto ); 
paulson@13134
   322
apply (subgoal_tac "m = Inter (Z) ")
paulson@13134
   323
apply blast+
paulson@13134
   324
done
paulson@13134
   325
paulson@13134
   326
(*Well-ordering of TFin(S,next)*)
paulson@13134
   327
lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next);  z:Z |] ==> Inter(Z) : Z"
paulson@13134
   328
apply (rule classical)
paulson@13134
   329
apply (subgoal_tac "Z = {Union (TFin (S,next))}")
paulson@13134
   330
apply (simp (no_asm_simp) add: Inter_singleton)
paulson@13134
   331
apply (erule equal_singleton)
paulson@13134
   332
apply (rule Union_upper [THEN equalityI])
paulson@13134
   333
apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec])
paulson@13134
   334
apply (blast intro: elim:)+
paulson@13134
   335
done
paulson@13134
   336
paulson@13134
   337
(*This theorem just packages the previous result*)
paulson@13134
   338
lemma well_ord_TFin:
paulson@13134
   339
     "next: increasing(S) ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
paulson@13134
   340
apply (rule well_ordI)
paulson@13134
   341
apply (unfold Subset_rel_def linear_def)
paulson@13134
   342
(*Prove the well-foundedness goal*)
paulson@13134
   343
apply (rule wf_onI)
paulson@13134
   344
apply (frule well_ord_TFin_lemma , assumption)
paulson@13134
   345
apply (drule_tac x = "Inter (Z) " in bspec , assumption)
paulson@13134
   346
apply blast
paulson@13134
   347
(*Now prove the linearity goal*)
paulson@13134
   348
apply (intro ballI)
paulson@13134
   349
apply (case_tac "x=y")
paulson@13134
   350
 apply (blast)
paulson@13134
   351
(*The x~=y case remains*)
paulson@13134
   352
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
paulson@13134
   353
       assumption+)
paulson@13134
   354
apply (blast intro: elim:)+
paulson@13134
   355
done
paulson@13134
   356
paulson@13134
   357
(** Defining the "next" operation for Zermelo's Theorem **)
paulson@13134
   358
paulson@13134
   359
lemma choice_Diff:
paulson@13134
   360
     "[| ch \<in> (\<Pi>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
paulson@13134
   361
apply (erule apply_type)
paulson@13134
   362
apply (blast elim!: equalityE)
paulson@13134
   363
done
paulson@13134
   364
paulson@13134
   365
(*This justifies Definition 6.1*)
paulson@13134
   366
lemma Zermelo_next_exists:
paulson@13134
   367
     "ch: (PROD X: Pow(S)-{0}. X) ==>                
paulson@13134
   368
           EX next: increasing(S). ALL X: Pow(S).        
paulson@13175
   369
                      next`X = (if X=S then S else cons(ch`(S-X), X))"
paulson@13175
   370
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
paulson@13175
   371
       in bexI)
paulson@13175
   372
apply (force );  
paulson@13134
   373
apply (unfold increasing_def)
paulson@13134
   374
apply (rule CollectI)
paulson@13134
   375
apply (rule lam_type)
paulson@13134
   376
(*Type checking is surprisingly hard!*)
paulson@13134
   377
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
paulson@13134
   378
apply (blast intro!: choice_Diff [THEN DiffD1])
paulson@13134
   379
(*Verify that it increases*)
paulson@13134
   380
apply (intro allI impI) 
paulson@13134
   381
apply (simp add: Pow_iff subset_consI subset_refl)
paulson@13134
   382
done
paulson@13134
   383
paulson@13134
   384
paulson@13134
   385
(*The construction of the injection*)
paulson@13134
   386
lemma choice_imp_injection:
paulson@13134
   387
     "[| ch: (PROD X: Pow(S)-{0}. X);                  
paulson@13134
   388
         next: increasing(S);                          
paulson@13134
   389
         ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]  
paulson@13134
   390
      ==> (lam x:S. Union({y: TFin(S,next). x~: y}))        
paulson@13134
   391
               : inj(S, TFin(S,next) - {S})"
paulson@13134
   392
apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
paulson@13134
   393
apply (rule DiffI)
paulson@13134
   394
apply (rule Collect_subset [THEN TFin_UnionI])
paulson@13134
   395
apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
paulson@13134
   396
apply (subgoal_tac "x ~: Union ({y: TFin (S,next) . x~: y}) ")
paulson@13134
   397
prefer 2 apply (blast elim: equalityE)
paulson@13134
   398
apply (subgoal_tac "Union ({y: TFin (S,next) . x~: y}) ~= S")
paulson@13134
   399
prefer 2 apply (blast elim: equalityE)
paulson@13134
   400
(*For proving x : next`Union(...)
paulson@13134
   401
  Abrial & Laffitte's justification appears to be faulty.*)
paulson@13134
   402
apply (subgoal_tac "~ next ` Union ({y: TFin (S,next) . x~: y}) <= Union ({y: TFin (S,next) . x~: y}) ")
paulson@13134
   403
prefer 2
paulson@13134
   404
apply (simp del: Union_iff 
paulson@13134
   405
            add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset] 
paulson@13134
   406
            Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
paulson@13134
   407
apply (subgoal_tac "x : next ` Union ({y: TFin (S,next) . x~: y}) ")
paulson@13134
   408
prefer 2
paulson@13134
   409
apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
paulson@13134
   410
(*End of the lemmas!*)
paulson@13134
   411
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
paulson@13134
   412
done
paulson@13134
   413
paulson@13134
   414
(*The wellordering theorem*)
paulson@13134
   415
lemma AC_well_ord: "EX r. well_ord(S,r)"
paulson@13134
   416
apply (rule AC_Pi_Pow [THEN exE])
paulson@13134
   417
apply (rule Zermelo_next_exists [THEN bexE])
paulson@13134
   418
apply assumption
paulson@13134
   419
apply (rule exI)
paulson@13134
   420
apply (rule well_ord_rvimage)
paulson@13134
   421
apply (erule_tac [2] well_ord_TFin)
paulson@13134
   422
apply (rule choice_imp_injection [THEN inj_weaken_type])
paulson@13134
   423
apply (blast intro: elim:)+
paulson@13134
   424
done
lcp@516
   425
  
lcp@516
   426
end