--- 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";
--- 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);
--- 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
--- 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
--- 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)";
--- 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]
--- 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));
--- 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);