|
%------------------------------------------------------------------------------
% Basic Arithmetic (including conjugation) on Complex Numbers.
%
% Author: David Lester, Manchester University & NIA
%
% Version 1.0 5/29/04 Initial version (DRL)
%
% Narkawicz 12/2013 +
%------------------------------------------------------------------------------
arithmetic: THEORY
BEGIN
IMPORTING complex_types
z,z1,z2: VAR complex
x : VAR real
n0z : VAR nzcomplex
complex_is_Re_Im : LEMMA z = Re(z) + Im(z)*i
complex_is_0_Re_Im : LEMMA z = 0 IFF (Re(z) = 0 AND Im(z) = 0)
complex_is_ne_0_Re_Im : LEMMA z /= 0 IFF (Re(z) /= 0 OR Im(z) /= 0)
complex_diff_eq_0 : LEMMA z1=z2 IFF z1-z2=0
conjugate(z):complex = Re(z) - Im(z)*i
sq_abs_def : LEMMA z * conjugate(z) = Re(z)*Re(z) + Im(z)*Im(z)
conjugate_nz : LEMMA conjugate(n0z) /= 0
sq_abs_realpred : LEMMA real_pred(z*conjugate(z)) %% RWB
AUTO_REWRITE+ sq_abs_realpred
nz_sq_abs_pos : LEMMA n0z*conjugate(n0z) > 0
sq_abs_nonneg : LEMMA z*conjugate(z) >= 0
Re_real : LEMMA Re(x) = x
Im_real : LEMMA Im(x) = 0
Re_imag : LEMMA Re(x*i) = 0
Im_imag : LEMMA Im(x*i) = x
Re_neg : LEMMA Re(-z) = -Re(z)
Im_neg : LEMMA Im(-z) = -Im(z)
Re_plus : LEMMA Re(z1+z2) = Re(z1)+Re(z2)
Im_plus : LEMMA Im(z1+z2) = Im(z1)+Im(z2)
Re_minus : LEMMA Re(z1-z2) = Re(z1)-Re(z2)
Im_minus : LEMMA Im(z1-z2) = Im(z1)-Im(z2)
Re_times : LEMMA Re(z1*z2) = Re(z1)*Re(z2) - Im(z1)*Im(z2)
Im_times : LEMMA Im(z1*z2) = Im(z1)*Re(z2) + Re(z1)*Im(z2)
Re_div : LEMMA Re(z/n0z) = (Re(z)*Re(n0z) + Im(z)*Im(n0z))/
(n0z*conjugate(n0z))
Im_div : LEMMA Im(z/n0z) = (Im(z)*Re(n0z) - Re(z)*Im(n0z))/
(n0z*conjugate(n0z))
plus_conjugate : LEMMA z + conjugate(z) = 2*Re(z)
minus_conjugate : LEMMA z - conjugate(z) = 2*Im(z)*i
conjugate_plus : LEMMA conjugate(z1+z2) = conjugate(z1) + conjugate(z2)
conjugate_neg : LEMMA conjugate(-z) = -conjugate(z)
conjugate_minus : LEMMA conjugate(z1-z2) = conjugate(z1) - conjugate(z2)
conjugate_times : LEMMA conjugate(z1*z2) = conjugate(z1) * conjugate(z2)
conjugate_inv : LEMMA conjugate(1/n0z) = 1/conjugate(n0z)
conjugate_div : LEMMA conjugate(x/n0z) = conjugate(x) / conjugate(n0z)
END arithmetic
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
