|
trig_rew: THEORY
BEGIN
%-----------------------------------------------------------------------------
%
% Experimental auto-rewrite-theory background trigonometry library
%
% Users should be able to issue
%
% (auto-rewrite_theory "trig_rew")
%
% at the beginning of a proof to automatically simplify formulas
%
%-----------------------------------------------------------------------------
IMPORTING trig_basic
a,b,c,d : VAR real
nnc : VAR nonneg_real
j,k,kk : VAR integer
n: VAR nat
% cos2 : LEMMA sq(cos(a)) = 1 - sq(sin(a))
tr_rew1 : LEMMA cos(0) = 1
tr_rew2 : LEMMA sin(0) = 0
tr_rew3 : LEMMA sin(pi/2) = 1
tr_rew4 : LEMMA cos(pi/2) = 0
tr_rew5 : LEMMA tan(0)=0
tr_rew6 : LEMMA sin(pi) = 0
tr_rew7 : LEMMA cos(pi) = -1
tr_rew8 : LEMMA tan(pi) = 0
tr_rew9 : LEMMA sin(3*pi/2) = -1
tr_rew10 : LEMMA cos(3*pi/2) = 0
tr_rew11 : LEMMA sin(2*pi) = 0
tr_rew12 : LEMMA cos(2*pi) = 1
tr_rew13 : LEMMA tan(2*pi) = 0
tr_rew14 : LEMMA sin(pi/2 - a) = cos(a)
tr_rew15 : LEMMA cos(pi/2 - a) = sin(a)
tr_rew16 : LEMMA sin(k*pi) = 0
tr_rew17 : LEMMA cos(2*k*pi) = 1
% tr_rew18 : LEMMA cos(k*pi) = (-1)^(k)
% tr_rew19 : LEMMA sin(k*pi + pi/2) = (-1)^k
tr_rew20 : LEMMA tan(k*pi) = 0
tr_rew22 : LEMMA sin(-a) = -sin(a)
tr_rew23 : LEMMA cos(-a) = cos(a)
tr_rew24 : LEMMA FORALL(a:(Tan?)): tan(-a) = -tan(a)
END trig_rew
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
