1.1 --- a/src/ZF/AC/AC_Equiv.thy	Mon Jan 16 12:33:26 2012 +0100
     1.2 +++ b/src/ZF/AC/AC_Equiv.thy	Fri Mar 23 16:16:35 2012 +0000
     1.3 @@ -162,11 +162,6 @@
     1.4       "[| f \<in> inj(A, B);  !!a. a \<in> A ==> f`a \<in> C |] ==> f \<in> inj(A,C)"
     1.5  by (unfold inj_def, blast intro: Pi_type) 
     1.6  
     1.7 -lemma nat_not_Finite: "~ Finite(nat)"
     1.8 -by (unfold Finite_def, blast dest: eqpoll_imp_lepoll ltI lt_not_lepoll)
     1.9 -
    1.10 -lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
    1.11 -
    1.12  (* ********************************************************************** *)
    1.13  (* Another elimination rule for \<exists>!                                       *)
    1.14  (* ********************************************************************** *)
    1.15 @@ -175,30 +170,18 @@
    1.16  by blast
    1.17  
    1.18  (* ********************************************************************** *)
    1.19 -(* image of a surjection                                                  *)
    1.20 -(* ********************************************************************** *)
    1.21 -
    1.22 -lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
    1.23 -apply (unfold surj_def)
    1.24 -apply (erule CollectE)
    1.25 -apply (rule image_fun [THEN ssubst], assumption, rule subset_refl)
    1.26 -apply (blast dest: apply_type) 
    1.27 -done
    1.28 -
    1.29 -
    1.30 -(* ********************************************************************** *)
    1.31  (* Lemmas used in the proofs like WO? ==> AC?                             *)
    1.32  (* ********************************************************************** *)
    1.33  
    1.34  lemma first_in_B:
    1.35 -     "[| well_ord(\<Union>(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
    1.36 +     "[| well_ord(\<Union>(A),r); 0 \<notin> A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
    1.37  by (blast dest!: well_ord_imp_ex1_first
    1.38                      [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
    1.39  
    1.40 -lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
    1.41 +lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0 \<notin> A |] ==> \<exists>f. f \<in> (\<Pi> X \<in> A. X)"
    1.42  by (fast elim!: first_in_B intro!: lam_type)
    1.43  
    1.44 -lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)"
    1.45 +lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
    1.46  by (fast elim!: well_ord_subset [THEN ex_choice_fun])
    1.47  
    1.48  

     2.1 --- a/src/ZF/AC/Cardinal_aux.thy	Mon Jan 16 12:33:26 2012 +0100
     2.2 +++ b/src/ZF/AC/Cardinal_aux.thy	Fri Mar 23 16:16:35 2012 +0000
     2.3 @@ -30,46 +30,32 @@
     2.4       "[| A \<prec> i; Ord(i) |] ==> \<exists>j. j<i & A \<approx> j"
     2.5  by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE)
     2.6  
     2.7 -lemma Inf_Ord_imp_InfCard_cardinal: "[| ~Finite(i); Ord(i) |] ==> InfCard(|i|)"
     2.8 -apply (unfold InfCard_def)
     2.9 -apply (rule conjI)
    2.10 -apply (rule Card_cardinal)
    2.11 -apply (rule Card_nat
    2.12 -            [THEN Card_def [THEN def_imp_iff, THEN iffD1, THEN ssubst]])
    2.13 -  -- "rewriting would loop!"
    2.14 -apply (rule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
    2.15 -apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
    2.16 -done
    2.17 -
    2.18 -text{*An alternative and more general proof goes like this: A and B are both
    2.19 -well-ordered (because they are injected into an ordinal), either @{term"A \<lesssim> B"}
    2.20 -or @{term"B \<lesssim> A"}.  Also both are equipollent to their cardinalities, so
    2.21 -(if A and B are infinite) then @{term"A \<union> B \<lesssim> |A\<oplus>B| \<longleftrightarrow> max(|A|,|B|) \<lesssim> i"}.
    2.22 -In fact, the correctly strengthened version of this theorem appears below.*}
    2.23 -lemma Un_lepoll_Inf_Ord_weak:
    2.24 -     "[|A \<approx> i; B \<approx> i; \<not> Finite(i); Ord(i)|] ==> A \<union> B \<lesssim> i"
    2.25 -apply (rule Un_lepoll_sum [THEN lepoll_trans])
    2.26 -apply (rule lepoll_imp_sum_lepoll_prod [THEN lepoll_trans])
    2.27 -apply (erule eqpoll_trans [THEN eqpoll_imp_lepoll])
    2.28 -apply (erule eqpoll_sym)
    2.29 -apply (rule subset_imp_lepoll [THEN lepoll_trans, THEN lepoll_trans])
    2.30 -apply (rule nat_2I [THEN OrdmemD], rule Ord_nat)
    2.31 -apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
    2.32 -apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
    2.33 -apply (erule prod_eqpoll_cong [THEN eqpoll_imp_lepoll, THEN lepoll_trans],
    2.34 -       assumption)
    2.35 -apply (rule eqpoll_imp_lepoll)
    2.36 -apply (rule well_ord_Memrel [THEN well_ord_InfCard_square_eq], assumption)
    2.37 -apply (rule Inf_Ord_imp_InfCard_cardinal, assumption+)
    2.38 -done
    2.39 -
    2.40  lemma Un_eqpoll_Inf_Ord:
    2.41 -     "[| A \<approx> i; B \<approx> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<approx> i"
    2.42 -apply (rule eqpollI)
    2.43 -apply (blast intro: Un_lepoll_Inf_Ord_weak)
    2.44 -apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
    2.45 -apply (rule Un_upper1 [THEN subset_imp_lepoll])
    2.46 -done
    2.47 +  assumes A: "A \<approx> i" and B: "B \<approx> i" and NFI: "\<not> Finite(i)" and i: "Ord(i)"
    2.48 +  shows "A \<union> B \<approx> i"
    2.49 +proof (rule eqpollI)
    2.50 +  have AB: "A \<approx> B" using A B by (blast intro: eqpoll_sym eqpoll_trans) 
    2.51 +  have "2 \<lesssim> nat" 
    2.52 +    by (rule subset_imp_lepoll) (rule OrdmemD [OF nat_2I Ord_nat]) 
    2.53 +  also have "... \<lesssim> i" 
    2.54 +    by (simp add: nat_le_infinite_Ord le_imp_lepoll NFI i)+
    2.55 +  also have "... \<approx> A" by (blast intro: eqpoll_sym A) 
    2.56 +  finally have "2 \<lesssim> A" .
    2.57 +  have ICI: "InfCard(|i|)" 
    2.58 +    by (simp add: Inf_Card_is_InfCard Finite_cardinal_iff NFI i) 
    2.59 +  have "A \<union> B \<lesssim> A + B" by (rule Un_lepoll_sum)
    2.60 +  also have "... \<lesssim> A \<times> B"
    2.61 +    by (rule lepoll_imp_sum_lepoll_prod [OF AB [THEN eqpoll_imp_lepoll] `2 \<lesssim> A`])
    2.62 +  also have "... \<approx> i \<times> i"
    2.63 +    by (blast intro: prod_eqpoll_cong eqpoll_imp_lepoll A B) 
    2.64 +  also have "... \<approx> i"
    2.65 +    by (blast intro: well_ord_InfCard_square_eq well_ord_Memrel ICI i) 
    2.66 +  finally show "A \<union> B \<lesssim> i" .
    2.67 +next  
    2.68 +  have "i \<approx> A" by (blast intro: A eqpoll_sym)
    2.69 +  also have "... \<lesssim> A \<union> B" by (blast intro: subset_imp_lepoll) 
    2.70 +  finally show "i \<lesssim> A \<union> B" .
    2.71 +qed
    2.72  
    2.73  schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
    2.74  apply (rule RepFun_bijective)
    2.75 @@ -82,8 +68,7 @@
    2.76  lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B \<inter> C = 0"
    2.77  by (fast intro!: paired_eqpoll equals0I elim: mem_asym)
    2.78  
    2.79 -(*Finally we reach this result.  Surely there's a simpler proof, as sketched
    2.80 -  above?*)
    2.81 +(*Finally we reach this result.  Surely there's a simpler proof?*)
    2.82  lemma Un_lepoll_Inf_Ord:
    2.83       "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<lesssim> i"
    2.84  apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE])

     3.1 --- a/src/ZF/Cardinal.thy	Mon Jan 16 12:33:26 2012 +0100
     3.2 +++ b/src/ZF/Cardinal.thy	Fri Mar 23 16:16:35 2012 +0000
     3.3 @@ -445,7 +445,7 @@
     3.4  
     3.5  (*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)
     3.6  
     3.7 -lemma Card_cardinal: "Card(|A|)"
     3.8 +lemma Card_cardinal [iff]: "Card(|A|)"
     3.9  proof (unfold cardinal_def)
    3.10    show "Card(\<mu> i. i \<approx> A)"
    3.11      proof (cases "\<exists>i. Ord (i) & i \<approx> A")
    3.12 @@ -1105,6 +1105,9 @@
    3.13  lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)"
    3.14  by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
    3.15  
    3.16 +lemma Finite_cardinal_iff:
    3.17 +  assumes i: "Ord(i)" shows "Finite(|i|) \<longleftrightarrow> Finite(i)"
    3.18 +  by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+
    3.19  
    3.20  
    3.21  (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered

     4.1 --- a/src/ZF/CardinalArith.thy	Mon Jan 16 12:33:26 2012 +0100
     4.2 +++ b/src/ZF/CardinalArith.thy	Fri Mar 23 16:16:35 2012 +0000
     4.3 @@ -682,7 +682,7 @@
     4.4  apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq])
     4.5  done
     4.6  
     4.7 -lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
     4.8 +lemma Inf_Card_is_InfCard: "[| Card(i); ~ Finite(i) |] ==> InfCard(i)"
     4.9  by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord])
    4.10  
    4.11  subsubsection{*Toward's Kunen's Corollary 10.13 (1)*}

     5.1 --- a/src/ZF/Perm.thy	Mon Jan 16 12:33:26 2012 +0100
     5.2 +++ b/src/ZF/Perm.thy	Fri Mar 23 16:16:35 2012 +0000
     5.3 @@ -505,6 +505,9 @@
     5.4  apply (blast intro: apply_equality apply_Pair Pi_type)
     5.5  done
     5.6  
     5.7 +lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
     5.8 +  by (auto simp add: surj_def image_fun) (blast dest: apply_type) 
     5.9 +
    5.10  lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
    5.11  by (auto simp add: restrict_def)
    5.12