src/HOL/Transcendental.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58410 6d46ad54a2ab
     1.1 --- a/src/HOL/Transcendental.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -481,10 +481,10 @@
     1.4    apply (rule setsum.cong [OF refl])
     1.5    apply (simp add: less_iff_Suc_add)
     1.6    apply (clarify)
     1.7 -  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
     1.8 +  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
     1.9                del: setsum_lessThan_Suc power_Suc)
    1.10    apply (subst mult.assoc [symmetric], subst power_add [symmetric])
    1.11 -  apply (simp add: mult_ac)
    1.12 +  apply (simp add: ac_simps)
    1.13    done
    1.14  
    1.15  lemma real_setsum_nat_ivl_bounded2:
    1.16 @@ -958,7 +958,7 @@
    1.17      hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
    1.18        by (rule order_trans [OF norm_mult_ineq])
    1.19      hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
    1.20 -      by (simp add: pos_divide_le_eq mult_ac)
    1.21 +      by (simp add: pos_divide_le_eq ac_simps)
    1.22      thus "norm (S (Suc n)) \<le> r * norm (S n)"
    1.23        by (simp add: S_Suc inverse_eq_divide)
    1.24    qed
    1.25 @@ -1058,7 +1058,7 @@
    1.26      by (rule distrib_right)
    1.27    also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
    1.28                  + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
    1.29 -    by (simp only: setsum_right_distrib mult_ac)
    1.30 +    by (simp only: setsum_right_distrib ac_simps)
    1.31    also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
    1.32                  + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.33      by (simp add: times_S Suc_diff_le)
    1.34 @@ -1431,7 +1431,7 @@
    1.35        by (rule mult_mono)
    1.36          (rule mult_mono, simp_all add: power_le_one a b)
    1.37      hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
    1.38 -      unfolding power_add by (simp add: mult_ac del: fact_Suc) }
    1.39 +      unfolding power_add by (simp add: ac_simps del: fact_Suc) }
    1.40    note aux1 = this
    1.41    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
    1.42      by (intro sums_mult geometric_sums, simp)
    1.43 @@ -2476,7 +2476,7 @@
    1.44  proof -
    1.45    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
    1.46      by (rule sin_converges [THEN sums_group], simp)
    1.47 -  thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
    1.48 +  thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: ac_simps)
    1.49  qed
    1.50  
    1.51  lemma sin_gt_zero:
    1.52 @@ -2512,7 +2512,7 @@
    1.53  proof -
    1.54    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
    1.55      by (rule cos_converges [THEN sums_group], simp)
    1.56 -  thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
    1.57 +  thus ?thesis unfolding cos_coeff_def by (simp add: ac_simps)
    1.58  qed
    1.59  
    1.60  lemmas realpow_num_eq_if = power_eq_if
    1.61 @@ -2533,7 +2533,7 @@
    1.62  apply (drule sums_summable)
    1.63  apply simp
    1.64  apply (erule suminf_pos)
    1.65 -apply (simp add: add_ac)
    1.66 +apply (simp add: ac_simps)
    1.67  done
    1.68  
    1.69  lemma cos_two_less_zero [simp]: