# HG changeset patch # User lcp # Date 789845437 -3600 # Node ID c4566750dc12dde23f258667fcfb4be2772fb9c1 # Parent 825e96b87ef7cd91f2d4a69770185eaa8cab72d0 Now proof of Ord_jump_cardinal uses ordertype_pred_unfold; proof of sum_0_eqpoll uses bij_0_sum; proof of sum_0_eqpoll uses sum_prod_distrib_bij; proof of sum_assoc_eqpoll uses sum_assoc_bij; proof of prod_assoc_eqpoll uses prod_assoc_bij. Proved well_ord_cadd_cmult_distrib. diff -r 825e96b87ef7 -r c4566750dc12 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Wed Jan 11 18:21:39 1995 +0100 +++ b/src/ZF/CardinalArith.ML Wed Jan 11 18:30:37 1995 +0100 @@ -5,10 +5,10 @@ Cardinal arithmetic -- WITHOUT the Axiom of Choice -Note: Could omit proving the associative laws for cardinal addition and +Note: Could omit proving the algebraic laws for cardinal addition and multiplication. On finite cardinals these operations coincide with addition and multiplication of natural numbers; on infinite cardinals they -coincide with union (maximum). Either way we get associativity for free. +coincide with union (maximum). Either way we get most laws for free. *) open CardinalArith; @@ -63,10 +63,7 @@ goalw CardinalArith.thy [eqpoll_def] "(A+B)+C eqpoll A+(B+C)"; by (rtac exI 1); -by (res_inst_tac [("c", "case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)))"), - ("d", "case(%x.Inl(Inl(x)), case(%x.Inl(Inr(x)), Inr))")] - lam_bijective 1); -by (ALLGOALS (asm_simp_tac (case_ss setloop etac sumE))); +by (resolve_tac [sum_assoc_bij] 1); qed "sum_assoc_eqpoll"; (*Unconditional version requires AC*) @@ -86,9 +83,7 @@ goalw CardinalArith.thy [eqpoll_def] "0+A eqpoll A"; by (rtac exI 1); -by (res_inst_tac [("c", "case(%x.x, %y.y)"), ("d", "Inr")] - lam_bijective 1); -by (ALLGOALS (asm_simp_tac (case_ss setloop eresolve_tac [sumE,emptyE]))); +by (rtac bij_0_sum 1); qed "sum_0_eqpoll"; goalw CardinalArith.thy [cadd_def] "!!K. Card(K) ==> 0 |+| K = K"; @@ -121,7 +116,7 @@ by (res_inst_tac [("d", "case(%w. Inl(converse(f)`w), %y. Inr(converse(fa)`y))")] lam_injective 1); -by (typechk_tac ([inj_is_fun,case_type, InlI, InrI] @ ZF_typechecks)); +by (typechk_tac ([inj_is_fun, case_type, InlI, InrI] @ ZF_typechecks)); by (etac sumE 1); by (ALLGOALS (asm_simp_tac (sum_ss addsimps [left_inverse]))); qed "sum_lepoll_mono"; @@ -187,11 +182,7 @@ goalw CardinalArith.thy [eqpoll_def] "(A*B)*C eqpoll A*(B*C)"; by (rtac exI 1); -by (res_inst_tac [("c", "split(%w z. split(%x y. >, w))"), - ("d", "split(%x. split(%y z. <, z>))")] - lam_bijective 1); -by (safe_tac ZF_cs); -by (ALLGOALS (asm_simp_tac ZF_ss)); +by (resolve_tac [prod_assoc_bij] 1); qed "prod_assoc_eqpoll"; (*Unconditional version requires AC*) @@ -211,14 +202,21 @@ goalw CardinalArith.thy [eqpoll_def] "(A+B)*C eqpoll (A*C)+(B*C)"; by (rtac exI 1); -by (res_inst_tac - [("c", "split(%x z. case(%y.Inl(), %y.Inr(), x))"), - ("d", "case(split(%x y.), split(%x y.))")] - lam_bijective 1); -by (safe_tac (ZF_cs addSEs [sumE])); -by (ALLGOALS (asm_simp_tac case_ss)); +by (resolve_tac [sum_prod_distrib_bij] 1); qed "sum_prod_distrib_eqpoll"; +goalw CardinalArith.thy [cadd_def, cmult_def] + "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ +\ (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"; +by (rtac cardinal_cong 1); +by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS + eqpoll_trans) 1); +by (rtac (sum_prod_distrib_eqpoll RS eqpoll_trans) 2); +by (rtac ([well_ord_cardinal_eqpoll, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS + eqpoll_sym) 2); +by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd] 1)); +qed "well_ord_cadd_cmult_distrib"; + (** Multiplication by 0 yields 0 **) goalw CardinalArith.thy [eqpoll_def] "0*A eqpoll 0"; @@ -236,9 +234,7 @@ goalw CardinalArith.thy [eqpoll_def] "{x}*A eqpoll A"; by (rtac exI 1); -by (res_inst_tac [("c", "snd"), ("d", "%z.")] lam_bijective 1); -by (safe_tac ZF_cs); -by (ALLGOALS (asm_simp_tac ZF_ss)); +by (resolve_tac [singleton_prod_bij RS bij_converse_bij] 1); qed "prod_singleton_eqpoll"; goalw CardinalArith.thy [cmult_def, succ_def] "!!K. Card(K) ==> 1 |*| K = K"; @@ -479,12 +475,12 @@ (** The cardinality of initial segments **) goal CardinalArith.thy - "!!K. [| InfCard(K); x \ + "!!K. [| Limit(K); x \ \ ordermap(K*K, csquare_rel(K)) ` lepoll \ \ ordermap(K*K, csquare_rel(K)) ` "; by (subgoals_tac ["z: K*K has no more than z*z predecessors..." (page 29) *) goalw CardinalArith.thy [cmult_def] - "!!K. [| InfCard(K); x \ + "!!K. [| Limit(K); x \ \ | ordermap(K*K, csquare_rel(K)) ` | le |succ(z)| |*| |succ(z)|"; by (rtac (well_ord_rmult RS well_ord_lepoll_imp_Card_le) 1); by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1)); by (subgoals_tac ["z K |*| K = |ordertype(K*K, csquare_rel(K))|"; -by (rtac cardinal_cong 1); -by (rewtac eqpoll_def); -by (rtac exI 1); -by (etac (well_ord_csquare RS ordermap_bij) 1); -qed "csquare_eq_ordertype"; - (*Main result: Kunen's Theorem 10.12*) goal CardinalArith.thy "!!K. InfCard(K) ==> K |*| K = K"; by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); @@ -568,7 +554,9 @@ by (assume_tac 2); by (assume_tac 2); by (asm_simp_tac - (ZF_ss addsimps [csquare_eq_ordertype, Ord_cardinal_le, + (ZF_ss addsimps [cmult_def, Ord_cardinal_le, + well_ord_csquare RS ordermap_bij RS + bij_imp_eqpoll RS cardinal_cong, well_ord_csquare RS Ord_ordertype]) 1); qed "InfCard_csquare_eq"; @@ -650,10 +638,11 @@ by (safe_tac (ZF_cs addSIs [Ord_ordertype])); by (rewtac Transset_def); by (safe_tac ZF_cs); -by (rtac (ordertype_subset RS exE) 1 THEN REPEAT (assume_tac 1)); +by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold]) 1); +by (safe_tac ZF_cs); by (rtac UN_I 1); by (rtac ReplaceI 2); -by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset]))); +by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset, predE]))); qed "Ord_jump_cardinal"; (*Allows selective unfolding. Less work than deriving intro/elim rules*)