src/ZF/CardinalArith.ML
changeset 823 33dc37d46296
parent 800 23f55b829ccb
child 846 c4566750dc12
--- 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.<converse(f)`w, converse(fa)`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<z;  y<z;  z<K |] ==> \
-\      <<x,y>, <z,z>> : csquare_rel(K)";
+ "!!K. [| x<z;  y<z;  z<K |] ==>  <<x,y>, <z,z>> : csquare_rel(K)";
 by (subgoals_tac ["x<K", "y<K"] 1);
 by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));
 by (REPEAT (etac ltE 1));
@@ -578,7 +577,7 @@
     "!!A. [| well_ord(A,r);  InfCard(|A|) |] ==> 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<L |] ==> 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);