src/ZF/Zorn.ML
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 5774 c675d4a8c26a
child 6065 3b4a29166f26
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
     1 (*  Title:      ZF/Zorn.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Proofs from the paper
     7     Abrial & Laffitte, 
     8     Towards the Mechanization of the Proofs of Some 
     9     Classical Theorems of Set Theory. 
    10 *)
    11 
    12 (*** Section 1.  Mathematical Preamble ***)
    13 
    14 Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
    15 by (Blast_tac 1);
    16 qed "Union_lemma0";
    17 
    18 Goal "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
    19 by (Blast_tac 1);
    20 qed "Inter_lemma0";
    21 
    22 
    23 (*** Section 2.  The Transfinite Construction ***)
    24 
    25 Goalw [increasing_def] "f: increasing(A) ==> f: Pow(A)->Pow(A)";
    26 by (etac CollectD1 1);
    27 qed "increasingD1";
    28 
    29 Goalw [increasing_def] "[| f: increasing(A); x<=A |] ==> x <= f`x";
    30 by (eresolve_tac [CollectD2 RS spec RS mp] 1);
    31 by (assume_tac 1);
    32 qed "increasingD2";
    33 
    34 (*Introduction rules*)
    35 val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
    36 val TFin_UnionI = PowI RS Pow_TFin_UnionI;
    37 
    38 val TFin_is_subset = TFin.dom_subset RS subsetD RS PowD;
    39 
    40 
    41 (** Structural induction on TFin(S,next) **)
    42 
    43 val major::prems = Goal
    44   "[| n: TFin(S,next);  \
    45 \     !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x); \
    46 \     !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y)) \
    47 \  |] ==> P(n)";
    48 by (rtac (major RS TFin.induct) 1);
    49 by (ALLGOALS (fast_tac (claset() addIs prems)));
    50 qed "TFin_induct";
    51 
    52 (*Perform induction on n, then prove the major premise using prems. *)
    53 fun TFin_ind_tac a prems i = 
    54     EVERY [res_inst_tac [("n",a)] TFin_induct i,
    55            rename_last_tac a ["1"] (i+1),
    56            rename_last_tac a ["2"] (i+2),
    57            ares_tac prems i];
    58 
    59 (*** Section 3.  Some Properties of the Transfinite Construction ***)
    60 
    61 bind_thm ("increasing_trans", 
    62           TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)));
    63 
    64 (*Lemma 1 of section 3.1*)
    65 Goal "[| n: TFin(S,next);  m: TFin(S,next);  \
    66 \        ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
    67 \     |] ==> n<=m | next`m<=n";
    68 by (etac TFin_induct 1);
    69 by (etac Union_lemma0 2);               (*or just Blast_tac*)
    70 by (blast_tac (subset_cs addIs [increasing_trans]) 1);
    71 qed "TFin_linear_lemma1";
    72 
    73 (*Lemma 2 of section 3.2.  Interesting in its own right!
    74   Requires next: increasing(S) in the second induction step. *)
    75 val [major,ninc] = goal Zorn.thy
    76     "[| m: TFin(S,next);  next: increasing(S) \
    77 \    |] ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m";
    78 by (rtac (major RS TFin_induct) 1);
    79 by (rtac (impI RS ballI) 1);
    80 (*case split using TFin_linear_lemma1*)
    81 by (res_inst_tac [("n1","n"), ("m1","x")] 
    82     (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    83 by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1);
    84 by (blast_tac (subset_cs addIs [increasing_trans]) 1);
    85 by (REPEAT (ares_tac [disjI1,equalityI] 1));
    86 (*second induction step*)
    87 by (rtac (impI RS ballI) 1);
    88 by (rtac (Union_lemma0 RS disjE) 1);
    89 by (etac disjI2 3);
    90 by (REPEAT (ares_tac [disjI1,equalityI] 2));
    91 by (rtac ballI 1);
    92 by (ball_tac 1);
    93 by (set_mp_tac 1);
    94 by (res_inst_tac [("n1","n"), ("m1","x")] 
    95     (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    96 by (blast_tac subset_cs 1);
    97 by (rtac (ninc RS increasingD2 RS subset_trans RS disjI1) 1);
    98 by (REPEAT (ares_tac [TFin_is_subset] 1));
    99 qed "TFin_linear_lemma2";
   100 
   101 (*a more convenient form for Lemma 2*)
   102 Goal "[| n<=m;  m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |] \
   103 \     ==> n=m | next`n<=m";
   104 by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1);
   105 by (REPEAT (assume_tac 1));
   106 qed "TFin_subsetD";
   107 
   108 (*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
   109 Goal "[| m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) |] \
   110 \     ==> n<=m | m<=n";
   111 by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1);
   112 by (REPEAT (assume_tac 1) THEN etac disjI2 1);
   113 by (blast_tac (subset_cs addIs [increasingD2 RS subset_trans, 
   114                                TFin_is_subset]) 1);
   115 qed "TFin_subset_linear";
   116 
   117 
   118 (*Lemma 3 of section 3.3*)
   119 Goal "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m";
   120 by (etac TFin_induct 1);
   121 by (dtac TFin_subsetD 1);
   122 by (REPEAT (assume_tac 1));
   123 by (fast_tac (claset() addEs [ssubst]) 1);
   124 by (blast_tac (subset_cs addIs [TFin_is_subset]) 1);
   125 qed "equal_next_upper";
   126 
   127 (*Property 3.3 of section 3.3*)
   128 Goal "[| m: TFin(S,next);  next: increasing(S) |]  \
   129 \     ==> m = next`m <-> m = Union(TFin(S,next))";
   130 by (rtac iffI 1);
   131 by (rtac (Union_upper RS equalityI) 1);
   132 by (rtac (equal_next_upper RS Union_least) 2);
   133 by (REPEAT (assume_tac 1));
   134 by (etac ssubst 1);
   135 by (rtac (increasingD2 RS equalityI) 1 THEN assume_tac 1);
   136 by (ALLGOALS
   137     (blast_tac (subset_cs addIs [TFin_UnionI, TFin_nextI, TFin_is_subset])));
   138 qed "equal_next_Union";
   139 
   140 
   141 (*** Section 4.  Hausdorff's Theorem: every set contains a maximal chain ***)
   142 (*** NB: We assume the partial ordering is <=, the subset relation! **)
   143 
   144 (** Defining the "next" operation for Hausdorff's Theorem **)
   145 
   146 Goalw [chain_def] "chain(A) <= Pow(A)";
   147 by (rtac Collect_subset 1);
   148 qed "chain_subset_Pow";
   149 
   150 Goalw [super_def] "super(A,c) <= chain(A)";
   151 by (rtac Collect_subset 1);
   152 qed "super_subset_chain";
   153 
   154 Goalw [maxchain_def] "maxchain(A) <= chain(A)";
   155 by (rtac Collect_subset 1);
   156 qed "maxchain_subset_chain";
   157 
   158 Goal "[| ch : (PROD X:Pow(chain(S)) - {0}. X);  \
   159 \        X : chain(S);  X ~: maxchain(S) |]     \
   160 \     ==> ch ` super(S,X) : super(S,X)";
   161 by (etac apply_type 1);
   162 by (rewrite_goals_tac [super_def, maxchain_def]);
   163 by (Blast_tac 1);
   164 qed "choice_super";
   165 
   166 Goal "[| ch : (PROD X:Pow(chain(S)) - {0}. X);      \
   167 \            X : chain(S);  X ~: maxchain(S) |]     \
   168 \     ==> ch ` super(S,X) ~= X";
   169 by (rtac notI 1);
   170 by (dtac choice_super 1);
   171 by (assume_tac 1);
   172 by (assume_tac 1);
   173 by (asm_full_simp_tac (simpset() addsimps [super_def]) 1);
   174 qed "choice_not_equals";
   175 
   176 (*This justifies Definition 4.4*)
   177 Goal "ch: (PROD X: Pow(chain(S))-{0}. X) ==>        \
   178 \     EX next: increasing(S). ALL X: Pow(S).       \
   179 \                  next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)";
   180 by (rtac bexI 1);
   181 by (rtac ballI 1);
   182 by (rtac beta 1);
   183 by (assume_tac 1);
   184 by (rewtac increasing_def);
   185 by (rtac CollectI 1);
   186 by (rtac lam_type 1);
   187 by (Asm_simp_tac 1);
   188 by (fast_tac (claset() addSIs [super_subset_chain RS subsetD,
   189 			       chain_subset_Pow RS subsetD,
   190 			       choice_super]) 1);
   191 (*Now, verify that it increases*)
   192 by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_refl]) 1);
   193 by Safe_tac;
   194 by (dtac choice_super 1);
   195 by (REPEAT (assume_tac 1));
   196 by (rewtac super_def);
   197 by (Blast_tac 1);
   198 qed "Hausdorff_next_exists";
   199 
   200 (*Lemma 4*)
   201 Goal " [| c: TFin(S,next);                              \
   202 \         ch: (PROD X: Pow(chain(S))-{0}. X);           \
   203 \         next: increasing(S);                          \
   204 \         ALL X: Pow(S). next`X =       \
   205 \                         if(X: chain(S)-maxchain(S), ch`super(S,X), X) \
   206 \      |] ==> c: chain(S)";
   207 by (etac TFin_induct 1);
   208 by (asm_simp_tac 
   209     (simpset() addsimps [chain_subset_Pow RS subsetD, 
   210 			 choice_super RS (super_subset_chain RS subsetD)]) 1);
   211 by (rewtac chain_def);
   212 by (rtac CollectI 1 THEN Blast_tac 1);
   213 by Safe_tac;
   214 by (res_inst_tac  [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
   215 by (ALLGOALS Fast_tac);   (*Blast_tac's slow*)
   216 qed "TFin_chain_lemma4";
   217 
   218 Goal "EX c. c : maxchain(S)";
   219 by (rtac (AC_Pi_Pow RS exE) 1);
   220 by (rtac (Hausdorff_next_exists RS bexE) 1);
   221 by (assume_tac 1);
   222 by (rename_tac "ch next" 1);
   223 by (subgoal_tac "Union(TFin(S,next)) : chain(S)" 1);
   224 by (REPEAT (ares_tac [TFin_chain_lemma4, subset_refl RS TFin_UnionI] 2));
   225 by (res_inst_tac [("x", "Union(TFin(S,next))")] exI 1);
   226 by (rtac classical 1);
   227 by (subgoal_tac "next ` Union(TFin(S,next)) = Union(TFin(S,next))" 1);
   228 by (resolve_tac [equal_next_Union RS iffD2 RS sym] 2);
   229 by (resolve_tac [subset_refl RS TFin_UnionI] 2);
   230 by (assume_tac 2);
   231 by (rtac refl 2);
   232 by (asm_full_simp_tac 
   233     (simpset() addsimps [subset_refl RS TFin_UnionI RS
   234 			 (TFin.dom_subset RS subsetD)]) 1);
   235 by (eresolve_tac [choice_not_equals RS notE] 1);
   236 by (REPEAT (assume_tac 1));
   237 qed "Hausdorff";
   238 
   239 
   240 (*** Section 5.  Zorn's Lemma: if all chains in S have upper bounds in S 
   241                                then S contains a maximal element ***)
   242 
   243 (*Used in the proof of Zorn's Lemma*)
   244 Goalw [chain_def]
   245     "[| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)";
   246 by (Blast_tac 1);
   247 qed "chain_extend";
   248 
   249 Goal "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z";
   250 by (resolve_tac [Hausdorff RS exE] 1);
   251 by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1);
   252 by (rename_tac "c" 1);
   253 by (res_inst_tac [("x", "Union(c)")] bexI 1);
   254 by (Blast_tac 2);
   255 by Safe_tac;
   256 by (rename_tac "z" 1);
   257 by (rtac classical 1);
   258 by (subgoal_tac "cons(z,c): super(S,c)" 1);
   259 by (blast_tac (claset() addEs [equalityE]) 1);
   260 by (rewtac super_def);
   261 by Safe_tac;
   262 by (fast_tac (claset() addEs [chain_extend]) 1);
   263 by (fast_tac (claset() addEs [equalityE]) 1);
   264 qed "Zorn";
   265 
   266 
   267 (*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
   268 
   269 (*Lemma 5*)
   270 Goal "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z |]  \
   271 \     ==> ALL m:Z. n<=m";
   272 by (etac TFin_induct 1);
   273 by (Blast_tac 2);                  (*second induction step is easy*)
   274 by (rtac ballI 1);
   275 by (rtac (bspec RS TFin_subsetD RS disjE) 1);
   276 by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
   277 by (subgoal_tac "x = Inter(Z)" 1);
   278 by (Blast_tac 1);
   279 by (Blast_tac 1);
   280 qed "TFin_well_lemma5";
   281 
   282 (*Well-ordering of TFin(S,next)*)
   283 Goal "[| Z <= TFin(S,next);  z:Z |] ==> Inter(Z) : Z";
   284 by (rtac classical 1);
   285 by (subgoal_tac "Z = {Union(TFin(S,next))}" 1);
   286 by (asm_simp_tac (simpset() addsimps [Inter_singleton]) 1);
   287 by (etac equal_singleton 1);
   288 by (rtac (Union_upper RS equalityI) 1);
   289 by (rtac (subset_refl RS TFin_UnionI RS TFin_well_lemma5 RS bspec) 2);
   290 by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
   291 qed "well_ord_TFin_lemma";
   292 
   293 (*This theorem just packages the previous result*)
   294 Goal "next: increasing(S) ==> \
   295 \         well_ord(TFin(S,next), Subset_rel(TFin(S,next)))";
   296 by (rtac well_ordI 1);
   297 by (rewrite_goals_tac [Subset_rel_def, linear_def]);
   298 (*Prove the linearity goal first*)
   299 by (REPEAT (rtac ballI 2));
   300 by (excluded_middle_tac "x=y" 2);
   301 by (Blast_tac 3);
   302 (*The x~=y case remains*)
   303 by (res_inst_tac [("n1","x"), ("m1","y")] 
   304     (TFin_subset_linear RS disjE) 2  THEN  REPEAT (assume_tac 2));
   305 by (Blast_tac 2);
   306 by (Blast_tac 2);
   307 (*Now prove the well_foundedness goal*)
   308 by (rtac wf_onI 1);
   309 by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
   310 by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
   311 by (Blast_tac 1);
   312 qed "well_ord_TFin";
   313 
   314 (** Defining the "next" operation for Zermelo's Theorem **)
   315 
   316 (*This justifies Definition 6.1*)
   317 Goal "ch: (PROD X: Pow(S)-{0}. X) ==>               \
   318 \          EX next: increasing(S). ALL X: Pow(S).       \
   319 \                     next`X = if(X=S, S, cons(ch`(S-X), X))";
   320 by (rtac bexI 1);
   321 by (rtac ballI 1);
   322 by (rtac beta 1);
   323 by (assume_tac 1);
   324 by (rewtac increasing_def);
   325 by (rtac CollectI 1);
   326 by (rtac lam_type 1);
   327 (*Verify that it increases*)
   328 by (rtac allI 2);
   329 by (rtac impI 2);
   330 by (asm_simp_tac (simpset() addsimps [Pow_iff, subset_consI, subset_refl]) 2);
   331 (*Type checking is surprisingly hard!*)
   332 by (asm_simp_tac
   333     (simpset() addsimps [Pow_iff, cons_subset_iff, subset_refl]) 1);
   334 by (blast_tac (claset() addSIs [choice_Diff RS DiffD1]) 1);
   335 qed "Zermelo_next_exists";
   336 
   337 
   338 (*The construction of the injection*)
   339 Goal "[| ch: (PROD X: Pow(S)-{0}. X);                 \
   340 \        next: increasing(S);                         \
   341 \        ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |] \
   342 \     ==> (lam x:S. Union({y: TFin(S,next). x~: y}))       \
   343 \              : inj(S, TFin(S,next) - {S})";
   344 by (res_inst_tac [("d", "%y. ch`(S-y)")] lam_injective 1);
   345 by (rtac DiffI 1);
   346 by (resolve_tac [Collect_subset RS TFin_UnionI] 1);
   347 by (blast_tac (claset() addSIs [Collect_subset RS TFin_UnionI]
   348                       addEs [equalityE]) 1);
   349 by (subgoal_tac "x ~: Union({y: TFin(S,next). x~: y})" 1);
   350 by (blast_tac (claset() addEs [equalityE]) 2);
   351 by (subgoal_tac "Union({y: TFin(S,next). x~: y}) ~= S" 1);
   352 by (blast_tac (claset() addEs [equalityE]) 2);
   353 (*For proving x : next`Union(...);
   354   Abrial & Laffitte's justification appears to be faulty.*)
   355 by (subgoal_tac "~ next ` Union({y: TFin(S,next). x~: y}) <= \
   356 \                  Union({y: TFin(S,next). x~: y})" 1);
   357 by (asm_simp_tac 
   358     (simpset() delsimps [Union_iff]
   359               addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
   360                      Pow_iff, cons_subset_iff, subset_refl,
   361                      choice_Diff RS DiffD2]) 2);
   362 by (subgoal_tac "x : next ` Union({y: TFin(S,next). x~: y})" 1);
   363 by (blast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2);
   364 (*End of the lemmas!*)
   365 by (asm_full_simp_tac 
   366     (simpset() addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
   367                      Pow_iff, cons_subset_iff, subset_refl]) 1);
   368 by (REPEAT (eresolve_tac [asm_rl, consE, sym, notE] 1));
   369 qed "choice_imp_injection";
   370 
   371 (*The wellordering theorem*)
   372 Goal "EX r. well_ord(S,r)";
   373 by (rtac (AC_Pi_Pow RS exE) 1);
   374 by (rtac (Zermelo_next_exists RS bexE) 1);
   375 by (assume_tac 1);
   376 by (rtac exI 1);
   377 by (rtac well_ord_rvimage 1);
   378 by (etac well_ord_TFin 2);
   379 by (resolve_tac [choice_imp_injection RS inj_weaken_type] 1);
   380 by (REPEAT (ares_tac [Diff_subset] 1));
   381 qed "AC_well_ord";