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";
```