# HG changeset patch # User paulson # Date 1332519395 0 # Node ID b846c299f412dce687e17f73f59ca5041c2beb3c # Parent f8f788c8b7f31d4e655c3c036af7dcb16cd78e54# Parent ded5cc757bc9cb322bc8e7db4a63127f62c941fb merged diff -r f8f788c8b7f3 -r b846c299f412 src/ZF/AC/AC_Equiv.thy --- 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 \ inj(A, B); !!a. a \ A ==> f`a \ C |] ==> f \ 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 \! *) (* ********************************************************************** *) @@ -175,30 +170,18 @@ by blast (* ********************************************************************** *) -(* image of a surjection *) -(* ********************************************************************** *) - -lemma surj_image_eq: "f \ 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(\(A),r); 0\A; B \ A |] ==> (THE b. first(b,B,r)) \ B" + "[| well_ord(\(A),r); 0 \ A; B \ A |] ==> (THE b. first(b,B,r)) \ 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(\(A), R); 0\A |] ==> \f. f:(\ X \ A. X)" +lemma ex_choice_fun: "[| well_ord(\(A), R); 0 \ A |] ==> \f. f \ (\ X \ A. X)" by (fast elim!: first_in_B intro!: lam_type) -lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \f. f:(\ X \ Pow(A)-{0}. X)" +lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \f. f \ (\ X \ Pow(A)-{0}. X)" by (fast elim!: well_ord_subset [THEN ex_choice_fun]) diff -r f8f788c8b7f3 -r b846c299f412 src/ZF/AC/Cardinal_aux.thy --- 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 \ i; Ord(i) |] ==> \j. j 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 \ B"} -or @{term"B \ A"}. Also both are equipollent to their cardinalities, so -(if A and B are infinite) then @{term"A \ B \ |A\B| \ max(|A|,|B|) \ i"}. -In fact, the correctly strengthened version of this theorem appears below.*} -lemma Un_lepoll_Inf_Ord_weak: - "[|A \ i; B \ i; \ Finite(i); Ord(i)|] ==> A \ B \ 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 \ i; B \ i; ~Finite(i); Ord(i) |] ==> A \ B \ 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 \ i" and B: "B \ i" and NFI: "\ Finite(i)" and i: "Ord(i)" + shows "A \ B \ i" +proof (rule eqpollI) + have AB: "A \ B" using A B by (blast intro: eqpoll_sym eqpoll_trans) + have "2 \ nat" + by (rule subset_imp_lepoll) (rule OrdmemD [OF nat_2I Ord_nat]) + also have "... \ i" + by (simp add: nat_le_infinite_Ord le_imp_lepoll NFI i)+ + also have "... \ A" by (blast intro: eqpoll_sym A) + finally have "2 \ A" . + have ICI: "InfCard(|i|)" + by (simp add: Inf_Card_is_InfCard Finite_cardinal_iff NFI i) + have "A \ B \ A + B" by (rule Un_lepoll_sum) + also have "... \ A \ B" + by (rule lepoll_imp_sum_lepoll_prod [OF AB [THEN eqpoll_imp_lepoll] `2 \ A`]) + also have "... \ i \ i" + by (blast intro: prod_eqpoll_cong eqpoll_imp_lepoll A B) + also have "... \ i" + by (blast intro: well_ord_InfCard_square_eq well_ord_Memrel ICI i) + finally show "A \ B \ i" . +next + have "i \ A" by (blast intro: A eqpoll_sym) + also have "... \ A \ B" by (blast intro: subset_imp_lepoll) + finally show "i \ A \ B" . +qed schematic_lemma paired_bij: "?f \ bij({{y,z}. y \ x}, x)" apply (rule RepFun_bijective) @@ -82,8 +68,7 @@ lemma ex_eqpoll_disjoint: "\B. B \ A & B \ 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 \ i; B \ i; ~Finite(i); Ord(i) |] ==> A \ B \ i" apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE]) diff -r f8f788c8b7f3 -r b846c299f412 src/ZF/Cardinal.thy --- 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(\ i. i \ A)" proof (cases "\i. Ord (i) & i \ A") @@ -1105,6 +1105,9 @@ lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \ Finite(A)" by (blast intro: Finite_Pow Finite_Pow_imp_Finite) +lemma Finite_cardinal_iff: + assumes i: "Ord(i)" shows "Finite(|i|) \ 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 diff -r f8f788c8b7f3 -r b846c299f412 src/ZF/CardinalArith.thy --- 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)*} diff -r f8f788c8b7f3 -r b846c299f412 src/ZF/Perm.thy --- 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 \ 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 \ B)" by (auto simp add: restrict_def)