19 |
19 |
20 Goalw [eqpoll_def] "A+B eqpoll B+A"; |
20 Goalw [eqpoll_def] "A+B eqpoll B+A"; |
21 by (rtac exI 1); |
21 by (rtac exI 1); |
22 by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")] |
22 by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")] |
23 lam_bijective 1); |
23 lam_bijective 1); |
24 by (safe_tac (claset() addSEs [sumE])); |
24 by Auto_tac; |
25 by (ALLGOALS (Asm_simp_tac)); |
|
26 qed "sum_commute_eqpoll"; |
25 qed "sum_commute_eqpoll"; |
27 |
26 |
28 Goalw [cadd_def] "i |+| j = j |+| i"; |
27 Goalw [cadd_def] "i |+| j = j |+| i"; |
29 by (rtac (sum_commute_eqpoll RS cardinal_cong) 1); |
28 by (rtac (sum_commute_eqpoll RS cardinal_cong) 1); |
30 qed "cadd_commute"; |
29 qed "cadd_commute"; |
270 Goalw [eqpoll_def] "succ(A)*B eqpoll B + A*B"; |
269 Goalw [eqpoll_def] "succ(A)*B eqpoll B + A*B"; |
271 by (rtac exI 1); |
270 by (rtac exI 1); |
272 by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"), |
271 by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"), |
273 ("d", "case(%y. <A,y>, %z. z)")] |
272 ("d", "case(%y. <A,y>, %z. z)")] |
274 lam_bijective 1); |
273 lam_bijective 1); |
275 by (safe_tac (claset() addSEs [sumE])); |
274 by Safe_tac; |
276 by (ALLGOALS |
275 by (ALLGOALS |
277 (asm_simp_tac (simpset() addsimps [succI2, if_type, mem_imp_not_eq]))); |
276 (asm_simp_tac (simpset() addsimps [succI2, if_type, mem_imp_not_eq]))); |
278 qed "prod_succ_eqpoll"; |
277 qed "prod_succ_eqpoll"; |
279 |
278 |
280 (*Unconditional version requires AC*) |
279 (*Unconditional version requires AC*) |
388 by (rtac pred_subset 1); |
387 by (rtac pred_subset 1); |
389 qed "ordermap_eqpoll_pred"; |
388 qed "ordermap_eqpoll_pred"; |
390 |
389 |
391 (** Establishing the well-ordering **) |
390 (** Establishing the well-ordering **) |
392 |
391 |
393 Goalw [inj_def] |
392 Goalw [inj_def] "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)"; |
394 "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)"; |
393 by (force_tac (claset() addIs [lam_type, Un_least_lt RS ltD, ltI], |
395 by (fast_tac (claset() addss (simpset()) |
394 simpset()) 1); |
396 addIs [lam_type, Un_least_lt RS ltD, ltI]) 1); |
|
397 qed "csquare_lam_inj"; |
395 qed "csquare_lam_inj"; |
398 |
396 |
399 Goalw [csquare_rel_def] |
397 Goalw [csquare_rel_def] "Ord(K) ==> well_ord(K*K, csquare_rel(K))"; |
400 "Ord(K) ==> well_ord(K*K, csquare_rel(K))"; |
|
401 by (rtac (csquare_lam_inj RS well_ord_rvimage) 1); |
398 by (rtac (csquare_lam_inj RS well_ord_rvimage) 1); |
402 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); |
399 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); |
403 qed "well_ord_csquare"; |
400 qed "well_ord_csquare"; |
404 |
401 |
405 (** Characterising initial segments of the well-ordering **) |
402 (** Characterising initial segments of the well-ordering **) |
406 |
403 |
407 Goalw [csquare_rel_def] |
404 Goalw [csquare_rel_def] |
408 "[| x<K; y<K; z<K |] ==> \ |
405 "[| <<x,y>, <z,z>> : csquare_rel(K); x<K; y<K; z<K |] ==> x le z & y le z"; |
409 \ <<x,y>, <z,z>> : csquare_rel(K) --> x le z & y le z"; |
406 by (etac rev_mp 1); |
410 by (REPEAT (etac ltE 1)); |
407 by (REPEAT (etac ltE 1)); |
411 by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
408 by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
412 Un_absorb, Un_least_mem_iff, ltD]) 1); |
409 Un_absorb, Un_least_mem_iff, ltD]) 1); |
413 by (safe_tac (claset() addSEs [mem_irrefl] |
410 by (safe_tac (claset() addSEs [mem_irrefl] |
414 addSIs [Un_upper1_le, Un_upper2_le])); |
411 addSIs [Un_upper1_le, Un_upper2_le])); |
415 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2, Ord_succ]))); |
412 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2, Ord_succ]))); |
416 qed_spec_mp "csquareD"; |
413 qed "csquareD"; |
417 |
414 |
418 Goalw [pred_def] |
415 Goalw [pred_def] |
419 "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"; |
416 "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"; |
420 by (safe_tac (claset_of ZF.thy addSEs [SigmaE])); (*avoids using succCI,...*) |
417 by (safe_tac (claset() delrules [SigmaI,succCI])); (*avoids using succCI,...*) |
421 by (rtac (csquareD RS conjE) 1); |
418 by (etac (csquareD RS conjE) 1); |
422 by (rewtac lt_def); |
419 by (rewtac lt_def); |
423 by (assume_tac 4); |
|
424 by (ALLGOALS Blast_tac); |
420 by (ALLGOALS Blast_tac); |
425 qed "pred_csquare_subset"; |
421 qed "pred_csquare_subset"; |
426 |
422 |
427 Goalw [csquare_rel_def] |
423 Goalw [csquare_rel_def] |
428 "[| x<z; y<z; z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K)"; |
424 "[| x<z; y<z; z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K)"; |