author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 47071  2884ee1ffbf0 
child 58871  c399ae4b836f 
permissions  rwrr 
1478  1 
(* Title: ZF/Cardinal_AC.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

484  3 
Copyright 1994 University of Cambridge 
4 

13134  5 
These results help justify infinitebranching datatypes 
484  6 
*) 
7 

13328  8 
header{*Cardinal Arithmetic Using AC*} 
9 

16417  10 
theory Cardinal_AC imports CardinalArith Zorn begin 
13134  11 

13356  12 
subsection{*Strengthened Forms of Existing Theorems on Cardinals*} 
13134  13 

46954  14 
lemma cardinal_eqpoll: "A \<approx> A" 
13134  15 
apply (rule AC_well_ord [THEN exE]) 
16 
apply (erule well_ord_cardinal_eqpoll) 

17 
done 

18 

14046  19 
text{*The theorem @{term "A = A"} *} 
45602  20 
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp] 
13134  21 

46954  22 
lemma cardinal_eqE: "X = Y ==> X \<approx> Y" 
13134  23 
apply (rule AC_well_ord [THEN exE]) 
24 
apply (rule AC_well_ord [THEN exE]) 

13269  25 
apply (rule well_ord_cardinal_eqE, assumption+) 
13134  26 
done 
27 

46954  28 
lemma cardinal_eqpoll_iff: "X = Y \<longleftrightarrow> X \<approx> Y" 
13269  29 
by (blast intro: cardinal_cong cardinal_eqE) 
13134  30 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

31 
lemma cardinal_disjoint_Un: 
46820  32 
"[ A=B; C=D; A \<inter> C = 0; B \<inter> D = 0 ] 
33 
==> A \<union> C = B \<union> D" 

13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

34 
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un) 
13134  35 

46954  36 
lemma lepoll_imp_Card_le: "A \<lesssim> B ==> A \<le> B" 
13134  37 
apply (rule AC_well_ord [THEN exE]) 
13269  38 
apply (erule well_ord_lepoll_imp_Card_le, assumption) 
13134  39 
done 
40 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

41 
lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)" 
13134  42 
apply (rule AC_well_ord [THEN exE]) 
43 
apply (rule AC_well_ord [THEN exE]) 

44 
apply (rule AC_well_ord [THEN exE]) 

13269  45 
apply (rule well_ord_cadd_assoc, assumption+) 
13134  46 
done 
47 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

48 
lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" 
13134  49 
apply (rule AC_well_ord [THEN exE]) 
50 
apply (rule AC_well_ord [THEN exE]) 

51 
apply (rule AC_well_ord [THEN exE]) 

13269  52 
apply (rule well_ord_cmult_assoc, assumption+) 
13134  53 
done 
54 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

55 
lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)" 
13134  56 
apply (rule AC_well_ord [THEN exE]) 
57 
apply (rule AC_well_ord [THEN exE]) 

58 
apply (rule AC_well_ord [THEN exE]) 

13269  59 
apply (rule well_ord_cadd_cmult_distrib, assumption+) 
13134  60 
done 
61 

46954  62 
lemma InfCard_square_eq: "InfCard(A) ==> A*A \<approx> A" 
13134  63 
apply (rule AC_well_ord [THEN exE]) 
13269  64 
apply (erule well_ord_InfCard_square_eq, assumption) 
13134  65 
done 
66 

67 

14046  68 
subsection {*The relationship between cardinality and lepollence*} 
13134  69 

46954  70 
lemma Card_le_imp_lepoll: 
71 
assumes "A \<le> B" shows "A \<lesssim> B" 

72 
proof  

73 
have "A \<approx> A" 

74 
by (rule cardinal_eqpoll [THEN eqpoll_sym]) 

75 
also have "... \<lesssim> B" 

76 
by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms) 

77 
also have "... \<approx> B" 

78 
by (rule cardinal_eqpoll) 

79 
finally show ?thesis . 

80 
qed 

13134  81 

46954  82 
lemma le_Card_iff: "Card(K) ==> A \<le> K \<longleftrightarrow> A \<lesssim> K" 
46820  83 
apply (erule Card_cardinal_eq [THEN subst], rule iffI, 
13269  84 
erule Card_le_imp_lepoll) 
46820  85 
apply (erule lepoll_imp_Card_le) 
13134  86 
done 
87 

46954  88 
lemma cardinal_0_iff_0 [simp]: "A = 0 \<longleftrightarrow> A = 0" 
46820  89 
apply auto 
14046  90 
apply (drule cardinal_0 [THEN ssubst]) 
91 
apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1]) 

92 
done 

93 

46954  94 
lemma cardinal_lt_iff_lesspoll: 
95 
assumes i: "Ord(i)" shows "i < A \<longleftrightarrow> i \<prec> A" 

96 
proof 

97 
assume "i < A" 

98 
hence "i \<prec> A" 

99 
by (blast intro: lt_Card_imp_lesspoll Card_cardinal) 

100 
also have "... \<approx> A" 

101 
by (rule cardinal_eqpoll) 

102 
finally show "i \<prec> A" . 

103 
next 

104 
assume "i \<prec> A" 

105 
also have "... \<approx> A" 

106 
by (blast intro: cardinal_eqpoll eqpoll_sym) 

107 
finally have "i \<prec> A" . 

108 
thus "i < A" using i 

109 
by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt) 

110 
qed 

14046  111 

112 
lemma cardinal_le_imp_lepoll: " i \<le> A ==> i \<lesssim> A" 

46954  113 
by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans) 
14046  114 

115 

116 
subsection{*Other Applications of AC*} 

117 

47052  118 
lemma surj_implies_inj: 
119 
assumes f: "f \<in> surj(X,Y)" shows "\<exists>g. g \<in> inj(Y,X)" 

120 
proof  

121 
from f AC_Pi [of Y "%y. f``{y}"] 

122 
obtain z where z: "z \<in> (\<Pi> y\<in>Y. f `` {y})" 

123 
by (auto simp add: surj_def) (fast dest: apply_Pair) 

124 
show ?thesis 

125 
proof 

126 
show "z \<in> inj(Y, X)" using z surj_is_fun [OF f] 

127 
by (blast dest: apply_type Pi_memberD 

128 
intro: apply_equality Pi_type f_imp_injective) 

129 
qed 

130 
qed 

13134  131 

47052  132 
text{*Kunen's Lemma 10.20*} 
133 
lemma surj_implies_cardinal_le: 

134 
assumes f: "f \<in> surj(X,Y)" shows "Y \<le> X" 

135 
proof (rule lepoll_imp_Card_le) 

136 
from f [THEN surj_implies_inj] obtain g where "g \<in> inj(Y,X)" .. 

137 
thus "Y \<lesssim> X" 

138 
by (auto simp add: lepoll_def) 

139 
qed 

13134  140 

47052  141 
text{*Kunen's Lemma 10.21*} 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

142 
lemma cardinal_UN_le: 
46963  143 
assumes K: "InfCard(K)" 
144 
shows "(!!i. i\<in>K ==> X(i) \<le> K) ==> \<Union>i\<in>K. X(i) \<le> K" 

145 
proof (simp add: K InfCard_is_Card le_Card_iff) 

146 
have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K) 

147 
assume "!!i. i\<in>K ==> X(i) \<lesssim> K" 

148 
hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def) 

149 
with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))" 

47052  150 
by force 
46963  151 
{ fix z 
152 
assume z: "z \<in> (\<Union>i\<in>K. X(i))" 

153 
then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)" 

154 
by (blast intro: Ord_in_Ord [of K]) 

155 
hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le) 

156 
hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i) 

157 
hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))" 

158 
by (auto intro: LeastI ltD i) 

159 
} note mems = this 

160 
have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K" 

161 
proof (unfold lepoll_def) 

162 
show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)" 

163 
apply (rule exI) 

164 
apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>" 

165 
and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective) 

166 
apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+ 

167 
done 

168 
qed 

169 
also have "... \<approx> K" 

170 
by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq) 

171 
finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" . 

172 
qed 

13134  173 

46963  174 
text{*The same again, using @{term csucc}*} 
13134  175 
lemma cardinal_UN_lt_csucc: 
47071
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

176 
"[ InfCard(K); \<And>i. i\<in>K \<Longrightarrow> X(i) < csucc(K) ] 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

177 
==> \<Union>i\<in>K. X(i) < csucc(K)" 
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

178 
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal) 
13134  179 

47052  180 
text{*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), 
181 
the least ordinal j such that i:Vfrom(A,j). *} 

13134  182 
lemma cardinal_UN_Ord_lt_csucc: 
47071
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

183 
"[ InfCard(K); \<And>i. i\<in>K \<Longrightarrow> j(i) < csucc(K) ] 
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset

184 
==> (\<Union>i\<in>K. j(i)) < csucc(K)" 
13269  185 
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption) 
13134  186 
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE) 
187 
apply (blast intro!: Ord_UN elim: ltE) 

188 
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc]) 

189 
done 

190 

191 

47071
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

192 
subsection{*The Main Result for InfiniteBranching Datatypes*} 
13134  193 

47071
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

194 
text{*As above, but the index set need not be a cardinal. Work 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

195 
backwards along the injection from @{term W} into @{term K}, given 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

196 
that @{term"W\<noteq>0"}.*} 
46954  197 

13134  198 
lemma inj_UN_subset: 
46954  199 
assumes f: "f \<in> inj(A,B)" and a: "a \<in> A" 
200 
shows "(\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" 

201 
proof (rule UN_least) 

202 
fix x 

203 
assume x: "x \<in> A" 

204 
hence fx: "f ` x \<in> B" by (blast intro: f inj_is_fun [THEN apply_type]) 

205 
have "C(x) \<subseteq> C(if f ` x \<in> range(f) then converse(f) ` (f ` x) else a)" 

206 
using f x by (simp add: inj_is_fun [THEN apply_rangeI]) 

207 
also have "... \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f) ` y else a))" 

208 
by (rule UN_upper [OF fx]) 

209 
finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" . 

210 
qed 

13134  211 

47071
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

212 
theorem le_UN_Ord_lt_csucc: 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

213 
assumes IK: "InfCard(K)" and WK: "W \<le> K" and j: "\<And>w. w\<in>W \<Longrightarrow> j(w) < csucc(K)" 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

214 
shows "(\<Union>w\<in>W. j(w)) < csucc(K)" 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

215 
proof  
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

216 
have CK: "Card(K)" 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

217 
by (simp add: InfCard_is_Card IK) 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

218 
then obtain f where f: "f \<in> inj(W, K)" using WK 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

219 
by(auto simp add: le_Card_iff lepoll_def) 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

220 
have OU: "Ord(\<Union>w\<in>W. j(w))" using j 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

221 
by (blast elim: ltE) 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

222 
note lt_subset_trans [OF _ _ OU, trans] 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

223 
show ?thesis 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

224 
proof (cases "W=0") 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

225 
case True {*solve the easy 0 case*} 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

226 
thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc) 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

227 
next 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

228 
case False 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

229 
then obtain x where x: "x \<in> W" by blast 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

230 
have "(\<Union>x\<in>W. j(x)) \<subseteq> (\<Union>k\<in>K. j(if k \<in> range(f) then converse(f) ` k else x))" 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

231 
by (rule inj_UN_subset [OF f x]) 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

232 
also have "... < csucc(K)" using IK 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

233 
proof (rule cardinal_UN_Ord_lt_csucc) 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

234 
fix k 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

235 
assume "k \<in> K" 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

236 
thus "j(if k \<in> range(f) then converse(f) ` k else x) < csucc(K)" using f x j 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

237 
by (simp add: inj_converse_fun [THEN apply_type]) 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

238 
qed 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

239 
finally show ?thesis . 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

240 
qed 
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
47052
diff
changeset

241 
qed 
13134  242 

243 
end 