Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
and consequential changes (and tidying)
--- a/src/ZF/AC/AC16_WO4.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Thu Aug 06 10:38:57 1998 +0200
@@ -99,15 +99,11 @@
by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1);
qed "succ_not_lepoll_imp_eqpoll";
-val [prem] = goalw thy [s_u_def]
+val [prem] = Goalw [s_u_def]
"(ALL v:s_u(u, t_n, k, y). k eqpoll v Int y ==> False) \
\ ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
by (resolve_tac [prem RS FalseE] 1);
-by (rtac ballI 1);
-by (etac CollectE 1);
-by (etac conjE 1);
-by (etac swap 1);
by (fast_tac (claset() addSEs [succ_not_lepoll_imp_eqpoll]) 1);
qed "suppose_not";
@@ -117,8 +113,7 @@
Goalw [lepoll_def, eqpoll_def]
"[| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y";
-by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)]
- addSIs [subset_refl]
+by (fast_tac (subset_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)]
addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1);
qed "nat_lepoll_imp_ex_eqpoll_n";
@@ -137,9 +132,9 @@
Goalw [lesspoll_def] "n: nat ==> n lesspoll nat";
by (fast_tac (claset() addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll,
- eqpoll_sym RS eqpoll_imp_lepoll]
- addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI
- RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1);
+ eqpoll_sym RS eqpoll_imp_lepoll]
+ addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI
+ RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1);
qed "n_lesspoll_nat";
Goal "[| well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; k: nat |] \
@@ -162,7 +157,7 @@
Goal "[| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0 \
\ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))";
-by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0E]) 1);
+by (fast_tac (claset() addSIs [cons_eqpoll_succ]) 1);
qed "cons_cons_eqpoll";
Goalw [s_u_def] "s_u(u, t_n, k, y) <= t_n";
@@ -180,8 +175,7 @@
by (Fast_tac 1);
qed "in_s_u_imp_u_in";
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
\ EX! w. w:t_n & z <= w; \
\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |] \
\ ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c";
@@ -193,16 +187,15 @@
by (rtac conjI 1);
by (rtac CollectI 1);
by (fast_tac (FOL_cs addSEs [s_uI]) 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
by (etac allE 1);
by (etac impE 1);
by (assume_tac 2);
by (fast_tac (claset() addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
qed "ex1_superset_a";
-Goal
- "[| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \
+Goal "[| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \
\ |] ==> A = cons(a, B)";
by (rtac equalityI 1);
by (Fast_tac 2);
@@ -219,13 +212,12 @@
(lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1);
qed "set_eq_cons";
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
-\ EX! w. w:t_n & z <= w; \
-\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \
-\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0; k:nat \
-\ |] ==> (THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c) \
-\ Int y = cons(b, a)";
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
+\ EX! w. w:t_n & z <= w; \
+\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \
+\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0; k:nat |] \
+\ ==> (THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c) \
+\ Int y = cons(b, a)";
by (dresolve_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1));
by (rtac set_eq_cons 1);
by (REPEAT (Fast_tac 1));
@@ -248,8 +240,7 @@
(* where a is certain k-2 element subset of y *)
(* ********************************************************************** *)
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
\ EX! w. w:t_n & z <= w; \
\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \
\ well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; \
@@ -282,8 +273,7 @@
(* some arithmetic *)
(* ********************************************************************** *)
-Goal
- "[| k:nat; m:nat |] ==> \
+Goal "[| k:nat; m:nat |] ==> \
\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m";
by (eres_inst_tac [("n","k")] nat_induct 1);
by (simp_tac (simpset() addsimps [add_0]) 1);
@@ -314,8 +304,7 @@
(* similar properties for eqpoll *)
(* ********************************************************************** *)
-Goal
- "[| k:nat; m:nat |] ==> \
+Goal "[| k:nat; m:nat |] ==> \
\ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m";
by (eres_inst_tac [("n","k")] nat_induct 1);
by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0]
@@ -348,7 +337,7 @@
Goal "[| x Int y = 0; w <= x Un y |] \
\ ==> w Int (x - {u}) = w - cons(u, w Int y)";
-by (fast_tac (claset() addEs [equals0E]) 1);
+by (Fast_tac 1);
qed "w_Int_eq_w_Diff";
Goal "[| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \
@@ -359,7 +348,7 @@
by (etac CollectE 1);
by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1));
by (fast_tac (claset() addSDs [s_u_subset RS subsetD]) 1);
-by (fast_tac (claset() addEs [equals0E] addSDs [bspec]
+by (fast_tac (claset() addSDs [bspec]
addDs [s_u_subset RS subsetD]
addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in]
addSIs [eqpoll_sum_imp_Diff_eqpoll]) 1);
@@ -370,10 +359,9 @@
addSEs [mem_irrefl, ltE, eqpoll_succ_imp_not_empty, natE]) 1);
qed "eqpoll_m_not_empty";
-Goal
- "[| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \
-\ |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}";
-by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0E, eqpoll_sym]) 1);
+Goal "[| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x |] \
+\ ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}";
+by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [eqpoll_sym]) 1);
qed "cons_cons_in";
(* ********************************************************************** *)
@@ -381,8 +369,7 @@
(* to {v:Pow(x). v eqpoll n-k} *)
(* ********************************************************************** *)
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \
\ EX! w. w:t_n & z <= w; \
\ t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \
\ 0<m; m:nat; l:nat; \
@@ -407,18 +394,16 @@
by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1));
by (etac ex1_two_eq 1);
-by (fast_tac (claset() addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
-by (fast_tac (claset() addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
+by (REPEAT (blast_tac
+ (claset() addDs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1));
qed "subset_s_u_lepoll_w";
Goal "[| 0<k; k:nat |] ==> EX l:nat. k = succ(l)";
by (etac natE 1);
-by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1);
-by (fast_tac (empty_cs addSIs [refl, bexI]) 1);
+by Auto_tac;
qed "ex_eq_succ";
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
\ EX! w. w:t_n & z <= w; \
\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \
@@ -467,23 +452,6 @@
qed "Int_empty";
(* ********************************************************************** *)
-(* unit set is well-ordered by the empty relation *)
-(* ********************************************************************** *)
-
-Goalw [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def]
- "tot_ord({a},0)";
-by (Simp_tac 1);
-qed "tot_ord_unit";
-
-Goalw [wf_on_def, wf_def] "wf[{a}](0)";
-by (Fast_tac 1);
-qed "wf_on_unit";
-
-Goalw [well_ord_def] "well_ord({a},0)";
-by (simp_tac (simpset() addsimps [tot_ord_unit, wf_on_unit]) 1);
-qed "well_ord_unit";
-
-(* ********************************************************************** *)
(* well_ord_subsets_lepoll_n *)
(* ********************************************************************** *)
@@ -547,8 +515,7 @@
(* The union of appropriate values is the whole x *)
(* ********************************************************************** *)
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
\ EX! w. w:t_n & z <= w; \
\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \
@@ -568,8 +535,7 @@
by (Fast_tac 1);
qed "MM_subset";
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
\ EX! w. w:t_n & z <= w; \
\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \
@@ -583,7 +549,7 @@
by (asm_full_simp_tac (simpset() delsimps ball_simps addsimps [Int_in_LL]) 1);
by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1
THEN (assume_tac 1));
-by (REPEAT (fast_tac (claset() addEs [equals0E] addSEs [Int_in_LL]) 1));
+by (REPEAT (fast_tac (claset() addSEs [Int_in_LL]) 1));
qed "exists_in_LL";
Goalw [LL_def]
@@ -595,8 +561,7 @@
unique_superset_in_MM RS the_equality2 RS ssubst]) 1);
qed "in_LL_eq_Int";
-Goal
- "[| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
+Goal "[| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
\ t_n <= {v:Pow(x Un y). v eqpoll n}; \
\ v : LL(t_n, k, y) |] \
\ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y";
@@ -618,8 +583,7 @@
by (fast_tac (claset() addEs [ssubst]) 1);
qed "GG_subset";
-Goal
- "[| well_ord(LL(t_n, succ(k), y), S); \
+Goal "[| well_ord(LL(t_n, succ(k), y), S); \
\ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \
\ well_ord(y,R); ~Finite(y); x Int y = 0; \
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \
--- a/src/ZF/AC/AC18_AC19.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/AC18_AC19.ML Thu Aug 06 10:38:57 1998 +0200
@@ -25,13 +25,13 @@
by (rtac subsetI 1);
by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1);
by (etac impE 1);
-by (fast_tac (claset() addEs [sym RS equals0E]) 1);
+by (Fast_tac 1);
by (etac exE 1);
by (rtac UN_I 1);
by (fast_tac (claset() addSEs [PROD_subsets]) 1);
by (Simp_tac 1);
-by (fast_tac (claset() addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)]
- ) 1);
+by (fast_tac (claset() addSEs [not_emptyE]
+ addDs [RepFunI RSN (2, apply_type)]) 1);
qed "lemma_AC18";
val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
--- a/src/ZF/AC/AC2_AC6.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/AC2_AC6.ML Thu Aug 06 10:38:57 1998 +0200
@@ -21,7 +21,7 @@
Goalw [pairwise_disjoint_def]
"[| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C";
-by (fast_tac (claset() addSEs [equals0E]) 1);
+by (Fast_tac 1);
val lemma2 = result();
Goalw AC_defs "AC1 ==> AC2";
@@ -39,8 +39,7 @@
(* ********************************************************************** *)
Goal "0~:A ==> 0 ~: {B*{B}. B:A}";
-by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]
- addSEs [equals0E]) 1);
+by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]) 1);
val lemma1 = result();
Goal "[| X*{X} Int C = {y}; X:A |] \
@@ -72,7 +71,7 @@
(* ********************************************************************** *)
Goal "0 ~: {R``{x}. x:domain(R)}";
-by (fast_tac (claset() addEs [sym RS equals0E]) 1);
+by (Blast_tac 1);
val lemma = result();
Goalw AC_defs "AC1 ==> AC4";
@@ -194,6 +193,6 @@
(* ********************************************************************** *)
Goalw AC_defs "AC1 <-> AC6";
-by (blast_tac (claset() addEs [equals0E]) 1);
+by (Blast_tac 1);
qed "AC1_iff_AC6";
--- a/src/ZF/AC/AC7_AC9.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/AC7_AC9.ML Thu Aug 06 10:38:57 1998 +0200
@@ -18,10 +18,8 @@
qed "mem_not_eq_not_mem";
Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
-by (fast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
- addDs [fun_space_emptyD, mem_not_eq_not_mem]
- addEs [equals0E]
- addSIs [equals0I,UnionI]) 1);
+by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
+ addDs [fun_space_emptyD, mem_not_eq_not_mem]) 1);
qed "Sigma_fun_space_not0";
Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
@@ -30,24 +28,18 @@
THEN REPEAT (assume_tac 1));
qed "all_eqpoll_imp_pair_eqpoll";
-Goal "[| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A \
-\ |] ==> P(b)=R(b)";
-by (dtac bspec 1 THEN (assume_tac 1));
-by (Asm_full_simp_tac 1);
+Goal "[| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A |] \
+\ ==> P(b)=R(b)";
+by Auto_tac;
qed "if_eqE1";
Goal "ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \
\ ==> ALL a:A. a~=b --> Q(a)=S(a)";
-by (rtac ballI 1);
-by (rtac impI 1);
-by (dtac bspec 1 THEN (assume_tac 1));
-by (Asm_full_simp_tac 1);
+by Auto_tac;
qed "if_eqE2";
Goal "[| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
-by (fast_tac (claset() addDs [subsetD]
- addSIs [lamI]
- addEs [equalityE, lamE]) 1);
+by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1);
qed "lam_eqE";
Goalw [inj_def]
@@ -84,7 +76,7 @@
(* ********************************************************************** *)
Goalw AC_defs "AC6 ==> AC7";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "AC6_AC7";
(* ********************************************************************** *)
@@ -97,13 +89,11 @@
by (fast_tac (claset() addSIs [lam_type, snd_type, apply_type]) 1);
val lemma1_1 = result();
-Goal "y: (PROD B:{Y*C. C:A}. B) \
-\ ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
+Goal "y: (PROD B:{Y*C. C:A}. B) ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
val lemma1_2 = result();
-Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 \
-\ ==> (PROD B:A. B) ~= 0";
+Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 ==> (PROD B:A. B) ~= 0";
by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]
addSEs [equals0E]) 1);
val lemma1 = result();
--- a/src/ZF/AC/AC_Equiv.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Thu Aug 06 10:38:57 1998 +0200
@@ -118,10 +118,6 @@
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
qed "inj_strengthen_type";
-Goal "A*B=0 <-> A=0 | B=0";
-by (fast_tac (claset() addSIs [equals0I] addEs [equals0E]) 1);
-qed "Sigma_empty_iff";
-
Goalw [Finite_def] "n:nat ==> Finite(n)";
by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
qed "nat_into_Finite";
--- a/src/ZF/AC/DC.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/DC.ML Thu Aug 06 10:38:57 1998 +0200
@@ -574,7 +574,7 @@
Goal "[| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R); \
\ b:a; Z:Pow(X); Z lesspoll a |] \
\ ==> {x:X. <Z,x> : R} ~= 0";
-by (blast_tac (claset() addEs [equals0E]) 1);
+by (Blast_tac 1);
val lemmaX = result();
Goal "[| Card(K); well_ord(X,Q); \
--- a/src/ZF/AC/WO1_AC.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/WO1_AC.ML Thu Aug 06 10:38:57 1998 +0200
@@ -44,12 +44,11 @@
by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1);
by (etac exE 1);
by (dtac ex_choice_fun 1);
-by (fast_tac (claset() addEs [sym RS equals0E]) 1);
+by (Fast_tac 1);
by (etac exE 1);
by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1);
by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addSDs [RepFunI RSN (2, apply_type)]
- addSEs [CollectD2]) 1);
+by (blast_tac (claset() addSDs [RepFunI RSN (2, apply_type)]) 1);
val lemma1 = result();
Goalw [WO1_def] "[| ~Finite(B); WO1 |] ==> |B| + |B| eqpoll B";
--- a/src/ZF/AC/WO2_AC16.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/WO2_AC16.ML Thu Aug 06 10:38:57 1998 +0200
@@ -378,12 +378,12 @@
Goal "[| A <= B Un C; A Int C = 0 |] ==> A <= B";
-by (fast_tac (claset() addEs [equals0E]) 1);
+by (Blast_tac 1);
qed "subset_Un_disjoint";
Goal "[| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0";
-by (fast_tac (claset() addSIs [equals0I]) 1);
+by (Blast_tac 1);
qed "Int_empty";
(* ********************************************************************** *)
--- a/src/ZF/AC/WO6_WO1.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Thu Aug 06 10:38:57 1998 +0200
@@ -375,7 +375,7 @@
(* ********************************************************************** *)
Goalw [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
-by (fast_tac (ZF_cs addEs [equals0E]) 1);
+by (fast_tac ZF_cs 1); (*SLOW if current claset is used*)
qed "WO6_imp_NN_not_empty";
(* ********************************************************************** *)
--- a/src/ZF/Cardinal.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/Cardinal.ML Thu Aug 06 10:38:57 1998 +0200
@@ -635,7 +635,7 @@
setloop etac UnE') 1);
by (asm_simp_tac
(simpset() addsimps [inj_converse_fun RS apply_funtype, right_inverse]) 1);
-by (blast_tac (claset() addEs [equals0E]) 1);
+by (Blast_tac 1);
qed "inj_disjoint_eqpoll";
@@ -684,7 +684,7 @@
Goalw [eqpoll_def] "A Int B = 0 ==> A Un B eqpoll A + B";
by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
-by (auto_tac (claset() addEs [equals0E], simpset()));
+by Auto_tac;
qed "disj_Un_eqpoll_sum";
--- a/src/ZF/Coind/Map.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/Coind/Map.ML Thu Aug 06 10:38:57 1998 +0200
@@ -8,28 +8,25 @@
(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
-
-Goalw [TMap_def]
- "{0,1} <= {1} Un TMap(I, {0,1})";
+Goalw [TMap_def] "{0,1} <= {1} Un TMap(I, {0,1})";
by (Blast_tac 1);
result();
-Goalw [TMap_def]
- "{0} Un TMap(I,1) <= {1} Un TMap(I, {0} Un TMap(I,1))";
+Goalw [TMap_def] "{0} Un TMap(I,1) <= {1} Un TMap(I, {0} Un TMap(I,1))";
by (Blast_tac 1);
result();
-Goalw [TMap_def]
- "{0,1} Un TMap(I,2) <= {1} Un TMap(I, {0,1} Un TMap(I,2))";
+Goalw [TMap_def] "{0,1} Un TMap(I,2) <= {1} Un TMap(I, {0,1} Un TMap(I,2))";
by (Blast_tac 1);
result();
+(*TOO SLOW
Goalw [TMap_def]
"{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) <= \
\ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
-(*twice as fast as Blast_tac alone*)
-by (Safe_tac THEN ALLGOALS Blast_tac);
+by (Blast_tac 1);
result();
+*)
(* ############################################################ *)
@@ -48,9 +45,6 @@
by (Fast_tac 1);
qed "image_Sigma1";
-Goal "0``A = 0";
-by (Fast_tac 1);
-qed "image_02";
(* ############################################################ *)
(* Inclusion in Quine Universes *)
@@ -95,8 +89,7 @@
(** map_emp **)
Goalw [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
-by Safe_tac;
-by (rtac image_02 1);
+by Auto_tac;
qed "pmap_empI";
(** map_owr **)
--- a/src/ZF/WF.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/WF.ML Thu Aug 06 10:38:57 1998 +0200
@@ -38,13 +38,11 @@
qed "wf_iff_wf_on_field";
Goalw [wf_on_def, wf_def] "[| wf[A](r); B<=A |] ==> wf[B](r)";
-by (Clarify_tac 1); (*essential for Blast_tac's efficiency*)
-by (Blast_tac 1);
+by (Fast_tac 1);
qed "wf_on_subset_A";
Goalw [wf_on_def, wf_def] "[| wf[A](r); s<=r |] ==> wf[A](s)";
-by (Clarify_tac 1); (*essential for Blast_tac's efficiency*)
-by (Blast_tac 1);
+by (Fast_tac 1);
qed "wf_on_subset_r";
(** Introduction rules for wf_on **)
--- a/src/ZF/ZF.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/ZF.ML Thu Aug 06 10:38:57 1998 +0200
@@ -447,6 +447,8 @@
qed_goal "equals0E" ZF.thy "!!P. [| A=0; a:A |] ==> P"
(fn _=> [ Full_simp_tac 1, Blast_tac 1 ]);
+AddEs [equals0E, sym RS equals0E];
+
qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
(fn _=> [ Blast_tac 1 ]);
--- a/src/ZF/Zorn.ML Thu Aug 06 10:37:39 1998 +0200
+++ b/src/ZF/Zorn.ML Thu Aug 06 10:38:57 1998 +0200
@@ -261,7 +261,7 @@
by (asm_full_simp_tac (simpset() addsimps [maxchain_def]) 1);
by (rename_tac "c" 1);
by (res_inst_tac [("x", "Union(c)")] bexI 1);
-by (Blast_tac 2);
+by (Fast_tac 2); (*Blast_tac: PROOF FAILED*)
by Safe_tac;
by (rename_tac "z" 1);
by (rtac classical 1);