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