src/HOL/Hyperreal/Transcendental.ML

 Addsimps [real_sqrt_sum_squares_mult_squared_eq];
 
 Goal "sqrt(x ^ 2) = abs(x)";
 by (rtac (abs_realpow_two RS subst) 1);
 by (rtac (real_sqrt_abs_abs RS subst) 1);
-by (rtac (real_pow_sqrt_eq_sqrt_pow RS ssubst) 1);
+by (stac real_pow_sqrt_eq_sqrt_pow 1);
 by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2, abs_mult,abs_ge_zero]));
 qed "real_sqrt_abs";
 Addsimps [real_sqrt_abs];
 
 Goal "sqrt(x*x) = abs(x)";

 Goal "0 < x ==> 0 < sqrt(x) ^ 2";
 by (asm_full_simp_tac (simpset() addsimps [real_sqrt_gt_zero_pow2]) 1); 
 qed "real_sqrt_pow2_gt_zero";
 
 Goal "0 < x ==> sqrt x ~= 0";
-by (forward_tac [real_sqrt_pow2_gt_zero] 1);
+by (ftac real_sqrt_pow2_gt_zero 1);
 by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2, real_less_not_refl]));
 qed "real_sqrt_not_eq_zero";
 
 Goal "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x";
-by (forward_tac [real_sqrt_not_eq_zero] 1);
+by (ftac real_sqrt_not_eq_zero 1);
 by (cut_inst_tac [("n1","2"),("r1","sqrt x")] (realpow_inverse RS sym) 1);
 by (auto_tac (claset() addDs [real_sqrt_gt_zero_pow2],simpset()));
 qed "real_inv_sqrt_pow2";
 
 Goal "[| 0 <= x; sqrt(x) = 0|] ==> x = 0";

 by (res_inst_tac [("N","n"),("c","r")] ratio_test 1);
 by (auto_tac (claset(),simpset() addsimps [abs_mult,real_mult_assoc RS sym]
     delsimps [fact_Suc]));
 by (rtac real_mult_le_le_mono2 1);
 by (res_inst_tac [("w1","abs x")] (real_mult_commute RS ssubst) 2);
-by (rtac (fact_Suc RS ssubst) 2);
-by (rtac (real_of_nat_mult RS ssubst) 2);
+by (stac fact_Suc 2);
+by (stac real_of_nat_mult 2);
 by (auto_tac (claset(),simpset() addsimps [abs_mult,real_inverse_distrib,
     abs_ge_zero]));
 by (auto_tac (claset(), simpset() addsimps 
      [real_mult_assoc RS sym, abs_ge_zero, abs_eqI2,
       real_inverse_gt_0]));

 Goal "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) = \
 \     y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))";
 by (auto_tac (claset(),simpset() addsimps [sumr_mult] delsimps [sumr_Suc]));
 by (rtac sumr_subst 1);
 by (strip_tac 1);
-by (rtac (lemma_realpow_diff RS ssubst) 1);
+by (stac lemma_realpow_diff 1);
 by (auto_tac (claset(),simpset() addsimps real_mult_ac));
 qed "lemma_realpow_diff_sumr";
 
 Goal "x ^ (Suc n) - y ^ (Suc n) = \
 \     (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))";
 by (induct_tac "n" 1);
 by (auto_tac (claset(),simpset() delsimps [sumr_Suc]));
-by (rtac (sumr_Suc RS ssubst) 1);
+by (stac sumr_Suc 1);
 by (dtac sym 1);
 by (auto_tac (claset(),simpset() addsimps [lemma_realpow_diff_sumr,
     real_add_mult_distrib2,real_diff_def] @ 
     real_mult_ac delsimps [sumr_Suc]));
 qed "lemma_realpow_diff_sumr2";

 by (case_tac "x = y" 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_commute,
     realpow_add RS sym] delsimps [sumr_Suc]));
 by (res_inst_tac [("c1","x - y")] (real_mult_left_cancel RS iffD1) 1);
 by (rtac (real_minus_minus RS subst) 2);
-by (rtac (real_minus_mult_eq1 RS ssubst) 2);
+by (stac real_minus_mult_eq1 2);
 by (auto_tac (claset(),simpset() addsimps [lemma_realpow_diff_sumr2 
     RS sym] delsimps [sumr_Suc]));
 qed "lemma_realpow_rev_sumr";
 
 (* ------------------------------------------------------------------------ *)

 qed "lemma_termdiff2";
 
 Goal "[| h ~= 0; abs z <= K; abs (z + h) <= K |] \
 \     ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0)) \
 \         <= real n * real (n - Suc 0) * K ^ (n - 2) * abs h";
-by (rtac (lemma_termdiff2 RS ssubst) 1);
+by (stac lemma_termdiff2 1);
 by (asm_full_simp_tac (simpset() addsimps [abs_mult,real_mult_commute]) 2);
 by (stac real_mult_commute 2); 
 by (rtac (sumr_rabs RS real_le_trans) 2);
 by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 2);
 by (rtac (real_mult_commute RS subst) 2);

 (* ------------------------------------------------------------------------ *)
 
 Goalw [diffs_def]  
       "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))";
 by (rtac ext 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac real_inverse_distrib 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
 qed "exp_fdiffs";
 
 Goalw [diffs_def,real_divide_def]
       "diffs(%n. if even n then 0 \
 \          else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) \
 \      = (%n. if even n then \
 \                (- 1) ^ (n div 2)/(real (fact n)) \
 \             else 0)";
 by (rtac ext 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by Auto_tac;
 qed "sin_fdiffs";
 
 Goalw  [diffs_def,real_divide_def]
        "diffs(%n. if even n then 0 \
 \          else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) n \
 \      = (if even n then \
 \                (- 1) ^ (n div 2)/(real (fact n)) \
 \             else 0)";
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by Auto_tac;
 qed "sin_fdiffs2";
 
 (* thms in EvenOdd needed *)
 Goalw [diffs_def,real_divide_def]
       "diffs(%n. if even n then \
 \                (- 1) ^ (n div 2)/(real (fact n)) else 0) \
 \      = (%n. - (if even n then 0 \
 \          else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))";
 by (rtac ext 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
 by (res_inst_tac [("z1","inverse(real (Suc n))")] 
      (real_mult_commute RS ssubst) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
     odd_not_even RS sym,odd_Suc_mult_two_ex]));

 Goalw [diffs_def,real_divide_def]
       "diffs(%n. if even n then \
 \                (- 1) ^ (n div 2)/(real (fact n)) else 0) n\
 \      = - (if even n then 0 \
 \          else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))";
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (even_Suc RS ssubst) 1);
-by (rtac (real_inverse_distrib RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac even_Suc 1);
+by (stac real_inverse_distrib 1);
 by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
 by (res_inst_tac [("z1","inverse (real (Suc n))")] 
      (real_mult_commute RS ssubst) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
     odd_not_even RS sym,odd_Suc_mult_two_ex]));

 Goal "exp = (%x. suminf (%n. inverse (real (fact n)) * x ^ n))";
 by (auto_tac (claset() addSIs [ext],simpset() addsimps [exp_def]));
 val lemma_exp_ext = result();
 
 Goalw [exp_def] "DERIV exp x :> exp(x)";
-by (rtac (lemma_exp_ext RS ssubst) 1);
+by (stac lemma_exp_ext 1);
 by (subgoal_tac "DERIV (%u. suminf (%n. inverse (real (fact n)) * u ^ n)) x \
 \    :> suminf (%n. diffs (%n. inverse (real (fact n))) n * x ^ n)" 1);
 by (res_inst_tac [("K","1 + abs(x)")] termdiffs 2);
 by (auto_tac (claset() addIs [exp_converges RS sums_summable],
     simpset() addsimps [exp_fdiffs]));

 \          else 0) * x ^ n))";
 by (auto_tac (claset() addSIs [ext],simpset() addsimps [cos_def]));
 val lemma_cos_ext = result();
 
 Goalw [cos_def] "DERIV sin x :> cos(x)";
-by (rtac (lemma_sin_ext RS ssubst) 1);
+by (stac lemma_sin_ext 1);
 by (auto_tac (claset(),simpset() addsimps [sin_fdiffs2 RS sym]));
 by (res_inst_tac [("K","1 + abs(x)")] termdiffs 1);
 by (auto_tac (claset() addIs [sin_converges, cos_converges, sums_summable] 
     addSIs [sums_minus RS sums_summable],
     simpset() addsimps [cos_fdiffs,sin_fdiffs]));
 by (arith_tac 1);
 qed "DERIV_sin";
 Addsimps [DERIV_sin];
 
 Goal "DERIV cos x :> -sin(x)";
-by (rtac (lemma_cos_ext RS ssubst) 1);
+by (stac lemma_cos_ext 1);
 by (auto_tac (claset(),simpset() addsimps [lemma_sin_minus,
     cos_fdiffs2 RS sym,real_minus_mult_eq1]));
 by (res_inst_tac [("K","1 + abs(x)")] termdiffs 1);
 by (auto_tac (claset() addIs [sin_converges,cos_converges, sums_summable] 
     addSIs [sums_minus RS sums_summable],

 Goal "DERIV (%x. exp (-x)) x :> - exp(-x)";
 by (auto_tac (claset(),simpset() addsimps
     [CLAIM_SIMP "(%x. exp(-x)) = exp o (%x. - x)" [ext]]));
 by (rtac (real_mult_1_right RS subst) 1);
 by (rtac (real_minus_mult_eq1 RS subst) 1);
-by (rtac (real_minus_mult_eq2 RS ssubst) 1);
+by (stac real_minus_mult_eq2 1);
 by (rtac DERIV_chain 1);
 by (rtac DERIV_minus 2);
 by Auto_tac;
 qed "DERIV_exp_minus";
 Addsimps [DERIV_exp_minus];

     addsimps real_mult_ac) 1);
 qed "exp_add";
 
 Goal "0 <= exp x";
 by (res_inst_tac [("t","x")] (real_sum_of_halves RS subst) 1);
-by (rtac (exp_add RS ssubst) 1 THEN Auto_tac);
+by (stac exp_add 1 THEN Auto_tac);
 qed "exp_ge_zero";
 Addsimps [exp_ge_zero];
 
 Goal "exp x ~= 0";
 by (cut_inst_tac [("x","x")] exp_mult_minus2 1);

 by (auto_tac (claset(), simpset() addsimps [numeral_2_eq_2])); 
 qed "sin_cos_squared_add";
 Addsimps [sin_cos_squared_add];
 
 Goal "(cos(x) ^ 2) + (sin(x) ^ 2) = 1";
-by (rtac (real_add_commute RS ssubst) 1);
+by (stac real_add_commute 1);
 by (simp_tac (simpset() delsimps [realpow_Suc]) 1);
 qed "sin_cos_squared_add2";
 Addsimps [sin_cos_squared_add2];
 
 Goal "cos x * cos x + sin x * sin x = 1";

     (CLAIM "[|(0::real)<z; z*x<z*y |] ==> x<y") 1);
 by (asm_simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym, real_mult_assoc RS sym]) 2);
 by (stac (CLAIM "6 = 2 * (3::real)") 2);
 by (rtac real_mult_less_mono 2);  
 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc]));
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac fact_Suc 1);
+by (stac fact_Suc 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
 by (simp_tac (simpset() addsimps [real_divide_def,
     real_inverse_distrib] delsimps [fact_Suc]) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym] 
     delsimps [fact_Suc]));
 by (multr_by_tac "real (Suc (Suc (4*m)))" 1);

 by (rtac real_mult_inverse_cancel2 1);
 by (TRYALL(rtac (real_of_nat_fact_gt_zero)));
 by (simp_tac (simpset() addsimps [real_mult_assoc RS sym] 
     delsimps [fact_Suc]) 1);
 by (rtac ((CLAIM "real(n::nat) * 4 = real(4 * n)") RS ssubst) 1);
-by (rtac (fact_Suc RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
-by (rtac (real_of_nat_mult RS ssubst) 1);
+by (stac fact_Suc 1);
+by (stac real_of_nat_mult 1);
+by (stac real_of_nat_mult 1);
 by (rtac real_mult_less_mono 1);
 by (Force_tac 1);
 by (Force_tac 2);
 by (rtac real_of_nat_fact_gt_zero 2);
 by (rtac (real_of_nat_less_iff RS iffD2) 1);

     cos_gt_zero_pi]));
 by Auto_tac;
 qed "cos_ge_zero";
 
 Goal "[| 0 < x; x < pi  |] ==> 0 < sin x";
-by (rtac (sin_cos_eq RS ssubst) 1);
+by (stac sin_cos_eq 1);
 by (rotate_tac 1 1);
 by (dtac (real_sum_of_halves RS ssubst) 1);
 by (auto_tac (claset() addSIs [cos_gt_zero_pi],
     simpset() delsimps [sin_cos_eq RS sym]));
 qed "sin_gt_zero_pi";

 qed "cos_2npi";
 Addsimps [cos_2npi];
 
 Goal "cos (3 / 2 * pi) = 0";
 by (rtac (CLAIM "(1::real) + 1/2 = 3/2" RS subst) 1);
-by (rtac (real_add_mult_distrib RS ssubst) 1);
+by (stac real_add_mult_distrib 1);
 by (auto_tac (claset(),simpset() addsimps [cos_add] @ real_mult_ac));
 qed "cos_3over2_pi";
 Addsimps [cos_3over2_pi];
 
 Goal "sin (2 * real (n::nat) * pi) = 0";

 qed "sin_2npi";
 Addsimps [sin_2npi];
 
 Goal "sin (3 / 2 * pi) = - 1";
 by (rtac (CLAIM "(1::real) + 1/2 = 3/2" RS subst) 1);
-by (rtac (real_add_mult_distrib RS ssubst) 1);
+by (stac real_add_mult_distrib 1);
 by (auto_tac (claset(),simpset() addsimps [sin_add] @real_mult_ac));
 qed "sin_3over2_pi";
 Addsimps [sin_3over2_pi];
 
 Goal "cos(xa + 1 / 2 * real (Suc m) * pi) = \