# HG changeset patch # User lcp # Date 806925672 -7200 # Node ID 3f460842e91953540c3e649cf521bb653fabdab9 # Parent 30df104ceb91b256ae90532aa61f2cc180e80d55 Ran expandshort and changed spelling of Grabczewski diff -r 30df104ceb91 -r 3f460842e919 src/ZF/AC/AC7_AC9.ML --- a/src/ZF/AC/AC7_AC9.ML Fri Jul 28 11:48:55 1995 +0200 +++ b/src/ZF/AC/AC7_AC9.ML Fri Jul 28 12:01:12 1995 +0200 @@ -1,6 +1,6 @@ (* Title: ZF/AC/AC7-AC9.ML ID: $Id$ - Author: Krzysztof Gr`abczewski + Author: Krzysztof Grabczewski The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous instances of AC. @@ -25,22 +25,22 @@ val Sigma_fun_space_not0 = result(); goal thy "!!A C. (ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)"; -by (REPEAT (resolve_tac [ballI] 1)); +by (REPEAT (rtac ballI 1)); by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1 THEN REPEAT (assume_tac 1)); val all_eqpoll_imp_pair_eqpoll = result(); goal thy "!!A. [| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A \ \ |] ==> P(b)=R(b)"; -by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (dtac bspec 1 THEN (assume_tac 1)); by (asm_full_simp_tac ZF_ss 1); val if_eqE1 = result(); goal thy "!!A. 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 (resolve_tac [ballI] 1); -by (resolve_tac [impI] 1); -by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (rtac ballI 1); +by (rtac impI 1); +by (dtac bspec 1 THEN (assume_tac 1)); by (asm_full_simp_tac ZF_ss 1); val if_eqE2 = result(); @@ -54,18 +54,18 @@ "!!A. C:A ==> (lam g:(nat->Union(A))*C. \ \ (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \ \ : inj((nat->Union(A))*C, (nat->Union(A)) ) "; -by (resolve_tac [CollectI] 1); +by (rtac CollectI 1); by (fast_tac (ZF_cs addSIs [lam_type,RepFunI,if_type,snd_type,apply_type, fst_type,diff_type,nat_succI,nat_0I]) 1); by (REPEAT (resolve_tac [ballI, impI] 1)); by (asm_full_simp_tac ZF_ss 1); -by (REPEAT (eresolve_tac [SigmaE] 1)); +by (REPEAT (etac SigmaE 1)); by (REPEAT (hyp_subst_tac 1)); by (asm_full_simp_tac ZF_ss 1); -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (dresolve_tac [nat_0I RSN (2, lam_eqE)] 2); by (asm_full_simp_tac AC_ss 2); -by (resolve_tac [fun_extension] 1 THEN REPEAT (assume_tac 1)); +by (rtac fun_extension 1 THEN REPEAT (assume_tac 1)); by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (assume_tac 1)); by (asm_full_simp_tac (AC_ss addsimps [succ_not_0 RS if_not_P]) 1); by (fast_tac (AC_cs addSEs [diff_succ_succ RS (diff_0 RSN (2, trans)) RS subst] @@ -73,10 +73,10 @@ val lemma = result(); goal thy "!!A. [| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))"; -by (resolve_tac [eqpollI] 1); +by (rtac eqpollI 1); by (fast_tac (ZF_cs addSEs [prod_lepoll_self, not_sym RS not_emptyE, subst_elem] addEs [swap]) 2); -by (rewrite_goals_tac [lepoll_def]); +by (rewtac lepoll_def); by (fast_tac (ZF_cs addSIs [lemma]) 1); val Sigma_fun_space_eqpoll = result(); @@ -116,13 +116,13 @@ val lemma2 = result(); goalw thy AC_defs "!!Z. AC7 ==> AC6"; -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); +by (rtac allI 1); +by (rtac impI 1); by (excluded_middle_tac "A=0" 1); by (fast_tac (ZF_cs addSIs [not_emptyI, empty_fun]) 2); -by (resolve_tac [lemma1] 1); -by (eresolve_tac [allE] 1); -by (eresolve_tac [impE] 1 THEN (assume_tac 2)); +by (rtac lemma1 1); +by (etac allE 1); +by (etac impE 1 THEN (assume_tac 2)); by (fast_tac (AC_cs addSEs [RepFunE] addSIs [lemma2, all_eqpoll_imp_pair_eqpoll, Sigma_fun_space_eqpoll]) 1); @@ -136,9 +136,9 @@ goalw thy [eqpoll_def] "!!A. ALL B:A. EX B1 B2. B= & B1 eqpoll B2 \ \ ==> 0 ~: { bij(fst(B),snd(B)). B:A }"; -by (resolve_tac [notI] 1); -by (eresolve_tac [RepFunE] 1); -by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (rtac notI 1); +by (etac RepFunE 1); +by (dtac bspec 1 THEN (assume_tac 1)); by (REPEAT (eresolve_tac [exE,conjE] 1)); by (hyp_subst_tac 1); by (asm_full_simp_tac AC_ss 1); @@ -152,11 +152,11 @@ val lemma2 = result(); goalw thy AC_defs "!!Z. AC1 ==> AC8"; -by (resolve_tac [allI] 1); -by (eresolve_tac [allE] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [impE] 1); -by (eresolve_tac [lemma1] 1); +by (rtac allI 1); +by (etac allE 1); +by (rtac impI 1); +by (etac impE 1); +by (etac lemma1 1); by (fast_tac (AC_cs addSEs [lemma2]) 1); qed "AC1_AC8"; @@ -177,11 +177,11 @@ val lemma2 = result(); goalw thy AC_defs "!!Z. AC8 ==> AC9"; -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [allE] 1); -by (eresolve_tac [impE] 1); -by (eresolve_tac [lemma1] 1); +by (rtac allI 1); +by (rtac impI 1); +by (etac allE 1); +by (etac impE 1); +by (etac lemma1 1); by (fast_tac (AC_cs addSEs [lemma2]) 1); qed "AC8_AC9"; @@ -218,20 +218,20 @@ \ Un {cons(0,(F*B)*N). B:A}. f` : bij(B1, B2) \ \ ==> (lam B:A. snd(fst((f`)`0))) : \ \ (PROD X:A. X)"; -by (resolve_tac [lam_type] 1); -by (resolve_tac [snd_type] 1); -by (resolve_tac [fst_type] 1); +by (rtac lam_type 1); +by (rtac snd_type 1); +by (rtac fst_type 1); by (resolve_tac [consI1 RSN (2, apply_type)] 1); by (fast_tac (ZF_cs addSIs [fun_weaken_type, bij_is_fun]) 1); val lemma2 = result(); goalw thy AC_defs "!!Z. AC9 ==> AC1"; -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [allE] 1); +by (rtac allI 1); +by (rtac impI 1); +by (etac allE 1); by (excluded_middle_tac "A=0" 1); by (fast_tac (FOL_cs addSIs [empty_fun]) 2); -by (eresolve_tac [impE] 1); -by (resolve_tac [lemma1] 1 THEN (REPEAT (assume_tac 1))); +by (etac impE 1); +by (rtac lemma1 1 THEN (REPEAT (assume_tac 1))); by (fast_tac (AC_cs addSEs [lemma2]) 1); qed "AC9_AC1"; diff -r 30df104ceb91 -r 3f460842e919 src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Fri Jul 28 11:48:55 1995 +0200 +++ b/src/ZF/AC/AC_Equiv.ML Fri Jul 28 12:01:12 1995 +0200 @@ -1,6 +1,6 @@ (* Title: ZF/AC/AC_Equiv.ML ID: $Id$ - Author: Krzysztof Gr`abczewski + Author: Krzysztof Grabczewski *) @@ -71,7 +71,7 @@ (*I don't know where to put this one.*) goal Cardinal.thy "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; -by (resolve_tac [not_emptyE] 1 THEN (assume_tac 1)); +by (rtac not_emptyE 1 THEN (assume_tac 1)); by (forward_tac [singleton_subsetI] 1); by (forward_tac [subsetD] 1 THEN (assume_tac 1)); by (res_inst_tac [("A2","A")] @@ -90,7 +90,7 @@ (* lemma for ordertype_Int *) goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; -by (resolve_tac [equalityI] 1); +by (rtac equalityI 1); by (step_tac ZF_cs 1); by (dres_inst_tac [("P","%a. :r")] (id_conv RS subst) 1 THEN (assume_tac 1)); @@ -156,7 +156,7 @@ (* ********************************************************************** *) goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y"; -by (eresolve_tac [ex1E] 1); +by (etac ex1E 1); by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); by (fast_tac AC_cs 1); by (fast_tac AC_cs 1); @@ -167,7 +167,7 @@ (* ********************************************************************** *) goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B"; -by (eresolve_tac [CollectE] 1); +by (etac CollectE 1); by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [RepFunE, apply_type] addSIs [RepFunI] addIs [equalityI]) 1); diff -r 30df104ceb91 -r 3f460842e919 src/ZF/AC/Cardinal_aux.ML --- a/src/ZF/AC/Cardinal_aux.ML Fri Jul 28 11:48:55 1995 +0200 +++ b/src/ZF/AC/Cardinal_aux.ML Fri Jul 28 12:01:12 1995 +0200 @@ -1,6 +1,6 @@ (* Title: ZF/AC/Cardinal_aux.ML ID: $Id$ - Author: Krzysztof Gr`abczewski + Author: Krzysztof Grabczewski Auxiliary lemmas concerning cardinalities *) @@ -15,8 +15,8 @@ val nat_0_in_2 = Ord_0 RS le_refl RS leI RS ltD; goalw thy [InfCard_def] "!!i. [| ~Finite(i); Ord(i) |] ==> InfCard(|i|)"; -by (resolve_tac [conjI] 1); -by (resolve_tac [Card_cardinal] 1); +by (rtac conjI 1); +by (rtac Card_cardinal 1); by (resolve_tac [Card_nat RS (Card_def RS def_imp_iff RS iffD1 RS ssubst)] 1); by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll RSN (2, well_ord_Memrel RS well_ord_lepoll_imp_Card_le)] 1 @@ -49,7 +49,7 @@ goal thy "!!A. [| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \ \ ==> A Un B eqpoll i"; -by (resolve_tac [eqpollI] 1); +by (rtac eqpollI 1); by (eresolve_tac [subset_imp_lepoll RSN (2, eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans)] 2); by (fast_tac AC_cs 2); @@ -70,26 +70,26 @@ goalw thy [lepoll_def] "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] \ \ ==> A Un C lepoll B Un D"; -by (REPEAT (eresolve_tac [exE] 1)); +by (REPEAT (etac exE 1)); by (res_inst_tac [("x","lam a: A Un C. if(a:A, f`a, fa`a)")] exI 1); by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(fa)`z)")] lam_injective 1); by (split_tac [expand_if] 1); -by (eresolve_tac [UnE] 1); +by (etac UnE 1); by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] addSIs [UnI2]) 1); by (REPEAT (split_tac [expand_if] 1)); -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (fast_tac (AC_cs addSEs [left_inverse, inj_is_fun RS apply_type] addEs [swap]) 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [UnE] 1); +by (rtac impI 1); +by (etac UnE 1); by (contr_tac 1); -by (resolve_tac [conjI] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [equals0D] 1); +by (rtac conjI 1); +by (rtac impI 1); +by (etac equals0D 1); by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); by (fast_tac (AC_cs addSEs [left_inverse]) 1); val Un_lepoll_Un = result(); @@ -123,7 +123,7 @@ goal thy "!!A. [| A lepoll i; B lepoll i; ~Finite(i); Ord(i) |] \ \ ==> A Un B lepoll i"; by (res_inst_tac [("A1","i"), ("C1","i")] (ex_eqpoll_disjoint RS exE) 1); -by (eresolve_tac [conjE] 1); +by (etac conjE 1); by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans)] 1); by (assume_tac 1); by (resolve_tac [Un_lepoll_Un RS lepoll_trans] 1 THEN (REPEAT (assume_tac 1))); @@ -134,10 +134,10 @@ goal thy "!!P. [| P(i); i:j; Ord(j) |] ==> (LEAST i. P(i)) : j"; by (eresolve_tac [Least_le RS leE] 1); -by (eresolve_tac [Ord_in_Ord] 1 THEN (assume_tac 1)); -by (eresolve_tac [ltE] 1); +by (etac Ord_in_Ord 1 THEN (assume_tac 1)); +by (etac ltE 1); by (fast_tac (AC_cs addDs [OrdmemD]) 1); -by (eresolve_tac [subst_elem] 1 THEN (assume_tac 1)); +by (etac subst_elem 1 THEN (assume_tac 1)); val Least_in_Ord = result(); goal thy "!!x. [| well_ord(x,r); y<=x; y lepoll succ(n); n:nat |] \ @@ -145,7 +145,7 @@ by (res_inst_tac [("Q","y=0")] (excluded_middle RS disjE) 1); by (fast_tac (AC_cs addSIs [Diff_sing_lepoll, the_first_in]) 1); by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1); -by (resolve_tac [empty_lepollI] 2); +by (rtac empty_lepollI 2); by (fast_tac (AC_cs addSIs [equalityI]) 1); val Diff_first_lepoll = result(); @@ -162,24 +162,24 @@ goal thy "!!a T. [| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==> \ \ ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a"; -by (eresolve_tac [nat_induct] 1); -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); +by (etac nat_induct 1); +by (rtac allI 1); +by (rtac impI 1); by (res_inst_tac [("b","UN b:a. f`b")] subst 1); -by (resolve_tac [empty_lepollI] 2); +by (rtac empty_lepollI 2); by (resolve_tac [equals0I RS sym] 1); by (REPEAT (eresolve_tac [UN_E, allE] 1)); by (fast_tac (AC_cs addDs [lepoll_0_is_0 RS subst]) 1); -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); +by (rtac allI 1); +by (rtac impI 1); by (eres_inst_tac [("x","lam x:a. f`x - {THE b. first(b,f`x,R)}")] allE 1); -by (eresolve_tac [impE] 1); +by (etac impE 1); by (asm_full_simp_tac AC_ss 1); by (fast_tac (AC_cs addSIs [Diff_first_lepoll]) 1); by (asm_full_simp_tac AC_ss 1); by (resolve_tac [UN_subset_split RS subset_imp_lepoll RS lepoll_trans] 1); -by (resolve_tac [Un_lepoll_Inf_Ord] 1 THEN (REPEAT_FIRST assume_tac)); -by (eresolve_tac [UN_sing_lepoll] 1); +by (rtac Un_lepoll_Inf_Ord 1 THEN (REPEAT_FIRST assume_tac)); +by (etac UN_sing_lepoll 1); val UN_fun_lepoll_lemma = result(); goal thy "!!a f. [| ALL b:a. f`b lepoll n & f`b <= T; well_ord(T, R); \ @@ -190,7 +190,7 @@ goal thy "!!a f. [| ALL b:a. F(b) lepoll n & F(b) <= T; well_ord(T, R); \ \ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. F(b)) lepoll a"; -by (resolve_tac [impE] 1 THEN (assume_tac 3)); +by (rtac impE 1 THEN (assume_tac 3)); by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2 THEN (TRYALL assume_tac)); by (simp_tac AC_ss 2); @@ -198,16 +198,16 @@ val UN_lepoll = result(); goal thy "!!a. Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))"; -by (resolve_tac [equalityI] 1); +by (rtac equalityI 1); by (fast_tac AC_cs 2); -by (resolve_tac [subsetI] 1); -by (eresolve_tac [UN_E] 1); -by (resolve_tac [UN_I] 1); +by (rtac subsetI 1); +by (etac UN_E 1); +by (rtac UN_I 1); by (res_inst_tac [("P","%z. x:F(z)")] Least_in_Ord 1 THEN (REPEAT (assume_tac 1))); -by (resolve_tac [DiffI] 1); +by (rtac DiffI 1); by (resolve_tac [Ord_in_Ord RSN (2, LeastI)] 1 THEN (REPEAT (assume_tac 1))); -by (resolve_tac [notI] 1); -by (eresolve_tac [UN_E] 1); +by (rtac notI 1); +by (etac UN_E 1); by (eres_inst_tac [("P","%z. x:F(z)"),("i","c")] less_LeastE 1); by (eresolve_tac [Ord_Least RSN (2, ltI)] 1); val UN_eq_UN_Diffs = result(); @@ -216,7 +216,7 @@ 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 (fast_tac (AC_cs addSIs [if_type, InlI, InrI]) 1); -by (TRYALL (eresolve_tac [sumE])); +by (TRYALL (etac sumE )); by (TRYALL (split_tac [expand_if])); by (TRYALL (asm_simp_tac sum_ss)); by (fast_tac (AC_cs addDs [equals0D]) 1); @@ -224,7 +224,7 @@ goalw thy [lepoll_def, eqpoll_def] "!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; -by (eresolve_tac [exE] 1); +by (etac exE 1); by (forward_tac [subset_refl RSN (2, restrict_bij)] 1); by (res_inst_tac [("x","f``a")] exI 1); by (fast_tac (AC_cs addSEs [inj_is_fun RS fun_is_rel RS image_subset]) 1); @@ -235,7 +235,7 @@ (* ********************************************************************** *) goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; -by (resolve_tac [eqpoll_trans] 1); +by (rtac eqpoll_trans 1); by (eresolve_tac [nat_implies_well_ord RS ( nat_implies_well_ord RSN (2, well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1 @@ -253,17 +253,17 @@ by (forw_inst_tac [("A2","b")] ([Ord_ordertype, Ord_ordertype] MRS Ord_linear) 1 THEN REPEAT (assume_tac 1)); -by (eresolve_tac [disjE] 1); -by (eresolve_tac [ltI] 1); -by (eresolve_tac [Ord_ordertype] 1); -by (eresolve_tac [disjE] 1); +by (etac disjE 1); +by (etac ltI 1); +by (etac Ord_ordertype 1); +by (etac disjE 1); by (REPEAT (eresolve_tac [conjE,notE] 1)); by (resolve_tac [exI RS (eqpoll_def RS (def_imp_iff RS iffD2))] 1); by (eresolve_tac [ordermap_bij RS comp_bij] 1); -by (eresolve_tac [ssubst] 1); +by (etac ssubst 1); by (eresolve_tac [ordermap_bij RS bij_converse_bij] 1); by (REPEAT (eresolve_tac [conjE,notE] 1)); -by (eresolve_tac [eqpollI] 1); +by (etac eqpollI 1); by (resolve_tac [Ord_ordertype RSN (2, OrdmemD RS subset_imp_lepoll) RSN (2, eqpoll_ordertype RS eqpoll_imp_lepoll RS ( eqpoll_ordertype RS eqpoll_sym RS eqpoll_imp_lepoll RSN (3, @@ -306,9 +306,9 @@ val le_in_nat = result(); goalw thy [Finite_def] "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; -by (REPEAT (eresolve_tac [bexE] 1)); -by (REPEAT (dresolve_tac [eqpoll_imp_lepoll] 1)); -by (dresolve_tac [sum_lepoll_mono] 1 THEN (assume_tac 1)); +by (REPEAT (etac bexE 1)); +by (REPEAT (dtac eqpoll_imp_lepoll 1)); +by (dtac sum_lepoll_mono 1 THEN (assume_tac 1)); by (dresolve_tac [nat_sum_eqpoll_sum RS eqpoll_imp_lepoll RSN (2, Un_lepoll_sum RS lepoll_trans RS lepoll_trans)] 1 THEN (REPEAT (assume_tac 1))); @@ -339,7 +339,7 @@ THEN (assume_tac 1)); by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper2_le))) 1 THEN (assume_tac 1)); -by (dresolve_tac [Un_least_lt] 1 THEN (assume_tac 1)); +by (dtac Un_least_lt 1 THEN (assume_tac 1)); by (dresolve_tac [le_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)] 1 THEN (assume_tac 1)); @@ -363,8 +363,8 @@ goal thy "!!A. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a |] \ \ ==> A - B eqpoll a"; -by (resolve_tac [swap] 1 THEN (fast_tac AC_cs 1)); -by (resolve_tac [Diff_lesspoll_eqpoll_Card_lemma] 1 THEN (REPEAT (assume_tac 1))); +by (rtac swap 1 THEN (fast_tac AC_cs 1)); +by (rtac Diff_lesspoll_eqpoll_Card_lemma 1 THEN (REPEAT (assume_tac 1))); by (fast_tac (AC_cs addSIs [lesspoll_def RS def_imp_iff RS iffD2, subset_imp_lepoll RS (eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1); val Diff_lesspoll_eqpoll_Card = result(); diff -r 30df104ceb91 -r 3f460842e919 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Fri Jul 28 11:48:55 1995 +0200 +++ b/src/ZF/AC/DC.ML Fri Jul 28 12:01:12 1995 +0200 @@ -1,6 +1,6 @@ (* Title: ZF/AC/DC.ML ID: $Id$ - Author: Krzysztof Gr`abczewski + Author: Krzysztof Grabczewski The proofs concerning the Axiom of Dependent Choice *) @@ -43,13 +43,13 @@ \ (UN n:nat. {f:n->X. ALL k:n. : R}). \ \ domain(snd(z))=succ(domain(fst(z))) \ \ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; -by (eresolve_tac [ballE] 1); +by (etac ballE 1); by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2); by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1); -by (eresolve_tac [bexE] 1); +by (etac bexE 1); by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); -by (resolve_tac [CollectI] 1); -by (resolve_tac [SigmaI] 1); +by (rtac CollectI 1); +by (rtac SigmaI 1); by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, empty_fun]) 1); by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type] addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, @@ -67,25 +67,25 @@ \ (UN n:nat. {f:n->X. ALL k:n. : R}). \ \ domain(snd(z))=succ(domain(fst(z))) \ \ & restrict(snd(z), domain(fst(z))) = fst(z)})"; -by (resolve_tac [range_subset_domain] 1); -by (resolve_tac [subsetI] 2); -by (eresolve_tac [CollectD1] 2); -by (eresolve_tac [UN_E] 1); -by (eresolve_tac [CollectE] 1); +by (rtac range_subset_domain 1); +by (rtac subsetI 2); +by (etac CollectD1 2); +by (etac UN_E 1); +by (etac CollectE 1); by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1 THEN (assume_tac 1)); by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 THEN REPEAT (assume_tac 1)); -by (eresolve_tac [bexE] 1); +by (etac bexE 1); by (res_inst_tac [("x","cons(, g)")] exI 1); -by (resolve_tac [CollectI] 1); -by (resolve_tac [SigmaI] 1); +by (rtac CollectI 1); +by (rtac SigmaI 1); by (fast_tac AC_cs 1); -by (resolve_tac [UN_I] 1); -by (eresolve_tac [nat_succI] 1); -by (resolve_tac [CollectI] 1); -by (eresolve_tac [cons_fun_type2] 1 THEN (assume_tac 1)); +by (rtac UN_I 1); +by (etac nat_succI 1); +by (rtac CollectI 1); +by (etac cons_fun_type2 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [succE] addss (AC_ss addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1); by (asm_full_simp_tac (AC_ss @@ -104,14 +104,14 @@ \ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \ \ XX = (UN n:nat. {f:n->X. ALL k:n. : R}); f:k->X \ \ |] ==> g:succ(k)->X"; -by (eresolve_tac [CollectE] 1); -by (dresolve_tac [SigmaD2] 1); +by (etac CollectE 1); +by (dtac SigmaD2 1); by (hyp_subst_tac 1); -by (eresolve_tac [UN_E] 1); -by (eresolve_tac [CollectE] 1); +by (etac UN_E 1); +by (etac CollectE 1); by (asm_full_simp_tac AC_ss 1); -by (dresolve_tac [domain_of_fun] 1); -by (eresolve_tac [conjE] 1); +by (dtac domain_of_fun 1); +by (etac conjE 1); by (forward_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); by (fast_tac AC_cs 1); val lemma2_1 = result(); @@ -123,24 +123,24 @@ \ f: nat -> XX; n:nat \ \ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \ \ & : R"; -by (eresolve_tac [nat_induct] 1); +by (etac nat_induct 1); by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); by (dresolve_tac [nat_0I RSN (2, bspec)] 1); by (asm_full_simp_tac AC_ss 1); -by (eresolve_tac [UN_E] 1); -by (eresolve_tac [CollectE] 1); -by (resolve_tac [bexI] 1 THEN (assume_tac 2)); +by (etac UN_E 1); +by (etac CollectE 1); +by (rtac bexI 1 THEN (assume_tac 2)); by (fast_tac (AC_cs addSEs [nat_0_le RS leE, ltD, ltD RSN (2, bspec)] addEs [sym RS trans RS succ_neq_0, domain_of_fun]) 1); -by (eresolve_tac [bexE] 1); +by (etac bexE 1); by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); -by (eresolve_tac [conjE] 1); -by (dresolve_tac [lemma2_1] 1 THEN REPEAT (assume_tac 1)); +by (etac conjE 1); +by (dtac lemma2_1 1 THEN REPEAT (assume_tac 1)); by (hyp_subst_tac 1); by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 THEN (assume_tac 1)); -by (eresolve_tac [UN_E] 1); -by (eresolve_tac [CollectE] 1); +by (etac UN_E 1); +by (etac CollectE 1); by (dresolve_tac [[domain_of_fun RS sym, domain_of_fun] MRS trans] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [nat_succI, nat_into_Ord RS succ_in_succ] @@ -153,21 +153,21 @@ \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ \ f: nat -> XX; n:nat \ \ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x"; -by (eresolve_tac [nat_induct] 1); +by (etac nat_induct 1); by (fast_tac AC_cs 1); -by (resolve_tac [ballI] 1); -by (eresolve_tac [succE] 1); -by (resolve_tac [restrict_eq_imp_val_eq] 1); +by (rtac ballI 1); +by (etac succE 1); +by (rtac restrict_eq_imp_val_eq 1); by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); by (asm_full_simp_tac AC_ss 1); -by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1)); +by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); by (fast_tac (AC_cs addSDs [domain_of_fun]) 1); by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); by (eresolve_tac [sym RS trans RS sym] 1); by (resolve_tac [restrict_eq_imp_val_eq RS sym] 1); by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); by (asm_full_simp_tac AC_ss 1); -by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1)); +by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); by (fast_tac (FOL_cs addSDs [domain_of_fun] addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); val lemma3_1 = result(); @@ -183,7 +183,7 @@ \ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ \ f: nat -> XX; n:nat \ \ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n"; -by (eresolve_tac [natE] 1); +by (etac natE 1); by (asm_full_simp_tac (AC_ss addsimps [image_0]) 1); by (resolve_tac [image_lam RS ssubst] 1); by (fast_tac (AC_cs addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1); @@ -197,7 +197,7 @@ val lemma3 = result(); goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C"; -by (resolve_tac [Pi_type] 1 THEN (assume_tac 1)); +by (rtac Pi_type 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [apply_type]) 1); val fun_type_gen = result(); @@ -206,11 +206,11 @@ by (REPEAT (eresolve_tac [conjE, allE] 1)); by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 THEN (assume_tac 1)); -by (eresolve_tac [bexE] 1); +by (etac bexE 1); by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1); by (fast_tac (AC_cs addSIs [lam_type] addSDs [refl RS lemma2] addSEs [fun_type_gen, apply_type]) 2); -by (resolve_tac [oallI] 1); +by (rtac oallI 1); by (forward_tac [ltD RSN (3, refl RS lemma2)] 1 THEN assume_tac 2); by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); @@ -257,29 +257,29 @@ val lesspoll_nat_is_Finite = result(); goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; -by (eresolve_tac [nat_induct] 1); -by (resolve_tac [allI] 1); +by (etac nat_induct 1); +by (rtac allI 1); by (fast_tac (AC_cs addSIs [Fin.emptyI] addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); -by (eresolve_tac [conjE] 1); +by (rtac allI 1); +by (rtac impI 1); +by (etac conjE 1); by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1)); by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); -by (eresolve_tac [allE] 1); -by (eresolve_tac [impE] 1); +by (etac allE 1); +by (etac impE 1); by (fast_tac AC_cs 1); -by (dresolve_tac [subsetD] 1 THEN (assume_tac 1)); +by (dtac subsetD 1 THEN (assume_tac 1)); by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); by (asm_full_simp_tac (AC_ss addsimps [cons_Diff]) 1); val Finite_Fin_lemma = result(); goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)"; -by (eresolve_tac [bexE] 1); -by (dresolve_tac [Finite_Fin_lemma] 1); -by (eresolve_tac [allE] 1); -by (eresolve_tac [impE] 1); +by (etac bexE 1); +by (dtac Finite_Fin_lemma 1); +by (etac allE 1); +by (etac impE 1); by (assume_tac 2); by (fast_tac AC_cs 1); val Finite_Fin = result(); @@ -301,11 +301,11 @@ \ range(R) <= domain(R); x:domain(R) \ \ |] ==> RR <= Pow(XX)*XX & \ \ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. :RR))"; -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE] addSIs [subsetI, SigmaI]) 1); -by (resolve_tac [ballI] 1); -by (resolve_tac [impI] 1); +by (rtac ballI 1); +by (rtac impI 1); by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 THEN (assume_tac 1)); by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \ @@ -343,7 +343,7 @@ \ {f:succ(n)->domain(R). ALL k:n. : R}); \ \ u=k; n:nat \ \ |] ==> f`n : succ(k) -> domain(R)"; -by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); +by (dtac apply_type 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); val f_n_type = result(); @@ -351,11 +351,11 @@ \ {f:succ(n)->domain(R). ALL k:n. : R}); \ \ domain(f`n) = succ(k); n:nat \ \ |] ==> ALL i:k. : R"; -by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); -by (eresolve_tac [UN_E] 1); -by (eresolve_tac [CollectE] 1); +by (dtac apply_type 1 THEN (assume_tac 1)); +by (etac UN_E 1); +by (etac CollectE 1); by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); -by (dresolve_tac [succ_eqD] 1); +by (dtac succ_eqD 1); by (asm_full_simp_tac AC_ss 1); val f_n_pairs_in_R = result(); @@ -363,7 +363,7 @@ "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ \ |] ==> restrict(cons(, f), domain(x)) = x"; by (eresolve_tac [sym RS trans RS sym] 1); -by (resolve_tac [fun_extension] 1); +by (rtac fun_extension 1); by (fast_tac (AC_cs addSIs [lam_type]) 1); by (fast_tac (AC_cs addSIs [lam_type]) 1); by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); @@ -375,12 +375,12 @@ \ n:nat; domain(f`n) = succ(n); \ \ (UN x:f``n. domain(x)) <= n |] \ \ ==> ALL x:f``succ(n). restrict(cons(, f`n), domain(x))=x"; -by (resolve_tac [ballI] 1); +by (rtac ballI 1); by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); -by (dresolve_tac [f_n_type] 1 THEN REPEAT (ares_tac [refl] 1)); -by (eresolve_tac [consE] 1); +by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); +by (etac consE 1); by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); -by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (dtac bspec 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); val all_in_image_restrict_eq = result(); @@ -396,9 +396,9 @@ \ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ \ & (UN f:fst(z). domain(f)) = b \ \ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; -by (resolve_tac [oallI] 1); -by (dresolve_tac [ltD] 1); -by (eresolve_tac [nat_induct] 1); +by (rtac oallI 1); +by (dtac ltD 1); +by (etac nat_induct 1); by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); by (fast_tac (FOL_cs addss (ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun, @@ -408,29 +408,29 @@ by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); by (fast_tac (FOL_cs addSEs [trans, subst_context] addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); -by (eresolve_tac [conjE] 1); -by (eresolve_tac [notE] 1); +by (etac conjE 1); +by (etac notE 1); by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); -by (eresolve_tac [conjE] 1); -by (dresolve_tac [apply_UN_type] 1 THEN REPEAT (assume_tac 1)); -by (eresolve_tac [domainE] 1); -by (eresolve_tac [domainE] 1); +by (etac conjE 1); +by (dtac apply_UN_type 1 THEN REPEAT (assume_tac 1)); +by (etac domainE 1); +by (etac domainE 1); by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); by (res_inst_tac [("x","cons(, f`xa)")] bexI 1); by (fast_tac (FOL_cs addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); -by (resolve_tac [UN_I] 1); -by (eresolve_tac [nat_succI] 1); -by (resolve_tac [CollectI] 1); +by (rtac UN_I 1); +by (etac nat_succI 1); +by (rtac CollectI 1); by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1 THEN REPEAT (assume_tac 1)); -by (resolve_tac [ballI] 1); -by (eresolve_tac [succE] 1); +by (rtac ballI 1); +by (etac succE 1); by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 THEN REPEAT (assume_tac 1)); -by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (dtac bspec 1 THEN (assume_tac 1)); by (asm_full_simp_tac (AC_ss addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); val simplify_recursion = result(); @@ -444,11 +444,11 @@ \ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ \ |] ==> f`n : succ(n) -> domain(R) \ \ & (ALL i:n. :R)"; -by (dresolve_tac [ospec] 1); +by (dtac ospec 1); by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); -by (eresolve_tac [CollectE] 1); +by (etac CollectE 1); by (asm_full_simp_tac AC_ss 1); -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (fast_tac (AC_cs addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); by (fast_tac (FOL_cs @@ -468,8 +468,8 @@ by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 THEN (assume_tac 1)); by (asm_full_simp_tac AC_ss 1); -by (REPEAT (eresolve_tac [conjE] 1)); -by (eresolve_tac [ballE] 1); +by (REPEAT (etac conjE 1)); +by (etac ballE 1); by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); by (fast_tac (AC_cs addSEs [ssubst]) 1); by (asm_full_simp_tac (AC_ss @@ -481,14 +481,14 @@ by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 THEN REPEAT (assume_tac 1)); -by (eresolve_tac [bexE] 1); +by (etac bexE 1); by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 THEN REPEAT (assume_tac 1)); by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1); -by (resolve_tac [lam_type] 2); +by (rtac lam_type 2); by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2 THEN REPEAT (assume_tac 2)); -by (resolve_tac [ballI] 1); +by (rtac ballI 1); by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1 THEN REPEAT (assume_tac 1)); by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1)); @@ -522,19 +522,19 @@ goalw thy [DC_def, WO3_def] "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; -by (resolve_tac [allI] 1); +by (rtac allI 1); by (excluded_middle_tac "A lesspoll Hartog(A)" 1); by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); by (REPEAT (eresolve_tac [allE, impE] 1)); -by (resolve_tac [Card_Hartog] 1); +by (rtac Card_Hartog 1); by (eres_inst_tac [("x","A")] allE 1); by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ \ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); by (asm_full_simp_tac AC_ss 1); -by (eresolve_tac [impE] 1); +by (etac impE 1); by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); -by (eresolve_tac [bexE] 1); +by (etac bexE 1); by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) RS (HartogI RS notE)] 1); by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); @@ -551,10 +551,10 @@ goal thy "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; -by (resolve_tac [images_eq] 1); +by (rtac images_eq 1); by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] addSIs [lam_type]) 2)); -by (resolve_tac [ballI] 1); +by (rtac ballI 1); by (dresolve_tac [OrdmemD RS subsetD] 1 THEN REPEAT (assume_tac 1)); by (asm_full_simp_tac AC_ss 1); @@ -582,13 +582,13 @@ by (res_inst_tac [("P","b:K")] impE 1 THEN TRYALL assume_tac); by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1 THEN REPEAT (assume_tac 1)); -by (resolve_tac [impI] 1); +by (rtac impI 1); by (resolve_tac [ff_def RS def_transrec RS ssubst] 1); -by (eresolve_tac [the_first_in] 1); +by (etac the_first_in 1); by (fast_tac AC_cs 1); by (asm_full_simp_tac (AC_ss addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1); -by (eresolve_tac [lemma_] 1 THEN (assume_tac 1)); +by (etac lemma_ 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [RepFunE, impE, notE] addEs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1); by (fast_tac (AC_cs addSEs [[in_Card_imp_lesspoll, RepFun_lepoll] @@ -600,7 +600,7 @@ by (REPEAT (resolve_tac [allI,impI] 1)); by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1); -by (resolve_tac [lam_type] 2); +by (rtac lam_type 2); by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2)); by (asm_full_simp_tac (AC_ss addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1); diff -r 30df104ceb91 -r 3f460842e919 src/ZF/AC/DC_lemmas.ML --- a/src/ZF/AC/DC_lemmas.ML Fri Jul 28 11:48:55 1995 +0200 +++ b/src/ZF/AC/DC_lemmas.ML Fri Jul 28 12:01:12 1995 +0200 @@ -1,6 +1,6 @@ (* Title: ZF/AC/DC_lemmas.ML ID: $Id$ - Author: Krzysztof Gr`abczewski + Author: Krzysztof Grabczewski More general lemmas used in the proofs concerning DC @@ -15,11 +15,11 @@ val RepFun_lepoll = result(); goalw thy [lesspoll_def] "!!n. n:nat ==> n lesspoll nat"; -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (eresolve_tac [Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll] 1); -by (resolve_tac [notI] 1); -by (eresolve_tac [eqpollE] 1); -by (resolve_tac [succ_lepoll_natE] 1 THEN (assume_tac 2)); +by (rtac notI 1); +by (etac eqpollE 1); +by (rtac succ_lepoll_natE 1 THEN (assume_tac 2)); by (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll) RS lepoll_trans] 1 THEN (assume_tac 1)); @@ -44,8 +44,8 @@ val [major, minor] = goal thy "[| (!!g. g:X ==> EX u. :R); R<=X*X \ \ |] ==> range(R) <= domain(R)"; -by (resolve_tac [subsetI] 1); -by (eresolve_tac [rangeE] 1); +by (rtac subsetI 1); +by (etac rangeE 1); by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1); by (fast_tac AC_cs 1); val range_subset_domain = result(); @@ -64,11 +64,11 @@ goal thy "!!g. g:n->X ==> cons(, g) : succ(n) -> cons(x, X)"; by (resolve_tac [Pi_iff_old RS iffD2] 1); -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (fast_tac (AC_cs addSIs [cons_subset, succI1] addEs [fun_is_rel RS subset_trans RS subsetD, succI2]) 1); -by (resolve_tac [ballI] 1); -by (eresolve_tac [succE] 1); +by (rtac ballI 1); +by (etac succE 1); by (fast_tac (AC_cs addDs [domain_of_fun, domainI] addSEs [mem_irrefl]) 1); by (fast_tac (AC_cs addDs [fun_unique_Pair] addSEs [mem_irrefl]) 1); val cons_fun_type = result(); @@ -103,10 +103,10 @@ val domain_cons_eq_succ = result(); goalw thy [restrict_def] "!!g. g:n->X ==> restrict(cons(, g), n)=g"; -by (resolve_tac [fun_extension] 1); -by (resolve_tac [lam_type] 1); +by (rtac fun_extension 1); +by (rtac lam_type 1); by (eresolve_tac [cons_fun_type RS apply_type] 1); -by (eresolve_tac [succI2] 1); +by (etac succI2 1); by (assume_tac 1); by (asm_full_simp_tac (AC_ss addsimps [cons_val_k]) 1); val restrict_cons_eq = result(); @@ -120,13 +120,13 @@ goalw thy [restrict_def] "!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; -by (eresolve_tac [subst] 1); +by (etac subst 1); by (asm_full_simp_tac AC_ss 1); val restrict_eq_imp_val_eq = result(); goal thy "!!a. succ(a) = succ(b) ==> a = b"; -by (eresolve_tac [equalityE] 1); -by (resolve_tac [equalityI] 1); +by (etac equalityE 1); +by (rtac equalityI 1); by (fast_tac (AC_cs addSEs [mem_irrefl] addEs [mem_asym]) 1); by (fast_tac (AC_cs addSEs [mem_irrefl] addEs [mem_asym]) 1); val succ_eqD = result(); diff -r 30df104ceb91 -r 3f460842e919 src/ZF/AC/HH.ML --- a/src/ZF/AC/HH.ML Fri Jul 28 11:48:55 1995 +0200 +++ b/src/ZF/AC/HH.ML Fri Jul 28 12:01:12 1995 +0200 @@ -1,6 +1,6 @@ (* Title: ZF/AC/HH.ML ID: $Id$ - Author: Krzysztof Gr`abczewski + Author: Krzysztof Grabczewski Some properties of the recursive definition of HH used in the proofs of AC17 ==> AC1 @@ -33,7 +33,7 @@ val subset_imp_Diff_eq = result(); goal thy "!!c. [| c:a-b; b c=b | b HH(f,x,a) = HH(f,x,a1)"; by (resolve_tac [HH_def_satisfies_eq RS (HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1); -by (eresolve_tac [subst_context] 1); +by (etac subst_context 1); val HH_eq = result(); goal thy "!!a. [| HH(f,x,b)={x}; b HH(f,x,a)={x}"; by (res_inst_tac [("P","b HH(f,x,b) : Pow(x)-{0}"; by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); -by (dresolve_tac [HH_is_x_gt_too] 1 THEN (assume_tac 1)); -by (dresolve_tac [subst] 1 THEN (assume_tac 1)); +by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1)); +by (dtac subst 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); val HH_subset_x_lt_too = result(); @@ -85,7 +85,7 @@ goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P"; by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1)); by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1); -by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1)); +by (dtac subst_elem 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSIs [singleton_iff RS iffD2, equals0I]) 1); val HH_eq_arg_lt = result(); @@ -94,7 +94,7 @@ by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac); by (resolve_tac [sym RS (ltD RSN (3, HH_eq_arg_lt))] 2 THEN REPEAT (assume_tac 2)); -by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1)); +by (dtac subst_elem 1 THEN (assume_tac 1)); by (fast_tac (FOL_cs addDs [ltD] addSEs [HH_eq_arg_lt]) 1); val HH_eq_imp_arg_eq = result(); @@ -118,7 +118,7 @@ goal thy "!!a. a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}"; by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); -by (resolve_tac [less_LeastE] 1); +by (rtac less_LeastE 1); by (eresolve_tac [Ord_Least RSN (2, ltI)] 2); by (assume_tac 1); val less_Least_subset_x = result(); @@ -152,15 +152,15 @@ \ ALL a:A. EX z:x. F(a) = {z} |] \ \ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})"; by (asm_full_simp_tac (AC_ss addsimps [Diff_eq_0_iff]) 1); -by (resolve_tac [conjI] 1); +by (rtac conjI 1); by (fast_tac (AC_cs addSIs [lam_type] addSEs [RepFun_eqI]) 1); -by (resolve_tac [ballI] 1); -by (eresolve_tac [RepFunE] 1); -by (dresolve_tac [subsetD] 1 THEN (assume_tac 1)); -by (eresolve_tac [UN_E] 1); -by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); -by (eresolve_tac [bexE] 1); -by (resolve_tac [bexI] 1 THEN (assume_tac 2)); +by (rtac ballI 1); +by (etac RepFunE 1); +by (dtac subsetD 1 THEN (assume_tac 1)); +by (etac UN_E 1); +by (dtac bspec 1 THEN (assume_tac 1)); +by (etac bexE 1); +by (rtac bexI 1 THEN (assume_tac 2)); by (forward_tac [elem_of_sing_eq] 1 THEN (assume_tac 1)); by (fast_tac AC_cs 1); val lam_surj_sing = result(); @@ -203,9 +203,9 @@ goal thy "!!f. [| f : (PROD X:Pow(x)-{0}. {{z}. z:x}); \ \ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}"; -by (dresolve_tac [less_Least_subset_x] 1); +by (dtac less_Least_subset_x 1); by (forward_tac [HH_subset_imp_eq] 1); -by (dresolve_tac [apply_type] 1); +by (dtac apply_type 1); by (resolve_tac [Diff_subset RS PowI RS DiffI] 1); by (fast_tac (AC_cs addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); by (fast_tac (AC_cs addSEs [RepFunE] addEs [ssubst]) 1);