# HG changeset patch # User paulson # Date 902392737 -7200 # Node ID 9d1d4c43c76d8fee5af6f8a76cd78f25b3c0c80c # Parent 7538fce1fe372591ceae4959cb143ef2ebf07d2b Disjointness reasoning by AddEs [equals0E, sym RS equals0E] and consequential changes (and tidying) diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/AC16_WO4.ML --- 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 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)}; \ diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/AC18_AC19.ML --- 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"; diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/AC2_AC6.ML --- 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"; diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/AC7_AC9.ML --- 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(); diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/AC_Equiv.ML --- 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"; diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/DC.ML --- 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. : R); \ \ b:a; Z:Pow(X); Z lesspoll a |] \ \ ==> {x:X. : R} ~= 0"; -by (blast_tac (claset() addEs [equals0E]) 1); +by (Blast_tac 1); val lemmaX = result(); Goal "[| Card(K); well_ord(X,Q); \ diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/WO1_AC.ML --- 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"; diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/WO2_AC16.ML --- 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"; (* ********************************************************************** *) diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/AC/WO6_WO1.ML --- 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"; (* ********************************************************************** *) diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/Cardinal.ML --- 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"; diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/Coind/Map.ML --- 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 **) diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/WF.ML --- 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 **) diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/ZF.ML --- 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 ]); diff -r 7538fce1fe37 -r 9d1d4c43c76d src/ZF/Zorn.ML --- 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);