src/HOL/Library/Zorn.thy
changeset 46008 c296c75f4cf4
parent 44890 22f665a2e91c
child 46752 e9e7209eb375
     1.1 --- a/src/HOL/Library/Zorn.thy	Wed Dec 28 15:08:12 2011 +0100
     1.2 +++ b/src/HOL/Library/Zorn.thy	Wed Dec 28 20:03:13 2011 +0100
     1.3 @@ -58,19 +58,18 @@
     1.4  lemma Abrial_axiom1: "x \<subseteq> succ S x"
     1.5    apply (auto simp add: succ_def super_def maxchain_def)
     1.6    apply (rule contrapos_np, assumption)
     1.7 -  apply (rule_tac Q="\<lambda>S. xa \<in> S" in someI2, blast+)
     1.8 +  apply (rule someI2)
     1.9 +  apply blast+
    1.10    done
    1.11  
    1.12  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
    1.13  
    1.14  lemma TFin_induct:
    1.15 -  assumes H: "n \<in> TFin S"
    1.16 -  and I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
    1.17 -    "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P(Union Y)"
    1.18 -  shows "P n" using H
    1.19 -  apply (induct rule: TFin.induct [where P=P])
    1.20 -   apply (blast intro: I)+
    1.21 -  done
    1.22 +  assumes H: "n \<in> TFin S" and
    1.23 +    I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
    1.24 +      "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P (Union Y)"
    1.25 +  shows "P n"
    1.26 +  using H by induct (blast intro: I)+
    1.27  
    1.28  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
    1.29    apply (erule subset_trans)
    1.30 @@ -160,7 +159,8 @@
    1.31  lemma select_super:
    1.32       "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
    1.33    apply (erule mem_super_Ex [THEN exE])
    1.34 -  apply (rule someI2 [where Q="%X. X : super S c"], auto)
    1.35 +  apply (rule someI2)
    1.36 +  apply auto
    1.37    done
    1.38  
    1.39  lemma select_not_equals:
    1.40 @@ -185,8 +185,8 @@
    1.41    apply (unfold chain_def chain_subset_def)
    1.42    apply (rule CollectI, safe)
    1.43     apply (drule bspec, assumption)
    1.44 -   apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
    1.45 -     best+)
    1.46 +   apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE])
    1.47 +      apply blast+
    1.48    done
    1.49  
    1.50  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"