# HG changeset patch # User paulson # Date 1030795429 -7200 # Node ID b7f64ee8da84b5b0250c7cb2438aa72b5a9fbe71 # Parent 5a176b8dda84308cef08ac7094055da3e7c7d407 converted Hyperreal/Zorn to Isar format and moved to Library diff -r 5a176b8dda84 -r b7f64ee8da84 src/HOL/Hyperreal/Filter.ML --- a/src/HOL/Hyperreal/Filter.ML Fri Aug 30 16:42:45 2002 +0200 +++ b/src/HOL/Hyperreal/Filter.ML Sat Aug 31 14:03:49 2002 +0200 @@ -5,6 +5,12 @@ Description : Filters and Ultrafilter *) +(*ML bindings for Library/Zorn theorems*) +val chain_def = thm "chain_def"; +val chainD = thm "chainD"; +val chainD2 = thm "chainD2"; +val Zorn_Lemma2 = thm "Zorn_Lemma2"; + (*------------------------------------------------------------------ Properties of Filters and Freefilters - rules for intro, destruction etc. diff -r 5a176b8dda84 -r b7f64ee8da84 src/HOL/Hyperreal/Zorn.ML --- a/src/HOL/Hyperreal/Zorn.ML Fri Aug 30 16:42:45 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,285 +0,0 @@ -(* Title : Zorn.ML - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML -*) - -(*--------------------------------------------------------------- - Section 1. Mathematical Preamble - ---------------------------------------------------------------*) - -Goal "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"; -by (Blast_tac 1); -qed "Union_lemma0"; - -(*-- similar to subset_cs in ZF/subset.thy --*) -bind_thms ("thissubset_SIs", - [subset_refl,Union_least, UN_least, Un_least, - Inter_greatest, Int_greatest, - Un_upper1, Un_upper2, Int_lower1, Int_lower2]); - - -(*A claset for subset reasoning*) -val thissubset_cs = claset() - delrules [subsetI, subsetCE] - addSIs thissubset_SIs - addIs [Union_upper, Inter_lower]; - -(* increasingD2 of ZF/Zorn.ML *) -Goalw [succ_def] "x <= succ S x"; -by (rtac (split_if RS iffD2) 1); -by (auto_tac (claset(),simpset() addsimps [super_def, - maxchain_def,psubset_def])); -by (rtac swap 1 THEN assume_tac 1); -by (rtac someI2 1); -by (ALLGOALS(Blast_tac)); -qed "Abrial_axiom1"; - -val [TFin_succI, Pow_TFin_UnionI] = TFin.intrs; -val TFin_UnionI = PowI RS Pow_TFin_UnionI; -bind_thm ("TFin_succI", TFin_succI); -bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI); -bind_thm ("TFin_UnionI", TFin_UnionI); - -val major::prems = Goal - "[| n : TFin S; \ -\ !!x. [| x: TFin S; P(x) |] ==> P(succ S x); \ -\ !!Y. [| Y <= TFin S; Ball Y P |] ==> P(Union Y) |] \ -\ ==> P(n)"; -by (rtac (major RS TFin.induct) 1); -by (ALLGOALS (fast_tac (claset() addIs prems))); -qed "TFin_induct"; - -(*Perform induction on n, then prove the major premise using prems. *) -fun TFin_ind_tac a prems i = - EVERY [induct_thm_tac TFin_induct a i, - rename_last_tac a ["1"] (i+1), - rename_last_tac a ["2"] (i+2), - ares_tac prems i]; - -Goal "x <= y ==> x <= succ S y"; -by (etac (Abrial_axiom1 RSN (2,subset_trans)) 1); -qed "succ_trans"; - -(*Lemma 1 of section 3.1*) -Goal "[| n: TFin S; m: TFin S; \ -\ ALL x: TFin S. x <= m --> x = m | succ S x <= m \ -\ |] ==> n <= m | succ S m <= n"; -by (etac TFin_induct 1); -by (etac Union_lemma0 2); (*or just Blast_tac*) -by (blast_tac (thissubset_cs addIs [succ_trans]) 1); -qed "TFin_linear_lemma1"; - -(* Lemma 2 of section 3.2 *) -Goal "m: TFin S ==> ALL n: TFin S. n<=m --> n=m | succ S n<=m"; -by (etac TFin_induct 1); -by (rtac (impI RS ballI) 1); -(*case split using TFin_linear_lemma1*) -by (res_inst_tac [("n1","n"), ("m1","x")] - (TFin_linear_lemma1 RS disjE) 1 THEN REPEAT (assume_tac 1)); -by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1); -by (blast_tac (thissubset_cs addIs [succ_trans]) 1); -by (REPEAT (ares_tac [disjI1,equalityI] 1)); -(*second induction step*) -by (rtac (impI RS ballI) 1); -by (rtac (Union_lemma0 RS disjE) 1); -by (rtac disjI2 3); -by (REPEAT (ares_tac [disjI1,equalityI] 2)); -by (rtac ballI 1); -by (ball_tac 1); -by (set_mp_tac 1); -by (res_inst_tac [("n1","n"), ("m1","x")] - (TFin_linear_lemma1 RS disjE) 1 THEN REPEAT (assume_tac 1)); -by (blast_tac thissubset_cs 1); -by (rtac (Abrial_axiom1 RS subset_trans RS disjI1) 1); -by (assume_tac 1); -qed "TFin_linear_lemma2"; - -(*a more convenient form for Lemma 2*) -Goal "[| n<=m; m: TFin S; n: TFin S |] ==> n=m | succ S n<=m"; -by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1); -by (REPEAT (assume_tac 1)); -qed "TFin_subsetD"; - -(*Consequences from section 3.3 -- Property 3.2, the ordering is total*) -Goal "[| m: TFin S; n: TFin S|] ==> n<=m | m<=n"; -by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1); -by (REPEAT (assume_tac 1) THEN etac disjI2 1); -by (blast_tac (thissubset_cs addIs [Abrial_axiom1 RS subset_trans]) 1); -qed "TFin_subset_linear"; - -(*Lemma 3 of section 3.3*) -Goal "[| n: TFin S; m: TFin S; m = succ S m |] ==> n<=m"; -by (etac TFin_induct 1); -by (dtac TFin_subsetD 1); -by (REPEAT (assume_tac 1)); -by (fast_tac (claset() addEs [ssubst]) 1); -by (blast_tac (thissubset_cs) 1); -qed "eq_succ_upper"; - -(*Property 3.3 of section 3.3*) -Goal "m: TFin S ==> (m = succ S m) = (m = Union(TFin S))"; -by (rtac iffI 1); -by (rtac (Union_upper RS equalityI) 1); -by (rtac (eq_succ_upper RS Union_least) 2); -by (REPEAT (assume_tac 1)); -by (etac ssubst 1); -by (rtac (Abrial_axiom1 RS equalityI) 1); -by (blast_tac (thissubset_cs addIs [TFin_UnionI, TFin_succI]) 1); -qed "equal_succ_Union"; - -(*------------------------------------------------------------------------- - Section 4. Hausdorff's Theorem: every set contains a maximal chain - NB: We assume the partial ordering is <=, the subset relation! - -------------------------------------------------------------------------*) - -Goalw [chain_def] "({} :: 'a set set) : chain S"; -by (Auto_tac); -qed "empty_set_mem_chain"; - -Goalw [super_def] "super S c <= chain S"; -by (Fast_tac 1); -qed "super_subset_chain"; - -Goalw [maxchain_def] "maxchain S <= chain S"; -by (Fast_tac 1); -qed "maxchain_subset_chain"; - -Goalw [succ_def] "c ~: chain S ==> succ S c = c"; -by (fast_tac (claset() addSIs [if_P]) 1); -qed "succI1"; - -Goalw [succ_def] "c: maxchain S ==> succ S c = c"; -by (fast_tac (claset() addSIs [if_P]) 1); -qed "succI2"; - -Goalw [succ_def] "c: chain S - maxchain S ==> \ -\ succ S c = (@c'. c': super S c)"; -by (fast_tac (claset() addSIs [if_not_P]) 1); -qed "succI3"; - -Goal "c: chain S - maxchain S ==> ? d. d: super S c"; -by (rewrite_goals_tac [super_def,maxchain_def]); -by (Auto_tac); -qed "mem_super_Ex"; - -Goal "c: chain S - maxchain S ==> \ -\ (@c'. c': super S c): super S c"; -by (etac (mem_super_Ex RS exE) 1); -by (rtac someI2 1); -by (Auto_tac); -qed "select_super"; - -Goal "c: chain S - maxchain S ==> \ -\ (@c'. c': super S c) ~= c"; -by (rtac notI 1); -by (dtac select_super 1); -by (asm_full_simp_tac (simpset() addsimps [super_def,psubset_def]) 1); -qed "select_not_equals"; - -Goal "c: chain S - maxchain S ==> \ -\ succ S c ~= c"; -by (ftac succI3 1); -by (Asm_simp_tac 1); -by (rtac select_not_equals 1); -by (assume_tac 1); -qed "succ_not_equals"; - -Goal "c: TFin S ==> (c :: 'a set set): chain S"; -by (etac TFin_induct 1); -by (asm_simp_tac (simpset() addsimps [succ_def, - select_super RS (super_subset_chain RS subsetD)] - addsplits [split_if]) 1); -by (rewtac chain_def); -by (rtac CollectI 1); -by Safe_tac; -by (dtac bspec 1 THEN assume_tac 1); -by (res_inst_tac [("m1","Xa"), ("n1","X")] (TFin_subset_linear RS disjE) 2); -by (ALLGOALS(Blast_tac)); -qed "TFin_chain_lemm4"; - -Goal "EX c. (c :: 'a set set): maxchain S"; -by (res_inst_tac [("x", "Union(TFin S)")] exI 1); -by (rtac classical 1); -by (subgoal_tac "succ S (Union(TFin S)) = Union(TFin S)" 1); -by (resolve_tac [equal_succ_Union RS iffD2 RS sym] 2); -by (resolve_tac [subset_refl RS TFin_UnionI] 2); -by (rtac refl 2); -by (cut_facts_tac [subset_refl RS TFin_UnionI RS TFin_chain_lemm4] 1); -by (dtac (DiffI RS succ_not_equals) 1); -by (ALLGOALS(Blast_tac)); -qed "Hausdorff"; - - -(*--------------------------------------------------------------- - Section 5. Zorn's Lemma: if all chains have upper bounds - there is a maximal element - ----------------------------------------------------------------*) -Goalw [chain_def] - "[| c: chain S; z: S; \ -\ ALL x:c. x<=(z:: 'a set) |] ==> {z} Un c : chain S"; -by (Blast_tac 1); -qed "chain_extend"; - -Goalw [chain_def] "[| c: chain S; x: c |] ==> x <= Union(c)"; -by (Auto_tac); -qed "chain_Union_upper"; - -Goalw [chain_def] "c: chain S ==> ! x: c. x <= Union(c)"; -by (Auto_tac); -qed "chain_ball_Union_upper"; - -Goal "[| c: maxchain S; u: S; Union(c) <= u |] ==> Union(c) = u"; -by (rtac ccontr 1); -by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1); -by (etac conjE 1); -by (subgoal_tac "({u} Un c): super S c" 1); -by (Asm_full_simp_tac 1); -by (rewrite_tac [super_def,psubset_def]); -by (blast_tac (claset() addIs [chain_extend] addDs [chain_Union_upper]) 1); -qed "maxchain_Zorn"; - -Goal "ALL c: chain S. Union(c): S ==> \ -\ EX y: S. ALL z: S. y <= z --> y = z"; -by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1); -by (etac exE 1); -by (dtac subsetD 1 THEN assume_tac 1); -by (dtac bspec 1 THEN assume_tac 1); -by (res_inst_tac [("x","Union(c)")] bexI 1); -by (rtac ballI 1 THEN rtac impI 1); -by (blast_tac (claset() addSDs [maxchain_Zorn]) 1); -by (assume_tac 1); -qed "Zorn_Lemma"; - -(*------------------------------------------------------------- - Alternative version of Zorn's Lemma - --------------------------------------------------------------*) -Goal "ALL (c:: 'a set set): chain S. EX y : S. ALL x : c. x <= y ==> \ -\ EX y : S. ALL x : S. (y :: 'a set) <= x --> y = x"; -by (cut_facts_tac [Hausdorff,maxchain_subset_chain] 1); -by (EVERY1[etac exE, dtac subsetD, assume_tac]); -by (EVERY1[dtac bspec, assume_tac, etac bexE]); -by (res_inst_tac [("x","y")] bexI 1); -by (assume_tac 2); -by (EVERY1[rtac ballI, rtac impI, rtac ccontr]); -by (forw_inst_tac [("z","x")] chain_extend 1); -by (assume_tac 1 THEN Blast_tac 1); -by (rewrite_tac [maxchain_def,super_def,psubset_def]); -by (blast_tac (claset() addSEs [equalityCE]) 1); -qed "Zorn_Lemma2"; - -(** misc. lemmas **) - -Goalw [chain_def] "[| c : chain S; x: c; y: c |] ==> x <= y | y <= x"; -by (Blast_tac 1); -qed "chainD"; - -Goalw [chain_def] "!!(c :: 'a set set). c: chain S ==> c <= S"; -by (Blast_tac 1); -qed "chainD2"; - -(* proved elsewhere? *) -Goal "x : Union(c) ==> EX m:c. x:m"; -by (Blast_tac 1); -qed "mem_UnionD"; diff -r 5a176b8dda84 -r b7f64ee8da84 src/HOL/Hyperreal/Zorn.thy --- a/src/HOL/Hyperreal/Zorn.thy Fri Aug 30 16:42:45 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -(* Title : Zorn.thy - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF -*) - -Zorn = Main + - -constdefs - chain :: 'a::ord set => 'a set set - "chain S == {F. F <= S & (ALL x: F. ALL y: F. x <= y | y <= x)}" - - super :: ['a::ord set,'a set] => 'a set set - "super S c == {d. d: chain(S) & c < d}" - - maxchain :: 'a::ord set => 'a set set - "maxchain S == {c. c: chain S & super S c = {}}" - - succ :: ['a::ord set,'a set] => 'a set - "succ S c == if (c ~: chain S| c: maxchain S) - then c else (@c'. c': (super S c))" - -consts - "TFin" :: 'a::ord set => 'a set set - -inductive "TFin(S)" - intrs - succI "x : TFin S ==> succ S x : TFin S" - Pow_UnionI "Y : Pow(TFin S) ==> Union(Y) : TFin S" - - monos Pow_mono -end - diff -r 5a176b8dda84 -r b7f64ee8da84 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Aug 30 16:42:45 2002 +0200 +++ b/src/HOL/IsaMakefile Sat Aug 31 14:03:49 2002 +0200 @@ -159,6 +159,7 @@ HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal $(OUT)/HOL-Hyperreal: $(OUT)/HOL-Real Hyperreal/ROOT.ML\ + Library/Zorn.thy\ Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\ Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\ Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\ @@ -176,8 +177,7 @@ Hyperreal/Poly.ML Hyperreal/Poly.thy\ Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\ Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\ - Hyperreal/Transcendental.thy Hyperreal/Zorn.ML Hyperreal/Zorn.thy\ - Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \ + Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \ Hyperreal/hypreal_arith0.ML @cd Hyperreal; $(ISATOOL) usedir -b $(OUT)/HOL-Real HOL-Hyperreal @@ -203,6 +203,7 @@ Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \ Library/README.html Library/Continuity.thy \ Library/Nested_Environment.thy Library/Rational_Numbers.thy \ + Library/Zorn.thy\ Library/Library/ROOT.ML Library/Library/document/root.tex \ Library/Library/document/root.bib Library/While_Combinator.thy @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library diff -r 5a176b8dda84 -r b7f64ee8da84 src/HOL/Library/Zorn.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Zorn.thy Sat Aug 31 14:03:49 2002 +0200 @@ -0,0 +1,263 @@ +(* Title \ Zorn.thy + ID \ $Id$ + Author \ Jacques D. Fleuriot + Copyright \ 1998 University of Cambridge + Description \ Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF +*) + +header {*Zorn's Lemma*} + +theory Zorn = Main: + +text{*The lemma and section numbers refer to an unpublished article ``Towards +the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by +Abrial and Laffitte. *} + +constdefs + chain :: "'a::ord set => 'a set set" + "chain S == {F. F \ S & (\x \ F. \y \ F. x \ y | y \ x)}" + + super :: "['a::ord set,'a set] => 'a set set" + "super S c == {d. d \ chain(S) & c < d}" + + maxchain :: "'a::ord set => 'a set set" + "maxchain S == {c. c \ chain S & super S c = {}}" + + succ :: "['a::ord set,'a set] => 'a set" + "succ S c == if (c \ chain S| c \ maxchain S) + then c else (@c'. c': (super S c))" + +consts + "TFin" :: "'a::ord set => 'a set set" + +inductive "TFin(S)" + intros + succI: "x \ TFin S ==> succ S x \ TFin S" + Pow_UnionI: "Y \ Pow(TFin S) ==> Union(Y) \ TFin S" + + monos Pow_mono + + +subsection{*Mathematical Preamble*} + +lemma Union_lemma0: "(\x \ C. x \ A | B \ x) ==> Union(C)<=A | B \ Union(C)" +by blast + + +text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*} +lemma Abrial_axiom1: "x \ succ S x" +apply (unfold succ_def) +apply (rule split_if [THEN iffD2]) +apply (auto simp add: super_def maxchain_def psubset_def) +apply (rule swap, assumption) +apply (rule someI2, blast+) +done + +lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI] + +lemma TFin_induct: + "[| n \ TFin S; + !!x. [| x \ TFin S; P(x) |] ==> P(succ S x); + !!Y. [| Y \ TFin S; Ball Y P |] ==> P(Union Y) |] + ==> P(n)" +apply (erule TFin.induct, blast+) +done + +lemma succ_trans: "x \ y ==> x \ succ S y" +apply (erule subset_trans) +apply (rule Abrial_axiom1) +done + +text{*Lemma 1 of section 3.1*} +lemma TFin_linear_lemma1: + "[| n \ TFin S; m \ TFin S; + \x \ TFin S. x \ m --> x = m | succ S x \ m + |] ==> n \ m | succ S m \ n" +apply (erule TFin_induct) +apply (erule_tac [2] Union_lemma0) txt{*or just Blast_tac*} +apply (blast del: subsetI intro: succ_trans) +done + +text{* Lemma 2 of section 3.2 *} +lemma TFin_linear_lemma2: + "m \ TFin S ==> \n \ TFin S. n \ m --> n=m | succ S n \ m" +apply (erule TFin_induct) +apply (rule impI [THEN ballI]) +txt{*case split using TFin_linear_lemma1*} +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], + assumption+) +apply (drule_tac x = n in bspec, assumption) +apply (blast del: subsetI intro: succ_trans, blast) +txt{*second induction step*} +apply (rule impI [THEN ballI]) +apply (rule Union_lemma0 [THEN disjE]) +apply (rule_tac [3] disjI2) + prefer 2 apply blast +apply (rule ballI) +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], + assumption+, auto) +apply (blast intro!: Abrial_axiom1 [THEN subsetD]) +done + +text{*Re-ordering the premises of Lemma 2*} +lemma TFin_subsetD: + "[| n \ m; m \ TFin S; n \ TFin S |] ==> n=m | succ S n \ m" +apply (rule TFin_linear_lemma2 [rule_format]) +apply (assumption+) +done + +text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*} +lemma TFin_subset_linear: "[| m \ TFin S; n \ TFin S|] ==> n \ m | m \ n" +apply (rule disjE) +apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2]) +apply (assumption+, erule disjI2) +apply (blast del: subsetI + intro: subsetI Abrial_axiom1 [THEN subset_trans]) +done + +text{*Lemma 3 of section 3.3*} +lemma eq_succ_upper: "[| n \ TFin S; m \ TFin S; m = succ S m |] ==> n \ m" +apply (erule TFin_induct) +apply (drule TFin_subsetD) +apply (assumption+, force, blast) +done + +text{*Property 3.3 of section 3.3*} +lemma equal_succ_Union: "m \ TFin S ==> (m = succ S m) = (m = Union(TFin S))" +apply (rule iffI) +apply (rule Union_upper [THEN equalityI]) +apply (rule_tac [2] eq_succ_upper [THEN Union_least]) +apply (assumption+) +apply (erule ssubst) +apply (rule Abrial_axiom1 [THEN equalityI]) +apply (blast del: subsetI + intro: subsetI TFin_UnionI TFin.succI) +done + +subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*} + +text{*NB: We assume the partial ordering is @{text "\"}, + the subset relation!*} + +lemma empty_set_mem_chain: "({} :: 'a set set) \ chain S" +by (unfold chain_def, auto) + +lemma super_subset_chain: "super S c \ chain S" +by (unfold super_def, fast) + +lemma maxchain_subset_chain: "maxchain S \ chain S" +by (unfold maxchain_def, fast) + +lemma mem_super_Ex: "c \ chain S - maxchain S ==> ? d. d \ super S c" +by (unfold super_def maxchain_def, auto) + +lemma select_super: "c \ chain S - maxchain S ==> + (@c'. c': super S c): super S c" +apply (erule mem_super_Ex [THEN exE]) +apply (rule someI2, auto) +done + +lemma select_not_equals: "c \ chain S - maxchain S ==> + (@c'. c': super S c) \ c" +apply (rule notI) +apply (drule select_super) +apply (simp add: super_def psubset_def) +done + +lemma succI3: "c \ chain S - maxchain S ==> succ S c = (@c'. c': super S c)" +apply (unfold succ_def) +apply (fast intro!: if_not_P) +done + +lemma succ_not_equals: "c \ chain S - maxchain S ==> succ S c \ c" +apply (frule succI3) +apply (simp (no_asm_simp)) +apply (rule select_not_equals, assumption) +done + +lemma TFin_chain_lemma4: "c \ TFin S ==> (c :: 'a set set): chain S" +apply (erule TFin_induct) +apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]]) +apply (unfold chain_def) +apply (rule CollectI, safe) +apply (drule bspec, assumption) +apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE], + blast+) +done + +theorem Hausdorff: "\c. (c :: 'a set set): maxchain S" +apply (rule_tac x = "Union (TFin S) " in exI) +apply (rule classical) +apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ") + prefer 2 + apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric]) +apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4]) +apply (drule DiffI [THEN succ_not_equals], blast+) +done + + +subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then + There Is a Maximal Element*} + +lemma chain_extend: + "[| c \ chain S; z \ S; + \x \ c. x<=(z:: 'a set) |] ==> {z} Un c \ chain S" +by (unfold chain_def, blast) + +lemma chain_Union_upper: "[| c \ chain S; x \ c |] ==> x \ Union(c)" +by (unfold chain_def, auto) + +lemma chain_ball_Union_upper: "c \ chain S ==> \x \ c. x \ Union(c)" +by (unfold chain_def, auto) + +lemma maxchain_Zorn: + "[| c \ maxchain S; u \ S; Union(c) \ u |] ==> Union(c) = u" +apply (rule ccontr) +apply (simp add: maxchain_def) +apply (erule conjE) +apply (subgoal_tac " ({u} Un c) \ super S c") +apply simp +apply (unfold super_def psubset_def) +apply (blast intro: chain_extend dest: chain_Union_upper) +done + +theorem Zorn_Lemma: + "\c \ chain S. Union(c): S ==> \y \ S. \z \ S. y \ z --> y = z" +apply (cut_tac Hausdorff maxchain_subset_chain) +apply (erule exE) +apply (drule subsetD, assumption) +apply (drule bspec, assumption) +apply (rule_tac x = "Union (c) " in bexI) +apply (rule ballI, rule impI) +apply (blast dest!: maxchain_Zorn, assumption) +done + +subsection{*Alternative version of Zorn's Lemma*} + +lemma Zorn_Lemma2: + "\c \ chain S. \y \ S. \x \ c. x \ y + ==> \y \ S. \x \ S. (y :: 'a set) \ x --> y = x" +apply (cut_tac Hausdorff maxchain_subset_chain) +apply (erule exE) +apply (drule subsetD, assumption) +apply (drule bspec, assumption, erule bexE) +apply (rule_tac x = y in bexI) + prefer 2 apply assumption +apply clarify +apply (rule ccontr) +apply (frule_tac z = x in chain_extend) +apply (assumption, blast) +apply (unfold maxchain_def super_def psubset_def) +apply (blast elim!: equalityCE) +done + +text{*Various other lemmas*} + +lemma chainD: "[| c \ chain S; x \ c; y \ c |] ==> x \ y | y \ x" +by (unfold chain_def, blast) + +lemma chainD2: "!!(c :: 'a set set). c \ chain S ==> c \ S" +by (unfold chain_def, blast) + +end +