# HG changeset patch
# User lcp
# Date 777546677 -7200
# Node ID 0b03ce5b62f7ad3478b24a2226029911b8241b86
# Parent  6333c181a3f7200be2ec1b1b8758ff827742770a
ZF/Cardinal: some results moved here from CardinalArith
ZF/CardinalArith/nat_succ_lepoll: removed obsolete proof
ZF/CardinalArith/nat_cons_eqpoll: new

diff -r 6333c181a3f7 -r 0b03ce5b62f7 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Mon Aug 22 11:07:40 1994 +0200
+++ b/src/ZF/Cardinal.ML	Mon Aug 22 11:11:17 1994 +0200
@@ -397,3 +397,81 @@
 by (etac cardinal_mono 1);
 val nat_le_cardinal = result();
 
+
+(*** Towards Cardinal Arithmetic ***)
+(** Congruence laws for successor, cardinal addition and multiplication **)
+
+val case_ss = ZF_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff,
+			      case_Inl, case_Inr, InlI, InrI];
+
+val bij_inverse_ss =
+    case_ss addsimps [bij_is_fun RS apply_type,
+		      bij_converse_bij RS bij_is_fun RS apply_type,
+		      left_inverse_bij, right_inverse_bij];
+
+
+(*Congruence law for  cons  under equipollence*)
+goalw Cardinal.thy [lepoll_def]
+    "!!A B. [| A lepoll B;  b ~: B |] ==> cons(a,A) lepoll cons(b,B)";
+by (safe_tac ZF_cs);
+by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1);
+by (res_inst_tac [("d","%z.if(z:B, converse(f)`z, a)")] 
+    lam_injective 1);
+by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, cons_iff]
+                        setloop etac consE') 1);
+by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse]
+                        setloop etac consE') 1);
+val cons_lepoll_cong = result();
+
+goal Cardinal.thy
+    "!!A B. [| A eqpoll B;  a ~: A;  b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
+by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff, cons_lepoll_cong]) 1);
+val cons_eqpoll_cong = result();
+
+(*Congruence law for  succ  under equipollence*)
+goalw Cardinal.thy [succ_def]
+    "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";
+by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1));
+val succ_eqpoll_cong = result();
+
+(*Congruence law for + under equipollence*)
+goalw Cardinal.thy [eqpoll_def]
+    "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A+B eqpoll C+D";
+by (safe_tac ZF_cs);
+by (rtac exI 1);
+by (res_inst_tac [("c", "case(%x. Inl(f`x), %y. Inr(fa`y))"),
+	 ("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")] 
+    lam_bijective 1);
+by (safe_tac (ZF_cs addSEs [sumE]));
+by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+val sum_eqpoll_cong = result();
+
+(*Congruence law for * under equipollence*)
+goalw Cardinal.thy [eqpoll_def]
+    "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A*B eqpoll C*D";
+by (safe_tac ZF_cs);
+by (rtac exI 1);
+by (res_inst_tac [("c", "split(%x y. <f`x, fa`y>)"),
+		  ("d", "split(%x y. <converse(f)`x, converse(fa)`y>)")] 
+    lam_bijective 1);
+by (safe_tac ZF_cs);
+by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+val prod_eqpoll_cong = result();
+
+goalw Cardinal.thy [eqpoll_def]
+    "!!f. [| f: inj(A,B);  A Int B = 0 |] ==> A Un (B - range(f)) eqpoll B";
+by (rtac exI 1);
+by (res_inst_tac [("c", "%x. if(x:A, f`x, x)"),
+		  ("d", "%y. if(y: range(f), converse(f)`y, y)")] 
+    lam_bijective 1);
+by (fast_tac (ZF_cs addSIs [if_type, apply_type] addIs [inj_is_fun]) 1);
+by (asm_simp_tac 
+    (ZF_ss addsimps [inj_converse_fun RS apply_funtype]
+           setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse]
+                        setloop etac UnE') 1);
+by (asm_simp_tac 
+    (ZF_ss addsimps [inj_converse_fun RS apply_funtype, right_inverse]
+           setloop split_tac [expand_if]) 1);
+by (fast_tac (ZF_cs addEs [equals0D]) 1);
+val inj_disjoint_eqpoll = result();
diff -r 6333c181a3f7 -r 0b03ce5b62f7 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Mon Aug 22 11:07:40 1994 +0200
+++ b/src/ZF/CardinalArith.ML	Mon Aug 22 11:11:17 1994 +0200
@@ -28,39 +28,6 @@
 by (assume_tac 1);
 val well_ord_lepoll_imp_le = result();
 
-val case_ss = ZF_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff,
-			      case_Inl, case_Inr, InlI, InrI];
-
-
-(** Congruence laws for successor, cardinal addition and multiplication **)
-
-val bij_inverse_ss =
-    case_ss addsimps [bij_is_fun RS apply_type,
-		      bij_converse_bij RS bij_is_fun RS apply_type,
-		      left_inverse_bij, right_inverse_bij];
-
-
-(*Congruence law for  cons  under equipollence*)
-goalw CardinalArith.thy [eqpoll_def]
-    "!!A B. [| A eqpoll B;  a ~: A;  b ~: B |] ==> cons(a,A) eqpoll cons(b,B)";
-by (safe_tac ZF_cs);
-by (rtac exI 1);
-by (res_inst_tac [("c", "%z.if(z=a,b,f`z)"), 
-                  ("d", "%z.if(z=b,a,converse(f)`z)")] lam_bijective 1);
-by (ALLGOALS
-    (asm_simp_tac (bij_inverse_ss addsimps [consI2]
- 		                  setloop (etac consE ORELSE' 
-				           split_tac [expand_if]))));
-by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1);
-by (fast_tac (ZF_cs addIs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
-val cons_eqpoll_cong = result();
-
-(*Congruence law for  succ  under equipollence*)
-goalw CardinalArith.thy [succ_def]
-    "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";
-by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1));
-val succ_eqpoll_cong = result();
-
 (*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";
@@ -71,36 +38,10 @@
                             addSEs [mem_irrefl]) 1);
 val Fin_eqpoll = result();
 
-(*Congruence law for + under equipollence*)
-goalw CardinalArith.thy [eqpoll_def]
-    "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A+B eqpoll C+D";
-by (safe_tac ZF_cs);
-by (rtac exI 1);
-by (res_inst_tac [("c", "case(%x. Inl(f`x), %y. Inr(fa`y))"),
-	 ("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")] 
-    lam_bijective 1);
-by (safe_tac (ZF_cs addSEs [sumE]));
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-val sum_eqpoll_cong = result();
-
-(*Congruence law for * under equipollence*)
-goalw CardinalArith.thy [eqpoll_def]
-    "!!A B C D. [| A eqpoll C;  B eqpoll D |] ==> A*B eqpoll C*D";
-by (safe_tac ZF_cs);
-by (rtac exI 1);
-by (res_inst_tac [("c", "split(%x y. <f`x, fa`y>)"),
-		  ("d", "split(%x y. <converse(f)`x, converse(fa)`y>)")] 
-    lam_bijective 1);
-by (safe_tac ZF_cs);
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-val prod_eqpoll_cong = result();
-
-
 (*** Cardinal addition ***)
 
 (** Cardinal addition is commutative **)
 
-(*Easier to prove the two directions separately*)
 goalw CardinalArith.thy [eqpoll_def] "A+B eqpoll B+A";
 by (rtac exI 1);
 by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")] 
@@ -309,34 +250,38 @@
 
 (*** Infinite Cardinals are Limit Ordinals ***)
 
+(*This proof is modelled upon one assuming nat<=A, with injection
+  lam z:cons(u,A). if(z=u, 0, if(z : nat, succ(z), z))  and inverse
+  %y. if(y:nat, nat_case(u,%z.z,y), y).  If f: inj(nat,A) then
+  range(f) behaves like the natural numbers.*)
 goalw CardinalArith.thy [lepoll_def]
-    "!!i. nat <= A ==> succ(A) lepoll A";
+    "!!i. nat lepoll A ==> cons(u,A) lepoll A";
+by (etac exE 1);
 by (res_inst_tac [("x",
-    "lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
-by (res_inst_tac [("d", "%y. if(y:nat, nat_case(A,%z.z,y), y)")] 
+    "lam z:cons(u,A). if(z=u, f`0, 	\
+\                        if(z: range(f), f`succ(converse(f)`z), z))")] exI 1);
+by (res_inst_tac [("d", "%y. if(y: range(f), 	\
+\                               nat_case(u, %z.f`z, converse(f)`y), y)")] 
     lam_injective 1);
-by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
+by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI, apply_type]
+                    addIs  [inj_is_fun, inj_converse_fun]) 1);
 by (asm_simp_tac 
-    (ZF_ss addsimps [nat_case_0, nat_case_succ, nat_0I, nat_succI]
+    (ZF_ss addsimps [inj_is_fun RS apply_rangeI,
+		     inj_converse_fun RS apply_rangeI,
+		     inj_converse_fun RS apply_funtype,
+		     left_inverse, right_inverse, nat_0I, nat_succI, 
+		     nat_case_0, nat_case_succ]
            setloop split_tac [expand_if]) 1);
-val nat_succ_lepoll = result();
+val nat_cons_lepoll = result();
 
-goalw CardinalArith.thy [lepoll_def, inj_def]
-    "!!i. nat <= A ==> succ(A) lepoll A";
-by (res_inst_tac [("x",
-   "lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
-by (rtac (lam_type RS CollectI) 1);
-by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
-by (REPEAT (rtac ballI 1));
-by (asm_simp_tac 
-    (ZF_ss addsimps [succ_inject_iff, succ_not_0, succ_not_0 RS not_sym]
-           setloop split_tac [expand_if]) 1);
-by (safe_tac (ZF_cs addSIs [nat_0I, nat_succI]));
-val nat_succ_lepoll = result();
+goal CardinalArith.thy "!!i. nat lepoll A ==> cons(u,A) eqpoll A";
+by (etac (nat_cons_lepoll RS eqpollI) 1);
+by (rtac (subset_consI RS subset_imp_lepoll) 1);
+val nat_cons_eqpoll = result();
 
-goal CardinalArith.thy "!!i. nat <= A ==> succ(A) eqpoll A";
-by (etac (nat_succ_lepoll RS eqpollI) 1);
-by (rtac (subset_succI RS subset_imp_lepoll) 1);
+(*Specialized version required below*)
+goalw CardinalArith.thy [succ_def] "!!i. nat <= A ==> succ(A) eqpoll A";
+by (eresolve_tac [subset_imp_lepoll RS nat_cons_eqpoll] 1);
 val nat_succ_eqpoll = result();
 
 goalw CardinalArith.thy [InfCard_def] "InfCard(nat)";