# HG changeset patch
# User paulson
# Date 1332264033 0
# Node ID e4ee21290dcae1f5a57dcfe68f2a1b209e3be4d2
# Parent  7be54568efa12b5cee053c7a8f5b4dce3fb9395a
proof tidying

diff -r 7be54568efa1 -r e4ee21290dca src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/ZF/Cardinal_AC.thy	Tue Mar 20 17:20:33 2012 +0000
@@ -115,24 +115,30 @@
 
 subsection{*Other Applications of AC*}
 
-lemma surj_implies_inj: "f: surj(X,Y) ==> \<exists>g. g: inj(Y,X)"
-apply (unfold surj_def)
-apply (erule CollectE)
-apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
-apply (fast elim!: apply_Pair)
-apply (blast dest: apply_type Pi_memberD
-             intro: apply_equality Pi_type f_imp_injective)
-done
+lemma surj_implies_inj:
+  assumes f: "f \<in> surj(X,Y)" shows "\<exists>g. g \<in> inj(Y,X)"
+proof -
+  from f AC_Pi [of Y "%y. f-``{y}"]
+  obtain z where z: "z \<in> (\<Pi> y\<in>Y. f -`` {y})"  
+    by (auto simp add: surj_def) (fast dest: apply_Pair)
+  show ?thesis
+    proof
+      show "z \<in> inj(Y, X)" using z surj_is_fun [OF f]
+        by (blast dest: apply_type Pi_memberD
+                  intro: apply_equality Pi_type f_imp_injective)
+    qed
+qed
 
-(*Kunen's Lemma 10.20*)
-lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| \<le> |X|"
-apply (rule lepoll_imp_Card_le)
-apply (erule surj_implies_inj [THEN exE])
-apply (unfold lepoll_def)
-apply (erule exI)
-done
+text{*Kunen's Lemma 10.20*}
+lemma surj_implies_cardinal_le: 
+  assumes f: "f \<in> surj(X,Y)" shows "|Y| \<le> |X|"
+proof (rule lepoll_imp_Card_le)
+  from f [THEN surj_implies_inj] obtain g where "g \<in> inj(Y,X)" ..
+  thus "Y \<lesssim> X"
+    by (auto simp add: lepoll_def)
+qed
 
-(*Kunen's Lemma 10.21*)
+text{*Kunen's Lemma 10.21*}
 lemma cardinal_UN_le:
   assumes K: "InfCard(K)" 
   shows "(!!i. i\<in>K ==> |X(i)| \<le> K) ==> |\<Union>i\<in>K. X(i)| \<le> K"
@@ -141,7 +147,7 @@
   assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
   hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def) 
   with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
-    apply - apply atomize apply auto done
+    by force 
   { fix z
     assume z: "z \<in> (\<Union>i\<in>K. X(i))"
     then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
@@ -171,8 +177,8 @@
       ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
 by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
 
-(*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
-  the least ordinal j such that i:Vfrom(A,j). *)
+text{*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
+  the least ordinal j such that i:Vfrom(A,j). *}
 lemma cardinal_UN_Ord_lt_csucc:
      "[| InfCard(K);  \<forall>i\<in>K. j(i) < csucc(K) |]
       ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
@@ -203,13 +209,12 @@
   finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
 qed
 
-(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
-  be weaker.*)
+text{*Simpler to require |W|=K; we'd have a bijection; but the theorem would
+  be weaker.*}
 lemma le_UN_Ord_lt_csucc:
      "[| InfCard(K);  |W| \<le> K;  \<forall>w\<in>W. j(w) < csucc(K) |]
       ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
-apply (case_tac "W=0")
-(*solve the easy 0 case*)
+apply (case_tac "W=0") --{*solve the easy 0 case*}
  apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]
                   Card_is_Ord Ord_0_lt_csucc)
 apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)