author  lcp 
Mon, 22 Aug 1994 11:11:17 +0200  
changeset 571  0b03ce5b62f7 
parent 522  e1de521e012a 
child 760  f0200e91b272 
permissions  rwrr 
435  1 
(* Title: ZF/Cardinal.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1994 University of Cambridge 

5 

6 
Cardinals in ZermeloFraenkel Set Theory 

7 

8 
This theory does NOT assume the Axiom of Choice 

9 
*) 

10 

11 
open Cardinal; 

12 

13 
(*** The SchroederBernstein Theorem  see Davey & Priestly, page 106 ***) 

14 

15 
(** Lemma: Banach's Decomposition Theorem **) 

16 

17 
goal Cardinal.thy "bnd_mono(X, %W. X  g``(Y  f``W))"; 

18 
by (rtac bnd_monoI 1); 

19 
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); 

20 
val decomp_bnd_mono = result(); 

21 

22 
val [gfun] = goal Cardinal.thy 

23 
"g: Y>X ==> \ 

24 
\ g``(Y  f`` lfp(X, %W. X  g``(Y  f``W))) = \ 

25 
\ X  lfp(X, %W. X  g``(Y  f``W)) "; 

26 
by (res_inst_tac [("P", "%u. ?v = Xu")] 

27 
(decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); 

28 
by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, 

29 
gfun RS fun_is_rel RS image_subset]) 1); 

30 
val Banach_last_equation = result(); 

31 

32 
val prems = goal Cardinal.thy 

33 
"[ f: X>Y; g: Y>X ] ==> \ 

34 
\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ 

35 
\ (YA Int YB = 0) & (YA Un YB = Y) & \ 

36 
\ f``XA=YA & g``YB=XB"; 

37 
by (REPEAT 

38 
(FIRSTGOAL 

39 
(resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); 

40 
by (rtac Banach_last_equation 3); 

41 
by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); 

42 
val decomposition = result(); 

43 

44 
val prems = goal Cardinal.thy 

45 
"[ f: inj(X,Y); g: inj(Y,X) ] ==> EX h. h: bij(X,Y)"; 

46 
by (cut_facts_tac prems 1); 

47 
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); 

48 
by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] 

49 
addIs [bij_converse_bij]) 1); 

50 
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" 

51 
is forced by the context!! *) 

52 
val schroeder_bernstein = result(); 

53 

54 

55 
(** Equipollence is an equivalence relation **) 

56 

57 
goalw Cardinal.thy [eqpoll_def] "X eqpoll X"; 

437  58 
by (rtac exI 1); 
59 
by (rtac id_bij 1); 

435  60 
val eqpoll_refl = result(); 
61 

62 
goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X"; 

63 
by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1); 

64 
val eqpoll_sym = result(); 

65 

66 
goalw Cardinal.thy [eqpoll_def] 

67 
"!!X Y. [ X eqpoll Y; Y eqpoll Z ] ==> X eqpoll Z"; 

68 
by (fast_tac (ZF_cs addIs [comp_bij]) 1); 

69 
val eqpoll_trans = result(); 

70 

71 
(** Lepollence is a partial ordering **) 

72 

73 
goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y"; 

437  74 
by (rtac exI 1); 
75 
by (etac id_subset_inj 1); 

435  76 
val subset_imp_lepoll = result(); 
77 

78 
val lepoll_refl = subset_refl RS subset_imp_lepoll; 

79 

80 
goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def] 

81 
"!!X Y. X eqpoll Y ==> X lepoll Y"; 

82 
by (fast_tac ZF_cs 1); 

83 
val eqpoll_imp_lepoll = result(); 

84 

85 
goalw Cardinal.thy [lepoll_def] 

86 
"!!X Y. [ X lepoll Y; Y lepoll Z ] ==> X lepoll Z"; 

87 
by (fast_tac (ZF_cs addIs [comp_inj]) 1); 

88 
val lepoll_trans = result(); 

89 

90 
(*Asymmetry law*) 

91 
goalw Cardinal.thy [lepoll_def,eqpoll_def] 

92 
"!!X Y. [ X lepoll Y; Y lepoll X ] ==> X eqpoll Y"; 

93 
by (REPEAT (etac exE 1)); 

94 
by (rtac schroeder_bernstein 1); 

95 
by (REPEAT (assume_tac 1)); 

96 
val eqpollI = result(); 

97 

98 
val [major,minor] = goal Cardinal.thy 

99 
"[ X eqpoll Y; [ X lepoll Y; Y lepoll X ] ==> P ] ==> P"; 

437  100 
by (rtac minor 1); 
435  101 
by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1)); 
102 
val eqpollE = result(); 

103 

104 
goal Cardinal.thy "X eqpoll Y <> X lepoll Y & Y lepoll X"; 

105 
by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1); 

106 
val eqpoll_iff = result(); 

107 

108 

109 
(** LEAST  the least number operator [from HOL/Univ.ML] **) 

110 

111 
val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def] 

112 
"[ P(i); Ord(i); !!x. x<i ==> ~P(x) ] ==> (LEAST x.P(x)) = i"; 

113 
by (rtac the_equality 1); 

114 
by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1); 

115 
by (REPEAT (etac conjE 1)); 

437  116 
by (etac (premOrd RS Ord_linear_lt) 1); 
435  117 
by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot]))); 
118 
val Least_equality = result(); 

119 

120 
goal Cardinal.thy "!!i. [ P(i); Ord(i) ] ==> P(LEAST x.P(x))"; 

121 
by (etac rev_mp 1); 

122 
by (trans_ind_tac "i" [] 1); 

123 
by (rtac impI 1); 

124 
by (rtac classical 1); 

125 
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); 

126 
by (assume_tac 2); 

127 
by (fast_tac (ZF_cs addSEs [ltE]) 1); 

128 
val LeastI = result(); 

129 

130 
(*Proof is almost identical to the one above!*) 

131 
goal Cardinal.thy "!!i. [ P(i); Ord(i) ] ==> (LEAST x.P(x)) le i"; 

132 
by (etac rev_mp 1); 

133 
by (trans_ind_tac "i" [] 1); 

134 
by (rtac impI 1); 

135 
by (rtac classical 1); 

136 
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); 

137 
by (etac le_refl 2); 

138 
by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1); 

139 
val Least_le = result(); 

140 

141 
(*LEAST really is the smallest*) 

142 
goal Cardinal.thy "!!i. [ P(i); i < (LEAST x.P(x)) ] ==> Q"; 

437  143 
by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1); 
435  144 
by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); 
145 
val less_LeastE = result(); 

146 

437  147 
(*If there is no such P then LEAST is vacuously 0*) 
148 
goalw Cardinal.thy [Least_def] 

149 
"!!P. [ ~ (EX i. Ord(i) & P(i)) ] ==> (LEAST x.P(x)) = 0"; 

150 
by (rtac the_0 1); 

151 
by (fast_tac ZF_cs 1); 

152 
val Least_0 = result(); 

153 

435  154 
goal Cardinal.thy "Ord(LEAST x.P(x))"; 
437  155 
by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1); 
435  156 
by (safe_tac ZF_cs); 
437  157 
by (rtac (Least_le RS ltE) 2); 
435  158 
by (REPEAT_SOME assume_tac); 
437  159 
by (etac (Least_0 RS ssubst) 1); 
160 
by (rtac Ord_0 1); 

435  161 
val Ord_Least = result(); 
162 

163 

164 
(** Basic properties of cardinals **) 

165 

166 
(*Not needed for simplification, but helpful below*) 

167 
val prems = goal Cardinal.thy 

168 
"[ !!y. P(y) <> Q(y) ] ==> (LEAST x.P(x)) = (LEAST x.Q(x))"; 

169 
by (simp_tac (FOL_ss addsimps prems) 1); 

170 
val Least_cong = result(); 

171 

172 
(*Need AC to prove X lepoll Y ==> X le Y ; see well_ord_lepoll_imp_le *) 

173 
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> X = Y"; 

437  174 
by (rtac Least_cong 1); 
435  175 
by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); 
176 
val cardinal_cong = result(); 

177 

178 
(*Under AC, the premise becomes trivial; one consequence is A = A*) 

179 
goalw Cardinal.thy [eqpoll_def, cardinal_def] 

180 
"!!A. well_ord(A,r) ==> A eqpoll A"; 

437  181 
by (rtac LeastI 1); 
182 
by (etac Ord_ordertype 2); 

183 
by (rtac exI 1); 

467  184 
by (etac (ordermap_bij RS bij_converse_bij) 1); 
435  185 
val well_ord_cardinal_eqpoll = result(); 
186 

187 
val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll 

188 
> standard; 

189 

190 
goal Cardinal.thy 

191 
"!!X Y. [ well_ord(X,r); well_ord(Y,s); X = Y ] ==> X eqpoll Y"; 

437  192 
by (rtac (eqpoll_sym RS eqpoll_trans) 1); 
193 
by (etac well_ord_cardinal_eqpoll 1); 

435  194 
by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); 
195 
val well_ord_cardinal_eqE = result(); 

196 

197 

198 
(** Observations from Kunen, page 28 **) 

199 

200 
goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> i le i"; 

437  201 
by (etac (eqpoll_refl RS Least_le) 1); 
435  202 
val Ord_cardinal_le = result(); 
203 

484  204 
goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> K = K"; 
437  205 
by (etac sym 1); 
435  206 
val Card_cardinal_eq = result(); 
207 

208 
val prems = goalw Cardinal.thy [Card_def,cardinal_def] 

209 
"[ Ord(i); !!j. j<i ==> ~(j eqpoll i) ] ==> Card(i)"; 

437  210 
by (rtac (Least_equality RS ssubst) 1); 
435  211 
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); 
212 
val CardI = result(); 

213 

214 
goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; 

437  215 
by (etac ssubst 1); 
216 
by (rtac Ord_Least 1); 

435  217 
val Card_is_Ord = result(); 
218 

484  219 
goalw Cardinal.thy [cardinal_def] "Ord(A)"; 
437  220 
by (rtac Ord_Least 1); 
435  221 
val Ord_cardinal = result(); 
222 

437  223 
goal Cardinal.thy "Card(0)"; 
224 
by (rtac (Ord_0 RS CardI) 1); 

225 
by (fast_tac (ZF_cs addSEs [ltE]) 1); 

226 
val Card_0 = result(); 

227 

522  228 
val [premK,premL] = goal Cardinal.thy 
229 
"[ Card(K); Card(L) ] ==> Card(K Un L)"; 

230 
by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1); 

231 
by (asm_simp_tac 

232 
(ZF_ss addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1); 

233 
by (asm_simp_tac 

234 
(ZF_ss addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1); 

235 
val Card_Un = result(); 

236 

237 
(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) 

238 

484  239 
goalw Cardinal.thy [cardinal_def] "Card(A)"; 
437  240 
by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1); 
241 
by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1); 

242 
by (rtac (Ord_Least RS CardI) 1); 

243 
by (safe_tac ZF_cs); 

244 
by (rtac less_LeastE 1); 

245 
by (assume_tac 2); 

246 
by (etac eqpoll_trans 1); 

247 
by (REPEAT (ares_tac [LeastI] 1)); 

248 
val Card_cardinal = result(); 

249 

435  250 
(*Kunen's Lemma 10.5*) 
251 
goal Cardinal.thy "!!i j. [ i le j; j le i ] ==> j = i"; 

437  252 
by (rtac (eqpollI RS cardinal_cong) 1); 
253 
by (etac (le_imp_subset RS subset_imp_lepoll) 1); 

254 
by (rtac lepoll_trans 1); 

255 
by (etac (le_imp_subset RS subset_imp_lepoll) 2); 

256 
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1); 

257 
by (rtac Ord_cardinal_eqpoll 1); 

435  258 
by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); 
259 
val cardinal_eq_lemma = result(); 

260 

261 
goal Cardinal.thy "!!i j. i le j ==> i le j"; 

262 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); 

263 
by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); 

437  264 
by (rtac cardinal_eq_lemma 1); 
265 
by (assume_tac 2); 

266 
by (etac le_trans 1); 

267 
by (etac ltE 1); 

268 
by (etac Ord_cardinal_le 1); 

435  269 
val cardinal_mono = result(); 
270 

271 
(*Since we have succ(nat) le nat, the converse of cardinal_mono fails!*) 

272 
goal Cardinal.thy "!!i j. [ i < j; Ord(i); Ord(j) ] ==> i < j"; 

437  273 
by (rtac Ord_linear2 1); 
435  274 
by (REPEAT_SOME assume_tac); 
437  275 
by (etac (lt_trans2 RS lt_irrefl) 1); 
276 
by (etac cardinal_mono 1); 

435  277 
val cardinal_lt_imp_lt = result(); 
278 

484  279 
goal Cardinal.thy "!!i j. [ i < K; Ord(i); Card(K) ] ==> i < K"; 
435  280 
by (asm_simp_tac (ZF_ss addsimps 
281 
[cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); 

282 
val Card_lt_imp_lt = result(); 

283 

484  284 
goal Cardinal.thy "!!i j. [ Ord(i); Card(K) ] ==> (i < K) <> (i < K)"; 
285 
by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1); 

286 
val Card_lt_iff = result(); 

287 

288 
goal Cardinal.thy "!!i j. [ Ord(i); Card(K) ] ==> (K le i) <> (K le i)"; 

289 
by (asm_simp_tac (ZF_ss addsimps 

290 
[Card_lt_iff, Card_is_Ord, Ord_cardinal, 

291 
not_lt_iff_le RS iff_sym]) 1); 

292 
val Card_le_iff = result(); 

293 

435  294 

295 
(** The swap operator [NOT USED] **) 

296 

297 
goalw Cardinal.thy [swap_def] 

298 
"!!A. [ x:A; y:A ] ==> swap(A,x,y) : A>A"; 

299 
by (REPEAT (ares_tac [lam_type,if_type] 1)); 

300 
val swap_type = result(); 

301 

302 
goalw Cardinal.thy [swap_def] 

303 
"!!A. [ x:A; y:A; z:A ] ==> swap(A,x,y)`(swap(A,x,y)`z) = z"; 

304 
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); 

305 
val swap_swap_identity = result(); 

306 

307 
goal Cardinal.thy "!!A. [ x:A; y:A ] ==> swap(A,x,y) : bij(A,A)"; 

437  308 
by (rtac nilpotent_imp_bijective 1); 
435  309 
by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2, 
310 
ballI, swap_swap_identity] 1)); 

311 
val swap_bij = result(); 

312 

313 
(*** The finite cardinals ***) 

314 

315 
(*Lemma suggested by Mike Fourman*) 

316 
val [prem] = goalw Cardinal.thy [inj_def] 

317 
"f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)"; 

437  318 
by (rtac CollectI 1); 
435  319 
(*Proving it's in the function space m>n*) 
320 
by (cut_facts_tac [prem] 1); 

437  321 
by (rtac (if_type RS lam_type) 1); 
322 
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1); 

323 
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1); 

435  324 
(*Proving it's injective*) 
325 
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); 

326 
(*Adding prem earlier would cause the simplifier to loop*) 

327 
by (cut_facts_tac [prem] 1); 

437  328 
by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1); 
435  329 
val inj_succ_succD = result(); 
330 

331 
val [prem] = goalw Cardinal.thy [lepoll_def] 

332 
"m:nat ==> ALL n: nat. m lepoll n > m le n"; 

333 
by (nat_ind_tac "m" [prem] 1); 

334 
by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); 

437  335 
by (rtac ballI 1); 
435  336 
by (eres_inst_tac [("n","n")] natE 1); 
337 
by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); 

338 
by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1); 

339 
val nat_lepoll_imp_le_lemma = result(); 

340 
val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp > standard; 

341 

342 
goal Cardinal.thy 

343 
"!!m n. [ m:nat; n: nat ] ==> m eqpoll n <> m = n"; 

437  344 
by (rtac iffI 1); 
435  345 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); 
437  346 
by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] 
347 
addSEs [eqpollE]) 1); 

435  348 
val nat_eqpoll_iff = result(); 
349 

350 
goalw Cardinal.thy [Card_def,cardinal_def] 

351 
"!!n. n: nat ==> Card(n)"; 

437  352 
by (rtac (Least_equality RS ssubst) 1); 
435  353 
by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); 
354 
by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); 

437  355 
by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1); 
435  356 
val nat_into_Card = result(); 
357 

358 
(*Part of Kunen's Lemma 10.6*) 

359 
goal Cardinal.thy "!!n. [ succ(n) lepoll n; n:nat ] ==> P"; 

437  360 
by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); 
435  361 
by (REPEAT (ares_tac [nat_succI] 1)); 
362 
val succ_lepoll_natE = result(); 

363 

364 

365 
(*** The first infinite cardinal: Omega, or nat ***) 

366 

367 
(*This implies Kunen's Lemma 10.6*) 

368 
goal Cardinal.thy "!!n. [ n<i; n:nat ] ==> ~ i lepoll n"; 

437  369 
by (rtac notI 1); 
435  370 
by (rtac succ_lepoll_natE 1 THEN assume_tac 2); 
371 
by (rtac lepoll_trans 1 THEN assume_tac 2); 

437  372 
by (etac ltE 1); 
435  373 
by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); 
374 
val lt_not_lepoll = result(); 

375 

376 
goal Cardinal.thy "!!i n. [ Ord(i); n:nat ] ==> i eqpoll n <> i=n"; 

437  377 
by (rtac iffI 1); 
435  378 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); 
379 
by (rtac Ord_linear_lt 1); 

380 
by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); 

381 
by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN 

382 
REPEAT (assume_tac 1)); 

383 
by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); 

437  384 
by (etac eqpoll_imp_lepoll 1); 
435  385 
val Ord_nat_eqpoll_iff = result(); 
386 

437  387 
goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; 
388 
by (rtac (Least_equality RS ssubst) 1); 

389 
by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); 

390 
by (etac ltE 1); 

391 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); 

392 
val Card_nat = result(); 

435  393 

437  394 
(*Allows showing that i is a limit cardinal*) 
395 
goal Cardinal.thy "!!i. nat le i ==> nat le i"; 

396 
by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1); 

397 
by (etac cardinal_mono 1); 

398 
val nat_le_cardinal = result(); 

399 

571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

400 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

401 
(*** Towards Cardinal Arithmetic ***) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

402 
(** Congruence laws for successor, cardinal addition and multiplication **) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

403 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

404 
val case_ss = ZF_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff, 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

405 
case_Inl, case_Inr, InlI, InrI]; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

406 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

407 
val bij_inverse_ss = 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

408 
case_ss addsimps [bij_is_fun RS apply_type, 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

409 
bij_converse_bij RS bij_is_fun RS apply_type, 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

410 
left_inverse_bij, right_inverse_bij]; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

411 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

412 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

413 
(*Congruence law for cons under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

414 
goalw Cardinal.thy [lepoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

415 
"!!A B. [ A lepoll B; b ~: B ] ==> cons(a,A) lepoll cons(b,B)"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

416 
by (safe_tac ZF_cs); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

417 
by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

418 
by (res_inst_tac [("d","%z.if(z:B, converse(f)`z, a)")] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

419 
lam_injective 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

420 
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, cons_iff] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

421 
setloop etac consE') 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

422 
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

423 
setloop etac consE') 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

424 
val cons_lepoll_cong = result(); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

425 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

426 
goal Cardinal.thy 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

427 
"!!A B. [ A eqpoll B; a ~: A; b ~: B ] ==> cons(a,A) eqpoll cons(b,B)"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

428 
by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff, cons_lepoll_cong]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

429 
val cons_eqpoll_cong = result(); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

430 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

431 
(*Congruence law for succ under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

432 
goalw Cardinal.thy [succ_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

433 
"!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

434 
by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

435 
val succ_eqpoll_cong = result(); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

436 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

437 
(*Congruence law for + under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

438 
goalw Cardinal.thy [eqpoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

439 
"!!A B C D. [ A eqpoll C; B eqpoll D ] ==> A+B eqpoll C+D"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

440 
by (safe_tac ZF_cs); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

441 
by (rtac exI 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

442 
by (res_inst_tac [("c", "case(%x. Inl(f`x), %y. Inr(fa`y))"), 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

443 
("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

444 
lam_bijective 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

445 
by (safe_tac (ZF_cs addSEs [sumE])); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

446 
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

447 
val sum_eqpoll_cong = result(); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

448 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

449 
(*Congruence law for * under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

450 
goalw Cardinal.thy [eqpoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

451 
"!!A B C D. [ A eqpoll C; B eqpoll D ] ==> A*B eqpoll C*D"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

452 
by (safe_tac ZF_cs); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

453 
by (rtac exI 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

454 
by (res_inst_tac [("c", "split(%x y. <f`x, fa`y>)"), 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

455 
("d", "split(%x y. <converse(f)`x, converse(fa)`y>)")] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

456 
lam_bijective 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

457 
by (safe_tac ZF_cs); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

458 
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

459 
val prod_eqpoll_cong = result(); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

460 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

461 
goalw Cardinal.thy [eqpoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

462 
"!!f. [ f: inj(A,B); A Int B = 0 ] ==> A Un (B  range(f)) eqpoll B"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

463 
by (rtac exI 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

464 
by (res_inst_tac [("c", "%x. if(x:A, f`x, x)"), 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

465 
("d", "%y. if(y: range(f), converse(f)`y, y)")] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

466 
lam_bijective 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

467 
by (fast_tac (ZF_cs addSIs [if_type, apply_type] addIs [inj_is_fun]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

468 
by (asm_simp_tac 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

469 
(ZF_ss addsimps [inj_converse_fun RS apply_funtype] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

470 
setloop split_tac [expand_if]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

471 
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

472 
setloop etac UnE') 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

473 
by (asm_simp_tac 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

474 
(ZF_ss addsimps [inj_converse_fun RS apply_funtype, right_inverse] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

475 
setloop split_tac [expand_if]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

476 
by (fast_tac (ZF_cs addEs [equals0D]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

477 
val inj_disjoint_eqpoll = result(); 