author  clasohm 
Wed, 14 Dec 1994 11:41:49 +0100  
changeset 782  200a16083201 
parent 765  06a484afc603 
child 792  5d2a7634da46 
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)); 

760  20 
qed "decomp_bnd_mono"; 
435  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); 

760  30 
qed "Banach_last_equation"; 
435  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)); 

760  42 
qed "decomposition"; 
435  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!! *) 

760  52 
qed "schroeder_bernstein"; 
435  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); 

760  60 
qed "eqpoll_refl"; 
435  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); 

760  64 
qed "eqpoll_sym"; 
435  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); 

760  69 
qed "eqpoll_trans"; 
435  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); 

760  76 
qed "subset_imp_lepoll"; 
435  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); 

760  83 
qed "eqpoll_imp_lepoll"; 
435  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); 

760  88 
qed "lepoll_trans"; 
435  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)); 

760  96 
qed "eqpollI"; 
435  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)); 
760  102 
qed "eqpollE"; 
435  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); 

760  106 
qed "eqpoll_iff"; 
435  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]))); 
760  118 
qed "Least_equality"; 
435  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); 

760  128 
qed "LeastI"; 
435  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); 

760  139 
qed "Least_le"; 
435  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)); 
760  145 
qed "less_LeastE"; 
435  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); 

760  152 
qed "Least_0"; 
437  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); 

760  161 
qed "Ord_Least"; 
435  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); 

760  170 
qed "Least_cong"; 
435  171 

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

435  174 
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> X = Y"; 
437  175 
by (rtac Least_cong 1); 
435  176 
by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); 
760  177 
qed "cardinal_cong"; 
435  178 

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

180 
goalw Cardinal.thy [eqpoll_def, cardinal_def] 

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

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

184 
by (rtac exI 1); 

467  185 
by (etac (ordermap_bij RS bij_converse_bij) 1); 
760  186 
qed "well_ord_cardinal_eqpoll"; 
435  187 

188 
val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll 

189 
> standard; 

190 

191 
goal Cardinal.thy 

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

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

435  195 
by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); 
760  196 
qed "well_ord_cardinal_eqE"; 
435  197 

198 

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

200 

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

437  202 
by (etac (eqpoll_refl RS Least_le) 1); 
760  203 
qed "Ord_cardinal_le"; 
435  204 

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

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

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

437  211 
by (rtac (Least_equality RS ssubst) 1); 
435  212 
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); 
760  213 
qed "CardI"; 
435  214 

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

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

760  218 
qed "Card_is_Ord"; 
435  219 

765  220 
goal Cardinal.thy "!!K. Card(K) ==> K le K"; 
221 
by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
765
diff
changeset

222 
qed "Card_cardinal_le"; 
765  223 

484  224 
goalw Cardinal.thy [cardinal_def] "Ord(A)"; 
437  225 
by (rtac Ord_Least 1); 
760  226 
qed "Ord_cardinal"; 
435  227 

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

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

760  231 
qed "Card_0"; 
437  232 

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

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

236 
by (asm_simp_tac 

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

238 
by (asm_simp_tac 

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

760  240 
qed "Card_Un"; 
522  241 

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

243 

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

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

248 
by (safe_tac ZF_cs); 

249 
by (rtac less_LeastE 1); 

250 
by (assume_tac 2); 

251 
by (etac eqpoll_trans 1); 

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

760  253 
qed "Card_cardinal"; 
437  254 

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

437  257 
by (rtac (eqpollI RS cardinal_cong) 1); 
258 
by (etac (le_imp_subset RS subset_imp_lepoll) 1); 

259 
by (rtac lepoll_trans 1); 

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

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

262 
by (rtac Ord_cardinal_eqpoll 1); 

435  263 
by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); 
760  264 
qed "cardinal_eq_lemma"; 
435  265 

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

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

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

437  269 
by (rtac cardinal_eq_lemma 1); 
270 
by (assume_tac 2); 

271 
by (etac le_trans 1); 

272 
by (etac ltE 1); 

273 
by (etac Ord_cardinal_le 1); 

760  274 
qed "cardinal_mono"; 
435  275 

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

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

437  278 
by (rtac Ord_linear2 1); 
435  279 
by (REPEAT_SOME assume_tac); 
437  280 
by (etac (lt_trans2 RS lt_irrefl) 1); 
281 
by (etac cardinal_mono 1); 

760  282 
qed "cardinal_lt_imp_lt"; 
435  283 

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

760  287 
qed "Card_lt_imp_lt"; 
435  288 

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

760  291 
qed "Card_lt_iff"; 
484  292 

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

294 
by (asm_simp_tac (ZF_ss addsimps 

295 
[Card_lt_iff, Card_is_Ord, Ord_cardinal, 

296 
not_lt_iff_le RS iff_sym]) 1); 

760  297 
qed "Card_le_iff"; 
484  298 

435  299 

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

301 

302 
goalw Cardinal.thy [swap_def] 

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

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

760  305 
qed "swap_type"; 
435  306 

307 
goalw Cardinal.thy [swap_def] 

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

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

760  310 
qed "swap_swap_identity"; 
435  311 

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

437  313 
by (rtac nilpotent_imp_bijective 1); 
435  314 
by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2, 
315 
ballI, swap_swap_identity] 1)); 

760  316 
qed "swap_bij"; 
435  317 

318 
(*** The finite cardinals ***) 

319 

320 
(*Lemma suggested by Mike Fourman*) 

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

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

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

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

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

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

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

332 
by (cut_facts_tac [prem] 1); 

437  333 
by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1); 
760  334 
qed "inj_succ_succD"; 
435  335 

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

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

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

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

437  340 
by (rtac ballI 1); 
435  341 
by (eres_inst_tac [("n","n")] natE 1); 
342 
by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); 

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

760  344 
qed "nat_lepoll_imp_le_lemma"; 
435  345 
val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp > standard; 
346 

347 
goal Cardinal.thy 

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

437  349 
by (rtac iffI 1); 
435  350 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); 
437  351 
by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] 
352 
addSEs [eqpollE]) 1); 

760  353 
qed "nat_eqpoll_iff"; 
435  354 

355 
goalw Cardinal.thy [Card_def,cardinal_def] 

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

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

437  360 
by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1); 
760  361 
qed "nat_into_Card"; 
435  362 

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

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

437  365 
by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); 
435  366 
by (REPEAT (ares_tac [nat_succI] 1)); 
760  367 
qed "succ_lepoll_natE"; 
435  368 

369 

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

371 

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

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

437  374 
by (rtac notI 1); 
435  375 
by (rtac succ_lepoll_natE 1 THEN assume_tac 2); 
376 
by (rtac lepoll_trans 1 THEN assume_tac 2); 

437  377 
by (etac ltE 1); 
435  378 
by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); 
760  379 
qed "lt_not_lepoll"; 
435  380 

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

437  382 
by (rtac iffI 1); 
435  383 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); 
384 
by (rtac Ord_linear_lt 1); 

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

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

387 
REPEAT (assume_tac 1)); 

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

437  389 
by (etac eqpoll_imp_lepoll 1); 
760  390 
qed "Ord_nat_eqpoll_iff"; 
435  391 

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

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

395 
by (etac ltE 1); 

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

760  397 
qed "Card_nat"; 
435  398 

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

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

402 
by (etac cardinal_mono 1); 

760  403 
qed "nat_le_cardinal"; 
437  404 

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

405 

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

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

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

408 

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

409 
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

410 
case_Inl, case_Inr, InlI, InrI]; 
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 
val bij_inverse_ss = 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

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

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

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

416 

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

417 

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

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

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

420 
"!!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

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

422 
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

423 
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

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

425 
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

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

427 
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

428 
setloop etac consE') 1); 
760  429 
qed "cons_lepoll_cong"; 
571
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 
goal Cardinal.thy 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

432 
"!!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

433 
by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff, cons_lepoll_cong]) 1); 
760  434 
qed "cons_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

435 

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

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

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

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

439 
by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); 
760  440 
qed "succ_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

441 

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

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

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

444 
"!!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

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

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

447 
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

448 
("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

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

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

451 
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); 
760  452 
qed "sum_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

453 

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

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

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

456 
"!!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

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

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

459 
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

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

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

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

463 
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); 
760  464 
qed "prod_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

465 

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

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

467 
"!!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

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

469 
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

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

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

472 
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

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] 
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 (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

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

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

479 
(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

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

481 
by (fast_tac (ZF_cs addEs [equals0D]) 1); 
760  482 
qed "inj_disjoint_eqpoll"; 