author paulson Thu, 10 Nov 2005 17:31:44 +0100 changeset 18143 fe14f0282c60 parent 18142 a51ab4152097 child 18144 4edcb5fdc3b0
tidying
 src/HOL/Library/Zorn.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Library/Zorn.thy	Thu Nov 10 00:36:26 2005 +0100
+++ b/src/HOL/Library/Zorn.thy	Thu Nov 10 17:31:44 2005 +0100
@@ -43,7 +43,7 @@
subsection{*Mathematical Preamble*}

lemma Union_lemma0:
-    "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
+    "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C) \<subseteq> A | B \<subseteq> Union(C)"
by blast

@@ -129,8 +129,8 @@
lemma equal_succ_Union: "m \<in> TFin S ==> (m = succ S m) = (m = Union(TFin S))"
apply (rule iffI)
apply (rule Union_upper [THEN equalityI])
-    apply (rule_tac  eq_succ_upper [THEN Union_least])
-      apply (assumption+)
+    apply assumption
+   apply (rule eq_succ_upper [THEN Union_least], assumption+)
apply (erule ssubst)
apply (rule Abrial_axiom1 [THEN equalityI])
apply (blast del: subsetI intro: subsetI TFin_UnionI TFin.succI)
@@ -153,14 +153,14 @@
lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
by (unfold super_def maxchain_def) auto

-lemma select_super: "c \<in> chain S - maxchain S ==>
-                          (\<some>c'. c': super S c): super S c"
+lemma select_super:
+     "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
apply (erule mem_super_Ex [THEN exE])
apply (rule someI2, auto)
done

-lemma select_not_equals: "c \<in> chain S - maxchain S ==>
-                          (\<some>c'. c': super S c) \<noteq> c"
+lemma select_not_equals:
+     "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c"
apply (rule notI)
apply (drule select_super)
@@ -186,7 +186,7 @@
done

theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
-  apply (rule_tac x = "Union (TFin S) " in exI)
+  apply (rule_tac x = "Union (TFin S)" in exI)
apply (rule classical)
apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
prefer 2
@@ -201,7 +201,7 @@

lemma chain_extend:
"[| c \<in> chain S; z \<in> S;
-        \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
+        \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chain S"
by (unfold chain_def) blast

lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
@@ -215,7 +215,7 @@
apply (rule ccontr)
apply (erule conjE)
-  apply (subgoal_tac " ({u} Un c) \<in> super S c")
+  apply (subgoal_tac "({u} Un c) \<in> super S c")
apply simp
apply (unfold super_def psubset_def)
apply (blast intro: chain_extend dest: chain_Union_upper)
@@ -227,7 +227,7 @@
apply (erule exE)
apply (drule subsetD, assumption)
apply (drule bspec, assumption)
-  apply (rule_tac x = "Union (c) " in bexI)
+  apply (rule_tac x = "Union(c)" in bexI)
apply (rule ballI, rule impI)
apply (blast dest!: maxchain_Zorn, assumption)
done