--- a/src/ZF/Arith.ML Tue Mar 26 11:38:17 1996 +0100
+++ b/src/ZF/Arith.ML Tue Mar 26 11:42:36 1996 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-For arith.thy. Arithmetic operators and their definitions
+Arithmetic operators and their definitions
Proofs about elementary arithmetic: addition, multiplication, etc.
@@ -42,8 +42,6 @@
(asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
qed "rec_type";
-val nat_le_refl = nat_into_Ord RS le_refl;
-
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
@@ -170,7 +168,6 @@
by (rtac (eqn RS rev_mp) 1);
by (nat_ind_tac "k" [knat] 1);
by (ALLGOALS (simp_tac arith_ss));
-by (fast_tac ZF_cs 1);
qed "add_left_cancel";
(*** Multiplication ***)
@@ -247,6 +244,15 @@
by (ALLGOALS (asm_simp_tac arith_ss));
qed "add_diff_inverse";
+(*Proof is IDENTICAL to that above*)
+goal Arith.thy "!!m n. [| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)";
+by (forward_tac [lt_nat_in_nat] 1);
+by (etac nat_succI 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+qed "diff_succ";
+
(*Subtraction is the inverse of addition. *)
val [mnat,nnat] = goal Arith.thy
"[| m:nat; n:nat |] ==> (n#+m) #- n = m";
@@ -266,7 +272,6 @@
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat])));
qed "diff_add_0";
-
(*** Remainder ***)
goal Arith.thy "!!m n. [| 0<n; n le m; m:nat |] ==> m #- n < m";
@@ -321,7 +326,7 @@
by (asm_simp_tac div_ss 1);
qed "div_geq";
-(*Main Result.*)
+(*A key result*)
goal Arith.thy
"!!m n. [| 0<n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m";
by (etac complete_induct 1);
@@ -335,6 +340,59 @@
div_termination RS ltD, add_diff_inverse]) 1);
qed "mod_div_equality";
+(*** Further facts about mod (mainly for mutilated checkerboard ***)
+
+goal Arith.thy
+ "!!m n. [| 0<n; m:nat; n:nat |] ==> \
+\ succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))";
+by (etac complete_induct 1);
+by (excluded_middle_tac "succ(x)<n" 1);
+(*case x<n*)
+by (asm_simp_tac (arith_ss addsimps [mod_less, nat_le_refl RS lt_trans,
+ succ_neq_self]) 2);
+by (asm_simp_tac (arith_ss addsimps [ltD RS mem_imp_not_eq]) 2);
+(*case n le x*)
+by (asm_full_simp_tac
+ (arith_ss addsimps [not_lt_iff_le, nat_into_Ord, mod_geq]) 1);
+be leE 1;
+by (asm_simp_tac (arith_ss addsimps [div_termination RS ltD, diff_succ,
+ mod_geq]) 1);
+by (asm_simp_tac (arith_ss addsimps [mod_less, diff_self_eq_0]) 1);
+qed "mod_succ";
+
+goal Arith.thy "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n < n";
+by (etac complete_induct 1);
+by (excluded_middle_tac "x<n" 1);
+(*case x<n*)
+by (asm_simp_tac (arith_ss addsimps [mod_less]) 2);
+(*case n le x*)
+by (asm_full_simp_tac
+ (arith_ss addsimps [not_lt_iff_le, nat_into_Ord,
+ mod_geq, div_termination RS ltD]) 1);
+qed "mod_less_divisor";
+
+
+goal Arith.thy
+ "!!k b. [| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = if(b=1,0,1)";
+by (subgoal_tac "k mod 2: 2" 1);
+by (asm_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD]) 2);
+by (dresolve_tac [ltD] 1);
+by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
+by (fast_tac ZF_cs 1);
+qed "mod2_cases";
+
+goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2";
+by (subgoal_tac "m mod 2: 2" 1);
+by (asm_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD]) 2);
+by (asm_simp_tac (arith_ss addsimps [mod_succ] setloop step_tac ZF_cs) 1);
+qed "mod2_succ_succ";
+
+goal Arith.thy "!!m. m:nat ==> (m#+m) mod 2 = 0";
+by (eresolve_tac [nat_induct] 1);
+by (simp_tac (arith_ss addsimps [mod_less]) 1);
+by (asm_simp_tac (arith_ss addsimps [mod2_succ_succ, add_succ_right]) 1);
+qed "mod2_add_self";
+
(**** Additional theorems about "le" ****)
@@ -395,3 +453,8 @@
rtac add_le_mono1 5]);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
qed "add_le_mono";
+
+val arith_ss0 = arith_ss
+and arith_ss = arith_ss addsimps [add_0_right, add_succ_right,
+ mult_0_right, mult_succ_right,
+ mod_less, mod_geq, div_less, div_geq];
--- a/src/ZF/Cardinal.ML Tue Mar 26 11:38:17 1996 +0100
+++ b/src/ZF/Cardinal.ML Tue Mar 26 11:42:36 1996 +0100
@@ -77,7 +77,9 @@
by (etac id_subset_inj 1);
qed "subset_imp_lepoll";
-val lepoll_refl = subset_refl RS subset_imp_lepoll;
+bind_thm ("lepoll_refl", subset_refl RS subset_imp_lepoll);
+
+bind_thm ("le_imp_lepoll", le_imp_subset RS subset_imp_lepoll);
goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def]
"!!X Y. X eqpoll Y ==> X lepoll Y";
@@ -114,12 +116,39 @@
(*0 lepoll Y*)
bind_thm ("empty_lepollI", empty_subsetI RS subset_imp_lepoll);
+goal Cardinal.thy "A lepoll 0 <-> A=0";
+by (fast_tac (ZF_cs addIs [lepoll_0_is_0, lepoll_refl]) 1);
+qed "lepoll_0_iff";
+
(*A eqpoll 0 ==> A=0*)
bind_thm ("eqpoll_0_is_0", eqpoll_imp_lepoll RS lepoll_0_is_0);
+goal Cardinal.thy "A eqpoll 0 <-> A=0";
+by (fast_tac (ZF_cs addIs [eqpoll_0_is_0, eqpoll_refl]) 1);
+qed "eqpoll_0_iff";
+
+goalw Cardinal.thy [eqpoll_def]
+ "!!A. [| A eqpoll B; C eqpoll D; A Int C = 0; B Int D = 0 |] ==> \
+\ A Un C eqpoll B Un D";
+by (fast_tac (ZF_cs addIs [bij_disjoint_Un]) 1);
+qed "eqpoll_disjoint_Un";
+
(*** lesspoll: contributions by Krzysztof Grabczewski ***)
+goalw Cardinal.thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B";
+by (fast_tac ZF_cs 1);
+qed "lesspoll_imp_lepoll";
+
+goalw Cardinal.thy [lepoll_def]
+ "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
+by (fast_tac (ZF_cs addSEs [well_ord_rvimage]) 1);
+qed "lepoll_well_ord";
+
+goalw Cardinal.thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B";
+by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE]) 1);
+qed "lepoll_iff_leqpoll";
+
goalw Cardinal.thy [inj_def, surj_def]
"!!f. [| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)";
by (safe_tac lemmas_cs);
@@ -221,8 +250,8 @@
by (simp_tac (FOL_ss addsimps prems) 1);
qed "Least_cong";
-(*Need AC to prove X lepoll Y ==> |X| le |Y| ;
- see well_ord_lepoll_imp_Card_le *)
+(*Need AC to get X lepoll Y ==> |X| le |Y|; see well_ord_lepoll_imp_Card_le
+ Converse also requires AC, but see well_ord_cardinal_eqE*)
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
by (rtac Least_cong 1);
by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1);
@@ -236,6 +265,7 @@
by (etac (ordermap_bij RS bij_converse_bij RS bij_imp_eqpoll) 1);
qed "well_ord_cardinal_eqpoll";
+(* Ord(A) ==> |A| eqpoll A *)
bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll);
goal Cardinal.thy
@@ -245,6 +275,11 @@
by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1);
qed "well_ord_cardinal_eqE";
+goal Cardinal.thy
+ "!!X Y. [| well_ord(X,r); well_ord(Y,s) |] ==> |X| = |Y| <-> X eqpoll Y";
+by (fast_tac (ZF_cs addSEs [cardinal_cong, well_ord_cardinal_eqE]) 1);
+qed "well_ord_cardinal_eqpoll_iff";
+
(** Observations from Kunen, page 28 **)
@@ -286,6 +321,11 @@
by (ALLGOALS assume_tac);
qed "Card_iff_initial";
+goalw Cardinal.thy [lesspoll_def] "!!a. [| Card(a); i<a |] ==> i lesspoll a";
+by (dresolve_tac [Card_iff_initial RS iffD1] 1);
+by (fast_tac (ZF_cs addSEs [leI RS le_imp_lepoll]) 1);
+qed "lt_Card_imp_lesspoll";
+
goal Cardinal.thy "Card(0)";
by (rtac (Ord_0 RS CardI) 1);
by (fast_tac (ZF_cs addSEs [ltE]) 1);
@@ -316,9 +356,9 @@
(*Kunen's Lemma 10.5*)
goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|";
by (rtac (eqpollI RS cardinal_cong) 1);
-by (etac (le_imp_subset RS subset_imp_lepoll) 1);
+by (etac le_imp_lepoll 1);
by (rtac lepoll_trans 1);
-by (etac (le_imp_subset RS subset_imp_lepoll) 2);
+by (etac le_imp_lepoll 2);
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1);
by (rtac Ord_cardinal_eqpoll 1);
by (REPEAT (eresolve_tac [ltE, Ord_succD] 1));
@@ -357,6 +397,32 @@
not_lt_iff_le RS iff_sym]) 1);
qed "Card_le_iff";
+(*Can use AC or finiteness to discharge first premise*)
+goal Cardinal.thy
+ "!!A B. [| well_ord(B,r); A lepoll B |] ==> |A| le |B|";
+by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1);
+by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
+by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1);
+by (rtac lepoll_trans 1);
+by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll) 1);
+by (assume_tac 1);
+by (etac (le_imp_lepoll RS lepoll_trans) 1);
+by (rtac eqpoll_imp_lepoll 1);
+by (rewtac lepoll_def);
+by (etac exE 1);
+by (rtac well_ord_cardinal_eqpoll 1);
+by (etac well_ord_rvimage 1);
+by (assume_tac 1);
+qed "well_ord_lepoll_imp_Card_le";
+
+
+goal Cardinal.thy "!!A. [| A lepoll i; Ord(i) |] ==> |A| le i";
+br le_trans 1;
+be (well_ord_Memrel RS well_ord_lepoll_imp_Card_le) 1;
+ba 1;
+be Ord_cardinal_le 1;
+qed "lepoll_cardinal_le";
+
(*** The finite cardinals ***)
@@ -395,7 +461,7 @@
by (asm_simp_tac (ZF_ss addsimps [lepoll_def, inj_def,
succI1 RS Pi_empty2]) 1);
by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
-val nat_lepoll_imp_le_lemma = result();
+qed "nat_lepoll_imp_le_lemma";
bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
@@ -407,6 +473,7 @@
addSEs [eqpollE]) 1);
qed "nat_eqpoll_iff";
+(*The object of all this work: every natural number is a (finite) cardinal*)
goalw Cardinal.thy [Card_def,cardinal_def]
"!!n. n: nat ==> Card(n)";
by (rtac (Least_equality RS ssubst) 1);
@@ -527,6 +594,11 @@
by (fast_tac (ZF_cs addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1);
qed "singleton_eqpoll_1";
+goal Cardinal.thy "|{a}| = 1";
+by (resolve_tac [singleton_eqpoll_1 RS cardinal_cong RS trans] 1);
+by (simp_tac (arith_ss addsimps [nat_into_Card RS Card_cardinal_eq]) 1);
+qed "cardinal_singleton";
+
(*Congruence law for succ under equipollence*)
goalw Cardinal.thy [succ_def]
"!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";
@@ -597,9 +669,22 @@
by (fast_tac (eq_cs addEs [equalityE]) 1);
qed "lepoll_1_is_sing";
+goalw Cardinal.thy [lepoll_def] "A Un B lepoll A+B";
+by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1);
+by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1);
+by (split_tac [expand_if] 1);
+by (fast_tac (ZF_cs addSIs [InlI, InrI]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [Inl_def, Inr_def]
+ setloop split_tac [expand_if]) 1);
+qed "Un_lepoll_sum";
+
(*** Finite and infinite sets ***)
+goalw Cardinal.thy [Finite_def] "Finite(0)";
+by (fast_tac (ZF_cs addSIs [eqpoll_refl, nat_0I]) 1);
+qed "Finite_0";
+
goalw Cardinal.thy [Finite_def]
"!!A. [| A lepoll n; n:nat |] ==> Finite(A)";
by (etac rev_mp 1);
@@ -615,6 +700,8 @@
rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1);
qed "lepoll_Finite";
+bind_thm ("Finite_Diff", Diff_subset RS subset_imp_lepoll RS lepoll_Finite);
+
goalw Cardinal.thy [Finite_def] "!!x. Finite(x) ==> Finite(cons(y,x))";
by (excluded_middle_tac "y:x" 1);
by (asm_simp_tac (ZF_ss addsimps [cons_absorb]) 2);
@@ -623,11 +710,11 @@
by (etac nat_succI 2);
by (asm_simp_tac
(ZF_ss addsimps [succ_def, cons_eqpoll_cong, mem_not_refl]) 1);
-qed "Finite_imp_cons_Finite";
+qed "Finite_cons";
goalw Cardinal.thy [succ_def] "!!x. Finite(x) ==> Finite(succ(x))";
-by (etac Finite_imp_cons_Finite 1);
-qed "Finite_imp_succ_Finite";
+by (etac Finite_cons 1);
+qed "Finite_succ";
goalw Cardinal.thy [Finite_def]
"!!i. [| Ord(i); ~ Finite(i) |] ==> nat le i";
@@ -636,6 +723,12 @@
by (fast_tac (ZF_cs addSIs [eqpoll_refl] addSEs [ltE]) 1);
qed "nat_le_infinite_Ord";
+goalw Cardinal.thy [Finite_def, eqpoll_def]
+ "!!A. Finite(A) ==> EX r. well_ord(A,r)";
+by (fast_tac (ZF_cs addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel,
+ nat_into_Ord]) 1);
+qed "Finite_imp_well_ord";
+
(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
set is well-ordered. Proofs simplified by lcp. *)
--- a/src/ZF/CardinalArith.ML Tue Mar 26 11:38:17 1996 +0100
+++ b/src/ZF/CardinalArith.ML Tue Mar 26 11:42:36 1996 +0100
@@ -13,36 +13,6 @@
open CardinalArith;
-(*** Elementary properties ***)
-
-(*Use AC to discharge first premise*)
-goal CardinalArith.thy
- "!!A B. [| well_ord(B,r); A lepoll B |] ==> |A| le |B|";
-by (res_inst_tac [("i","|A|"),("j","|B|")] Ord_linear_le 1);
-by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
-by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1);
-by (rtac lepoll_trans 1);
-by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll) 1);
-by (assume_tac 1);
-by (etac (le_imp_subset RS subset_imp_lepoll RS lepoll_trans) 1);
-by (rtac eqpoll_imp_lepoll 1);
-by (rewtac lepoll_def);
-by (etac exE 1);
-by (rtac well_ord_cardinal_eqpoll 1);
-by (etac well_ord_rvimage 1);
-by (assume_tac 1);
-qed "well_ord_lepoll_imp_Card_le";
-
-(*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 (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]
- addSEs [mem_irrefl]) 1);
-qed "Fin_eqpoll";
-
(*** Cardinal addition ***)
(** Cardinal addition is commutative **)
@@ -493,8 +463,7 @@
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, Limit_has_succ]) 2);
-by (rtac (ordermap_z_lt RS leI RS le_imp_subset RS subset_imp_lepoll RS
- lepoll_trans) 1);
+by (rtac (ordermap_z_lt RS leI RS le_imp_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 (Limit_is_Ord RS well_ord_csquare) 1);
@@ -736,3 +705,109 @@
lt_csucc RS leI RSN (2,le_trans)]) 1);
qed "InfCard_csucc";
+
+(*** Finite sets ***)
+
+goal CardinalArith.thy
+ "!!n. n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
+by (eresolve_tac [nat_induct] 1);
+by (simp_tac (ZF_ss addsimps (eqpoll_0_iff::Fin.intrs)) 1);
+by (step_tac ZF_cs 1);
+by (subgoal_tac "EX u. u:A" 1);
+by (eresolve_tac [exE] 1);
+by (resolve_tac [Diff_sing_eqpoll RS revcut_rl] 1);
+by (assume_tac 2);
+by (assume_tac 1);
+by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1);
+by (assume_tac 1);
+by (resolve_tac [Fin.consI] 1);
+by (fast_tac ZF_cs 1);
+by (deepen_tac (ZF_cs addIs [Fin_mono RS subsetD]) 0 1); (*SLOW*)
+(*Now for the lemma assumed above*)
+by (rewrite_goals_tac [eqpoll_def]);
+by (fast_tac (ZF_cs addSEs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
+val lemma = result();
+
+goalw CardinalArith.thy [Finite_def] "!!A. Finite(A) ==> A : Fin(A)";
+by (fast_tac (ZF_cs addIs [lemma RS spec RS mp]) 1);
+qed "Finite_into_Fin";
+
+goal CardinalArith.thy "!!A. A : Fin(U) ==> Finite(A)";
+by (fast_tac (ZF_cs addSIs [Finite_0, Finite_cons] addEs [Fin.induct]) 1);
+qed "Fin_into_Finite";
+
+goal CardinalArith.thy "Finite(A) <-> A : Fin(A)";
+by (fast_tac (ZF_cs addIs [Finite_into_Fin] addEs [Fin_into_Finite]) 1);
+qed "Finite_Fin_iff";
+
+goal CardinalArith.thy
+ "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)";
+by (fast_tac (ZF_cs addSIs [Fin_into_Finite, Fin_UnI]
+ addSDs [Finite_into_Fin]
+ addSEs [Un_upper1 RS Fin_mono RS subsetD,
+ Un_upper2 RS Fin_mono RS subsetD]) 1);
+qed "Finite_Un";
+
+
+(** Removing elements from a finite set decreases its cardinality **)
+
+goal CardinalArith.thy
+ "!!A. A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A";
+by (eresolve_tac [Fin_induct] 1);
+by (simp_tac (ZF_ss addsimps [lepoll_0_iff]) 1);
+by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1);
+by (asm_simp_tac ZF_ss 1);
+by (fast_tac (ZF_cs addSDs [cons_lepoll_consD]) 1);
+by (fast_tac eq_cs 1);
+qed "Fin_imp_not_cons_lepoll";
+
+goal CardinalArith.thy
+ "!!a A. [| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)";
+by (rewrite_goals_tac [cardinal_def]);
+by (resolve_tac [Least_equality] 1);
+by (fold_tac [cardinal_def]);
+by (simp_tac (ZF_ss addsimps [succ_def]) 1);
+by (fast_tac (ZF_cs addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll]
+ addSEs [mem_irrefl]
+ addSDs [Finite_imp_well_ord]) 1);
+by (fast_tac (ZF_cs addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1);
+by (resolve_tac [notI] 1);
+by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] 1);
+by (eresolve_tac [le_imp_lepoll RS lepoll_trans] 1);
+by (fast_tac (ZF_cs addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll]
+ addSDs [Finite_imp_well_ord]) 1);
+qed "Finite_imp_cardinal_cons";
+
+
+goal CardinalArith.thy "!!a A. [| Finite(A); a:A |] ==> |A-{a}| < |A|";
+by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1);
+by (assume_tac 1);
+by (asm_simp_tac (ZF_ss addsimps [Finite_imp_cardinal_cons,
+ Diff_subset RS subset_imp_lepoll RS
+ lepoll_Finite]) 1);
+by (asm_simp_tac (ZF_ss addsimps [cons_Diff, Ord_cardinal RS le_refl]) 1);
+qed "Finite_imp_cardinal_Diff";
+
+
+(** Thanks to Krzysztof Grabczewski **)
+
+val nat_implies_well_ord = nat_into_Ord RS well_ord_Memrel;
+
+goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
+by (rtac eqpoll_trans 1);
+by (eresolve_tac [nat_implies_well_ord RS (
+ nat_implies_well_ord RSN (2,
+ well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1
+ THEN (assume_tac 1));
+by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1));
+by (asm_full_simp_tac (ZF_ss addsimps [cadd_def, eqpoll_refl]) 1);
+qed "nat_sum_eqpoll_sum";
+
+goal Nat.thy "!!m. [| m le n; n:nat |] ==> m:nat";
+by (fast_tac (ZF_cs addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))]
+ addSEs [ltE]) 1);
+qed "le_in_nat";
+
--- a/src/ZF/Cardinal_AC.ML Tue Mar 26 11:38:17 1996 +0100
+++ b/src/ZF/Cardinal_AC.ML Tue Mar 26 11:42:36 1996 +0100
@@ -26,6 +26,17 @@
by (REPEAT_SOME assume_tac);
qed "cardinal_eqE";
+goal Cardinal_AC.thy "|X| = |Y| <-> X eqpoll Y";
+by (fast_tac (ZF_cs addSEs [cardinal_cong, cardinal_eqE]) 1);
+qed "cardinal_eqpoll_iff";
+
+goal Cardinal_AC.thy
+ "!!A. [| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \
+\ |A Un C| = |B Un D|";
+by (asm_full_simp_tac (ZF_ss addsimps [cardinal_eqpoll_iff,
+ eqpoll_disjoint_Un]) 1);
+qed "cardinal_disjoint_Un";
+
goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";
by (resolve_tac [AC_well_ord RS exE] 1);
by (etac well_ord_lepoll_imp_Card_le 1);
--- a/src/ZF/upair.ML Tue Mar 26 11:38:17 1996 +0100
+++ b/src/ZF/upair.ML Tue Mar 26 11:42:36 1996 +0100
@@ -156,6 +156,15 @@
[ (rtac (disjCI RS (cons_iff RS iffD2)) 1),
(etac prem 1) ]);
+qed_goal "cons_neq_0" ZF.thy "cons(a,B)=0 ==> P"
+ (fn [major]=>
+ [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
+ (rtac consI1 1) ]);
+
+(*Useful for rewriting*)
+qed_goal "cons_not_0" ZF.thy "cons(a,B) ~= 0"
+ (fn _=> [ (rtac notI 1), (etac cons_neq_0 1) ]);
+
(*** Singletons - using cons ***)
qed_goal "singletonI" ZF.thy "a : {a}"
@@ -308,6 +317,10 @@
(* succ(c) <= B ==> c : B *)
val succ_subsetD = succI1 RSN (2,subsetD);
+(* succ(b) ~= b *)
+bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
+
+
qed_goal "succ_inject" ZF.thy "!!m n. succ(m) = succ(n) ==> m=n"
(fn _ =>
[ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD]