Tidying: removing redundant args in classical reasoner calls
authorpaulson
Wed Aug 21 11:43:37 1996 +0200 (1996-08-21)
changeset 1932cc9f1ba8f29a
parent 1931 c77409a88b75
child 1933 8b24773de6db
Tidying: removing redundant args in classical reasoner calls
src/ZF/AC/AC10_AC15.ML
src/ZF/AC/AC16_WO4.ML
src/ZF/AC/AC2_AC6.ML
src/ZF/AC/Cardinal_aux.ML
src/ZF/AC/DC.ML
src/ZF/AC/WO1_WO6.ML
src/ZF/AC/WO1_WO8.ML
src/ZF/AC/WO2_AC16.ML
     1.1 --- a/src/ZF/AC/AC10_AC15.ML	Wed Aug 21 11:00:04 1996 +0200
     1.2 +++ b/src/ZF/AC/AC10_AC15.ML	Wed Aug 21 11:43:37 1996 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4  by (asm_full_simp_tac (AC_ss addsimps
     1.5                  [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
     1.6                  singletonI RS not_emptyI]) 1);
     1.7 -by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1);
     1.8 +by (fast_tac (AC_cs addSEs [apply_type]) 1);
     1.9  qed "AC1_AC13";
    1.10  
    1.11  (* ********************************************************************** *)
     2.1 --- a/src/ZF/AC/AC16_WO4.ML	Wed Aug 21 11:00:04 1996 +0200
     2.2 +++ b/src/ZF/AC/AC16_WO4.ML	Wed Aug 21 11:43:37 1996 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4  by (fast_tac (AC_cs addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun,
     2.5          equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
     2.6          nat_1_lepoll_iff RS iffD2]
     2.7 -        addSEs [singletonE, apply_type, ltE]) 1);
     2.8 +        addSEs [apply_type, ltE]) 1);
     2.9  val lemma1 = result();
    2.10  
    2.11  (* ********************************************************************** *)
     3.1 --- a/src/ZF/AC/AC2_AC6.ML	Wed Aug 21 11:00:04 1996 +0200
     3.2 +++ b/src/ZF/AC/AC2_AC6.ML	Wed Aug 21 11:43:37 1996 +0200
     3.3 @@ -16,7 +16,7 @@
     3.4  
     3.5  goal thy "!!B. [| B:A; f:(PROD X:A. X); 0~:A |]  \
     3.6  \               ==> {f`B} <= B Int {f`C. C:A}";
     3.7 -by (fast_tac (AC_cs addSEs [singletonE, apply_type, RepFunI]) 1);
     3.8 +by (fast_tac (ZF_cs addSEs [apply_type]) 1);
     3.9  val lemma1 = result();
    3.10  
    3.11  goalw thy [pairwise_disjoint_def]
    3.12 @@ -143,7 +143,7 @@
    3.13  by (rtac apply_equality 1 THEN (assume_tac 2));
    3.14  by (etac domainE 1);
    3.15  by (forward_tac [range_type] 1 THEN (assume_tac 1));
    3.16 -by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1);
    3.17 +by (fast_tac (ZF_cs addDs [apply_equality]) 1);
    3.18  qed "AC4_AC5";
    3.19  
    3.20  
    3.21 @@ -157,9 +157,9 @@
    3.22  
    3.23  goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
    3.24  by (rtac equalityI 1);
    3.25 -by (fast_tac (AC_cs addSEs [lamE, Pair_inject]
    3.26 +by (fast_tac (AC_cs addSEs [lamE]
    3.27                  addEs [subst_elem]
    3.28 -                addSDs [converseD, Pair_fst_snd_eq]) 1);
    3.29 +                addSDs [Pair_fst_snd_eq]) 1);
    3.30  by (rtac subsetI 1);
    3.31  by (etac domainE 1);
    3.32  by (rtac domainI 1);
     4.1 --- a/src/ZF/AC/Cardinal_aux.ML	Wed Aug 21 11:00:04 1996 +0200
     4.2 +++ b/src/ZF/AC/Cardinal_aux.ML	Wed Aug 21 11:43:37 1996 +0200
     4.3 @@ -76,7 +76,7 @@
     4.4  by (split_tac [expand_if] 1);
     4.5  by (asm_full_simp_tac (ZF_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
     4.6  by (fast_tac (ZF_cs addSIs [the_equality, equalityI, equals0I]
     4.7 -                addEs [equalityE] addSEs [singletonE]) 1);
     4.8 +                addEs [equalityE]) 1);
     4.9  val paired_bij_lemma = result();
    4.10  
    4.11  goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w}))  \
    4.12 @@ -131,7 +131,7 @@
    4.13  by (res_inst_tac [("x","lam z:(UN x:a. {P(x)}). (LEAST i. P(i)=z)")] exI 1);
    4.14  by (res_inst_tac [("d","%z. P(z)")] lam_injective 1);
    4.15  by (fast_tac (AC_cs addSIs [Least_in_Ord]) 1);
    4.16 -by (fast_tac (AC_cs addIs [LeastI] addSEs [singletonE, Ord_in_Ord]) 1);
    4.17 +by (fast_tac (AC_cs addIs [LeastI] addSEs [Ord_in_Ord]) 1);
    4.18  val UN_sing_lepoll = result();
    4.19  
    4.20  goal thy "!!a T. [| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==>  \
     5.1 --- a/src/ZF/AC/DC.ML	Wed Aug 21 11:00:04 1996 +0200
     5.2 +++ b/src/ZF/AC/DC.ML	Wed Aug 21 11:43:37 1996 +0200
     5.3 @@ -302,8 +302,7 @@
     5.4  \       |] ==> RR <= Pow(XX)*XX &  \
     5.5  \       (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))";
     5.6  by (rtac conjI 1);
     5.7 -by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE]
     5.8 -        addSIs [subsetI, SigmaI]) 1);
     5.9 +by (deepen_tac (ZF_cs addSEs [FinD RS PowI]) 0 1);
    5.10  by (rtac ballI 1);
    5.11  by (rtac impI 1);
    5.12  by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1
     6.1 --- a/src/ZF/AC/WO1_WO6.ML	Wed Aug 21 11:00:04 1996 +0200
     6.2 +++ b/src/ZF/AC/WO1_WO6.ML	Wed Aug 21 11:43:37 1996 +0200
     6.3 @@ -33,11 +33,11 @@
     6.4  (* ********************************************************************** *)
     6.5  
     6.6  goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
     6.7 -by (fast_tac (ZF_cs addSIs [lam_type, RepFunI, apply_type]) 1);
     6.8 +by (fast_tac (ZF_cs addSIs [lam_type, apply_type]) 1);
     6.9  val lam_sets = result();
    6.10  
    6.11  goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
    6.12 -by (fast_tac (ZF_cs addSIs [equalityI] addSEs [singletonE, apply_type]) 1);
    6.13 +by (fast_tac (ZF_cs addSIs [equalityI] addSEs [apply_type]) 1);
    6.14  val surj_imp_eq_ = result();
    6.15  
    6.16  goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
     7.1 --- a/src/ZF/AC/WO1_WO8.ML	Wed Aug 21 11:00:04 1996 +0200
     7.2 +++ b/src/ZF/AC/WO1_WO8.ML	Wed Aug 21 11:43:37 1996 +0200
     7.3 @@ -24,7 +24,7 @@
     7.4  by (fast_tac (AC_cs addSEs [lam_sing_bij RS bij_is_inj RS
     7.5                          well_ord_rvimage]) 2);
     7.6  by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
     7.7 -by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym]
     7.8 +by (fast_tac (ZF_cs addSEs [singleton_eq_iff RS iffD1 RS sym]
     7.9                  addSIs [lam_type]
    7.10                  addIs [the_equality RS ssubst]) 1);
    7.11  qed "WO8_WO1";
     8.1 --- a/src/ZF/AC/WO2_AC16.ML	Wed Aug 21 11:00:04 1996 +0200
     8.2 +++ b/src/ZF/AC/WO2_AC16.ML	Wed Aug 21 11:43:37 1996 +0200
     8.3 @@ -380,7 +380,7 @@
     8.4  by (REPEAT (eresolve_tac [allE, impE] 1));
     8.5  by (rtac conjI 1);
     8.6  by (fast_tac AC_cs 2);
     8.7 -by (fast_tac (eq_cs addSEs [singletonE]) 1);
     8.8 +by (fast_tac ZF_cs 1);
     8.9  by (etac Diffs_eq_imp_eq 1
    8.10          THEN REPEAT (assume_tac 1));
    8.11  val subset_imp_eq_lemma = result();