src/HOL/Transcendental.thy
changeset 49962 a8cc904a6820
parent 47489 04e7d09ade7a
child 50326 b5afeccab2db
     1.1 --- a/src/HOL/Transcendental.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  apply (simp del: setsum_op_ivl_Suc)
     1.5  apply (subst setsum_op_ivl_Suc)
     1.6  apply (subst lemma_realpow_diff_sumr)
     1.7 -apply (simp add: right_distrib del: setsum_op_ivl_Suc)
     1.8 +apply (simp add: distrib_left del: setsum_op_ivl_Suc)
     1.9  apply (subst mult_left_commute [of "x - y"])
    1.10  apply (erule subst)
    1.11  apply (simp add: algebra_simps)
    1.12 @@ -922,7 +922,7 @@
    1.13      by (simp only: Suc)
    1.14    also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
    1.15                  + y * (\<Sum>i=0..n. S x i * S y (n-i))"
    1.16 -    by (rule left_distrib)
    1.17 +    by (rule distrib_right)
    1.18    also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
    1.19                  + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
    1.20      by (simp only: setsum_right_distrib mult_ac)
    1.21 @@ -1001,7 +1001,7 @@
    1.22  
    1.23  lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
    1.24  apply (induct "n")
    1.25 -apply (auto simp add: real_of_nat_Suc right_distrib exp_add mult_commute)
    1.26 +apply (auto simp add: real_of_nat_Suc distrib_left exp_add mult_commute)
    1.27  done
    1.28  
    1.29  text {* Strict monotonicity of exponential. *}
    1.30 @@ -1626,7 +1626,7 @@
    1.31  
    1.32  lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
    1.33  apply (induct "n")
    1.34 -apply (auto simp add: real_of_nat_Suc left_distrib)
    1.35 +apply (auto simp add: real_of_nat_Suc distrib_right)
    1.36  done
    1.37  
    1.38  lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
    1.39 @@ -1638,7 +1638,7 @@
    1.40  
    1.41  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
    1.42  apply (induct "n")
    1.43 -apply (auto simp add: real_of_nat_Suc left_distrib)
    1.44 +apply (auto simp add: real_of_nat_Suc distrib_right)
    1.45  done
    1.46  
    1.47  lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
    1.48 @@ -1784,7 +1784,7 @@
    1.49        \<exists>n::nat. even n & x = real n * (pi/2)"
    1.50  apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
    1.51   apply (clarify, rule_tac x = "n - 1" in exI)
    1.52 - apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
    1.53 + apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
    1.54  apply (rule cos_zero_lemma)
    1.55  apply (simp_all add: cos_add)
    1.56  done
    1.57 @@ -1799,7 +1799,7 @@
    1.58  apply (drule cos_zero_lemma, assumption+)
    1.59  apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
    1.60  apply (force simp add: minus_equation_iff [of x])
    1.61 -apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
    1.62 +apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
    1.63  apply (auto simp add: cos_add)
    1.64  done
    1.65  
    1.66 @@ -2029,7 +2029,7 @@
    1.67  lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x"
    1.68  proof (induct n arbitrary: x)
    1.69    case (Suc n)
    1.70 -  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
    1.71 +  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
    1.72    show ?case unfolding split_pi_off using Suc by auto
    1.73  qed auto
    1.74  
    1.75 @@ -2212,7 +2212,7 @@
    1.76    show "0 \<le> cos (arctan x)"
    1.77      by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
    1.78    have "(cos (arctan x))\<twosuperior> * (1 + (tan (arctan x))\<twosuperior>) = 1"
    1.79 -    unfolding tan_def by (simp add: right_distrib power_divide)
    1.80 +    unfolding tan_def by (simp add: distrib_left power_divide)
    1.81    thus "(cos (arctan x))\<twosuperior> = (1 / sqrt (1 + x\<twosuperior>))\<twosuperior>"
    1.82      using `0 < 1 + x\<twosuperior>` by (simp add: power_divide eq_divide_eq)
    1.83  qed
    1.84 @@ -2226,7 +2226,7 @@
    1.85  apply (rule power_inverse [THEN subst])
    1.86  apply (rule_tac c1 = "(cos x)\<twosuperior>" in real_mult_right_cancel [THEN iffD1])
    1.87  apply (auto dest: field_power_not_zero
    1.88 -        simp add: power_mult_distrib left_distrib power_divide tan_def
    1.89 +        simp add: power_mult_distrib distrib_right power_divide tan_def
    1.90                    mult_assoc power_inverse [symmetric])
    1.91  done
    1.92  
    1.93 @@ -2397,7 +2397,7 @@
    1.94    have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
    1.95      by (auto simp add: algebra_simps sin_add)
    1.96    thus ?thesis
    1.97 -    by (simp add: real_of_nat_Suc left_distrib add_divide_distrib
    1.98 +    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
    1.99                    mult_commute [of pi])
   1.100  qed
   1.101  
   1.102 @@ -2418,7 +2418,7 @@
   1.103  done
   1.104  
   1.105  lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
   1.106 -by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
   1.107 +by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
   1.108  
   1.109  lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
   1.110    by (auto intro!: DERIV_intros)