matita/contribs/CoRN-Decl/transc/Trigonometric.ma

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