src/HOL/Complex/CLim.ML
changeset 14373 67a628beb981
parent 14365 3d4df8c166ae
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Complex/CLim.ML	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/CLim.ML	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -284,7 +284,7 @@
     1.4  (*** NSCLIM_zero, CLIM_zero, etc. ***)
     1.5  
     1.6  Goal "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0";
     1.7 -by (res_inst_tac [("z1","l")] (complex_add_minus_right_zero RS subst) 1);
     1.8 +by (res_inst_tac [("a1","l")] (right_minus RS subst) 1);
     1.9  by (rewtac complex_diff_def);
    1.10  by (rtac NSCLIM_add 1 THEN Auto_tac);
    1.11  qed "NSCLIM_zero";
    1.12 @@ -701,7 +701,7 @@
    1.13  by (Step_tac 1);
    1.14  by (dres_inst_tac [("x","x - a")] spec 1);
    1.15  by (dres_inst_tac [("x","x + a")] spec 2);
    1.16 -by (auto_tac (claset(), simpset() addsimps complex_add_ac));
    1.17 +by (auto_tac (claset(), simpset() addsimps add_ac));
    1.18  qed "CDERIV_CLIM_iff";
    1.19  
    1.20  Goalw [cderiv_def] "(CDERIV f x :> D) = \
    1.21 @@ -755,10 +755,10 @@
    1.22      [mem_cinfmal_iff RS sym,hcomplex_add_commute]));
    1.23  by (dres_inst_tac [("c","xa + - hcomplex_of_complex x")] capprox_mult1 1);
    1.24  by (auto_tac (claset() addIs [CInfinitesimal_subset_CFinite
    1.25 -    RS subsetD],simpset() addsimps [hcomplex_mult_assoc]));
    1.26 +    RS subsetD],simpset() addsimps [mult_assoc]));
    1.27  by (dres_inst_tac [("x3","D")] (CFinite_hcomplex_of_complex RSN
    1.28      (2,CInfinitesimal_CFinite_mult) RS (mem_cinfmal_iff RS iffD1)) 1);
    1.29 -by (blast_tac (claset() addIs [capprox_trans,hcomplex_mult_commute RS subst,
    1.30 +by (blast_tac (claset() addIs [capprox_trans,mult_commute RS subst,
    1.31      (capprox_minus_iff RS iffD2)]) 1);
    1.32  qed "NSCDERIV_isNSContc";
    1.33  
    1.34 @@ -833,10 +833,9 @@
    1.35  by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1);
    1.36  by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4);
    1.37  by (auto_tac (claset() addSIs [capprox_add_mono1],
    1.38 -      simpset() addsimps [hcomplex_add_mult_distrib, right_distrib, 
    1.39 -			  hcomplex_mult_commute, hcomplex_add_assoc]));
    1.40 -by (res_inst_tac [("w1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")]
    1.41 -    (hcomplex_add_commute RS subst) 1);
    1.42 +     simpset() addsimps [left_distrib, right_distrib, mult_commute, add_assoc]));
    1.43 +by (res_inst_tac [("b1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")]
    1.44 +    (add_commute RS subst) 1);
    1.45  by (auto_tac (claset() addSIs [CInfinitesimal_add_capprox_self2 RS capprox_sym,
    1.46  			       CInfinitesimal_add, CInfinitesimal_mult,
    1.47  			       CInfinitesimal_hcomplex_of_complex_mult,
    1.48 @@ -853,7 +852,7 @@
    1.49  Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D";
    1.50  by (asm_full_simp_tac 
    1.51      (simpset() addsimps [times_divide_eq_right RS sym, NSCDERIV_NSCLIM_iff,
    1.52 -                         minus_mult_right, complex_add_mult_distrib2 RS sym,
    1.53 +                         minus_mult_right, right_distrib RS sym,
    1.54                           complex_diff_def] 
    1.55               delsimps [times_divide_eq_right, minus_mult_right RS sym]) 1);
    1.56  by (etac (NSCLIM_const RS NSCLIM_mult) 1);
    1.57 @@ -866,9 +865,8 @@
    1.58  
    1.59  Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D";
    1.60  by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,complex_diff_def]) 1);
    1.61 -by (res_inst_tac [("t","f x")] (complex_minus_minus RS subst) 1);
    1.62 -by (asm_simp_tac (simpset() addsimps [complex_minus_add_distrib RS sym] 
    1.63 -                   delsimps [complex_minus_add_distrib, complex_minus_minus]
    1.64 +by (res_inst_tac [("t","f x")] (minus_minus RS subst) 1);
    1.65 +by (asm_simp_tac (simpset() addsimps [minus_add_distrib RS sym] 
    1.66                     delsimps [minus_add_distrib, minus_minus]
    1.67  
    1.68  ) 1);
    1.69 @@ -1032,12 +1030,12 @@
    1.70  by (dtac (CDERIV_Id RS CDERIV_mult) 2);
    1.71  by (auto_tac (claset(), 
    1.72                simpset() addsimps [complex_of_real_add RS sym,
    1.73 -                        complex_add_mult_distrib,real_of_nat_Suc] 
    1.74 +                        left_distrib,real_of_nat_Suc] 
    1.75                   delsimps [complex_of_real_add]));
    1.76  by (case_tac "n" 1);
    1.77  by (auto_tac (claset(), 
    1.78 -              simpset() addsimps [complex_mult_assoc, complex_add_commute]));
    1.79 -by (auto_tac (claset(),simpset() addsimps [complex_mult_commute]));
    1.80 +              simpset() addsimps [mult_assoc, add_commute]));
    1.81 +by (auto_tac (claset(),simpset() addsimps [mult_commute]));
    1.82  qed "CDERIV_pow";
    1.83  Addsimps [CDERIV_pow,simplify (simpset()) CDERIV_pow];
    1.84  
    1.85 @@ -1095,10 +1093,9 @@
    1.86  
    1.87  Goal "[| CDERIV f x :> d; f(x) ~= 0 |] \
    1.88  \     ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
    1.89 -by (rtac (complex_mult_commute RS subst) 1);
    1.90 -by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1,
    1.91 -    power_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym,
    1.92 -complex_minus_mult_eq1 RS sym]) 1);
    1.93 +by (rtac (mult_commute RS subst) 1);
    1.94 +by (asm_simp_tac (simpset() addsimps [minus_mult_left,
    1.95 +    power_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym]) 1);
    1.96  by (fold_goals_tac [o_def]);
    1.97  by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1);
    1.98  qed "CDERIV_inverse_fun";
    1.99 @@ -1126,8 +1123,8 @@
   1.100  by (dtac CDERIV_mult 2);
   1.101  by (REPEAT(assume_tac 1));
   1.102  by (asm_full_simp_tac
   1.103 -    (simpset() addsimps [complex_divide_def, complex_add_mult_distrib2,
   1.104 -                         power_inverse,complex_minus_mult_eq1] @ complex_mult_ac 
   1.105 +    (simpset() addsimps [complex_divide_def, right_distrib,
   1.106 +                         power_inverse,minus_mult_left] @ mult_ac 
   1.107         delsimps [complexpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
   1.108  qed "CDERIV_quotient";
   1.109  
   1.110 @@ -1161,7 +1158,7 @@
   1.111  by (Step_tac 1);
   1.112  by (res_inst_tac 
   1.113      [("x","%z. if  z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
   1.114 -by (auto_tac (claset(),simpset() addsimps [complex_mult_assoc,
   1.115 +by (auto_tac (claset(),simpset() addsimps [mult_assoc,
   1.116      CLAIM "z ~= x ==> z - x ~= (0::complex)"]));
   1.117  by (auto_tac (claset(),simpset() addsimps [isContc_iff,CDERIV_iff]));
   1.118  by (ALLGOALS(rtac (CLIM_equal RS iffD1)));