--- 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. <x,<y,z>>, w))"),
- ("d", "split(%x. split(%y z. <<x,y>, 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,z>), %y.Inr(<y,z>), x))"),
- ("d", "case(split(%x y.<Inl(x),y>), split(%x y.<Inr(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.<x,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; y<K; z=succ(x Un y) |] ==> \
+ "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \
\ ordermap(K*K, csquare_rel(K)) ` <x,y> lepoll \
\ ordermap(K*K, csquare_rel(K)) ` <z,z>";
by (subgoals_tac ["z<K", "well_ord(K*K, csquare_rel(K))"] 1);
-by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 2);
-by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, Limit_has_succ]) 2);
+by (etac (Limit_is_Ord RS well_ord_csquare) 2);
+by (fast_tac (ZF_cs addSIs [Un_least_lt, Limit_has_succ]) 2);
by (rtac (OrdmemD RS subset_imp_lepoll) 1);
by (res_inst_tac [("z1","z")] (csquare_ltI RS ordermap_mono) 1);
by (etac well_ord_is_wf 4);
@@ -495,17 +491,16 @@
(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
goalw CardinalArith.thy [cmult_def]
- "!!K. [| InfCard(K); x<K; y<K; z=succ(x Un y) |] ==> \
+ "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \
\ | ordermap(K*K, csquare_rel(K)) ` <x,y> | 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"] 1);
-by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit,
- Limit_has_succ]) 2);
+by (fast_tac (ZF_cs addSIs [Un_least_lt, Limit_has_succ]) 2);
by (rtac (ordermap_z_lepoll RS lepoll_trans) 1);
by (REPEAT_SOME assume_tac);
by (rtac (ordermap_eqpoll_pred RS eqpoll_imp_lepoll RS lepoll_trans) 1);
-by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 1);
+by (etac (Limit_is_Ord RS well_ord_csquare) 1);
by (fast_tac (ZF_cs addIs [ltD]) 1);
by (rtac (pred_csquare_subset RS subset_imp_lepoll RS lepoll_trans) 1 THEN
assume_tac 1);
@@ -529,7 +524,7 @@
by (safe_tac (ZF_cs addSEs [ltE]));
by (subgoals_tac ["Ord(xb)", "Ord(y)"] 1);
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 2));
-by (rtac (ordermap_csquare_le RS lt_trans1) 1 THEN
+by (rtac (InfCard_is_Limit RS ordermap_csquare_le RS lt_trans1) 1 THEN
REPEAT (ares_tac [refl] 1 ORELSE etac ltI 1));
by (res_inst_tac [("i","xb Un y"), ("j","nat")] Ord_linear2 1 THEN
REPEAT (ares_tac [Ord_Un, Ord_nat] 1));
@@ -539,7 +534,7 @@
by (asm_full_simp_tac
(ZF_ss addsimps [lt_def, nat_cmult_eq_mult, nat_succI, mult_type,
nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1);
-(*case nat le (xb Un y), equivalently InfCard(xb Un y) *)
+(*case nat le (xb Un y) *)
by (asm_full_simp_tac
(ZF_ss addsimps [le_imp_subset RS nat_succ_eqpoll RS cardinal_cong,
le_succ_iff, InfCard_def, Card_cardinal, Un_least_lt,
@@ -547,15 +542,6 @@
Ord_cardinal_le RS lt_trans1 RS ltD]) 1);
qed "ordertype_csquare_le";
-(*This lemma can easily be generalized to premise well_ord(A*A,r) *)
-goalw CardinalArith.thy [cmult_def]
- "!!K. Ord(K) ==> 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*)