Top File of PVS complex_alt Library

 
%------------------------------------------------------------------------------
% Complex Numbers (an alternative version)
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            14/06/09  Initial Version
%     Version 1.1            16/03/11  Additional rewrites added (DRL)
%
% This alternative formulation of the complex numbers integrates with
% the standard PVS decision procedures. The technique is to auto-rewrite
% complex equalities, such as z1 = z2 as the pair of rules:
%
% Re(z1) = Re(z2) & Im(Z1) = Im(z2)
%
%------------------------------------------------------------------------------
top: THEORY

BEGIN

  IMPORTING complex_types,  % Type definitions and basic arithmetic
            polar,          % Polar coordinates
            complex_lnexp,  % complex exp/ln
            complex_sqrt,   % complex sqrt
            complex_fun_ops % Functions [T->complex]

END top

The tag identifies links that are outside the NASA domain