author | wenzelm |
Thu, 19 Jun 2008 20:48:01 +0200 | |
changeset 27277 | 7b7ce2d7fafe |
parent 16417 | 9bc16273c2d4 |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Cardinal_AC.thy |
484 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
484 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
13134 | 6 |
These results help justify infinite-branching datatypes |
484 | 7 |
*) |
8 |
||
13328 | 9 |
header{*Cardinal Arithmetic Using AC*} |
10 |
||
16417 | 11 |
theory Cardinal_AC imports CardinalArith Zorn begin |
13134 | 12 |
|
13356 | 13 |
subsection{*Strengthened Forms of Existing Theorems on Cardinals*} |
13134 | 14 |
|
15 |
lemma cardinal_eqpoll: "|A| eqpoll A" |
|
16 |
apply (rule AC_well_ord [THEN exE]) |
|
17 |
apply (erule well_ord_cardinal_eqpoll) |
|
18 |
done |
|
19 |
||
14046 | 20 |
text{*The theorem @{term "||A|| = |A|"} *} |
21 |
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard, simp] |
|
13134 | 22 |
|
23 |
lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y" |
|
24 |
apply (rule AC_well_ord [THEN exE]) |
|
25 |
apply (rule AC_well_ord [THEN exE]) |
|
13269 | 26 |
apply (rule well_ord_cardinal_eqE, assumption+) |
13134 | 27 |
done |
28 |
||
29 |
lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y" |
|
13269 | 30 |
by (blast intro: cardinal_cong cardinal_eqE) |
13134 | 31 |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
32 |
lemma cardinal_disjoint_Un: |
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
33 |
"[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] |
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
34 |
==> |A Un C| = |B Un D|" |
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
35 |
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un) |
13134 | 36 |
|
37 |
lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|" |
|
38 |
apply (rule AC_well_ord [THEN exE]) |
|
13269 | 39 |
apply (erule well_ord_lepoll_imp_Card_le, assumption) |
13134 | 40 |
done |
41 |
||
42 |
lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)" |
|
43 |
apply (rule AC_well_ord [THEN exE]) |
|
44 |
apply (rule AC_well_ord [THEN exE]) |
|
45 |
apply (rule AC_well_ord [THEN exE]) |
|
13269 | 46 |
apply (rule well_ord_cadd_assoc, assumption+) |
13134 | 47 |
done |
48 |
||
49 |
lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)" |
|
50 |
apply (rule AC_well_ord [THEN exE]) |
|
51 |
apply (rule AC_well_ord [THEN exE]) |
|
52 |
apply (rule AC_well_ord [THEN exE]) |
|
13269 | 53 |
apply (rule well_ord_cmult_assoc, assumption+) |
13134 | 54 |
done |
55 |
||
56 |
lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)" |
|
57 |
apply (rule AC_well_ord [THEN exE]) |
|
58 |
apply (rule AC_well_ord [THEN exE]) |
|
59 |
apply (rule AC_well_ord [THEN exE]) |
|
13269 | 60 |
apply (rule well_ord_cadd_cmult_distrib, assumption+) |
13134 | 61 |
done |
62 |
||
63 |
lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A" |
|
64 |
apply (rule AC_well_ord [THEN exE]) |
|
13269 | 65 |
apply (erule well_ord_InfCard_square_eq, assumption) |
13134 | 66 |
done |
67 |
||
68 |
||
14046 | 69 |
subsection {*The relationship between cardinality and le-pollence*} |
13134 | 70 |
|
71 |
lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B" |
|
72 |
apply (rule cardinal_eqpoll |
|
73 |
[THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans]) |
|
74 |
apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans]) |
|
75 |
apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll]) |
|
76 |
done |
|
77 |
||
78 |
lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K" |
|
79 |
apply (erule Card_cardinal_eq [THEN subst], rule iffI, |
|
13269 | 80 |
erule Card_le_imp_lepoll) |
13134 | 81 |
apply (erule lepoll_imp_Card_le) |
82 |
done |
|
83 |
||
14046 | 84 |
lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0"; |
85 |
apply auto |
|
86 |
apply (drule cardinal_0 [THEN ssubst]) |
|
87 |
apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1]) |
|
88 |
done |
|
89 |
||
90 |
lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A" |
|
91 |
apply (cut_tac A = "A" in cardinal_eqpoll) |
|
92 |
apply (auto simp add: eqpoll_iff) |
|
93 |
apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal) |
|
94 |
apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2 |
|
95 |
simp add: cardinal_idem) |
|
96 |
done |
|
97 |
||
98 |
lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A" |
|
99 |
apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans) |
|
100 |
done |
|
101 |
||
102 |
||
103 |
subsection{*Other Applications of AC*} |
|
104 |
||
13134 | 105 |
lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)" |
106 |
apply (unfold surj_def) |
|
107 |
apply (erule CollectE) |
|
13784 | 108 |
apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE]) |
13134 | 109 |
apply (fast elim!: apply_Pair) |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
110 |
apply (blast dest: apply_type Pi_memberD |
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
111 |
intro: apply_equality Pi_type f_imp_injective) |
13134 | 112 |
done |
113 |
||
114 |
(*Kunen's Lemma 10.20*) |
|
115 |
lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| le |X|" |
|
116 |
apply (rule lepoll_imp_Card_le) |
|
117 |
apply (erule surj_implies_inj [THEN exE]) |
|
118 |
apply (unfold lepoll_def) |
|
119 |
apply (erule exI) |
|
120 |
done |
|
121 |
||
122 |
(*Kunen's Lemma 10.21*) |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
123 |
lemma cardinal_UN_le: |
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
124 |
"[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |\<Union>i\<in>K. X(i)| le K" |
13134 | 125 |
apply (simp add: InfCard_is_Card le_Card_iff) |
126 |
apply (rule lepoll_trans) |
|
127 |
prefer 2 |
|
128 |
apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll]) |
|
129 |
apply (simp add: InfCard_is_Card Card_cardinal_eq) |
|
130 |
apply (unfold lepoll_def) |
|
131 |
apply (frule InfCard_is_Card [THEN Card_is_Ord]) |
|
132 |
apply (erule AC_ball_Pi [THEN exE]) |
|
133 |
apply (rule exI) |
|
134 |
(*Lemma needed in both subgoals, for a fixed z*) |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
135 |
apply (subgoal_tac "ALL z: (\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) & |
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
136 |
(LEAST i. z:X (i)) : K") |
13134 | 137 |
prefer 2 |
138 |
apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI |
|
139 |
elim!: LeastI Ord_in_Ord) |
|
13269 | 140 |
apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>" |
13134 | 141 |
and d = "%<i,j>. converse (f`i) ` j" in lam_injective) |
142 |
(*Instantiate the lemma proved above*) |
|
13269 | 143 |
by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force) |
13134 | 144 |
|
145 |
||
146 |
(*The same again, using csucc*) |
|
147 |
lemma cardinal_UN_lt_csucc: |
|
148 |
"[| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
149 |
==> |\<Union>i\<in>K. X(i)| < csucc(K)" |
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
150 |
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal) |
13134 | 151 |
|
152 |
(*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), |
|
153 |
the least ordinal j such that i:Vfrom(A,j). *) |
|
154 |
lemma cardinal_UN_Ord_lt_csucc: |
|
155 |
"[| InfCard(K); ALL i:K. j(i) < csucc(K) |] |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
156 |
==> (\<Union>i\<in>K. j(i)) < csucc(K)" |
13269 | 157 |
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption) |
13134 | 158 |
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE) |
159 |
apply (blast intro!: Ord_UN elim: ltE) |
|
160 |
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc]) |
|
161 |
done |
|
162 |
||
163 |
||
164 |
(** Main result for infinite-branching datatypes. As above, but the index |
|
165 |
set need not be a cardinal. Surprisingly complicated proof! |
|
166 |
**) |
|
167 |
||
168 |
(*Work backwards along the injection from W into K, given that W~=0.*) |
|
169 |
lemma inj_UN_subset: |
|
170 |
"[| f: inj(A,B); a:A |] ==> |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
171 |
(\<Union>x\<in>A. C(x)) <= (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))" |
13134 | 172 |
apply (rule UN_least) |
173 |
apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper]) |
|
174 |
apply (simp add: inj_is_fun [THEN apply_rangeI]) |
|
175 |
apply (blast intro: inj_is_fun [THEN apply_type]) |
|
176 |
done |
|
177 |
||
178 |
(*Simpler to require |W|=K; we'd have a bijection; but the theorem would |
|
179 |
be weaker.*) |
|
180 |
lemma le_UN_Ord_lt_csucc: |
|
181 |
"[| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
182 |
==> (\<Union>w\<in>W. j(w)) < csucc(K)" |
13134 | 183 |
apply (case_tac "W=0") |
184 |
(*solve the easy 0 case*) |
|
185 |
apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc] |
|
186 |
Card_is_Ord Ord_0_lt_csucc) |
|
187 |
apply (simp add: InfCard_is_Card le_Card_iff lepoll_def) |
|
188 |
apply (safe intro!: equalityI) |
|
13269 | 189 |
apply (erule swap) |
190 |
apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+) |
|
13134 | 191 |
apply (simp add: inj_converse_fun [THEN apply_type]) |
192 |
apply (blast intro!: Ord_UN elim: ltE) |
|
193 |
done |
|
194 |
||
14046 | 195 |
ML |
196 |
{* |
|
197 |
val cardinal_0_iff_0 = thm "cardinal_0_iff_0"; |
|
198 |
val cardinal_lt_iff_lesspoll = thm "cardinal_lt_iff_lesspoll"; |
|
199 |
*} |
|
200 |
||
13134 | 201 |
end |