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