# HG changeset patch
# User paulson
# Date 947781090 -3600
# Node ID a71686059be0e529b8ed7c9ae18ad5108cece610
# Parent  b43ad07660b970e0e1388ec5d96fbd783892c8c8
a bit of tidying

diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Thu Jan 13 17:31:30 2000 +0100
@@ -44,8 +44,9 @@
 
 Goal "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)";
 by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1);
-by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS
-                well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1);
+by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS
+		 (Ord_Hartog RS
+		  well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1);
 by (fast_tac 
     (claset() addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired,
 		      HartogI RSN (2, lepoll_trans1),
@@ -55,9 +56,8 @@
 		      lepoll_paired RS lepoll_Finite]) 1);
 val lemma2 = result();
 
-val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)";
-by (fast_tac (claset()
-        addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1);
+Goal "~Finite(B) ==> ~Finite(A Un B)";
+by (blast_tac (claset() addIs [subset_Finite]) 1);
 qed "infinite_Un";
 
 (* ********************************************************************** *)
@@ -613,7 +613,8 @@
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (eres_inst_tac [("x","A Un y")] allE 1);
 by (ftac infinite_Un 1 THEN (mp_tac 1));
-by (etac zero_lt_natE 1); by (assume_tac 1);
+by (etac zero_lt_natE 1); 
+by (assume_tac 1);
 by (Clarify_tac 1);
 by (DEPTH_SOLVE (ares_tac [export conclusion] 1));
 qed "AC16_WO4";
diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/AC_Equiv.ML	Thu Jan 13 17:31:30 2000 +0100
@@ -4,9 +4,6 @@
 
 *)
 
-
-open AC_Equiv;
-
 val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def];
  
 val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def, 
@@ -99,10 +96,6 @@
         addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
 qed "inj_strengthen_type";
 
-Goalw [Finite_def] "n:nat ==> Finite(n)";
-by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
-qed "nat_into_Finite";
-
 Goalw [Finite_def] "~Finite(nat)";
 by (fast_tac (claset() addSDs [eqpoll_imp_lepoll]
                 addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1);
diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Thu Jan 13 17:31:30 2000 +0100
@@ -12,7 +12,10 @@
 but slightly changed.
 *)
 
-AC_Equiv = CardinalArith + Univ + 
+
+AC_Equiv = CardinalArith + Univ +
+           (*NOT "Main" because that theory includes AC!!!*)
+
 
 consts
   
diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML	Thu Jan 13 17:31:30 2000 +0100
@@ -11,17 +11,16 @@
 (* ********************************************************************** *)
 
 (* j=|A| *)
-goal Cardinal.thy
-    "!!A. [| A lepoll i; Ord(i) |] ==> EX j. j le i & A eqpoll j";
-by (fast_tac (claset() addIs [lepoll_cardinal_le, well_ord_Memrel,
-                            well_ord_cardinal_eqpoll RS eqpoll_sym]
-                    addDs [lepoll_well_ord]) 1);
+Goal "[| A lepoll i; Ord(i) |] ==> EX j. j le i & A eqpoll j";
+by (blast_tac (claset() addSIs [lepoll_cardinal_le, well_ord_Memrel,
+				well_ord_cardinal_eqpoll RS eqpoll_sym]
+                        addDs [lepoll_well_ord]) 1);
 qed "lepoll_imp_ex_le_eqpoll";
 
 (* j=|A| *)
-goalw Cardinal.thy [lesspoll_def]
-    "!!A a. [| A lesspoll i; Ord(i) |] ==> EX j. j<i & A eqpoll j";
-by (fast_tac (claset() addSDs [lepoll_imp_ex_le_eqpoll] addSEs [leE]) 1);
+Goalw [lesspoll_def]
+    "[| A lesspoll i; Ord(i) |] ==> EX j. j<i & A eqpoll j";
+by (blast_tac (claset() addSDs [lepoll_imp_ex_le_eqpoll] addSEs [leE]) 1);
 qed "lesspoll_imp_ex_lt_eqpoll";
 
 Goalw [InfCard_def] "[| ~Finite(i); Ord(i) |] ==> InfCard(|i|)";
@@ -161,7 +160,7 @@
 qed "UN_eq_UN_Diffs";
 
 Goalw [lepoll_def, eqpoll_def]
-        "a lepoll X ==> EX Y. Y<=X & a eqpoll Y";
+     "a lepoll X ==> EX Y. Y<=X & a eqpoll Y";
 by (etac exE 1);
 by (forward_tac [subset_refl RSN (2, restrict_bij)] 1);
 by (res_inst_tac [("x","f``a")] exI 1);
@@ -176,9 +175,9 @@
 \               A-B lesspoll a |] ==> P";
 by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE,
         Card_is_Ord, conjE] 1));
-by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper1_le))) 1
+by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper1_le) 1
         THEN (assume_tac 1));
-by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper2_le))) 1
+by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper2_le) 1
         THEN (assume_tac 1));
 by (dtac Un_least_lt 1 THEN (assume_tac 1));
 by (dresolve_tac [le_imp_lepoll RSN
diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/DC.ML	Thu Jan 13 17:31:30 2000 +0100
@@ -200,8 +200,7 @@
 
 Goalw [lesspoll_def, Finite_def]
         "A lesspoll nat ==> Finite(A)";
-by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll]
-                       addSIs [Ord_nat]) 1);
+by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll]) 1);
 qed "lesspoll_nat_is_Finite";
 
 Goal "n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)";
diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/DC_lemmas.ML
--- a/src/ZF/AC/DC_lemmas.ML	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/DC_lemmas.ML	Thu Jan 13 17:31:30 2000 +0100
@@ -85,9 +85,7 @@
 
 Goal "[| Ord(k); i:k |] ==> succ(i) : succ(k)";
 by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3));
-by (REPEAT (fast_tac (claset() addSIs [Ord_succ]
-        addEs [Ord_in_Ord, mem_irrefl, mem_asym]
-        addSDs [succ_inject]) 1));
+by (REPEAT (fast_tac (claset() addEs [Ord_in_Ord, mem_irrefl, mem_asym]) 1));
 qed "succ_in_succ";
 
 Goalw [restrict_def]
diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/WO2_AC16.ML	Thu Jan 13 17:31:30 2000 +0100
@@ -38,8 +38,8 @@
 \               ALL i j. i le j --> F(i) <= F(j); i<x; j<x; z<a;  \
 \               V: F(i); f(z)<=V; W:F(j); f(z)<=W |]  \
 \               ==> V = W";
-by (res_inst_tac [("j","j")] (lt_Ord RS (lt_Ord RSN (2, Ord_linear_le))) 1
-        THEN (REPEAT (assume_tac 1)));
+by (res_inst_tac [("j","j")] ([lt_Ord, lt_Ord] MRS Ord_linear_le) 1
+    THEN (REPEAT (assume_tac 1)));
 by (eresolve_tac [lemma3_1 RS sym] 1 THEN (REPEAT (assume_tac 1)));
 by (etac lemma3_1 1 THEN (REPEAT (assume_tac 1)));
 val lemma3 = result();
@@ -118,7 +118,7 @@
 
 
 Goalw [lesspoll_def]
-        "!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a";
+        "[| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a";
 by (rtac conjI 1);
 by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1
         THEN (assume_tac 1));
@@ -129,48 +129,13 @@
         subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1);
 qed "Finite_lesspoll_infinite_Ord";
 
-
-Goal "x:X ==> Union(X) = Union(X-{x}) Un x";
-by (Fast_tac 1);
-qed "Union_eq_Un_Diff";
-
-
-Goal "n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x))  \
-\       --> Finite(Union(X))";
-by (induct_tac "n" 1);
-by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]
-        addSIs [nat_0I RS nat_into_Finite] addss (simpset())) 1);
-by (REPEAT (resolve_tac [allI, impI] 1));
-by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1));
-by (res_inst_tac [("P","%z. Finite(z)")] (Union_eq_Un_Diff RS ssubst) 1
-        THEN (assume_tac 1));
-by (rtac Finite_Un 1);
-by (Fast_tac 2);
-by (fast_tac (claset() addSIs [Diff_sing_eqpoll]) 1);
-qed "Finite_Union_lemma";
-
-
-Goal "[| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))";
-by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1);
-by (dtac Finite_Union_lemma 1);
-by (Fast_tac 1);
-qed "Finite_Union";
-
-
-Goalw [Finite_def] "[| x lepoll n; n:nat |] ==> Finite(x)";
-by (fast_tac (claset()
-        addEs [nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll) RS exE,
-        Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD]) 1);
-qed "lepoll_nat_num_imp_Finite";
-
-
 Goal "[| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b;  \
 \       b<a; ~Finite(a); Card(a); n:nat |]  \
 \       ==> Union(X) lesspoll a";
 by (excluded_middle_tac "Finite(X)" 1);
 by (resolve_tac [Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord)] 2
         THEN (REPEAT (assume_tac 3)));
-by (fast_tac (claset() addSEs [lepoll_nat_num_imp_Finite]
+by (fast_tac (claset() addSEs [lepoll_nat_imp_Finite]
                 addSIs [Finite_Union]) 2);
 by (dresolve_tac [lt_Ord RSN (2, lepoll_imp_ex_le_eqpoll)] 1 THEN (assume_tac 1));
 by (REPEAT (eresolve_tac [exE, conjE] 1));
@@ -311,8 +276,9 @@
 by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac));
 by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1)));
 by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1));
-by (resolve_tac [nat_succI RSN (2, bexI RS (Finite_def RS def_imp_iff RS
-        iffD2)) RS (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1
+by (resolve_tac [nat_succI RSN 
+		 (2, bexI RS (Finite_def RS def_imp_iff RS iffD2)) RS 
+		 (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1
         THEN (TRYALL assume_tac));
 by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type) RS CollectE] 1
         THEN (TRYALL assume_tac));
@@ -320,17 +286,16 @@
 
 (* back to the proof *)
 
-val disj_Un_eqpoll_nat_sum = disj_Un_eqpoll_sum RS (
-                             sum_eqpoll_cong RSN (2, 
-                             nat_sum_eqpoll_sum RSN (3, 
-                             eqpoll_trans RS eqpoll_trans))) |> standard;
+val disj_Un_eqpoll_nat_sum = 
+    [disj_Un_eqpoll_sum, sum_eqpoll_cong, nat_sum_eqpoll_sum] MRS 
+    (eqpoll_trans RS eqpoll_trans) |> standard;
 
 
 Goal "[| x : Pow(A - B - fa`i); x eqpoll m;  \
 \       fa : bij(a, {x: Pow(A) . x eqpoll k}); i<a; k:nat; m:nat |]  \
 \       ==> fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}";
 by (rtac CollectI 1);
-by (fast_tac (claset() addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))] 
+by (fast_tac (claset() 
         addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1);
 by (rtac disj_Un_eqpoll_nat_sum 1
         THEN (TRYALL assume_tac));
diff -r b43ad07660b9 -r a71686059be0 src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/WO6_WO1.ML	Thu Jan 13 17:31:30 2000 +0100
@@ -57,10 +57,10 @@
 (* Two cases for lemma ii                                                 *)
 (* ********************************************************************** *)
 Goalw [lesspoll_def] 
-  "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==>  \
-\            (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 &  \
-\                                       u(f,b,g,d) lesspoll m)) |  \
-\            (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 -->  \
+     "ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m  \
+\     ==> (ALL b<a. f`b ~= 0 --> \
+\                 (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & u(f,b,g,d) lesspoll m)) \
+\       | (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 -->  \
 \                                       u(f,b,g,d) eqpoll m))";
 by (Asm_simp_tac 1);
 by (blast_tac (claset() delrules [equalityI]) 1);