--- a/src/ZF/AC/AC_Equiv.thy Fri Mar 23 12:03:59 2012 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Fri Mar 23 16:16:15 2012 +0000
@@ -162,11 +162,6 @@
"[| f \<in> inj(A, B); !!a. a \<in> A ==> f`a \<in> C |] ==> f \<in> inj(A,C)"
by (unfold inj_def, blast intro: Pi_type)
-lemma nat_not_Finite: "~ Finite(nat)"
-by (unfold Finite_def, blast dest: eqpoll_imp_lepoll ltI lt_not_lepoll)
-
-lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
-
(* ********************************************************************** *)
(* Another elimination rule for \<exists>! *)
(* ********************************************************************** *)
@@ -175,30 +170,18 @@
by blast
(* ********************************************************************** *)
-(* image of a surjection *)
-(* ********************************************************************** *)
-
-lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
-apply (unfold surj_def)
-apply (erule CollectE)
-apply (rule image_fun [THEN ssubst], assumption, rule subset_refl)
-apply (blast dest: apply_type)
-done
-
-
-(* ********************************************************************** *)
(* Lemmas used in the proofs like WO? ==> AC? *)
(* ********************************************************************** *)
lemma first_in_B:
- "[| well_ord(\<Union>(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
+ "[| well_ord(\<Union>(A),r); 0 \<notin> A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
by (blast dest!: well_ord_imp_ex1_first
[THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
-lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
+lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0 \<notin> A |] ==> \<exists>f. f \<in> (\<Pi> X \<in> A. X)"
by (fast elim!: first_in_B intro!: lam_type)
-lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)"
+lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
by (fast elim!: well_ord_subset [THEN ex_choice_fun])
--- a/src/ZF/AC/Cardinal_aux.thy Fri Mar 23 12:03:59 2012 +0100
+++ b/src/ZF/AC/Cardinal_aux.thy Fri Mar 23 16:16:15 2012 +0000
@@ -30,46 +30,32 @@
"[| A \<prec> i; Ord(i) |] ==> \<exists>j. j<i & A \<approx> j"
by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE)
-lemma Inf_Ord_imp_InfCard_cardinal: "[| ~Finite(i); Ord(i) |] ==> InfCard(|i|)"
-apply (unfold InfCard_def)
-apply (rule conjI)
-apply (rule Card_cardinal)
-apply (rule Card_nat
- [THEN Card_def [THEN def_imp_iff, THEN iffD1, THEN ssubst]])
- -- "rewriting would loop!"
-apply (rule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
-apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
-done
-
-text{*An alternative and more general proof goes like this: A and B are both
-well-ordered (because they are injected into an ordinal), either @{term"A \<lesssim> B"}
-or @{term"B \<lesssim> A"}. Also both are equipollent to their cardinalities, so
-(if A and B are infinite) then @{term"A \<union> B \<lesssim> |A\<oplus>B| \<longleftrightarrow> max(|A|,|B|) \<lesssim> i"}.
-In fact, the correctly strengthened version of this theorem appears below.*}
-lemma Un_lepoll_Inf_Ord_weak:
- "[|A \<approx> i; B \<approx> i; \<not> Finite(i); Ord(i)|] ==> A \<union> B \<lesssim> i"
-apply (rule Un_lepoll_sum [THEN lepoll_trans])
-apply (rule lepoll_imp_sum_lepoll_prod [THEN lepoll_trans])
-apply (erule eqpoll_trans [THEN eqpoll_imp_lepoll])
-apply (erule eqpoll_sym)
-apply (rule subset_imp_lepoll [THEN lepoll_trans, THEN lepoll_trans])
-apply (rule nat_2I [THEN OrdmemD], rule Ord_nat)
-apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
-apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
-apply (erule prod_eqpoll_cong [THEN eqpoll_imp_lepoll, THEN lepoll_trans],
- assumption)
-apply (rule eqpoll_imp_lepoll)
-apply (rule well_ord_Memrel [THEN well_ord_InfCard_square_eq], assumption)
-apply (rule Inf_Ord_imp_InfCard_cardinal, assumption+)
-done
-
lemma Un_eqpoll_Inf_Ord:
- "[| A \<approx> i; B \<approx> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<approx> i"
-apply (rule eqpollI)
-apply (blast intro: Un_lepoll_Inf_Ord_weak)
-apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
-apply (rule Un_upper1 [THEN subset_imp_lepoll])
-done
+ assumes A: "A \<approx> i" and B: "B \<approx> i" and NFI: "\<not> Finite(i)" and i: "Ord(i)"
+ shows "A \<union> B \<approx> i"
+proof (rule eqpollI)
+ have AB: "A \<approx> B" using A B by (blast intro: eqpoll_sym eqpoll_trans)
+ have "2 \<lesssim> nat"
+ by (rule subset_imp_lepoll) (rule OrdmemD [OF nat_2I Ord_nat])
+ also have "... \<lesssim> i"
+ by (simp add: nat_le_infinite_Ord le_imp_lepoll NFI i)+
+ also have "... \<approx> A" by (blast intro: eqpoll_sym A)
+ finally have "2 \<lesssim> A" .
+ have ICI: "InfCard(|i|)"
+ by (simp add: Inf_Card_is_InfCard Finite_cardinal_iff NFI i)
+ have "A \<union> B \<lesssim> A + B" by (rule Un_lepoll_sum)
+ also have "... \<lesssim> A \<times> B"
+ by (rule lepoll_imp_sum_lepoll_prod [OF AB [THEN eqpoll_imp_lepoll] `2 \<lesssim> A`])
+ also have "... \<approx> i \<times> i"
+ by (blast intro: prod_eqpoll_cong eqpoll_imp_lepoll A B)
+ also have "... \<approx> i"
+ by (blast intro: well_ord_InfCard_square_eq well_ord_Memrel ICI i)
+ finally show "A \<union> B \<lesssim> i" .
+next
+ have "i \<approx> A" by (blast intro: A eqpoll_sym)
+ also have "... \<lesssim> A \<union> B" by (blast intro: subset_imp_lepoll)
+ finally show "i \<lesssim> A \<union> B" .
+qed
schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
apply (rule RepFun_bijective)
@@ -82,8 +68,7 @@
lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B \<inter> C = 0"
by (fast intro!: paired_eqpoll equals0I elim: mem_asym)
-(*Finally we reach this result. Surely there's a simpler proof, as sketched
- above?*)
+(*Finally we reach this result. Surely there's a simpler proof?*)
lemma Un_lepoll_Inf_Ord:
"[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<lesssim> i"
apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE])
--- a/src/ZF/Cardinal.thy Fri Mar 23 12:03:59 2012 +0100
+++ b/src/ZF/Cardinal.thy Fri Mar 23 16:16:15 2012 +0000
@@ -445,7 +445,7 @@
(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*)
-lemma Card_cardinal: "Card(|A|)"
+lemma Card_cardinal [iff]: "Card(|A|)"
proof (unfold cardinal_def)
show "Card(\<mu> i. i \<approx> A)"
proof (cases "\<exists>i. Ord (i) & i \<approx> A")
@@ -1105,6 +1105,9 @@
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)"
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
+lemma Finite_cardinal_iff:
+ assumes i: "Ord(i)" shows "Finite(|i|) \<longleftrightarrow> Finite(i)"
+ by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+
(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
--- a/src/ZF/CardinalArith.thy Fri Mar 23 12:03:59 2012 +0100
+++ b/src/ZF/CardinalArith.thy Fri Mar 23 16:16:15 2012 +0000
@@ -682,7 +682,7 @@
apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq])
done
-lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
+lemma Inf_Card_is_InfCard: "[| Card(i); ~ Finite(i) |] ==> InfCard(i)"
by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord])
subsubsection{*Toward's Kunen's Corollary 10.13 (1)*}
--- a/src/ZF/Perm.thy Fri Mar 23 12:03:59 2012 +0100
+++ b/src/ZF/Perm.thy Fri Mar 23 16:16:15 2012 +0000
@@ -505,6 +505,9 @@
apply (blast intro: apply_equality apply_Pair Pi_type)
done
+lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
+ by (auto simp add: surj_def image_fun) (blast dest: apply_type)
+
lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
by (auto simp add: restrict_def)