src/ZF/CardinalArith.ML
changeset 767 a4fce3b94065
parent 760 f0200e91b272
child 782 200a16083201
--- a/src/ZF/CardinalArith.ML	Thu Dec 08 13:53:28 1994 +0100
+++ b/src/ZF/CardinalArith.ML	Thu Dec 08 14:06:16 1994 +0100
@@ -26,7 +26,7 @@
 by (rtac well_ord_cardinal_eqpoll 1);
 by (etac well_ord_rvimage 1);
 by (assume_tac 1);
-qed "well_ord_lepoll_imp_le";
+qed "well_ord_lepoll_imp_Card_le";
 
 (*Each element of Fin(A) is equivalent to a natural number*)
 goal CardinalArith.thy
@@ -91,6 +91,44 @@
 				  Card_cardinal_eq]) 1);
 qed "cadd_0";
 
+(** Addition by another cardinal **)
+
+goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A+B";
+by (res_inst_tac [("x", "lam x:A. Inl(x)")] exI 1);
+by (asm_simp_tac (sum_ss addsimps [lam_type]) 1);
+val sum_lepoll_self = result();
+
+(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
+goalw CardinalArith.thy [cadd_def]
+    "!!K. [| Card(K);  Ord(L) |] ==> K le (K |+| L)";
+by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1);
+by (rtac sum_lepoll_self 3);
+by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Card_is_Ord] 1));
+val cadd_le_self = result();
+
+(** Monotonicity of addition **)
+
+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));
+by (res_inst_tac [("x", "lam z:A+B. case(%w. Inl(f`w), %y. Inr(fa`y), z)")] 
+    exI 1);
+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 (eresolve_tac [sumE] 1);
+by (ALLGOALS (asm_simp_tac (sum_ss addsimps [left_inverse])));
+val sum_lepoll_mono = result();
+
+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 (REPEAT (ares_tac [sum_lepoll_mono, subset_imp_lepoll] 2));
+by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));
+val cadd_le_mono = result();
+
 (** Addition of finite cardinals is "ordinary" addition **)
 
 goalw CardinalArith.thy [eqpoll_def] "succ(A)+B eqpoll succ(A+B)";
@@ -176,19 +214,6 @@
 by (ALLGOALS (asm_simp_tac case_ss));
 qed "sum_prod_distrib_eqpoll";
 
-goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A*A";
-by (res_inst_tac [("x", "lam x:A. <x,x>")] exI 1);
-by (simp_tac (ZF_ss addsimps [lam_type]) 1);
-qed "prod_square_lepoll";
-
-goalw CardinalArith.thy [cmult_def] "!!K. Card(K) ==> K le K |*| K";
-by (rtac le_trans 1);
-by (rtac well_ord_lepoll_imp_le 2);
-by (rtac prod_square_lepoll 3);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord] 2));
-by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);
-qed "cmult_square_le";
-
 (** Multiplication by 0 yields 0 **)
 
 goalw CardinalArith.thy [eqpoll_def] "0*A eqpoll 0";
@@ -216,7 +241,60 @@
 				  Card_cardinal_eq]) 1);
 qed "cmult_1";
 
-(** Multiplication of finite cardinals is "ordinary" multiplication **)
+(*** Some inequalities for multiplication ***)
+
+goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A*A";
+by (res_inst_tac [("x", "lam x:A. <x,x>")] exI 1);
+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*)
+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);
+by (rtac prod_square_lepoll 3);
+by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord] 2));
+by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);
+qed "cmult_square_le";
+
+(** Multiplication by a non-zero cardinal **)
+
+goalw CardinalArith.thy [lepoll_def, inj_def] "!!b. b: B ==> A lepoll A*B";
+by (res_inst_tac [("x", "lam x:A. <x,b>")] exI 1);
+by (asm_simp_tac (ZF_ss addsimps [lam_type]) 1);
+val prod_lepoll_self = result();
+
+(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
+goalw CardinalArith.thy [cmult_def]
+    "!!K. [| Card(K);  Ord(L);  0<L |] ==> K le (K |*| L)";
+by (rtac ([Card_cardinal_le, well_ord_lepoll_imp_Card_le] MRS le_trans) 1);
+by (rtac prod_lepoll_self 3);
+by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord, ltD] 1));
+val cmult_le_self = result();
+
+(** 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));
+by (res_inst_tac [("x", "lam z:A*B. split(%w y.<f`w, fa`y>, z)")] exI 1);
+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 (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
+val prod_lepoll_mono = result();
+
+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 (REPEAT (ares_tac [prod_lepoll_mono, subset_imp_lepoll] 2));
+by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
+val cmult_le_mono = result();
+
+(*** Multiplication of finite cardinals is "ordinary" multiplication ***)
 
 goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B";
 by (rtac exI 1);
@@ -228,7 +306,6 @@
     (asm_simp_tac (case_ss addsimps [succI2, if_type, mem_imp_not_eq])));
 qed "prod_succ_eqpoll";
 
-
 (*Unconditional version requires AC*)
 goalw CardinalArith.thy [cmult_def, cadd_def]
     "!!m n. [| Ord(m);  Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)";
@@ -247,6 +324,13 @@
 				     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";
+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);
+val cmult_2 = result();
+
 
 (*** Infinite Cardinals are Limit Ordinals ***)
 
@@ -413,7 +497,7 @@
 goalw CardinalArith.thy [cmult_def]
   "!!K. [| InfCard(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_le) 1);
+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, 
@@ -488,7 +572,7 @@
                      well_ord_csquare RS Ord_ordertype]) 1);
 qed "InfCard_csquare_eq";
 
-
+(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
 goal CardinalArith.thy
     "!!A. [| well_ord(A,r);  InfCard(|A|) |] ==> A*A eqpoll A";
 by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1);
@@ -498,6 +582,65 @@
 by (asm_simp_tac (ZF_ss addsimps [symmetric cmult_def, InfCard_csquare_eq]) 1);
 qed "well_ord_InfCard_square_eq";
 
+(** 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
+    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));
+by (asm_simp_tac (ZF_ss addsimps [InfCard_csquare_eq]) 1);
+val InfCard_le_cmult_eq = result();
+
+(*Corollary 10.13 (1), for cardinal multiplication*)
+goal CardinalArith.thy
+    "!!K. [| InfCard(K);  InfCard(L) |] ==> K |*| L = K Un L";
+by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1);
+by (typechk_tac [InfCard_is_Card, Card_is_Ord]);
+by (resolve_tac [cmult_commute RS ssubst] 1);
+by (resolve_tac [Un_commute RS ssubst] 1);
+by (ALLGOALS
+    (asm_simp_tac 
+     (ZF_ss addsimps [InfCard_is_Limit RS Limit_has_0, InfCard_le_cmult_eq,
+		      subset_Un_iff2 RS iffD1, le_imp_subset])));
+val InfCard_cmult_eq = result();
+
+(*This proof appear to be the simplest!*)
+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 (typechk_tac [Ord_0, le_refl, leI]);
+by (typechk_tac [InfCard_is_Limit, Limit_has_0, Limit_has_succ]);
+val InfCard_cdouble_eq = result();
+
+(*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
+    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));
+by (asm_simp_tac (ZF_ss addsimps [InfCard_cdouble_eq]) 1);
+val InfCard_le_cadd_eq = result();
+
+goal CardinalArith.thy
+    "!!K. [| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L";
+by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1);
+by (typechk_tac [InfCard_is_Card, Card_is_Ord]);
+by (resolve_tac [cadd_commute RS ssubst] 1);
+by (resolve_tac [Un_commute RS ssubst] 1);
+by (ALLGOALS
+    (asm_simp_tac 
+     (ZF_ss addsimps [InfCard_le_cadd_eq,
+		      subset_Un_iff2 RS iffD1, le_imp_subset])));
+val InfCard_cadd_eq = result();
+
+(*The other part, Corollary 10.13 (2), refers to the cardinality of the set
+  of all n-tuples of elements of K.  A better version for the Isabelle theory
+  might be  InfCard(K) ==> |list(K)| = K.
+*)
 
 (*** For every cardinal number there exists a greater one
      [Kunen's Theorem 10.16, which would be trivial using AC] ***)