helm/software/matita/contribs/procedural/CoRN/transc/Trigonometric.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: Trigonometric.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
  20
  21 include "transc/TaylorSeries.ma".
  22
  23 (*#* *The Trigonometric Functions
  24
  25 In this section, we explore the properties of the trigonometric functions which we previously defined.
  26 *)
  27
  28 (* UNEXPORTED
  29 Section Lemmas
  30 *)
  31
  32 (*#* First, we need a lemma on mappings. *)
  33
  34 inline procedural "cic:/CoRN/transc/Trigonometric/maps_translation.con" as lemma.
  35
  36 (* UNEXPORTED
  37 End Lemmas
  38 *)
  39
  40 (* UNEXPORTED
  41 Section Sine_and_Cosine
  42 *)
  43
  44 (*#* Sine, cosine and tangent at [Zero]. *)
  45
  46 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_zero.con" as lemma.
  47
  48 inline procedural "cic:/CoRN/transc/Trigonometric/Cos_zero.con" as lemma.
  49
  50 (* UNEXPORTED
  51 Hint Resolve Sin_zero Cos_zero: algebra.
  52 *)
  53
  54 (* UNEXPORTED
  55 Opaque Sine Cosine.
  56 *)
  57
  58 inline procedural "cic:/CoRN/transc/Trigonometric/Tan_zero.con" as lemma.
  59
  60 (* UNEXPORTED
  61 Transparent Sine Cosine.
  62 *)
  63
  64 (*#*
  65 Continuity of sine and cosine are trivial.
  66 *)
  67
  68 inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Sin.con" as lemma.
  69
  70 inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Cos.con" as lemma.
  71
  72 (*#*
  73 The rules for the derivative of the sine and cosine function; we begin by proving that their defining sequences can be expressed in terms of one another.
  74 *)
  75
  76 inline procedural "cic:/CoRN/transc/Trigonometric/cos_sin_seq.con" as lemma.
  77
  78 inline procedural "cic:/CoRN/transc/Trigonometric/sin_cos_seq.con" as lemma.
  79
  80 inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Sin.con" as lemma.
  81
  82 inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Cos.con" as lemma.
  83
  84 (* UNEXPORTED
  85 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
  86 *)
  87
  88 (* UNEXPORTED
  89 Hint Resolve Continuous_Sin Continuous_Cos: continuous.
  90 *)
  91
  92 (* UNEXPORTED
  93 Section Sine_of_Sum
  94 *)
  95
  96 (*#*
  97 We now prove the rule for the sine and cosine of the sum.  These rules
  98 have to be proved first as functional equalities, which is why we also
  99 state the results in a function form (which we won't do in other
 100 situations).
 101
 102 %\begin{convention}% Let:
 103  - [F := fun y => Sine[o] (FId{+} [-C-]y)];
 104  - [G := fun y => (Sine{*} [-C-] (Cos y)) {+} (Cosine{*} [-C-] (Sin y))].
 105
 106 %\end{convention}%
 107 *)
 108
 109 (* begin hide *)
 110
 111 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 112
 113 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 114
 115 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F'.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 116
 117 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G'.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
 118
 119 (* end hide *)
 120
 121 (* UNEXPORTED
 122 Opaque Sine Cosine.
 123 *)
 124
 125 (* UNEXPORTED
 126 Opaque FAbs.
 127 *)
 128
 129 (* UNEXPORTED
 130 Transparent FAbs.
 131 *)
 132
 133 (* UNEXPORTED
 134 Opaque FAbs.
 135 *)
 136
 137 (* UNEXPORTED
 138 Transparent FAbs.
 139 *)
 140
 141 (* UNEXPORTED
 142 Opaque FAbs.
 143 *)
 144
 145 (* UNEXPORTED
 146 Transparent FAbs.
 147 *)
 148
 149 (* UNEXPORTED
 150 Opaque FAbs.
 151 *)
 152
 153 (* UNEXPORTED
 154 Transparent FAbs.
 155 *)
 156
 157 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_lft.con" as lemma.
 158
 159 (* UNEXPORTED
 160 Opaque FAbs.
 161 *)
 162
 163 (* UNEXPORTED
 164 Transparent FAbs.
 165 *)
 166
 167 (* UNEXPORTED
 168 Opaque FAbs.
 169 *)
 170
 171 (* UNEXPORTED
 172 Transparent FAbs.
 173 *)
 174
 175 (* UNEXPORTED
 176 Opaque FAbs.
 177 *)
 178
 179 (* UNEXPORTED
 180 Transparent FAbs.
 181 *)
 182
 183 (* UNEXPORTED
 184 Opaque FAbs.
 185 *)
 186
 187 (* UNEXPORTED
 188 Transparent FAbs.
 189 *)
 190
 191 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_rht.con" as lemma.
 192
 193 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_eq.con" as lemma.
 194
 195 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_lft.con" as lemma.
 196
 197 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con" as lemma.
 198
 199 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con" as lemma.
 200
 201 (* UNEXPORTED
 202 End Sine_of_Sum
 203 *)
 204
 205 (* UNEXPORTED
 206 Opaque Sine Cosine.
 207 *)
 208
 209 inline procedural "cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con" as lemma.
 210
 211 (* UNEXPORTED
 212 End Sine_and_Cosine
 213 *)
 214