src/HOL/Library/Zorn.thy
 changeset 14706 71590b7733b7 parent 13652 172600c40793 child 15131 c69542757a4d
```     1.1 --- a/src/HOL/Library/Zorn.thy	Thu May 06 12:43:00 2004 +0200
1.2 +++ b/src/HOL/Library/Zorn.thy	Thu May 06 14:14:18 2004 +0200
1.3 @@ -1,39 +1,40 @@
1.4 -(*  Title       : Zorn.thy
1.5 +(*  Title       : HOL/Library/Zorn.thy
1.6      ID          : \$Id\$
1.7      Author      : Jacques D. Fleuriot
1.8 -    Description : Zorn's Lemma -- See Larry Paulson's Zorn.thy in ZF
1.9 -*)
1.10 +    Description : Zorn's Lemma -- see Larry Paulson's Zorn.thy in ZF
1.11 +*)
1.12
1.14 +header {* Zorn's Lemma *}
1.15
1.16  theory Zorn = Main:
1.17
1.18 -text{*The lemma and section numbers refer to an unpublished article ``Towards
1.19 -the Mechanization of the Proofs of Some Classical Theorems of Set Theory,'' by
1.20 -Abrial and Laffitte.  *}
1.21 +text{*
1.22 +  The lemma and section numbers refer to an unpublished article
1.23 +  \cite{Abrial-Laffitte}.
1.24 +*}
1.25
1.26  constdefs
1.27    chain     ::  "'a set set => 'a set set set"
1.28 -    "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
1.29 +  "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
1.30
1.31    super     ::  "['a set set,'a set set] => 'a set set set"
1.32 -    "super S c == {d. d \<in> chain(S) & c < d}"
1.33 +  "super S c == {d. d \<in> chain S & c \<subset> d}"
1.34
1.35    maxchain  ::  "'a set set => 'a set set set"
1.36 -    "maxchain S == {c. c \<in> chain S & super S c = {}}"
1.37 +  "maxchain S == {c. c \<in> chain S & super S c = {}}"
1.38
1.39    succ      ::  "['a set set,'a set set] => 'a set set"
1.40 -    "succ S c == if (c \<notin> chain S| c \<in> maxchain S)
1.41 -                 then c else (@c'. c': (super S c))"
1.42 +  "succ S c ==
1.43 +    if c \<notin> chain S | c \<in> maxchain S
1.44 +    then c else SOME c'. c' \<in> super S c"
1.45
1.46 -consts
1.47 -  "TFin" ::  "'a set set => 'a set set set"
1.48 +consts
1.49 +  TFin :: "'a set set => 'a set set set"
1.50
1.51 -inductive "TFin(S)"
1.52 +inductive "TFin S"
1.53    intros
1.54      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
1.55      Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
1.56 -
1.57    monos          Pow_mono
1.58
1.59
1.60 @@ -54,26 +55,26 @@
1.61
1.62  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
1.63
1.64 -lemma TFin_induct:
1.65 -          "[| n \<in> TFin S;
1.66 -             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
1.67 -             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
1.68 +lemma TFin_induct:
1.69 +          "[| n \<in> TFin S;
1.70 +             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
1.71 +             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
1.72            ==> P(n)"
1.73  apply (erule TFin.induct, blast+)
1.74  done
1.75
1.76  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
1.77 -apply (erule subset_trans)
1.78 -apply (rule Abrial_axiom1)
1.79 +apply (erule subset_trans)
1.80 +apply (rule Abrial_axiom1)
1.81  done
1.82
1.83  text{*Lemma 1 of section 3.1*}
1.84  lemma TFin_linear_lemma1:
1.85 -     "[| n \<in> TFin S;  m \<in> TFin S;
1.86 -         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
1.87 +     "[| n \<in> TFin S;  m \<in> TFin S;
1.88 +         \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
1.89        |] ==> n \<subseteq> m | succ S m \<subseteq> n"
1.90  apply (erule TFin_induct)
1.91 -apply (erule_tac  Union_lemma0) txt{*or just Blast_tac*}
1.92 +apply (erule_tac  Union_lemma0) (*or just blast*)
1.93  apply (blast del: subsetI intro: succ_trans)
1.94  done
1.95
1.96 @@ -82,20 +83,20 @@
1.97       "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
1.98  apply (erule TFin_induct)
1.99  apply (rule impI [THEN ballI])
1.100 -txt{*case split using TFin_linear_lemma1*}
1.101 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
1.102 +txt{*case split using @{text TFin_linear_lemma1}*}
1.103 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
1.104         assumption+)
1.105  apply (drule_tac x = n in bspec, assumption)
1.106 -apply (blast del: subsetI intro: succ_trans, blast)
1.107 +apply (blast del: subsetI intro: succ_trans, blast)
1.108  txt{*second induction step*}
1.109  apply (rule impI [THEN ballI])
1.110  apply (rule Union_lemma0 [THEN disjE])
1.111  apply (rule_tac  disjI2)
1.112 - prefer 2 apply blast
1.113 + prefer 2 apply blast
1.114  apply (rule ballI)
1.115 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
1.116 -       assumption+, auto)
1.117 -apply (blast intro!: Abrial_axiom1 [THEN subsetD])
1.118 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
1.119 +       assumption+, auto)
1.120 +apply (blast intro!: Abrial_axiom1 [THEN subsetD])
1.121  done
1.122
1.123  text{*Re-ordering the premises of Lemma 2*}
1.124 @@ -107,10 +108,10 @@
1.125
1.126  text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
1.127  lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
1.128 -apply (rule disjE)
1.129 +apply (rule disjE)
1.130  apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
1.131  apply (assumption+, erule disjI2)
1.132 -apply (blast del: subsetI
1.133 +apply (blast del: subsetI
1.134               intro: subsetI Abrial_axiom1 [THEN subset_trans])
1.135  done
1.136
1.137 @@ -130,12 +131,12 @@
1.138  apply (erule ssubst)
1.139  apply (rule Abrial_axiom1 [THEN equalityI])
1.140  apply (blast del: subsetI
1.141 -	     intro: subsetI TFin_UnionI TFin.succI)
1.142 +             intro: subsetI TFin_UnionI TFin.succI)
1.143  done
1.144
1.145  subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
1.146
1.147 -text{*NB: We assume the partial ordering is @{text "\<subseteq>"},
1.148 +text{*NB: We assume the partial ordering is @{text "\<subseteq>"},
1.149   the subset relation!*}
1.150
1.151  lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
1.152 @@ -150,13 +151,13 @@
1.153  lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
1.154  by (unfold super_def maxchain_def, auto)
1.155
1.156 -lemma select_super: "c \<in> chain S - maxchain S ==>
1.157 +lemma select_super: "c \<in> chain S - maxchain S ==>
1.158                            (@c'. c': super S c): super S c"
1.159  apply (erule mem_super_Ex [THEN exE])
1.160  apply (rule someI2, auto)
1.161  done
1.162
1.163 -lemma select_not_equals: "c \<in> chain S - maxchain S ==>
1.164 +lemma select_not_equals: "c \<in> chain S - maxchain S ==>
1.165                            (@c'. c': super S c) \<noteq> c"
1.166  apply (rule notI)
1.167  apply (drule select_super)
1.168 @@ -180,26 +181,26 @@
1.169  apply (unfold chain_def)
1.170  apply (rule CollectI, safe)
1.171  apply (drule bspec, assumption)
1.172 -apply (rule_tac  m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
1.173 +apply (rule_tac  m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
1.174         blast+)
1.175  done
1.176 -
1.177 +
1.178  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
1.179  apply (rule_tac x = "Union (TFin S) " in exI)
1.180  apply (rule classical)
1.181  apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
1.182   prefer 2
1.183 - apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
1.184 + apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
1.185  apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
1.186  apply (drule DiffI [THEN succ_not_equals], blast+)
1.187  done
1.188
1.189
1.190 -subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
1.191 +subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
1.192                                 There Is  a Maximal Element*}
1.193
1.194 -lemma chain_extend:
1.195 -    "[| c \<in> chain S; z \<in> S;
1.196 +lemma chain_extend:
1.197 +    "[| c \<in> chain S; z \<in> S;
1.198          \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
1.199  by (unfold chain_def, blast)
1.200
1.201 @@ -237,16 +238,16 @@
1.202       "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
1.203        ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
1.204  apply (cut_tac Hausdorff maxchain_subset_chain)
1.205 -apply (erule exE)
1.206 -apply (drule subsetD, assumption)
1.207 -apply (drule bspec, assumption, erule bexE)
1.208 +apply (erule exE)
1.209 +apply (drule subsetD, assumption)
1.210 +apply (drule bspec, assumption, erule bexE)
1.211  apply (rule_tac x = y in bexI)
1.212   prefer 2 apply assumption
1.213 -apply clarify
1.214 -apply (rule ccontr)
1.215 +apply clarify
1.216 +apply (rule ccontr)
1.217  apply (frule_tac z = x in chain_extend)
1.218  apply (assumption, blast)
1.219 -apply (unfold maxchain_def super_def psubset_def)
1.220 +apply (unfold maxchain_def super_def psubset_def)
1.221  apply (blast elim!: equalityCE)
1.222  done
1.223
1.224 @@ -259,4 +260,3 @@
1.225  by (unfold chain_def, blast)
1.226
1.227  end
1.228 -
```