src/ZF/Zorn.thy
author ballarin
Tue Jul 29 17:50:48 2008 +0200 (2008-07-29)
changeset 27704 5b1585b48952
parent 26056 6a0801279f4c
child 32960 69916a850301
permissions -rw-r--r--
Zorn's Lemma for partial orders.
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
krauss@26056
    10
theory Zorn imports OrderArith AC Inductive_ZF begin
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
wenzelm@24893
    15
definition
wenzelm@24893
    16
  Subset_rel :: "i=>i"  where
paulson@13558
    17
   "Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}"
paulson@13134
    18
wenzelm@24893
    19
definition
wenzelm@24893
    20
  chain      :: "i=>i"  where
paulson@13558
    21
   "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
lcp@516
    22
wenzelm@24893
    23
definition
wenzelm@24893
    24
  super      :: "[i,i]=>i"  where
wenzelm@14653
    25
   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
wenzelm@14653
    26
wenzelm@24893
    27
definition
wenzelm@24893
    28
  maxchain   :: "i=>i"  where
paulson@13558
    29
   "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
paulson@13558
    30
wenzelm@24893
    31
definition
wenzelm@24893
    32
  increasing :: "i=>i"  where
paulson@13558
    33
    "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A --> x<=f`x}"
lcp@516
    34
paulson@13356
    35
paulson@13558
    36
text{*Lemma for the inductive definition below*}
paulson@13558
    37
lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> Union(Y) \<in> Pow(A)"
paulson@13356
    38
by blast
paulson@13356
    39
paulson@13356
    40
paulson@13558
    41
text{*We could make the inductive definition conditional on
paulson@13356
    42
    @{term "next \<in> increasing(S)"}
lcp@516
    43
    but instead we make this a side-condition of an introduction rule.  Thus
lcp@516
    44
    the induction rule lets us assume that condition!  Many inductive proofs
paulson@13356
    45
    are therefore unconditional.*}
lcp@516
    46
consts
paulson@13134
    47
  "TFin" :: "[i,i]=>i"
lcp@516
    48
lcp@516
    49
inductive
lcp@516
    50
  domains       "TFin(S,next)" <= "Pow(S)"
paulson@13134
    51
  intros
paulson@13558
    52
    nextI:       "[| x \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson@13558
    53
                  ==> next`x \<in> TFin(S,next)"
lcp@516
    54
paulson@13558
    55
    Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> Union(Y) \<in> TFin(S,next)"
lcp@516
    56
paulson@6053
    57
  monos         Pow_mono
paulson@6053
    58
  con_defs      increasing_def
paulson@13134
    59
  type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow
paulson@13134
    60
paulson@13134
    61
paulson@13356
    62
subsection{*Mathematical Preamble *}
paulson@13134
    63
paulson@13558
    64
lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
paulson@13269
    65
by blast
paulson@13134
    66
paulson@13356
    67
lemma Inter_lemma0:
paulson@13558
    68
     "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A <= Inter(C) | Inter(C) <= B"
paulson@13269
    69
by blast
paulson@13134
    70
paulson@13134
    71
paulson@13356
    72
subsection{*The Transfinite Construction *}
paulson@13134
    73
paulson@13558
    74
lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)"
paulson@13134
    75
apply (unfold increasing_def)
paulson@13134
    76
apply (erule CollectD1)
paulson@13134
    77
done
paulson@13134
    78
paulson@13558
    79
lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x <= f`x"
paulson@13269
    80
by (unfold increasing_def, blast)
paulson@13134
    81
paulson@13134
    82
lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
paulson@13134
    83
paulson@13134
    84
lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard]
paulson@13134
    85
paulson@13134
    86
paulson@13558
    87
text{*Structural induction on @{term "TFin(S,next)"} *}
paulson@13134
    88
lemma TFin_induct:
paulson@13558
    89
  "[| n \<in> TFin(S,next);
paulson@13558
    90
      !!x. [| x \<in> TFin(S,next);  P(x);  next \<in> increasing(S) |] ==> P(next`x);
paulson@13558
    91
      !!Y. [| Y <= TFin(S,next);  \<forall>y\<in>Y. P(y) |] ==> P(Union(Y))
paulson@13134
    92
   |] ==> P(n)"
paulson@13356
    93
by (erule TFin.induct, blast+)
paulson@13134
    94
paulson@13134
    95
paulson@13356
    96
subsection{*Some Properties of the Transfinite Construction *}
paulson@13134
    97
paulson@13558
    98
lemmas increasing_trans = subset_trans [OF _ increasingD2,
paulson@13134
    99
                                        OF _ _ TFin_is_subset]
paulson@13134
   100
paulson@13558
   101
text{*Lemma 1 of section 3.1*}
paulson@13134
   102
lemma TFin_linear_lemma1:
paulson@13558
   103
     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);
paulson@13558
   104
         \<forall>x \<in> TFin(S,next) . x<=m --> x=m | next`x<=m |]
paulson@13134
   105
      ==> n<=m | next`m<=n"
paulson@13134
   106
apply (erule TFin_induct)
paulson@13134
   107
apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
paulson@13134
   108
(*downgrade subsetI from intro! to intro*)
paulson@13134
   109
apply (blast dest: increasing_trans)
paulson@13134
   110
done
paulson@13134
   111
paulson@13558
   112
text{*Lemma 2 of section 3.2.  Interesting in its own right!
paulson@13558
   113
  Requires @{term "next \<in> increasing(S)"} in the second induction step.*}
paulson@13134
   114
lemma TFin_linear_lemma2:
paulson@13558
   115
    "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson@13558
   116
     ==> \<forall>n \<in> TFin(S,next). n<=m --> n=m | next`n <= m"
paulson@13134
   117
apply (erule TFin_induct)
paulson@13134
   118
apply (rule impI [THEN ballI])
paulson@13558
   119
txt{*case split using @{text TFin_linear_lemma1}*}
paulson@13784
   120
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
paulson@13134
   121
       assumption+)
paulson@13134
   122
apply (blast del: subsetI
paulson@13558
   123
	     intro: increasing_trans subsetI, blast)
paulson@13558
   124
txt{*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@13558
   128
prefer 2 apply blast
paulson@13134
   129
apply (rule ballI)
paulson@13558
   130
apply (drule bspec, assumption)
paulson@13558
   131
apply (drule subsetD, assumption)
paulson@13784
   132
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
paulson@13558
   133
       assumption+, blast)
paulson@13134
   134
apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
paulson@13134
   135
apply (blast dest: TFin_is_subset)+
paulson@13134
   136
done
paulson@13134
   137
paulson@13558
   138
text{*a more convenient form for Lemma 2*}
paulson@13134
   139
lemma TFin_subsetD:
paulson@13558
   140
     "[| n<=m;  m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson@13558
   141
      ==> n=m | next`n <= m"
paulson@13558
   142
by (blast dest: TFin_linear_lemma2 [rule_format])
paulson@13134
   143
paulson@13558
   144
text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
paulson@13134
   145
lemma TFin_subset_linear:
paulson@13558
   146
     "[| m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson@13558
   147
      ==> n <= m | m<=n"
paulson@13558
   148
apply (rule disjE)
paulson@13134
   149
apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
paulson@13134
   150
apply (assumption+, erule disjI2)
paulson@13558
   151
apply (blast del: subsetI
paulson@13134
   152
             intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)
paulson@13134
   153
done
paulson@13134
   154
paulson@13134
   155
paulson@13558
   156
text{*Lemma 3 of section 3.3*}
paulson@13134
   157
lemma equal_next_upper:
paulson@13558
   158
     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n <= m"
paulson@13134
   159
apply (erule TFin_induct)
paulson@13134
   160
apply (drule TFin_subsetD)
paulson@13784
   161
apply (assumption+, force, blast)
paulson@13134
   162
done
paulson@13134
   163
paulson@13558
   164
text{*Property 3.3 of section 3.3*}
paulson@13558
   165
lemma equal_next_Union:
paulson@13558
   166
     "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson@13134
   167
      ==> m = next`m <-> m = Union(TFin(S,next))"
paulson@13134
   168
apply (rule iffI)
paulson@13134
   169
apply (rule Union_upper [THEN equalityI])
paulson@13134
   170
apply (rule_tac [2] equal_next_upper [THEN Union_least])
paulson@13134
   171
apply (assumption+)
paulson@13134
   172
apply (erule ssubst)
paulson@13269
   173
apply (rule increasingD2 [THEN equalityI], assumption)
paulson@13134
   174
apply (blast del: subsetI
paulson@13134
   175
	     intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
paulson@13134
   176
done
paulson@13134
   177
paulson@13134
   178
paulson@13356
   179
subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain*}
paulson@13356
   180
paulson@13356
   181
text{*NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset
paulson@13356
   182
relation!*}
paulson@13134
   183
paulson@13558
   184
text{** 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@13558
   201
lemma choice_super:
skalberg@14171
   202
     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
paulson@13558
   203
      ==> ch ` super(S,X) \<in> super(S,X)"
paulson@13134
   204
apply (erule apply_type)
paulson@13269
   205
apply (unfold super_def maxchain_def, blast)
paulson@13134
   206
done
paulson@13134
   207
paulson@13134
   208
lemma choice_not_equals:
skalberg@14171
   209
     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
paulson@13558
   210
      ==> ch ` super(S,X) \<noteq> X"
paulson@13134
   211
apply (rule notI)
paulson@13784
   212
apply (drule choice_super, assumption, 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:
skalberg@14171
   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);
skalberg@14171
   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
ballarin@27704
   301
text {* Alternative version of Zorn's Lemma *}
ballarin@27704
   302
ballarin@27704
   303
theorem Zorn2:
ballarin@27704
   304
  "\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x <= y ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z --> y=z"
ballarin@27704
   305
apply (cut_tac Hausdorff maxchain_subset_chain)
ballarin@27704
   306
apply (erule exE)
ballarin@27704
   307
apply (drule subsetD, assumption)
ballarin@27704
   308
apply (drule bspec, assumption, erule bexE)
ballarin@27704
   309
apply (rule_tac x = y in bexI)
ballarin@27704
   310
  prefer 2 apply assumption
ballarin@27704
   311
apply clarify
ballarin@27704
   312
apply rule apply assumption
ballarin@27704
   313
apply rule
ballarin@27704
   314
apply (rule ccontr)
ballarin@27704
   315
apply (frule_tac z=z in chain_extend)
ballarin@27704
   316
  apply (assumption, blast)
ballarin@27704
   317
apply (unfold maxchain_def super_def)
ballarin@27704
   318
apply (blast elim!: equalityCE)
ballarin@27704
   319
done
ballarin@27704
   320
paulson@13134
   321
paulson@13356
   322
subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*}
paulson@13134
   323
paulson@13558
   324
text{*Lemma 5*}
paulson@13134
   325
lemma TFin_well_lemma5:
paulson@13558
   326
     "[| n \<in> TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) \<in> Z |]
paulson@13558
   327
      ==> \<forall>m \<in> Z. n <= m"
paulson@13134
   328
apply (erule TFin_induct)
paulson@13558
   329
prefer 2 apply blast txt{*second induction step is easy*}
paulson@13134
   330
apply (rule ballI)
paulson@13558
   331
apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
paulson@13134
   332
apply (subgoal_tac "m = Inter (Z) ")
paulson@13134
   333
apply blast+
paulson@13134
   334
done
paulson@13134
   335
paulson@13558
   336
text{*Well-ordering of @{term "TFin(S,next)"} *}
paulson@13558
   337
lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next);  z \<in> Z |] ==> Inter(Z) \<in> Z"
paulson@13134
   338
apply (rule classical)
paulson@13134
   339
apply (subgoal_tac "Z = {Union (TFin (S,next))}")
paulson@13134
   340
apply (simp (no_asm_simp) add: Inter_singleton)
paulson@13134
   341
apply (erule equal_singleton)
paulson@13134
   342
apply (rule Union_upper [THEN equalityI])
paulson@13269
   343
apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
paulson@13134
   344
done
paulson@13134
   345
paulson@13558
   346
text{*This theorem just packages the previous result*}
paulson@13134
   347
lemma well_ord_TFin:
paulson@13558
   348
     "next \<in> increasing(S) 
paulson@13558
   349
      ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
paulson@13134
   350
apply (rule well_ordI)
paulson@13134
   351
apply (unfold Subset_rel_def linear_def)
paulson@13558
   352
txt{*Prove the well-foundedness goal*}
paulson@13134
   353
apply (rule wf_onI)
paulson@13269
   354
apply (frule well_ord_TFin_lemma, assumption)
paulson@13269
   355
apply (drule_tac x = "Inter (Z) " in bspec, assumption)
paulson@13134
   356
apply blast
paulson@13558
   357
txt{*Now prove the linearity goal*}
paulson@13134
   358
apply (intro ballI)
paulson@13134
   359
apply (case_tac "x=y")
paulson@13269
   360
 apply blast
paulson@13558
   361
txt{*The @{term "x\<noteq>y"} case remains*}
paulson@13134
   362
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
paulson@13269
   363
       assumption+, blast+)
paulson@13134
   364
done
paulson@13134
   365
paulson@13558
   366
text{** Defining the "next" operation for Zermelo's Theorem **}
paulson@13134
   367
paulson@13134
   368
lemma choice_Diff:
skalberg@14171
   369
     "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
paulson@13134
   370
apply (erule apply_type)
paulson@13134
   371
apply (blast elim!: equalityE)
paulson@13134
   372
done
paulson@13134
   373
paulson@13558
   374
text{*This justifies Definition 6.1*}
paulson@13134
   375
lemma Zermelo_next_exists:
skalberg@14171
   376
     "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
paulson@13558
   377
           \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
paulson@13175
   378
                      next`X = (if X=S then S else cons(ch`(S-X), X))"
paulson@13175
   379
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
paulson@13175
   380
       in bexI)
paulson@13558
   381
apply force
paulson@13134
   382
apply (unfold increasing_def)
paulson@13134
   383
apply (rule CollectI)
paulson@13134
   384
apply (rule lam_type)
paulson@13558
   385
txt{*Type checking is surprisingly hard!*}
paulson@13134
   386
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
paulson@13134
   387
apply (blast intro!: choice_Diff [THEN DiffD1])
paulson@13558
   388
txt{*Verify that it increases*}
paulson@13558
   389
apply (intro allI impI)
paulson@13134
   390
apply (simp add: Pow_iff subset_consI subset_refl)
paulson@13134
   391
done
paulson@13134
   392
paulson@13134
   393
paulson@13558
   394
text{*The construction of the injection*}
paulson@13134
   395
lemma choice_imp_injection:
skalberg@14171
   396
     "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
paulson@13558
   397
         next \<in> increasing(S);
paulson@13558
   398
         \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
paulson@13558
   399
      ==> (\<lambda> x \<in> S. Union({y \<in> TFin(S,next). x \<notin> y}))
paulson@13558
   400
               \<in> inj(S, TFin(S,next) - {S})"
paulson@13134
   401
apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
paulson@13134
   402
apply (rule DiffI)
paulson@13134
   403
apply (rule Collect_subset [THEN TFin_UnionI])
paulson@13134
   404
apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
paulson@13558
   405
apply (subgoal_tac "x \<notin> Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson@13134
   406
prefer 2 apply (blast elim: equalityE)
paulson@13558
   407
apply (subgoal_tac "Union ({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
paulson@13134
   408
prefer 2 apply (blast elim: equalityE)
paulson@13558
   409
txt{*For proving @{text "x \<in> next`Union(...)"}.
paulson@13558
   410
  Abrial and Laffitte's justification appears to be faulty.*}
paulson@13558
   411
apply (subgoal_tac "~ next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) 
paulson@13558
   412
                    <= Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson@13558
   413
 prefer 2
paulson@13558
   414
 apply (simp del: Union_iff
paulson@13558
   415
	     add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]
paulson@13558
   416
	     Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
paulson@13558
   417
apply (subgoal_tac "x \<in> next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson@13558
   418
 prefer 2
paulson@13558
   419
 apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
paulson@13558
   420
txt{*End of the lemmas!*}
paulson@13134
   421
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
paulson@13134
   422
done
paulson@13134
   423
paulson@13558
   424
text{*The wellordering theorem*}
paulson@13558
   425
theorem AC_well_ord: "\<exists>r. well_ord(S,r)"
paulson@13134
   426
apply (rule AC_Pi_Pow [THEN exE])
paulson@13269
   427
apply (rule Zermelo_next_exists [THEN bexE], assumption)
paulson@13134
   428
apply (rule exI)
paulson@13134
   429
apply (rule well_ord_rvimage)
paulson@13134
   430
apply (erule_tac [2] well_ord_TFin)
paulson@13269
   431
apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
paulson@13134
   432
done
paulson@13558
   433
ballarin@27704
   434
ballarin@27704
   435
subsection {* Zorn's Lemma for Partial Orders *}
ballarin@27704
   436
ballarin@27704
   437
text {* Reimported from HOL by Clemens Ballarin. *}
ballarin@27704
   438
ballarin@27704
   439
ballarin@27704
   440
definition Chain :: "i => i" where
ballarin@27704
   441
  "Chain(r) = {A : Pow(field(r)). ALL a:A. ALL b:A. <a, b> : r | <b, a> : r}"
ballarin@27704
   442
ballarin@27704
   443
lemma mono_Chain:
ballarin@27704
   444
  "r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)"
ballarin@27704
   445
  unfolding Chain_def
ballarin@27704
   446
  by blast
ballarin@27704
   447
ballarin@27704
   448
theorem Zorn_po:
ballarin@27704
   449
  assumes po: "Partial_order(r)"
ballarin@27704
   450
    and u: "ALL C:Chain(r). EX u:field(r). ALL a:C. <a, u> : r"
ballarin@27704
   451
  shows "EX m:field(r). ALL a:field(r). <m, a> : r --> a = m"
ballarin@27704
   452
proof -
ballarin@27704
   453
  have "Preorder(r)" using po by (simp add: partial_order_on_def)
ballarin@27704
   454
  --{* Mirror r in the set of subsets below (wrt r) elements of A (?). *}
ballarin@27704
   455
  let ?B = "lam x:field(r). r -`` {x}" let ?S = "?B `` field(r)"
ballarin@27704
   456
  have "ALL C:chain(?S). EX U:?S. ALL A:C. A \<subseteq> U"
ballarin@27704
   457
  proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
ballarin@27704
   458
    fix C
ballarin@27704
   459
    assume 1: "C \<subseteq> ?S" and 2: "ALL A:C. ALL B:C. A \<subseteq> B | B \<subseteq> A"
ballarin@27704
   460
    let ?A = "{x : field(r). EX M:C. M = ?B`x}"
ballarin@27704
   461
    have "C = ?B `` ?A" using 1
ballarin@27704
   462
      apply (auto simp: image_def)
ballarin@27704
   463
      apply rule
ballarin@27704
   464
      apply rule
ballarin@27704
   465
      apply (drule subsetD) apply assumption
ballarin@27704
   466
      apply (erule CollectE)
ballarin@27704
   467
      apply rule apply assumption
ballarin@27704
   468
      apply (erule bexE)
ballarin@27704
   469
      apply rule prefer 2 apply assumption
ballarin@27704
   470
      apply rule
ballarin@27704
   471
      apply (erule lamE) apply simp
ballarin@27704
   472
      apply assumption
ballarin@27704
   473
ballarin@27704
   474
      apply (thin_tac "C \<subseteq> ?X")
ballarin@27704
   475
      apply (fast elim: lamE)
ballarin@27704
   476
      done
ballarin@27704
   477
    have "?A : Chain(r)"
ballarin@27704
   478
    proof (simp add: Chain_def subsetI, intro conjI ballI impI)
ballarin@27704
   479
      fix a b
ballarin@27704
   480
      assume "a : field(r)" "r -`` {a} : C" "b : field(r)" "r -`` {b} : C"
ballarin@27704
   481
      hence "r -`` {a} \<subseteq> r -`` {b} | r -`` {b} \<subseteq> r -`` {a}" using 2 by auto
ballarin@27704
   482
      then show "<a, b> : r | <b, a> : r"
ballarin@27704
   483
	using `Preorder(r)` `a : field(r)` `b : field(r)`
ballarin@27704
   484
	by (simp add: subset_vimage1_vimage1_iff)
ballarin@27704
   485
    qed
ballarin@27704
   486
    then obtain u where uA: "u : field(r)" "ALL a:?A. <a, u> : r"
ballarin@27704
   487
      using u
ballarin@27704
   488
      apply auto
ballarin@27704
   489
      apply (drule bspec) apply assumption
ballarin@27704
   490
      apply auto
ballarin@27704
   491
      done
ballarin@27704
   492
    have "ALL A:C. A \<subseteq> r -`` {u}"
ballarin@27704
   493
    proof (auto intro!: vimageI)
ballarin@27704
   494
      fix a B
ballarin@27704
   495
      assume aB: "B : C" "a : B"
ballarin@27704
   496
      with 1 obtain x where "x : field(r)" "B = r -`` {x}"
ballarin@27704
   497
	apply -
ballarin@27704
   498
	apply (drule subsetD) apply assumption
ballarin@27704
   499
	apply (erule imageE)
ballarin@27704
   500
	apply (erule lamE)
ballarin@27704
   501
	apply simp
ballarin@27704
   502
	done
ballarin@27704
   503
      then show "<a, u> : r" using uA aB `Preorder(r)`
ballarin@27704
   504
	by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+
ballarin@27704
   505
    qed
ballarin@27704
   506
    then show "EX U:field(r). ALL A:C. A \<subseteq> r -`` {U}"
ballarin@27704
   507
      using `u : field(r)` ..
ballarin@27704
   508
  qed
ballarin@27704
   509
  from Zorn2 [OF this]
ballarin@27704
   510
  obtain m B where "m : field(r)" "B = r -`` {m}"
ballarin@27704
   511
    "ALL x:field(r). B \<subseteq> r -`` {x} --> B = r -`` {x}"
ballarin@27704
   512
    by (auto elim!: lamE simp: ball_image_simp)
ballarin@27704
   513
  then have "ALL a:field(r). <m, a> : r --> a = m"
ballarin@27704
   514
    using po `Preorder(r)` `m : field(r)`
ballarin@27704
   515
    by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff)
ballarin@27704
   516
  then show ?thesis using `m : field(r)` by blast
ballarin@27704
   517
qed
ballarin@27704
   518
lcp@516
   519
end