author | paulson |
Tue, 18 Dec 2001 15:03:27 +0100 | |
changeset 12536 | e9a729259385 |
parent 11317 | 7f9e4c389318 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/Cardinal_aux.ML |
1196 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1196 | 4 |
|
5 |
Auxiliary lemmas concerning cardinalities |
|
6 |
*) |
|
7 |
||
8 |
(* ********************************************************************** *) |
|
1461 | 9 |
(* Lemmas involving ordinals and cardinalities used in the proofs *) |
10 |
(* concerning AC16 and DC *) |
|
1196 | 11 |
(* ********************************************************************** *) |
12 |
||
1616
6d7278c3f686
Moved some proofs to Cardinal.ML; simplified others
paulson
parents:
1461
diff
changeset
|
13 |
(* j=|A| *) |
11317 | 14 |
Goal "[| A lepoll i; Ord(i) |] ==> \\<exists>j. j le i & A eqpoll j"; |
8123 | 15 |
by (blast_tac (claset() addSIs [lepoll_cardinal_le, well_ord_Memrel, |
16 |
well_ord_cardinal_eqpoll RS eqpoll_sym] |
|
17 |
addDs [lepoll_well_ord]) 1); |
|
1616
6d7278c3f686
Moved some proofs to Cardinal.ML; simplified others
paulson
parents:
1461
diff
changeset
|
18 |
qed "lepoll_imp_ex_le_eqpoll"; |
6d7278c3f686
Moved some proofs to Cardinal.ML; simplified others
paulson
parents:
1461
diff
changeset
|
19 |
|
6d7278c3f686
Moved some proofs to Cardinal.ML; simplified others
paulson
parents:
1461
diff
changeset
|
20 |
(* j=|A| *) |
8123 | 21 |
Goalw [lesspoll_def] |
11317 | 22 |
"[| A lesspoll i; Ord(i) |] ==> \\<exists>j. j<i & A eqpoll j"; |
8123 | 23 |
by (blast_tac (claset() addSDs [lepoll_imp_ex_le_eqpoll] addSEs [leE]) 1); |
1616
6d7278c3f686
Moved some proofs to Cardinal.ML; simplified others
paulson
parents:
1461
diff
changeset
|
24 |
qed "lesspoll_imp_ex_lt_eqpoll"; |
1196 | 25 |
|
5137 | 26 |
Goalw [InfCard_def] "[| ~Finite(i); Ord(i) |] ==> InfCard(|i|)"; |
1207 | 27 |
by (rtac conjI 1); |
28 |
by (rtac Card_cardinal 1); |
|
1196 | 29 |
by (resolve_tac [Card_nat RS (Card_def RS def_imp_iff RS iffD1 RS ssubst)] 1); |
30 |
by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll |
|
1461 | 31 |
RSN (2, well_ord_Memrel RS well_ord_lepoll_imp_Card_le)] 1 |
1196 | 32 |
THEN REPEAT (assume_tac 1)); |
3731 | 33 |
qed "Inf_Ord_imp_InfCard_cardinal"; |
1196 | 34 |
|
5137 | 35 |
Goal "[| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \ |
1461 | 36 |
\ ==> A Un B eqpoll i"; |
1207 | 37 |
by (rtac eqpollI 1); |
1196 | 38 |
by (eresolve_tac [subset_imp_lepoll RSN (2, eqpoll_sym RS eqpoll_imp_lepoll |
1461 | 39 |
RS lepoll_trans)] 2); |
2469 | 40 |
by (Fast_tac 2); |
1196 | 41 |
by (resolve_tac [Un_lepoll_sum RS lepoll_trans] 1); |
42 |
by (resolve_tac [lepoll_imp_sum_lepoll_prod RS lepoll_trans] 1); |
|
43 |
by (eresolve_tac [eqpoll_sym RSN (2, eqpoll_trans) RS eqpoll_imp_lepoll] 1 |
|
1461 | 44 |
THEN (assume_tac 1)); |
1196 | 45 |
by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll RS |
1461 | 46 |
(Ord_nat RS (nat_2I RS OrdmemD) RS subset_imp_lepoll RS lepoll_trans) |
47 |
RS (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans))] 1 |
|
1196 | 48 |
THEN (REPEAT (assume_tac 1))); |
49 |
by (eresolve_tac [prod_eqpoll_cong RS eqpoll_imp_lepoll RS lepoll_trans] 1 |
|
50 |
THEN (assume_tac 1)); |
|
51 |
by (resolve_tac [Inf_Ord_imp_InfCard_cardinal RSN (2, well_ord_Memrel RS |
|
1461 | 52 |
well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1 |
1196 | 53 |
THEN REPEAT (assume_tac 1)); |
3731 | 54 |
qed "Un_eqpoll_Inf_Ord"; |
1196 | 55 |
|
56 |
||
11317 | 57 |
Goal "?f \\<in> bij({{y,z}. y \\<in> x}, x)"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5241
diff
changeset
|
58 |
by (rtac RepFun_bijective 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5241
diff
changeset
|
59 |
by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5241
diff
changeset
|
60 |
by (Blast_tac 1); |
3731 | 61 |
qed "paired_bij"; |
1196 | 62 |
|
11317 | 63 |
Goalw [eqpoll_def] "{{y,z}. y \\<in> x} eqpoll x"; |
4091 | 64 |
by (fast_tac (claset() addSIs [paired_bij]) 1); |
3731 | 65 |
qed "paired_eqpoll"; |
1196 | 66 |
|
11317 | 67 |
Goal "\\<exists>B. B eqpoll A & B Int C = 0"; |
4091 | 68 |
by (fast_tac (claset() addSIs [paired_eqpoll, equals0I] addEs [mem_asym]) 1); |
3731 | 69 |
qed "ex_eqpoll_disjoint"; |
1196 | 70 |
|
5137 | 71 |
Goal "[| A lepoll i; B lepoll i; ~Finite(i); Ord(i) |] \ |
1461 | 72 |
\ ==> A Un B lepoll i"; |
1196 | 73 |
by (res_inst_tac [("A1","i"), ("C1","i")] (ex_eqpoll_disjoint RS exE) 1); |
1207 | 74 |
by (etac conjE 1); |
1196 | 75 |
by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans)] 1); |
76 |
by (assume_tac 1); |
|
77 |
by (resolve_tac [Un_lepoll_Un RS lepoll_trans] 1 THEN (REPEAT (assume_tac 1))); |
|
78 |
by (eresolve_tac [eqpoll_refl RSN (2, Un_eqpoll_Inf_Ord) RS |
|
1461 | 79 |
eqpoll_imp_lepoll] 1 |
80 |
THEN (REPEAT (assume_tac 1))); |
|
3731 | 81 |
qed "Un_lepoll_Inf_Ord"; |
1196 | 82 |
|
11317 | 83 |
Goal "[| P(i); i \\<in> j; Ord(j) |] ==> (LEAST i. P(i)) \\<in> j"; |
1196 | 84 |
by (eresolve_tac [Least_le RS leE] 1); |
1207 | 85 |
by (etac Ord_in_Ord 1 THEN (assume_tac 1)); |
86 |
by (etac ltE 1); |
|
4091 | 87 |
by (fast_tac (claset() addDs [OrdmemD]) 1); |
1207 | 88 |
by (etac subst_elem 1 THEN (assume_tac 1)); |
3731 | 89 |
qed "Least_in_Ord"; |
1196 | 90 |
|
11317 | 91 |
Goal "[| well_ord(x,r); y \\<subseteq> x; y lepoll succ(n); n \\<in> nat |] \ |
1461 | 92 |
\ ==> y-{THE b. first(b,y,r)} lepoll n"; |
1196 | 93 |
by (res_inst_tac [("Q","y=0")] (excluded_middle RS disjE) 1); |
4091 | 94 |
by (fast_tac (claset() addSIs [Diff_sing_lepoll, the_first_in]) 1); |
1196 | 95 |
by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1); |
1207 | 96 |
by (rtac empty_lepollI 2); |
2496 | 97 |
by (Fast_tac 1); |
3731 | 98 |
qed "Diff_first_lepoll"; |
1196 | 99 |
|
11317 | 100 |
Goal "(\\<Union>x \\<in> X. P(x)) \\<subseteq> (\\<Union>x \\<in> X. P(x)-Q(x)) Un (\\<Union>x \\<in> X. Q(x))"; |
2469 | 101 |
by (Fast_tac 1); |
3731 | 102 |
qed "UN_subset_split"; |
1196 | 103 |
|
11317 | 104 |
Goalw [lepoll_def] "Ord(a) ==> (\\<Union>x \\<in> a. {P(x)}) lepoll a"; |
105 |
by (res_inst_tac [("x","\\<lambda>z \\<in> (\\<Union>x \\<in> a. {P(x)}). (LEAST i. P(i)=z)")] exI 1); |
|
1196 | 106 |
by (res_inst_tac [("d","%z. P(z)")] lam_injective 1); |
4091 | 107 |
by (fast_tac (claset() addSIs [Least_in_Ord]) 1); |
108 |
by (fast_tac (claset() addIs [LeastI] addSEs [Ord_in_Ord]) 1); |
|
3731 | 109 |
qed "UN_sing_lepoll"; |
1196 | 110 |
|
11317 | 111 |
Goal "[| well_ord(T, R); ~Finite(a); Ord(a); n \\<in> nat |] ==> \ |
112 |
\ \\<forall>f. (\\<forall>b \\<in> a. f`b lepoll n & f`b \\<subseteq> T) --> (\\<Union>b \\<in> a. f`b) lepoll a"; |
|
6070 | 113 |
by (induct_tac "n" 1); |
1207 | 114 |
by (rtac allI 1); |
115 |
by (rtac impI 1); |
|
11317 | 116 |
by (res_inst_tac [("b","\\<Union>b \\<in> a. f`b")] subst 1); |
1207 | 117 |
by (rtac empty_lepollI 2); |
1196 | 118 |
by (resolve_tac [equals0I RS sym] 1); |
119 |
by (REPEAT (eresolve_tac [UN_E, allE] 1)); |
|
4091 | 120 |
by (fast_tac (claset() addDs [lepoll_0_is_0 RS subst]) 1); |
1207 | 121 |
by (rtac allI 1); |
122 |
by (rtac impI 1); |
|
11317 | 123 |
by (eres_inst_tac [("x","\\<lambda>x \\<in> a. f`x - {THE b. first(b,f`x,R)}")] allE 1); |
1207 | 124 |
by (etac impE 1); |
2469 | 125 |
by (Asm_full_simp_tac 1); |
4091 | 126 |
by (fast_tac (claset() addSIs [Diff_first_lepoll]) 1); |
2469 | 127 |
by (Asm_full_simp_tac 1); |
1196 | 128 |
by (resolve_tac [UN_subset_split RS subset_imp_lepoll RS lepoll_trans] 1); |
1207 | 129 |
by (rtac Un_lepoll_Inf_Ord 1 THEN (REPEAT_FIRST assume_tac)); |
130 |
by (etac UN_sing_lepoll 1); |
|
3731 | 131 |
qed "UN_fun_lepoll_lemma"; |
1196 | 132 |
|
11317 | 133 |
Goal "[| \\<forall>b \\<in> a. f`b lepoll n & f`b \\<subseteq> T; well_ord(T, R); \ |
134 |
\ ~Finite(a); Ord(a); n \\<in> nat |] ==> (\\<Union>b \\<in> a. f`b) lepoll a"; |
|
1196 | 135 |
by (eresolve_tac [UN_fun_lepoll_lemma RS allE] 1 THEN (REPEAT (assume_tac 1))); |
2469 | 136 |
by (Fast_tac 1); |
3731 | 137 |
qed "UN_fun_lepoll"; |
1196 | 138 |
|
11317 | 139 |
Goal "[| \\<forall>b \\<in> a. F(b) lepoll n & F(b) \\<subseteq> T; well_ord(T, R); \ |
140 |
\ ~Finite(a); Ord(a); n \\<in> nat |] ==> (\\<Union>b \\<in> a. F(b)) lepoll a"; |
|
1207 | 141 |
by (rtac impE 1 THEN (assume_tac 3)); |
11317 | 142 |
by (res_inst_tac [("f","\\<lambda>b \\<in> a. F(b)")] (UN_fun_lepoll) 2 |
1461 | 143 |
THEN (TRYALL assume_tac)); |
6153 | 144 |
by Auto_tac; |
3731 | 145 |
qed "UN_lepoll"; |
1196 | 146 |
|
11317 | 147 |
Goal "Ord(a) ==> (\\<Union>b \\<in> a. F(b)) = (\\<Union>b \\<in> a. F(b) - (\\<Union>c \\<in> b. F(c)))"; |
1207 | 148 |
by (rtac equalityI 1); |
2469 | 149 |
by (Fast_tac 2); |
1207 | 150 |
by (rtac subsetI 1); |
151 |
by (etac UN_E 1); |
|
152 |
by (rtac UN_I 1); |
|
11317 | 153 |
by (res_inst_tac [("P","%z. x \\<in> F(z)")] Least_in_Ord 1 THEN (REPEAT (assume_tac 1))); |
1207 | 154 |
by (rtac DiffI 1); |
1196 | 155 |
by (resolve_tac [Ord_in_Ord RSN (2, LeastI)] 1 THEN (REPEAT (assume_tac 1))); |
1207 | 156 |
by (rtac notI 1); |
157 |
by (etac UN_E 1); |
|
11317 | 158 |
by (eres_inst_tac [("P","%z. x \\<in> F(z)"),("i","c")] less_LeastE 1); |
1196 | 159 |
by (eresolve_tac [Ord_Least RSN (2, ltI)] 1); |
3731 | 160 |
qed "UN_eq_UN_Diffs"; |
1196 | 161 |
|
5068 | 162 |
Goalw [lepoll_def, eqpoll_def] |
11317 | 163 |
"a lepoll X ==> \\<exists>Y. Y \\<subseteq> X & a eqpoll Y"; |
1207 | 164 |
by (etac exE 1); |
1196 | 165 |
by (forward_tac [subset_refl RSN (2, restrict_bij)] 1); |
166 |
by (res_inst_tac [("x","f``a")] exI 1); |
|
4091 | 167 |
by (fast_tac (claset() addSEs [inj_is_fun RS fun_is_rel RS image_subset]) 1); |
3731 | 168 |
qed "lepoll_imp_eqpoll_subset"; |
1196 | 169 |
|
170 |
(* ********************************************************************** *) |
|
1461 | 171 |
(* Diff_lesspoll_eqpoll_Card *) |
1196 | 172 |
(* ********************************************************************** *) |
173 |
||
12536
e9a729259385
replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
paulson
parents:
11317
diff
changeset
|
174 |
Goal "[| A\\<approx>a; ~Finite(a); Card(a); B lesspoll a; A-B lesspoll a |] ==> P"; |
1196 | 175 |
by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE, |
1461 | 176 |
Card_is_Ord, conjE] 1)); |
8123 | 177 |
by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper1_le) 1 |
1461 | 178 |
THEN (assume_tac 1)); |
8123 | 179 |
by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper2_le) 1 |
1461 | 180 |
THEN (assume_tac 1)); |
1207 | 181 |
by (dtac Un_least_lt 1 THEN (assume_tac 1)); |
1196 | 182 |
by (dresolve_tac [le_imp_lepoll RSN |
1461 | 183 |
(2, eqpoll_imp_lepoll RS lepoll_trans)] 1 |
184 |
THEN (assume_tac 1)); |
|
1196 | 185 |
by (dresolve_tac [le_imp_lepoll RSN |
1461 | 186 |
(2, eqpoll_imp_lepoll RS lepoll_trans)] 1 |
187 |
THEN (assume_tac 1)); |
|
1196 | 188 |
by (res_inst_tac [("Q","Finite(x Un xa)")] (excluded_middle RS disjE) 1); |
189 |
by (dresolve_tac [[lepoll_Finite, lepoll_Finite] MRS Finite_Un] 2 |
|
1461 | 190 |
THEN (REPEAT (assume_tac 2))); |
1196 | 191 |
by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_Finite] 2); |
4091 | 192 |
by (fast_tac (claset() |
1461 | 193 |
addDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite]) 2); |
12536
e9a729259385
replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
paulson
parents:
11317
diff
changeset
|
194 |
by (dresolve_tac [ Un_lepoll_Inf_Ord] 1 THEN (REPEAT (assume_tac 1))); |
4091 | 195 |
by (fast_tac (claset() addSEs [ltE, Ord_in_Ord]) 1); |
12536
e9a729259385
replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
paulson
parents:
11317
diff
changeset
|
196 |
by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RS |
e9a729259385
replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
paulson
parents:
11317
diff
changeset
|
197 |
(lt_Card_imp_lesspoll RSN (2, lesspoll_trans1))] 1 |
1461 | 198 |
THEN (TRYALL assume_tac)); |
4091 | 199 |
by (fast_tac (claset() addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1); |
3731 | 200 |
qed "Diff_lesspoll_eqpoll_Card_lemma"; |
1196 | 201 |
|
5137 | 202 |
Goal "[| A eqpoll a; ~Finite(a); Card(a); B lesspoll a |] \ |
1461 | 203 |
\ ==> A - B eqpoll a"; |
2469 | 204 |
by (rtac swap 1 THEN (Fast_tac 1)); |
1207 | 205 |
by (rtac Diff_lesspoll_eqpoll_Card_lemma 1 THEN (REPEAT (assume_tac 1))); |
4091 | 206 |
by (fast_tac (claset() addSIs [lesspoll_def RS def_imp_iff RS iffD2, |
1461 | 207 |
subset_imp_lepoll RS (eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1); |
3731 | 208 |
qed "Diff_lesspoll_eqpoll_Card"; |
1196 | 209 |