src/ZF/Cardinal_AC.thy

--- a/src/ZF/Cardinal_AC.thy	Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy	Tue Oct 01 13:26:10 2002 +0200
@@ -28,10 +28,10 @@
 lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
 by (blast intro: cardinal_cong cardinal_eqE)
 
-lemma cardinal_disjoint_Un: "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] ==>  
-          |A Un C| = |B Un D|"
-apply (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
-done
+lemma cardinal_disjoint_Un:
+     "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] 
+      ==> |A Un C| = |B Un D|"
+by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
 
 lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
 apply (rule AC_well_ord [THEN exE])
@@ -85,7 +85,8 @@
 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)
+apply (blast dest: apply_type Pi_memberD 
+             intro: apply_equality Pi_type f_imp_injective)
 done
 
 (*Kunen's Lemma 10.20*)
@@ -97,7 +98,8 @@
 done
 
 (*Kunen's Lemma 10.21*)
-lemma cardinal_UN_le: "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"
+lemma cardinal_UN_le:
+     "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |\<Union>i\<in>K. X(i)| le K"
 apply (simp add: InfCard_is_Card le_Card_iff)
 apply (rule lepoll_trans)
  prefer 2
@@ -108,7 +110,8 @@
 apply (erule AC_ball_Pi [THEN exE])
 apply (rule exI)
 (*Lemma needed in both subgoals, for a fixed z*)
-apply (subgoal_tac "ALL z: (UN i:K. X (i)). z: X (LEAST i. z:X (i)) & (LEAST i. z:X (i)) : K")
+apply (subgoal_tac "ALL z: (\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) & 
+                    (LEAST i. z:X (i)) : K")
  prefer 2
  apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
              elim!: LeastI Ord_in_Ord)
@@ -121,15 +124,14 @@
 (*The same again, using csucc*)
 lemma cardinal_UN_lt_csucc:
      "[| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |]
-      ==> |UN i:K. X(i)| < csucc(K)"
-apply (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
-done
+      ==> |\<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). *)
 lemma cardinal_UN_Ord_lt_csucc:
      "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
-      ==> (UN i:K. j(i)) < csucc(K)"
+      ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
 apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
 apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
 apply (blast intro!: Ord_UN elim: ltE)
@@ -144,7 +146,7 @@
 (*Work backwards along the injection from W into K, given that W~=0.*)
 lemma inj_UN_subset:
      "[| f: inj(A,B);  a:A |] ==>            
-      (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))"
+      (\<Union>x\<in>A. C(x)) <= (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
 apply (rule UN_least)
 apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
  apply (simp add: inj_is_fun [THEN apply_rangeI])
@@ -155,7 +157,7 @@
   be weaker.*)
 lemma le_UN_Ord_lt_csucc:
      "[| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |]
-      ==> (UN w:W. j(w)) < csucc(K)"
+      ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
 apply (case_tac "W=0")
 (*solve the easy 0 case*)
  apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]