# HG changeset patch # User lcp # Date 788196394 -3600 # Node ID 33dc37d4629650c453ce811db8a6016b71c0918e # Parent 8d5748202c536459e0828ede8ae6ec3b47d98e9d Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit diff -r 8d5748202c53 -r 33dc37d46296 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Fri Dec 23 16:25:45 1994 +0100 +++ b/src/ZF/CardinalArith.ML Fri Dec 23 16:26:34 1994 +0100 @@ -4,6 +4,11 @@ Copyright 1994 University of Cambridge Cardinal arithmetic -- WITHOUT the Axiom of Choice + +Note: Could omit proving the associative 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. *) open CardinalArith; @@ -31,7 +36,7 @@ (*Each element of Fin(A) is equivalent to a natural number*) goal CardinalArith.thy "!!X A. X: Fin(A) ==> EX n:nat. X eqpoll n"; -by (eresolve_tac [Fin_induct] 1); +by (etac Fin_induct 1); by (fast_tac (ZF_cs addIs [eqpoll_refl, nat_0I]) 1); by (fast_tac (ZF_cs addSIs [cons_eqpoll_cong, rewrite_rule [succ_def] nat_succI] @@ -69,11 +74,11 @@ "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ \ (i |+| j) |+| k = i |+| (j |+| k)"; by (rtac cardinal_cong 1); -br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS - eqpoll_trans) 1; +by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS + eqpoll_trans) 1); by (rtac (sum_assoc_eqpoll RS eqpoll_trans) 2); -br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS - eqpoll_sym) 2; +by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS + eqpoll_sym) 2); by (REPEAT (ares_tac [well_ord_radd] 1)); qed "well_ord_cadd_assoc"; @@ -117,14 +122,14 @@ [("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 (eresolve_tac [sumE] 1); +by (etac sumE 1); by (ALLGOALS (asm_simp_tac (sum_ss addsimps [left_inverse]))); qed "sum_lepoll_mono"; goalw CardinalArith.thy [cadd_def] "!!K. [| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)"; by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); -by (resolve_tac [well_ord_lepoll_imp_Card_le] 1); +by (rtac well_ord_lepoll_imp_Card_le 1); by (REPEAT (ares_tac [sum_lepoll_mono, subset_imp_lepoll] 2)); by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1)); qed "cadd_le_mono"; @@ -194,11 +199,11 @@ "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ \ (i |*| j) |*| k = i |*| (j |*| k)"; by (rtac cardinal_cong 1); -br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS - eqpoll_trans) 1; +by (rtac ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS + eqpoll_trans) 1); by (rtac (prod_assoc_eqpoll RS eqpoll_trans) 2); -br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS prod_eqpoll_cong RS - eqpoll_sym) 2; +by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS prod_eqpoll_cong RS + eqpoll_sym) 2); by (REPEAT (ares_tac [well_ord_rmult] 1)); qed "well_ord_cmult_assoc"; @@ -248,7 +253,7 @@ by (simp_tac (ZF_ss addsimps [lam_type]) 1); qed "prod_square_lepoll"; -(*Could probably weaken the premise to well_ord(K,r), or removing using AC*) +(*Could probably weaken the premise to well_ord(K,r), or remove using AC*) goalw CardinalArith.thy [cmult_def] "!!K. Card(K) ==> K le K |*| K"; by (rtac le_trans 1); by (rtac well_ord_lepoll_imp_Card_le 2); @@ -274,7 +279,6 @@ (** Monotonicity of multiplication **) -(*Equivalent to KG's lepoll_SigmaI*) goalw CardinalArith.thy [lepoll_def] "!!A B C D. [| A lepoll C; B lepoll D |] ==> A * B lepoll C * D"; by (REPEAT (etac exE 1)); @@ -282,14 +286,14 @@ by (res_inst_tac [("d", "split(%w y.)")] lam_injective 1); by (typechk_tac (inj_is_fun::ZF_typechecks)); -by (eresolve_tac [SigmaE] 1); +by (etac SigmaE 1); by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1); qed "prod_lepoll_mono"; goalw CardinalArith.thy [cmult_def] "!!K. [| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)"; by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); -by (resolve_tac [well_ord_lepoll_imp_Card_le] 1); +by (rtac well_ord_lepoll_imp_Card_le 1); by (REPEAT (ares_tac [prod_lepoll_mono, subset_imp_lepoll] 2)); by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); qed "cmult_le_mono"; @@ -324,8 +328,7 @@ nat_cadd_eq_add]) 1); qed "nat_cmult_eq_mult"; -(*Needs Krzysztof Grabczewski's macro "2" == "succ(1)"*) -goal CardinalArith.thy "!!m n. Card(n) ==> succ(1) |*| n = n |+| n"; +goal CardinalArith.thy "!!m n. Card(n) ==> 2 |*| n = n |+| n"; by (asm_simp_tac (ZF_ss addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, Card_is_Ord, read_instantiate [("j","0")] cadd_commute, cadd_0]) 1); @@ -385,21 +388,18 @@ (*Kunen's Lemma 10.11*) goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Limit(K)"; by (etac conjE 1); +by (forward_tac [Card_is_Ord] 1); by (rtac (ltI RS non_succ_LimitI) 1); by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1); -by (etac Card_is_Ord 1); by (safe_tac (ZF_cs addSDs [Limit_nat RS Limit_le_succD])); -by (forward_tac [Card_is_Ord RS Ord_succD] 1); by (rewtac Card_def); -by (res_inst_tac [("i", "succ(y)")] lt_irrefl 1); -by (dtac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1); -(*Tricky combination of substitutions; backtracking needed*) -by (etac ssubst 1 THEN etac ssubst 1 THEN rtac Ord_cardinal_le 1); -by (assume_tac 1); +by (dtac trans 1); +by (etac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1); +by (etac (Ord_succD RS Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1); +by (REPEAT (ares_tac [le_eqI, Ord_cardinal] 1)); qed "InfCard_is_Limit"; - (*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***) (*A general fact about ordermap*) @@ -453,8 +453,7 @@ qed "pred_csquare_subset"; goalw CardinalArith.thy [csquare_rel_def] - "!!K. [| x \ -\ <, > : csquare_rel(K)"; + "!!K. [| x <, > : csquare_rel(K)"; by (subgoals_tac ["x A*A eqpoll A"; by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1); by (REPEAT (etac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1)); -by (resolve_tac [well_ord_cardinal_eqE] 1); +by (rtac well_ord_cardinal_eqE 1); by (REPEAT (ares_tac [Ord_cardinal, well_ord_rmult, well_ord_Memrel] 1)); by (asm_simp_tac (ZF_ss addsimps [symmetric cmult_def, InfCard_csquare_eq]) 1); qed "well_ord_InfCard_square_eq"; @@ -586,8 +585,8 @@ (** Toward's Kunen's Corollary 10.13 (1) **) goal CardinalArith.thy "!!K. [| InfCard(K); L le K; 0 K |*| L = K"; -by (resolve_tac [le_anti_sym] 1); -by (eresolve_tac [ltE] 2 THEN +by (rtac le_anti_sym 1); +by (etac ltE 2 THEN REPEAT (ares_tac [cmult_le_self, InfCard_is_Card] 2)); by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); by (resolve_tac [cmult_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); @@ -611,15 +610,15 @@ goal CardinalArith.thy "!!K. InfCard(K) ==> K |+| K = K"; by (asm_simp_tac (ZF_ss addsimps [cmult_2 RS sym, InfCard_is_Card, cmult_commute]) 1); -by (resolve_tac [InfCard_le_cmult_eq] 1); +by (rtac InfCard_le_cmult_eq 1); by (typechk_tac [Ord_0, le_refl, leI]); by (typechk_tac [InfCard_is_Limit, Limit_has_0, Limit_has_succ]); qed "InfCard_cdouble_eq"; (*Corollary 10.13 (1), for cardinal addition*) goal CardinalArith.thy "!!K. [| InfCard(K); L le K |] ==> K |+| L = K"; -by (resolve_tac [le_anti_sym] 1); -by (eresolve_tac [ltE] 2 THEN +by (rtac le_anti_sym 1); +by (etac ltE 2 THEN REPEAT (ares_tac [cadd_le_self, InfCard_is_Card] 2)); by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); by (resolve_tac [cadd_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); @@ -649,11 +648,11 @@ goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))"; by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); by (safe_tac (ZF_cs addSIs [Ord_ordertype])); -bw Transset_def; +by (rewtac Transset_def); by (safe_tac ZF_cs); by (rtac (ordertype_subset RS exE) 1 THEN REPEAT (assume_tac 1)); -by (resolve_tac [UN_I] 1); -by (resolve_tac [ReplaceI] 2); +by (rtac UN_I 1); +by (rtac ReplaceI 2); by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset]))); qed "Ord_jump_cardinal"; @@ -669,7 +668,7 @@ by (resolve_tac [Ord_jump_cardinal RSN (2,ltI)] 1); by (resolve_tac [jump_cardinal_iff RS iffD2] 1); by (REPEAT_FIRST (ares_tac [exI, conjI, well_ord_Memrel])); -by (resolve_tac [subset_refl] 2); +by (rtac subset_refl 2); by (asm_simp_tac (ZF_ss addsimps [Memrel_def, subset_iff]) 1); by (asm_simp_tac (ZF_ss addsimps [ordertype_Memrel]) 1); qed "K_lt_jump_cardinal"; @@ -696,7 +695,7 @@ (*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) goal CardinalArith.thy "Card(jump_cardinal(K))"; by (rtac (Ord_jump_cardinal RS CardI) 1); -by (rewrite_goals_tac [eqpoll_def]); +by (rewtac eqpoll_def); by (safe_tac (ZF_cs addSDs [ltD, jump_cardinal_iff RS iffD1])); by (REPEAT (ares_tac [Card_jump_cardinal_lemma RS mem_irrefl] 1)); qed "Card_jump_cardinal"; @@ -727,9 +726,9 @@ goal CardinalArith.thy "!!K. [| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K"; -by (resolve_tac [iffI] 1); -by (resolve_tac [Card_lt_imp_lt] 2); -by (eresolve_tac [lt_trans1] 2); +by (rtac iffI 1); +by (rtac Card_lt_imp_lt 2); +by (etac lt_trans1 2); by (REPEAT (ares_tac [lt_csucc, Card_csucc, Card_is_Ord] 2)); by (resolve_tac [notI RS not_lt_imp_le] 1); by (resolve_tac [Card_cardinal RS csucc_le RS lt_trans1 RS lt_irrefl] 1);