author paulson Wed Mar 18 14:13:27 2015 +0000 (2015-03-18) changeset 59741 5b762cd73a8e parent 59734 f41a2f77ab1b child 59742 1441ca50f047
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
 src/HOL/Complex.thy file | annotate | diff | revisions src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | revisions src/HOL/NthRoot.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/Probability/Lebesgue_Measure.thy file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions src/HOL/Real_Vector_Spaces.thy file | annotate | diff | revisions src/HOL/Series.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     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
```