# HG changeset patch
# User paulson
# Date 828006332 -3600
# Node ID 4b0608ce6150a9618c6a93233b3fb00292880d29
# Parent  d92f42acdb26b1a8a88ec9f0ebd5aace1453b5f0
New theorem Finite_imp_succ_cardinal_Diff

diff -r d92f42acdb26 -r 4b0608ce6150 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Wed Mar 27 18:48:50 1996 +0100
+++ b/src/ZF/CardinalArith.ML	Thu Mar 28 10:45:32 1996 +0100
@@ -710,11 +710,11 @@
 
 goal CardinalArith.thy
     "!!n. n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
-by (eresolve_tac [nat_induct] 1);
+by (etac 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 (etac exE 1);
 by (resolve_tac [Diff_sing_eqpoll RS revcut_rl] 1);
 by (assume_tac 2);
 by (assume_tac 1);
@@ -724,7 +724,7 @@
 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 (rewtac eqpoll_def);
 by (fast_tac (ZF_cs addSEs [bij_converse_bij RS bij_is_fun RS apply_type]) 1);
 val lemma = result();
 
@@ -744,8 +744,8 @@
     "!!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);
+                    addSEs [Un_upper1 RS Fin_mono RS subsetD,
+                            Un_upper2 RS Fin_mono RS subsetD]) 1);
 qed "Finite_Un";
 
 
@@ -753,7 +753,7 @@
 
 goal CardinalArith.thy
     "!!A. A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A";
-by (eresolve_tac [Fin_induct] 1);
+by (etac 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);
@@ -763,15 +763,15 @@
 
 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 (rewtac cardinal_def);
+by (rtac 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 (rtac 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);
@@ -782,13 +782,18 @@
 qed "Finite_imp_cardinal_cons";
 
 
-goal CardinalArith.thy "!!a A. [| Finite(A);  a:A |] ==> |A-{a}| < |A|";
+goal CardinalArith.thy "!!a A. [| Finite(A);  a:A |] ==> succ(|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);
+                                  Diff_subset RS subset_Finite]) 1);
+by (asm_simp_tac (ZF_ss addsimps [cons_Diff]) 1);
+qed "Finite_imp_succ_cardinal_Diff";
+
+goal CardinalArith.thy "!!a A. [| Finite(A);  a:A |] ==> |A-{a}| < |A|";
+by (rtac succ_leE 1);
+by (asm_simp_tac (ZF_ss addsimps [Finite_imp_succ_cardinal_Diff, 
+                                  Ord_cardinal RS le_refl]) 1);
 qed "Finite_imp_cardinal_Diff";