merged
authorpaulson
Fri, 23 Mar 2012 16:16:35 +0000
changeset 47102 b846c299f412
parent 47100 f8f788c8b7f3 (current diff)
parent 47101 ded5cc757bc9 (diff)
child 47103 187cac088582
child 47105 e64ffc96a49f
merged
--- a/src/ZF/AC/AC_Equiv.thy	Mon Jan 16 12:33:26 2012 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Fri Mar 23 16:16:35 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	Mon Jan 16 12:33:26 2012 +0100
+++ b/src/ZF/AC/Cardinal_aux.thy	Fri Mar 23 16:16:35 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	Mon Jan 16 12:33:26 2012 +0100
+++ b/src/ZF/Cardinal.thy	Fri Mar 23 16:16:35 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	Mon Jan 16 12:33:26 2012 +0100
+++ b/src/ZF/CardinalArith.thy	Fri Mar 23 16:16:35 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	Mon Jan 16 12:33:26 2012 +0100
+++ b/src/ZF/Perm.thy	Fri Mar 23 16:16:35 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)