Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
authorpaulson <lp15@cam.ac.uk>
Wed Mar 18 14:13:27 2015 +0000 (2015-03-18)
changeset 597415b762cd73a8e
parent 59734 f41a2f77ab1b
child 59742 1441ca50f047
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/NthRoot.thy
src/HOL/Power.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/ROOT
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Complex.thy	Tue Mar 17 17:45:03 2015 +0000
     1.2 +++ b/src/HOL/Complex.thy	Wed Mar 18 14:13:27 2015 +0000
     1.3 @@ -215,6 +215,18 @@
     1.4  lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
     1.5    by (metis mult.commute power2_i power_mult)
     1.6  
     1.7 +lemma Re_ii_times [simp]: "Re (ii*z) = - Im z"
     1.8 +  by simp
     1.9 +
    1.10 +lemma Im_ii_times [simp]: "Im (ii*z) = Re z"
    1.11 +  by simp
    1.12 +
    1.13 +lemma ii_times_eq_iff: "ii*w = z \<longleftrightarrow> w = -(ii*z)"
    1.14 +  by auto
    1.15 +
    1.16 +lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
    1.17 +  by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
    1.18 +
    1.19  subsection {* Vector Norm *}
    1.20  
    1.21  instantiation complex :: real_normed_field
    1.22 @@ -309,6 +321,9 @@
    1.23    apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
    1.24    done
    1.25  
    1.26 +lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
    1.27 +  by (simp add: norm_complex_def divide_simps complex_eq_iff)
    1.28 +
    1.29  
    1.30  text {* Properties of complex signum. *}
    1.31  
    1.32 @@ -508,10 +523,10 @@
    1.33     (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
    1.34           simp del: of_real_power)
    1.35  
    1.36 -lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
    1.37 +lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
    1.38    by (auto simp add: Re_divide)
    1.39  
    1.40 -lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
    1.41 +lemma Im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
    1.42    by (auto simp add: Im_divide)
    1.43  
    1.44  lemma complex_div_gt_0:
    1.45 @@ -526,27 +541,27 @@
    1.46      by (simp add: Re_divide Im_divide zero_less_divide_iff)
    1.47  qed
    1.48  
    1.49 -lemma re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
    1.50 -  and im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
    1.51 +lemma Re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
    1.52 +  and Im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
    1.53    using complex_div_gt_0 by auto
    1.54  
    1.55 -lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
    1.56 -  by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
    1.57 +lemma Re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
    1.58 +  by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)
    1.59  
    1.60 -lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
    1.61 -  by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
    1.62 +lemma Im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
    1.63 +  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)
    1.64  
    1.65 -lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
    1.66 -  by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
    1.67 +lemma Re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
    1.68 +  by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)
    1.69  
    1.70 -lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
    1.71 -  by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
    1.72 +lemma Im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
    1.73 +  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)
    1.74  
    1.75 -lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
    1.76 -  by (metis not_le re_complex_div_gt_0)
    1.77 +lemma Re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
    1.78 +  by (metis not_le Re_complex_div_gt_0)
    1.79  
    1.80 -lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
    1.81 -  by (metis im_complex_div_gt_0 not_le)
    1.82 +lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
    1.83 +  by (metis Im_complex_div_gt_0 not_le)
    1.84  
    1.85  lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
    1.86    by (induct s rule: infinite_finite_induct) auto
    1.87 @@ -807,7 +822,7 @@
    1.88  lemma csqrt_ii [simp]: "csqrt \<i> = (1 + \<i>) / sqrt 2"
    1.89    by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)
    1.90  
    1.91 -lemma power2_csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
    1.92 +lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
    1.93  proof cases
    1.94    assume "Im z = 0" then show ?thesis
    1.95      using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 17 17:45:03 2015 +0000
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 18 14:13:27 2015 +0000
     2.3 @@ -1718,8 +1718,10 @@
     2.4            by (auto simp: real_power_down_fl intro!: power_down_le)
     2.5        next
     2.6          case True
     2.7 -        have "power_down_fl prec (Float 1 (- 2))  ?num \<le> real (Float 1 (- 2)) ^ ?num"
     2.8 -          by (auto simp: real_power_down_fl power_down)
     2.9 +        have "power_down_fl prec (Float 1 (- 2))  ?num \<le> (Float 1 (- 2)) ^ ?num"
    2.10 +          by (metis Float_le_zero_iff less_imp_le linorder_not_less not_numeral_le_zero numeral_One power_down_fl)
    2.11 +        then have "power_down_fl prec (Float 1 (- 2))  ?num \<le> real (Float 1 (- 2)) ^ ?num"
    2.12 +          by simp
    2.13          also
    2.14          have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
    2.15          from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
    2.16 @@ -1727,7 +1729,7 @@
    2.17          from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
    2.18          have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
    2.19          hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
    2.20 -          by (auto intro!: power_mono)
    2.21 +          by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
    2.22          also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
    2.23          finally show ?thesis
    2.24            unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_P[OF True] real_of_float_power
     3.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 17 17:45:03 2015 +0000
     3.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Mar 18 14:13:27 2015 +0000
     3.3 @@ -8,8 +8,6 @@
     3.4  imports Complex_Main
     3.5  begin
     3.6  
     3.7 -lemmas fact_Suc = fact.simps(2)
     3.8 -
     3.9  subsection {* The type of formal power series*}
    3.10  
    3.11  typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
    3.12 @@ -594,7 +592,7 @@
    3.13        fix n :: nat
    3.14        assume nn0: "n \<ge> n0"
    3.15        then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
    3.16 -        by (auto intro: power_decreasing)
    3.17 +        by (simp add: divide_simps)
    3.18        {
    3.19          assume "?s n = a"
    3.20          then have "dist (?s n) a < r"
    3.21 @@ -612,9 +610,9 @@
    3.22            by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff
    3.23                split: split_if_asm intro: LeastI2_ex)
    3.24          then have "dist (?s n) a < (1/2)^n"
    3.25 -          unfolding dth by (auto intro: power_strict_decreasing)
    3.26 +          unfolding dth by (simp add: divide_simps)
    3.27          also have "\<dots> \<le> (1/2)^n0"
    3.28 -          using nn0 by (auto intro: power_decreasing)
    3.29 +          using nn0 by (simp add: divide_simps)
    3.30          also have "\<dots> < r"
    3.31            using n0 by simp
    3.32          finally have "dist (?s n) a < r" .
     4.1 --- a/src/HOL/NthRoot.thy	Tue Mar 17 17:45:03 2015 +0000
     4.2 +++ b/src/HOL/NthRoot.thy	Wed Mar 18 14:13:27 2015 +0000
     4.3 @@ -626,19 +626,24 @@
     4.4  apply (simp add: zero_less_divide_iff)
     4.5  done
     4.6  
     4.7 +lemma sqrt2_less_2: "sqrt 2 < (2::real)"
     4.8 +  by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
     4.9 +
    4.10 +
    4.11  text{*Needed for the infinitely close relation over the nonstandard
    4.12      complex numbers*}
    4.13  lemma lemma_sqrt_hcomplex_capprox:
    4.14       "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<^sup>2 + y\<^sup>2) < u"
    4.15 -apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
    4.16 -apply (erule_tac [2] lemma_real_divide_sqrt_less)
    4.17 -apply (rule power2_le_imp_le)
    4.18 -apply (auto simp add: zero_le_divide_iff power_divide)
    4.19 -apply (rule_tac t = "u\<^sup>2" in real_sum_of_halves [THEN subst])
    4.20 -apply (rule add_mono)
    4.21 -apply (auto simp add: four_x_squared intro: power_mono)
    4.22 -done
    4.23 -
    4.24 +  apply (rule real_sqrt_sum_squares_less)
    4.25 +  apply (auto simp add: abs_if field_simps)
    4.26 +  apply (rule le_less_trans [where y = "x*2"])
    4.27 +  using less_eq_real_def sqrt2_less_2 apply force
    4.28 +  apply assumption
    4.29 +  apply (rule le_less_trans [where y = "y*2"])
    4.30 +  using less_eq_real_def sqrt2_less_2 mult_le_cancel_left 
    4.31 +  apply auto 
    4.32 +  done
    4.33 +  
    4.34  text "Legacy theorem names:"
    4.35  lemmas real_root_pos2 = real_root_power_cancel
    4.36  lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
     5.1 --- a/src/HOL/Power.thy	Tue Mar 17 17:45:03 2015 +0000
     5.2 +++ b/src/HOL/Power.thy	Wed Mar 18 14:13:27 2015 +0000
     5.3 @@ -51,6 +51,10 @@
     5.4    "a ^ 1 = a"
     5.5    by simp
     5.6  
     5.7 +lemma power_Suc0_right [simp]:
     5.8 +  "a ^ Suc 0 = a"
     5.9 +  by simp
    5.10 +
    5.11  lemma power_commutes:
    5.12    "a ^ n * a = a * a ^ n"
    5.13    by (induct n) (simp_all add: mult.assoc)
    5.14 @@ -127,6 +131,9 @@
    5.15  
    5.16  end
    5.17  
    5.18 +declare power_mult_distrib [where a = "numeral w" for w, simp]
    5.19 +declare power_mult_distrib [where b = "numeral w" for w, simp]
    5.20 +
    5.21  context semiring_numeral
    5.22  begin
    5.23  
    5.24 @@ -301,6 +308,8 @@
    5.25    "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
    5.26    by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
    5.27  
    5.28 +declare nonzero_power_divide [where b = "numeral w" for w, simp]
    5.29 +
    5.30  end
    5.31  
    5.32  
     6.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 17 17:45:03 2015 +0000
     6.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 18 14:13:27 2015 +0000
     6.3 @@ -502,13 +502,26 @@
     6.4  end
     6.5  
     6.6  lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
     6.7 -  unfolding UN_box_eq_UNIV[symmetric]
     6.8 -  apply (subst SUP_emeasure_incseq[symmetric])
     6.9 -  apply (auto simp: incseq_def subset_box inner_add_left setprod_constant intro!: SUP_PInfty)
    6.10 -  apply (rule_tac x="Suc n" in exI)
    6.11 -  apply (rule order_trans[OF _ self_le_power])
    6.12 -  apply (auto simp: card_gt_0_iff real_of_nat_Suc)
    6.13 -  done
    6.14 +proof -
    6.15 +  { fix n::nat
    6.16 +    let ?Ba = "Basis :: 'a set"
    6.17 +    have "real n \<le> (2::real) ^ card ?Ba * real n"
    6.18 +      by (simp add: mult_le_cancel_right1)
    6.19 +    also 
    6.20 +    have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba"
    6.21 +      apply (rule mult_left_mono)
    6.22 +      apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le real_of_nat_le_iff real_of_nat_power self_le_power zero_less_Suc)
    6.23 +      apply (simp add: DIM_positive)
    6.24 +      done
    6.25 +    finally have "real n \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" .
    6.26 +  } note [intro!] = this
    6.27 +  show ?thesis
    6.28 +    unfolding UN_box_eq_UNIV[symmetric]
    6.29 +    apply (subst SUP_emeasure_incseq[symmetric])
    6.30 +    apply (auto simp: incseq_def subset_box inner_add_left setprod_constant 
    6.31 +               intro!: SUP_PInfty)
    6.32 +    done 
    6.33 +qed
    6.34  
    6.35  lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
    6.36    using emeasure_lborel_cbox[of x x] nonempty_Basis
     7.1 --- a/src/HOL/ROOT	Tue Mar 17 17:45:03 2015 +0000
     7.2 +++ b/src/HOL/ROOT	Wed Mar 18 14:13:27 2015 +0000
     7.3 @@ -688,6 +688,7 @@
     7.4      Determinants
     7.5      PolyRoots
     7.6      Complex_Analysis_Basics
     7.7 +    Complex_Transcendental
     7.8    document_files
     7.9      "root.tex"
    7.10  
     8.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 17 17:45:03 2015 +0000
     8.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Mar 18 14:13:27 2015 +0000
     8.3 @@ -444,7 +444,8 @@
     8.4    then show thesis ..
     8.5  qed
     8.6  
     8.7 -lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
     8.8 +lemma setsum_in_Reals [intro,simp]:
     8.9 +  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
    8.10  proof (cases "finite s")
    8.11    case True then show ?thesis using assms
    8.12      by (induct s rule: finite_induct) auto
    8.13 @@ -453,7 +454,8 @@
    8.14      by (metis Reals_0 setsum.infinite)
    8.15  qed
    8.16  
    8.17 -lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
    8.18 +lemma setprod_in_Reals [intro,simp]: 
    8.19 +  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
    8.20  proof (cases "finite s")
    8.21    case True then show ?thesis using assms
    8.22      by (induct s rule: finite_induct) auto
     9.1 --- a/src/HOL/Series.thy	Tue Mar 17 17:45:03 2015 +0000
     9.2 +++ b/src/HOL/Series.thy	Wed Mar 18 14:13:27 2015 +0000
     9.3 @@ -434,7 +434,7 @@
     9.4    have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
     9.5      by auto
     9.6    have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
     9.7 -    by simp
     9.8 +    by (simp add: mult.commute)
     9.9    thus ?thesis using sums_divide [OF 2, of 2]
    9.10      by simp
    9.11  qed
    10.1 --- a/src/HOL/Transcendental.thy	Tue Mar 17 17:45:03 2015 +0000
    10.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 18 14:13:27 2015 +0000
    10.3 @@ -1512,6 +1512,10 @@
    10.4    using exp_bound [of "1/2"]
    10.5    by (simp add: field_simps)
    10.6  
    10.7 +corollary exp_le: "exp 1 \<le> (3::real)"
    10.8 +  using exp_bound [of 1]
    10.9 +  by (simp add: field_simps)
   10.10 +
   10.11  lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
   10.12    by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
   10.13  
   10.14 @@ -3071,6 +3075,84 @@
   10.15  lemma sin_two_pi [simp]: "sin (2*pi) = 0"
   10.16    by (simp add: sin_double)
   10.17  
   10.18 +
   10.19 +lemma sin_times_sin:
   10.20 +  fixes w :: "'a::{real_normed_field,banach}"
   10.21 +  shows "sin(w) * sin(z) = (cos(w - z) - cos(w + z)) / 2"
   10.22 +  by (simp add: cos_diff cos_add)
   10.23 +
   10.24 +lemma sin_times_cos:
   10.25 +  fixes w :: "'a::{real_normed_field,banach}"
   10.26 +  shows "sin(w) * cos(z) = (sin(w + z) + sin(w - z)) / 2"
   10.27 +  by (simp add: sin_diff sin_add)
   10.28 +
   10.29 +lemma cos_times_sin:
   10.30 +  fixes w :: "'a::{real_normed_field,banach}"
   10.31 +  shows "cos(w) * sin(z) = (sin(w + z) - sin(w - z)) / 2"
   10.32 +  by (simp add: sin_diff sin_add)
   10.33 +
   10.34 +lemma cos_times_cos:
   10.35 +  fixes w :: "'a::{real_normed_field,banach}"
   10.36 +  shows "cos(w) * cos(z) = (cos(w - z) + cos(w + z)) / 2"
   10.37 +  by (simp add: cos_diff cos_add)
   10.38 +
   10.39 +lemma sin_plus_sin:  (*FIXME field_inverse_zero should not be necessary*)
   10.40 +  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   10.41 +  shows "sin(w) + sin(z) = 2 * sin((w + z) / 2) * cos((w - z) / 2)"
   10.42 +  apply (simp add: mult.assoc sin_times_cos)
   10.43 +  apply (simp add: field_simps)
   10.44 +  done
   10.45 +
   10.46 +lemma sin_diff_sin: 
   10.47 +  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   10.48 +  shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)"
   10.49 +  apply (simp add: mult.assoc sin_times_cos)
   10.50 +  apply (simp add: field_simps)
   10.51 +  done
   10.52 +
   10.53 +lemma cos_plus_cos: 
   10.54 +  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   10.55 +  shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)"
   10.56 +  apply (simp add: mult.assoc cos_times_cos)
   10.57 +  apply (simp add: field_simps)
   10.58 +  done
   10.59 +
   10.60 +lemma cos_diff_cos: 
   10.61 +  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
   10.62 +  shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)"
   10.63 +  apply (simp add: mult.assoc sin_times_sin)
   10.64 +  apply (simp add: field_simps)
   10.65 +  done
   10.66 +
   10.67 +lemma cos_double_cos: 
   10.68 +  fixes z :: "'a::{real_normed_field,banach}"
   10.69 +  shows "cos(2 * z) = 2 * cos z ^ 2 - 1"
   10.70 +by (simp add: cos_double sin_squared_eq)
   10.71 +
   10.72 +lemma cos_double_sin: 
   10.73 +  fixes z :: "'a::{real_normed_field,banach}"
   10.74 +  shows "cos(2 * z) = 1 - 2 * sin z ^ 2"
   10.75 +by (simp add: cos_double sin_squared_eq)
   10.76 +
   10.77 +lemma sin_pi_minus [simp]: "sin (pi - x) = sin x"
   10.78 +  by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff)
   10.79 +
   10.80 +lemma cos_pi_minus [simp]: "cos (pi - x) = -(cos x)"
   10.81 +  by (metis cos_minus cos_periodic_pi uminus_add_conv_diff)
   10.82 +
   10.83 +lemma sin_minus_pi [simp]: "sin (x - pi) = - (sin x)"
   10.84 +  by (simp add: sin_diff)
   10.85 +
   10.86 +lemma cos_minus_pi [simp]: "cos (x - pi) = -(cos x)"
   10.87 +  by (simp add: cos_diff)
   10.88 +
   10.89 +lemma sin_2pi_minus [simp]: "sin (2*pi - x) = -(sin x)"
   10.90 +  by (metis sin_periodic_pi2 add_diff_eq mult_2 sin_pi_minus)
   10.91 +
   10.92 +lemma cos_2pi_minus [simp]: "cos (2*pi - x) = cos x"
   10.93 +  by (metis (no_types, hide_lams) cos_add cos_minus cos_two_pi sin_minus sin_two_pi 
   10.94 +           diff_0_right minus_diff_eq mult_1 mult_zero_left uminus_add_conv_diff)
   10.95 +
   10.96  lemma sin_gt_zero2: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < sin x"
   10.97    by (metis sin_gt_zero_02 order_less_trans pi_half_less_two)
   10.98