]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
update in delayed_updating
[helm.git] / matita / 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