src/HOL/Library/Zorn.thy
changeset 18143 fe14f0282c60
parent 17200 3a4d03d1a31b
child 18585 5d379fe2eb74
     1.1 --- a/src/HOL/Library/Zorn.thy	Thu Nov 10 00:36:26 2005 +0100
     1.2 +++ b/src/HOL/Library/Zorn.thy	Thu Nov 10 17:31:44 2005 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  subsection{*Mathematical Preamble*}
     1.5  
     1.6  lemma Union_lemma0:
     1.7 -    "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
     1.8 +    "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C) \<subseteq> A | B \<subseteq> Union(C)"
     1.9    by blast
    1.10  
    1.11  
    1.12 @@ -129,8 +129,8 @@
    1.13  lemma equal_succ_Union: "m \<in> TFin S ==> (m = succ S m) = (m = Union(TFin S))"
    1.14    apply (rule iffI)
    1.15     apply (rule Union_upper [THEN equalityI])
    1.16 -    apply (rule_tac [2] eq_succ_upper [THEN Union_least])
    1.17 -      apply (assumption+)
    1.18 +    apply assumption
    1.19 +   apply (rule eq_succ_upper [THEN Union_least], assumption+)
    1.20    apply (erule ssubst)
    1.21    apply (rule Abrial_axiom1 [THEN equalityI])
    1.22    apply (blast del: subsetI intro: subsetI TFin_UnionI TFin.succI)
    1.23 @@ -153,14 +153,14 @@
    1.24  lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
    1.25    by (unfold super_def maxchain_def) auto
    1.26  
    1.27 -lemma select_super: "c \<in> chain S - maxchain S ==>
    1.28 -                          (\<some>c'. c': super S c): super S c"
    1.29 +lemma select_super:
    1.30 +     "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
    1.31    apply (erule mem_super_Ex [THEN exE])
    1.32    apply (rule someI2, auto)
    1.33    done
    1.34  
    1.35 -lemma select_not_equals: "c \<in> chain S - maxchain S ==>
    1.36 -                          (\<some>c'. c': super S c) \<noteq> c"
    1.37 +lemma select_not_equals:
    1.38 +     "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c"
    1.39    apply (rule notI)
    1.40    apply (drule select_super)
    1.41    apply (simp add: super_def psubset_def)
    1.42 @@ -186,7 +186,7 @@
    1.43    done
    1.44  
    1.45  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
    1.46 -  apply (rule_tac x = "Union (TFin S) " in exI)
    1.47 +  apply (rule_tac x = "Union (TFin S)" in exI)
    1.48    apply (rule classical)
    1.49    apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
    1.50     prefer 2
    1.51 @@ -201,7 +201,7 @@
    1.52  
    1.53  lemma chain_extend:
    1.54      "[| c \<in> chain S; z \<in> S;
    1.55 -        \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
    1.56 +        \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chain S"
    1.57    by (unfold chain_def) blast
    1.58  
    1.59  lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
    1.60 @@ -215,7 +215,7 @@
    1.61    apply (rule ccontr)
    1.62    apply (simp add: maxchain_def)
    1.63    apply (erule conjE)
    1.64 -  apply (subgoal_tac " ({u} Un c) \<in> super S c")
    1.65 +  apply (subgoal_tac "({u} Un c) \<in> super S c")
    1.66     apply simp
    1.67    apply (unfold super_def psubset_def)
    1.68    apply (blast intro: chain_extend dest: chain_Union_upper)
    1.69 @@ -227,7 +227,7 @@
    1.70    apply (erule exE)
    1.71    apply (drule subsetD, assumption)
    1.72    apply (drule bspec, assumption)
    1.73 -  apply (rule_tac x = "Union (c) " in bexI)
    1.74 +  apply (rule_tac x = "Union(c)" in bexI)
    1.75     apply (rule ballI, rule impI)
    1.76     apply (blast dest!: maxchain_Zorn, assumption)
    1.77    done