src/ZF/Zorn.thy
author wenzelm
Thu Dec 14 11:24:26 2017 +0100 (20 months ago)
changeset 67198 694f29a5433b
parent 61980 6b780867d426
child 67443 3abf6a722518
permissions -rw-r--r--
merged
clasohm@1478
     1
(*  Title:      ZF/Zorn.thy
clasohm@1478
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@516
     3
    Copyright   1994  University of Cambridge
lcp@516
     4
*)
lcp@516
     5
wenzelm@60770
     6
section\<open>Zorn's Lemma\<close>
paulson@13356
     7
krauss@26056
     8
theory Zorn imports OrderArith AC Inductive_ZF begin
lcp@516
     9
wenzelm@60770
    10
text\<open>Based upon the unpublished article ``Towards the Mechanization of the
wenzelm@60770
    11
Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.\<close>
paulson@13356
    12
wenzelm@24893
    13
definition
wenzelm@24893
    14
  Subset_rel :: "i=>i"  where
paulson@13558
    15
   "Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}"
paulson@13134
    16
wenzelm@24893
    17
definition
wenzelm@24893
    18
  chain      :: "i=>i"  where
paulson@13558
    19
   "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
lcp@516
    20
wenzelm@24893
    21
definition
wenzelm@24893
    22
  super      :: "[i,i]=>i"  where
wenzelm@14653
    23
   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
wenzelm@14653
    24
wenzelm@24893
    25
definition
wenzelm@24893
    26
  maxchain   :: "i=>i"  where
paulson@13558
    27
   "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
paulson@13558
    28
wenzelm@24893
    29
definition
wenzelm@24893
    30
  increasing :: "i=>i"  where
paulson@46820
    31
    "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}"
lcp@516
    32
paulson@13356
    33
wenzelm@60770
    34
text\<open>Lemma for the inductive definition below\<close>
paulson@46820
    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
wenzelm@60770
    39
text\<open>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
wenzelm@60770
    43
    are therefore unconditional.\<close>
lcp@516
    44
consts
paulson@13134
    45
  "TFin" :: "[i,i]=>i"
lcp@516
    46
lcp@516
    47
inductive
paulson@46820
    48
  domains       "TFin(S,next)" \<subseteq> "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@46820
    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
wenzelm@60770
    60
subsection\<open>Mathematical Preamble\<close>
paulson@13134
    61
paulson@46820
    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@46820
    66
     "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A \<subseteq> \<Inter>(C) | \<Inter>(C) \<subseteq> B"
paulson@13269
    67
by blast
paulson@13134
    68
paulson@13134
    69
wenzelm@60770
    70
subsection\<open>The Transfinite Construction\<close>
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@46820
    77
lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x \<subseteq> f`x"
paulson@13269
    78
by (unfold increasing_def, blast)
paulson@13134
    79
wenzelm@45602
    80
lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]
paulson@13134
    81
wenzelm@45602
    82
lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD]
paulson@13134
    83
paulson@13134
    84
wenzelm@60770
    85
text\<open>Structural induction on @{term "TFin(S,next)"}\<close>
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@46820
    89
      !!Y. [| Y \<subseteq> 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
wenzelm@60770
    94
subsection\<open>Some Properties of the Transfinite Construction\<close>
paulson@13134
    95
paulson@13558
    96
lemmas increasing_trans = subset_trans [OF _ increasingD2,
paulson@13134
    97
                                        OF _ _ TFin_is_subset]
paulson@13134
    98
wenzelm@60770
    99
text\<open>Lemma 1 of section 3.1\<close>
paulson@13134
   100
lemma TFin_linear_lemma1:
paulson@13558
   101
     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);
paulson@46820
   102
         \<forall>x \<in> TFin(S,next) . x<=m \<longrightarrow> 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
wenzelm@60770
   110
text\<open>Lemma 2 of section 3.2.  Interesting in its own right!
wenzelm@60770
   111
  Requires @{term "next \<in> increasing(S)"} in the second induction step.\<close>
paulson@13134
   112
lemma TFin_linear_lemma2:
paulson@13558
   113
    "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson@46820
   114
     ==> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
paulson@13134
   115
apply (erule TFin_induct)
paulson@13134
   116
apply (rule impI [THEN ballI])
wenzelm@61798
   117
txt\<open>case split using \<open>TFin_linear_lemma1\<close>\<close>
paulson@13784
   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
wenzelm@32960
   121
             intro: increasing_trans subsetI, blast)
wenzelm@60770
   122
txt\<open>second induction step\<close>
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@13784
   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
wenzelm@60770
   136
text\<open>a more convenient form for Lemma 2\<close>
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@46820
   139
      ==> n=m | next`n \<subseteq> m"
paulson@13558
   140
by (blast dest: TFin_linear_lemma2 [rule_format])
paulson@13134
   141
wenzelm@60770
   142
text\<open>Consequences from section 3.3 -- Property 3.2, the ordering is total\<close>
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@46820
   145
      ==> n \<subseteq> 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
wenzelm@60770
   154
text\<open>Lemma 3 of section 3.3\<close>
paulson@13134
   155
lemma equal_next_upper:
paulson@46820
   156
     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n \<subseteq> m"
paulson@13134
   157
apply (erule TFin_induct)
paulson@13134
   158
apply (drule TFin_subsetD)
paulson@13784
   159
apply (assumption+, force, blast)
paulson@13134
   160
done
paulson@13134
   161
wenzelm@60770
   162
text\<open>Property 3.3 of section 3.3\<close>
paulson@13558
   163
lemma equal_next_Union:
paulson@13558
   164
     "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson@46820
   165
      ==> m = next`m <-> m = \<Union>(TFin(S,next))"
paulson@13134
   166
apply (rule iffI)
paulson@13134
   167
apply (rule Union_upper [THEN equalityI])
paulson@13134
   168
apply (rule_tac [2] equal_next_upper [THEN Union_least])
paulson@13134
   169
apply (assumption+)
paulson@13134
   170
apply (erule ssubst)
paulson@13269
   171
apply (rule increasingD2 [THEN equalityI], assumption)
paulson@13134
   172
apply (blast del: subsetI
wenzelm@32960
   173
             intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
paulson@13134
   174
done
paulson@13134
   175
paulson@13134
   176
wenzelm@60770
   177
subsection\<open>Hausdorff's Theorem: Every Set Contains a Maximal Chain\<close>
paulson@13356
   178
wenzelm@61798
   179
text\<open>NOTE: We assume the partial ordering is \<open>\<subseteq>\<close>, the subset
wenzelm@60770
   180
relation!\<close>
paulson@13134
   181
wenzelm@60770
   182
text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close>
paulson@13134
   183
paulson@46820
   184
lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)"
paulson@13134
   185
apply (unfold chain_def)
paulson@13134
   186
apply (rule Collect_subset)
paulson@13134
   187
done
paulson@13134
   188
paulson@46820
   189
lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)"
paulson@13134
   190
apply (unfold super_def)
paulson@13134
   191
apply (rule Collect_subset)
paulson@13134
   192
done
paulson@13134
   193
paulson@46820
   194
lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)"
paulson@13134
   195
apply (unfold maxchain_def)
paulson@13134
   196
apply (rule Collect_subset)
paulson@13134
   197
done
paulson@13134
   198
paulson@13558
   199
lemma choice_super:
wenzelm@61980
   200
     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
paulson@13558
   201
      ==> ch ` super(S,X) \<in> super(S,X)"
paulson@13134
   202
apply (erule apply_type)
paulson@13269
   203
apply (unfold super_def maxchain_def, blast)
paulson@13134
   204
done
paulson@13134
   205
paulson@13134
   206
lemma choice_not_equals:
wenzelm@61980
   207
     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
paulson@13558
   208
      ==> ch ` super(S,X) \<noteq> X"
paulson@13134
   209
apply (rule notI)
paulson@13784
   210
apply (drule choice_super, assumption, assumption)
paulson@13134
   211
apply (simp add: super_def)
paulson@13134
   212
done
paulson@13134
   213
wenzelm@60770
   214
text\<open>This justifies Definition 4.4\<close>
paulson@13134
   215
lemma Hausdorff_next_exists:
wenzelm@61980
   216
     "ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X) ==>
paulson@13558
   217
      \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
paulson@13558
   218
                   next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
paulson@13558
   219
apply (rule_tac x="\<lambda>X\<in>Pow(S).
paulson@13558
   220
                   if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
paulson@13175
   221
       in bexI)
paulson@13558
   222
apply force
paulson@13134
   223
apply (unfold increasing_def)
paulson@13134
   224
apply (rule CollectI)
paulson@13134
   225
apply (rule lam_type)
paulson@13134
   226
apply (simp (no_asm_simp))
paulson@13558
   227
apply (blast dest: super_subset_chain [THEN subsetD] 
paulson@13558
   228
                   chain_subset_Pow [THEN subsetD] choice_super)
wenzelm@60770
   229
txt\<open>Now, verify that it increases\<close>
paulson@13134
   230
apply (simp (no_asm_simp) add: Pow_iff subset_refl)
paulson@13134
   231
apply safe
paulson@13134
   232
apply (drule choice_super)
paulson@13134
   233
apply (assumption+)
paulson@13269
   234
apply (simp add: super_def, blast)
paulson@13134
   235
done
paulson@13134
   236
wenzelm@60770
   237
text\<open>Lemma 4\<close>
paulson@13134
   238
lemma TFin_chain_lemma4:
paulson@13558
   239
     "[| c \<in> TFin(S,next);
wenzelm@61980
   240
         ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X);
paulson@13558
   241
         next \<in> increasing(S);
paulson@13558
   242
         \<forall>X \<in> Pow(S). next`X =
paulson@13558
   243
                          if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
paulson@13558
   244
     ==> c \<in> chain(S)"
paulson@13134
   245
apply (erule TFin_induct)
paulson@13558
   246
apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
paulson@13134
   247
            choice_super [THEN super_subset_chain [THEN subsetD]])
paulson@13134
   248
apply (unfold chain_def)
paulson@13269
   249
apply (rule CollectI, blast, safe)
paulson@13558
   250
apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
wenzelm@61798
   251
      txt\<open>\<open>Blast_tac's\<close> slow\<close>
paulson@13134
   252
done
paulson@13134
   253
paulson@13558
   254
theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)"
paulson@13134
   255
apply (rule AC_Pi_Pow [THEN exE])
paulson@13269
   256
apply (rule Hausdorff_next_exists [THEN bexE], assumption)
paulson@13134
   257
apply (rename_tac ch "next")
paulson@46820
   258
apply (subgoal_tac "\<Union>(TFin (S,next)) \<in> chain (S) ")
paulson@13134
   259
prefer 2
paulson@13134
   260
 apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
paulson@46820
   261
apply (rule_tac x = "\<Union>(TFin (S,next))" in exI)
paulson@13134
   262
apply (rule classical)
paulson@46820
   263
apply (subgoal_tac "next ` Union(TFin (S,next)) = \<Union>(TFin (S,next))")
paulson@13134
   264
apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
paulson@13134
   265
apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
paulson@13269
   266
prefer 2 apply assumption
paulson@13134
   267
apply (rule_tac [2] refl)
paulson@13558
   268
apply (simp add: subset_refl [THEN TFin_UnionI,
paulson@13134
   269
                              THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
paulson@13134
   270
apply (erule choice_not_equals [THEN notE])
paulson@13134
   271
apply (assumption+)
paulson@13134
   272
done
paulson@13134
   273
paulson@13134
   274
wenzelm@60770
   275
subsection\<open>Zorn's Lemma: If All Chains in S Have Upper Bounds In S,
wenzelm@60770
   276
       then S contains a Maximal Element\<close>
paulson@13356
   277
wenzelm@60770
   278
text\<open>Used in the proof of Zorn's Lemma\<close>
paulson@13558
   279
lemma chain_extend:
paulson@13558
   280
    "[| c \<in> chain(A);  z \<in> A;  \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)"
paulson@13356
   281
by (unfold chain_def, blast)
paulson@13134
   282
paulson@46820
   283
lemma Zorn: "\<forall>c \<in> chain(S). \<Union>(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
paulson@13134
   284
apply (rule Hausdorff [THEN exE])
paulson@13134
   285
apply (simp add: maxchain_def)
paulson@13134
   286
apply (rename_tac c)
paulson@46820
   287
apply (rule_tac x = "\<Union>(c)" in bexI)
paulson@13269
   288
prefer 2 apply blast
paulson@13134
   289
apply safe
paulson@13134
   290
apply (rename_tac z)
paulson@13134
   291
apply (rule classical)
paulson@13558
   292
apply (subgoal_tac "cons (z,c) \<in> super (S,c) ")
paulson@13134
   293
apply (blast elim: equalityE)
paulson@13269
   294
apply (unfold super_def, safe)
paulson@13134
   295
apply (fast elim: chain_extend)
paulson@13134
   296
apply (fast elim: equalityE)
paulson@13134
   297
done
paulson@13134
   298
wenzelm@60770
   299
text \<open>Alternative version of Zorn's Lemma\<close>
ballarin@27704
   300
ballarin@27704
   301
theorem Zorn2:
paulson@46820
   302
  "\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
ballarin@27704
   303
apply (cut_tac Hausdorff maxchain_subset_chain)
ballarin@27704
   304
apply (erule exE)
ballarin@27704
   305
apply (drule subsetD, assumption)
ballarin@27704
   306
apply (drule bspec, assumption, erule bexE)
ballarin@27704
   307
apply (rule_tac x = y in bexI)
ballarin@27704
   308
  prefer 2 apply assumption
ballarin@27704
   309
apply clarify
ballarin@27704
   310
apply rule apply assumption
ballarin@27704
   311
apply rule
ballarin@27704
   312
apply (rule ccontr)
ballarin@27704
   313
apply (frule_tac z=z in chain_extend)
ballarin@27704
   314
  apply (assumption, blast)
ballarin@27704
   315
apply (unfold maxchain_def super_def)
ballarin@27704
   316
apply (blast elim!: equalityCE)
ballarin@27704
   317
done
ballarin@27704
   318
paulson@13134
   319
wenzelm@60770
   320
subsection\<open>Zermelo's Theorem: Every Set can be Well-Ordered\<close>
paulson@13134
   321
wenzelm@60770
   322
text\<open>Lemma 5\<close>
paulson@13134
   323
lemma TFin_well_lemma5:
paulson@46820
   324
     "[| n \<in> TFin(S,next);  Z \<subseteq> TFin(S,next);  z:Z;  ~ \<Inter>(Z) \<in> Z |]
paulson@46820
   325
      ==> \<forall>m \<in> Z. n \<subseteq> m"
paulson@13134
   326
apply (erule TFin_induct)
wenzelm@60770
   327
prefer 2 apply blast txt\<open>second induction step is easy\<close>
paulson@13134
   328
apply (rule ballI)
paulson@13558
   329
apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
paulson@46820
   330
apply (subgoal_tac "m = \<Inter>(Z) ")
paulson@13134
   331
apply blast+
paulson@13134
   332
done
paulson@13134
   333
wenzelm@60770
   334
text\<open>Well-ordering of @{term "TFin(S,next)"}\<close>
paulson@46820
   335
lemma well_ord_TFin_lemma: "[| Z \<subseteq> TFin(S,next);  z \<in> Z |] ==> \<Inter>(Z) \<in> Z"
paulson@13134
   336
apply (rule classical)
paulson@46820
   337
apply (subgoal_tac "Z = {\<Union>(TFin (S,next))}")
paulson@13134
   338
apply (simp (no_asm_simp) add: Inter_singleton)
paulson@13134
   339
apply (erule equal_singleton)
paulson@13134
   340
apply (rule Union_upper [THEN equalityI])
paulson@13269
   341
apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
paulson@13134
   342
done
paulson@13134
   343
wenzelm@60770
   344
text\<open>This theorem just packages the previous result\<close>
paulson@13134
   345
lemma well_ord_TFin:
paulson@13558
   346
     "next \<in> increasing(S) 
paulson@13558
   347
      ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
paulson@13134
   348
apply (rule well_ordI)
paulson@13134
   349
apply (unfold Subset_rel_def linear_def)
wenzelm@60770
   350
txt\<open>Prove the well-foundedness goal\<close>
paulson@13134
   351
apply (rule wf_onI)
paulson@13269
   352
apply (frule well_ord_TFin_lemma, assumption)
paulson@46820
   353
apply (drule_tac x = "\<Inter>(Z) " in bspec, assumption)
paulson@13134
   354
apply blast
wenzelm@60770
   355
txt\<open>Now prove the linearity goal\<close>
paulson@13134
   356
apply (intro ballI)
paulson@13134
   357
apply (case_tac "x=y")
paulson@13269
   358
 apply blast
wenzelm@60770
   359
txt\<open>The @{term "x\<noteq>y"} case remains\<close>
paulson@13134
   360
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
paulson@13269
   361
       assumption+, blast+)
paulson@13134
   362
done
paulson@13134
   363
wenzelm@60770
   364
text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close>
paulson@13134
   365
paulson@13134
   366
lemma choice_Diff:
wenzelm@61980
   367
     "[| ch \<in> (\<Prod>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
paulson@13134
   368
apply (erule apply_type)
paulson@13134
   369
apply (blast elim!: equalityE)
paulson@13134
   370
done
paulson@13134
   371
wenzelm@60770
   372
text\<open>This justifies Definition 6.1\<close>
paulson@13134
   373
lemma Zermelo_next_exists:
wenzelm@61980
   374
     "ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X) ==>
paulson@13558
   375
           \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
paulson@13175
   376
                      next`X = (if X=S then S else cons(ch`(S-X), X))"
paulson@13175
   377
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
paulson@13175
   378
       in bexI)
paulson@13558
   379
apply force
paulson@13134
   380
apply (unfold increasing_def)
paulson@13134
   381
apply (rule CollectI)
paulson@13134
   382
apply (rule lam_type)
wenzelm@60770
   383
txt\<open>Type checking is surprisingly hard!\<close>
paulson@13134
   384
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
paulson@13134
   385
apply (blast intro!: choice_Diff [THEN DiffD1])
wenzelm@60770
   386
txt\<open>Verify that it increases\<close>
paulson@13558
   387
apply (intro allI impI)
paulson@13134
   388
apply (simp add: Pow_iff subset_consI subset_refl)
paulson@13134
   389
done
paulson@13134
   390
paulson@13134
   391
wenzelm@60770
   392
text\<open>The construction of the injection\<close>
paulson@13134
   393
lemma choice_imp_injection:
wenzelm@61980
   394
     "[| ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X);
paulson@13558
   395
         next \<in> increasing(S);
paulson@13558
   396
         \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
paulson@46820
   397
      ==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
paulson@13558
   398
               \<in> inj(S, TFin(S,next) - {S})"
paulson@13134
   399
apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
paulson@13134
   400
apply (rule DiffI)
paulson@13134
   401
apply (rule Collect_subset [THEN TFin_UnionI])
paulson@13134
   402
apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
paulson@46820
   403
apply (subgoal_tac "x \<notin> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson@13134
   404
prefer 2 apply (blast elim: equalityE)
paulson@46820
   405
apply (subgoal_tac "\<Union>({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
paulson@13134
   406
prefer 2 apply (blast elim: equalityE)
wenzelm@61798
   407
txt\<open>For proving \<open>x \<in> next`\<Union>(...)\<close>.
wenzelm@60770
   408
  Abrial and Laffitte's justification appears to be faulty.\<close>
paulson@46820
   409
apply (subgoal_tac "~ next ` Union({y \<in> TFin (S,next) . x \<notin> y}) 
paulson@46820
   410
                    \<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson@13558
   411
 prefer 2
paulson@13558
   412
 apply (simp del: Union_iff
wenzelm@32960
   413
             add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]
wenzelm@32960
   414
             Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
paulson@46820
   415
apply (subgoal_tac "x \<in> next ` Union({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson@13558
   416
 prefer 2
paulson@13558
   417
 apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
wenzelm@60770
   418
txt\<open>End of the lemmas!\<close>
paulson@13134
   419
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
paulson@13134
   420
done
paulson@13134
   421
wenzelm@60770
   422
text\<open>The wellordering theorem\<close>
paulson@13558
   423
theorem AC_well_ord: "\<exists>r. well_ord(S,r)"
paulson@13134
   424
apply (rule AC_Pi_Pow [THEN exE])
paulson@13269
   425
apply (rule Zermelo_next_exists [THEN bexE], assumption)
paulson@13134
   426
apply (rule exI)
paulson@13134
   427
apply (rule well_ord_rvimage)
paulson@13134
   428
apply (erule_tac [2] well_ord_TFin)
paulson@13269
   429
apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
paulson@13134
   430
done
paulson@13558
   431
ballarin@27704
   432
wenzelm@60770
   433
subsection \<open>Zorn's Lemma for Partial Orders\<close>
ballarin@27704
   434
wenzelm@60770
   435
text \<open>Reimported from HOL by Clemens Ballarin.\<close>
ballarin@27704
   436
ballarin@27704
   437
ballarin@27704
   438
definition Chain :: "i => i" where
paulson@46820
   439
  "Chain(r) = {A \<in> Pow(field(r)). \<forall>a\<in>A. \<forall>b\<in>A. <a, b> \<in> r | <b, a> \<in> r}"
ballarin@27704
   440
ballarin@27704
   441
lemma mono_Chain:
ballarin@27704
   442
  "r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)"
ballarin@27704
   443
  unfolding Chain_def
ballarin@27704
   444
  by blast
ballarin@27704
   445
ballarin@27704
   446
theorem Zorn_po:
ballarin@27704
   447
  assumes po: "Partial_order(r)"
paulson@46820
   448
    and u: "\<forall>C\<in>Chain(r). \<exists>u\<in>field(r). \<forall>a\<in>C. <a, u> \<in> r"
paulson@46820
   449
  shows "\<exists>m\<in>field(r). \<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
ballarin@27704
   450
proof -
ballarin@27704
   451
  have "Preorder(r)" using po by (simp add: partial_order_on_def)
wenzelm@61798
   452
  \<comment>\<open>Mirror r in the set of subsets below (wrt r) elements of A (?).\<close>
paulson@46820
   453
  let ?B = "\<lambda>x\<in>field(r). r -`` {x}" let ?S = "?B `` field(r)"
paulson@46820
   454
  have "\<forall>C\<in>chain(?S). \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
ballarin@27704
   455
  proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
ballarin@27704
   456
    fix C
paulson@46820
   457
    assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B | B \<subseteq> A"
paulson@46820
   458
    let ?A = "{x \<in> field(r). \<exists>M\<in>C. M = ?B`x}"
ballarin@27704
   459
    have "C = ?B `` ?A" using 1
ballarin@27704
   460
      apply (auto simp: image_def)
ballarin@27704
   461
      apply rule
ballarin@27704
   462
      apply rule
ballarin@27704
   463
      apply (drule subsetD) apply assumption
ballarin@27704
   464
      apply (erule CollectE)
ballarin@27704
   465
      apply rule apply assumption
ballarin@27704
   466
      apply (erule bexE)
ballarin@27704
   467
      apply rule prefer 2 apply assumption
ballarin@27704
   468
      apply rule
ballarin@27704
   469
      apply (erule lamE) apply simp
ballarin@27704
   470
      apply assumption
ballarin@27704
   471
wenzelm@59788
   472
      apply (thin_tac "C \<subseteq> X" for X)
ballarin@27704
   473
      apply (fast elim: lamE)
ballarin@27704
   474
      done
paulson@46820
   475
    have "?A \<in> Chain(r)"
ballarin@27704
   476
    proof (simp add: Chain_def subsetI, intro conjI ballI impI)
ballarin@27704
   477
      fix a b
paulson@46820
   478
      assume "a \<in> field(r)" "r -`` {a} \<in> C" "b \<in> field(r)" "r -`` {b} \<in> C"
ballarin@27704
   479
      hence "r -`` {a} \<subseteq> r -`` {b} | r -`` {b} \<subseteq> r -`` {a}" using 2 by auto
paulson@46820
   480
      then show "<a, b> \<in> r | <b, a> \<in> r"
wenzelm@60770
   481
        using \<open>Preorder(r)\<close> \<open>a \<in> field(r)\<close> \<open>b \<in> field(r)\<close>
wenzelm@32960
   482
        by (simp add: subset_vimage1_vimage1_iff)
ballarin@27704
   483
    qed
paulson@46820
   484
    then obtain u where uA: "u \<in> field(r)" "\<forall>a\<in>?A. <a, u> \<in> r"
ballarin@27704
   485
      using u
ballarin@27704
   486
      apply auto
ballarin@27704
   487
      apply (drule bspec) apply assumption
ballarin@27704
   488
      apply auto
ballarin@27704
   489
      done
paulson@46820
   490
    have "\<forall>A\<in>C. A \<subseteq> r -`` {u}"
ballarin@27704
   491
    proof (auto intro!: vimageI)
ballarin@27704
   492
      fix a B
paulson@46820
   493
      assume aB: "B \<in> C" "a \<in> B"
paulson@46820
   494
      with 1 obtain x where "x \<in> field(r)" "B = r -`` {x}"
wenzelm@32960
   495
        apply -
wenzelm@32960
   496
        apply (drule subsetD) apply assumption
wenzelm@32960
   497
        apply (erule imageE)
wenzelm@32960
   498
        apply (erule lamE)
wenzelm@32960
   499
        apply simp
wenzelm@32960
   500
        done
wenzelm@60770
   501
      then show "<a, u> \<in> r" using uA aB \<open>Preorder(r)\<close>
wenzelm@32960
   502
        by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+
ballarin@27704
   503
    qed
paulson@46820
   504
    then show "\<exists>U\<in>field(r). \<forall>A\<in>C. A \<subseteq> r -`` {U}"
wenzelm@60770
   505
      using \<open>u \<in> field(r)\<close> ..
ballarin@27704
   506
  qed
ballarin@27704
   507
  from Zorn2 [OF this]
paulson@46820
   508
  obtain m B where "m \<in> field(r)" "B = r -`` {m}"
paulson@46820
   509
    "\<forall>x\<in>field(r). B \<subseteq> r -`` {x} \<longrightarrow> B = r -`` {x}"
ballarin@27704
   510
    by (auto elim!: lamE simp: ball_image_simp)
paulson@46820
   511
  then have "\<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
wenzelm@60770
   512
    using po \<open>Preorder(r)\<close> \<open>m \<in> field(r)\<close>
ballarin@27704
   513
    by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff)
wenzelm@60770
   514
  then show ?thesis using \<open>m \<in> field(r)\<close> by blast
ballarin@27704
   515
qed
ballarin@27704
   516
lcp@516
   517
end