src/ZF/Zorn.thy
changeset 46820 c656222c4dc1
parent 45602 2a858377c3d2
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Zorn.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/Zorn.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -28,11 +28,11 @@
     1.4  
     1.5  definition
     1.6    increasing :: "i=>i"  where
     1.7 -    "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A --> x<=f`x}"
     1.8 +    "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}"
     1.9  
    1.10  
    1.11  text{*Lemma for the inductive definition below*}
    1.12 -lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> Union(Y) \<in> Pow(A)"
    1.13 +lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> \<Union>(Y) \<in> Pow(A)"
    1.14  by blast
    1.15  
    1.16  
    1.17 @@ -45,12 +45,12 @@
    1.18    "TFin" :: "[i,i]=>i"
    1.19  
    1.20  inductive
    1.21 -  domains       "TFin(S,next)" <= "Pow(S)"
    1.22 +  domains       "TFin(S,next)" \<subseteq> "Pow(S)"
    1.23    intros
    1.24      nextI:       "[| x \<in> TFin(S,next);  next \<in> increasing(S) |]
    1.25                    ==> next`x \<in> TFin(S,next)"
    1.26  
    1.27 -    Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> Union(Y) \<in> TFin(S,next)"
    1.28 +    Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> \<Union>(Y) \<in> TFin(S,next)"
    1.29  
    1.30    monos         Pow_mono
    1.31    con_defs      increasing_def
    1.32 @@ -59,11 +59,11 @@
    1.33  
    1.34  subsection{*Mathematical Preamble *}
    1.35  
    1.36 -lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
    1.37 +lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> \<Union>(C)<=A | B<=\<Union>(C)"
    1.38  by blast
    1.39  
    1.40  lemma Inter_lemma0:
    1.41 -     "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A <= Inter(C) | Inter(C) <= B"
    1.42 +     "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A \<subseteq> \<Inter>(C) | \<Inter>(C) \<subseteq> B"
    1.43  by blast
    1.44  
    1.45  
    1.46 @@ -74,7 +74,7 @@
    1.47  apply (erule CollectD1)
    1.48  done
    1.49  
    1.50 -lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x <= f`x"
    1.51 +lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x \<subseteq> f`x"
    1.52  by (unfold increasing_def, blast)
    1.53  
    1.54  lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]
    1.55 @@ -86,7 +86,7 @@
    1.56  lemma TFin_induct:
    1.57    "[| n \<in> TFin(S,next);
    1.58        !!x. [| x \<in> TFin(S,next);  P(x);  next \<in> increasing(S) |] ==> P(next`x);
    1.59 -      !!Y. [| Y <= TFin(S,next);  \<forall>y\<in>Y. P(y) |] ==> P(Union(Y))
    1.60 +      !!Y. [| Y \<subseteq> TFin(S,next);  \<forall>y\<in>Y. P(y) |] ==> P(\<Union>(Y))
    1.61     |] ==> P(n)"
    1.62  by (erule TFin.induct, blast+)
    1.63  
    1.64 @@ -99,7 +99,7 @@
    1.65  text{*Lemma 1 of section 3.1*}
    1.66  lemma TFin_linear_lemma1:
    1.67       "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);
    1.68 -         \<forall>x \<in> TFin(S,next) . x<=m --> x=m | next`x<=m |]
    1.69 +         \<forall>x \<in> TFin(S,next) . x<=m \<longrightarrow> x=m | next`x<=m |]
    1.70        ==> n<=m | next`m<=n"
    1.71  apply (erule TFin_induct)
    1.72  apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
    1.73 @@ -111,7 +111,7 @@
    1.74    Requires @{term "next \<in> increasing(S)"} in the second induction step.*}
    1.75  lemma TFin_linear_lemma2:
    1.76      "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
    1.77 -     ==> \<forall>n \<in> TFin(S,next). n<=m --> n=m | next`n <= m"
    1.78 +     ==> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
    1.79  apply (erule TFin_induct)
    1.80  apply (rule impI [THEN ballI])
    1.81  txt{*case split using @{text TFin_linear_lemma1}*}
    1.82 @@ -136,13 +136,13 @@
    1.83  text{*a more convenient form for Lemma 2*}
    1.84  lemma TFin_subsetD:
    1.85       "[| n<=m;  m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
    1.86 -      ==> n=m | next`n <= m"
    1.87 +      ==> n=m | next`n \<subseteq> m"
    1.88  by (blast dest: TFin_linear_lemma2 [rule_format])
    1.89  
    1.90  text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
    1.91  lemma TFin_subset_linear:
    1.92       "[| m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
    1.93 -      ==> n <= m | m<=n"
    1.94 +      ==> n \<subseteq> m | m<=n"
    1.95  apply (rule disjE)
    1.96  apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
    1.97  apply (assumption+, erule disjI2)
    1.98 @@ -153,7 +153,7 @@
    1.99  
   1.100  text{*Lemma 3 of section 3.3*}
   1.101  lemma equal_next_upper:
   1.102 -     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n <= m"
   1.103 +     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n \<subseteq> m"
   1.104  apply (erule TFin_induct)
   1.105  apply (drule TFin_subsetD)
   1.106  apply (assumption+, force, blast)
   1.107 @@ -162,7 +162,7 @@
   1.108  text{*Property 3.3 of section 3.3*}
   1.109  lemma equal_next_Union:
   1.110       "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
   1.111 -      ==> m = next`m <-> m = Union(TFin(S,next))"
   1.112 +      ==> m = next`m <-> m = \<Union>(TFin(S,next))"
   1.113  apply (rule iffI)
   1.114  apply (rule Union_upper [THEN equalityI])
   1.115  apply (rule_tac [2] equal_next_upper [THEN Union_least])
   1.116 @@ -181,17 +181,17 @@
   1.117  
   1.118  text{** Defining the "next" operation for Hausdorff's Theorem **}
   1.119  
   1.120 -lemma chain_subset_Pow: "chain(A) <= Pow(A)"
   1.121 +lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)"
   1.122  apply (unfold chain_def)
   1.123  apply (rule Collect_subset)
   1.124  done
   1.125  
   1.126 -lemma super_subset_chain: "super(A,c) <= chain(A)"
   1.127 +lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)"
   1.128  apply (unfold super_def)
   1.129  apply (rule Collect_subset)
   1.130  done
   1.131  
   1.132 -lemma maxchain_subset_chain: "maxchain(A) <= chain(A)"
   1.133 +lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)"
   1.134  apply (unfold maxchain_def)
   1.135  apply (rule Collect_subset)
   1.136  done
   1.137 @@ -255,12 +255,12 @@
   1.138  apply (rule AC_Pi_Pow [THEN exE])
   1.139  apply (rule Hausdorff_next_exists [THEN bexE], assumption)
   1.140  apply (rename_tac ch "next")
   1.141 -apply (subgoal_tac "Union (TFin (S,next)) \<in> chain (S) ")
   1.142 +apply (subgoal_tac "\<Union>(TFin (S,next)) \<in> chain (S) ")
   1.143  prefer 2
   1.144   apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
   1.145 -apply (rule_tac x = "Union (TFin (S,next))" in exI)
   1.146 +apply (rule_tac x = "\<Union>(TFin (S,next))" in exI)
   1.147  apply (rule classical)
   1.148 -apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))")
   1.149 +apply (subgoal_tac "next ` Union(TFin (S,next)) = \<Union>(TFin (S,next))")
   1.150  apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
   1.151  apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
   1.152  prefer 2 apply assumption
   1.153 @@ -280,11 +280,11 @@
   1.154      "[| c \<in> chain(A);  z \<in> A;  \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)"
   1.155  by (unfold chain_def, blast)
   1.156  
   1.157 -lemma Zorn: "\<forall>c \<in> chain(S). Union(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z --> y=z"
   1.158 +lemma Zorn: "\<forall>c \<in> chain(S). \<Union>(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
   1.159  apply (rule Hausdorff [THEN exE])
   1.160  apply (simp add: maxchain_def)
   1.161  apply (rename_tac c)
   1.162 -apply (rule_tac x = "Union (c)" in bexI)
   1.163 +apply (rule_tac x = "\<Union>(c)" in bexI)
   1.164  prefer 2 apply blast
   1.165  apply safe
   1.166  apply (rename_tac z)
   1.167 @@ -299,7 +299,7 @@
   1.168  text {* Alternative version of Zorn's Lemma *}
   1.169  
   1.170  theorem Zorn2:
   1.171 -  "\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x <= y ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z --> y=z"
   1.172 +  "\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
   1.173  apply (cut_tac Hausdorff maxchain_subset_chain)
   1.174  apply (erule exE)
   1.175  apply (drule subsetD, assumption)
   1.176 @@ -321,20 +321,20 @@
   1.177  
   1.178  text{*Lemma 5*}
   1.179  lemma TFin_well_lemma5:
   1.180 -     "[| n \<in> TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) \<in> Z |]
   1.181 -      ==> \<forall>m \<in> Z. n <= m"
   1.182 +     "[| n \<in> TFin(S,next);  Z \<subseteq> TFin(S,next);  z:Z;  ~ \<Inter>(Z) \<in> Z |]
   1.183 +      ==> \<forall>m \<in> Z. n \<subseteq> m"
   1.184  apply (erule TFin_induct)
   1.185  prefer 2 apply blast txt{*second induction step is easy*}
   1.186  apply (rule ballI)
   1.187  apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
   1.188 -apply (subgoal_tac "m = Inter (Z) ")
   1.189 +apply (subgoal_tac "m = \<Inter>(Z) ")
   1.190  apply blast+
   1.191  done
   1.192  
   1.193  text{*Well-ordering of @{term "TFin(S,next)"} *}
   1.194 -lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next);  z \<in> Z |] ==> Inter(Z) \<in> Z"
   1.195 +lemma well_ord_TFin_lemma: "[| Z \<subseteq> TFin(S,next);  z \<in> Z |] ==> \<Inter>(Z) \<in> Z"
   1.196  apply (rule classical)
   1.197 -apply (subgoal_tac "Z = {Union (TFin (S,next))}")
   1.198 +apply (subgoal_tac "Z = {\<Union>(TFin (S,next))}")
   1.199  apply (simp (no_asm_simp) add: Inter_singleton)
   1.200  apply (erule equal_singleton)
   1.201  apply (rule Union_upper [THEN equalityI])
   1.202 @@ -350,7 +350,7 @@
   1.203  txt{*Prove the well-foundedness goal*}
   1.204  apply (rule wf_onI)
   1.205  apply (frule well_ord_TFin_lemma, assumption)
   1.206 -apply (drule_tac x = "Inter (Z) " in bspec, assumption)
   1.207 +apply (drule_tac x = "\<Inter>(Z) " in bspec, assumption)
   1.208  apply blast
   1.209  txt{*Now prove the linearity goal*}
   1.210  apply (intro ballI)
   1.211 @@ -394,25 +394,25 @@
   1.212       "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
   1.213           next \<in> increasing(S);
   1.214           \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
   1.215 -      ==> (\<lambda> x \<in> S. Union({y \<in> TFin(S,next). x \<notin> y}))
   1.216 +      ==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
   1.217                 \<in> inj(S, TFin(S,next) - {S})"
   1.218  apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
   1.219  apply (rule DiffI)
   1.220  apply (rule Collect_subset [THEN TFin_UnionI])
   1.221  apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
   1.222 -apply (subgoal_tac "x \<notin> Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
   1.223 +apply (subgoal_tac "x \<notin> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
   1.224  prefer 2 apply (blast elim: equalityE)
   1.225 -apply (subgoal_tac "Union ({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
   1.226 +apply (subgoal_tac "\<Union>({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
   1.227  prefer 2 apply (blast elim: equalityE)
   1.228 -txt{*For proving @{text "x \<in> next`Union(...)"}.
   1.229 +txt{*For proving @{text "x \<in> next`\<Union>(...)"}.
   1.230    Abrial and Laffitte's justification appears to be faulty.*}
   1.231 -apply (subgoal_tac "~ next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) 
   1.232 -                    <= Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
   1.233 +apply (subgoal_tac "~ next ` Union({y \<in> TFin (S,next) . x \<notin> y}) 
   1.234 +                    \<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
   1.235   prefer 2
   1.236   apply (simp del: Union_iff
   1.237               add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]
   1.238               Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
   1.239 -apply (subgoal_tac "x \<in> next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
   1.240 +apply (subgoal_tac "x \<in> next ` Union({y \<in> TFin (S,next) . x \<notin> y}) ")
   1.241   prefer 2
   1.242   apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
   1.243  txt{*End of the lemmas!*}
   1.244 @@ -436,7 +436,7 @@
   1.245  
   1.246  
   1.247  definition Chain :: "i => i" where
   1.248 -  "Chain(r) = {A : Pow(field(r)). ALL a:A. ALL b:A. <a, b> : r | <b, a> : r}"
   1.249 +  "Chain(r) = {A \<in> Pow(field(r)). \<forall>a\<in>A. \<forall>b\<in>A. <a, b> \<in> r | <b, a> \<in> r}"
   1.250  
   1.251  lemma mono_Chain:
   1.252    "r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)"
   1.253 @@ -445,17 +445,17 @@
   1.254  
   1.255  theorem Zorn_po:
   1.256    assumes po: "Partial_order(r)"
   1.257 -    and u: "ALL C:Chain(r). EX u:field(r). ALL a:C. <a, u> : r"
   1.258 -  shows "EX m:field(r). ALL a:field(r). <m, a> : r --> a = m"
   1.259 +    and u: "\<forall>C\<in>Chain(r). \<exists>u\<in>field(r). \<forall>a\<in>C. <a, u> \<in> r"
   1.260 +  shows "\<exists>m\<in>field(r). \<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
   1.261  proof -
   1.262    have "Preorder(r)" using po by (simp add: partial_order_on_def)
   1.263    --{* Mirror r in the set of subsets below (wrt r) elements of A (?). *}
   1.264 -  let ?B = "lam x:field(r). r -`` {x}" let ?S = "?B `` field(r)"
   1.265 -  have "ALL C:chain(?S). EX U:?S. ALL A:C. A \<subseteq> U"
   1.266 +  let ?B = "\<lambda>x\<in>field(r). r -`` {x}" let ?S = "?B `` field(r)"
   1.267 +  have "\<forall>C\<in>chain(?S). \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
   1.268    proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
   1.269      fix C
   1.270 -    assume 1: "C \<subseteq> ?S" and 2: "ALL A:C. ALL B:C. A \<subseteq> B | B \<subseteq> A"
   1.271 -    let ?A = "{x : field(r). EX M:C. M = ?B`x}"
   1.272 +    assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B | B \<subseteq> A"
   1.273 +    let ?A = "{x \<in> field(r). \<exists>M\<in>C. M = ?B`x}"
   1.274      have "C = ?B `` ?A" using 1
   1.275        apply (auto simp: image_def)
   1.276        apply rule
   1.277 @@ -472,46 +472,46 @@
   1.278        apply (thin_tac "C \<subseteq> ?X")
   1.279        apply (fast elim: lamE)
   1.280        done
   1.281 -    have "?A : Chain(r)"
   1.282 +    have "?A \<in> Chain(r)"
   1.283      proof (simp add: Chain_def subsetI, intro conjI ballI impI)
   1.284        fix a b
   1.285 -      assume "a : field(r)" "r -`` {a} : C" "b : field(r)" "r -`` {b} : C"
   1.286 +      assume "a \<in> field(r)" "r -`` {a} \<in> C" "b \<in> field(r)" "r -`` {b} \<in> C"
   1.287        hence "r -`` {a} \<subseteq> r -`` {b} | r -`` {b} \<subseteq> r -`` {a}" using 2 by auto
   1.288 -      then show "<a, b> : r | <b, a> : r"
   1.289 -        using `Preorder(r)` `a : field(r)` `b : field(r)`
   1.290 +      then show "<a, b> \<in> r | <b, a> \<in> r"
   1.291 +        using `Preorder(r)` `a \<in> field(r)` `b \<in> field(r)`
   1.292          by (simp add: subset_vimage1_vimage1_iff)
   1.293      qed
   1.294 -    then obtain u where uA: "u : field(r)" "ALL a:?A. <a, u> : r"
   1.295 +    then obtain u where uA: "u \<in> field(r)" "\<forall>a\<in>?A. <a, u> \<in> r"
   1.296        using u
   1.297        apply auto
   1.298        apply (drule bspec) apply assumption
   1.299        apply auto
   1.300        done
   1.301 -    have "ALL A:C. A \<subseteq> r -`` {u}"
   1.302 +    have "\<forall>A\<in>C. A \<subseteq> r -`` {u}"
   1.303      proof (auto intro!: vimageI)
   1.304        fix a B
   1.305 -      assume aB: "B : C" "a : B"
   1.306 -      with 1 obtain x where "x : field(r)" "B = r -`` {x}"
   1.307 +      assume aB: "B \<in> C" "a \<in> B"
   1.308 +      with 1 obtain x where "x \<in> field(r)" "B = r -`` {x}"
   1.309          apply -
   1.310          apply (drule subsetD) apply assumption
   1.311          apply (erule imageE)
   1.312          apply (erule lamE)
   1.313          apply simp
   1.314          done
   1.315 -      then show "<a, u> : r" using uA aB `Preorder(r)`
   1.316 +      then show "<a, u> \<in> r" using uA aB `Preorder(r)`
   1.317          by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+
   1.318      qed
   1.319 -    then show "EX U:field(r). ALL A:C. A \<subseteq> r -`` {U}"
   1.320 -      using `u : field(r)` ..
   1.321 +    then show "\<exists>U\<in>field(r). \<forall>A\<in>C. A \<subseteq> r -`` {U}"
   1.322 +      using `u \<in> field(r)` ..
   1.323    qed
   1.324    from Zorn2 [OF this]
   1.325 -  obtain m B where "m : field(r)" "B = r -`` {m}"
   1.326 -    "ALL x:field(r). B \<subseteq> r -`` {x} --> B = r -`` {x}"
   1.327 +  obtain m B where "m \<in> field(r)" "B = r -`` {m}"
   1.328 +    "\<forall>x\<in>field(r). B \<subseteq> r -`` {x} \<longrightarrow> B = r -`` {x}"
   1.329      by (auto elim!: lamE simp: ball_image_simp)
   1.330 -  then have "ALL a:field(r). <m, a> : r --> a = m"
   1.331 -    using po `Preorder(r)` `m : field(r)`
   1.332 +  then have "\<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
   1.333 +    using po `Preorder(r)` `m \<in> field(r)`
   1.334      by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff)
   1.335 -  then show ?thesis using `m : field(r)` by blast
   1.336 +  then show ?thesis using `m \<in> field(r)` by blast
   1.337  qed
   1.338  
   1.339  end