src/HOL/Real/Hyperreal/Zorn.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 8856 435187ffc64e
child 9188 379b0c3f7c85
permissions -rw-r--r--
bind_thm(s);
     1 (*  Title       : Zorn.ML
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML
     6 *) 
     7 
     8 (*---------------------------------------------------------------
     9       Section 1.  Mathematical Preamble 
    10  ---------------------------------------------------------------*)
    11 
    12 Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
    13 by (Blast_tac 1);
    14 qed "Union_lemma0";
    15 
    16 (*-- similar to subset_cs in ZF/subset.thy --*)
    17 bind_thms ("thissubset_SIs",
    18     [subset_refl,Union_least, UN_least, Un_least, 
    19      Inter_greatest, Int_greatest,
    20      Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
    21 
    22 
    23 (*A claset for subset reasoning*)
    24 val thissubset_cs = claset() 
    25     delrules [subsetI, subsetCE]
    26     addSIs thissubset_SIs
    27     addIs  [Union_upper, Inter_lower];
    28 
    29 (* increasingD2 of ZF/Zorn.ML *) 
    30 Goalw [succ_def] "x <= succ S x";
    31 by (rtac (expand_if RS iffD2) 1);
    32 by (auto_tac (claset(),simpset() addsimps [super_def,
    33                maxchain_def,psubset_def]));
    34 by (rtac swap 1 THEN assume_tac 1);
    35 by (rtac selectI2 1);
    36 by (ALLGOALS(Blast_tac));
    37 qed "Abrial_axiom1";
    38 
    39 val [TFin_succI, Pow_TFin_UnionI] = TFin.intrs;
    40 val TFin_UnionI = PowI RS Pow_TFin_UnionI;
    41 bind_thm ("TFin_succI", TFin_succI);
    42 bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI);
    43 bind_thm ("TFin_UnionI", TFin_UnionI);
    44 
    45 val major::prems = Goal  
    46           "[| n : TFin S; \
    47 \            !!x. [| x: TFin S; P(x) |] ==> P(succ S x); \
    48 \            !!Y. [| Y <= TFin S; Ball Y P |] ==> P(Union Y) |] \
    49 \         ==> P(n)";
    50 by (rtac (major RS TFin.induct) 1);
    51 by (ALLGOALS (fast_tac (claset() addIs prems)));
    52 qed "TFin_induct";
    53 
    54 (*Perform induction on n, then prove the major premise using prems. *)
    55 fun TFin_ind_tac a prems i = 
    56     EVERY [res_inst_tac [("n",a)] TFin_induct i,
    57            rename_last_tac a ["1"] (i+1),
    58            rename_last_tac a ["2"] (i+2),
    59            ares_tac prems i];
    60 
    61 Goal "x <= y ==> x <= succ S y";
    62 by (etac (Abrial_axiom1 RSN (2,subset_trans)) 1);
    63 qed "succ_trans";
    64 
    65 (*Lemma 1 of section 3.1*)
    66 Goal "[| n: TFin S;  m: TFin S;  \
    67 \        ALL x: TFin S. x <= m --> x = m | succ S x <= m \
    68 \     |] ==> n <= m | succ S m <= n";
    69 by (etac TFin_induct 1);
    70 by (etac Union_lemma0 2);               (*or just Blast_tac*)
    71 by (blast_tac (thissubset_cs addIs [succ_trans]) 1);
    72 qed "TFin_linear_lemma1";
    73 
    74 (* Lemma 2 of section 3.2 *)
    75 Goal "m: TFin S ==> ALL n: TFin S. n<=m --> n=m | succ S n<=m";
    76 by (etac TFin_induct 1);
    77 by (rtac (impI RS ballI) 1);
    78 (*case split using TFin_linear_lemma1*)
    79 by (res_inst_tac [("n1","n"), ("m1","x")] 
    80     (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    81 by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1);
    82 by (blast_tac (thissubset_cs addIs [succ_trans]) 1);
    83 by (REPEAT (ares_tac [disjI1,equalityI] 1));
    84 (*second induction step*)
    85 by (rtac (impI RS ballI) 1);
    86 by (rtac (Union_lemma0 RS disjE) 1);
    87 by (rtac disjI2 3);
    88 by (REPEAT (ares_tac [disjI1,equalityI] 2));
    89 by (rtac ballI 1);
    90 by (ball_tac 1);
    91 by (set_mp_tac 1);
    92 by (res_inst_tac [("n1","n"), ("m1","x")] 
    93     (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    94 by (blast_tac thissubset_cs 1);
    95 by (rtac (Abrial_axiom1 RS subset_trans RS disjI1) 1);
    96 by (assume_tac 1);
    97 qed "TFin_linear_lemma2";
    98 
    99 (*a more convenient form for Lemma 2*)
   100 Goal "[| n<=m;  m: TFin S;  n: TFin S |] ==> n=m | succ S n<=m";
   101 by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1);
   102 by (REPEAT (assume_tac 1));
   103 qed "TFin_subsetD";
   104 
   105 (*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
   106 Goal "[| m: TFin S;  n: TFin S|] ==> n<=m | m<=n";
   107 by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1);
   108 by (REPEAT (assume_tac 1) THEN etac disjI2 1);
   109 by (blast_tac (thissubset_cs addIs [Abrial_axiom1 RS subset_trans]) 1);
   110 qed "TFin_subset_linear";
   111 
   112 (*Lemma 3 of section 3.3*)
   113 Goal "[| n: TFin S;  m: TFin S;  m = succ S m |] ==> n<=m";
   114 by (etac TFin_induct 1);
   115 by (dtac TFin_subsetD 1);
   116 by (REPEAT (assume_tac 1));
   117 by (fast_tac (claset() addEs [ssubst]) 1);
   118 by (blast_tac (thissubset_cs) 1);
   119 qed "eq_succ_upper";
   120 
   121 (*Property 3.3 of section 3.3*)
   122 Goal "m: TFin S ==> (m = succ S m) = (m = Union(TFin S))";
   123 by (rtac iffI 1);
   124 by (rtac (Union_upper RS equalityI) 1);
   125 by (rtac (eq_succ_upper RS Union_least) 2);
   126 by (REPEAT (assume_tac 1));
   127 by (etac ssubst 1);
   128 by (rtac (Abrial_axiom1 RS equalityI) 1);
   129 by (blast_tac (thissubset_cs addIs [TFin_UnionI, TFin_succI]) 1);
   130 qed "equal_succ_Union";
   131 
   132 (*-------------------------------------------------------------------------
   133     Section 4.  Hausdorff's Theorem: every set contains a maximal chain 
   134     NB: We assume the partial ordering is <=, the subset relation! 
   135  -------------------------------------------------------------------------*)
   136 
   137 Goalw [chain_def] "({} :: 'a set set) : chain S";
   138 by (Auto_tac);
   139 qed "empty_set_mem_chain";
   140 
   141 Goalw [super_def] "super S c <= chain S";
   142 by (Fast_tac 1);
   143 qed "super_subset_chain";
   144 
   145 Goalw [maxchain_def] "maxchain S <= chain S";
   146 by (Fast_tac 1);
   147 qed "maxchain_subset_chain";
   148 
   149 Goalw [succ_def] "c ~: chain S ==> succ S c = c";
   150 by (fast_tac (claset() addSIs [if_P]) 1);
   151 qed "succI1";
   152 
   153 Goalw [succ_def] "c: maxchain S ==> succ S c = c";
   154 by (fast_tac (claset() addSIs [if_P]) 1);
   155 qed "succI2";
   156 
   157 Goalw [succ_def] "c: chain S - maxchain S ==> \
   158 \                         succ S c = (@c'. c': super S c)";
   159 by (fast_tac (claset() addSIs [if_not_P]) 1);
   160 qed "succI3";
   161 
   162 Goal "c: chain S - maxchain S ==> ? d. d: super S c";
   163 by (rewrite_goals_tac [super_def,maxchain_def]);
   164 by (Auto_tac);
   165 qed "mem_super_Ex";
   166 
   167 Goal "c: chain S - maxchain S ==> \
   168 \                         (@c'. c': super S c): super S c";
   169 by (etac (mem_super_Ex RS exE) 1);
   170 by (rtac selectI2 1);
   171 by (Auto_tac);
   172 qed "select_super";
   173 
   174 Goal "c: chain S - maxchain S ==> \
   175 \                         (@c'. c': super S c) ~= c";
   176 by (rtac notI 1);
   177 by (dtac select_super 1);
   178 by (asm_full_simp_tac (simpset() addsimps [super_def,psubset_def]) 1);
   179 qed "select_not_equals";
   180 
   181 Goal "c: chain S - maxchain S ==> \
   182 \                         succ S c ~= c";
   183 by (ftac succI3 1);
   184 by (Asm_simp_tac 1);
   185 by (rtac select_not_equals 1);
   186 by (assume_tac 1);
   187 qed "succ_not_equals";
   188 
   189 Goal "c: TFin S ==> (c :: 'a set set): chain S";
   190 by (etac TFin_induct 1);
   191 by (asm_simp_tac (simpset() addsimps [succ_def,
   192     select_super RS (super_subset_chain RS subsetD)]
   193                    setloop split_tac [expand_if]) 1);
   194 by (rewtac chain_def);
   195 by (rtac CollectI 1);
   196 by Safe_tac;
   197 by (dtac bspec 1 THEN assume_tac 1);
   198 by (res_inst_tac  [("m1","Xa"), ("n1","X")] (TFin_subset_linear RS disjE) 2);
   199 by (ALLGOALS(Blast_tac));
   200 qed "TFin_chain_lemm4";
   201  
   202 Goal "EX c. (c :: 'a set set): maxchain S";
   203 by (res_inst_tac [("x", "Union(TFin S)")] exI 1);
   204 by (rtac classical 1);
   205 by (subgoal_tac "succ S (Union(TFin S)) = Union(TFin S)" 1);
   206 by (resolve_tac [equal_succ_Union RS iffD2 RS sym] 2);
   207 by (resolve_tac [subset_refl RS TFin_UnionI] 2);
   208 by (rtac refl 2);
   209 by (cut_facts_tac [subset_refl RS TFin_UnionI RS TFin_chain_lemm4] 1);
   210 by (dtac (DiffI RS succ_not_equals) 1);
   211 by (ALLGOALS(Blast_tac));
   212 qed "Hausdorff";
   213 
   214 
   215 (*---------------------------------------------------------------
   216   Section 5.  Zorn's Lemma: if all chains have upper bounds 
   217                                there is  a maximal element 
   218  ----------------------------------------------------------------*)
   219 Goalw [chain_def]
   220     "[| c: chain S; z: S; \
   221 \             ALL x:c. x<=(z:: 'a set) |] ==> {z} Un c : chain S";
   222 by (Blast_tac 1);
   223 qed "chain_extend";
   224 
   225 Goalw [chain_def] "[| c: chain S; x: c |] ==> x <= Union(c)";
   226 by (Auto_tac);
   227 qed "chain_Union_upper";
   228 
   229 Goalw [chain_def] "c: chain S ==> ! x: c. x <= Union(c)";
   230 by (Auto_tac);
   231 qed "chain_ball_Union_upper";
   232 
   233 Goal "[| c: maxchain S; u: S; Union(c) <= u |] ==> Union(c) = u";
   234 by (rtac ccontr 1);
   235 by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1);
   236 by (etac conjE 1);
   237 by (subgoal_tac "({u} Un c): super S c" 1);
   238 by (Asm_full_simp_tac 1);
   239 by (rewrite_tac [super_def,psubset_def]);
   240 by Safe_tac;
   241 by (fast_tac (claset() addEs [chain_extend]) 1);
   242 by (subgoal_tac "u ~: c" 1);
   243 by (blast_tac (claset() addEs [equalityE]) 1);
   244 by (blast_tac (claset() addDs [chain_Union_upper]) 1);
   245 qed "maxchain_Zorn";
   246 
   247 Goal "ALL c: chain S. Union(c): S ==> \
   248 \     EX y: S. ALL z: S. y <= z --> y = z";
   249 by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1);
   250 by (etac exE 1);
   251 by (dtac subsetD 1 THEN assume_tac 1);
   252 by (dtac bspec 1 THEN assume_tac 1);
   253 by (res_inst_tac [("x","Union(c)")] bexI 1);
   254 by (rtac ballI 1 THEN rtac impI 1);
   255 by (blast_tac (claset() addSDs [maxchain_Zorn]) 1);
   256 by (assume_tac 1);
   257 qed "Zorn_Lemma";
   258 
   259 (*-------------------------------------------------------------
   260              Alternative version of Zorn's Lemma
   261  --------------------------------------------------------------*)
   262 Goal "ALL (c:: 'a set set): chain S. EX y : S. ALL x : c. x <= y ==> \
   263 \     EX y : S. ALL x : S. (y :: 'a set) <= x --> y = x";
   264 by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1);
   265 by (EVERY1[etac exE, dtac subsetD, assume_tac]);
   266 by (EVERY1[dtac bspec, assume_tac, etac bexE]);
   267 by (res_inst_tac [("x","y")] bexI 1);
   268 by (assume_tac 2);
   269 by (EVERY1[rtac ballI, rtac impI, rtac ccontr]);
   270 by (forw_inst_tac [("z","x")]  chain_extend 1);
   271 by (assume_tac 1 THEN Blast_tac 1);
   272 by (rewrite_tac [maxchain_def,super_def,psubset_def]);
   273 by (Step_tac 1);
   274 by (eres_inst_tac [("c","{x} Un c")] equalityCE 1);
   275 by (Step_tac 1);
   276 by (subgoal_tac "x ~: c" 1);
   277 by (blast_tac (claset() addEs [equalityE]) 1);
   278 by (Blast_tac 1);
   279 qed "Zorn_Lemma2";
   280 
   281 (** misc. lemmas **)
   282 
   283 Goalw [chain_def] "[| c : chain S; x: c; y: c |] ==> x <= y | y <= x";
   284 by (Blast_tac 1);
   285 qed "chainD";
   286 
   287 Goalw [chain_def] "!!(c :: 'a set set). c: chain S ==> c <= S";
   288 by (Blast_tac 1);
   289 qed "chainD2";
   290 
   291 (* proved elsewhere? *) 
   292 Goal "x : Union(c) ==> EX m:c. x:m";
   293 by (Blast_tac 1);
   294 qed "mem_UnionD";