1.1 --- a/src/ZF/AC/AC_Equiv.thy Fri Mar 23 12:03:59 2012 +0100
1.2 +++ b/src/ZF/AC/AC_Equiv.thy Fri Mar 23 16:16:15 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 Fri Mar 23 12:03:59 2012 +0100
2.2 +++ b/src/ZF/AC/Cardinal_aux.thy Fri Mar 23 16:16:15 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 Fri Mar 23 12:03:59 2012 +0100
3.2 +++ b/src/ZF/Cardinal.thy Fri Mar 23 16:16:15 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 Fri Mar 23 12:03:59 2012 +0100
4.2 +++ b/src/ZF/CardinalArith.thy Fri Mar 23 16:16:15 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 Fri Mar 23 12:03:59 2012 +0100
5.2 +++ b/src/ZF/Perm.thy Fri Mar 23 16:16:15 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