converted Hyperreal/Zorn to Isar format and moved to Library
authorpaulson
Sat Aug 31 14:03:49 2002 +0200 (2002-08-31)
changeset 13551b7f64ee8da84
parent 13550 5a176b8dda84
child 13552 83d674e8cd2a
converted Hyperreal/Zorn to Isar format and moved to Library
src/HOL/Hyperreal/Filter.ML
src/HOL/Hyperreal/Zorn.ML
src/HOL/Hyperreal/Zorn.thy
src/HOL/IsaMakefile
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Hyperreal/Filter.ML	Fri Aug 30 16:42:45 2002 +0200
     1.2 +++ b/src/HOL/Hyperreal/Filter.ML	Sat Aug 31 14:03:49 2002 +0200
     1.3 @@ -5,6 +5,12 @@
     1.4      Description : Filters and Ultrafilter
     1.5  *) 
     1.6  
     1.7 +(*ML bindings for Library/Zorn theorems*)
     1.8 +val chain_def = thm "chain_def";
     1.9 +val chainD = thm "chainD";
    1.10 +val chainD2 = thm "chainD2";
    1.11 +val Zorn_Lemma2 = thm "Zorn_Lemma2";
    1.12 +
    1.13  (*------------------------------------------------------------------
    1.14        Properties of Filters and Freefilters - 
    1.15        rules for intro, destruction etc.
     2.1 --- a/src/HOL/Hyperreal/Zorn.ML	Fri Aug 30 16:42:45 2002 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,285 +0,0 @@
     2.4 -(*  Title       : Zorn.ML
     2.5 -    ID          : $Id$
     2.6 -    Author      : Jacques D. Fleuriot
     2.7 -    Copyright   : 1998  University of Cambridge
     2.8 -    Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML
     2.9 -*) 
    2.10 -
    2.11 -(*---------------------------------------------------------------
    2.12 -      Section 1.  Mathematical Preamble 
    2.13 - ---------------------------------------------------------------*)
    2.14 -
    2.15 -Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
    2.16 -by (Blast_tac 1);
    2.17 -qed "Union_lemma0";
    2.18 -
    2.19 -(*-- similar to subset_cs in ZF/subset.thy --*)
    2.20 -bind_thms ("thissubset_SIs",
    2.21 -    [subset_refl,Union_least, UN_least, Un_least, 
    2.22 -     Inter_greatest, Int_greatest,
    2.23 -     Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
    2.24 -
    2.25 -
    2.26 -(*A claset for subset reasoning*)
    2.27 -val thissubset_cs = claset() 
    2.28 -    delrules [subsetI, subsetCE]
    2.29 -    addSIs thissubset_SIs
    2.30 -    addIs  [Union_upper, Inter_lower];
    2.31 -
    2.32 -(* increasingD2 of ZF/Zorn.ML *) 
    2.33 -Goalw [succ_def] "x <= succ S x";
    2.34 -by (rtac (split_if RS iffD2) 1);
    2.35 -by (auto_tac (claset(),simpset() addsimps [super_def,
    2.36 -               maxchain_def,psubset_def]));
    2.37 -by (rtac swap 1 THEN assume_tac 1);
    2.38 -by (rtac someI2 1);
    2.39 -by (ALLGOALS(Blast_tac));
    2.40 -qed "Abrial_axiom1";
    2.41 -
    2.42 -val [TFin_succI, Pow_TFin_UnionI] = TFin.intrs;
    2.43 -val TFin_UnionI = PowI RS Pow_TFin_UnionI;
    2.44 -bind_thm ("TFin_succI", TFin_succI);
    2.45 -bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI);
    2.46 -bind_thm ("TFin_UnionI", TFin_UnionI);
    2.47 -
    2.48 -val major::prems = Goal  
    2.49 -          "[| n : TFin S; \
    2.50 -\            !!x. [| x: TFin S; P(x) |] ==> P(succ S x); \
    2.51 -\            !!Y. [| Y <= TFin S; Ball Y P |] ==> P(Union Y) |] \
    2.52 -\         ==> P(n)";
    2.53 -by (rtac (major RS TFin.induct) 1);
    2.54 -by (ALLGOALS (fast_tac (claset() addIs prems)));
    2.55 -qed "TFin_induct";
    2.56 -
    2.57 -(*Perform induction on n, then prove the major premise using prems. *)
    2.58 -fun TFin_ind_tac a prems i = 
    2.59 -    EVERY [induct_thm_tac TFin_induct a i,
    2.60 -           rename_last_tac a ["1"] (i+1),
    2.61 -           rename_last_tac a ["2"] (i+2),
    2.62 -           ares_tac prems i];
    2.63 -
    2.64 -Goal "x <= y ==> x <= succ S y";
    2.65 -by (etac (Abrial_axiom1 RSN (2,subset_trans)) 1);
    2.66 -qed "succ_trans";
    2.67 -
    2.68 -(*Lemma 1 of section 3.1*)
    2.69 -Goal "[| n: TFin S;  m: TFin S;  \
    2.70 -\        ALL x: TFin S. x <= m --> x = m | succ S x <= m \
    2.71 -\     |] ==> n <= m | succ S m <= n";
    2.72 -by (etac TFin_induct 1);
    2.73 -by (etac Union_lemma0 2);               (*or just Blast_tac*)
    2.74 -by (blast_tac (thissubset_cs addIs [succ_trans]) 1);
    2.75 -qed "TFin_linear_lemma1";
    2.76 -
    2.77 -(* Lemma 2 of section 3.2 *)
    2.78 -Goal "m: TFin S ==> ALL n: TFin S. n<=m --> n=m | succ S n<=m";
    2.79 -by (etac TFin_induct 1);
    2.80 -by (rtac (impI RS ballI) 1);
    2.81 -(*case split using TFin_linear_lemma1*)
    2.82 -by (res_inst_tac [("n1","n"), ("m1","x")] 
    2.83 -    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    2.84 -by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1);
    2.85 -by (blast_tac (thissubset_cs addIs [succ_trans]) 1);
    2.86 -by (REPEAT (ares_tac [disjI1,equalityI] 1));
    2.87 -(*second induction step*)
    2.88 -by (rtac (impI RS ballI) 1);
    2.89 -by (rtac (Union_lemma0 RS disjE) 1);
    2.90 -by (rtac disjI2 3);
    2.91 -by (REPEAT (ares_tac [disjI1,equalityI] 2));
    2.92 -by (rtac ballI 1);
    2.93 -by (ball_tac 1);
    2.94 -by (set_mp_tac 1);
    2.95 -by (res_inst_tac [("n1","n"), ("m1","x")] 
    2.96 -    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
    2.97 -by (blast_tac thissubset_cs 1);
    2.98 -by (rtac (Abrial_axiom1 RS subset_trans RS disjI1) 1);
    2.99 -by (assume_tac 1);
   2.100 -qed "TFin_linear_lemma2";
   2.101 -
   2.102 -(*a more convenient form for Lemma 2*)
   2.103 -Goal "[| n<=m;  m: TFin S;  n: TFin S |] ==> n=m | succ S n<=m";
   2.104 -by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1);
   2.105 -by (REPEAT (assume_tac 1));
   2.106 -qed "TFin_subsetD";
   2.107 -
   2.108 -(*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
   2.109 -Goal "[| m: TFin S;  n: TFin S|] ==> n<=m | m<=n";
   2.110 -by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1);
   2.111 -by (REPEAT (assume_tac 1) THEN etac disjI2 1);
   2.112 -by (blast_tac (thissubset_cs addIs [Abrial_axiom1 RS subset_trans]) 1);
   2.113 -qed "TFin_subset_linear";
   2.114 -
   2.115 -(*Lemma 3 of section 3.3*)
   2.116 -Goal "[| n: TFin S;  m: TFin S;  m = succ S m |] ==> n<=m";
   2.117 -by (etac TFin_induct 1);
   2.118 -by (dtac TFin_subsetD 1);
   2.119 -by (REPEAT (assume_tac 1));
   2.120 -by (fast_tac (claset() addEs [ssubst]) 1);
   2.121 -by (blast_tac (thissubset_cs) 1);
   2.122 -qed "eq_succ_upper";
   2.123 -
   2.124 -(*Property 3.3 of section 3.3*)
   2.125 -Goal "m: TFin S ==> (m = succ S m) = (m = Union(TFin S))";
   2.126 -by (rtac iffI 1);
   2.127 -by (rtac (Union_upper RS equalityI) 1);
   2.128 -by (rtac (eq_succ_upper RS Union_least) 2);
   2.129 -by (REPEAT (assume_tac 1));
   2.130 -by (etac ssubst 1);
   2.131 -by (rtac (Abrial_axiom1 RS equalityI) 1);
   2.132 -by (blast_tac (thissubset_cs addIs [TFin_UnionI, TFin_succI]) 1);
   2.133 -qed "equal_succ_Union";
   2.134 -
   2.135 -(*-------------------------------------------------------------------------
   2.136 -    Section 4.  Hausdorff's Theorem: every set contains a maximal chain 
   2.137 -    NB: We assume the partial ordering is <=, the subset relation! 
   2.138 - -------------------------------------------------------------------------*)
   2.139 -
   2.140 -Goalw [chain_def] "({} :: 'a set set) : chain S";
   2.141 -by (Auto_tac);
   2.142 -qed "empty_set_mem_chain";
   2.143 -
   2.144 -Goalw [super_def] "super S c <= chain S";
   2.145 -by (Fast_tac 1);
   2.146 -qed "super_subset_chain";
   2.147 -
   2.148 -Goalw [maxchain_def] "maxchain S <= chain S";
   2.149 -by (Fast_tac 1);
   2.150 -qed "maxchain_subset_chain";
   2.151 -
   2.152 -Goalw [succ_def] "c ~: chain S ==> succ S c = c";
   2.153 -by (fast_tac (claset() addSIs [if_P]) 1);
   2.154 -qed "succI1";
   2.155 -
   2.156 -Goalw [succ_def] "c: maxchain S ==> succ S c = c";
   2.157 -by (fast_tac (claset() addSIs [if_P]) 1);
   2.158 -qed "succI2";
   2.159 -
   2.160 -Goalw [succ_def] "c: chain S - maxchain S ==> \
   2.161 -\                         succ S c = (@c'. c': super S c)";
   2.162 -by (fast_tac (claset() addSIs [if_not_P]) 1);
   2.163 -qed "succI3";
   2.164 -
   2.165 -Goal "c: chain S - maxchain S ==> ? d. d: super S c";
   2.166 -by (rewrite_goals_tac [super_def,maxchain_def]);
   2.167 -by (Auto_tac);
   2.168 -qed "mem_super_Ex";
   2.169 -
   2.170 -Goal "c: chain S - maxchain S ==> \
   2.171 -\                         (@c'. c': super S c): super S c";
   2.172 -by (etac (mem_super_Ex RS exE) 1);
   2.173 -by (rtac someI2 1);
   2.174 -by (Auto_tac);
   2.175 -qed "select_super";
   2.176 -
   2.177 -Goal "c: chain S - maxchain S ==> \
   2.178 -\                         (@c'. c': super S c) ~= c";
   2.179 -by (rtac notI 1);
   2.180 -by (dtac select_super 1);
   2.181 -by (asm_full_simp_tac (simpset() addsimps [super_def,psubset_def]) 1);
   2.182 -qed "select_not_equals";
   2.183 -
   2.184 -Goal "c: chain S - maxchain S ==> \
   2.185 -\                         succ S c ~= c";
   2.186 -by (ftac succI3 1);
   2.187 -by (Asm_simp_tac 1);
   2.188 -by (rtac select_not_equals 1);
   2.189 -by (assume_tac 1);
   2.190 -qed "succ_not_equals";
   2.191 -
   2.192 -Goal "c: TFin S ==> (c :: 'a set set): chain S";
   2.193 -by (etac TFin_induct 1);
   2.194 -by (asm_simp_tac (simpset() addsimps [succ_def,
   2.195 -    select_super RS (super_subset_chain RS subsetD)]
   2.196 -                   addsplits [split_if]) 1);
   2.197 -by (rewtac chain_def);
   2.198 -by (rtac CollectI 1);
   2.199 -by Safe_tac;
   2.200 -by (dtac bspec 1 THEN assume_tac 1);
   2.201 -by (res_inst_tac  [("m1","Xa"), ("n1","X")] (TFin_subset_linear RS disjE) 2);
   2.202 -by (ALLGOALS(Blast_tac));
   2.203 -qed "TFin_chain_lemm4";
   2.204 - 
   2.205 -Goal "EX c. (c :: 'a set set): maxchain S";
   2.206 -by (res_inst_tac [("x", "Union(TFin S)")] exI 1);
   2.207 -by (rtac classical 1);
   2.208 -by (subgoal_tac "succ S (Union(TFin S)) = Union(TFin S)" 1);
   2.209 -by (resolve_tac [equal_succ_Union RS iffD2 RS sym] 2);
   2.210 -by (resolve_tac [subset_refl RS TFin_UnionI] 2);
   2.211 -by (rtac refl 2);
   2.212 -by (cut_facts_tac [subset_refl RS TFin_UnionI RS TFin_chain_lemm4] 1);
   2.213 -by (dtac (DiffI RS succ_not_equals) 1);
   2.214 -by (ALLGOALS(Blast_tac));
   2.215 -qed "Hausdorff";
   2.216 -
   2.217 -
   2.218 -(*---------------------------------------------------------------
   2.219 -  Section 5.  Zorn's Lemma: if all chains have upper bounds 
   2.220 -                               there is  a maximal element 
   2.221 - ----------------------------------------------------------------*)
   2.222 -Goalw [chain_def]
   2.223 -    "[| c: chain S; z: S; \
   2.224 -\             ALL x:c. x<=(z:: 'a set) |] ==> {z} Un c : chain S";
   2.225 -by (Blast_tac 1);
   2.226 -qed "chain_extend";
   2.227 -
   2.228 -Goalw [chain_def] "[| c: chain S; x: c |] ==> x <= Union(c)";
   2.229 -by (Auto_tac);
   2.230 -qed "chain_Union_upper";
   2.231 -
   2.232 -Goalw [chain_def] "c: chain S ==> ! x: c. x <= Union(c)";
   2.233 -by (Auto_tac);
   2.234 -qed "chain_ball_Union_upper";
   2.235 -
   2.236 -Goal "[| c: maxchain S; u: S; Union(c) <= u |] ==> Union(c) = u";
   2.237 -by (rtac ccontr 1);
   2.238 -by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1);
   2.239 -by (etac conjE 1);
   2.240 -by (subgoal_tac "({u} Un c): super S c" 1);
   2.241 -by (Asm_full_simp_tac 1);
   2.242 -by (rewrite_tac [super_def,psubset_def]);
   2.243 -by (blast_tac (claset() addIs [chain_extend] addDs [chain_Union_upper]) 1);
   2.244 -qed "maxchain_Zorn";
   2.245 -
   2.246 -Goal "ALL c: chain S. Union(c): S ==> \
   2.247 -\     EX y: S. ALL z: S. y <= z --> y = z";
   2.248 -by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1);
   2.249 -by (etac exE 1);
   2.250 -by (dtac subsetD 1 THEN assume_tac 1);
   2.251 -by (dtac bspec 1 THEN assume_tac 1);
   2.252 -by (res_inst_tac [("x","Union(c)")] bexI 1);
   2.253 -by (rtac ballI 1 THEN rtac impI 1);
   2.254 -by (blast_tac (claset() addSDs [maxchain_Zorn]) 1);
   2.255 -by (assume_tac 1);
   2.256 -qed "Zorn_Lemma";
   2.257 -
   2.258 -(*-------------------------------------------------------------
   2.259 -             Alternative version of Zorn's Lemma
   2.260 - --------------------------------------------------------------*)
   2.261 -Goal "ALL (c:: 'a set set): chain S. EX y : S. ALL x : c. x <= y ==> \
   2.262 -\     EX y : S. ALL x : S. (y :: 'a set) <= x --> y = x";
   2.263 -by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1);
   2.264 -by (EVERY1[etac exE, dtac subsetD, assume_tac]);
   2.265 -by (EVERY1[dtac bspec, assume_tac, etac bexE]);
   2.266 -by (res_inst_tac [("x","y")] bexI 1);
   2.267 -by (assume_tac 2);
   2.268 -by (EVERY1[rtac ballI, rtac impI, rtac ccontr]);
   2.269 -by (forw_inst_tac [("z","x")]  chain_extend 1);
   2.270 -by (assume_tac 1 THEN Blast_tac 1);
   2.271 -by (rewrite_tac [maxchain_def,super_def,psubset_def]);
   2.272 -by (blast_tac (claset() addSEs [equalityCE]) 1);
   2.273 -qed "Zorn_Lemma2";
   2.274 -
   2.275 -(** misc. lemmas **)
   2.276 -
   2.277 -Goalw [chain_def] "[| c : chain S; x: c; y: c |] ==> x <= y | y <= x";
   2.278 -by (Blast_tac 1);
   2.279 -qed "chainD";
   2.280 -
   2.281 -Goalw [chain_def] "!!(c :: 'a set set). c: chain S ==> c <= S";
   2.282 -by (Blast_tac 1);
   2.283 -qed "chainD2";
   2.284 -
   2.285 -(* proved elsewhere? *) 
   2.286 -Goal "x : Union(c) ==> EX m:c. x:m";
   2.287 -by (Blast_tac 1);
   2.288 -qed "mem_UnionD";
     3.1 --- a/src/HOL/Hyperreal/Zorn.thy	Fri Aug 30 16:42:45 2002 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,34 +0,0 @@
     3.4 -(*  Title       : Zorn.thy
     3.5 -    ID          : $Id$
     3.6 -    Author      : Jacques D. Fleuriot
     3.7 -    Copyright   : 1998  University of Cambridge
     3.8 -    Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
     3.9 -*) 
    3.10 -
    3.11 -Zorn = Main +
    3.12 -
    3.13 -constdefs
    3.14 -  chain     ::  'a::ord set => 'a set set
    3.15 -    "chain S  == {F. F <= S & (ALL x: F. ALL y: F. x <= y | y <= x)}" 
    3.16 -
    3.17 -  super     ::  ['a::ord set,'a set] => 'a set set
    3.18 -    "super S c == {d. d: chain(S) & c < d}"
    3.19 -
    3.20 -  maxchain  ::  'a::ord set => 'a set set
    3.21 -    "maxchain S == {c. c: chain S & super S c = {}}"
    3.22 -
    3.23 -  succ      ::  ['a::ord set,'a set] => 'a set
    3.24 -    "succ S c == if (c ~: chain S| c: maxchain S) 
    3.25 -                 then c else (@c'. c': (super S c))" 
    3.26 -
    3.27 -consts 
    3.28 -  "TFin" :: 'a::ord set => 'a set set
    3.29 -
    3.30 -inductive "TFin(S)"
    3.31 -  intrs
    3.32 -    succI        "x : TFin S ==> succ S x : TFin S"
    3.33 -    Pow_UnionI   "Y : Pow(TFin S) ==> Union(Y) : TFin S"
    3.34 -           
    3.35 -  monos          Pow_mono
    3.36 -end
    3.37 -
     4.1 --- a/src/HOL/IsaMakefile	Fri Aug 30 16:42:45 2002 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Sat Aug 31 14:03:49 2002 +0200
     4.3 @@ -159,6 +159,7 @@
     4.4  HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal
     4.5  
     4.6  $(OUT)/HOL-Hyperreal: $(OUT)/HOL-Real Hyperreal/ROOT.ML\
     4.7 +  Library/Zorn.thy\
     4.8    Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
     4.9    Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
    4.10    Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
    4.11 @@ -176,8 +177,7 @@
    4.12    Hyperreal/Poly.ML Hyperreal/Poly.thy\
    4.13    Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\
    4.14    Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\
    4.15 -  Hyperreal/Transcendental.thy Hyperreal/Zorn.ML Hyperreal/Zorn.thy\
    4.16 -  Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
    4.17 +  Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
    4.18    Hyperreal/hypreal_arith0.ML
    4.19  	@cd Hyperreal; $(ISATOOL) usedir -b $(OUT)/HOL-Real HOL-Hyperreal
    4.20  
    4.21 @@ -203,6 +203,7 @@
    4.22    Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
    4.23    Library/README.html Library/Continuity.thy \
    4.24    Library/Nested_Environment.thy Library/Rational_Numbers.thy \
    4.25 +  Library/Zorn.thy\
    4.26    Library/Library/ROOT.ML Library/Library/document/root.tex \
    4.27    Library/Library/document/root.bib Library/While_Combinator.thy
    4.28  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Zorn.thy	Sat Aug 31 14:03:49 2002 +0200
     5.3 @@ -0,0 +1,263 @@
     5.4 +(*  Title       \<in> Zorn.thy
     5.5 +    ID          \<in> $Id$
     5.6 +    Author      \<in> Jacques D. Fleuriot
     5.7 +    Copyright   \<in> 1998  University of Cambridge
     5.8 +    Description \<in> Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
     5.9 +*) 
    5.10 +
    5.11 +header {*Zorn's Lemma*}
    5.12 +
    5.13 +theory Zorn = Main:
    5.14 +
    5.15 +text{*The lemma and section numbers refer to an unpublished article ``Towards
    5.16 +the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by
    5.17 +Abrial and Laffitte.  *}
    5.18 +
    5.19 +constdefs
    5.20 +  chain     ::  "'a::ord set => 'a set set"
    5.21 +    "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}" 
    5.22 +
    5.23 +  super     ::  "['a::ord set,'a set] => 'a set set"
    5.24 +    "super S c == {d. d \<in> chain(S) & c < d}"
    5.25 +
    5.26 +  maxchain  ::  "'a::ord set => 'a set set"
    5.27 +    "maxchain S == {c. c \<in> chain S & super S c = {}}"
    5.28 +
    5.29 +  succ      ::  "['a::ord set,'a set] => 'a set"
    5.30 +    "succ S c == if (c \<notin> chain S| c \<in> maxchain S) 
    5.31 +                 then c else (@c'. c': (super S c))" 
    5.32 +
    5.33 +consts 
    5.34 +  "TFin" ::  "'a::ord set => 'a set set"
    5.35 +
    5.36 +inductive "TFin(S)"
    5.37 +  intros
    5.38 +    succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    5.39 +    Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    5.40 +           
    5.41 +  monos          Pow_mono
    5.42 +
    5.43 +
    5.44 +subsection{*Mathematical Preamble*}
    5.45 +
    5.46 +lemma Union_lemma0: "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
    5.47 +by blast
    5.48 +
    5.49 +
    5.50 +text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
    5.51 +lemma Abrial_axiom1: "x \<subseteq> succ S x"
    5.52 +apply (unfold succ_def)
    5.53 +apply (rule split_if [THEN iffD2])
    5.54 +apply (auto simp add: super_def maxchain_def psubset_def)
    5.55 +apply (rule swap, assumption)
    5.56 +apply (rule someI2, blast+)
    5.57 +done
    5.58 +
    5.59 +lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
    5.60 +
    5.61 +lemma TFin_induct: 
    5.62 +          "[| n \<in> TFin S;  
    5.63 +             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);  
    5.64 +             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]  
    5.65 +          ==> P(n)"
    5.66 +apply (erule TFin.induct, blast+)
    5.67 +done
    5.68 +
    5.69 +lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
    5.70 +apply (erule subset_trans) 
    5.71 +apply (rule Abrial_axiom1) 
    5.72 +done
    5.73 +
    5.74 +text{*Lemma 1 of section 3.1*}
    5.75 +lemma TFin_linear_lemma1:
    5.76 +     "[| n \<in> TFin S;  m \<in> TFin S;   
    5.77 +         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m  
    5.78 +      |] ==> n \<subseteq> m | succ S m \<subseteq> n"
    5.79 +apply (erule TFin_induct)
    5.80 +apply (erule_tac [2] Union_lemma0) txt{*or just Blast_tac*}
    5.81 +apply (blast del: subsetI intro: succ_trans)
    5.82 +done
    5.83 +
    5.84 +text{* Lemma 2 of section 3.2 *}
    5.85 +lemma TFin_linear_lemma2:
    5.86 +     "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
    5.87 +apply (erule TFin_induct)
    5.88 +apply (rule impI [THEN ballI])
    5.89 +txt{*case split using TFin_linear_lemma1*}
    5.90 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
    5.91 +       assumption+)
    5.92 +apply (drule_tac x = n in bspec, assumption)
    5.93 +apply (blast del: subsetI intro: succ_trans, blast) 
    5.94 +txt{*second induction step*}
    5.95 +apply (rule impI [THEN ballI])
    5.96 +apply (rule Union_lemma0 [THEN disjE])
    5.97 +apply (rule_tac [3] disjI2)
    5.98 + prefer 2 apply blast 
    5.99 +apply (rule ballI)
   5.100 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 
   5.101 +       assumption+, auto) 
   5.102 +apply (blast intro!: Abrial_axiom1 [THEN subsetD])  
   5.103 +done
   5.104 +
   5.105 +text{*Re-ordering the premises of Lemma 2*}
   5.106 +lemma TFin_subsetD:
   5.107 +     "[| n \<subseteq> m;  m \<in> TFin S;  n \<in> TFin S |] ==> n=m | succ S n \<subseteq> m"
   5.108 +apply (rule TFin_linear_lemma2 [rule_format])
   5.109 +apply (assumption+)
   5.110 +done
   5.111 +
   5.112 +text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
   5.113 +lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
   5.114 +apply (rule disjE) 
   5.115 +apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
   5.116 +apply (assumption+, erule disjI2)
   5.117 +apply (blast del: subsetI 
   5.118 +             intro: subsetI Abrial_axiom1 [THEN subset_trans])
   5.119 +done
   5.120 +
   5.121 +text{*Lemma 3 of section 3.3*}
   5.122 +lemma eq_succ_upper: "[| n \<in> TFin S;  m \<in> TFin S;  m = succ S m |] ==> n \<subseteq> m"
   5.123 +apply (erule TFin_induct)
   5.124 +apply (drule TFin_subsetD)
   5.125 +apply (assumption+, force, blast)
   5.126 +done
   5.127 +
   5.128 +text{*Property 3.3 of section 3.3*}
   5.129 +lemma equal_succ_Union: "m \<in> TFin S ==> (m = succ S m) = (m = Union(TFin S))"
   5.130 +apply (rule iffI)
   5.131 +apply (rule Union_upper [THEN equalityI])
   5.132 +apply (rule_tac [2] eq_succ_upper [THEN Union_least])
   5.133 +apply (assumption+)
   5.134 +apply (erule ssubst)
   5.135 +apply (rule Abrial_axiom1 [THEN equalityI])
   5.136 +apply (blast del: subsetI
   5.137 +	     intro: subsetI TFin_UnionI TFin.succI)
   5.138 +done
   5.139 +
   5.140 +subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
   5.141 +
   5.142 +text{*NB: We assume the partial ordering is @{text "\<subseteq>"}, 
   5.143 + the subset relation!*}
   5.144 +
   5.145 +lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
   5.146 +by (unfold chain_def, auto)
   5.147 +
   5.148 +lemma super_subset_chain: "super S c \<subseteq> chain S"
   5.149 +by (unfold super_def, fast)
   5.150 +
   5.151 +lemma maxchain_subset_chain: "maxchain S \<subseteq> chain S"
   5.152 +by (unfold maxchain_def, fast)
   5.153 +
   5.154 +lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
   5.155 +by (unfold super_def maxchain_def, auto)
   5.156 +
   5.157 +lemma select_super: "c \<in> chain S - maxchain S ==>  
   5.158 +                          (@c'. c': super S c): super S c"
   5.159 +apply (erule mem_super_Ex [THEN exE])
   5.160 +apply (rule someI2, auto)
   5.161 +done
   5.162 +
   5.163 +lemma select_not_equals: "c \<in> chain S - maxchain S ==>  
   5.164 +                          (@c'. c': super S c) \<noteq> c"
   5.165 +apply (rule notI)
   5.166 +apply (drule select_super)
   5.167 +apply (simp add: super_def psubset_def)
   5.168 +done
   5.169 +
   5.170 +lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (@c'. c': super S c)"
   5.171 +apply (unfold succ_def)
   5.172 +apply (fast intro!: if_not_P)
   5.173 +done
   5.174 +
   5.175 +lemma succ_not_equals: "c \<in> chain S - maxchain S ==> succ S c \<noteq> c"
   5.176 +apply (frule succI3)
   5.177 +apply (simp (no_asm_simp))
   5.178 +apply (rule select_not_equals, assumption)
   5.179 +done
   5.180 +
   5.181 +lemma TFin_chain_lemma4: "c \<in> TFin S ==> (c :: 'a set set): chain S"
   5.182 +apply (erule TFin_induct)
   5.183 +apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
   5.184 +apply (unfold chain_def)
   5.185 +apply (rule CollectI, safe)
   5.186 +apply (drule bspec, assumption)
   5.187 +apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE], 
   5.188 +       blast+)
   5.189 +done
   5.190 + 
   5.191 +theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
   5.192 +apply (rule_tac x = "Union (TFin S) " in exI)
   5.193 +apply (rule classical)
   5.194 +apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
   5.195 + prefer 2
   5.196 + apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric]) 
   5.197 +apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
   5.198 +apply (drule DiffI [THEN succ_not_equals], blast+)
   5.199 +done
   5.200 +
   5.201 +
   5.202 +subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then 
   5.203 +                               There Is  a Maximal Element*}
   5.204 +
   5.205 +lemma chain_extend: 
   5.206 +    "[| c \<in> chain S; z \<in> S;  
   5.207 +        \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
   5.208 +by (unfold chain_def, blast)
   5.209 +
   5.210 +lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
   5.211 +by (unfold chain_def, auto)
   5.212 +
   5.213 +lemma chain_ball_Union_upper: "c \<in> chain S ==> \<forall>x \<in> c. x \<subseteq> Union(c)"
   5.214 +by (unfold chain_def, auto)
   5.215 +
   5.216 +lemma maxchain_Zorn:
   5.217 +     "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
   5.218 +apply (rule ccontr)
   5.219 +apply (simp add: maxchain_def)
   5.220 +apply (erule conjE)
   5.221 +apply (subgoal_tac " ({u} Un c) \<in> super S c")
   5.222 +apply simp
   5.223 +apply (unfold super_def psubset_def)
   5.224 +apply (blast intro: chain_extend dest: chain_Union_upper)
   5.225 +done
   5.226 +
   5.227 +theorem Zorn_Lemma:
   5.228 +     "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
   5.229 +apply (cut_tac Hausdorff maxchain_subset_chain)
   5.230 +apply (erule exE)
   5.231 +apply (drule subsetD, assumption)
   5.232 +apply (drule bspec, assumption)
   5.233 +apply (rule_tac x = "Union (c) " in bexI)
   5.234 +apply (rule ballI, rule impI)
   5.235 +apply (blast dest!: maxchain_Zorn, assumption)
   5.236 +done
   5.237 +
   5.238 +subsection{*Alternative version of Zorn's Lemma*}
   5.239 +
   5.240 +lemma Zorn_Lemma2:
   5.241 +     "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   5.242 +      ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   5.243 +apply (cut_tac Hausdorff maxchain_subset_chain)
   5.244 +apply (erule exE) 
   5.245 +apply (drule subsetD, assumption) 
   5.246 +apply (drule bspec, assumption, erule bexE) 
   5.247 +apply (rule_tac x = y in bexI)
   5.248 + prefer 2 apply assumption
   5.249 +apply clarify 
   5.250 +apply (rule ccontr) 
   5.251 +apply (frule_tac z = x in chain_extend)
   5.252 +apply (assumption, blast)
   5.253 +apply (unfold maxchain_def super_def psubset_def) 
   5.254 +apply (blast elim!: equalityCE)
   5.255 +done
   5.256 +
   5.257 +text{*Various other lemmas*}
   5.258 +
   5.259 +lemma chainD: "[| c \<in> chain S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
   5.260 +by (unfold chain_def, blast)
   5.261 +
   5.262 +lemma chainD2: "!!(c :: 'a set set). c \<in> chain S ==> c \<subseteq> S"
   5.263 +by (unfold chain_def, blast)
   5.264 +
   5.265 +end
   5.266 +