src/HOL/Library/Zorn.thy
changeset 26806 40b411ec05aa
parent 26298 53e382ccf71f
child 27064 267cab537760
     1.1 --- a/src/HOL/Library/Zorn.thy	Wed May 07 10:56:58 2008 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Wed May 07 10:57:19 2008 +0200
     1.3 @@ -44,7 +44,6 @@
     1.4    where
     1.5      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
     1.6    | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
     1.7 -  monos          Pow_mono
     1.8  
     1.9  
    1.10  subsection{*Mathematical Preamble*}
    1.11 @@ -57,22 +56,20 @@
    1.12  text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
    1.13  
    1.14  lemma Abrial_axiom1: "x \<subseteq> succ S x"
    1.15 -  apply (unfold succ_def)
    1.16 -  apply (rule split_if [THEN iffD2])
    1.17 -  apply (auto simp add: super_def maxchain_def psubset_def)
    1.18 +  apply (auto simp add: succ_def super_def maxchain_def)
    1.19    apply (rule contrapos_np, assumption)
    1.20 -  apply (rule someI2, blast+)
    1.21 +  apply (rule_tac Q="\<lambda>S. xa \<in> S" in someI2, blast+)
    1.22    done
    1.23  
    1.24  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
    1.25  
    1.26  lemma TFin_induct:
    1.27 -          "[| n \<in> TFin S;
    1.28 -             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
    1.29 -             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
    1.30 -          ==> P(n)"
    1.31 -  apply (induct set: TFin)
    1.32 -   apply blast+
    1.33 +  assumes H: "n \<in> TFin S"
    1.34 +  and I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
    1.35 +    "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P(Union Y)"
    1.36 +  shows "P n" using H
    1.37 +  apply (induct rule: TFin.induct [where P=P])
    1.38 +   apply (blast intro: I)+
    1.39    done
    1.40  
    1.41  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
    1.42 @@ -163,14 +160,14 @@
    1.43  lemma select_super:
    1.44       "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
    1.45    apply (erule mem_super_Ex [THEN exE])
    1.46 -  apply (rule someI2, auto)
    1.47 +  apply (rule someI2 [where Q="%X. X : super S c"], auto)
    1.48    done
    1.49  
    1.50  lemma select_not_equals:
    1.51       "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c"
    1.52    apply (rule notI)
    1.53    apply (drule select_super)
    1.54 -  apply (simp add: super_def psubset_def)
    1.55 +  apply (simp add: super_def less_le)
    1.56    done
    1.57  
    1.58  lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (\<some>c'. c': super S c)"
    1.59 @@ -189,7 +186,7 @@
    1.60    apply (rule CollectI, safe)
    1.61     apply (drule bspec, assumption)
    1.62     apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
    1.63 -     blast+)
    1.64 +     best+)
    1.65    done
    1.66  
    1.67  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
    1.68 @@ -223,7 +220,7 @@
    1.69  apply (erule conjE)
    1.70  apply (subgoal_tac "({u} Un c) \<in> super S c")
    1.71   apply simp
    1.72 -apply (unfold super_def psubset_def)
    1.73 +apply (unfold super_def less_le)
    1.74  apply (blast intro: chain_extend dest: chain_Union_upper)
    1.75  done
    1.76  
    1.77 @@ -253,7 +250,7 @@
    1.78  apply (rule ccontr)
    1.79  apply (frule_tac z = x in chain_extend)
    1.80    apply (assumption, blast)
    1.81 -apply (unfold maxchain_def super_def psubset_def)
    1.82 +apply (unfold maxchain_def super_def less_le)
    1.83  apply (blast elim!: equalityCE)
    1.84  done
    1.85